what4: Don't annotate {Nonce,}AppExprs

GaloisInc · Dec 6, 2023 · a3199cb · a3199cb
1 parent e46dff4
commit a3199cb
Showing 1 changed file with 5 additions and 3 deletions.
diff --git a/what4/src/What4/Expr/Builder.hs b/what4/src/What4/Expr/Builder.hs
@@ -1630,18 +1630,20 @@ 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)
         return (n, e')
 
   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 =