what4: Don't annotate bound variables

GaloisInc · Dec 6, 2023 · be3e8b1 · be3e8b1
1 parent 076f49b
commit be3e8b1
Showing 1 changed file with 3 additions and 0 deletions.
diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs
@@ -1630,6 +1630,7 @@ instance IsExprBuilder (ExprBuilder t st fs) where
 
   annotateTerm sym e =
     case e of
+      BoundVarExpr (bvarId -> n) -> return (n, e)
       NonceAppExpr (nonceExprApp -> Annotation _ n _) -> return (n, e)
       _ -> do
         let tpr = exprType e
@@ -1639,11 +1640,13 @@ instance IsExprBuilder (ExprBuilder t st fs) where
 
   getAnnotation _sym e =
     case e of
+      BoundVarExpr (bvarId -> n) -> Just n
       NonceAppExpr (nonceExprApp -> Annotation _ n _) -> Just n
       _ -> Nothing
 
   getUnannotatedTerm _sym e =
     case e of
+      BoundVarExpr {} -> Just e
       NonceAppExpr (nonceExprApp -> Annotation _ _ x) -> Just x
       _ -> Nothing