From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Tue, 4 Jan 2022 17:35:49 +0000 (-0600)
Subject: Fix int blaster (#7856)
X-Git-Tag: cvc5-1.0.0~607
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=480affdf43c9872580697f4a4853c2a85bb4ed57;p=cvc5.git

Fix int blaster (#7856)
---

diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
index ec76d82f9..b761a5dcd 100644
--- 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 6009c020d..fa3bd1cf8 100644
--- 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
index 000000000..7480783c9
--- /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)