summaryrefslogtreecommitdiff
path: root/src/smt
diff options
context:
space:
mode:
Diffstat (limited to 'src/smt')
-rw-r--r--src/smt/smt_engine.cpp3
1 files changed, 3 insertions, 0 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e73af60e9..97407a425 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -291,6 +291,9 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
setTimeLimit(Options::current()->cumulativeMillisecondLimit, true);
}
+
+ d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(true));
+ d_propEngine->assertFormula(NodeManager::currentNM()->mkConst<bool>(false).notNode());
}
void SmtEngine::shutdown() {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback