[IntToBV] Add check for unsupported operators (#8949)

Fixes #8935. This adds a check for unsupported operators in the IntToBV
preprocessing pass and improves error messages. Previously, operators
such as str.to_int, which return an integer but do not take an integer
as an argument were not detected as unsupported.

diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index e8ec68b884448e6273d7796c957d0eae4f799f3a..f3b6ab4f764db7e9c27ef55320e46cd5b561980d 100644 (file)
--- a/src/preprocessing/passes/int_to_bv.cpp
+++ b/src/preprocessing/passes/int_to_bv.cpp
@@ -30,6 +30,7 @@
 #include "options/smt_options.h"
 #include "preprocessing/assertion_pipeline.h"
 #include "preprocessing/preprocessing_pass_context.h"
+#include "smt/logic_exception.h"
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 #include "util/bitvector.h"
@@ -179,12 +180,14 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache)
           case kind::ITE: break;
           default:
             if (childrenTypesChanged(current, cache)) {
-              throw TypeCheckingExceptionPrivate(
-                  current,
-                  string("Cannot translate to BV: ") + current.toString());
+              std::stringstream ss;
+              ss << "Cannot translate " << current
+                 << " to a bit-vector term. Remove option `--solve-int-as-bv`.";
+              throw LogicException(ss.str());
             }
             break;
         }
+
         for (size_t i = 0, csize = children.size(); i < csize; ++i)
         {
           TypeNode type = children[i].getType();
@@ -202,6 +205,14 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache)
           }
         }
       }
+
+      if (tn.isInteger() && newKind == current.getKind())
+      {
+        std::stringstream ss;
+        ss << "Cannot translate the operator " << current.getKind()
+           << " to a bit-vector operator. Remove option `--solve-int-as-bv`.";
+        throw LogicException(ss.str());
+      }
       NodeBuilder builder(newKind);
       if (current.getMetaKind() == kind::metakind::PARAMETERIZED) {
         builder << current.getOperator();

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
index c7ee7ca1d337982469834026b9e4e3711f746e82..a39b7b344f9d72c85a6a7798b91d0cf40350e7b6 100644 (file)
--- a/test/regress/cli/CMakeLists.txt
+++ b/test/regress/cli/CMakeLists.txt
@@ -733,6 +733,7 @@ set(regress_0_tests
   regress0/ineq_basic.smtv1.smt2
   regress0/ineq_slack.smtv1.smt2
   regress0/int-to-bv/basic.smt2
+  regress0/int-to-bv/issue8935-unsupported-operators.smt2
   regress0/int-to-bv/neg-consts.smt2
   regress0/int-to-bv/not-enough-bits.smt2
   regress0/int-to-bv/overflow.smt2

diff --git a/test/regress/cli/regress0/int-to-bv/issue8935-unsupported-operators.smt2 b/test/regress/cli/regress0/int-to-bv/issue8935-unsupported-operators.smt2
new file mode 100644 (file)
index 0000000..0fac589
--- /dev/null
+++ b/test/regress/cli/regress0/int-to-bv/issue8935-unsupported-operators.smt2
@@ -0,0 +1,7 @@
+; EXPECT: (error "Cannot translate the operator STRING_STOI to a bit-vector operator. Remove option `--solve-int-as-bv`.")
+; EXIT: 1
+(set-option :solve-int-as-bv 1)
+(set-logic ALL)
+(declare-fun a () String)
+(assert (ite (= (- 1) (str.to_int a)) false true))
+(check-sat)