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, 2 insertions, 1 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index cb6dd3460..6ea9de45e 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -463,7 +463,8 @@ void SmtEnginePrivate::addFormula(SmtEngine& smt, TNode n)
throw(NoSuchFunctionException, AssertionException) {
Debug("smt") << "push_back assertion " << n << endl;
smt.d_haveAdditions = true;
- smt.d_propEngine->assertFormula(SmtEnginePrivate::preprocess(smt, n));
+ Node node = SmtEnginePrivate::preprocess(smt, n);
+ smt.d_propEngine->assertFormula(node);
}
void SmtEngine::ensureBoolean(const BoolExpr& e) {
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback