Fixes a bug where registration occurs before preregistration.

1 files changed, 3 insertions, 2 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 1a0b25ade..9af4fc572 100644
--- 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;