From 5f7eee9f639496ce4959206999f4576a7da32663 Mon Sep 17 00:00:00 2001
From: Andres Noetzli <andres.noetzli@gmail.com>
Date: Mon, 11 Jul 2022 10:57:22 -0700
Subject: [PATCH] [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.
---
 src/preprocessing/passes/int_to_bv.cpp          | 17 ++++++++++++++---
 test/regress/cli/CMakeLists.txt                 |  1 +
 .../issue8935-unsupported-operators.smt2        |  7 +++++++
 3 files changed, 22 insertions(+), 3 deletions(-)
 create mode 100644 test/regress/cli/regress0/int-to-bv/issue8935-unsupported-operators.smt2

diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index e8ec68b88..f3b6ab4f7 100644
--- 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 c7ee7ca1d..a39b7b344 100644
--- 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
index 000000000..0fac58919
--- /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)
-- 
2.30.2