summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_engine.cpp')
-rw-r--r--src/theory/theory_engine.cpp5
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;
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback