From 30e6dc83aed15ef002087e55cf228f0735c63f40 Mon Sep 17 00:00:00 2001 From: Mathias Preiner Date: Tue, 22 Sep 2020 15:40:48 -0700 Subject: [PATCH] Add simple BV solver (#5065) This PR adds a simple BV solver that sends bit-blasting lemmas to the internal MiniSat. --- src/CMakeLists.txt | 2 + src/options/bv_options.toml | 16 + src/smt/set_defaults.cpp | 8 + src/theory/bv/bv_solver.h | 9 +- src/theory/bv/bv_solver_simple.cpp | 296 ++++++++++++++++++ src/theory/bv/bv_solver_simple.h | 80 +++++ src/theory/bv/theory_bv.cpp | 25 +- src/theory/bv/theory_bv.h | 10 + src/theory/bv/theory_bv_rewrite_rules.h | 2 + .../theory_bv_rewrite_rules_simplification.h | 17 + src/theory/bv/theory_bv_rewriter.cpp | 7 + src/theory/bv/theory_bv_rewriter.h | 5 +- src/theory/theory_state.cpp | 5 + src/theory/theory_state.h | 3 + test/regress/regress0/bv/ackermann1.smt2 | 1 + test/regress/regress0/bv/bool-model.smt2 | 1 + test/regress/regress0/bv/bool-to-bv-ite.smt2 | 1 + test/regress/regress0/bv/bug734.smt2 | 1 + test/regress/regress0/bv/issue-4076.smt2 | 1 + .../regress0/bv/pr4993-bvugt-bvurem-b.smt2 | 1 + test/regress/regress1/bug520.smt2 | 1 + 21 files changed, 487 insertions(+), 5 deletions(-) create mode 100644 src/theory/bv/bv_solver_simple.cpp create mode 100644 src/theory/bv/bv_solver_simple.h diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 1bc393053..e939915d5 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -456,6 +456,8 @@ libcvc4_add_sources( theory/bv/bv_solver.h theory/bv/bv_solver_lazy.cpp theory/bv/bv_solver_lazy.h + theory/bv/bv_solver_simple.cpp + theory/bv/bv_solver_simple.h theory/bv/bv_subtheory.h theory/bv/bv_subtheory_algebraic.cpp theory/bv/bv_subtheory_algebraic.h diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml index d91c8bf9f..42401268d 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -235,3 +235,19 @@ header = "options/bv_options.h" type = "bool" default = "false" help = "print bit-vector constants in decimal (e.g. (_ bv1 4)) instead of binary (e.g. #b0001), applies to SMT-LIB 2.x" + +[[option]] + name = "bvSolver" + category = "regular" + long = "bv-solver=MODE" + type = "BVSolver" + default = "LAZY" + help = "choose bit-vector solver, see --bv-solver=help" + help_mode = "Bit-vector solvers." +[[option.mode.LAZY]] + name = "lazy" + help = "Enables the lazy BV solver infrastructure." +[[option.mode.SIMPLE]] + name = "simple" + help = "Enables simple bitblasting solver with proof support." + diff --git a/src/smt/set_defaults.cpp b/src/smt/set_defaults.cpp index 2dc0d52ac..32e716ab2 100644 --- a/src/smt/set_defaults.cpp +++ b/src/smt/set_defaults.cpp @@ -124,6 +124,14 @@ void setDefaults(LogicInfo& logic, bool isInternalSubsolver) } } + /* BVSolver::SIMPLE does not natively support int2bv and nat2bv, they need to + * to be eliminated eagerly. */ + if (options::bvSolver() == options::BVSolver::SIMPLE) + { + options::bvLazyReduceExtf.set(false); + options::bvLazyRewriteExtf.set(false); + } + if (options::solveIntAsBV() > 0) { // not compatible with incremental diff --git a/src/theory/bv/bv_solver.h b/src/theory/bv/bv_solver.h index 36444afbe..6e251fc2d 100644 --- a/src/theory/bv/bv_solver.h +++ b/src/theory/bv/bv_solver.h @@ -68,7 +68,7 @@ class BVSolver */ virtual void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) {} - virtual bool needsCheckLastEffort() = 0; + virtual bool needsCheckLastEffort() { return false; } virtual void propagate(Theory::Effort e){}; @@ -103,7 +103,12 @@ class BVSolver /** Called by abstraction preprocessing pass. */ virtual bool applyAbstraction(const std::vector& assertions, - std::vector& new_assertions) = 0; + std::vector& new_assertions) + { + new_assertions.insert( + new_assertions.end(), assertions.begin(), assertions.end()); + return false; + }; protected: TheoryState& d_state; diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp new file mode 100644 index 000000000..e03feedfc --- /dev/null +++ b/src/theory/bv/bv_solver_simple.cpp @@ -0,0 +1,296 @@ +/********************* */ +/*! \file bv_solver_simple.cpp + ** \verbatim + ** Top contributors (to current version): + ** Mathias Preiner + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Simple bit-blast solver + ** + ** Simple bit-blast solver that sends bitblast lemmas directly to MiniSat. + **/ + +#include "theory/bv/bv_solver_simple.h" + +#include "theory/bv/bitblast/lazy_bitblaster.h" +#include "theory/bv/theory_bv.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/theory_model.h" + +namespace CVC4 { +namespace theory { +namespace bv { + +/** + * Implementation of a simple Node-based bit-blaster. + * + * Implements the bare minimum to bit-blast bit-vector atoms/terms. + */ +class BBSimple : public TBitblaster +{ + using Bits = std::vector; + + public: + BBSimple(TheoryState& state); + ~BBSimple() = default; + + /** Bit-blast term 'node' and return bit-blasted 'bits'. */ + void bbTerm(TNode node, Bits& bits) override; + /** Bit-blast atom 'node'. */ + void bbAtom(TNode node) override; + /** Get bit-blasted atom, returns 'atom' itself since it's Boolean. */ + Node getBBAtom(TNode atom) const override; + /** Store Boolean node representing the bit-blasted atom. */ + void storeBBAtom(TNode atom, Node atom_bb) override; + /** Store bits of bit-blasted term. */ + void storeBBTerm(TNode node, const Bits& bits) override; + /** Check if atom was already bit-blasted. */ + bool hasBBAtom(TNode atom) const override; + /** Get bit-blasted node stored for atom. */ + Node getStoredBBAtom(TNode node); + /** Create 'bits' for variable 'var'. */ + void makeVariable(TNode var, Bits& bits) override; + + /** Collect model values for all relevant terms given in 'relevantTerms'. */ + bool collectModelValues(TheoryModel* m, const std::set& relevantTerms); + + prop::SatSolver* getSatSolver() override { Unreachable(); } + + private: + /** Query SAT solver for assignment of node 'a'. */ + Node getModelFromSatSolver(TNode a, bool fullModel) override; + + /** Caches variables for which we already created bits. */ + TNodeSet d_variables; + /** Stores bit-blasted atoms. */ + std::unordered_map d_bbAtoms; + /** Theory state. */ + TheoryState& d_state; +}; + +BBSimple::BBSimple(TheoryState& s) : TBitblaster(), d_state(s) {} + +void BBSimple::bbAtom(TNode node) +{ + node = node.getKind() == kind::NOT ? node[0] : node; + + if (hasBBAtom(node)) + { + return; + } + + Node normalized = Rewriter::rewrite(node); + Node atom_bb = + normalized.getKind() != kind::CONST_BOOLEAN + && normalized.getKind() != kind::BITVECTOR_BITOF + ? d_atomBBStrategies[normalized.getKind()](normalized, this) + : normalized; + + storeBBAtom(node, atom_bb); +} + +void BBSimple::storeBBAtom(TNode atom, Node atom_bb) +{ + d_bbAtoms.emplace(atom, atom_bb); +} + +void BBSimple::storeBBTerm(TNode node, const Bits& bits) +{ + d_termCache.emplace(node, bits); +} + +bool BBSimple::hasBBAtom(TNode atom) const +{ + return d_bbAtoms.find(atom) != d_bbAtoms.end(); +} + +void BBSimple::makeVariable(TNode var, Bits& bits) +{ + Assert(bits.size() == 0); + for (unsigned i = 0; i < utils::getSize(var); ++i) + { + bits.push_back(utils::mkBitOf(var, i)); + } + d_variables.insert(var); +} + +Node BBSimple::getBBAtom(TNode node) const { return node; } + +void BBSimple::bbTerm(TNode node, Bits& bits) +{ + Assert(node.getType().isBitVector()); + if (hasBBTerm(node)) + { + getBBTerm(node, bits); + return; + } + d_termBBStrategies[node.getKind()](node, bits, this); + Assert(bits.size() == utils::getSize(node)); + storeBBTerm(node, bits); +} + +Node BBSimple::getStoredBBAtom(TNode node) +{ + bool negated = false; + if (node.getKind() == kind::NOT) + { + node = node[0]; + negated = true; + } + + Assert(hasBBAtom(node)); + Node atom_bb = d_bbAtoms.at(node); + return negated ? atom_bb.negate() : atom_bb; +} + +Node BBSimple::getModelFromSatSolver(TNode a, bool fullModel) +{ + if (!hasBBTerm(a)) + { + return utils::mkConst(utils::getSize(a), 0u); + } + + bool assignment; + Bits bits; + getBBTerm(a, bits); + Integer value(0); + Integer one(1), zero(0); + for (int i = bits.size() - 1; i >= 0; --i) + { + Integer bit; + if (d_state.hasSatValue(bits[i], assignment)) + { + bit = assignment ? one : zero; + } + else + { + bit = zero; + } + value = value * 2 + bit; + } + return utils::mkConst(bits.size(), value); +} + +bool BBSimple::collectModelValues(TheoryModel* m, + const std::set& relevantTerms) +{ + for (const auto& var : relevantTerms) + { + if (d_variables.find(var) == d_variables.end()) continue; + + Node const_value = getModelFromSatSolver(var, true); + Assert(const_value.isNull() || const_value.isConst()); + if (!const_value.isNull()) + { + if (!m->assertEquality(var, const_value, true)) + { + return false; + } + } + } + return true; +} + +/* -------------------------------------------------------------------------- */ + +namespace { + +bool isBVAtom(TNode n) +{ + return (n.getKind() == kind::EQUAL && n[0].getType().isBitVector()) + || n.getKind() == kind::BITVECTOR_ULT + || n.getKind() == kind::BITVECTOR_ULE + || n.getKind() == kind::BITVECTOR_SLT + || n.getKind() == kind::BITVECTOR_SLE; +} + +/* Traverse Boolean nodes and collect BV atoms. */ +void collectBVAtoms(TNode n, std::unordered_set& atoms) +{ + std::vector visit; + std::unordered_set visited; + + visit.push_back(n); + + do + { + TNode cur = visit.back(); + visit.pop_back(); + + if (visited.find(cur) != visited.end() || !cur.getType().isBoolean()) + continue; + + visited.insert(cur); + if (isBVAtom(cur)) + { + atoms.insert(cur); + continue; + } + + visit.insert(visit.end(), cur.begin(), cur.end()); + } while (!visit.empty()); +} + +} // namespace + +BVSolverSimple::BVSolverSimple(TheoryState& s, TheoryInferenceManager& inferMgr) + : BVSolver(s, inferMgr), d_bitblaster(new BBSimple(s)) +{ +} + +void BVSolverSimple::addBBLemma(TNode fact) +{ + if (!d_bitblaster->hasBBAtom(fact)) + { + d_bitblaster->bbAtom(fact); + } + NodeManager* nm = NodeManager::currentNM(); + Node atom_bb = Rewriter::rewrite(d_bitblaster->getStoredBBAtom(fact)); + Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb); + d_inferManager.lemma(lemma); +} + +bool BVSolverSimple::preNotifyFact( + TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) +{ + if (fact.getKind() == kind::NOT) + { + fact = fact[0]; + } + + if (isBVAtom(fact)) + { + addBBLemma(fact); + } + else if (fact.getKind() == kind::BITVECTOR_EAGER_ATOM) + { + TNode n = fact[0]; + + NodeManager* nm = NodeManager::currentNM(); + Node lemma = nm->mkNode(kind::EQUAL, fact, n); + d_inferManager.lemma(lemma); + + std::unordered_set bv_atoms; + collectBVAtoms(n, bv_atoms); + for (const Node& nn : bv_atoms) + { + addBBLemma(nn); + } + } + + return true; +} + +bool BVSolverSimple::collectModelValues(TheoryModel* m, + const std::set& termSet) +{ + return d_bitblaster->collectModelValues(m, termSet); +} + +} // namespace bv +} // namespace theory +} // namespace CVC4 diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h new file mode 100644 index 000000000..b7d86cf67 --- /dev/null +++ b/src/theory/bv/bv_solver_simple.h @@ -0,0 +1,80 @@ +/********************* */ +/*! \file bv_solver_simple.h + ** \verbatim + ** Top contributors (to current version): + ** Mathias Preiner + ** This file is part of the CVC4 project. + ** Copyright (c) 2009-2020 by the authors listed in the file AUTHORS + ** in the top-level source directory) and their institutional affiliations. + ** All rights reserved. See the file COPYING in the top-level source + ** directory for licensing information.\endverbatim + ** + ** \brief Simple bit-blast solver + ** + ** Simple bit-blast solver that sends bit-blast lemmas directly to MiniSat. + **/ + +#include "cvc4_private.h" + +#ifndef CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H +#define CVC4__THEORY__BV__BV_SOLVER_SIMPLE_H + +#include + +#include "theory/bv/bv_solver.h" + +namespace CVC4 { + +namespace theory { +namespace bv { + +class BBSimple; + +/** + * Simple bit-blasting solver that sends bit-blasting lemmas directly to the + * internal MiniSat. It is also ablo to handle atoms of kind + * BITVECTOR_EAGER_ATOM. + * + * Sends lemmas atom <=> bb(atom) to MiniSat on preNotifyFact(). + */ +class BVSolverSimple : public BVSolver +{ + public: + BVSolverSimple(TheoryState& state, TheoryInferenceManager& inferMgr); + ~BVSolverSimple() = default; + + void preRegisterTerm(TNode n) override {} + + bool preNotifyFact(TNode atom, + bool pol, + TNode fact, + bool isPrereg, + bool isInternal) override; + + std::string identify() const override { return "BVSolverSimple"; }; + + Theory::PPAssertStatus ppAssert(TNode in, + SubstitutionMap& outSubstitutions) override + { + return Theory::PPAssertStatus::PP_ASSERT_STATUS_UNSOLVED; + } + + bool collectModelValues(TheoryModel* m, + const std::set& termSet) override; + + private: + /** + * Sends a bit-blasting lemma fact <=> d_bitblaster.bbAtom(fact) to the + * inference manager. + */ + void addBBLemma(TNode fact); + + /** Bit-blaster used to bit-blast atoms/terms. */ + std::unique_ptr d_bitblaster; +}; + +} // namespace bv +} // namespace theory +} // namespace CVC4 + +#endif diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 3e462d5cc..857d4d6fb 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -17,6 +17,7 @@ #include "options/bv_options.h" #include "theory/bv/bv_solver_lazy.h" +#include "theory/bv/bv_solver_simple.h" #include "theory/bv/theory_bv_utils.h" namespace CVC4 { @@ -38,7 +39,16 @@ TheoryBV::TheoryBV(context::Context* c, d_state(c, u, valuation), d_inferMgr(*this, d_state, pnm) { - d_internal.reset(new BVSolverLazy(*this, c, u, pnm, name)); + switch (options::bvSolver()) + { + case options::BVSolver::LAZY: + d_internal.reset(new BVSolverLazy(*this, c, u, pnm, name)); + break; + + default: + AlwaysAssert(options::bvSolver() == options::BVSolver::SIMPLE); + d_internal.reset(new BVSolverSimple(d_state, d_inferMgr)); + } d_theoryState = &d_state; d_inferManager = &d_inferMgr; } @@ -159,6 +169,19 @@ void TheoryBV::preRegisterTerm(TNode node) bool TheoryBV::preCheck(Effort e) { return d_internal->preCheck(e); } +void TheoryBV::postCheck(Effort e) { d_internal->postCheck(e); } + +bool TheoryBV::preNotifyFact( + TNode atom, bool pol, TNode fact, bool isPrereg, bool isInternal) +{ + return d_internal->preNotifyFact(atom, pol, fact, isPrereg, isInternal); +} + +void TheoryBV::notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) +{ + d_internal->notifyFact(atom, pol, fact, isInternal); +} + bool TheoryBV::needsCheckLastEffort() { return d_internal->needsCheckLastEffort(); diff --git a/src/theory/bv/theory_bv.h b/src/theory/bv/theory_bv.h index a93fd438b..a01c74382 100644 --- a/src/theory/bv/theory_bv.h +++ b/src/theory/bv/theory_bv.h @@ -65,6 +65,16 @@ class TheoryBV : public Theory bool preCheck(Effort e) override; + void postCheck(Effort e) override; + + bool preNotifyFact(TNode atom, + bool pol, + TNode fact, + bool isPrereg, + bool isInternal) override; + + void notifyFact(TNode atom, bool pol, TNode fact, bool isInternal) override; + bool needsCheckLastEffort() override; void propagate(Effort e) override; diff --git a/src/theory/bv/theory_bv_rewrite_rules.h b/src/theory/bv/theory_bv_rewrite_rules.h index bfea2f1e6..8f97bf3a6 100644 --- a/src/theory/bv/theory_bv_rewrite_rules.h +++ b/src/theory/bv/theory_bv_rewrite_rules.h @@ -203,6 +203,7 @@ enum RewriteRuleId ConcatToMult, IsPowerOfTwo, MultSltMult, + BitOfConst, }; inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { @@ -367,6 +368,7 @@ inline std::ostream& operator << (std::ostream& out, RewriteRuleId ruleId) { case IsPowerOfTwo: out << "IsPowerOfTwo"; return out; case MultSltMult: out << "MultSltMult"; return out; case NormalizeEqPlusNeg: out << "NormalizeEqPlusNeg"; return out; + case BitOfConst: out << "BitOfConst"; return out; default: Unreachable(); } diff --git a/src/theory/bv/theory_bv_rewrite_rules_simplification.h b/src/theory/bv/theory_bv_rewrite_rules_simplification.h index d0c68c9e7..dd0d47078 100644 --- a/src/theory/bv/theory_bv_rewrite_rules_simplification.h +++ b/src/theory/bv/theory_bv_rewrite_rules_simplification.h @@ -28,6 +28,23 @@ namespace CVC4 { namespace theory { namespace bv { +/* -------------------------------------------------------------------------- */ + +/** + * BitOfConst + */ +template <> +inline bool RewriteRule::applies(TNode node) +{ + return node.getKind() == kind::BITVECTOR_BITOF && node[0].isConst(); +} + +template <> +inline Node RewriteRule::apply(TNode node) +{ + size_t pos = node.getOperator().getConst().d_bitIndex; + return utils::getBit(node[0], pos) ? utils::mkTrue() : utils::mkFalse(); +} /* -------------------------------------------------------------------------- */ diff --git a/src/theory/bv/theory_bv_rewriter.cpp b/src/theory/bv/theory_bv_rewriter.cpp index 6cea74a95..4f84facca 100644 --- a/src/theory/bv/theory_bv_rewriter.cpp +++ b/src/theory/bv/theory_bv_rewriter.cpp @@ -53,6 +53,12 @@ RewriteResponse TheoryBVRewriter::postRewrite(TNode node) { return res; } +RewriteResponse TheoryBVRewriter::RewriteBitOf(TNode node, bool prerewrite) +{ + Node resultNode = LinearRewriteStrategy>::apply(node); + return RewriteResponse(REWRITE_DONE, resultNode); +} + RewriteResponse TheoryBVRewriter::RewriteUlt(TNode node, bool prerewrite) { // reduce common subexpressions on both sides Node resultNode = LinearRewriteStrategy @@ -683,6 +689,7 @@ void TheoryBVRewriter::initializeRewrites() { } d_rewriteTable [ kind::EQUAL ] = RewriteEqual; + d_rewriteTable[kind::BITVECTOR_BITOF] = RewriteBitOf; d_rewriteTable [ kind::BITVECTOR_ULT ] = RewriteUlt; d_rewriteTable [ kind::BITVECTOR_SLT ] = RewriteSlt; d_rewriteTable [ kind::BITVECTOR_ULE ] = RewriteUle; diff --git a/src/theory/bv/theory_bv_rewriter.h b/src/theory/bv/theory_bv_rewriter.h index dee0f81d6..7e2110b14 100644 --- a/src/theory/bv/theory_bv_rewriter.h +++ b/src/theory/bv/theory_bv_rewriter.h @@ -50,8 +50,9 @@ class TheoryBVRewriter : public TheoryRewriter private: static RewriteResponse IdentityRewrite(TNode node, bool prerewrite = false); - static RewriteResponse UndefinedRewrite(TNode node, bool prerewrite = false); - + static RewriteResponse UndefinedRewrite(TNode node, bool prerewrite = false); + + static RewriteResponse RewriteBitOf(TNode node, bool prerewrite = false); static RewriteResponse RewriteEqual(TNode node, bool prerewrite = false); static RewriteResponse RewriteUlt(TNode node, bool prerewrite = false); static RewriteResponse RewriteUltBv(TNode node, bool prerewrite = false); diff --git a/src/theory/theory_state.cpp b/src/theory/theory_state.cpp index d1c7b42b4..95a96808e 100644 --- a/src/theory/theory_state.cpp +++ b/src/theory/theory_state.cpp @@ -132,5 +132,10 @@ bool TheoryState::isSatLiteral(TNode lit) const TheoryModel* TheoryState::getModel() { return d_valuation.getModel(); } +bool TheoryState::hasSatValue(TNode n, bool& value) const +{ + return d_valuation.hasSatValue(n, value); +} + } // namespace theory } // namespace CVC4 diff --git a/src/theory/theory_state.h b/src/theory/theory_state.h index 1c73912d7..187d586a1 100644 --- a/src/theory/theory_state.h +++ b/src/theory/theory_state.h @@ -80,6 +80,9 @@ class TheoryState */ TheoryModel* getModel(); + /** Returns true if n has a current SAT assignment and stores it in value. */ + virtual bool hasSatValue(TNode n, bool& value) const; + protected: /** Pointer to the SAT context object used by the theory. */ context::Context* d_context; diff --git a/test/regress/regress0/bv/ackermann1.smt2 b/test/regress/regress0/bv/ackermann1.smt2 index 7fd76c8cc..bdf74ce49 100644 --- a/test/regress/regress0/bv/ackermann1.smt2 +++ b/test/regress/regress0/bv/ackermann1.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-unsat-cores +; COMMAND-LINE: --bitblast=eager --bv-solver=simple --no-check-models --no-check-unsat-cores ; EXPECT: sat (set-logic QF_UFBV) (set-info :smt-lib-version 2.0) diff --git a/test/regress/regress0/bv/bool-model.smt2 b/test/regress/regress0/bv/bool-model.smt2 index 30531418c..f30dbef6f 100644 --- a/test/regress/regress0/bv/bool-model.smt2 +++ b/test/regress/regress0/bv/bool-model.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --bitblast=eager +; COMMAND-LINE: --bitblast=eager --bv-solver=simple (set-info :status sat) (set-logic QF_BV) (declare-fun x () Bool) diff --git a/test/regress/regress0/bv/bool-to-bv-ite.smt2 b/test/regress/regress0/bv/bool-to-bv-ite.smt2 index e1be3ea10..de0ec8897 100644 --- a/test/regress/regress0/bv/bool-to-bv-ite.smt2 +++ b/test/regress/regress0/bv/bool-to-bv-ite.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --bool-to-bv=ite +; COMMAND-LINE: --bool-to-bv=ite --bv-solver=simple ; EXPECT: sat (set-logic QF_BV) (declare-fun x2 () (_ BitVec 3)) diff --git a/test/regress/regress0/bv/bug734.smt2 b/test/regress/regress0/bv/bug734.smt2 index 1747c6cc4..5e92036ec 100644 --- a/test/regress/regress0/bv/bug734.smt2 +++ b/test/regress/regress0/bv/bug734.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --incremental +; COMMAND-LINE: --incremental --bv-solver=simple ; EXPECT: sat ; EXPECT: sat (set-logic QF_BV) diff --git a/test/regress/regress0/bv/issue-4076.smt2 b/test/regress/regress0/bv/issue-4076.smt2 index c52d2169a..e94779439 100644 --- a/test/regress/regress0/bv/issue-4076.smt2 +++ b/test/regress/regress0/bv/issue-4076.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --incremental +; COMMAND-LINE: --incremental --bv-solver=simple ; EXPECT: sat ; EXPECT: sat (set-logic ALL) diff --git a/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 b/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 index 7cc75ef62..0888031d5 100644 --- a/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 +++ b/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 @@ -1,4 +1,5 @@ ; COMMAND-LINE: --no-bv-div-zero-const --no-check-unsat-cores +; COMMAND-LINE: --bv-solver=simple --no-bv-div-zero-const --no-check-unsat-cores (set-logic QF_BV) (set-info :status sat) (declare-const x (_ BitVec 4)) diff --git a/test/regress/regress1/bug520.smt2 b/test/regress/regress1/bug520.smt2 index 0965487e1..cfafc0a0a 100644 --- a/test/regress/regress1/bug520.smt2 +++ b/test/regress/regress1/bug520.smt2 @@ -1,5 +1,6 @@ ; COMMAND-LINE: --bitblast=lazy ; COMMAND-LINE: --bitblast=eager --no-check-models +; COMMAND-LINE: --bv-solver=simple ; EXPECT: sat ; Automatically generated by SBV. Do not edit. (set-logic QF_UFBV) -- 2.30.2