From 85d2571c1b269051ff6f45fa11e7ce90185a4e52 Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Tue, 11 Feb 2025 21:28:31 -0500
Subject: [PATCH] Preserve abstract values in `annotateTerm`

---
 what4/src/What4/Expr/Builder.hs | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs
index 5ec400ee..b5457a3c 100644
--- 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