updated preprocessing and rewriting input equalities into inequalities for LRA

2 files changed, 8 insertions, 8 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 6732b09bc..0967f54ff 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -121,15 +121,16 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
     d_nodeCache[~lit] = node.notNode();
   }
 
+  // If a theory literal, we pre-register it
+  if (theoryLiteral) {
+    bool backup = d_assertingLemma;
+    d_registrar.preRegister(node);
+    d_assertingLemma = backup;
+  }
+
   // Here, you can have it
   Debug("cnf") << "newLiteral(" << node << ") => " << lit << endl;
 
-  // have to keep track of this, because with the call to preRegister(),
-  // the cnf stream is re-entrant!
-  bool wasAssertingLemma = d_assertingLemma;
-  d_registrar.preRegister(node);
-  d_assertingLemma = wasAssertingLemma;
-
   return lit;
 }
 
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 63228a803..7e335a21b 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -81,7 +81,7 @@ 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(d_theoryEngine->preprocess(node), false, false);
 }
 
 void PropEngine::assertLemma(TNode node) {
@@ -93,7 +93,6 @@ void PropEngine::assertLemma(TNode node) {
   d_cnfStream->convertAndAssert(node, true, false);
 }
 
-
 void PropEngine::printSatisfyingAssignment(){
   const CnfStream::TranslationCache& transCache =
     d_cnfStream->getTranslationCache();