progress

yoni206 · May 2, 2024 · 22e58c7 · 22e58c7
1 parent 8a4bc42
commit 22e58c7
Show file tree

Hide file tree

Showing 3 changed files with 3 additions and 1 deletion.
diff --git a/src/preprocessing/passes/bv_to_int.cpp b/src/preprocessing/passes/bv_to_int.cpp
@@ -49,6 +49,7 @@ BVToInt::BVToInt(PreprocessingPassContext* preprocContext)
 PreprocessingPassResult BVToInt::applyInternal(
     AssertionPipeline* assertionsToPreprocess)
 {
+  Trace("bv-to-int-debug") << "entering applyInternal" << std::endl;
   // vector of boolean nodes for additional constraints
   // this will always contain range constraints
   // and for options::SolveBVAsIntMode::BITWISE, it will

diff --git a/src/theory/bv/int_blaster.cpp b/src/theory/bv/int_blaster.cpp
@@ -975,7 +975,7 @@ void IntBlaster::collectQuantificationData(Node n) {
     }
     if (n.getNumChildren() > 0) {
       for (Node child : n) {
-        Assert(d_quantifiedVariables.find(child) != d_quantifiedVariables.end());
+        Assert(d_quantifiedVariables.find(child) != d_quantifiedVariables.end()) << child;
         std::unordered_set<Node> varsOfChild = d_quantifiedVariables[child];
         qfvarsOfChildren.insert(varsOfChild.begin(), varsOfChild.end());
       }

diff --git a/test/regress/cli/regress0/bv/bv_to_int_8798.smt2 b/test/regress/cli/regress0/bv/bv_to_int_8798.smt2
@@ -1,6 +1,7 @@
 ; EXPECT: sat
 (set-logic ALL)
 (set-option :solve-bv-as-int iand)
+(set-option :mbqi true)
 (declare-sort byte 0)
 (declare-fun to_rep1 (byte) (_ BitVec 8))
 (assert (forall ((a (Array Int byte))) (exists ((temp Int)) (= (to_rep1 (select a temp)) (to_rep1 (select a (+ temp 1)))))))