From 47f003828a8ba0cd8edd362accaef8b2449b0c46 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
Date: Wed, 5 Aug 2020 20:55:00 +0200
Subject: [PATCH] Improve error message for unsupported exponents (#4852)

We have had a few issues where essentially users misinterpreted the error message about which types of exponents are supported for (^ base exp). Given that this is rewritten to a multiplication of length exp, we only support reasonably small natural numbers.
This PR improves the error message.
Fixes #4692
---
 src/theory/arith/arith_rewriter.cpp      | 11 +++++++----
 test/regress/CMakeLists.txt              |  1 +
 test/regress/regress1/arith/bug716.1.cvc |  2 +-
 test/regress/regress1/arith/bug716.2.cvc |  6 ++++++
 4 files changed, 15 insertions(+), 5 deletions(-)
 create mode 100644 test/regress/regress1/arith/bug716.2.cvc

diff --git a/src/theory/arith/arith_rewriter.cpp b/src/theory/arith/arith_rewriter.cpp
index 188ef47e6..f0e0487a0 100644
--- a/src/theory/arith/arith_rewriter.cpp
+++ b/src/theory/arith/arith_rewriter.cpp
@@ -229,8 +229,9 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
           if(exp.sgn() == 0){
             return RewriteResponse(REWRITE_DONE, mkRationalNode(Rational(1)));
           }else if(exp.sgn() > 0 && exp.isIntegral()){
-            CVC4::Rational r(INT_MAX);
-            if( exp<r ){
+            CVC4::Rational r(expr::NodeValue::MAX_CHILDREN);
+            if (exp <= r)
+            {
               unsigned num = exp.getNumerator().toUnsignedInt();
               if( num==1 ){
                 return RewriteResponse(REWRITE_AGAIN, base);
@@ -249,8 +250,10 @@ RewriteResponse ArithRewriter::postRewriteTerm(TNode t){
 
         // Todo improve the exception thrown
         std::stringstream ss;
-        ss << "The POW(^) operator can only be used with a natural number ";
-        ss << "in the exponent.  Exception occurred in:" << std::endl;
+        ss << "The exponent of the POW(^) operator can only be a positive "
+              "integral constant below "
+           << (expr::NodeValue::MAX_CHILDREN + 1) << ". ";
+        ss << "Exception occurred in:" << std::endl;
         ss << "  " << t;
         throw LogicException(ss.str());
       }
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index f9840e552..0b0da8e93 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1247,6 +1247,7 @@ set(regress_1_tests
   regress1/arith/bug547.1.smt2
   regress1/arith/bug716.0.smt2
   regress1/arith/bug716.1.cvc
+  regress1/arith/bug716.2.cvc
   regress1/arith/div.03.smt2
   regress1/arith/div.06.smt2
   regress1/arith/div.08.smt2
diff --git a/test/regress/regress1/arith/bug716.1.cvc b/test/regress/regress1/arith/bug716.1.cvc
index d9330c727..854062beb 100644
--- a/test/regress/regress1/arith/bug716.1.cvc
+++ b/test/regress/regress1/arith/bug716.1.cvc
@@ -1,4 +1,4 @@
-% EXPECT: The POW(^) operator can only be used with a natural number in the exponent.  Exception occurred in:
+% EXPECT: The exponent of the POW(^) operator can only be a positive integral constant below 67108864. Exception occurred in:
 % EXPECT:   2 ^ x
 % EXIT: 1
 x: INT;
diff --git a/test/regress/regress1/arith/bug716.2.cvc b/test/regress/regress1/arith/bug716.2.cvc
new file mode 100644
index 000000000..eb9b733fc
--- /dev/null
+++ b/test/regress/regress1/arith/bug716.2.cvc
@@ -0,0 +1,6 @@
+% EXPECT: The exponent of the POW(^) operator can only be a positive integral constant below 67108864. Exception occurred in:
+% EXPECT:   x ^ 67108864
+% EXIT: 1
+x: INT;
+ASSERT x^67108864 = 8;
+QUERY x=3;
-- 
2.30.2