Fixes a bug where registration occurs before preregistration.

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 1a0b25ade4dbf2d4609f5a8a1142bc23b8f7caf0..9af4fc572e7b94310122ebe628f3d9e1e941cd7a 100644 (file)
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -86,7 +86,8 @@ Node TheoryEngine::preprocess(TNode t) {
 
   return top;
 }
-  /* Our goal is to tease out any ITE's sitting under a theory operator. */
+
+/* Our goal is to tease out any ITE's sitting under a theory operator. */
 Node TheoryEngine::removeITEs(TNode node) {
   Debug("ite") << "handleNonAtomicNode(" << node << ")" << endl;
 
@@ -118,7 +119,7 @@ Node TheoryEngine::removeITEs(TNode node) {
                      << endl;
       }
 
-      Node preprocessed = rewrite(newAssertion);
+      Node preprocessed = preprocess(newAssertion);
       d_propEngine->assertFormula(preprocessed);
 
       return skolem;