what4: Don't annotate {Nonce,}AppExprs

These constructors already carry `Nonce`s, adding another layer can only
hurt performance by adding allocations/indirections, and especially,
disabling important rewrites.

what4/src/What4/Expr/Builder.hs

@@ -2044,18 +2044,22 @@ 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 =

what4/test/ExprBuilderSMTLib2.hs

@@ -1164,7 +1164,7 @@ testUnsafeSetAbstractValue2 = testCase "test unsafeSetAbstractValue2" $
     e2A <- freshConstant sym (userSymbol' "x2A") (BaseBVRepr w)
     e2B <- freshConstant sym (userSymbol' "x2B") (BaseBVRepr w)
     e2C <- bvAdd sym e2A e2B
-    (_, e2C') <- annotateTerm sym $ unsafeSetAbstractValue (WUB.BVDArith (WUBA.range w 2 2)) e2C
+    e2C' <- opacify sym $ unsafeSetAbstractValue (WUB.BVDArith (WUBA.range w 2 2)) e2C
     unsignedBVBounds e2C' @?= Just (2, 2)
     e2D <- bvAdd sym e2C' =<< bvOne sym w
     case asBV e2D of