1 files changed, 3 insertions, 2 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 05ee12462..412c0f3af 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -27,11 +27,12 @@ void SmtEngine::processAssertionList() {
   for(std::vector<Expr>::iterator i = d_assertions.begin();
       i != d_assertions.end();
       ++i)
-    ;//d_expr = d_expr.isNull() ? *i : d_expr.andExpr(*i);
+    d_expr = d_expr.isNull() ? *i : d_expr.andExpr(*i);
 }
 
 Result SmtEngine::check() {
   processAssertionList();
+  d_prop.solve(d_expr);
   return Result(Result::VALIDITY_UNKNOWN);
 }
 
@@ -56,7 +57,7 @@ Result SmtEngine::query(Expr e) {
   return check();
 }
 
-Result SmtEngine::assert(Expr e) {
+Result SmtEngine::assertFormula(Expr e) {
   e = preprocess(e);
   addFormula(e);
   return quickCheck();