Lemmas on demand work, push-pop, some cleanup.

27 files changed, 731 insertions, 307 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index da41b1de4..0c692501f 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -37,6 +37,14 @@ CnfStream::CnfStream(SatInputInterface *satSolver) :
   d_satSolver(satSolver) {
 }
 
+void CnfStream::recordTranslation(TNode node) {
+  if (d_assertingLemma) {
+    d_lemmas.push_back(stripNot(node));
+  } else {
+    d_translationTrail.push_back(stripNot(node));
+  }
+}
+
 TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver) :
   CnfStream(satSolver) {
 }
@@ -67,42 +75,61 @@ void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral
   assertClause(node, clause);
 }
 
-bool CnfStream::isCached(TNode n) const {
-  return d_translationCache.find(n) != d_translationCache.end();
+bool CnfStream::isTranslated(TNode n) const {
+  TranslationCache::const_iterator find = d_translationCache.find(n);
+  return find != d_translationCache.end() && find->second.level >= 0;
 }
 
-SatLiteral CnfStream::lookupInCache(TNode node) const {
-  Assert(isCached(node), "Node is not in CNF translation cache");
-  return d_translationCache.find(node)->second;
-}
-
-void CnfStream::cacheTranslation(TNode node, SatLiteral lit) {
-  Debug("cnf") << "caching translation " << node << " to " << lit << endl;
-  // We always cash both the node and the negation at the same time
-  d_translationCache[node] = lit;
-  d_translationCache[node.notNode()] = ~lit;
+bool CnfStream::hasLiteral(TNode n) const {
+  TranslationCache::const_iterator find = d_translationCache.find(n);
+  return find != d_translationCache.end();
 }
 
 SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
-  SatLiteral lit = Minisat::mkLit(d_satSolver->newVar(theoryLiteral));
-  cacheTranslation(node, lit);
+  Debug("cnf") << "newLiteral(" << node << ")" << endl;
+
+  // Get the literal for this node
+  SatLiteral lit;
+  if (!hasLiteral(node)) {
+    // If no literal, well make one
+    lit = Minisat::mkLit(d_satSolver->newVar(theoryLiteral));
+    d_translationCache[node].literal = lit;
+    d_translationCache[node.notNode()].literal = ~lit;
+  } else {
+    // We already have a literal
+    lit = getLiteral(node);
+    d_satSolver->renewVar(lit);
+  }
+
+  // We will translate clauses, so remember the level
+  int level = d_satSolver->getLevel();
+  d_translationCache[node].level = level;
+  d_translationCache[node.notNode()].level = level;
+
+  // If it's a theory literal, store it for back queries
   if (theoryLiteral) {
     d_nodeCache[lit] = node;
     d_nodeCache[~lit] = node.notNode();
   }
+
+  // Here, you can have it
+  Debug("cnf") << "newLiteral(" << node << ") => " << lit << endl;
   return lit;
 }
 
-Node CnfStream::getNode(const SatLiteral& literal) {
+TNode CnfStream::getNode(const SatLiteral& literal) {
+  Debug("cnf") << "getNode(" << literal << ")" << endl;
   NodeCache::iterator find = d_nodeCache.find(literal);
   Assert(find != d_nodeCache.end());
+  Assert(d_translationCache.find(find->second) != d_translationCache.end());
+  Debug("cnf") << "getNode(" << literal << ") => " << find->second << endl;
   return find->second;
 }
 
 SatLiteral CnfStream::convertAtom(TNode node) {
   Debug("cnf") << "convertAtom(" << node << ")" << endl;
 
-  Assert(!isCached(node), "atom already mapped!");
+  Assert(!isTranslated(node), "atom already mapped!");
 
   bool theoryLiteral = node.getKind() != kind::VARIABLE;
   SatLiteral lit = newLiteral(node, theoryLiteral);
@@ -121,13 +148,13 @@ SatLiteral CnfStream::convertAtom(TNode node) {
 SatLiteral CnfStream::getLiteral(TNode node) {
   TranslationCache::iterator find = d_translationCache.find(node);
   Assert(find != d_translationCache.end(), "Literal not in the CNF Cache");
-  SatLiteral literal = find->second;
+  SatLiteral literal = find->second.literal;
   Debug("cnf") << "CnfStream::getLiteral(" << node << ") => " << literal << std::endl;
   return literal;
 }
 
 SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
-  Assert(!isCached(xorNode), "Atom already mapped!");
+  Assert(!isTranslated(xorNode), "Atom already mapped!");
   Assert(xorNode.getKind() == XOR, "Expecting an XOR expression!");
   Assert(xorNode.getNumChildren() == 2, "Expecting exactly 2 children!");
 
@@ -145,7 +172,7 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
 }
 
 SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
-  Assert(!isCached(orNode), "Atom already mapped!");
+  Assert(!isTranslated(orNode), "Atom already mapped!");
   Assert(orNode.getKind() == OR, "Expecting an OR expression!");
   Assert(orNode.getNumChildren() > 1, "Expecting more then 1 child!");
 
@@ -181,7 +208,7 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
 }
 
 SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
-  Assert(!isCached(andNode), "Atom already mapped!");
+  Assert(!isTranslated(andNode), "Atom already mapped!");
   Assert(andNode.getKind() == AND, "Expecting an AND expression!");
   Assert(andNode.getNumChildren() > 1, "Expecting more than 1 child!");
 
@@ -216,7 +243,7 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
 }
 
 SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
-  Assert(!isCached(impliesNode), "Atom already mapped!");
+  Assert(!isTranslated(impliesNode), "Atom already mapped!");
   Assert(impliesNode.getKind() == IMPLIES, "Expecting an IMPLIES expression!");
   Assert(impliesNode.getNumChildren() == 2, "Expecting exactly 2 children!");
 
@@ -241,7 +268,7 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
 
 
 SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
-  Assert(!isCached(iffNode), "Atom already mapped!");
+  Assert(!isTranslated(iffNode), "Atom already mapped!");
   Assert(iffNode.getKind() == IFF, "Expecting an IFF expression!");
   Assert(iffNode.getNumChildren() == 2, "Expecting exactly 2 children!");
 
@@ -273,15 +300,12 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
 
 
 SatLiteral TseitinCnfStream::handleNot(TNode notNode) {
-  Assert(!isCached(notNode), "Atom already mapped!");
+  Assert(!isTranslated(notNode), "Atom already mapped!");
   Assert(notNode.getKind() == NOT, "Expecting a NOT expression!");
   Assert(notNode.getNumChildren() == 1, "Expecting exactly 1 child!");
 
   SatLiteral notLit = ~toCNF(notNode[0]);
 
-  // Since we don't introduce new variables, we need to cache the translation
-  cacheTranslation(notNode, notLit);
-
   return notLit;
 }
 
@@ -328,8 +352,12 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
   Node negatedNode = node.notNode();
 
   // If the non-negated node has already been translated, get the translation
-  if(isCached(node)) {
-    nodeLit = lookupInCache(node);
+  if(isTranslated(node)) {
+    nodeLit = getLiteral(node);
+    // If we are asserting a lemma, we need to take the whole tree to level 0
+    if (d_assertingLemma) {
+      moveToBaseLevel(node);
+    }
   } else {
     // Handle each Boolean operator case
     switch(node.getKind()) {
@@ -395,6 +423,7 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, bool lemma, bool negated)
     for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
       Assert( disjunct != node.end() );
       clause[i] = toCNF(*disjunct, true);
+      recordTranslation(*disjunct);
     }
     Assert(disjunct == node.end());
     assertClause(node, clause);
@@ -411,6 +440,7 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool lemma, bool negated)
     for(int i = 0; i < nChildren; ++ disjunct, ++ i) {
       Assert( disjunct != node.end() );
       clause[i] = toCNF(*disjunct, false);
+      recordTranslation(*disjunct);
     }
     Assert(disjunct == node.end());
     assertClause(node, clause);
@@ -451,6 +481,8 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool lemma, bool negated)
     clause2[1] = ~q;
     assertClause(node, clause2);
   }
+  recordTranslation(node[0]);
+  recordTranslation(node[1]);
 }
 
 void TseitinCnfStream::convertAndAssertIff(TNode node, bool lemma, bool negated) {
@@ -481,6 +513,8 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool lemma, bool negated)
     clause2[1] = q;
     assertClause(node, clause2);
   }
+  recordTranslation(node[0]);
+  recordTranslation(node[1]);
 }
 
 void TseitinCnfStream::convertAndAssertImplies(TNode node, bool lemma, bool negated) {
@@ -493,6 +527,8 @@ void TseitinCnfStream::convertAndAssertImplies(TNode node, bool lemma, bool nega
     clause[0] = ~p;
     clause[1] = q;
     assertClause(node, clause);
+    recordTranslation(node[0]);
+    recordTranslation(node[1]);
   } else {// Construct the
     // !(p => q) is the same as (p && ~q)
     convertAndAssert(node[0], lemma, false);
@@ -523,6 +559,10 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool lemma, bool negated)
   clause4[0] = r;
   clause4[1] = p;
   assertClause(node, clause4);
+
+  recordTranslation(node[0]);
+  recordTranslation(node[1]);
+  recordTranslation(node[2]);
 }
 
 // At the top level we must ensure that all clauses that are asserted are
@@ -556,9 +596,79 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool lemma, bool negated) {
   default:
     // Atoms
     assertClause(node, toCNF(node, negated));
+    recordTranslation(node);
     break;
   }
 }
 
+void CnfStream::removeClausesAboveLevel(int level) {
+  while (d_translationTrail.size() > 0) {
+    TNode node = d_translationTrail.back();
+    Debug("cnf") << "Removing node " << node << " from CNF translation" << endl;
+    d_translationTrail.pop_back();
+    // Get the translation informations
+    TranslationInfo& infoPos = d_translationCache.find(node)->second;
+    // If already untranslated, we're done
+    if (infoPos.level == -1) continue;
+    // If the level of the node is less or equal to given we are done
+    if (infoPos.level <= level) break;
+    // Otherwise we have to undo the translation
+    undoTranslate(node, level);
+  }
+}
+
+void CnfStream::undoTranslate(TNode node, int level) {
+  // Get the translation information
+  TranslationInfo& infoPos = d_translationCache.find(node)->second;
+  // If already untranslated, we are done
+  if (infoPos.level == -1) return;
+  // If under the given level we're also done
+  if (infoPos.level <= level) return;
+  // Untranslate
+  infoPos.level = -1;
+  // Untranslate the negation node
+  // If not a not node, unregister it from sat and untranslate the negation
+  if (node.getKind() != kind::NOT) {
+    // Unregister the literal from SAT
+    SatLiteral lit = getLiteral(node);
+    d_satSolver->unregisterVar(lit);
+    // Untranslate the negation
+    TranslationInfo& infoNeg = d_translationCache.find(node.notNode())->second;
+    infoNeg.level = -1;
+  }
+  // undoTranslate the children
+  TNode::iterator child = node.begin();
+  TNode::iterator child_end = node.end();
+  while (child != child_end) {
+    undoTranslate(*child, level);
+    ++ child;
+  }
+}
+
+void CnfStream::moveToBaseLevel(TNode node) {
+  TNode posNode = stripNot(node);
+  TranslationInfo& infoPos = d_translationCache.find(posNode)->second;
+
+  Assert(infoPos.level >= 0);
+  if (infoPos.level == 0) return;
+
+  TNode negNode = node.notNode();
+  TranslationInfo& infoNeg = d_translationCache.find(negNode)->second;
+
+  infoPos.level = 0;
+  infoNeg.level = 0;
+
+  d_satSolver->renewVar(infoPos.literal, 0);
+
+  // undoTranslate the children
+  TNode::iterator child = posNode.begin();
+  TNode::iterator child_end = posNode.end();
+  while (child != child_end) {
+    moveToBaseLevel(*child);
+    ++ child;
+  }
+
+}
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 96d1925de..b35f3eafe 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -47,10 +47,18 @@ class CnfStream {
 public:
 
   /** Cache of what nodes have been registered to a literal. */
-  typedef __gnu_cxx::hash_map<SatLiteral, Node, SatSolver::SatLiteralHashFunction> NodeCache;
+  typedef __gnu_cxx::hash_map<SatLiteral, TNode, SatSolver::SatLiteralHashFunction> NodeCache;
+
+  /** Per node translation information */
+  struct TranslationInfo {
+    /** The level at which this node was translated (negative if not translated) */
+    int level;
+    /** The literal of this node */
+    SatLiteral literal;
+  };
 
   /** Cache of what literals have been registered to a node. */
-  typedef __gnu_cxx::hash_map<Node, SatLiteral, NodeHashFunction> TranslationCache;
+  typedef __gnu_cxx::hash_map<Node, TranslationInfo, NodeHashFunction> TranslationCache;
 
 private:
 
@@ -62,6 +70,33 @@ private:
 
 protected:
 
+  /** Top level nodes that we translated */
+  std::vector<TNode> d_translationTrail;
+
+  /** Nodes belonging to asserted lemmas */
+  std::vector<Node> d_lemmas;
+
+  /** Remove nots from the node */
+  TNode stripNot(TNode node) {
+    while (node.getKind() == kind::NOT) {
+      node = node[0];
+    }
+    return node;
+  }
+
+  /** Record this translation */
+  void recordTranslation(TNode node);
+
+  /**
+   * Moves the node and all of it's parents to level 0.
+   */
+  void moveToBaseLevel(TNode node);
+
+  /**
+   * Mark the node, and all parent at levels above level as untranslated.
+   */
+  void undoTranslate(TNode node, int level);
+
   /**
    * Are we asserting a lemma (true) or a permanent clause (false).
    * This is set at the begining of convertAndAssert so that it doesn't
@@ -105,22 +140,16 @@ protected:
    * @param node the node
    * @return true if the node has been cached
    */
-  bool isCached(TNode node) const;
-
-  /**
-   * Returns the cached literal corresponding to the given node.
-   * @param node the node to lookup
-   * @return returns the corresponding literal
-   */
-  SatLiteral lookupInCache(TNode node) const;
+  bool isTranslated(TNode node) const;
 
   /**
+   * Returns true if the node has an assigned literal (it might not be translated).
    * Caches the pair of the node and the literal corresponding to the
    * translation.
    * @param node the node
    * @param lit the literal
    */
-  void cacheTranslation(TNode node, SatLiteral lit);
+  bool hasLiteral(TNode node) const;
 
   /**
    * Acquires a new variable from the SAT solver to represent the node
@@ -172,7 +201,7 @@ public:
    * @param literal the literal from the sat solver
    * @return the actual node
    */
-  Node getNode(const SatLiteral& literal);
+  TNode getNode(const SatLiteral& literal);
 
   /**
    * Returns the literal that represents the given node in the SAT CNF
@@ -190,6 +219,11 @@ public:
     return d_nodeCache;
   }
 
+  /**
+   * Removes all the translation information of clauses that have the given associated assert level.
+   */
+  void removeClausesAboveLevel(int level);
+
 };/* class CnfStream */
 
 
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index e8efe3d03..3e1fbba17 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -50,9 +50,13 @@ static DoubleOption  opt_garbage_frac      (_cat, "gc-frac",     "The fraction o
 //=================================================================================================
 // Constructor/Destructor:
 
-Solver::Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context) :
+Solver::Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bool enable_incremental) :
     proxy(proxy)
   , context(context)
+  , assertionLevel(0)
+  , enable_incremental(enable_incremental)
+  , problem_extended(false)
+  , in_propagate(false)
     // Parameters (user settable):
     //
   , verbosity        (0)
@@ -92,7 +96,7 @@ Solver::Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context) :
   , simpDB_props       (0)
   , order_heap         (VarOrderLt(activity))
   , progress_estimate  (0)
-  , remove_satisfied   (true)
+  , remove_satisfied   (!enable_incremental)
 
     // Resource constraints:
     //
@@ -120,7 +124,7 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom)
     watches  .init(mkLit(v, false));
     watches  .init(mkLit(v, true ));
     assigns  .push(l_Undef);
-    vardata  .push(mkVarData(CRef_Undef, 0));
+    vardata  .push(mkVarData(CRef_Undef, 0, assertionLevel));
     //activity .push(0);
     activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0);
     seen     .push(0);
@@ -128,7 +132,14 @@ Var Solver::newVar(bool sign, bool dvar, bool theoryAtom)
     decision .push();
     trail    .capacity(v+1);
     setDecisionVar(v, dvar);
-	theory   .push(theoryAtom);
+    theory   .push(theoryAtom);
+
+    // We have extended the problem
+    if (in_propagate) {
+      problem_extended = true;
+      insertVarOrder(v);
+    }
+
     return v;
 }
 
@@ -148,9 +159,19 @@ CRef Solver::reason(Var x) const {
     // We're actually changing the state, so we hack it into non-const
     Solver* nonconst_this = const_cast<Solver*>(this);
 
-    // Construct the reason
-    CRef real_reason = nonconst_this->ca.alloc(explanation, true);
-    nonconst_this->vardata[x] = mkVarData(real_reason, level(x));
+    // Compute the assertion level for this clause
+    int explLevel = 0;
+    for (int i = 0; i < explanation.size(); ++ i) {
+      int varLevel = intro_level(var(explanation[i]));
+      if (varLevel > explLevel) {
+        explLevel = varLevel;
+      }
+    }
+
+    // Construct the reason (level 0)
+    // TODO compute the level
+    CRef real_reason = nonconst_this->ca.alloc(explLevel, explanation, true);
+    nonconst_this->vardata[x] = mkVarData(real_reason, level(x), intro_level(x));
     nonconst_this->learnts.push(real_reason);
     nonconst_this->attachClause(real_reason);
     return real_reason;
@@ -158,18 +179,61 @@ CRef Solver::reason(Var x) const {
 
 bool Solver::addClause_(vec<Lit>& ps, ClauseType type)
 {
-    assert(decisionLevel() == 0);
     if (!ok) return false;
 
+    // If a lemma propagates the literal, we mark this
+    bool propagate_first_literal = false;
+
     // Check if clause is satisfied and remove false/duplicate literals:
     sort(ps);
     Lit p; int i, j;
-    for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
-        if (value(ps[i]) == l_True || ps[i] == ~p)
+    if (type != CLAUSE_LEMMA) {
+        // Problem clause
+        for (i = j = 0, p = lit_Undef; i < ps.size(); i++)
+            if (value(ps[i]) == l_True || ps[i] == ~p)
+                return true;
+            else if (value(ps[i]) != l_False && ps[i] != p)
+                ps[j++] = p = ps[i];
+        ps.shrink(i - j);
+    } else {
+      // Lemma
+      vec<Lit> assigned_lits;
+        for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
+          if (ps[i] == ~p) {
+            // We don't add clauses that represent splits directly, they are decision literals
+            // so they will get decided upon and sent to the theory
             return true;
-        else if (value(ps[i]) != l_False && ps[i] != p)
-            ps[j++] = p = ps[i];
-    ps.shrink(i - j);
+          }
+          if (value(ps[i]) == l_Undef) {
+            // Anything not having a value gets added
+            if (ps[i] != p) {
+              ps[j++] = p = ps[i];
+            }
+          } else {
+            // If the literal has a value it gets added to the end of the clause
+            p = ps[i];
+            assigned_lits.push(p);
+            Debug("minisat::lemmas") << proxy->getNode(p) << " has value " << value(p) << endl;
+          }
+        }
+        Assert(j >= 1, "You are asserting a falsified lemma, produce a conflict instead!");
+        // If only one literal we could have unit propagation
+        if (j == 1) propagate_first_literal = true;
+        int max_level = -1;
+        int max_level_j = -1;
+        for (int assigned_i = 0; assigned_i < assigned_lits.size(); ++ assigned_i) {
+          ps[j++] = p = assigned_lits[assigned_i];
+          if (value(p) == l_True) propagate_first_literal = false;
+          else if (level(var(p)) > max_level) {
+            max_level = level(var(p));
+            max_level_j = j - 1;
+          }
+        }
+        if (value(ps[1]) != l_Undef) {
+          swap(ps[1], ps[max_level_j]);
+        }
+        ps.shrink(i - j);
+    }
 
     if (ps.size() == 0)
         return ok = false;
@@ -179,10 +243,19 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type)
         uncheckedEnqueue(ps[0]);
         return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef);
     }else{
-        CRef cr = ca.alloc(ps, false);
+        CRef cr = ca.alloc(type == CLAUSE_LEMMA ? 0 : assertionLevel, ps, false);
         clauses.push(cr);
-	if (type == CLAUSE_LEMMA) lemmas.push(cr);
-        attachClause(cr);
+	attachClause(cr);
+        if (propagate_first_literal) {
+          Debug("minisat::lemmas") << "Lemma propagating: " << (theory[var(ps[0])] ? proxy->getNode(ps[0]).toString() : "bool") << endl;
+          lemma_propagated_literals.push(ps[0]);
+          lemma_propagated_reasons.push(cr);
+          propagating_lemmas.push(cr);
+        }
+    }
+
+    if (in_propagate && type == CLAUSE_LEMMA) {
+      problem_extended = true;
     }
 
     return true;
@@ -191,6 +264,7 @@ bool Solver::addClause_(vec<Lit>& ps, ClauseType type)
 
 void Solver::attachClause(CRef cr) {
     const Clause& c = ca[cr];
+    CVC4::Debug("minisat") << "Solver::attachClause(" << c << ")" << std::endl;
     Assert(c.size() > 1);
     watches[~c[0]].push(Watcher(cr, c[1]));
     watches[~c[1]].push(Watcher(cr, c[0]));
@@ -250,15 +324,47 @@ void Solver::cancelUntil(int level) {
         qhead = trail_lim[level];
         trail.shrink(trail.size() - trail_lim[level]);
         trail_lim.shrink(trail_lim.size() - level);
-        // We can erase the lemmas now
-        for (int c = lemmas.size() - 1; c >= lemmas_lim[level]; c--) {
-          // TODO: can_erase[lemma[c]] = true;
+
+        // Propagate the lemma literals
+        int i, j;
+        for (i = j = propagating_lemmas_lim[level]; i < propagating_lemmas.size(); ++ i) {
+          Clause& lemma = ca[propagating_lemmas[i]];
+          bool propagating = value(var(lemma[0])) == l_Undef;;
+          for(int lit = 1; lit < lemma.size() && propagating; ++ lit)  {
+            if (value(var(lemma[lit])) != l_False) {
+              propagating = false;
+              break;
+            }
+          }
+          if (propagating) {
+            // Propagate
+            uncheckedEnqueue(lemma[0], propagating_lemmas[i]);
+            // Remember the lemma
+            propagating_lemmas[j++] = propagating_lemmas[i];
+          }
         }
-        lemmas.shrink(lemmas.size() - lemmas_lim[level]);
-        lemmas_lim.shrink(lemmas_lim.size() - level);
+        propagating_lemmas.shrink(i - j);
+        propagating_lemmas_lim.shrink(propagating_lemmas_lim.size() - level);
     }
 }
 
+void Solver::popTrail() {
+  // If we're not incremental, just pop until level 0
+  if (!enable_incremental) {
+    cancelUntil(0);
+  } else {
+    // Otherwise pop until the last recorded level 0 trail index
+    int target_size = trail_user_lim.last();
+    for (int c = trail.size()-1; c >= target_size; c--){
+      Var      x  = var(trail[c]);
+      assigns [x] = l_Undef;
+      if (phase_saving > 1 || (phase_saving == 1) && c > trail_lim.last())
+        polarity[x] = sign(trail[c]);
+      insertVarOrder(x); }
+    qhead = target_size;
+    trail.shrink(trail.size() - target_size);
+  }
+}
 
 //=================================================================================================
 // Major methods:
@@ -301,9 +407,10 @@ Lit Solver::pickBranchLit()
 |      * 'out_learnt[0]' is the asserting literal at level 'out_btlevel'.
 |      * If out_learnt.size() > 1 then 'out_learnt[1]' has the greatest decision level of the 
 |        rest of literals. There may be others from the same level though.
+|      * returns the maximal level of the resolved clauses
 |  
 |________________________________________________________________________________________________@*/
-void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
+int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
 {
     int pathC = 0;
     Lit p     = lit_Undef;
@@ -313,10 +420,16 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
     out_learnt.push();      // (leave room for the asserting literal)
     int index   = trail.size() - 1;
 
+    int max_level = 0; // Maximal level of the resolved clauses
+
     do{
         assert(confl != CRef_Undef); // (otherwise should be UIP)
         Clause& c = ca[confl];
 
+        if (c.level() > max_level) {
+          max_level = c.level();
+        }
+
         if (c.learnt())
             claBumpActivity(c);
 
@@ -344,7 +457,6 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
     out_learnt[0] = ~p;
 
     // Simplify conflict clause:
-    //
     int i, j;
     out_learnt.copyTo(analyze_toclear);
     if (ccmin_mode == 2){
@@ -352,9 +464,23 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
         for (i = 1; i < out_learnt.size(); i++)
             abstract_level |= abstractLevel(var(out_learnt[i])); // (maintain an abstraction of levels involved in conflict)
 
-        for (i = j = 1; i < out_learnt.size(); i++)
-            if (reason(var(out_learnt[i])) == CRef_Undef || !litRedundant(out_learnt[i], abstract_level))
+        for (i = j = 1; i < out_learnt.size(); i++) {
+            if (reason(var(out_learnt[i])) == CRef_Undef) {
                 out_learnt[j++] = out_learnt[i];
+            } else {
+              // Check if the literal is redundant
+              int red_level = litRedundant(out_learnt[i], abstract_level);
+              if (red_level < 0) {
+                // Literal is not redundant
+                out_learnt[j++] = out_learnt[i];
+              } else {
+                // Literal is redundant, mark the level of the redundancy derivation
+                if (max_level < red_level) {
+                  max_level = red_level;
+                }
+              }
+            }
+        }
         
     }else if (ccmin_mode == 1){
         for (i = j = 1; i < out_learnt.size(); i++){
@@ -395,18 +521,25 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
     }
 
     for (int j = 0; j < analyze_toclear.size(); j++) seen[var(analyze_toclear[j])] = 0;    // ('seen[]' is now cleared)
+
+    // Return the maximal resolution level
+    return max_level;
 }
 
 
 // Check if 'p' can be removed. 'abstract_levels' is used to abort early if the algorithm is
 // visiting literals at levels that cannot be removed later.
-bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
+int Solver::litRedundant(Lit p, uint32_t abstract_levels)
 {
     analyze_stack.clear(); analyze_stack.push(p);
     int top = analyze_toclear.size();
+    int max_level = 0;
     while (analyze_stack.size() > 0){
         assert(reason(var(analyze_stack.last())) != CRef_Undef);
         Clause& c = ca[reason(var(analyze_stack.last()))]; analyze_stack.pop();
+        if (c.level() > max_level) {
+            max_level = c.level();
+        }
 
         for (int i = 1; i < c.size(); i++){
             Lit p  = c[i];
@@ -419,13 +552,13 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
                     for (int j = top; j < analyze_toclear.size(); j++)
                         seen[var(analyze_toclear[j])] = 0;
                     analyze_toclear.shrink(analyze_toclear.size() - top);
-                    return false;
+                    return -1;
                 }
             }
         }
     }
 
-    return true;
+    return max_level;
 }
 
 
@@ -472,7 +605,7 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
 {
     assert(value(p) == l_Undef);
     assigns[var(p)] = lbool(!sign(p));
-    vardata[var(p)] = mkVarData(from, decisionLevel());
+    vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)));
     trail.push_(p);
     if (theory[var(p)] && from != CRef_Lazy) {
       // Enqueue to the theory
@@ -483,17 +616,22 @@ void Solver::uncheckedEnqueue(Lit p, CRef from)
 
 CRef Solver::propagate(TheoryCheckType type)
 {
+    in_propagate = true;
+
     CRef confl = CRef_Undef;
 
     // If this is the final check, no need for Boolean propagation and
     // theory propagation
     if (type == CHECK_WITHOUTH_PROPAGATION_FINAL) {
-      return theoryCheck(CVC4::theory::Theory::FULL_EFFORT);
+      confl = theoryCheck(CVC4::theory::Theory::FULL_EFFORT);
+      in_propagate = false;
+      return confl;
     }
 
     // The effort we will be using to theory check
     CVC4::theory::Theory::Effort effort = type == CHECK_WITHOUTH_PROPAGATION_QUICK ?
-    CVC4::theory::Theory::QUICK_CHECK : CVC4::theory::Theory::STANDARD;
+    		CVC4::theory::Theory::QUICK_CHECK : 
+    		CVC4::theory::Theory::STANDARD;
 
     // Keep running until we have checked everything, we
     // have no conflict and no new literals have been asserted
@@ -513,6 +651,8 @@ CRef Solver::propagate(TheoryCheckType type)
         }
     } while (new_assertions);
 
+    in_propagate = false;
+
     return confl;
 }
 
@@ -548,11 +688,15 @@ CRef Solver::theoryCheck(CVC4::theory::Theory::Effort effort)
   if(clause_size > 0) {
     // Find the max level of the conflict
     int max_level = 0;
+    int max_intro_level = 0;
     for (int i = 0; i < clause_size; ++i) {
-      int current_level = level(var(clause[i]));
-      Debug("minisat") << "Literal: " << clause[i] << " with reason " << reason(var(clause[i])) << " at level " << current_level << std::endl;
+      Var v = var(clause[i]);
+      int current_level = level(v);
+      int current_intro_level = intro_level(v);
+      Debug("minisat") << "Literal: " << clause[i] << " with reason " << reason(v) << " at level " << current_level << std::endl;
       Assert(value(clause[i]) != l_Undef, "Got an unassigned literal in conflict!");
       if (current_level > max_level) max_level = current_level;
+      if (current_intro_level > max_intro_level) max_intro_level = current_intro_level;
     }
     // If smaller than the decision level then pop back so we can analyse
     Debug("minisat") << "Max-level is " << max_level << " in decision level " << decisionLevel() << std::endl;
@@ -561,8 +705,8 @@ CRef Solver::theoryCheck(CVC4::theory::Theory::Effort effort)
       Debug("minisat") << "Max-level is " << max_level << " in decision level " << decisionLevel() << std::endl;
       cancelUntil(max_level);
     }
-    // Create the new clause and attach all the information
-    c = ca.alloc(clause, true);
+    // Create the new clause and attach all the information (level 0)
+    c = ca.alloc(max_intro_level, clause, true);
     learnts.push(c);
     attachClause(c);
   }
@@ -690,6 +834,18 @@ void Solver::removeSatisfied(vec<CRef>& cs)
     cs.shrink(i - j);
 }
 
+void Solver::removeClausesAboveLevel(vec<CRef>& cs, int level)
+{
+    int i, j;
+    for (i = j = 0; i < cs.size(); i++){
+        Clause& c = ca[cs[i]];
+        if (c.level() > level)
+            removeClause(cs[i]);
+        else
+            cs[j++] = cs[i];
+    }
+    cs.shrink(i - j);
+}
 
 void Solver::rebuildOrderHeap()
 {
@@ -756,20 +912,25 @@ lbool Solver::search(int nof_conflicts)
 
     TheoryCheckType check_type = CHECK_WITH_PROPAGATION_STANDARD;
     for (;;){
+        problem_extended = false;
         CRef confl = propagate(check_type);
         if (confl != CRef_Undef){
             // CONFLICT
             conflicts++; conflictC++;
             if (decisionLevel() == 0) return l_False;
 
+	    // Clear the propagated literals
+            lemma_propagated_literals.clear();
+            lemma_propagated_reasons.clear();
+			
             learnt_clause.clear();
-            analyze(confl, learnt_clause, backtrack_level);
+            int max_level = analyze(confl, learnt_clause, backtrack_level);
             cancelUntil(backtrack_level);
 
             if (learnt_clause.size() == 1){
                 uncheckedEnqueue(learnt_clause[0]);
             }else{
-                CRef cr = ca.alloc(learnt_clause, true);
+                CRef cr = ca.alloc(max_level, learnt_clause, true);
                 learnts.push(cr);
                 attachClause(cr);
                 claBumpActivity(ca[cr]);
@@ -791,11 +952,27 @@ lbool Solver::search(int nof_conflicts)
                            (int)max_learnts, nLearnts(), (double)learnts_literals/nLearnts(), progressEstimate()*100);
             }
 
-	    // We have a conflict so, we are going back to standard checks
+		    // We have a conflict so, we are going back to standard checks
             check_type = CHECK_WITH_PROPAGATION_STANDARD;
         }else{
             // NO CONFLICT
 
+            // If we have more assertions from lemmas, we continue
+            if (problem_extended) {
+
+              for (int i = 0, i_end = lemma_propagated_literals.size(); i < i_end; ++ i) {
+                Debug("minisat::lemmas") << "Lemma propagating: " << proxy->getNode(lemma_propagated_literals[i]) << endl;
+                uncheckedEnqueue(lemma_propagated_literals[i], lemma_propagated_reasons[i]);
+              }
+
+              lemma_propagated_literals.clear();
+              lemma_propagated_reasons.clear();
+
+              check_type = CHECK_WITH_PROPAGATION_STANDARD;
+
+              continue;
+            }
+
 	    // If this was a final check, we are satisfiable
             if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL)
               return l_True;
@@ -895,6 +1072,8 @@ static double luby(double y, int x){
 // NOTE: assumptions passed in member-variable 'assumptions'.
 lbool Solver::solve_()
 {
+    Debug("minisat") << "nvars = " << nVars() << endl;
+
     model.clear();
     conflict.clear();
     if (!ok) return l_False;
@@ -929,11 +1108,16 @@ lbool Solver::solve_()
     if (status == l_True){
         // Extend & copy model:
         model.growTo(nVars());
-        for (int i = 0; i < nVars(); i++) model[i] = value(i);
+        for (int i = 0; i < nVars(); i++) {
+          model[i] = value(i);
+          Debug("minisat") << i << " = " << model[i] << endl;
+        }
     }else if (status == l_False && conflict.size() == 0)
         ok = false;
 
-    cancelUntil(0);
+    // Cancel the trail downto previous push
+    popTrail();
+
     return status;
 }
 
@@ -1066,3 +1250,42 @@ void Solver::garbageCollect()
                ca.size()*ClauseAllocator::Unit_Size, to.size()*ClauseAllocator::Unit_Size);
     to.moveTo(ca);
 }
+
+void Solver::push()
+{
+  if (enable_incremental) {
+    ++ assertionLevel;
+    trail_user_lim.push(trail.size());
+  }
+}
+
+void Solver::pop()
+{
+  if (enable_incremental) {
+    -- assertionLevel;
+    // Remove all the clauses asserted (and implied) above the new base level
+    removeClausesAboveLevel(learnts, assertionLevel);
+    removeClausesAboveLevel(clauses, assertionLevel);
+
+    // Pop the user trail size
+    popTrail();
+    trail_user_lim.pop();
+
+    // Notify the cnf
+    proxy->removeClausesAboveLevel(assertionLevel);
+  }
+}
+
+void Solver::unregisterVar(Lit lit) {
+  Var v = var(lit);
+  vardata[v].intro_level = -1;
+  setDecisionVar(v, false);
+}
+
+void Solver::renewVar(Lit lit, int level) {
+  Var v = var(lit);
+  vardata[v].intro_level = level == -1 ? getAssertionLevel() : level;
+  setDecisionVar(v, true);
+}
+
+
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index bb8a81f16..7050f2d10 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -56,18 +56,44 @@ protected:
   /** The context from the SMT solver */
   CVC4::context::Context* context;
 
+  /** The current assertion level (user) */
+  int assertionLevel; 
+
+  /** Returns the current user assertion level */
+  int getAssertionLevel() const { return assertionLevel; }
+
+  /** Do we allow incremental solving */
+  bool enable_incremental;  
+
+  /** Did the problem get extended in the meantime (i.e. by adding a lemma) */
+  bool problem_extended;   
+
+  /** Literals propagated by lemmas */
+  vec<Lit> lemma_propagated_literals; 
+  /** Reasons of literals propagated by lemmas */
+  vec<CRef> lemma_propagated_reasons; 
+  /** Lemmas that propagated something, we need to recheck them after backtracking */
+  vec<CRef> propagating_lemmas;
+  vec<int> propagating_lemmas_lim;
+
+  /** Shrink 'cs' to contain only clauses below given level */
+  void removeClausesAboveLevel(vec<CRef>& cs, int level); 
+
+  /** True if we are inside the propagate method */
+  bool in_propagate;
+
 public:
 
     // Constructor/Destructor:
     //
-    Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context);
+    Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bool enableIncremental = false);
     CVC4_PUBLIC ~Solver();
 
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true, bool theoryAtom = false); // Add a new variable with parameters specifying variable mode.
 
-	// Types of clauses
+    // Types of clauses
     enum ClauseType {
       // Clauses defined by the problem
       CLAUSE_PROBLEM,
@@ -77,6 +103,13 @@ public:
       CLAUSE_CONFLICT
     };
 
+    // CVC4 context push/pop
+    void          push                     ();
+    void          pop                      ();
+
+    void unregisterVar(Lit lit); // Unregister the literal (set assertion level to -1)
+    void renewVar(Lit lit, int level = -1); // Register the literal (set assertion level to the given level, or current level if -1)
+
     bool    addClause (const vec<Lit>& ps, ClauseType type);                     // Add a clause to the solver. 
     bool    addEmptyClause(ClauseType type);                                     // Add the empty clause, making the solver contradictory.
     bool    addClause (Lit p, ClauseType type);                                  // Add a unit clause to the solver. 
@@ -174,8 +207,8 @@ protected:
 
     // Helper structures:
     //
-    struct VarData { CRef reason; int level; };
-    static inline VarData mkVarData(CRef cr, int l){ VarData d = {cr, l}; return d; }
+    struct VarData { CRef reason; int level; int intro_level; };
+    static inline VarData mkVarData(CRef cr, int l, int intro_l){ VarData d = {cr, l, intro_l}; return d; }
 
     struct Watcher {
         CRef cref;
@@ -213,6 +246,7 @@ protected:
     vec<char>           decision;         // Declares if a variable is eligible for selection in the decision heuristic.
     vec<Lit>            trail;            // Assignment stack; stores all assigments made in the order they were made.
     vec<int>            trail_lim;        // Separator indices for different decision levels in 'trail'.
+    vec<int>            trail_user_lim;   // Separator indices for different user push levels in 'trail'.
     vec<VarData>        vardata;          // Stores reason and level for each variable.
     int                 qhead;            // Head of queue (as index into the trail -- no more explicit propagation queue in MiniSat).
     int                 simpDB_assigns;   // Number of top-level assignments since last execution of 'simplify()'.
@@ -224,10 +258,8 @@ protected:
 
     ClauseAllocator     ca;
 
-	// CVC4 Stuff
+    // CVC4 Stuff
     vec<bool>           theory;           // Is the variable representing a theory atom
-    vec<CRef>           lemmas;           // List of lemmas we added (context dependent)
-    vec<int>            lemmas_lim;       // Separator indices for different decision levels in 'lemmas'.
 
     enum TheoryCheckType {
       // Quick check, but don't perform theory propagation
@@ -268,9 +300,10 @@ protected:
     bool     propagateTheory  ();                                                      // Perform Theory propagation. Return true if any literals were asserted.
     CRef     theoryCheck      (CVC4::theory::Theory::Effort effort);                   // Perform a theory satisfiability check. Returns possibly conflicting clause.
     void     cancelUntil      (int level);                                             // Backtrack until a certain level.
-    void     analyze          (CRef confl, vec<Lit>& out_learnt, int& out_btlevel);    // (bt = backtrack)
+    void     popTrail         ();                                                      // Backtrack the trail to the previous push position
+    int      analyze          (CRef confl, vec<Lit>& out_learnt, int& out_btlevel);    // (bt = backtrack)
     void     analyzeFinal     (Lit p, vec<Lit>& out_conflict);                         // COULD THIS BE IMPLEMENTED BY THE ORDINARIY "analyze" BY SOME REASONABLE GENERALIZATION?
-    bool     litRedundant     (Lit p, uint32_t abstract_levels);                       // (helper method for 'analyze()')
+    int      litRedundant     (Lit p, uint32_t abstract_levels);                       // (helper method for 'analyze()') - returns the maximal level of the clauses proving redundancy of p
     lbool    search           (int nof_conflicts);                                     // Search for a given number of conflicts.
     lbool    solve_           ();                                                      // Main solve method (assumptions given in 'assumptions').
     void     reduceDB         ();                                                      // Reduce the set of learnt clauses.
@@ -302,6 +335,7 @@ protected:
     CRef     reason           (Var x) const;
     bool     hasReason        (Var x) const; // Does the variable have a reason
     int      level            (Var x) const;
+    int      intro_level      (Var x) const; // Level at which this variable was introduced
     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
     bool     withinBudget     ()      const;
 
@@ -321,6 +355,7 @@ protected:
 };
 
 
+
 //=================================================================================================
 // Implementation of inline methods:
 
@@ -328,6 +363,8 @@ inline bool Solver::hasReason(Var x) const { return vardata[x].reason != CRef_Un
 
 inline int  Solver::level (Var x) const { return vardata[x].level; }
 
+inline int  Solver::intro_level(Var x) const { return vardata[x].intro_level; }
+
 inline void Solver::insertVarOrder(Var x) {
     if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
 
@@ -365,7 +402,7 @@ inline bool     Solver::addClause       (Lit p, ClauseType type)
 inline bool     Solver::addClause       (Lit p, Lit q, ClauseType type)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, type); }
 inline bool     Solver::addClause       (Lit p, Lit q, Lit r, ClauseType type)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, type); }
 inline bool     Solver::locked          (const Clause& c) const { return value(c[0]) == l_True && reason(var(c[0])) != CRef_Undef && ca.lea(reason(var(c[0]))) == &c; }
-inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); lemmas_lim.push(lemmas.size()); context->push(); }
+inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.size()); propagating_lemmas_lim.push(propagating_lemmas.size()); context->push(); }
 
 inline int      Solver::decisionLevel ()      const   { return trail_lim.size(); }
 inline uint32_t Solver::abstractLevel (Var x) const   { return 1 << (level(x) & 31); }
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index 12a0fdb6b..41e9be744 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -127,19 +127,21 @@ class Clause {
         unsigned learnt    : 1;
         unsigned has_extra : 1;
         unsigned reloced   : 1;
-        unsigned size      : 27; }                            header;
+        unsigned size      : 27;
+        unsigned level     : 32; }                            header;
     union { Lit lit; float act; uint32_t abs; CRef rel; } data[0];
 
     friend class ClauseAllocator;
 
     // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
     template<class V>
-    Clause(const V& ps, bool use_extra, bool learnt) {
+    Clause(const V& ps, bool use_extra, bool learnt, int level) {
         header.mark      = 0;
         header.learnt    = learnt;
         header.has_extra = use_extra;
         header.reloced   = 0;
         header.size      = ps.size();
+        header.level     = level;
 
         for (int i = 0; i < ps.size(); i++) 
             data[i].lit = ps[i];
@@ -160,6 +162,7 @@ public:
         data[header.size].abs = abstraction;  }
 
 
+    int          level       ()      const   { return header.level; }
     int          size        ()      const   { return header.size; }
     void         shrink      (int i)         { assert(i <= size()); if (header.has_extra) data[header.size-i] = data[header.size]; header.size -= i; }
     void         pop         ()              { shrink(1); }
@@ -208,14 +211,14 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
         RegionAllocator<uint32_t>::moveTo(to); }
 
     template<class Lits>
-    CRef alloc(const Lits& ps, bool learnt = false)
+    CRef alloc(int level, const Lits& ps, bool learnt = false)
     {
         assert(sizeof(Lit)      == sizeof(uint32_t));
         assert(sizeof(float)    == sizeof(uint32_t));
         bool use_extra = learnt | extra_clause_field;
 
         CRef cid = RegionAllocator<uint32_t>::alloc(clauseWord32Size(ps.size(), use_extra));
-        new (lea(cid)) Clause(ps, use_extra, learnt);
+        new (lea(cid)) Clause(ps, use_extra, learnt, level);
 
         return cid;
     }
@@ -239,7 +242,7 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
         
         if (c.reloced()) { cr = c.relocation(); return; }
         
-        cr = to.alloc(c, c.learnt());
+        cr = to.alloc(c.level(), c, c.learnt());
         c.relocate(cr);
         
         // Copy extra data-fields: 
@@ -368,6 +371,11 @@ class CMap
 |________________________________________________________________________________________________@*/
 inline Lit Clause::subsumes(const Clause& other) const
 {
+    // We restrict subsumtion to clauses at higher levels (if !enable_incremantal this should always be false)
+    if (level() > other.level()) {
+      return lit_Error;
+    }
+
     //if (other.size() < size() || (extra.abst & ~other.extra.abst) != 0)
     //if (other.size() < size() || (!learnt() && !other.learnt() && (extra.abst & ~other.extra.abst) != 0))
     assert(!header.learnt);   assert(!other.header.learnt);
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 32ac223d6..8bcd9fe76 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -44,15 +44,15 @@ static DoubleOption opt_simp_garbage_frac(_cat, "simp-gc-frac", "The fraction of
 // Constructor/Destructor:
 
 
-SimpSolver::SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context) :
-    Solver(proxy, context)
+SimpSolver::SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bool enableIncremental) :
+    Solver(proxy, context, enableIncremental)
   , grow               (opt_grow)
   , clause_lim         (opt_clause_lim)
   , subsumption_lim    (opt_subsumption_lim)
   , simp_garbage_frac  (opt_simp_garbage_frac)
   , use_asymm          (opt_use_asymm)
   , use_rcheck         (opt_use_rcheck)
-  , use_elim           (opt_use_elim)
+  , use_elim           (!enableIncremental)
   , merges             (0)
   , asymm_lits         (0)
   , eliminated_vars    (0)
@@ -65,7 +65,7 @@ SimpSolver::SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* con
 {
     vec<Lit> dummy(1,lit_Undef);
     ca.extra_clause_field = true; // NOTE: must happen before allocating the dummy clause below.
-    bwdsub_tmpunit        = ca.alloc(dummy);
+    bwdsub_tmpunit        = ca.alloc(0, dummy);
     remove_satisfied      = false;
 }
 
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 977da46e5..a7359e28e 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -41,7 +41,7 @@ class SimpSolver : public Solver {
  public:
     // Constructor/Destructor:
     //
-    SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context);
+    SimpSolver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bool enableIncremental = false);
     CVC4_PUBLIC ~SimpSolver();
 
     // Problem specification:
@@ -52,7 +52,7 @@ class SimpSolver : public Solver {
     bool    addClause (Lit p, ClauseType type);               // Add a unit clause to the solver.
     bool    addClause (Lit p, Lit q, ClauseType type);        // Add a binary clause to the solver.
     bool    addClause (Lit p, Lit q, Lit r, ClauseType type); // Add a ternary clause to the solver.
-    bool    addClause_(      vec<Lit>& ps, ClauseType type);
+    bool    addClause_(vec<Lit>& ps, ClauseType type);
     bool    substitute(Var v, Lit x);  // Replace all occurences of v with x (may cause a contradiction).
 
     // Variable mode:
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 5851f3990..45d941553 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -22,7 +22,6 @@
 
 #include "theory/theory_engine.h"
 #include "util/Assert.h"
-#include "util/decision_engine.h"
 #include "util/options.h"
 #include "util/output.h"
 #include "util/result.h"
@@ -57,11 +56,9 @@ public:
   }
 };
 
-PropEngine::PropEngine(DecisionEngine* de, TheoryEngine* te, 
+PropEngine::PropEngine(TheoryEngine* te,
                        Context* context, const Options& opts) :
   d_inCheckSat(false),
-  // d_options(opts),
-  d_decisionEngine(de),
   d_theoryEngine(te),
   d_context(context) {
   Debug("prop") << "Constructing the PropEngine" << endl;
@@ -85,9 +82,9 @@ void PropEngine::assertFormula(TNode node) {
 
 void PropEngine::assertLemma(TNode node) {
   Assert(d_inCheckSat, "Sat solver should be in solve()!");
-  Debug("prop") << "assertFormula(" << node << ")" << endl;
+  Debug("prop::lemma") << "assertLemma(" << node << ")" << endl;
   // Assert as removable
-  d_cnfStream->convertAndAssert(node, false, false);
+  d_cnfStream->convertAndAssert(node, true, false);
 }
 
 
@@ -101,8 +98,8 @@ void PropEngine::printSatisfyingAssignment(){
       end = transCache.end();
       i != end;
       ++i) {
-    pair<Node, SatLiteral> curr = *i;
-    SatLiteral l = curr.second;
+    pair<Node, CnfStream::TranslationInfo> curr = *i;
+    SatLiteral l = curr.second.literal;
     if(!sign(l)) {
       Node n = curr.first;
       SatLiteralValue value = d_satSolver->value(l);
@@ -150,11 +147,13 @@ Node PropEngine::getValue(TNode node) {
 
 void PropEngine::push() {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
+  d_satSolver->push();
   Debug("prop") << "push()" << endl;
 }
 
 void PropEngine::pop() {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
+  d_satSolver->pop();
   Debug("prop") << "pop()" << endl;
 }
 
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index ecef29ac2..b43c2d859 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -24,7 +24,6 @@
 #define __CVC4__PROP_ENGINE_H
 
 #include "expr/node.h"
-#include "util/decision_engine.h"
 #include "util/options.h"
 #include "util/result.h"
 
@@ -52,9 +51,6 @@ class PropEngine {
   /** The global options */
   //const Options d_options;
 
-  /** The decision engine we will be using */
-  DecisionEngine *d_decisionEngine;
-
   /** The theory engine we will be using */
   TheoryEngine *d_theoryEngine;
 
@@ -76,7 +72,7 @@ public:
   /**
    * Create a PropEngine with a particular decision and theory engine.
    */
-  PropEngine(DecisionEngine*, TheoryEngine*, context::Context*, const Options&);
+  PropEngine(TheoryEngine*, context::Context*, const Options&);
 
   /**
    * Destructor.
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index 2197cb23e..97c5d1419 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -94,5 +94,13 @@ void SatSolver::setCnfStream(CnfStream* cnfStream) {
   d_cnfStream = cnfStream;
 }
 
+void SatSolver::removeClausesAboveLevel(int level) {
+  d_cnfStream->removeClausesAboveLevel(level);
+}
+
+TNode SatSolver::getNode(SatLiteral lit) {
+  return d_cnfStream->getNode(lit);
+}
+
 }/* CVC4::prop namespace */
 }/* CVC4 namespace */
diff --git a/src/prop/sat.h b/src/prop/sat.h
index 550de5527..6e244d9d7 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -103,6 +103,12 @@ public:
   virtual void addClause(SatClause& clause, bool lemma) = 0;
   /** Create a new boolean variable in the solver. */
   virtual SatVariable newVar(bool theoryAtom = false) = 0;
+  /** Get the current decision level of the solver */
+  virtual int getLevel() const = 0;
+  /** Unregister the variable (of the literal) from solving */
+  virtual void unregisterVar(SatLiteral lit) = 0;
+  /** Register the variable (of the literal) for solving */
+  virtual void renewVar(SatLiteral lit, int level = -1) = 0;
 };
 
 /**
@@ -226,6 +232,21 @@ public:
   void setCnfStream(CnfStream* cnfStream);
 
   SatLiteralValue value(SatLiteral l);
+
+  int getLevel() const;
+
+  void push();
+
+  void pop();
+
+  void removeClausesAboveLevel(int level);
+
+  void unregisterVar(SatLiteral lit);
+
+  void renewVar(SatLiteral lit, int level = -1);
+
+  TNode getNode(SatLiteral lit);
+
 };/* class SatSolver */
 
 /* Functions that delegate to the concrete SAT solver. */
@@ -241,7 +262,7 @@ inline SatSolver::SatSolver(PropEngine* propEngine, TheoryEngine* theoryEngine,
   d_statistics()
 {
   // Create the solver
-  d_minisat = new Minisat::SimpSolver(this, d_context);
+  d_minisat = new Minisat::SimpSolver(this, d_context, options.incrementalSolving);
   // Setup the verbosity
   d_minisat->verbosity = (options.verbosity > 0) ? 1 : -1;
 
@@ -273,6 +294,26 @@ inline SatLiteralValue SatSolver::value(SatLiteral l) {
   return d_minisat->modelValue(l);
 }
 
+inline void SatSolver::push() {
+  d_minisat->push();
+}
+
+inline void SatSolver::pop() {
+  d_minisat->pop();
+}
+
+inline int SatSolver::getLevel() const {
+  return d_minisat->getAssertionLevel();
+}
+
+inline void SatSolver::unregisterVar(SatLiteral lit) {
+  d_minisat->unregisterVar(lit);
+}
+
+inline void SatSolver::renewVar(SatLiteral lit, int level) {
+  d_minisat->renewVar(lit, level);
+}
+
 #endif /* __CVC4_USE_MINISAT */
 
 inline size_t
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 151f7237b..bf74ab844 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -124,24 +124,24 @@ SmtEngine::SmtEngine(ExprManager* em, const Options& opts) throw() :
 
 void SmtEngine::init(const Options& opts) throw() {
   d_context = d_exprManager->getContext();
+  d_userContext = new Context();
+
   d_nodeManager = d_exprManager->getNodeManager();
 
   NodeManagerScope nms(d_nodeManager);
 
-  d_decisionEngine = new DecisionEngine;
   // We have mutual dependancy here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
   d_theoryEngine = new TheoryEngine(d_context, opts);
-  d_propEngine = new PropEngine(d_decisionEngine, d_theoryEngine, 
-                                d_context, opts);
+  d_propEngine = new PropEngine(d_theoryEngine, d_context, opts);
   d_theoryEngine->setPropEngine(d_propEngine);
 
-  d_definedFunctions = new(true) DefinedFunctionMap(d_context);
+  d_definedFunctions = new(true) DefinedFunctionMap(d_userContext);
 
   d_assertionList = NULL;
   d_interactive = opts.interactive;
   if(d_interactive) {
-    d_assertionList = new(true) AssertionList(d_context);
+    d_assertionList = new(true) AssertionList(d_userContext);
   }
 
   d_assignments = NULL;
@@ -156,7 +156,6 @@ void SmtEngine::init(const Options& opts) throw() {
 void SmtEngine::shutdown() {
   d_propEngine->shutdown();
   d_theoryEngine->shutdown();
-  d_decisionEngine->shutdown();
 }
 
 SmtEngine::~SmtEngine() {
@@ -174,9 +173,10 @@ SmtEngine::~SmtEngine() {
 
   d_definedFunctions->deleteSelf();
 
+  delete d_userContext;
+
   delete d_theoryEngine;
   delete d_propEngine;
-  delete d_decisionEngine;
 }
 
 void SmtEngine::setLogic(const std::string& s) throw(ModalException) {
@@ -457,8 +457,10 @@ Result SmtEngine::checkSat(const BoolExpr& e) {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT checkSat(" << e << ")" << endl;
   ensureBoolean(e);// ensure expr is type-checked at this point
+  internalPush();
   SmtEnginePrivate::addFormula(*this, e.getNode());
   Result r = check().asSatisfiabilityResult();
+  internalPop();
   d_status = r;
   d_haveAdditions = false;
   Debug("smt") << "SMT checkSat(" << e << ") ==> " << r << endl;
@@ -470,8 +472,10 @@ Result SmtEngine::query(const BoolExpr& e) {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT query(" << e << ")" << endl;
   ensureBoolean(e);// ensure expr is type-checked at this point
+  internalPush();
   SmtEnginePrivate::addFormula(*this, e.getNode().notNode());
   Result r = check().asValidityResult();
+  internalPop();
   d_status = r;
   d_haveAdditions = false;
   Debug("smt") << "SMT query(" << e << ") ==> " << r << endl;
@@ -629,21 +633,37 @@ vector<Expr> SmtEngine::getAssertions()
 void SmtEngine::push() {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT push()" << endl;
-  d_context->push();
-  d_propEngine->push();
+  d_userLevels.push_back(d_userContext->getLevel());
+  internalPush();
   Debug("userpushpop") << "SmtEngine: pushed to level "
-                       << d_context->getLevel() << endl;
+                       << d_userContext->getLevel() << endl;
 }
 
 void SmtEngine::pop() {
   NodeManagerScope nms(d_nodeManager);
   Debug("smt") << "SMT pop()" << endl;
-  d_propEngine->pop();
-  d_context->pop();
+  Assert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel());
+  while (d_userLevels.back() < d_userContext->getLevel()) {
+    internalPop();
+  }
+  d_userLevels.pop_back();
+
   Debug("userpushpop") << "SmtEngine: popped to level "
-                       << d_context->getLevel() << endl;
+                       << d_userContext->getLevel() << endl;
   // FIXME: should we reset d_status here?
   // SMT-LIBv2 spec seems to imply no, but it would make sense to..
 }
 
+void SmtEngine::internalPop() {
+  Debug("smt") << "internalPop()" << endl;
+  d_propEngine->pop();
+  d_userContext->pop();
+}
+
+void SmtEngine::internalPush() {
+  Debug("smt") << "internalPush()" << endl;
+  d_userContext->push();
+  d_propEngine->push();
+}
+
 }/* CVC4 namespace */
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 854399bd7..d8d9f4b54 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -48,7 +48,6 @@ typedef NodeTemplate<false> TNode;
 class NodeHashFunction;
 
 class TheoryEngine;
-class DecisionEngine;
 
 namespace context {
   class Context;
@@ -91,16 +90,18 @@ class CVC4_PUBLIC SmtEngine {
   /** The type of our internal assignment set */
   typedef context::CDSet<Node, NodeHashFunction> AssignmentSet;
 
-  /** Our Context */
+  /** Expr manager context */
   context::Context* d_context;
+
+  /** The context levels of user pushes */
+  std::vector<int> d_userLevels;
+  /** User level context */
+  context::Context* d_userContext;
+
   /** Our expression manager */
   ExprManager* d_exprManager;
   /** Out internal expression/node manager */
   NodeManager* d_nodeManager;
-  /** User-level options */
-  //const Options d_options;
-  /** The decision engine */
-  DecisionEngine* d_decisionEngine;
   /** The decision engine */
   TheoryEngine* d_theoryEngine;
   /** The propositional engine */
@@ -190,6 +191,10 @@ class CVC4_PUBLIC SmtEngine {
    */
   void ensureBoolean(const BoolExpr& e);
 
+  void internalPush();
+
+  void internalPop();
+
   friend class ::CVC4::smt::SmtEnginePrivate;
 
 public:
diff --git a/src/theory/arith/arith_utilities.h b/src/theory/arith/arith_utilities.h
index d50c48552..25aff4e75 100644
--- a/src/theory/arith/arith_utilities.h
+++ b/src/theory/arith/arith_utilities.h
@@ -237,10 +237,12 @@ inline int deltaCoeff(Kind k){
       case  kind::EQUAL:
         return  kind::DISTINCT;
       default:
+        Unreachable();
         return  kind::UNDEFINED_KIND;
       }
     }
   default:
+    Unreachable();
     return kind::UNDEFINED_KIND;
   }
 }
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 181632812..7b768d9af 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -103,21 +103,8 @@ ArithVar TheoryArith::findBasicRow(ArithVar variable){
 void TheoryArith::preRegisterTerm(TNode n) {
   Debug("arith_preregister") <<"begin arith::preRegisterTerm("<< n <<")"<< endl;
   Kind k = n.getKind();
-  if(k == EQUAL){
-    TNode left = n[0];
-    TNode right = n[1];
-
-    Node lt = NodeManager::currentNM()->mkNode(LT, left,right);
-    Node gt = NodeManager::currentNM()->mkNode(GT, left,right);
-    Node eagerSplit = NodeManager::currentNM()->mkNode(OR, n, lt, gt);
-
-    d_splits.push_back(eagerSplit);
 
-
-    d_out->augmentingLemma(eagerSplit);
-  }
-
-  bool isStrictlyVarList = n.getKind() == kind::MULT && VarList::isMember(n);
+  bool isStrictlyVarList = k == kind::MULT && VarList::isMember(n);
 
   if(isStrictlyVarList){
     d_out->setIncomplete();
@@ -307,15 +294,49 @@ bool TheoryArith::assertionCases(TNode assertion){
                             <<x_i<<" "<< simpKind <<" "<< c_i << ")" << std::endl;
   switch(simpKind){
   case LEQ:
+    if (d_partialModel.hasLowerBound(x_i) && d_partialModel.getLowerBound(x_i) == c_i) {
+      Node diseq = assertion[0].eqNode(assertion[1]).notNode();
+      if (d_diseq.find(diseq) != d_diseq.end()) {
+        NodeBuilder<3> conflict(kind::AND);
+        conflict << diseq << assertion << d_partialModel.getLowerConstraint(x_i);
+        d_out->conflict((TNode)conflict);
+        return true;
+      }
+    }
   case LT:
     return d_simplex.AssertUpper(x_i, c_i, assertion);
-  case GT:
   case GEQ:
+    if (d_partialModel.hasUpperBound(x_i) && d_partialModel.getUpperBound(x_i) == c_i) {
+      Node diseq = assertion[0].eqNode(assertion[1]).notNode();
+      if (d_diseq.find(diseq) != d_diseq.end()) {
+        NodeBuilder<3> conflict(kind::AND);
+        conflict << diseq << assertion << d_partialModel.getUpperConstraint(x_i);
+        d_out->conflict((TNode)conflict);
+        return true;
+      }
+    }
+  case GT:
     return d_simplex.AssertLower(x_i, c_i, assertion);
   case EQUAL:
     return d_simplex.AssertEquality(x_i, c_i, assertion);
   case DISTINCT:
-    d_diseq.push_back(assertion);
+    {
+      d_diseq.insert(assertion);
+      // Check if it conflicts with the the bounds
+      TNode eq = assertion[0];
+      Assert(eq.getKind() == kind::EQUAL);
+      TNode lhs = eq[0];
+      TNode rhs = eq[1];
+      Assert(rhs.getKind() == CONST_RATIONAL);
+      ArithVar lhsVar = determineLeftVariable(eq, kind::EQUAL);
+      DeltaRational rhsValue = determineRightConstant(eq, kind::EQUAL);
+      if (d_partialModel.hasLowerBound(lhsVar) && d_partialModel.hasUpperBound(lhsVar) &&
+          d_partialModel.getLowerBound(lhsVar) == rhsValue && d_partialModel.getUpperBound(lhsVar) == rhsValue) {
+        NodeBuilder<3> conflict(kind::AND);
+        conflict << assertion << d_partialModel.getLowerConstraint(lhsVar) << d_partialModel.getUpperConstraint(lhsVar);
+        d_out->conflict((TNode)conflict);
+      }
+    }
     return false;
   default:
     Unreachable();
@@ -323,7 +344,7 @@ bool TheoryArith::assertionCases(TNode assertion){
   }
 }
 
-void TheoryArith::check(Effort level){
+void TheoryArith::check(Effort effortLevel){
   Debug("arith") << "TheoryArith::check begun" << std::endl;
 
   while(!done()){
@@ -339,8 +360,25 @@ void TheoryArith::check(Effort level){
     }
   }
 
-  //TODO This must be done everytime for the time being
-  if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
+  if(Debug.isOn("arith::print_assertions") && fullEffort(effortLevel)) {
+    Debug("arith::print_assertions") << "Assertions:" << endl;
+    for (ArithVar i = 0; i < d_variables.size(); ++ i) {
+      if (d_partialModel.hasLowerBound(i)) {
+        Node lConstr = d_partialModel.getLowerConstraint(i);
+        Debug("arith::print_assertions") << lConstr.toString() << endl;
+      }
+
+      if (d_partialModel.hasUpperBound(i)) {
+        Node uConstr = d_partialModel.getUpperConstraint(i);
+        Debug("arith::print_assertions") << uConstr.toString() << endl;
+      }
+    }
+    context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin();
+    context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end();
+    for(; it != it_end; ++ it) {
+      Debug("arith::print_assertions") << *it << endl;
+    }
+  }
 
   Node possibleConflict = d_simplex.updateInconsistentVars();
   if(possibleConflict != Node::null()){
@@ -355,10 +393,36 @@ void TheoryArith::check(Effort level){
     Debug("arith_conflict") <<"Found a conflict "<< possibleConflict << endl;
   }else{
     d_partialModel.commitAssignmentChanges();
+
+    if (fullEffort(effortLevel)) {
+      context::CDSet<Node, NodeHashFunction>::iterator it = d_diseq.begin();
+      context::CDSet<Node, NodeHashFunction>::iterator it_end = d_diseq.end();
+      for(; it != it_end; ++ it) {
+        TNode eq = (*it)[0];
+        Assert(eq.getKind() == kind::EQUAL);
+        TNode lhs = eq[0];
+        TNode rhs = eq[1];
+        Assert(rhs.getKind() == CONST_RATIONAL);
+        ArithVar lhsVar = determineLeftVariable(eq, kind::EQUAL);
+        if(d_tableau.isEjected(lhsVar)){
+          d_simplex.reinjectVariable(lhsVar);
+        }
+        DeltaRational lhsValue = d_partialModel.getAssignment(lhsVar);
+        DeltaRational rhsValue = determineRightConstant(eq, kind::EQUAL);
+        if (lhsValue == rhsValue) {
+          Debug("arith_lemma") << "Splitting on " << eq << endl;
+          Debug("arith_lemma") << "LHS value = " << lhsValue << endl;
+          Debug("arith_lemma") << "RHS value = " << rhsValue << endl;
+          Node ltNode = NodeBuilder<2>(kind::LT) << lhs << rhs;
+          Node gtNode = NodeBuilder<2>(kind::GT) << lhs << rhs;
+          Node lemma = NodeBuilder<3>(OR) << eq << ltNode << gtNode;
+          d_out->lemma(lemma);
+        }
+      }
+    }
   }
   if(Debug.isOn("paranoid:check_tableau")){ d_simplex.checkTableau(); }
 
-
   Debug("arith") << "TheoryArith::check end" << std::endl;
 
   if(Debug.isOn("arith::print_model")) {
@@ -372,17 +436,6 @@ void TheoryArith::check(Effort level){
       Debug("arith::print_model") << endl;
     }
   }
-  if(Debug.isOn("arith::print_assertions")) {
-    Debug("arith::print_assertions") << "Assertions:" << endl;
-    for (ArithVar i = 0; i < d_variables.size(); ++ i) {
-      Node lConstr = d_partialModel.getLowerConstraint(i);
-      Debug("arith::print_assertions") << lConstr.toString() << endl;
-
-      Node uConstr = d_partialModel.getUpperConstraint(i);
-      Debug("arith::print_assertions") << uConstr.toString() << endl;
-
-    }
-  }
 }
 
 void TheoryArith::explain(TNode n, Effort e) {
diff --git a/src/theory/arith/theory_arith.h b/src/theory/arith/theory_arith.h
index af52da444..5c65b993d 100644
--- a/src/theory/arith/theory_arith.h
+++ b/src/theory/arith/theory_arith.h
@@ -24,6 +24,7 @@
 #include "theory/theory.h"
 #include "context/context.h"
 #include "context/cdlist.h"
+#include "context/cdset.h"
 #include "expr/node.h"
 
 #include "theory/arith/arith_utilities.h"
@@ -86,7 +87,7 @@ private:
   /**
    * List of all of the inequalities asserted in the current context.
    */
-  context::CDList<Node> d_diseq;
+  context::CDSet<Node, NodeHashFunction> d_diseq;
 
   /**
    * The tableau for all of the constraints seen thus far in the system.
diff --git a/src/theory/output_channel.h b/src/theory/output_channel.h
index 1c48c0160..269f28732 100644
--- a/src/theory/output_channel.h
+++ b/src/theory/output_channel.h
@@ -100,17 +100,6 @@ public:
     throw(Interrupted, AssertionException) = 0;
 
   /**
-   * Tell the core to add the following valid lemma as if it were a
-   * user assertion.  This should NOT be called during solving, only
-   * preprocessing.
-   *
-   * @param n - a theory lemma valid to be asserted
-   * @param safe - whether it is safe to be interrupted
-   */
-  virtual void augmentingLemma(TNode n, bool safe = false)
-    throw(Interrupted, AssertionException) = 0;
-
-  /**
    * Provide an explanation in response to an explanation request.
    *
    * @param n - an explanation
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index b2f047824..7958d977e 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -106,11 +106,7 @@ class TheoryEngine {
       ++(d_engine->d_statistics.d_statLemma);
       d_engine->newLemma(node);
     }
-    void augmentingLemma(TNode node, bool)
-      throw(theory::Interrupted, AssertionException) {
-      ++(d_engine->d_statistics.d_statAugLemma);
-      d_engine->newAugmentingLemma(node);
-    }
+
     void explanation(TNode explanationNode, bool)
       throw(theory::Interrupted, AssertionException) {
       d_explanationNode = explanationNode;
@@ -322,12 +318,7 @@ public:
   }
 
   inline void newLemma(TNode node) {
-    d_propEngine->assertLemma(node);
-  }
-
-  inline void newAugmentingLemma(TNode node) {
-    Node preprocessed = preprocess(node);
-    d_propEngine->assertFormula(preprocessed);
+    d_propEngine->assertLemma(preprocess(node));
   }
 
   /**
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index af3457550..837837cd6 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -12,8 +12,6 @@ libutil_la_SOURCES = \
 	Makefile.in \
 	congruence_closure.h \
 	debug.h \
-	decision_engine.cpp \
-	decision_engine.h \
 	exception.h \
 	hash.h \
 	bool.h \
@@ -29,7 +27,6 @@ libutil_la_SOURCES = \
 	rational.h \
 	integer.h \
 	bitvector.h \
-	bitvector.cpp \
 	gmp_util.h \
 	sexpr.h \
 	stats.h \
@@ -44,12 +41,10 @@ BUILT_SOURCES = \
 
 if CVC4_CLN_IMP
 libutil_la_SOURCES += \
-	integer_cln_imp.cpp \
 	rational_cln_imp.cpp
 endif
 if CVC4_GMP_IMP
 libutil_la_SOURCES += \
-	integer_gmp_imp.cpp \
 	rational_gmp_imp.cpp
 endif
 
@@ -57,11 +52,9 @@ EXTRA_DIST = \
 	rational_cln_imp.h \
 	integer_cln_imp.h \
 	rational_cln_imp.cpp \
-	integer_cln_imp.cpp \
 	rational_gmp_imp.h \
 	integer_gmp_imp.h \
 	rational_gmp_imp.cpp \
-	integer_gmp_imp.cpp \
 	rational.h.in \
 	integer.h.in \
 	tls.h.in
diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp
deleted file mode 100644
index 8ea95e1c9..000000000
--- a/src/util/bitvector.cpp
+++ /dev/null
@@ -1,32 +0,0 @@
-/*********************                                                        */
-/*! \file bitvector.cpp
- ** \verbatim
- ** Original author: dejan
- ** Major contributors: mdeters
- ** Minor contributors (to current version): taking
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief [[ Add one-line brief description here ]]
- **
- ** [[ Add lengthier description here ]]
- ** \todo document this file
- **/
-
-#include "bitvector.h"
-
-namespace CVC4 {
-
-std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
-  return os << bv.toString();
-}
-
-std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
-  return os << "[" << bv.high << ":" << bv.low << "]";
-}
-
-}/* CVC4 namespace */
diff --git a/src/util/bitvector.h b/src/util/bitvector.h
index edf4e987d..51239cbbb 100644
--- a/src/util/bitvector.h
+++ b/src/util/bitvector.h
@@ -245,8 +245,13 @@ struct UnsignedHashStrategy {
   }
 };
 
-std::ostream& operator <<(std::ostream& os, const BitVector& bv);
-std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv);
+inline std::ostream& operator <<(std::ostream& os, const BitVector& bv) {
+  return os << bv.toString();
+}
+
+inline std::ostream& operator <<(std::ostream& os, const BitVectorExtract& bv) {
+  return os << "[" << bv.high << ":" << bv.low << "]";
+}
 
 }/* CVC4 namespace */
 
diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp
deleted file mode 100644
index 692520257..000000000
--- a/src/util/integer_cln_imp.cpp
+++ /dev/null
@@ -1,37 +0,0 @@
-/*********************                                                        */
-/*! \file integer_cln_imp.cpp
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief A multiprecision rational constant.
- **
- ** A multiprecision rational constant.
- ** This stores the rational as a pair of multiprecision integers,
- ** one for the numerator and one for the denominator.
- ** The number is always stored so that the gcd of the numerator and denominator
- ** is 1.  (This is referred to as referred to as canonical form in GMP's
- ** literature.) A consquence is that that the numerator and denominator may be
- ** different than the values used to construct the Rational.
- **/
-
-#include "cvc4autoconfig.h"
-#include "util/integer.h"
-
-#ifndef CVC4_CLN_IMP
-#  error "This source should only ever be built if CVC4_CLN_IMP is on !"
-#endif /* CVC4_CLN_IMP */
-
-using namespace CVC4;
-
-std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) {
-  return os << n.toString();
-}
-
diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h
index ee256867a..21f6c7581 100644
--- a/src/util/integer_cln_imp.h
+++ b/src/util/integer_cln_imp.h
@@ -228,7 +228,9 @@ struct IntegerHashStrategy {
   }
 };/* struct IntegerHashStrategy */
 
-std::ostream& operator<<(std::ostream& os, const Integer& n);
+inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
+  return os << n.toString();
+}
 
 }/* CVC4 namespace */
 
diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp
deleted file mode 100644
index 1c2bd7ccd..000000000
--- a/src/util/integer_gmp_imp.cpp
+++ /dev/null
@@ -1,37 +0,0 @@
-/*********************                                                        */
-/*! \file integer_gmp_imp.cpp
- ** \verbatim
- ** Original author: taking
- ** Major contributors: mdeters
- ** Minor contributors (to current version): none
- ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010  The Analysis of Computer Systems Group (ACSys)
- ** Courant Institute of Mathematical Sciences
- ** New York University
- ** See the file COPYING in the top-level source directory for licensing
- ** information.\endverbatim
- **
- ** \brief A multiprecision rational constant.
- **
- ** A multiprecision rational constant.
- ** This stores the rational as a pair of multiprecision integers,
- ** one for the numerator and one for the denominator.
- ** The number is always stored so that the gcd of the numerator and denominator
- ** is 1.  (This is referred to as referred to as canonical form in GMP's
- ** literature.) A consquence is that that the numerator and denominator may be
- ** different than the values used to construct the Rational.
- **/
-
-#include "cvc4autoconfig.h"
-#include "util/integer.h"
-
-#ifndef CVC4_GMP_IMP
-#  error "This source should only ever be built if CVC4_GMP_IMP is on !"
-#endif /* CVC4_GMP_IMP */
-
-using namespace CVC4;
-
-std::ostream& CVC4::operator<<(std::ostream& os, const Integer& n) {
-  return os << n.toString();
-}
-
diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h
index 44f460559..72a653545 100644
--- a/src/util/integer_gmp_imp.h
+++ b/src/util/integer_gmp_imp.h
@@ -164,7 +164,9 @@ struct IntegerHashStrategy {
   }
 };/* struct IntegerHashStrategy */
 
-std::ostream& operator<<(std::ostream& os, const Integer& n);
+inline std::ostream& operator<<(std::ostream& os, const Integer& n) {
+  return os << n.toString();
+}
 
 }/* CVC4 namespace */
 
diff --git a/src/util/options.cpp b/src/util/options.cpp
index dbfed887d..8f26d9376 100644
--- a/src/util/options.cpp
+++ b/src/util/options.cpp
@@ -66,7 +66,8 @@ static const string optionsDescription = "\
    --no-interactive       do not run interactively\n\
    --produce-models       support the get-value command\n\
    --produce-assignments  support the get-assignment command\n\
-   --lazy-definition-expansion expand define-fun lazily\n";
+   --lazy-definition-expansion expand define-fun lazily\n\
+   --incremental          enable incremental solving\n";
 
 static const string languageDescription = "\
 Languages currently supported as arguments to the -L / --lang option:\n\
@@ -119,6 +120,7 @@ enum OptionValue {
   NO_TYPE_CHECKING,
   LAZY_TYPE_CHECKING,
   EAGER_TYPE_CHECKING,
+  INCREMENTAL
 };/* enum OptionValue */
 
 /**
@@ -174,6 +176,7 @@ static struct option cmdlineOptions[] = {
   { "no-type-checking", no_argument, NULL, NO_TYPE_CHECKING},
   { "lazy-type-checking", no_argument, NULL, LAZY_TYPE_CHECKING},
   { "eager-type-checking", no_argument, NULL, EAGER_TYPE_CHECKING},
+  { "incremental", no_argument, NULL, INCREMENTAL},
   { NULL         , no_argument      , NULL, '\0'        }
 };/* if you add things to the above, please remember to update usage.h! */
 
@@ -367,6 +370,10 @@ throw(OptionException) {
       earlyTypeChecking = true;
       break;
 
+    case INCREMENTAL:
+      incrementalSolving = true;
+      break;
+
     case SHOW_CONFIG:
       fputs(Configuration::about().c_str(), stdout);
       printf("\n");
diff --git a/src/util/options.h b/src/util/options.h
index 60c8f2a1a..1eca0d499 100644
--- a/src/util/options.h
+++ b/src/util/options.h
@@ -126,6 +126,9 @@ struct CVC4_PUBLIC Options {
   /** Whether we do typechecking at Expr creation time. */
   bool earlyTypeChecking;
 
+  /** Whether incemental solving (push/pop) */
+  bool incrementalSolving;
+
   Options() :
     binary_name(),
     statistics(false),
@@ -147,7 +150,8 @@ struct CVC4_PUBLIC Options {
     produceModels(false),
     produceAssignments(false),
     typeChecking(DO_SEMANTIC_CHECKS_BY_DEFAULT),
-    earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT) {
+    earlyTypeChecking(USE_EARLY_TYPE_CHECKING_BY_DEFAULT),
+    incrementalSolving(false) {
   }
 
   /**