From a3199cb5903c48665756f553c1cf3b20f02d8a2d Mon Sep 17 00:00:00 2001
From: Langston Barrett <langston.barrett@gmail.com>
Date: Wed, 6 Dec 2023 11:34:58 -0500
Subject: [PATCH] what4: Don't annotate `{Nonce,}AppExpr`s

---
 what4/src/What4/Expr/Builder.hs | 8 +++++---
 1 file changed, 5 insertions(+), 3 deletions(-)

diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs
index 258562c9..778d3328 100644
--- a/what4/src/What4/Expr/Builder.hs
+++ b/what4/src/What4/Expr/Builder.hs
@@ -1630,9 +1630,10 @@ instance IsExprBuilder (ExprBuilder t st fs) where
 
   annotateTerm sym e =
     case e of
+      AppExpr (appExprId -> n) -> return (n, e)
       BoundVarExpr (bvarId -> n) -> return (n, e)
-      NonceAppExpr (nonceExprApp -> Annotation _ n _) -> return (n, e)
-      _ -> do
+      NonceAppExpr (nonceExprId -> n) -> return (n, e)
+      _ -> do  -- literals
         let tpr = exprType e
         n <- sbFreshIndex sym
         e' <- sbNonceExpr sym (Annotation tpr n e)
@@ -1640,8 +1641,9 @@ instance IsExprBuilder (ExprBuilder t st fs) where
 
   getAnnotation _sym e =
     case e of
+      AppExpr (appExprId -> n) -> Just n
       BoundVarExpr (bvarId -> n) -> Just n
-      NonceAppExpr (nonceExprApp -> Annotation _ n _) -> Just n
+      NonceAppExpr (nonceExprId -> n) -> Just n
       _ -> Nothing
 
   getUnannotatedTerm _sym e =