summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2010-03-11 21:53:38 +0000
committerMorgan Deters <mdeters@gmail.com>2010-03-11 21:53:38 +0000
commit3cf73e344987c2449943ca3a97054565eb9d5726 (patch)
tree7e9448caaabb7cb3261de74031070eb5c50b864d /src/smt
parent90d829959edf8ad97bd837230933c8443f63b95b (diff)
naive rewriting to fix minisat invariant; rewrite x == x ==> TRUE
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/smt_engine.cpp2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 6e3a1b801..e97adb1d2 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -88,7 +88,7 @@ void SmtEngine::doCommand(Command* c) {
}
Node SmtEnginePrivate::preprocess(SmtEngine& smt, TNode e) {
- return e;
+ return smt.d_theoryEngine->preprocess(e);
}
Result SmtEngine::check() {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback