From 65eb6421b58ab943414749251a63b85f34e801ec Mon Sep 17 00:00:00 2001 From: Tim King Date: Thu, 3 Jun 2010 18:26:15 +0000 Subject: [PATCH] Fixes a bug where registration occurs before preregistration. --- src/theory/theory_engine.cpp | 5 +++-- 1 file 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; -- 2.30.2