Split Assertions from SmtEngine (#4788)

This splits all things related to storing assertions in the SmtEngine into a separate class "Assertions". It also converts the interface for its methods from Expr to Node.

1 files changed, 85 insertions, 243 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index e5b95d656..43aa3b0c8 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -82,6 +82,7 @@
 #include "prop/prop_engine.h"
 #include "smt/abduction_solver.h"
 #include "smt/abstract_values.h"
+#include "smt/assertions.h"
 #include "smt/expr_names.h"
 #include "smt/command.h"
 #include "smt/defined_function.h"
@@ -162,9 +163,6 @@ class SmtEnginePrivate
   /** A circuit propagator for non-clausal propositional deduction */
   booleans::CircuitPropagator d_propagator;
 
-  /** Assertions in the preprocessing pipeline */
-  AssertionPipeline d_assertions;
-
   /** Whether any assertions have been processed */
   CDO<bool> d_assertionsProcessed;
 
@@ -178,7 +176,6 @@ class SmtEnginePrivate
   ProcessAssertions d_processor;
 
  public:
-  IteSkolemMap& getIteSkolemMap() { return d_assertions.getIteSkolemMap(); }
 
   /** Instance of the ITE remover */
   RemoveTermFormulas d_iteRemover;
@@ -208,7 +205,6 @@ class SmtEnginePrivate
   SmtEnginePrivate(SmtEngine& smt)
       : d_smt(smt),
         d_propagator(true, true),
-        d_assertions(),
         d_assertionsProcessed(smt.getUserContext(), false),
         d_processor(smt, *smt.getResourceManager()),
         d_iteRemover(smt.getUserContext()),
@@ -241,12 +237,11 @@ class SmtEnginePrivate
   /**
    * Process the assertions that have been asserted.
    */
-  void processAssertions();
+  void processAssertions(Assertions& as);
 
   /** Process a user push.
   */
   void notifyPush() {
-
   }
 
   /**
@@ -256,32 +251,8 @@ class SmtEnginePrivate
    * last map of expression names from notifyPush.
    */
   void notifyPop() {
-    d_assertions.clear();
     d_propagator.getLearnedLiterals().clear();
-    getIteSkolemMap().clear();
   }
-
-  /**
-   * Adds a formula to the current context.  Action here depends on
-   * the SimplificationMode (in the current Options scope); the
-   * formula might be pushed out to the propositional layer
-   * immediately, or it might be simplified and kept, or it might not
-   * even be simplified.
-   * The arguments isInput and isAssumption are used for bookkeeping for proofs.
-   * The argument maybeHasFv should be set to true if the assertion may have
-   * free variables. By construction, assertions from the smt2 parser are
-   * guaranteed not to have free variables. However, other cases such as
-   * assertions from the SyGuS parser may have free variables (say if the
-   * input contains an assert or define-fun-rec command).
-   *
-   * @param isAssumption If true, the formula is considered to be an assumption
-   * (this is used to distinguish assertions and assumptions)
-   */
-  void addFormula(TNode n,
-                  bool inUnsatCore,
-                  bool inInput = true,
-                  bool isAssumption = false,
-                  bool maybeHasFv = false);
   /**
    * Simplify node "in" by expanding definitions and applying any
    * substitutions learned from preprocessing.
@@ -291,8 +262,6 @@ class SmtEnginePrivate
     // Expand definitions.
     NodeToNodeHashMap cache;
     Node n = d_processor.expandDefinitions(in, cache).toExpr();
-    // Make sure we've done all preprocessing, etc.
-    Assert(d_assertions.size() == 0);
     return applySubstitutions(n).toExpr();
   }
 };/* class SmtEnginePrivate */
@@ -306,6 +275,7 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_exprManager(em),
       d_nodeManager(d_exprManager->getNodeManager()),
       d_absValues(new AbstractValues(d_nodeManager)),
+      d_asserts(new Assertions(d_userContext.get(), *d_absValues.get())),
       d_exprNames(new ExprNames(d_userContext.get())),
       d_dumpm(new DumpManager(d_userContext.get())),
       d_routListener(new ResourceOutListener(*this)),
@@ -316,7 +286,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_rewriter(new theory::Rewriter()),
       d_definedFunctions(nullptr),
       d_abductSolver(nullptr),
-      d_assertionList(nullptr),
       d_assignments(nullptr),
       d_defineCommands(),
       d_logic(),
@@ -326,7 +295,6 @@ SmtEngine::SmtEngine(ExprManager* em, Options* optr)
       d_fullyInited(false),
       d_queryMade(false),
       d_needPostsolve(false),
-      d_globalNegation(false),
       d_status(),
       d_expectedStatus(),
       d_smtMode(SMT_MODE_START),
@@ -434,18 +402,8 @@ void SmtEngine::finishInit()
   d_userContext->push();
   d_context->push();
 
-  Trace("smt-debug") << "Set up assertion list..." << std::endl;
-  // [MGD 10/20/2011] keep around in incremental mode, due to a
-  // cleanup ordering issue and Nodes/TNodes.  If SAT is popped
-  // first, some user-context-dependent TNodes might still exist
-  // with rc == 0.
-  if(options::produceAssertions() ||
-     options::incrementalSolving()) {
-    // In the case of incremental solving, we appear to need these to
-    // ensure the relevant Nodes remain live.
-    d_assertionList = new (true) AssertionList(getUserContext());
-    d_globalDefineFunRecLemmas.reset(new std::vector<Node>());
-  }
+  Trace("smt-debug") << "Set up assertions..." << std::endl;
+  d_asserts->finishInit();
 
   // dump out a set-logic command only when raw-benchmark is disabled to avoid
   // dumping the command twice.
@@ -534,12 +492,6 @@ SmtEngine::~SmtEngine()
       d_assignments->deleteSelf();
     }
 
-    d_globalDefineFunRecLemmas.reset();
-
-    if(d_assertionList != NULL) {
-      d_assertionList->deleteSelf();
-    }
-
     d_definedFunctions->deleteSelf();
 
     //destroy all passes before destroying things that they refer to
@@ -557,6 +509,7 @@ SmtEngine::~SmtEngine()
 #endif
 
     d_absValues.reset(nullptr);
+    d_asserts.reset(nullptr);
     d_exprNames.reset(nullptr);
     d_dumpm.reset(nullptr);
 
@@ -647,12 +600,6 @@ void SmtEngine::setLogicInternal()
   d_userLogic.lock();
 }
 
-void SmtEngine::setProblemExtended()
-{
-  d_smtMode = SMT_MODE_ASSERT;
-  d_assumptions.clear();
-}
-
 void SmtEngine::setInfo(const std::string& key, const CVC4::SExpr& value)
 {
   SmtScope smts(this);
@@ -983,7 +930,6 @@ void SmtEngine::defineFunctionsRec(
   }
 
   ExprManager* em = getExprManager();
-  bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
   for (unsigned i = 0, size = funcs.size(); i < size; i++)
   {
     // we assert a quantified formula
@@ -1018,22 +964,9 @@ void SmtEngine::defineFunctionsRec(
     // assert the quantified formula
     //   notice we don't call assertFormula directly, since this would
     //   duplicate the output on raw-benchmark.
-    Node n = d_absValues->substituteAbstractValues(Node::fromExpr(lem));
-    if (d_assertionList != nullptr)
-    {
-      d_assertionList->push_back(n);
-    }
-    if (global && d_globalDefineFunRecLemmas != nullptr)
-    {
-      // Global definitions are asserted at check-sat-time because we have to
-      // make sure that they are always present
-      Assert(!language::isInputLangSygus(options::inputLanguage()));
-      d_globalDefineFunRecLemmas->emplace_back(n);
-    }
-    else
-    {
-      d_private->addFormula(n, false, true, false, maybeHasFv);
-    }
+    Node lemn = Node::fromExpr(lem);
+    // add define recursive definition to the assertions
+    d_asserts->addDefineFunRecDefinition(lemn, global);
   }
 }
 
@@ -1084,7 +1017,7 @@ Result SmtEngine::check() {
 
   // Make sure the prop layer has all of the assertions
   Trace("smt") << "SmtEngine::check(): processing assertions" << endl;
-  d_private->processAssertions();
+  d_private->processAssertions(*d_asserts);
   Trace("smt") << "SmtEngine::check(): done processing assertions" << endl;
 
   TimerStat::CodeTimer solveTimer(d_stats->d_solveTime);
@@ -1147,13 +1080,17 @@ theory::TheoryModel* SmtEngine::getAvailableModel(const char* c) const
   return m;
 }
 
-void SmtEnginePrivate::processAssertions() {
+void SmtEnginePrivate::processAssertions(Assertions& as)
+{
   TimerStat::CodeTimer paTimer(d_smt.d_stats->d_processAssertionsTime);
   spendResource(ResourceManager::Resource::PreprocessStep);
   Assert(d_smt.d_fullyInited);
   Assert(d_smt.d_pendingPops == 0);
 
-  if (d_assertions.size() == 0) {
+  AssertionPipeline& ap = as.getAssertionPipeline();
+
+  if (ap.size() == 0)
+  {
     // nothing to do
     return;
   }
@@ -1161,24 +1098,24 @@ void SmtEnginePrivate::processAssertions() {
     // TODO(b/1255): Substitutions in incremental mode should be managed with a
     // proper data structure.
 
-    d_assertions.enableStoreSubstsInAsserts();
+    ap.enableStoreSubstsInAsserts();
   }
   else
   {
-    d_assertions.disableStoreSubstsInAsserts();
+    ap.disableStoreSubstsInAsserts();
   }
 
   // process the assertions
-  bool noConflict = d_processor.apply(d_assertions);
+  bool noConflict = d_processor.apply(as);
 
   //notify theory engine new preprocessed assertions
-  d_smt.d_theoryEngine->notifyPreprocessedAssertions( d_assertions.ref() );
+  d_smt.d_theoryEngine->notifyPreprocessedAssertions(ap.ref());
 
   // Push the formula to decision engine
   if (noConflict)
   {
     Chat() << "pushing to decision engine..." << endl;
-    d_smt.d_propEngine->addAssertionsToDecisionEngine(d_assertions);
+    d_smt.d_propEngine->addAssertionsToDecisionEngine(ap);
   }
 
   // end: INVARIANT to maintain: no reordering of assertions or
@@ -1187,91 +1124,30 @@ void SmtEnginePrivate::processAssertions() {
   // if incremental, compute which variables are assigned
   if (options::incrementalSolving())
   {
-    d_preprocessingPassContext->recordSymbolsInAssertions(d_assertions.ref());
+    d_preprocessingPassContext->recordSymbolsInAssertions(ap.ref());
   }
 
   // Push the formula to SAT
   {
     Chat() << "converting to CNF..." << endl;
     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime);
-    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
-      Chat() << "+ " << d_assertions[i] << std::endl;
-      d_smt.d_propEngine->assertFormula(d_assertions[i]);
-    }
-  }
-
-  d_assertionsProcessed = true;
-
-  d_assertions.clear();
-  getIteSkolemMap().clear();
-}
-
-void SmtEnginePrivate::addFormula(
-    TNode n, bool inUnsatCore, bool inInput, bool isAssumption, bool maybeHasFv)
-{
-  if (n == d_true) {
-    // nothing to do
-    return;
-  }
-
-  Trace("smt") << "SmtEnginePrivate::addFormula(" << n
-               << "), inUnsatCore = " << inUnsatCore
-               << ", inInput = " << inInput
-               << ", isAssumption = " << isAssumption << endl;
-
-  // Ensure that it does not contain free variables
-  if (maybeHasFv)
-  {
-    if (expr::hasFreeVar(n))
+    for (const Node& assertion : ap.ref())
     {
-      std::stringstream se;
-      se << "Cannot process assertion with free variable.";
-      if (language::isInputLangSygus(options::inputLanguage()))
-      {
-        // Common misuse of SyGuS is to use top-level assert instead of
-        // constraint when defining the synthesis conjecture.
-        se << " Perhaps you meant `constraint` instead of `assert`?";
-      }
-      throw ModalException(se.str().c_str());
+      Chat() << "+ " << assertion << std::endl;
+      d_smt.d_propEngine->assertFormula(assertion);
     }
   }
 
-  // Give it to proof manager
-  PROOF(
-    if( inInput ){
-      // n is an input assertion
-      if (inUnsatCore || options::unsatCores() || options::dumpUnsatCores() || options::checkUnsatCores() || options::fewerPreprocessingHoles()) {
-
-        ProofManager::currentPM()->addCoreAssertion(n.toExpr());
-      }
-    }else{
-      // n is the result of an unknown preprocessing step, add it to dependency map to null
-      ProofManager::currentPM()->addDependence(n, Node::null());
-    }
-  );
-
-  // Add the normalized formula to the queue
-  d_assertions.push_back(n, isAssumption);
-  //d_assertions.push_back(Rewriter::rewrite(n));
-}
+  d_assertionsProcessed = true;
 
-void SmtEngine::ensureBoolean(const Node& n)
-{
-  TypeNode type = n.getType(options::typeChecking());
-  TypeNode boolType = NodeManager::currentNM()->booleanType();
-  if(type != boolType) {
-    stringstream ss;
-    ss << "Expected " << boolType << "\n"
-       << "The assertion : " << n << "\n"
-       << "Its type      : " << type;
-    throw TypeCheckingException(n.toExpr(), ss.str());
-  }
+  // clear the current assertions
+  as.clearCurrent();
 }
 
 Result SmtEngine::checkSat(const Expr& assumption, bool inUnsatCore)
 {
   Dump("benchmark") << CheckSatCommand(assumption);
-  return checkSatisfiability(assumption, inUnsatCore, false);
+  return checkSatisfiability(Node::fromExpr(assumption), inUnsatCore, false);
 }
 
 Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
@@ -1284,36 +1160,46 @@ Result SmtEngine::checkSat(const vector<Expr>& assumptions, bool inUnsatCore)
   {
     Dump("benchmark") << CheckSatAssumingCommand(assumptions);
   }
-
-  return checkSatisfiability(assumptions, inUnsatCore, false);
+  std::vector<Node> assumps;
+  for (const Expr& e : assumptions)
+  {
+    assumps.push_back(Node::fromExpr(e));
+  }
+  return checkSatisfiability(assumps, inUnsatCore, false);
 }
 
-Result SmtEngine::checkEntailed(const Expr& expr, bool inUnsatCore)
+Result SmtEngine::checkEntailed(const Expr& node, bool inUnsatCore)
 {
-  Dump("benchmark") << QueryCommand(expr, inUnsatCore);
-  return checkSatisfiability(
-             expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr},
-             inUnsatCore,
-             true)
+  Dump("benchmark") << QueryCommand(node, inUnsatCore);
+  return checkSatisfiability(node.isNull()
+                                 ? std::vector<Node>()
+                                 : std::vector<Node>{Node::fromExpr(node)},
+                             inUnsatCore,
+                             true)
       .asEntailmentResult();
 }
 
-Result SmtEngine::checkEntailed(const vector<Expr>& exprs, bool inUnsatCore)
+Result SmtEngine::checkEntailed(const vector<Expr>& nodes, bool inUnsatCore)
 {
-  return checkSatisfiability(exprs, inUnsatCore, true).asEntailmentResult();
+  std::vector<Node> ns;
+  for (const Expr& e : nodes)
+  {
+    ns.push_back(Node::fromExpr(e));
+  }
+  return checkSatisfiability(ns, inUnsatCore, true).asEntailmentResult();
 }
 
-Result SmtEngine::checkSatisfiability(const Expr& expr,
+Result SmtEngine::checkSatisfiability(const Node& node,
                                       bool inUnsatCore,
                                       bool isEntailmentCheck)
 {
   return checkSatisfiability(
-      expr.isNull() ? std::vector<Expr>() : std::vector<Expr>{expr},
+      node.isNull() ? std::vector<Node>() : std::vector<Node>{node},
       inUnsatCore,
       isEntailmentCheck);
 }
 
-Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
+Result SmtEngine::checkSatisfiability(const vector<Node>& assumptions,
                                       bool inUnsatCore,
                                       bool isEntailmentCheck)
 {
@@ -1333,70 +1219,23 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
                            "(try --incremental)");
     }
 
-    // Note that a query has been made
+    // Note that a query has been made and we are in assert mode
     d_queryMade = true;
-    // reset global negation
-    d_globalNegation = false;
+    d_smtMode = SMT_MODE_ASSERT;
 
+    // push if there are assumptions
     bool didInternalPush = false;
-
-    setProblemExtended();
-
-    if (isEntailmentCheck)
-    {
-      size_t size = assumptions.size();
-      if (size > 1)
-      {
-        /* Assume: not (BIGAND assumptions)  */
-        d_assumptions.push_back(
-            d_exprManager->mkExpr(kind::AND, assumptions).notExpr());
-      }
-      else if (size == 1)
-      {
-        /* Assume: not expr  */
-        d_assumptions.push_back(assumptions[0].notExpr());
-      }
-    }
-    else
-    {
-      /* Assume: BIGAND assumptions  */
-      d_assumptions = assumptions;
-    }
-
-    if (!d_assumptions.empty())
+    if (!assumptions.empty())
     {
       internalPush();
       didInternalPush = true;
     }
 
-    Result r(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
-    for (Expr e : d_assumptions)
-    {
-      // Substitute out any abstract values in ex.
-      Node n = d_absValues->substituteAbstractValues(Node::fromExpr(e));
-      // Ensure expr is type-checked at this point.
-      ensureBoolean(n);
+    // then, initialize the assertions
+    d_asserts->initializeCheckSat(assumptions, inUnsatCore, isEntailmentCheck);
 
-      /* Add assumption  */
-      if (d_assertionList != NULL)
-      {
-        d_assertionList->push_back(n);
-      }
-      d_private->addFormula(n, inUnsatCore, true, true);
-    }
-
-    if (d_globalDefineFunRecLemmas != nullptr)
-    {
-      // Global definitions are asserted at check-sat-time because we have to
-      // make sure that they are always present (they are essentially level
-      // zero assertions)
-      for (const Node& lemma : *d_globalDefineFunRecLemmas)
-      {
-        d_private->addFormula(lemma, false, true, false, false);
-      }
-    }
-
-    r = check();
+    // make the check
+    Result r = check();
 
     if ((options::solveRealAsInt() || options::solveIntAsBV() > 0)
         && r.asSatisfiabilityResult().isSat() == Result::UNSAT)
@@ -1404,7 +1243,7 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
       r = Result(Result::SAT_UNKNOWN, Result::UNKNOWN_REASON);
     }
     // flipped if we did a global negation
-    if (d_globalNegation)
+    if (d_asserts->isGlobalNegated())
     {
       Trace("smt") << "SmtEngine::process global negate " << r << std::endl;
       if (r.asSatisfiabilityResult().isSat() == Result::UNSAT)
@@ -1492,7 +1331,7 @@ Result SmtEngine::checkSatisfiability(const vector<Expr>& assumptions,
   }
 }
 
-vector<Expr> SmtEngine::getUnsatAssumptions(void)
+std::vector<Node> SmtEngine::getUnsatAssumptions(void)
 {
   Trace("smt") << "SMT getUnsatAssumptions()" << endl;
   SmtScope smts(this);
@@ -1514,10 +1353,14 @@ vector<Expr> SmtEngine::getUnsatAssumptions(void)
     Dump("benchmark") << GetUnsatAssumptionsCommand();
   }
   UnsatCore core = getUnsatCoreInternal();
-  vector<Expr> res;
-  for (const Expr& e : d_assumptions)
+  std::vector<Node> res;
+  std::vector<Node>& assumps = d_asserts->getAssumptions();
+  for (const Node& e : assumps)
   {
-    if (find(core.begin(), core.end(), e) != core.end()) { res.push_back(e); }
+    if (std::find(core.begin(), core.end(), e.toExpr()) != core.end())
+    {
+      res.push_back(e);
+    }
   }
   return res;
 }
@@ -1537,12 +1380,7 @@ Result SmtEngine::assertFormula(const Node& formula, bool inUnsatCore)
   // Substitute out any abstract values in ex
   Node n = d_absValues->substituteAbstractValues(formula);
 
-  ensureBoolean(n);
-  if(d_assertionList != NULL) {
-    d_assertionList->push_back(n);
-  }
-  bool maybeHasFv = language::isInputLangSygus(options::inputLanguage());
-  d_private->addFormula(n, inUnsatCore, true, false, maybeHasFv);
+  d_asserts->assertFormula(n, inUnsatCore);
   return quickCheck().asEntailmentResult();
 }/* SmtEngine::assertFormula() */
 
@@ -1801,7 +1639,7 @@ Expr SmtEngine::simplify(const Expr& ex)
   }
 
   // Make sure all preprocessing is done
-  d_private->processAssertions();
+  d_private->processAssertions(*d_asserts);
   Node n = d_private->simplify(Node::fromExpr(e));
   n = postprocess(n, TypeNode::fromType(e.getType()));
   return n.toExpr();
@@ -2233,9 +2071,10 @@ void SmtEngine::checkUnsatCore() {
 }
 
 void SmtEngine::checkModel(bool hardFailure) {
+  context::CDList<Node>* al = d_asserts->getAssertionList();
   // --check-model implies --produce-assertions, which enables the
   // assertion list, so we should be ok.
-  Assert(d_assertionList != NULL)
+  Assert(al != nullptr)
       << "don't have an assertion list to check in SmtEngine::checkModel()";
 
   TimerStat::CodeTimer checkModelTimer(d_stats->d_checkModelTime);
@@ -2354,7 +2193,7 @@ void SmtEngine::checkModel(bool hardFailure) {
   }
 
   // Now go through all our user assertions checking if they're satisfied.
-  for (const Node& assertion : *d_assertionList)
+  for (const Node& assertion : *al)
   {
     Notice() << "SmtEngine::checkModel(): checking assertion " << assertion
              << endl;
@@ -2507,7 +2346,8 @@ void SmtEngine::checkSynthSolution()
 
   Trace("check-synth-sol") << "Retrieving assertions\n";
   // Build conjecture from original assertions
-  if (d_assertionList == NULL)
+  context::CDList<Node>* al = d_asserts->getAssertionList();
+  if (al == nullptr)
   {
     Trace("check-synth-sol") << "No assertions to check\n";
     return;
@@ -2516,7 +2356,7 @@ void SmtEngine::checkSynthSolution()
   std::vector<Node> auxAssertions;
   // expand definitions cache
   std::unordered_map<Node, Node, NodeHashFunction> cache;
-  for (const Node& assertion : *d_assertionList)
+  for (const Node& assertion : *al)
   {
     Notice() << "SmtEngine::checkSynthSolution(): checking assertion "
              << assertion << endl;
@@ -2857,9 +2697,10 @@ vector<Expr> SmtEngine::getAssertions() {
       "Cannot query the current assertion list when not in produce-assertions mode.";
     throw ModalException(msg);
   }
-  Assert(d_assertionList != NULL);
+  context::CDList<Node>* al = d_asserts->getAssertionList();
+  Assert(al != nullptr);
   std::vector<Expr> res;
-  for (const Node& n : *d_assertionList)
+  for (const Node& n : *al)
   {
     res.emplace_back(n.toExpr());
   }
@@ -2874,7 +2715,7 @@ void SmtEngine::push()
   doPendingPops();
   Trace("smt") << "SMT push()" << endl;
   d_private->notifyPush();
-  d_private->processAssertions();
+  d_private->processAssertions(*d_asserts);
   if(Dump.isOn("benchmark")) {
     Dump("benchmark") << PushCommand();
   }
@@ -2886,7 +2727,7 @@ void SmtEngine::push()
   // The problem isn't really "extended" yet, but this disallows
   // get-model after a push, simplifying our lives somewhat and
   // staying symmetric with pop.
-  setProblemExtended();
+  d_smtMode = SMT_MODE_ASSERT;
 
   d_userLevels.push_back(d_userContext->getLevel());
   internalPush();
@@ -2914,7 +2755,7 @@ void SmtEngine::pop() {
   // but also it would be weird to have a legally-executed (get-model)
   // that only returns a subset of the assignment (because the rest
   // is no longer in scope!).
-  setProblemExtended();
+  d_smtMode = SMT_MODE_ASSERT;
 
   AlwaysAssert(d_userContext->getLevel() > 0);
   AlwaysAssert(d_userLevels.back() < d_userContext->getLevel());
@@ -2924,6 +2765,7 @@ void SmtEngine::pop() {
   d_userLevels.pop_back();
 
   // Clear out assertion queues etc., in case anything is still in there
+  d_asserts->clearCurrent();
   d_private->notifyPop();
 
   Trace("userpushpop") << "SmtEngine: popped to level "
@@ -2937,7 +2779,7 @@ void SmtEngine::internalPush() {
   Trace("smt") << "SmtEngine::internalPush()" << endl;
   doPendingPops();
   if(options::incrementalSolving()) {
-    d_private->processAssertions();
+    d_private->processAssertions(*d_asserts);
     TimerStat::CodeTimer pushPopTimer(d_stats->d_pushPopTime);
     d_userContext->push();
     // the d_context push is done inside of the SAT solver