From: Mathias Preiner Date: Thu, 15 Jul 2021 01:27:33 +0000 (-0700) Subject: bv: Rename simple solver to bitblast-internal. (#6888) X-Git-Tag: cvc5-1.0.0~1485 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=ffdf7434ba53191546e13663764894852e8bc6dd;p=cvc5.git bv: Rename simple solver to bitblast-internal. (#6888) --- diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e001dd462..8dc1f986f 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -589,10 +589,10 @@ libcvc5_add_sources( theory/bv/bv_solver.h theory/bv/bv_solver_bitblast.cpp theory/bv/bv_solver_bitblast.h + theory/bv/bv_solver_bitblast_internal.cpp + theory/bv/bv_solver_bitblast_internal.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 8d4c2b1de..3faf9a111 100644 --- a/src/options/bv_options.toml +++ b/src/options/bv_options.toml @@ -220,9 +220,9 @@ name = "Bitvector Theory" [[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." +[[option.mode.BITBLAST_INTERNAL]] + name = "bitblast-internal" + help = "Enables bitblasting to internal SAT solver with proof support." [[option]] name = "bvAssertInput" diff --git a/src/theory/bv/bv_solver_bitblast_internal.cpp b/src/theory/bv/bv_solver_bitblast_internal.cpp new file mode 100644 index 000000000..bd47cc45e --- /dev/null +++ b/src/theory/bv/bv_solver_bitblast_internal.cpp @@ -0,0 +1,157 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Gereon Kremer, Haniel Barbosa + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Bit-blast solver that sends bit-blast lemmas directly to the internal + * MiniSat. + */ + +#include "theory/bv/bv_solver_bitblast_internal.h" + +#include "proof/conv_proof_generator.h" +#include "theory/bv/theory_bv.h" +#include "theory/bv/theory_bv_utils.h" +#include "theory/theory_model.h" + +namespace cvc5 { +namespace theory { +namespace bv { + +/* -------------------------------------------------------------------------- */ + +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 + +BVSolverBitblastInternal::BVSolverBitblastInternal( + TheoryState* s, TheoryInferenceManager& inferMgr, ProofNodeManager* pnm) + : BVSolver(*s, inferMgr), + d_pnm(pnm), + d_bitblaster(new BBProof(s, pnm, false)) +{ +} + +void BVSolverBitblastInternal::addBBLemma(TNode fact) +{ + if (!d_bitblaster->hasBBAtom(fact)) + { + d_bitblaster->bbAtom(fact); + } + NodeManager* nm = NodeManager::currentNM(); + + Node atom_bb = d_bitblaster->getStoredBBAtom(fact); + Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb); + + if (d_pnm == nullptr) + { + d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA); + } + else + { + TrustNode tlem = + TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator()); + d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA); + } +} + +bool BVSolverBitblastInternal::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); + + if (d_pnm == nullptr) + { + d_im.lemma(lemma, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA); + } + else + { + d_bitblaster->getProofGenerator()->addRewriteStep( + fact, n, PfRule::BV_EAGER_ATOM, {}, {fact}); + TrustNode tlem = + TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator()); + d_im.trustedLemma(tlem, InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA); + } + + std::unordered_set bv_atoms; + collectBVAtoms(n, bv_atoms); + for (const Node& nn : bv_atoms) + { + addBBLemma(nn); + } + } + + return true; +} + +bool BVSolverBitblastInternal::collectModelValues(TheoryModel* m, + const std::set& termSet) +{ + return d_bitblaster->collectModelValues(m, termSet); +} + +BVProofRuleChecker* BVSolverBitblastInternal::getProofChecker() +{ + return &d_checker; +} + +} // namespace bv +} // namespace theory +} // namespace cvc5 diff --git a/src/theory/bv/bv_solver_bitblast_internal.h b/src/theory/bv/bv_solver_bitblast_internal.h new file mode 100644 index 000000000..8a1886084 --- /dev/null +++ b/src/theory/bv/bv_solver_bitblast_internal.h @@ -0,0 +1,80 @@ +/****************************************************************************** + * Top contributors (to current version): + * Mathias Preiner, Haniel Barbosa, Andrew Reynolds + * + * This file is part of the cvc5 project. + * + * Copyright (c) 2009-2021 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. + * **************************************************************************** + * + * Bit-blast solver that sends bit-blast lemmas directly to the internal + * MiniSat. + */ + +#include "cvc5_private.h" + +#ifndef CVC5__THEORY__BV__BV_SOLVER_BITBLAST_INTERNAL_H +#define CVC5__THEORY__BV__BV_SOLVER_BITBLAST_INTERNAL_H + +#include "theory/bv/bitblast/proof_bitblaster.h" +#include "theory/bv/bv_solver.h" +#include "theory/bv/proof_checker.h" + +namespace cvc5 { +namespace theory { +namespace bv { + +/** + * 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 BVSolverBitblastInternal : public BVSolver +{ + public: + BVSolverBitblastInternal(TheoryState* state, + TheoryInferenceManager& inferMgr, + ProofNodeManager* pnm); + ~BVSolverBitblastInternal() = 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 "BVSolverBitblastInternal"; }; + + bool collectModelValues(TheoryModel* m, + const std::set& termSet) override; + + /** get the proof checker of this theory */ + BVProofRuleChecker* getProofChecker(); + + private: + /** + * Sends a bit-blasting lemma fact <=> d_bitblaster.bbAtom(fact) to the + * inference manager. + */ + void addBBLemma(TNode fact); + + /** Proof node manager. */ + ProofNodeManager* d_pnm; + /** Bit-blaster used to bit-blast atoms/terms. */ + std::unique_ptr d_bitblaster; + /** Proof rule checker */ + BVProofRuleChecker d_checker; +}; + +} // namespace bv +} // namespace theory +} // namespace cvc5 + +#endif diff --git a/src/theory/bv/bv_solver_simple.cpp b/src/theory/bv/bv_solver_simple.cpp deleted file mode 100644 index 414de41ce..000000000 --- a/src/theory/bv/bv_solver_simple.cpp +++ /dev/null @@ -1,154 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mathias Preiner, Gereon Kremer, Haniel Barbosa - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Simple bit-blast solver that sends bitblast lemmas directly to MiniSat. - */ - -#include "theory/bv/bv_solver_simple.h" - -#include "proof/conv_proof_generator.h" -#include "theory/bv/theory_bv.h" -#include "theory/bv/theory_bv_utils.h" -#include "theory/theory_model.h" - -namespace cvc5 { -namespace theory { -namespace bv { - -/* -------------------------------------------------------------------------- */ - -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, - ProofNodeManager* pnm) - : BVSolver(*s, inferMgr), - d_pnm(pnm), - d_bitblaster(new BBProof(s, pnm, false)) -{ -} - -void BVSolverSimple::addBBLemma(TNode fact) -{ - if (!d_bitblaster->hasBBAtom(fact)) - { - d_bitblaster->bbAtom(fact); - } - NodeManager* nm = NodeManager::currentNM(); - - Node atom_bb = d_bitblaster->getStoredBBAtom(fact); - Node lemma = nm->mkNode(kind::EQUAL, fact, atom_bb); - - if (d_pnm == nullptr) - { - d_im.lemma(lemma, InferenceId::BV_SIMPLE_BITBLAST_LEMMA); - } - else - { - TrustNode tlem = - TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator()); - d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_BITBLAST_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); - - if (d_pnm == nullptr) - { - d_im.lemma(lemma, InferenceId::BV_SIMPLE_LEMMA); - } - else - { - d_bitblaster->getProofGenerator()->addRewriteStep( - fact, n, PfRule::BV_EAGER_ATOM, {}, {fact}); - TrustNode tlem = - TrustNode::mkTrustLemma(lemma, d_bitblaster->getProofGenerator()); - d_im.trustedLemma(tlem, InferenceId::BV_SIMPLE_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); -} - -BVProofRuleChecker* BVSolverSimple::getProofChecker() { return &d_checker; } - -} // namespace bv -} // namespace theory -} // namespace cvc5 diff --git a/src/theory/bv/bv_solver_simple.h b/src/theory/bv/bv_solver_simple.h deleted file mode 100644 index 0af4f5b89..000000000 --- a/src/theory/bv/bv_solver_simple.h +++ /dev/null @@ -1,82 +0,0 @@ -/****************************************************************************** - * Top contributors (to current version): - * Mathias Preiner, Haniel Barbosa, Andrew Reynolds - * - * This file is part of the cvc5 project. - * - * Copyright (c) 2009-2021 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. - * **************************************************************************** - * - * Simple bit-blast solver that sends bit-blast lemmas directly to MiniSat. - */ - -#include "cvc5_private.h" - -#ifndef CVC5__THEORY__BV__BV_SOLVER_SIMPLE_H -#define CVC5__THEORY__BV__BV_SOLVER_SIMPLE_H - -#include "theory/bv/bitblast/proof_bitblaster.h" -#include "theory/bv/bv_solver.h" -#include "theory/bv/proof_checker.h" - -namespace cvc5 { - -class TConvProofGenerator; - -namespace theory { -namespace bv { - -/** - * 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, - ProofNodeManager* pnm); - ~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"; }; - - bool collectModelValues(TheoryModel* m, - const std::set& termSet) override; - - /** get the proof checker of this theory */ - BVProofRuleChecker* getProofChecker(); - - private: - /** - * Sends a bit-blasting lemma fact <=> d_bitblaster.bbAtom(fact) to the - * inference manager. - */ - void addBBLemma(TNode fact); - - /** Proof node manager. */ - ProofNodeManager* d_pnm; - /** Bit-blaster used to bit-blast atoms/terms. */ - std::unique_ptr d_bitblaster; - /** Proof rule checker */ - BVProofRuleChecker d_checker; -}; - -} // namespace bv -} // namespace theory -} // namespace cvc5 - -#endif diff --git a/src/theory/bv/theory_bv.cpp b/src/theory/bv/theory_bv.cpp index 3d7f11f6d..b3cf6da59 100644 --- a/src/theory/bv/theory_bv.cpp +++ b/src/theory/bv/theory_bv.cpp @@ -20,8 +20,8 @@ #include "proof/proof_checker.h" #include "smt/smt_statistics_registry.h" #include "theory/bv/bv_solver_bitblast.h" +#include "theory/bv/bv_solver_bitblast_internal.h" #include "theory/bv/bv_solver_lazy.h" -#include "theory/bv/bv_solver_simple.h" #include "theory/bv/theory_bv_utils.h" #include "theory/ee_setup_info.h" #include "theory/trust_substitutions.h" @@ -56,8 +56,8 @@ TheoryBV::TheoryBV(context::Context* c, break; default: - AlwaysAssert(options::bvSolver() == options::BVSolver::SIMPLE); - d_internal.reset(new BVSolverSimple(&d_state, d_im, pnm)); + AlwaysAssert(options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL); + d_internal.reset(new BVSolverBitblastInternal(&d_state, d_im, pnm)); } d_theoryState = &d_state; d_inferManager = &d_im; @@ -69,9 +69,10 @@ TheoryRewriter* TheoryBV::getTheoryRewriter() { return &d_rewriter; } ProofRuleChecker* TheoryBV::getProofChecker() { - if (options::bvSolver() == options::BVSolver::SIMPLE) + if (options::bvSolver() == options::BVSolver::BITBLAST_INTERNAL) { - return static_cast(d_internal.get())->getProofChecker(); + return static_cast(d_internal.get()) + ->getProofChecker(); } return nullptr; } diff --git a/src/theory/inference_id.cpp b/src/theory/inference_id.cpp index 0ef0ad6bd..612c99d82 100644 --- a/src/theory/inference_id.cpp +++ b/src/theory/inference_id.cpp @@ -112,8 +112,10 @@ const char* toString(InferenceId i) case InferenceId::BV_BITBLAST_CONFLICT: return "BV_BITBLAST_CONFLICT"; case InferenceId::BV_LAZY_CONFLICT: return "BV_LAZY_CONFLICT"; case InferenceId::BV_LAZY_LEMMA: return "BV_LAZY_LEMMA"; - case InferenceId::BV_SIMPLE_LEMMA: return "BV_SIMPLE_LEMMA"; - case InferenceId::BV_SIMPLE_BITBLAST_LEMMA: return "BV_SIMPLE_BITBLAST_LEMMA"; + case InferenceId::BV_BITBLAST_INTERNAL_EAGER_LEMMA: + return "BV_BITBLAST_EAGER_LEMMA"; + case InferenceId::BV_BITBLAST_INTERNAL_BITBLAST_LEMMA: + return "BV_BITBLAST_INTERNAL_BITBLAST_LEMMA"; case InferenceId::BV_EXTF_LEMMA: return "BV_EXTF_LEMMA"; case InferenceId::BV_EXTF_COLLAPSE: return "BV_EXTF_COLLAPSE"; diff --git a/src/theory/inference_id.h b/src/theory/inference_id.h index ba268b396..ebbccfd54 100644 --- a/src/theory/inference_id.h +++ b/src/theory/inference_id.h @@ -175,8 +175,8 @@ enum class InferenceId BV_BITBLAST_CONFLICT, BV_LAZY_CONFLICT, BV_LAZY_LEMMA, - BV_SIMPLE_LEMMA, - BV_SIMPLE_BITBLAST_LEMMA, + BV_BITBLAST_INTERNAL_EAGER_LEMMA, + BV_BITBLAST_INTERNAL_BITBLAST_LEMMA, BV_EXTF_LEMMA, BV_EXTF_COLLAPSE, // ---------------------------------- end bitvector theory diff --git a/test/regress/regress0/bv/ackermann1.smt2 b/test/regress/regress0/bv/ackermann1.smt2 index 579e438a5..f70dc4a3d 100644 --- a/test/regress/regress0/bv/ackermann1.smt2 +++ b/test/regress/regress0/bv/ackermann1.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --bitblast=eager --no-check-models -; COMMAND-LINE: --bitblast=eager --bv-solver=simple --no-check-models +; COMMAND-LINE: --bitblast=eager --bv-solver=bitblast-internal --no-check-models ; EXPECT: sat (set-logic QF_UFBV) (set-info :smt-lib-version 2.6) diff --git a/test/regress/regress0/bv/bool-model.smt2 b/test/regress/regress0/bv/bool-model.smt2 index f30dbef6f..2a2998b35 100644 --- a/test/regress/regress0/bv/bool-model.smt2 +++ b/test/regress/regress0/bv/bool-model.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --bitblast=eager -; COMMAND-LINE: --bitblast=eager --bv-solver=simple +; COMMAND-LINE: --bitblast=eager --bv-solver=bitblast-internal (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 de0ec8897..09fcb4e11 100644 --- a/test/regress/regress0/bv/bool-to-bv-ite.smt2 +++ b/test/regress/regress0/bv/bool-to-bv-ite.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --bool-to-bv=ite -; COMMAND-LINE: --bool-to-bv=ite --bv-solver=simple +; COMMAND-LINE: --bool-to-bv=ite --bv-solver=bitblast-internal ; 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 5e92036ec..0e392d3c6 100644 --- a/test/regress/regress0/bv/bug734.smt2 +++ b/test/regress/regress0/bv/bug734.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --incremental -; COMMAND-LINE: --incremental --bv-solver=simple +; COMMAND-LINE: --incremental --bv-solver=bitblast-internal ; 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 e94779439..12bc3e4ca 100644 --- a/test/regress/regress0/bv/issue-4076.smt2 +++ b/test/regress/regress0/bv/issue-4076.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: --incremental -; COMMAND-LINE: --incremental --bv-solver=simple +; COMMAND-LINE: --incremental --bv-solver=bitblast-internal ; 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 0c6e7e0eb..2a924dac8 100644 --- a/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 +++ b/test/regress/regress0/bv/pr4993-bvugt-bvurem-b.smt2 @@ -1,5 +1,5 @@ ; COMMAND-LINE: -; COMMAND-LINE: --bv-solver=simple +; COMMAND-LINE: --bv-solver=bitblast-internal (set-logic QF_BV) (set-info :status unsat) (declare-const x (_ BitVec 4)) diff --git a/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2 b/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2 index 98d75d74f..8cb717258 100644 --- a/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2 +++ b/test/regress/regress0/proofs/open-pf-if-unordered-iff.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --bv-solver=simple +; COMMAND-LINE: --bv-solver=bitblast-internal ; EXPECT: unsat (set-logic ALL) (declare-const __ (_ BitVec 3)) diff --git a/test/regress/regress0/proofs/open-pf-rederivation.smt2 b/test/regress/regress0/proofs/open-pf-rederivation.smt2 index 7095ec942..877389184 100644 --- a/test/regress/regress0/proofs/open-pf-rederivation.smt2 +++ b/test/regress/regress0/proofs/open-pf-rederivation.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --bv-solver=simple +; COMMAND-LINE: --bv-solver=bitblast-internal ; EXPECT: unsat (set-logic ALL) (declare-const __ (_ BitVec 7)) diff --git a/test/regress/regress1/bug520.smt2 b/test/regress/regress1/bug520.smt2 index cfafc0a0a..238fec914 100644 --- a/test/regress/regress1/bug520.smt2 +++ b/test/regress/regress1/bug520.smt2 @@ -1,6 +1,6 @@ ; COMMAND-LINE: --bitblast=lazy ; COMMAND-LINE: --bitblast=eager --no-check-models -; COMMAND-LINE: --bv-solver=simple +; COMMAND-LINE: --bv-solver=bitblast-internal ; EXPECT: sat ; Automatically generated by SBV. Do not edit. (set-logic QF_UFBV)