1 files changed, 6 insertions, 0 deletions
diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 6eda6283c..5baaaf317 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -255,6 +255,12 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
             }
           }
         }
+        else if (t[0].getKind() == kind::CONST_RATIONAL
+                 && t[0].getConst<Rational>().getNumerator().toUnsignedInt() == 2)
+        {
+          return RewriteResponse(
+              REWRITE_DONE, NodeManager::currentNM()->mkNode(kind::POW2, t[1]));
+        }
 
         // Todo improve the exception thrown
         std::stringstream ss;