This commit merges the arith-prop-opt branch into the main trunk. This was done by way of the intermediate branch arith-prop-tmp. Both arith-prop-opt and arith-prop-tmp will now be phased out.

2 files changed, 8 insertions, 0 deletions

diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index d89b8ec2f..f3caead8b 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -87,6 +87,13 @@ void PropEngine::assertLemma(TNode node) {
   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 =
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index b43c2d859..c0483e943 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -103,6 +103,7 @@ public:
    * @param node the formula to assert
    */
   void assertLemma(TNode node);
+  void assertSafeLemma(TNode node);
 
   /**
    * Checks the current context for satisfiability.