diff options
author | Tim King <taking@cs.nyu.edu> | 2010-06-03 18:26:15 +0000 |
---|---|---|
committer | Tim King <taking@cs.nyu.edu> | 2010-06-03 18:26:15 +0000 |
commit | 65eb6421b58ab943414749251a63b85f34e801ec (patch) | |
tree | 071dd22220fab41c14f3bf1c6c762b233d7c1de4 | |
parent | a120ebfd29062a8681f8a1e03c598bc9c7c2a790 (diff) |
Fixes a bug where registration occurs before preregistration.
-rw-r--r-- | src/theory/theory_engine.cpp | 5 |
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; |