1 files changed, 36 insertions, 0 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index f8667fb71..f9539a1a4 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -194,6 +194,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw(AssertionException) :
   d_logic(""),
   d_problemExtended(false),
   d_queryMade(false),
+  d_needPostsolve(false),
   d_timeBudgetCumulative(0),
   d_timeBudgetPerCall(0),
   d_resourceBudgetCumulative(0),
@@ -253,6 +254,13 @@ void SmtEngine::shutdown() {
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << QuitCommand() << endl;
   }
+
+  // check to see if a postsolve() is pending
+  if(d_needPostsolve) {
+    d_theoryEngine->postsolve();
+    d_needPostsolve = false;
+  }
+
   d_propEngine->shutdown();
   d_theoryEngine->shutdown();
 }
@@ -863,6 +871,12 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
     ensureBoolean(e);
   }
 
+  // check to see if a postsolve() is pending
+  if(d_needPostsolve) {
+    d_theoryEngine->postsolve();
+    d_needPostsolve = false;
+  }
+
   // Push the context
   internalPush();
 
@@ -877,6 +891,7 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
 
   // Run the check
   Result r = check().asSatisfiabilityResult();
+  d_needPostsolve = true;
 
   // Dump the query if requested
   if(Dump.isOn("benchmark")) {
@@ -915,6 +930,12 @@ Result SmtEngine::query(const BoolExpr& e) {
   // Ensure that the expression is type-checked at this point, and Boolean
   ensureBoolean(e);
 
+  // check to see if a postsolve() is pending
+  if(d_needPostsolve) {
+    d_theoryEngine->postsolve();
+    d_needPostsolve = false;
+  }
+
   // Push the context
   internalPush();
 
@@ -927,6 +948,7 @@ Result SmtEngine::query(const BoolExpr& e) {
 
   // Run the check
   Result r = check().asValidityResult();
+  d_needPostsolve = true;
 
   // Dump the query if requested
   if(Dump.isOn("benchmark")) {
@@ -1157,6 +1179,13 @@ void SmtEngine::push() {
   if(!Options::current()->incrementalSolving) {
     throw ModalException("Cannot push when not solving incrementally (use --incremental)");
   }
+
+  // check to see if a postsolve() is pending
+  if(d_needPostsolve) {
+    d_theoryEngine->postsolve();
+    d_needPostsolve = false;
+  }
+
   d_userLevels.push_back(d_userContext->getLevel());
   internalPush();
   Trace("userpushpop") << "SmtEngine: pushed to level "
@@ -1175,6 +1204,13 @@ void SmtEngine::pop() {
   if(d_userContext->getLevel() == 0) {
     throw ModalException("Cannot pop beyond the first user frame");
   }
+
+  // check to see if a postsolve() is pending
+  if(d_needPostsolve) {
+    d_theoryEngine->postsolve();
+    d_needPostsolve = false;
+  }
+
   AlwaysAssert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel());
   while (d_userLevels.back() < d_userContext->getLevel()) {
     internalPop();