updated preprocessing and rewriting input equalities into inequalities for LRA

1 files changed, 7 insertions, 6 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;
 }