fix

yoni206 · Oct 6, 2023 · 7d57ea1 · 7d57ea1
1 parent c926d61
commit 7d57ea1
Show file tree

Hide file tree

Showing 3 changed files with 16 additions and 1 deletion.
diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
@@ -47,6 +47,7 @@ using namespace cvc5::internal::theory;
 namespace {
 
 bool childrenTypesChanged(Node n, NodeMap& cache) {
+  Trace("int-to-bv-debug") << "childrenTypesChanged: " << n << std::endl;
   for (Node child : n) {
     TypeNode originalType = child.getType();
     TypeNode newType = cache[child].getType();
@@ -206,9 +207,12 @@ Node IntToBV::intToBV(TNode n, NodeMap& cache)
           }
         }
       }
+      Trace("int-to-bv-debug") << "tn: " << tn << std::endl;
 
-      if (tn.isInteger() && newKind == current.getKind())
+      if (tn.isInteger() && newKind != Kind::ITE
+          && newKind == current.getKind())
       {
+        Trace("int-to-bv-debug") << "current: " << current << std::endl;
         std::stringstream ss;
         ss << "Cannot translate the operator " << current.getKind()
            << " to a bit-vector operator. Remove option `--solve-int-as-bv`.";

diff --git a/test/regress/cli/CMakeLists.txt b/test/regress/cli/CMakeLists.txt
@@ -469,6 +469,7 @@ set(regress_0_tests
   regress0/bv/inequality03.smt2
   regress0/bv/inequality04.smt2
   regress0/bv/inequality05.smt2
+  regress0/bv/int_to_bv_10080_ite.smt2
   regress0/bv/int_to_bv_err_on_demand_1.smt2
   regress0/bv/int_to_bv_model.smt2
   regress0/bv/int_to_bv_model2.smt2

diff --git a/test/regress/cli/regress0/bv/int_to_bv_10080_ite.smt2 b/test/regress/cli/regress0/bv/int_to_bv_10080_ite.smt2
@@ -0,0 +1,10 @@
+; EXPECT: sat
+; COMMAND-LINE: --solve-int-as-bv=8
+(set-logic QF_LIA)
+(declare-const x Int)
+(declare-const y Int)
+(declare-const z Int)
+; (assert (not (= x 0)))
+(assert (> y 0))
+(assert (= z (ite (> x y) x (+ x y))))
+(check-sat)