Fix arithmetic rewriter for exponential (#3688)

1 files changed, 10 insertions, 4 deletions

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index a1264c612..d8dd2cf58 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -390,12 +390,18 @@ RewriteResponse ArithRewriter::postRewriteTranscendental(TNode t) {
       }else{          
         return RewriteResponse(REWRITE_DONE, t);
       }
-    }else if(t[0].getKind() == kind::PLUS ){
+    }
+    else if (t[0].getKind() == kind::PLUS)
+    {
       std::vector<Node> product;
-      for( unsigned i=0; i<t[0].getNumChildren(); i++ ){
-        product.push_back(nm->mkNode(kind::EXPONENTIAL, t[0][i]));
+      for (const Node tc : t[0])
+      {
+        product.push_back(nm->mkNode(kind::EXPONENTIAL, tc));
       }
-      return RewriteResponse(REWRITE_AGAIN, nm->mkNode(kind::MULT, product));
+      // We need to do a full rewrite here, since we can get exponentials of
+      // constants, e.g. when we are rewriting exp(2 + x)
+      return RewriteResponse(REWRITE_AGAIN_FULL,
+                             nm->mkNode(kind::MULT, product));
     }
   }
     break;