diff options
Diffstat (limited to 'src/smt/assertions.cpp')
| -rw-r--r-- | src/smt/assertions.cpp | 26 |
1 files changed, 15 insertions, 11 deletions
diff --git a/src/smt/assertions.cpp b/src/smt/assertions.cpp index ea3acf2d1..8019c383d 100644 --- a/src/smt/assertions.cpp +++ b/src/smt/assertions.cpp @@ -17,7 +17,6 @@ #include "expr/node_algorithm.h" #include "options/base_options.h" #include "options/language.h" -#include "options/proof_options.h" #include "options/smt_options.h" #include "proof/proof_manager.h" #include "smt/smt_engine.h" @@ -179,18 +178,23 @@ void Assertions::addFormula( } // Give it to proof manager - PROOF(if (inInput) { - // n is an input assertion - if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores() - || options::checkUnsatCores() || options::fewerPreprocessingHoles()) + if (options::unsatCores()) + { + if (inInput) + { // n is an input assertion + if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores() + || options::checkUnsatCores()) + { + ProofManager::currentPM()->addCoreAssertion(n.toExpr()); + } + } + else { - ProofManager::currentPM()->addCoreAssertion(n.toExpr()); + // n is the result of an unknown preprocessing step, add it to dependency + // map to null + ProofManager::currentPM()->addDependence(n, Node::null()); } - } 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); |