Fix int blaster (#7856)

diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
index ec76d82f9026bcefcdc570a5789789b7bc5ec5d1..b761a5dcdc5687c8b88116469330c65486c10b4f 100644 (file)
--- a/src/theory/bv/int_blaster.cpp
+++ b/src/theory/bv/int_blaster.cpp
@@ -215,12 +215,16 @@ Node IntBlaster::intBlast(Node n,
           std::vector<Node> translated_children;
           if (current.getKind() == kind::APPLY_UF)
           {
+            Assert(d_intblastCache.find(current.getOperator())
+                   != d_intblastCache.end());
             translated_children.push_back(
                 d_intblastCache[current.getOperator()]);
           }
-          for (uint64_t i = 0; i < currentNumChildren; i++)
+          for (const Node& cc : current)
           {
-            translated_children.push_back(d_intblastCache[current[i]]);
+            Node ccb = makeBinary(cc);
+            Assert(d_intblastCache.find(ccb) != d_intblastCache.end());
+            translated_children.push_back(d_intblastCache[ccb]);
           }
           translation =
               translateWithChildren(current, translated_children, lemmas);
@@ -234,6 +238,7 @@ Node IntBlaster::intBlast(Node n,
       }
     }
   }
+  Assert(d_intblastCache.find(n) != d_intblastCache.end());
   return d_intblastCache[n].get();
 }
 

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 6009c020da784f7b4fec89eac5ca861462c41469..fa3bd1cf8a293a74666dd02e844d4f1886c9cefd 100644 (file)
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -1648,6 +1648,7 @@ set(regress_1_tests
   regress1/bags/union_max1.smt2
   regress1/bags/union_max2.smt2
   regress1/bv2int-isabelle.smt2
+  regress1/bv2int-make-binary.smt2
   regress1/bv/bench_38.delta.smt2
   regress1/bv/bug787.smt2
   regress1/bv/bug_extract_mult_leading_bit.smt2

diff --git a/test/regress/regress1/bv2int-make-binary.smt2 b/test/regress/regress1/bv2int-make-binary.smt2
new file mode 100644 (file)
index 0000000..7480783
--- /dev/null
+++ b/test/regress/regress1/bv2int-make-binary.smt2
@@ -0,0 +1,5 @@
+(set-logic QF_BV)
+(set-info :status sat)
+(declare-const x (_ BitVec 2))
+(assert (= (_ bv0 256) (bvand (_ bv131070 256) ((_ zero_extend 128) ((_ zero_extend 126) x)))))
+(check-sat)