From: Dejan Jovanović Date: Mon, 11 Jun 2012 18:54:38 +0000 (+0000) Subject: fixing bitvector bugs X-Git-Tag: cvc5-1.0.0~8082 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=d54c761087af01874ea6674111888cb94ffa4ee6;p=cvc5.git 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 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& explanation) { vec queue; queue.push(p); - __gnu_cxx::hash_set visited; + Debug("bvminisat::explain") << OUTPUT_TAG << "starting explain of " << p << std::endl; + + __gnu_cxx::hash_set 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& 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& 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 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 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]))