fixing bitvector bugs

* clauses shouldn't be erased when they could be a reason for outside propagation
* propagation of p and !p is ignored as this must lead to a conflict in the subtheory internally

52 files changed, 267 insertions, 88 deletions

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 41c0c4ac9..2eadbdf22 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -31,19 +31,26 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 using namespace BVMinisat;
 
-// purely debugging functions
-void printDebug2 (BVMinisat::Lit l) {
-  std::cout<< (sign(l) ? "-" : "") << var(l) + 1 << std::endl;
+namespace CVC4 {
+
+#define OUTPUT_TAG "bvminisat: [a=" << assumptions.size() << ",l=" << decisionLevel() << "] "
+
+std::ostream& operator << (std::ostream& out, const BVMinisat::Lit& l) {
+  out << (sign(l) ? "-" : "") << var(l) + 1;
+  return out;
 }
 
-void printDebug2 (BVMinisat::Clause& c) {
+std::ostream& operator << (std::ostream& out, const BVMinisat::Clause& c) {
   for (int i = 0; i < c.size(); i++) {
-    std::cout << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; 
+    if (i > 0) {
+      out << " ";
+    }
+    out << c[i];
   }
-  std::cout << std::endl;
+  return out;
 }
 
-
+}
 
 //=================================================================================================
 // Options:
@@ -243,7 +250,8 @@ bool Solver::satisfied(const Clause& c) const {
 //
 void Solver::cancelUntil(int level) {
     if (decisionLevel() > level){
-        for (int c = trail.size()-1; c >= trail_lim[level]; c--){
+      Debug("bvminisat::explain") << OUTPUT_TAG << " backtracking to " << level << std::endl;
+      for (int c = trail.size()-1; c >= trail_lim[level]; c--){
             Var      x  = var(trail[c]);
             assigns [x] = l_Undef;
             if (marker[x] == 2) marker[x] = 1;
@@ -502,6 +510,7 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
     trail.push_(p);
     if (decisionLevel() <= assumptions.size() && marker[var(p)] == 1) {
       if (notify) {
+        Debug("bvminisat::explain") << OUTPUT_TAG << "propagating " << p << std::endl;
         notify->notify(p);
       }
     }
@@ -757,6 +766,7 @@ lbool Solver::search(int nof_conflicts, UIP uip)
             if (assumption) {
               assert(decisionLevel() < assumptions.size());
               analyzeFinal(p, conflict);
+              Debug("bvminisat::search") << OUTPUT_TAG << " conflict on assumptions " << std::endl;
               return l_False;
             }
             
@@ -779,17 +789,24 @@ lbool Solver::search(int nof_conflicts, UIP uip)
             // NO CONFLICT
             if (decisionLevel() > assumptions.size() && nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){
                 // Reached bound on number of conflicts:
+                Debug("bvminisat::search") << OUTPUT_TAG << " restarting " << std::endl;
                 progress_estimate = progressEstimate();
                 cancelUntil(assumptions.size());
                 return l_Undef; }
 
             // Simplify the set of problem clauses:
-            if (decisionLevel() == 0 && !simplify())
+            if (decisionLevel() == 0 && !simplify()) {
+                Debug("bvminisat::search") << OUTPUT_TAG << " base level conflict, we're unsat" << std::endl;
                 return l_False;
+            }
 
-            if (learnts.size()-nAssigns() >= max_learnts)
+            // We can't erase clauses if there is unprocessed assumptions, there might be some
+            // propagationg we need to redu
+            if (decisionLevel() >= assumptions.size() && learnts.size()-nAssigns() >= max_learnts) {
                 // Reduce the set of learnt clauses:
+                Debug("bvminisat::search") << OUTPUT_TAG << " cleaning up database" << std::endl;
                 reduceDB();
+            }
 
             Lit next = lit_Undef;
             while (decisionLevel() < assumptions.size()){
@@ -800,6 +817,7 @@ lbool Solver::search(int nof_conflicts, UIP uip)
                     newDecisionLevel();
                 }else if (value(p) == l_False){
                     analyzeFinal(~p, conflict);
+                    Debug("bvminisat::search") << OUTPUT_TAG << " assumption false, we're unsat" << std::endl;
                     return l_False;
                 }else{
                     marker[var(p)] = 2;
@@ -811,6 +829,7 @@ lbool Solver::search(int nof_conflicts, UIP uip)
             if (next == lit_Undef){
 
                 if (only_bcp) {
+                  Debug("bvminisat::search") << OUTPUT_TAG << " only bcp, skipping rest of the problem" << std::endl;
                   return l_True;
                 }
 
@@ -818,9 +837,11 @@ lbool Solver::search(int nof_conflicts, UIP uip)
                 decisions++;
                 next = pickBranchLit();
 
-                if (next == lit_Undef)
+                if (next == lit_Undef) {
+                    Debug("bvminisat::search") << OUTPUT_TAG << " satisfiable" << std::endl;
                     // Model found:
                     return l_True;
+                }
             }
 
             // Increase decision level and enqueue 'next'
@@ -930,11 +951,16 @@ void Solver::explain(Lit p, std::vector<Lit>& explanation) {
   vec<Lit> queue;
   queue.push(p);
 
-  __gnu_cxx::hash_set<Var> visited;
+  Debug("bvminisat::explain") << OUTPUT_TAG << "starting explain of " << p << std::endl;
+
+      __gnu_cxx::hash_set<Var> visited;
   visited.insert(var(p));
   
   while(queue.size() > 0) {
     Lit l = queue.last();
+
+    Debug("bvminisat::explain") << OUTPUT_TAG << "processing " << l << std::endl;
+
     assert(value(l) == l_True);
     queue.pop();
     if (reason(var(l)) == CRef_Undef) {
diff --git a/src/theory/bv/bitblaster.cpp b/src/theory/bv/bitblaster.cpp
index d512847d5..5bb906841 100644
--- a/src/theory/bv/bitblaster.cpp
+++ b/src/theory/bv/bitblaster.cpp
@@ -337,7 +337,7 @@ Bitblaster::Statistics::~Statistics() {
 }
 
 bool Bitblaster::MinisatNotify::notify(prop::SatLiteral lit) {
-  return d_bv->storePropagation(d_cnf->getNode(lit), TheoryBV::SUB_BITBLAST);
+  return d_bv->storePropagation(d_cnf->getNode(lit), SUB_BITBLAST);
 };
 
 void Bitblaster::MinisatNotify::notify(prop::SatClause& clause) {
diff --git a/src/theory/bv/bv_subtheory.h b/src/theory/bv/bv_subtheory.h
index a8813b7aa..f8c763e3f 100644
--- a/src/theory/bv/bv_subtheory.h
+++ b/src/theory/bv/bv_subtheory.h
@@ -30,6 +30,27 @@ namespace CVC4 {
 namespace theory {
 namespace bv {
 
+enum SubTheory {
+  SUB_EQUALITY = 1,
+  SUB_BITBLAST = 2
+};
+
+inline std::ostream& operator << (std::ostream& out, SubTheory subtheory) {
+  switch (subtheory) {
+  case SUB_BITBLAST:
+    out << "BITBLASTER";
+    break;
+  case SUB_EQUALITY:
+    out << "EQUALITY";
+    break;
+  default:
+    Unreachable();
+    break;
+  }
+  return out;
+}
+
+
 const bool d_useEqualityEngine = true;
 const bool d_useSatPropagation = true;
 
diff --git a/src/theory/bv/bv_subtheory_bitblast.cpp b/src/theory/bv/bv_subtheory_bitblast.cpp
index ff0fc2b1a..334a704e9 100644
--- a/src/theory/bv/bv_subtheory_bitblast.cpp
+++ b/src/theory/bv/bv_subtheory_bitblast.cpp
@@ -79,7 +79,7 @@ bool BitblastSolver::addAssertions(const std::vector<TNode>& assertions, Theory:
   // propagation
   for (unsigned i = 0; i < assertions.size(); ++i) {
     TNode fact = assertions[i];
-    if (!d_bv->inConflict() && !d_bv->propagatedBy(fact, TheoryBV::SUB_BITBLAST)) {
+    if (!d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_BITBLAST)) {
       // Some atoms have not been bit-blasted yet
       d_bitblaster->bbAtom(fact);
       // Assert to sat
diff --git a/src/theory/bv/bv_subtheory_eq.cpp b/src/theory/bv/bv_subtheory_eq.cpp
index afb4a8b4a..cb08a1ad8 100644
--- a/src/theory/bv/bv_subtheory_eq.cpp
+++ b/src/theory/bv/bv_subtheory_eq.cpp
@@ -96,7 +96,7 @@ bool EqualitySolver::addAssertions(const std::vector<TNode>& assertions, Theory:
     TNode fact = assertions[i];
 
     // Notify the equality engine
-    if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, TheoryBV::TheoryBV::SUB_EQUALITY) ) {
+    if (d_useEqualityEngine && !d_bv->inConflict() && !d_bv->propagatedBy(fact, SUB_EQUALITY) ) {
       bool negated = fact.getKind() == kind::NOT;
       TNode predicate = negated ? fact[0] : fact;
       if (predicate.getKind() == kind::EQUAL) {
@@ -156,7 +156,7 @@ void EqualitySolver::NotifyClass::eqNotifyConstantTermMerge(TNode t1, TNode t2)
 }
 
 bool EqualitySolver::storePropagation(TNode literal) {
-  return d_bv->storePropagation(literal, TheoryBV::SUB_EQUALITY);
+  return d_bv->storePropagation(literal, SUB_EQUALITY);
 }
   
 void EqualitySolver::conflict(TNode a, TNode b) {
diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp
index 66f443d50..208ffba6c 100644
--- a/src/theory/bv/theory_bv.cpp
+++ b/src/theory/bv/theory_bv.cpp
@@ -77,15 +77,25 @@ void TheoryBV::preRegisterTerm(TNode node) {
   d_equalitySolver.preRegister(node); 
 }
 
+void TheoryBV::sendConflict() {
+  Assert(d_conflict);
+  if (d_conflictNode.isNull()) {
+    return;
+  } else {
+    BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
+    d_out->conflict(d_conflictNode);
+    d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
+    d_conflictNode = Node::null();
+  }
+}
+
 void TheoryBV::check(Effort e)
 {
   BVDebug("bitvector") << "TheoryBV::check(" << e << ")" << std::endl;
 
   // if we are already in conflict just return the conflict 
-  if (d_conflict) {
-    BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
-    d_out->conflict(d_conflictNode);
-    d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
+  if (inConflict()) {
+    sendConflict();
     return;
   }
   
@@ -98,20 +108,18 @@ void TheoryBV::check(Effort e)
     BVDebug("bitvector-assertions") << "TheoryBV::check assertion " << fact << "\n"; 
   }
 
-  // sending assertions to the equality solver first
-  bool ok = d_equalitySolver.addAssertions(new_assertions, e);
+  if (!inConflict()) {
+    // sending assertions to the equality solver first
+    d_equalitySolver.addAssertions(new_assertions, e);
+  }
   
-  if (ok) {
+  if (!inConflict()) {
     // sending assertions to the bitblast solver
-    ok = d_bitblastSolver.addAssertions(new_assertions, e); 
+    d_bitblastSolver.addAssertions(new_assertions, e);
   }
   
-  if (!ok) {
-    // output conflict 
-    Assert (d_conflict);
-    BVDebug("bitvector") << indent() << "TheoryBV::check(): conflict " << d_conflictNode;
-    d_out->conflict(d_conflictNode);
-    d_statistics.d_avgConflictSize.addEntry(d_conflictNode.getNumChildren());
+  if (inConflict()) {
+    sendConflict();
   }
 }
 
@@ -136,14 +144,20 @@ Node TheoryBV::getValue(TNode n) {
 void TheoryBV::propagate(Effort e) {
   BVDebug("bitvector") << indent() << "TheoryBV::propagate()" << std::endl;
 
-  if (d_conflict) {
+  if (inConflict()) {
     return;
   }
 
   // go through stored propagations
-  for (; d_literalsToPropagateIndex < d_literalsToPropagate.size(); d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
+  bool ok = true;
+  for (; d_literalsToPropagateIndex < d_literalsToPropagate.size() && ok; d_literalsToPropagateIndex = d_literalsToPropagateIndex + 1) {
     TNode literal = d_literalsToPropagate[d_literalsToPropagateIndex];
-    d_out->propagate(literal);
+    ok = d_out->propagate(literal);
+  }
+
+  if (!ok) {
+    BVDebug("bitvector::propagate") << indent() << "TheoryBV::propagate(): conflict from theory engine" << std::endl;
+    setConflict();
   }
 }
 
@@ -177,11 +191,11 @@ Theory::PPAssertStatus TheoryBV::ppAssert(TNode in, SubstitutionMap& outSubstitu
 
 bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 {
-  Debug("bitvector") << indent() << "TheoryBV::storePropagation(" << literal  << ")" << std::endl;
+  Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ")" << std::endl;
 
   // If already in conflict, no more propagation
   if (d_conflict) {
-    Debug("bitvector") << indent() << "TheoryBV::storePropagation(" << literal << "): already in conflict" << std::endl;
+    Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << "): already in conflict" << std::endl;
     return false;
   }
 
@@ -190,6 +204,13 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
   if (find != d_propagatedBy.end()) {
     return true;
   } else {
+    bool polarity = literal.getKind() != kind::NOT;
+    Node negatedLiteral = polarity ? literal.notNode() : (Node) literal[0];
+    find = d_propagatedBy.find(negatedLiteral);
+    if (find != d_propagatedBy.end() && (*find).second != subtheory) {
+      // Safe to ignore this one, subtheory should produce a conflict
+      return true;
+    }
     d_propagatedBy[literal] = subtheory;
   }
 
@@ -199,7 +220,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
 
   // If asserted, we might be in conflict
   if (hasSatValue && !satValue) {
-    Debug("bitvector-prop") << indent() << "TheoryBV::storePropagation(" << literal << ") => conflict" << std::endl;
+    Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ") => conflict" << std::endl;
     std::vector<TNode> assumptions;
     Node negatedLiteral = literal.getKind() == kind::NOT ? (Node) literal[0] : literal.notNode();
     assumptions.push_back(negatedLiteral);
@@ -209,7 +230,7 @@ bool TheoryBV::storePropagation(TNode literal, SubTheory subtheory)
   }
 
   // Nothing, just enqueue it for propagation and mark it as asserted already
-  Debug("bitvector-prop") << indent() << "TheoryBV::storePropagation(" << literal << ") => enqueuing for propagation" << std::endl;
+  Debug("bitvector::propagate") << indent() << "TheoryBV::storePropagation(" << literal << ", " << subtheory << ") => enqueuing for propagation" << std::endl;
   d_literalsToPropagate.push_back(literal);
 
   // No conflict
diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h
index f79b7ab71..a2cf39049 100644
--- a/src/theory/bv/theory_bv.h
+++ b/src/theory/bv/theory_bv.h
@@ -91,11 +91,6 @@ private:
   /** Index of the next literal to propagate */
   context::CDO<unsigned> d_literalsToPropagateIndex;
 
-  enum SubTheory {
-    SUB_EQUALITY = 1,
-    SUB_BITBLAST = 2
-  };
-
   /**
    * Keeps a map from nodes to the subtheory that propagated it so that we can explain it
    * properly.
@@ -127,12 +122,16 @@ private:
     return indentStr;
   }
 
-  void setConflict(Node conflict) {
+  void setConflict(Node conflict = Node::null()) {
     d_conflict = true; 
-    d_conflictNode = conflict; 
+    d_conflictNode = conflict;
   }
 
-  bool inConflict() { return d_conflict == true; }
+  bool inConflict() {
+    return d_conflict;
+  }
+
+  void sendConflict();
 
   friend class Bitblaster;
   friend class BitblastSolver;
@@ -142,6 +141,7 @@ private:
 
 }/* CVC4::theory::bv namespace */
 }/* CVC4::theory namespace */
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__THEORY__BV__THEORY_BV_H */
diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am
index 07619b965..995ade606 100644
--- a/test/regress/regress0/bv/Makefile.am
+++ b/test/regress/regress0/bv/Makefile.am
@@ -29,6 +29,49 @@ SMT_TESTS = \
 	fuzz12.smt \
 	fuzz13.smt \
 	fuzz14.smt \
+	fuzz15.delta01.smt \
+	fuzz16.delta01.smt \
+	fuzz17.delta01.smt \
+	fuzz18.delta01.smt \
+	fuzz18.smt \
+	fuzz19.delta01.smt \
+	fuzz19.smt \
+	fuzz20.delta01.smt \
+	fuzz20.smt \
+	fuzz21.delta01.smt \
+	fuzz21.smt \
+	fuzz22.delta01.smt \
+	fuzz22.smt \
+	fuzz23.delta01.smt \
+	fuzz23.smt \
+	fuzz24.delta01.smt \
+	fuzz24.smt \
+	fuzz25.delta01.smt \
+	fuzz25.smt \
+	fuzz26.delta01.smt \
+	fuzz26.smt \
+	fuzz27.delta01.smt \
+	fuzz27.smt \
+	fuzz28.delta01.smt \
+	fuzz28.smt \
+	fuzz29.delta01.smt \
+	fuzz29.smt \
+	fuzz30.delta01.smt \
+	fuzz30.smt \
+	fuzz31.delta01.smt \
+	fuzz31.smt \
+	fuzz32.delta01.smt \
+	fuzz32.smt \
+	fuzz33.delta01.smt \
+	fuzz33.smt \
+	fuzz34.delta01.smt \
+	fuzz34.smt \
+	fuzz35.delta01.smt \
+	fuzz35.smt \
+	fuzz36.delta01.smt \
+	fuzz36.smt \
+	fuzz37.delta01.smt \
+	fuzz37.smt \
 	calc2_sec2_shifter_mult_bmc15.atlas.delta01.smt
 
 # Regression tests for SMT2 inputs
diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am
index f58b01bc2..718e8f756 100644
--- a/test/regress/regress0/bv/core/Makefile.am
+++ b/test/regress/regress0/bv/core/Makefile.am
@@ -68,7 +68,6 @@ TESTS =	\
 	slice-18.smt \
 	slice-19.smt \
 	slice-20.smt \
-	ext_con_004_001_1024.smt \
 	a78test0002.smt \
 	a95test0002.smt \
 	bitvec0.smt \
diff --git a/test/regress/regress0/bv/fuzz15.delta01.smt b/test/regress/regress0/bv/fuzz15.delta01.smt
index f3eb57e17..b3fad3a2b 100644
--- a/test/regress/regress0/bv/fuzz15.delta01.smt
+++ b/test/regress/regress0/bv/fuzz15.delta01.smt
@@ -10,7 +10,7 @@
 :extrafuns ((v0 BitVec[15]))
 :extrafuns ((v14 BitVec[14]))
 :extrafuns ((v19 BitVec[10]))
-:status unknown
+:status unsat
 :formula
 (let (?n1 (sign_extend[2] v11))
 (let (?n2 (sign_extend[6] ?n1))
diff --git a/test/regress/regress0/bv/fuzz16.delta01.smt b/test/regress/regress0/bv/fuzz16.delta01.smt
new file mode 100644
index 000000000..c9fef69de
--- /dev/null
+++ b/test/regress/regress0/bv/fuzz16.delta01.smt
@@ -0,0 +1,69 @@
+(benchmark fuzzsmt
+:logic QF_BV
+:extrafuns ((v1 BitVec[12]))
+:extrafuns ((v15 BitVec[8]))
+:extrafuns ((v11 BitVec[12]))
+:extrafuns ((v12 BitVec[15]))
+:status unsat
+:formula
+(flet ($n1 true)
+(let (?n2 bv0[12])
+(flet ($n3 (bvslt ?n2 v1))
+(flet ($n4 (not $n3))
+(let (?n5 bv0[1])
+(let (?n6 bv1[1])
+(let (?n7 bv1[12])
+(flet ($n8 (bvult v11 ?n7))
+(let (?n9 (ite $n8 ?n6 ?n5))
+(flet ($n10 (= ?n6 ?n9))
+(let (?n11 (ite $n10 v11 ?n2))
+(let (?n12 (sign_extend[3] ?n11))
+(flet ($n13 (bvult ?n12 v12))
+(let (?n14 (ite $n13 ?n6 ?n5))
+(flet ($n15 (bvult ?n5 ?n14))
+(flet ($n16 (not $n15))
+(let (?n17 bv0[5])
+(let (?n18 (sign_extend[1] v1))
+(let (?n19 (sign_extend[2] ?n18))
+(let (?n20 (bvxnor v12 ?n19))
+(flet ($n21 (bvult ?n19 ?n20))
+(let (?n22 (ite $n21 ?n6 ?n5))
+(let (?n23 (repeat[5] ?n22))
+(flet ($n24 (bvult ?n17 ?n23))
+(let (?n25 bv0[10])
+(let (?n26 bv0[15])
+(flet ($n27 (bvsge ?n20 ?n26))
+(let (?n28 (ite $n27 ?n6 ?n5))
+(let (?n29 (sign_extend[9] ?n28))
+(flet ($n30 (= ?n25 ?n29))
+(let (?n31 bv1[14])
+(flet ($n32 (bvult ?n22 ?n6))
+(let (?n33 (ite $n32 ?n6 ?n5))
+(let (?n34 (zero_extend[13] ?n33))
+(let (?n35 (bvadd ?n31 ?n34))
+(let (?n36 bv0[14])
+(flet ($n37 (bvugt ?n35 ?n36))
+(flet ($n38 false)
+(let (?n39 bv1[15])
+(let (?n40 (zero_extend[4] v15))
+(let (?n41 (bvcomp v11 ?n40))
+(let (?n42 (zero_extend[14] ?n41))
+(flet ($n43 (distinct ?n39 ?n42))
+(let (?n44 (ite $n43 ?n6 ?n5))
+(let (?n45 (sign_extend[11] ?n44))
+(let (?n46 (bvxor v1 ?n45))
+(flet ($n47 (bvsgt ?n2 ?n46))
+(let (?n48 (zero_extend[12] ?n44))
+(let (?n49 bv0[13])
+(flet ($n50 (bvule ?n48 ?n49))
+(flet ($n51 (or $n38 $n47 $n50))
+(flet ($n52 (bvsle ?n2 v1))
+(let (?n53 (ite $n52 ?n6 ?n5))
+(let (?n54 (bvadd ?n6 ?n53))
+(flet ($n55 (bvugt ?n54 ?n5))
+(let (?n56 (ite $n55 ?n6 ?n5))
+(let (?n57 (sign_extend[14] ?n56))
+(flet ($n58 (bvuge ?n57 ?n39))
+(flet ($n59 (and $n4 $n16 $n24 $n30 $n37 $n51 $n58))
+$n59
+))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
diff --git a/test/regress/regress0/bv/fuzz17.delta01.smt b/test/regress/regress0/bv/fuzz17.delta01.smt
index e4adff5f6..568658e9d 100644
--- a/test/regress/regress0/bv/fuzz17.delta01.smt
+++ b/test/regress/regress0/bv/fuzz17.delta01.smt
@@ -6,7 +6,7 @@
 :extrafuns ((v3 BitVec[11]))
 :extrafuns ((v8 BitVec[9]))
 :extrafuns ((v4 BitVec[14]))
-:status unknown
+:status sat
 :formula
 (let (?n1 bv0[1])
 (let (?n2 bv1[16])
diff --git a/test/regress/regress0/bv/fuzz18.delta01.smt b/test/regress/regress0/bv/fuzz18.delta01.smt
index 6622ebc15..87cceb8e8 100644
--- a/test/regress/regress0/bv/fuzz18.delta01.smt
+++ b/test/regress/regress0/bv/fuzz18.delta01.smt
@@ -5,7 +5,7 @@
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v6 BitVec[4]))
-:status unknown
+:status unsat
 :formula
 (let (?n1 bv1[1])
 (let (?n2 (extract[1:1] v2))
diff --git a/test/regress/regress0/bv/fuzz18.smt b/test/regress/regress0/bv/fuzz18.smt
index 71a4eb6f3..aae85a343 100644
--- a/test/regress/regress0/bv/fuzz18.smt
+++ b/test/regress/regress0/bv/fuzz18.smt
@@ -9,7 +9,7 @@
 :extrafuns ((v5 BitVec[4]))
 :extrafuns ((v3 BitVec[4]))
 :extrafuns ((v7 BitVec[4]))
-:status unknown
+:status unsat
 :formula
 (flet ($n1 true)
 (let (?n2 (bvcomp v3 v2))
diff --git a/test/regress/regress0/bv/fuzz19.delta01.smt b/test/regress/regress0/bv/fuzz19.delta01.smt
index e6395f1aa..fd044074d 100644
--- a/test/regress/regress0/bv/fuzz19.delta01.smt
+++ b/test/regress/regress0/bv/fuzz19.delta01.smt
@@ -6,7 +6,7 @@
 :extrafuns ((v3 BitVec[4]))
 :extrafuns ((v4 BitVec[4]))
 :extrafuns ((v5 BitVec[4]))
-:status unknown
+:status unsat
 :formula
 (flet ($n1 true)
 (let (?n2 (extract[0:0] v2))
diff --git a/test/regress/regress0/bv/fuzz19.smt b/test/regress/regress0/bv/fuzz19.smt
index bcd4dfec0..91bf1e01b 100644
--- a/test/regress/regress0/bv/fuzz19.smt
+++ b/test/regress/regress0/bv/fuzz19.smt
@@ -6,7 +6,7 @@
 :extrafuns ((v5 BitVec[4]))
 :extrafuns ((v3 BitVec[4]))
 :extrafuns ((v4 BitVec[4]))
-:status unknown
+:status unsat
 :formula
 (flet ($n1 true)
 (let (?n2 (extract[0:0] v2))
diff --git a/test/regress/regress0/bv/fuzz20.delta01.smt b/test/regress/regress0/bv/fuzz20.delta01.smt
index 32c8673d5..66208cf74 100644
--- a/test/regress/regress0/bv/fuzz20.delta01.smt
+++ b/test/regress/regress0/bv/fuzz20.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v2 BitVec[4]))
-:status unknown
+:status unsat
 :formula
 (let (?n1 bv1[1])
 (let (?n2 bv0[4])
diff --git a/test/regress/regress0/bv/fuzz20.smt b/test/regress/regress0/bv/fuzz20.smt
index 5cca0878b..b7b493c82 100644
--- a/test/regress/regress0/bv/fuzz20.smt
+++ b/test/regress/regress0/bv/fuzz20.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz21.delta01.smt b/test/regress/regress0/bv/fuzz21.delta01.smt
index 86bcd823c..e74eaff8b 100644
--- a/test/regress/regress0/bv/fuzz21.delta01.smt
+++ b/test/regress/regress0/bv/fuzz21.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v1 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 (bvmul v1 v1))
 (let (?n2 bv0[4])
diff --git a/test/regress/regress0/bv/fuzz21.smt b/test/regress/regress0/bv/fuzz21.smt
index 4af799450..9ad27d844 100644
--- a/test/regress/regress0/bv/fuzz21.smt
+++ b/test/regress/regress0/bv/fuzz21.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz22.delta01.smt b/test/regress/regress0/bv/fuzz22.delta01.smt
index 62b8114d6..a1ef9e444 100644
--- a/test/regress/regress0/bv/fuzz22.delta01.smt
+++ b/test/regress/regress0/bv/fuzz22.delta01.smt
@@ -5,7 +5,7 @@
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
 :extrafuns ((v4 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (flet ($n1 true)
 (let (?n2 bv12[4])
diff --git a/test/regress/regress0/bv/fuzz22.smt b/test/regress/regress0/bv/fuzz22.smt
index fa479ab30..5aad8f7f7 100644
--- a/test/regress/regress0/bv/fuzz22.smt
+++ b/test/regress/regress0/bv/fuzz22.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status sat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz23.delta01.smt b/test/regress/regress0/bv/fuzz23.delta01.smt
index e06b0c670..d7aa145b4 100644
--- a/test/regress/regress0/bv/fuzz23.delta01.smt
+++ b/test/regress/regress0/bv/fuzz23.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v1 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 bv1[1])
 (let (?n2 (bvnot v1))
diff --git a/test/regress/regress0/bv/fuzz23.smt b/test/regress/regress0/bv/fuzz23.smt
index 5250bac0c..11b207870 100644
--- a/test/regress/regress0/bv/fuzz23.smt
+++ b/test/regress/regress0/bv/fuzz23.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz24.delta01.smt b/test/regress/regress0/bv/fuzz24.delta01.smt
index 9a219175b..84c9db88a 100644
--- a/test/regress/regress0/bv/fuzz24.delta01.smt
+++ b/test/regress/regress0/bv/fuzz24.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v1 BitVec[4]))
-:status unknown
+:status unsat
 :formula
 (let (?n1 bv0[4])
 (flet ($n2 (bvslt v1 ?n1))
diff --git a/test/regress/regress0/bv/fuzz24.smt b/test/regress/regress0/bv/fuzz24.smt
index 0f722108a..a32c1e804 100644
--- a/test/regress/regress0/bv/fuzz24.smt
+++ b/test/regress/regress0/bv/fuzz24.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :formula
diff --git a/test/regress/regress0/bv/fuzz25.delta01.smt b/test/regress/regress0/bv/fuzz25.delta01.smt
index 1a26485db..01a7da590 100644
--- a/test/regress/regress0/bv/fuzz25.delta01.smt
+++ b/test/regress/regress0/bv/fuzz25.delta01.smt
@@ -2,7 +2,7 @@
 :logic QF_BV
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 bv0[4])
 (flet ($n2 (bvule v0 ?n1))
diff --git a/test/regress/regress0/bv/fuzz25.smt b/test/regress/regress0/bv/fuzz25.smt
index 1193a62e1..a73ddb56b 100644
--- a/test/regress/regress0/bv/fuzz25.smt
+++ b/test/regress/regress0/bv/fuzz25.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz26.delta01.smt b/test/regress/regress0/bv/fuzz26.delta01.smt
index e6467a284..8ea0741dc 100644
--- a/test/regress/regress0/bv/fuzz26.delta01.smt
+++ b/test/regress/regress0/bv/fuzz26.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v1 BitVec[4]))
-:status unknown
+:status unsat
 :formula
 (let (?n1 bv0[4])
 (let (?n2 bv14[4])
diff --git a/test/regress/regress0/bv/fuzz26.smt b/test/regress/regress0/bv/fuzz26.smt
index 5a938c9e8..af360df8b 100644
--- a/test/regress/regress0/bv/fuzz26.smt
+++ b/test/regress/regress0/bv/fuzz26.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz27.delta01.smt b/test/regress/regress0/bv/fuzz27.delta01.smt
index 29da5fce3..f7a118b16 100644
--- a/test/regress/regress0/bv/fuzz27.delta01.smt
+++ b/test/regress/regress0/bv/fuzz27.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v0 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 bv0[4])
 (flet ($n2 (bvslt v0 ?n1))
diff --git a/test/regress/regress0/bv/fuzz27.smt b/test/regress/regress0/bv/fuzz27.smt
index c26632ebc..786a6aa9c 100644
--- a/test/regress/regress0/bv/fuzz27.smt
+++ b/test/regress/regress0/bv/fuzz27.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status sat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz28.delta01.smt b/test/regress/regress0/bv/fuzz28.delta01.smt
index 1bfdea909..5f8ca0f84 100644
--- a/test/regress/regress0/bv/fuzz28.delta01.smt
+++ b/test/regress/regress0/bv/fuzz28.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v0 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 (bvnot v0))
 (let (?n2 bv1[4])
diff --git a/test/regress/regress0/bv/fuzz28.smt b/test/regress/regress0/bv/fuzz28.smt
index 2c7a71a0f..732017750 100644
--- a/test/regress/regress0/bv/fuzz28.smt
+++ b/test/regress/regress0/bv/fuzz28.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz29.delta01.smt b/test/regress/regress0/bv/fuzz29.delta01.smt
index 31e09808e..ec5e74e1d 100644
--- a/test/regress/regress0/bv/fuzz29.delta01.smt
+++ b/test/regress/regress0/bv/fuzz29.delta01.smt
@@ -3,7 +3,7 @@
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (flet ($n1 true)
 (flet ($n2 false)
diff --git a/test/regress/regress0/bv/fuzz29.smt b/test/regress/regress0/bv/fuzz29.smt
index f1275af5c..1a9fb0b73 100644
--- a/test/regress/regress0/bv/fuzz29.smt
+++ b/test/regress/regress0/bv/fuzz29.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status sat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz30.delta01.smt b/test/regress/regress0/bv/fuzz30.delta01.smt
index 8f0eecaf0..e99995377 100644
--- a/test/regress/regress0/bv/fuzz30.delta01.smt
+++ b/test/regress/regress0/bv/fuzz30.delta01.smt
@@ -2,7 +2,7 @@
 :logic QF_BV
 :extrafuns ((v2 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 (bvmul v1 v2))
 (let (?n2 (bvneg ?n1))
diff --git a/test/regress/regress0/bv/fuzz30.smt b/test/regress/regress0/bv/fuzz30.smt
index 2fc1669cb..494cde3a3 100644
--- a/test/regress/regress0/bv/fuzz30.smt
+++ b/test/regress/regress0/bv/fuzz30.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status sat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz31.delta01.smt b/test/regress/regress0/bv/fuzz31.delta01.smt
index 24ed4fcd4..07f8b4ae3 100644
--- a/test/regress/regress0/bv/fuzz31.delta01.smt
+++ b/test/regress/regress0/bv/fuzz31.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v1 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 bv8[4])
 (let (?n2 bv12[4])
diff --git a/test/regress/regress0/bv/fuzz31.smt b/test/regress/regress0/bv/fuzz31.smt
index cb64a270e..452e3d2da 100644
--- a/test/regress/regress0/bv/fuzz31.smt
+++ b/test/regress/regress0/bv/fuzz31.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz32.delta01.smt b/test/regress/regress0/bv/fuzz32.delta01.smt
index 0f2b24505..18fed3adf 100644
--- a/test/regress/regress0/bv/fuzz32.delta01.smt
+++ b/test/regress/regress0/bv/fuzz32.delta01.smt
@@ -2,7 +2,7 @@
 :logic QF_BV
 :extrafuns ((v2 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 bv1[1])
 (let (?n2 bv0[4])
diff --git a/test/regress/regress0/bv/fuzz32.smt b/test/regress/regress0/bv/fuzz32.smt
index 3bf1cbc46..5384eee65 100644
--- a/test/regress/regress0/bv/fuzz32.smt
+++ b/test/regress/regress0/bv/fuzz32.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz33.delta01.smt b/test/regress/regress0/bv/fuzz33.delta01.smt
index 321d7af0d..6d7589ca7 100644
--- a/test/regress/regress0/bv/fuzz33.delta01.smt
+++ b/test/regress/regress0/bv/fuzz33.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v0 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 bv0[1])
 (let (?n2 bv1[4])
diff --git a/test/regress/regress0/bv/fuzz33.smt b/test/regress/regress0/bv/fuzz33.smt
index d7ab6c9a1..b7898b810 100644
--- a/test/regress/regress0/bv/fuzz33.smt
+++ b/test/regress/regress0/bv/fuzz33.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status sat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :formula
diff --git a/test/regress/regress0/bv/fuzz34.delta01.smt b/test/regress/regress0/bv/fuzz34.delta01.smt
index ab13890bf..2bd289657 100644
--- a/test/regress/regress0/bv/fuzz34.delta01.smt
+++ b/test/regress/regress0/bv/fuzz34.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v0 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 bv0[1])
 (let (?n2 bv0[4])
diff --git a/test/regress/regress0/bv/fuzz34.smt b/test/regress/regress0/bv/fuzz34.smt
index 704702421..200bed99f 100644
--- a/test/regress/regress0/bv/fuzz34.smt
+++ b/test/regress/regress0/bv/fuzz34.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :formula
diff --git a/test/regress/regress0/bv/fuzz35.delta01.smt b/test/regress/regress0/bv/fuzz35.delta01.smt
index e44a22c7e..640e44f6f 100644
--- a/test/regress/regress0/bv/fuzz35.delta01.smt
+++ b/test/regress/regress0/bv/fuzz35.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v0 BitVec[4]))
-:status unknown
+:status unsat
 :formula
 (let (?n1 bv4[4])
 (let (?n2 bv12[4])
diff --git a/test/regress/regress0/bv/fuzz35.smt b/test/regress/regress0/bv/fuzz35.smt
index f8f16a8db..73ae721b2 100644
--- a/test/regress/regress0/bv/fuzz35.smt
+++ b/test/regress/regress0/bv/fuzz35.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status unsat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz36.delta01.smt b/test/regress/regress0/bv/fuzz36.delta01.smt
index 153b46719..65c88add2 100644
--- a/test/regress/regress0/bv/fuzz36.delta01.smt
+++ b/test/regress/regress0/bv/fuzz36.delta01.smt
@@ -3,7 +3,7 @@
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
 :extrafuns ((v3 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (flet ($n1 true)
 (flet ($n2 false)
diff --git a/test/regress/regress0/bv/fuzz36.smt b/test/regress/regress0/bv/fuzz36.smt
index 96924c4a3..b128ef10f 100644
--- a/test/regress/regress0/bv/fuzz36.smt
+++ b/test/regress/regress0/bv/fuzz36.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status sat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))
diff --git a/test/regress/regress0/bv/fuzz37.delta01.smt b/test/regress/regress0/bv/fuzz37.delta01.smt
index 8baaa1101..044894164 100644
--- a/test/regress/regress0/bv/fuzz37.delta01.smt
+++ b/test/regress/regress0/bv/fuzz37.delta01.smt
@@ -1,7 +1,7 @@
 (benchmark fuzzsmt
 :logic QF_BV
 :extrafuns ((v1 BitVec[4]))
-:status unknown
+:status sat
 :formula
 (let (?n1 bv1[4])
 (flet ($n2 (bvugt ?n1 v1))
diff --git a/test/regress/regress0/bv/fuzz37.smt b/test/regress/regress0/bv/fuzz37.smt
index 4bdf0ceee..98fdfda48 100644
--- a/test/regress/regress0/bv/fuzz37.smt
+++ b/test/regress/regress0/bv/fuzz37.smt
@@ -1,6 +1,6 @@
 (benchmark fuzzsmt
 :logic QF_BV
-:status unknown
+:status sat
 :extrafuns ((v0 BitVec[4]))
 :extrafuns ((v1 BitVec[4]))
 :extrafuns ((v2 BitVec[4]))