Changes to Solver and PropEngine to support lemmasOnDemand during solve but not yet in d_checkSat.

1 files changed, 3 insertions, 8 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index f3caead8b..ab1afceba 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -81,19 +81,14 @@ void PropEngine::assertFormula(TNode node) {
 }
 
 void PropEngine::assertLemma(TNode node) {
-  Assert(d_inCheckSat, "Sat solver should be in solve()!");
+  //Assert(d_inCheckSat, "Sat solver should be in solve()!");
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
+
+  //TODO This comment is now false
   // Assert as removable
   d_cnfStream->convertAndAssert(node, true, false);
 }
 
-void PropEngine::assertSafeLemma(TNode node) {
-  if(d_inCheckSat){
-    assertLemma(node);
-  }else{
-    assertFormula(node);
-  }
-}
 
 void PropEngine::printSatisfyingAssignment(){
   const CnfStream::TranslationCache& transCache =