Preserve abstract values in opacify

GaloisInc · Feb 12, 2025 · eef72a0 · eef72a0
1 parent 862a865
commit eef72a0
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs
@@ -2070,7 +2070,9 @@ instance IsExprBuilder (ExprBuilder t st fs) where
   opacify sym e =
     case e of
       NonceAppExpr (nonceExprApp -> Opaque _ _) -> return e
-      _ -> sbNonceExpr sym (Opaque (exprType e) e)
+      _ -> do
+        e' <- sbNonceExpr sym (Opaque (exprType e) e)
+        pure (unsafeSetAbstractValue (exprAbsValue e') e')
 
   clarify _sym e =
     case e of