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

1 files changed, 7 insertions, 4 deletions

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());
       }