Preserve abstract values in annotateTerm

GaloisInc · Feb 12, 2025 · 85d2571 · 85d2571
1 parent eef72a0
commit 85d2571
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs
@@ -2052,7 +2052,8 @@ instance IsExprBuilder (ExprBuilder t st fs) where
         let tpr = exprType e
         n <- sbFreshIndex sym
         e' <- sbNonceExpr sym (Annotation tpr n e)
-        return (n, e')
+        let e'' = unsafeSetAbstractValue (exprAbsValue e') e'
+        return (n, e'')
 
   getAnnotation _sym e =
     case e of