From 7d57ea14ee0bd1ffc4979dfe25de7fd91a48aedf Mon Sep 17 00:00:00 2001
From: Yoni Zohar <yoni206@gmail.com>
Date: Fri, 6 Oct 2023 16:05:31 +0300
Subject: [PATCH] fix

---
 src/preprocessing/passes/int_to_bv.cpp                |  6 +++++-
 test/regress/cli/CMakeLists.txt                       |  1 +
 test/regress/cli/regress0/bv/int_to_bv_10080_ite.smt2 | 10 ++++++++++
 3 files changed, 16 insertions(+), 1 deletion(-)
 create mode 100644 test/regress/cli/regress0/bv/int_to_bv_10080_ite.smt2

diff --git a/src/preprocessing/passes/int_to_bv.cpp b/src/preprocessing/passes/int_to_bv.cpp
index aa02b45fc88..0e275614c37 100644
--- 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
index 7110a6bd76c..85fcc53d3e4 100644
--- 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
new file mode 100644
index 00000000000..41cb6557150
--- /dev/null
+++ 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)