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

diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 41c0c4ac9c78aa45cf5c2528fb6fe17a212084dd..2eadbdf22411daa20ac7c8d4d5dae91d9eeb9919 100644 (file)
--- 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 d512847d59daab82fe83067b2c2c8a9c4944aea1..5bb90684152f1357aa8a1bcd3b87f0413f31e340 100644 (file)
--- 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 a8813b7aaf487afa4e22baab86211c635cdf7ea6..f8c763e3fa466f83d1b9f785d41305bc26a47df9 100644 (file)
--- 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 ff0fc2b1aa11894a548bec0b0ad56728b36e1057..334a704e97ccdf9cb3a3e4225156b409b7883e9f 100644 (file)
--- 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 afb4a8b4a78645c9269a1849301132fa1fbb7daf..cb08a1ad869ec723b9a49379e0adcbe649799cb8 100644 (file)
--- 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 66f443d508ac739ad36a152fc3f6aaeea7c2b2ac..208ffba6cd6256cb60805f4577c63ec7745dfa81 100644 (file)
--- 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 f79b7ab717576b7126b075e53d1c217558a1480f..a2cf39049eb925f6b8aec59d7cd8836b7f6cbbc2 100644 (file)
--- 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 07619b9650096076b70ab114570a80246f71e209..995ade606ecd8ef7de83becaea44d34c6fd15b1d 100644 (file)
--- 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 f58b01bc230f927ded9a51292af1ceb6dd7bcb8f..718e8f75690b5acb570da7f62cec0610c2a6d91e 100644 (file)
--- 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 f3eb57e17093a8ce12949027aec3a9ef767e42ab..b3fad3a2bf518528af27d25c0b4b363162ce95c7 100644 (file)
--- 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 (file)
index 0000000..c9fef69
--- /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 e4adff5f60ad49c3aaf0ab61b355a17bb0d70c33..568658e9dcf8d1a6940eced7b5c0ee5b8980effb 100644 (file)
--- 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 6622ebc158d2a4d9ec21555f6aebd6ff99e76097..87cceb8e8ea16901b76b8cc6084bf424710f07a4 100644 (file)
--- 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 71a4eb6f36bf447c06fe93209a93546f086c938a..aae85a3437452d57a2d67a95f1e3b00d45f6ca38 100644 (file)
--- 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 e6395f1aa27c04f3730216bc20a361c8d00d49d9..fd044074d04d30a4ee745c827c7cf284c52dfde0 100644 (file)
--- 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 bcd4dfec0e1c7ed51ce160c5794b06bd01f25ccf..91bf1e01bcdb9621807254cb85778cccb02c7e37 100644 (file)
--- 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 32c8673d585c3b46111501ce9a070bdade8f178d..66208cf7443765d71495820b07ac63d556601f79 100644 (file)
--- 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 5cca0878baba3249c79552996baa2928e1f02c63..b7b493c8292318d3c69d3d86637ddd2d8d802d39 100644 (file)
--- 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 86bcd823ceabd3d4095e9d3485fbed1f5d047c04..e74eaff8b81271b7501f6d6ff37a900577b07429 100644 (file)
--- 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 4af7994505ea6dd393ac36c0f1e3b6678a198106..9ad27d84406c369a382d0a23c6e962783ea4d0b3 100644 (file)
--- 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 62b8114d6401ceebc1508ad4a1db8befa8b6a3e8..a1ef9e44493f02b4489a13ffdec6d0f6463e5802 100644 (file)
--- 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 fa479ab30756dbf29dc46ac7fb5ebabd9d331572..5aad8f7f783ae2661500d68717456c42d0167c15 100644 (file)
--- 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 e06b0c6700033957d3399e796de5f2f0fb87c3f9..d7aa145b4840869472b132bb32ad9e1748cad8a0 100644 (file)
--- 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 5250bac0c1511f800c37be7404708a15facf2de4..11b207870611efb22af5ba84a0caf3665a0fe15f 100644 (file)
--- 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 9a219175bf6d2eefeedbcfedcabd00d379ad9acb..84c9db88a523e297529c40849c67718b77e38afb 100644 (file)
--- 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 0f722108a4cf13e5b9363942ccb2f09ba989e93b..a32c1e80496ad16cae5ad2e9f13c22cfe02530b5 100644 (file)
--- 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 1a26485dbb449c5e9384cfbf7fed7771b5450c94..01a7da590c5f017e1820d192436181448cd5e026 100644 (file)
--- 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 1193a62e152b37eb583a40aaba787193c064343b..a73ddb56b3e304dea30ecb36016daf8032b74af1 100644 (file)
--- 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 e6467a2841c92c410017bca10c574faa3fc7cb2a..8ea0741dcd41f3f988007d7f602fa3f18112f1cd 100644 (file)
--- 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 5a938c9e84ca4cd8959f3688c0287f28c3741d9d..af360df8b8dc169f6f8024486db57abe1e0a2f96 100644 (file)
--- 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 29da5fce3d538ef93e6411d61bb0e6b88361816e..f7a118b169f4cd354f723ac826383bcf140e8b8e 100644 (file)
--- 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 c26632ebc4cf84baf86656c6ade7c87c812f6eb7..786a6aa9c2f2769e58d07e7f1757d4667f3e24be 100644 (file)
--- 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 1bfdea909b20b0189c4fe8ac190cc64fd7ca07d2..5f8ca0f8454d6a00d895ed3435ca39d1e01cbf66 100644 (file)
--- 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 2c7a71a0f55423dd105f9385a4762bdf621751d5..7320177507bcbe9d078526021032190f981c05d1 100644 (file)
--- 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 31e09808e382383faea26697ab572a9f1291dea9..ec5e74e1dc4b21d838283122a64922de57377661 100644 (file)
--- 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 f1275af5cbdb996f94ddb60ec38f0b9e1dcc10bf..1a9fb0b73587925cdb1723a9c2615cab22ab450f 100644 (file)
--- 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 8f0eecaf09fabd2edcd797fd772ff656374da5e8..e99995377d29a75e7bf433d7ae3d1433028994ea 100644 (file)
--- 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 2fc1669cbca3d953350631596603bb95b7150296..494cde3a3047394e7df7a640a452ded71fc0cfa5 100644 (file)
--- 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 24ed4fcd4ea937e5cf8ea8f6eddff74b571d93c1..07f8b4ae35aaad648327e00eaced749621aed7af 100644 (file)
--- 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 cb64a270ecd18a74f6dd61e86066ccdb219da9c3..452e3d2da117fa5ac3eae5cefd567c95a9f1baa8 100644 (file)
--- 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 0f2b2450588c769200a5c430dda6f90f2ed1159c..18fed3adf313692c874a4e7ddeb05a8b56e37e88 100644 (file)
--- 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 3bf1cbc466c9660c3d2f026e62d0f799bedc74e6..5384eee658e8be6555598273dc9e26246d923d0d 100644 (file)
--- 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 321d7af0d16d4632397500c0fee468aabe10c77e..6d7589ca7fcf193fff211d2fd635a31811060e79 100644 (file)
--- 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 d7ab6c9a1811384590a8964b7e12061e55c87ae5..b7898b810219252aaceebfc7e4f835acd48bab4f 100644 (file)
--- 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 ab13890bfc9f1e440dfbee19291ecef8dcbd1488..2bd2896570ae188d9d18247af9408df1fddbbcfc 100644 (file)
--- 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 7047024218c03f8922463c485f91a90d1e2e1893..200bed99fe28c174cffe6c186ecc7112db3f5a93 100644 (file)
--- 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 e44a22c7edc50160df2ed4e76ebc70d674ea8e07..640e44f6ff86b26bb9a621de28f463e4ccc7aed3 100644 (file)
--- 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 f8f16a8dba386324d8c13bad3e8790f18fee9da5..73ae721b2a4255551080fce0da7566f22200e135 100644 (file)
--- 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 153b4671966b1b665b9a9d33fcee95ff2c228fdb..65c88add278a98c9f284cc728a54c646cf824240 100644 (file)
--- 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 96924c4a385b71ab4f0f252302f4db67b7a1a250..b128ef10f450f0f192f52815c978aeacdc574283 100644 (file)
--- 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 8baaa110165c62b69e9fc705590441102aacf4e6..0448941641b19f4c686f256721071cf2f38b29e9 100644 (file)
--- 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 4bdf0ceee98b5f1bad80730f1d36dc8b198f0169..98fdfda4844f5366b7119761bf7092c89bf769b5 100644 (file)
--- 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]))