1 files changed, 8 insertions, 6 deletions
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 234814245..2c99bc7eb 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -135,6 +135,11 @@ class CVC4_PUBLIC SmtEngine {
   LogicInfo d_logic;
 
   /**
+   * Number of internal pops that have been deferred.
+   */
+  unsigned d_pendingPops;
+
+  /**
    * Whether or not this SmtEngine has been fully initialized (that is,
    * the ).  This post-construction initialization is automatically
    * triggered by the use of the SmtEngine; e.g. when setLogic() is
@@ -238,7 +243,9 @@ class CVC4_PUBLIC SmtEngine {
 
   void internalPush();
 
-  void internalPop();
+  void internalPop(bool immediate = false);
+
+  void doPendingPops();
 
   /**
    * Internally handle the setting of a logic.  This function should always
@@ -415,11 +422,6 @@ public:
   std::vector<Expr> getAssertions() throw(ModalException, AssertionException);
 
   /**
-   * Get the current context level.
-   */
-  size_t getStackLevel() const;
-
-  /**
    * Push a user-level context.
    */
   void push();