diff options
Diffstat (limited to 'src/prop/prop_engine.cpp')
| -rw-r--r-- | src/prop/prop_engine.cpp | 9 |
1 files changed, 5 insertions, 4 deletions
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp index 82c0bae1a..a02e40e32 100644 --- a/src/prop/prop_engine.cpp +++ b/src/prop/prop_engine.cpp @@ -25,6 +25,7 @@ #include "decision/options.h" #include "theory/theory_engine.h" #include "theory/theory_registrar.h" +#include "proof/proof_manager.h" #include "util/cvc4_assert.h" #include "options/options.h" #include "smt/options.h" @@ -109,15 +110,15 @@ void PropEngine::assertFormula(TNode node) { Assert(!d_inCheckSat, "Sat solver in solve()!"); Debug("prop") << "assertFormula(" << node << ")" << endl; // Assert as non-removable - d_cnfStream->convertAndAssert(node, false, false); + d_cnfStream->convertAndAssert(node, false, false, RULE_GIVEN); } -void PropEngine::assertLemma(TNode node, bool negated, bool removable) { +void PropEngine::assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from) { //Assert(d_inCheckSat, "Sat solver should be in solve()!"); Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl; - // Assert as removable - d_cnfStream->convertAndAssert(node, removable, negated); + // Assert as (possibly) removable + d_cnfStream->convertAndAssert(node, removable, negated, rule, from); } void PropEngine::requirePhase(TNode n, bool phase) { |