From: Tim King <taking@cs.nyu.edu>
Date: Thu, 3 Jun 2010 18:26:15 +0000 (+0000)
Subject: Fixes a bug where registration occurs before preregistration.
X-Git-Tag: cvc5-1.0.0~9005
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=65eb6421b58ab943414749251a63b85f34e801ec;p=cvc5.git

Fixes a bug where registration occurs before preregistration.
---

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;