From 480affdf43c9872580697f4a4853c2a85bb4ed57 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Tue, 4 Jan 2022 11:35:49 -0600 Subject: [PATCH] Fix int blaster (#7856) --- src/theory/bv/int_blaster.cpp | 9 +++++++-- test/regress/CMakeLists.txt | 1 + test/regress/regress1/bv2int-make-binary.smt2 | 5 +++++ 3 files changed, 13 insertions(+), 2 deletions(-) create mode 100644 test/regress/regress1/bv2int-make-binary.smt2 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 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) -- 2.30.2