diff options
| author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2021-02-22 16:07:16 -0600 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-02-22 16:07:16 -0600 |
| commit | 71d72df0437607723256bbd7b4f28cd6c89fe40f (patch) | |
| tree | 1021b9e166290db4637a0be447da359d0aed4752 /src/prop/prop_engine.cpp | |
| parent | 580f3e93c2cc4564e6fa87d07426dc1ff87224e4 (diff) | |
(proof-new) Change proof-new option to proof (#5955)
Also moves several proof-specific options to proof_options.
Diffstat (limited to 'src/prop/prop_engine.cpp')
| -rw-r--r-- | src/prop/prop_engine.cpp | 5 |
1 files changed, 2 insertions, 3 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index e99e11eb2..738b4dc9c 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -27,6 +27,7 @@ #include "options/decision_options.h" #include "options/main_options.h" #include "options/options.h" +#include "options/proof_options.h" #include "options/smt_options.h" #include "proof/proof_manager.h" #include "prop/cnf_stream.h" @@ -36,7 +37,6 @@ #include "prop/theory_proxy.h" #include "smt/smt_statistics_registry.h" #include "theory/output_channel.h" -#include "theory/rewriter.h" #include "theory/theory_engine.h" #include "util/resource_manager.h" #include "util/result.h" @@ -205,7 +205,7 @@ void PropEngine::assertLemma(theory::TrustNode tlemma, theory::LemmaProperty p) Assert(ppSkolems.size() == ppLemmas.size()); // do final checks on the lemmas we are about to send - if (isProofEnabled() && options::proofNewEagerChecking()) + if (isProofEnabled() && options::proofEagerChecking()) { Assert(tplemma.getGenerator() != nullptr); // ensure closed, make the proof node eagerly here to debug @@ -444,7 +444,6 @@ Node PropEngine::ensureLiteral(TNode n) Node PropEngine::getPreprocessedTerm(TNode n) { - Node rewritten = theory::Rewriter::rewrite(n); // must preprocess std::vector<theory::TrustNode> newLemmas; std::vector<Node> newSkolems; |