diff options
Diffstat (limited to 'src/smt/assertions.cpp')
| -rw-r--r-- | src/smt/assertions.cpp | 20 |
1 files changed, 0 insertions, 20 deletions
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index 7dc2e915d..504dce71e 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -23,7 +23,6 @@ #include "options/expr_options.h" #include "options/language.h" #include "options/smt_options.h" -#include "proof/proof_manager.h" #include "smt/abstract_values.h" #include "smt/env.h" #include "smt/smt_engine.h" @@ -193,25 +192,6 @@ void Assertions::addFormula(TNode n, } } - // Give it to the old proof manager - if (options::unsatCoresMode() == options::UnsatCoresMode::OLD_PROOF) - { - if (inInput) - { // n is an input assertion - if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores() - || options::checkUnsatCores()) - { - ProofManager::currentPM()->addCoreAssertion(n); - } - } - else - { - // n is the result of an unknown preprocessing step, add it to dependency - // map to null - ProofManager::currentPM()->addDependence(n, Node::null()); - } - } - // Add the normalized formula to the queue d_assertions.push_back(n, isAssumption, true); } |