Remove getUnannotatedTerm case for bound variables

GaloisInc · Dec 6, 2023 · e46dff4 · e46dff4
1 parent be3e8b1
commit e46dff4
Show file tree

Hide file tree

Showing 2 changed files with 2 additions and 2 deletions.
diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs
@@ -1646,7 +1646,6 @@ instance IsExprBuilder (ExprBuilder t st fs) where
 
   getUnannotatedTerm _sym e =
     case e of
-      BoundVarExpr {} -> Just e
       NonceAppExpr (nonceExprApp -> Annotation _ _ x) -> Just x
       _ -> Nothing
 

diff --git a/what4/src/What4/Interface.hs b/what4/src/What4/Interface.hs
@@ -691,7 +691,8 @@ class ( IsExpr (SymExpr sym), HashableF (SymExpr sym), HashableF (BoundVar sym)
   getAnnotation :: sym -> SymExpr sym tp -> Maybe (SymAnnotation sym tp)
 
   -- | Project the original, unannotated term from an annotated term.
-  --   This returns 'Nothing' for terms that do not have annotations.
+  --   This returns 'Nothing' for terms that do not have annotations,
+  --   or for terms that cannot be separated from their annotations.
   getUnannotatedTerm :: sym -> SymExpr sym tp -> Maybe (SymExpr sym tp)
 
   ----------------------------------------------------------------------