new implementation of lemmas on demand

comparison <http://goedel.cims.nyu.edu/regress-results/compare_jobs.php?job_id=2673&&p=5&reference_id=2637>

14 files changed, 507 insertions, 512 deletions

diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index 36df53ca3..629e44e3e 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -46,9 +46,7 @@ CnfStream::CnfStream(SatInputInterface *satSolver, theory::Registrar registrar)
 }
 
 void CnfStream::recordTranslation(TNode node) {
-  if (d_assertingLemma) {
-    d_lemmas.push_back(stripNot(node));
-  } else {
+  if (!d_removable) {
     d_translationTrail.push_back(stripNot(node));
   }
 }
@@ -59,7 +57,7 @@ TseitinCnfStream::TseitinCnfStream(SatInputInterface* satSolver, theory::Registr
 
 void CnfStream::assertClause(TNode node, SatClause& c) {
   Debug("cnf") << "Inserting into stream " << c << endl;
-  d_satSolver->addClause(c, d_assertingLemma);
+  d_satSolver->addClause(c, d_removable);
 }
 
 void CnfStream::assertClause(TNode node, SatLiteral a) {
@@ -123,9 +121,9 @@ SatLiteral CnfStream::newLiteral(TNode node, bool theoryLiteral) {
 
   // If a theory literal, we pre-register it
   if (theoryLiteral) {
-    bool backup = d_assertingLemma;
+    bool backup = d_removable;
     d_registrar.preRegister(node);
-    d_assertingLemma = backup;
+    d_removable = backup;
   }
 
   // Here, you can have it
@@ -372,10 +370,6 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
   // If the non-negated node has already been translated, get the translation
   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()) {
@@ -425,13 +419,13 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
   else return ~nodeLit;
 }
 
-void TseitinCnfStream::convertAndAssertAnd(TNode node, bool lemma, bool negated) {
+void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated) {
   Assert(node.getKind() == AND);
   if (!negated) {
     // If the node is a conjunction, we handle each conjunct separately
     for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
         conjunct != node_end; ++conjunct ) {
-      convertAndAssert(*conjunct, lemma, false);
+      convertAndAssert(*conjunct, false);
     }
   } else {
     // If the node is a disjunction, we construct a clause and assert it
@@ -448,7 +442,7 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, bool lemma, bool negated)
   }
 }
 
-void TseitinCnfStream::convertAndAssertOr(TNode node, bool lemma, bool negated) {
+void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated) {
   Assert(node.getKind() == OR);
   if (!negated) {
     // If the node is a disjunction, we construct a clause and assert it
@@ -466,12 +460,12 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool lemma, bool negated)
     // If the node is a conjunction, we handle each conjunct separately
     for(TNode::const_iterator conjunct = node.begin(), node_end = node.end();
         conjunct != node_end; ++conjunct ) {
-      convertAndAssert(*conjunct, lemma, true);
+      convertAndAssert(*conjunct, true);
     }
   }
 }
 
-void TseitinCnfStream::convertAndAssertXor(TNode node, bool lemma, bool negated) {
+void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) {
   if (!negated) {
     // p XOR q
     SatLiteral p = toCNF(node[0], false);
@@ -503,7 +497,7 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool lemma, bool negated)
   recordTranslation(node[1]);
 }
 
-void TseitinCnfStream::convertAndAssertIff(TNode node, bool lemma, bool negated) {
+void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) {
   if (!negated) {
     // p <=> q
     SatLiteral p = toCNF(node[0], false);
@@ -535,7 +529,7 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool lemma, bool negated)
   recordTranslation(node[1]);
 }
 
-void TseitinCnfStream::convertAndAssertImplies(TNode node, bool lemma, bool negated) {
+void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) {
   if (!negated) {
     // p => q
     SatLiteral p = toCNF(node[0], false);
@@ -549,12 +543,12 @@ void TseitinCnfStream::convertAndAssertImplies(TNode node, bool lemma, bool nega
     recordTranslation(node[1]);
   } else {// Construct the
     // !(p => q) is the same as (p && ~q)
-    convertAndAssert(node[0], lemma, false);
-    convertAndAssert(node[1], lemma, true);
+    convertAndAssert(node[0], false);
+    convertAndAssert(node[1], true);
   }
 }
 
-void TseitinCnfStream::convertAndAssertIte(TNode node, bool lemma, bool negated) {
+void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) {
   // ITE(p, q, r)
   SatLiteral p = toCNF(node[0], false);
   SatLiteral q = toCNF(node[1], negated);
@@ -578,30 +572,35 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool lemma, bool negated)
 // At the top level we must ensure that all clauses that are asserted are
 // not unit, except for the direct assertions. This allows us to remove the
 // clauses later when they are not needed anymore (lemmas for example).
-void TseitinCnfStream::convertAndAssert(TNode node, bool lemma, bool negated) {
-  Debug("cnf") << "convertAndAssert(" << node << ", lemma = " << lemma << ", negated = " << (negated ? "true" : "false") << ")" << endl;
-  d_assertingLemma = lemma;
+void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated) {
+  Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl;
+  d_removable = removable;
+  convertAndAssert(node, negated);
+}
+
+void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
+  Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
   switch(node.getKind()) {
   case AND:
-    convertAndAssertAnd(node, lemma, negated);
+    convertAndAssertAnd(node, negated);
     break;
   case OR:
-    convertAndAssertOr(node, lemma, negated);
+    convertAndAssertOr(node, negated);
     break;
   case IFF:
-    convertAndAssertIff(node, lemma, negated);
+    convertAndAssertIff(node, negated);
     break;
   case XOR:
-    convertAndAssertXor(node, lemma, negated);
+    convertAndAssertXor(node, negated);
     break;
   case IMPLIES:
-    convertAndAssertImplies(node, lemma, negated);
+    convertAndAssertImplies(node, negated);
     break;
   case ITE:
-    convertAndAssertIte(node, lemma, negated);
+    convertAndAssertIte(node, negated);
     break;
   case NOT:
-    convertAndAssert(node[0], lemma, !negated);
+    convertAndAssert(node[0], !negated);
     break;
   default:
     // Atoms
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index e53b46d9b..fd0ab6291 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -77,9 +77,6 @@ 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) {
@@ -102,11 +99,11 @@ protected:
   void undoTranslate(TNode node, int level);
 
   /**
-   * Are we asserting a lemma (true) or a permanent clause (false).
+   * Are we asserting a removable clause (true) or a permanent clause (false).
    * This is set at the begining of convertAndAssert so that it doesn't
    * need to be passed on over the stack.
    */
-  bool d_assertingLemma;
+  bool d_removable;
 
   /**
    * Asserts the given clause to the sat solver.
@@ -187,10 +184,10 @@ public:
   /**
    * Converts and asserts a formula.
    * @param node node to convert and assert
-   * @param lemma whether the sat solver can choose to remove the clauses
+   * @param removable whether the sat solver can choose to remove the clauses
    * @param negated wheather we are asserting the node negated
    */
-  virtual void convertAndAssert(TNode node, bool lemma, bool negated = false) = 0;
+  virtual void convertAndAssert(TNode node, bool removable, bool negated) = 0;
 
   /**
    * Get the node that is represented by the given SatLiteral.
@@ -248,10 +245,10 @@ public:
   /**
    * Convert a given formula to CNF and assert it to the SAT solver.
    * @param node the formula to assert
-   * @param lemma is this a lemma that is erasable
+   * @param removable is this something that can be erased
    * @param negated true if negated
    */
-  void convertAndAssert(TNode node, bool lemma, bool negated = false);
+  void convertAndAssert(TNode node, bool removable, bool negated);
 
   /**
    * Constructs the stream to use the given sat solver.
@@ -262,6 +259,11 @@ public:
 
 private:
 
+  /**
+   * Same as above, except that removable is rememebered.
+   */
+  void convertAndAssert(TNode node, bool negated);
+
   // Each of these formulas handles takes care of a Node of each Kind.
   //
   // Each handleX(Node &n) is responsible for:
@@ -280,12 +282,12 @@ private:
   SatLiteral handleAnd(TNode node);
   SatLiteral handleOr(TNode node);
 
-  void convertAndAssertAnd(TNode node, bool lemma, bool negated);
-  void convertAndAssertOr(TNode node, bool lemma, bool negated);
-  void convertAndAssertXor(TNode node, bool lemma, bool negated);
-  void convertAndAssertIff(TNode node, bool lemma, bool negated);
-  void convertAndAssertImplies(TNode node, bool lemma, bool negated);
-  void convertAndAssertIte(TNode node, bool lemma, bool negated);
+  void convertAndAssertAnd(TNode node, bool negated);
+  void convertAndAssertOr(TNode node, bool negated);
+  void convertAndAssertXor(TNode node, bool negated);
+  void convertAndAssertIff(TNode node, bool negated);
+  void convertAndAssertImplies(TNode node, bool negated);
+  void convertAndAssertIte(TNode node, bool negated);
 
   /**
    * Transforms the node into CNF recursively.
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 0c4f00875..a5774ee7b 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -47,6 +47,20 @@ static DoubleOption  opt_restart_inc       (_cat, "rinc",        "Restart interv
 static DoubleOption  opt_garbage_frac      (_cat, "gc-frac",     "The fraction of wasted memory allowed before a garbage collection is triggered",  0.20, DoubleRange(0, false, HUGE_VAL, false));
 
 
+class ScopedBool {
+  bool& watch;
+  bool oldValue;
+public:
+  ScopedBool(bool& watch, bool newValue)
+  : watch(watch), oldValue(watch) {
+    watch = newValue;
+  }
+  ~ScopedBool() {
+    watch = oldValue;
+  }
+};
+
+
 //=================================================================================================
 // Constructor/Destructor:
 
@@ -55,8 +69,7 @@ Solver::Solver(CVC4::prop::SatSolver* proxy, CVC4::context::Context* context, bo
   , context(context)
   , assertionLevel(0)
   , enable_incremental(enable_incremental)
-  , problem_extended(false)
-  , in_solve(false)
+  , minisat_busy(false)
     // Parameters (user settable):
     //
   , verbosity        (0)
@@ -121,30 +134,26 @@ Solver::~Solver()
 Var Solver::newVar(bool sign, bool dvar, bool theoryAtom)
 {
     int v = nVars();
+
     watches  .init(mkLit(v, false));
     watches  .init(mkLit(v, true ));
     assigns  .push(l_Undef);
-    vardata  .push(mkVarData(CRef_Undef, 0, assertionLevel));
-    //activity .push(0);
+    vardata  .push(mkVarData(CRef_Undef, 0, assertionLevel, 0));
     activity .push(rnd_init_act ? drand(random_seed) * 0.00001 : 0);
     seen     .push(0);
     polarity .push(sign);
     decision .push();
     trail    .capacity(v+1);
-    setDecisionVar(v, dvar);
     theory   .push(theoryAtom);
 
-    // We have extended the problem
-    if (in_solve) {
-      problem_extended = true;
-      insertVarOrder(v);
-    }
+    setDecisionVar(v, dvar);
 
     return v;
 }
 
 
-CRef Solver::reason(Var x) const {
+CRef Solver::reason(Var x) {
+
     // If we already have a reason, just return it
     if (vardata[x].reason != CRef_Lazy) return vardata[x].reason;
 
@@ -154,11 +163,12 @@ CRef Solver::reason(Var x) const {
     // Get the explanation from the theory
     SatClause explanation;
     proxy->explainPropagation(l, explanation);
+    
+    // Sort the literals by trail index level
+    lemma_lt lt(*this);
+    sort(explanation, lt);
     Assert(explanation[0] == l);
 
-    // We're actually changing the state, so we hack it into non-const
-    Solver* nonconst_this = const_cast<Solver*>(this);
-
     // Compute the assertion level for this clause
     int explLevel = 0;
     for (int i = 0; i < explanation.size(); ++ i) {
@@ -169,105 +179,54 @@ CRef Solver::reason(Var x) const {
     }
 
     // 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);
+    CRef real_reason = ca.alloc(explLevel, explanation, true);
+    vardata[x] = mkVarData(real_reason, level(x), intro_level(x), trail_index(x));
+    clauses_removable.push(real_reason);
+    attachClause(real_reason);
     return real_reason;
 }
 
-bool Solver::addClause_(vec<Lit>& ps, ClauseType type)
+bool Solver::addClause_(vec<Lit>& ps, bool removable)
 {
     if (!ok) return false;
 
-    bool propagate_first_literal = false;
-
     // Check if clause is satisfied and remove false/duplicate literals:
     sort(ps);
     Lit p; int i, j;
-    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;
-        Debug("minisat::lemmas") << "Asserting lemma with " << ps.size() << " literals." << std::endl;
-        bool lemmaSatisfied = false;
-        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
-            Debug("minisat::lemmas") << "Lemma is a tautology." << std::endl;
-            return true;
-          }
-          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];
-            if (value(p) == l_True) lemmaSatisfied = true;
-            assigned_lits.push(p);
-            Debug("minisat::lemmas") << proxy->getNode(p) << " has value " << value(p) << std::endl;
-          }
-        }
-        Assert(j >= 1 || lemmaSatisfied, "You are asserting a falsified lemma, produce a conflict instead!");
-        // If only one literal we could have unit propagation
-        if (j == 1 && !lemmaSatisfied) 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 (level(var(p)) > max_level && value(p) == l_False) {
-            max_level = level(var(p));
-            max_level_j = j - 1;
-          }
-        }
-        if (value(ps[1]) != l_Undef && max_level != -1) {
-          std::swap(ps[1], ps[max_level_j]);
-        }
-        ps.shrink(i - j);
+
+    // Check the clause for tautologies and similar
+    for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
+      if ((ps[i] == ~p) || (value(ps[i]) == l_True && level(var(ps[i])) == 0)) {
+        // Clause can be ignored
+        return true;
+      }
+      if ((ps[i] != p) && (value(ps[i]) != l_False || level(var(ps[i])) > 0)) {
+        // This literal is a keeper
+        ps[j++] = p = ps[i];
+      }
     }
 
-    if (ps.size() == 0)
-        return ok = false;
-    else if (ps.size() == 1){
-        if(in_solve) {
-          assert(type != CLAUSE_LEMMA);
-          assert(value(ps[0]) == l_Undef);
-        } else {
-          // [MGD] at "pre-solve" time we allow unit T-lemmas
-          if(value(ps[0]) == l_True) {
-            // this unit T-lemma is extraneous (perhaps it was
-            // discovered twice at presolve time)
-            return true;
-          }
-          assert(value(ps[0]) == l_Undef);
-        }
+    // Fit to size
+    ps.shrink(i - j);
+
+
+    // If we are in solve or decision level > 0
+    if (minisat_busy || decisionLevel() > 0) {
+      lemmas.push();
+      ps.copyTo(lemmas.last());
+      lemmas_removable.push(removable);
+    } else {
+      // Add the clause and attach if not a lemma
+      if (ps.size() == 0) {
+          return ok = false;
+      } else if (ps.size() == 1) {
         uncheckedEnqueue(ps[0]);
         return ok = (propagate(CHECK_WITHOUTH_PROPAGATION_QUICK) == CRef_Undef);
-    }else{
-        CRef cr = ca.alloc(type == CLAUSE_LEMMA ? 0 : assertionLevel, ps, false);
-        clauses.push(cr);
+      } else {
+        CRef cr = ca.alloc(assertionLevel, ps, false);
+        clauses_persistent.push(cr);
 	attachClause(cr);
-        if (propagate_first_literal) {
-          Debug("minisat::lemmas") << "Lemma propagating: " << (theory[var(ps[0])] ? proxy->getNode(ps[0]).toString() : "bool") << std::endl;
-          lemma_propagated_literals.push(ps[0]);
-          lemma_propagated_reasons.push(cr);
-          propagating_lemmas.push(cr);
-        }
-    }
-
-    if (type == CLAUSE_LEMMA) {
-      problem_extended = true;
+      }
     }
 
     return true;
@@ -280,7 +239,7 @@ void Solver::attachClause(CRef cr) {
     Assert(c.size() > 1);
     watches[~c[0]].push(Watcher(cr, c[1]));
     watches[~c[1]].push(Watcher(cr, c[0]));
-    if (c.learnt()) learnts_literals += c.size();
+    if (c.removable()) learnts_literals += c.size();
     else            clauses_literals += c.size(); }
 
 
@@ -298,7 +257,7 @@ void Solver::detachClause(CRef cr, bool strict) {
         watches.smudge(~c[1]);
     }
 
-    if (c.learnt()) learnts_literals -= c.size();
+    if (c.removable()) learnts_literals -= c.size();
     else            clauses_literals -= c.size(); }
 
 
@@ -322,7 +281,7 @@ bool Solver::satisfied(const Clause& c) const {
 
 // Revert to the state at given level (keeping all assignment at 'level' but not beyond).
 //
-void Solver::cancelUntil(int level, bool re_propagate) {
+void Solver::cancelUntil(int level) {
     if (decisionLevel() > level){
         // Pop the SMT context
         for (int l = trail_lim.size() - level; l > 0; --l)
@@ -336,49 +295,7 @@ void Solver::cancelUntil(int level, bool re_propagate) {
         qhead = trail_lim[level];
         trail.shrink(trail.size() - trail_lim[level]);
         trail_lim.shrink(trail_lim.size() - level);
-
-        // Re-Propagate the lemmas if asked
-        if (re_propagate) {
-          rePropagate(level);
-        }
-    }
-}
-
-CRef Solver::rePropagate(int level) {
-  // 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) {
-      if (value(lemma[0]) != l_Undef) {
-        if (value(lemma[0]) == l_False) {
-          // Conflict
-          return propagating_lemmas[i];
-        } else {
-          // Already there
-          continue;
-        }
-      }
-      // Propagate
-      uncheckedEnqueue(lemma[0], propagating_lemmas[i]);
-      // Remember the lemma
-      propagating_lemmas[j++] = propagating_lemmas[i];
     }
-  }
-  Assert(i >= j);
-  propagating_lemmas.shrink(propagating_lemmas.size() - j);
-  Assert(propagating_lemmas_lim.size() >= level);
-  propagating_lemmas_lim.shrink(propagating_lemmas_lim.size() - level);
-
-  // No conflict
-  return CRef_Undef;
 }
 
 void Solver::popTrail() {
@@ -470,7 +387,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
           max_level = c.level();
         }
 
-        if (c.learnt())
+        if (c.removable())
             claBumpActivity(c);
 
         for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
@@ -650,7 +567,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(), intro_level(var(p)));
+    vardata[var(p)] = mkVarData(from, decisionLevel(), intro_level(var(p)), trail.size());
     trail.push_(p);
     if (theory[var(p)]) {
       // Enqueue to the theory
@@ -663,11 +580,25 @@ CRef Solver::propagate(TheoryCheckType type)
 {
     CRef confl = CRef_Undef;
 
+    ScopedBool scoped_bool(minisat_busy, true);
+
+    // If we are not in the quick mode add the lemmas that were left begind
+    if (type != CHECK_WITHOUTH_PROPAGATION_QUICK && lemmas.size() > 0) {
+      confl = updateLemmas();
+      if (confl != CRef_Undef) {
+        return confl;
+      }
+    }
+
     // If this is the final check, no need for Boolean propagation and
     // theory propagation
     if (type == CHECK_WITHOUTH_PROPAGATION_FINAL) {
-      confl = theoryCheck(CVC4::theory::Theory::FULL_EFFORT);
-      return confl;
+      // Do the theory check
+      theoryCheck(CVC4::theory::Theory::FULL_EFFORT);
+      // If there are lemmas (or conflicts) update them
+      if (lemmas.size() > 0) {
+        return updateLemmas();
+      }
     }
 
     // The effort we will be using to theory check
@@ -677,26 +608,36 @@ CRef Solver::propagate(TheoryCheckType type)
 
     // Keep running until we have checked everything, we
     // have no conflict and no new literals have been asserted
-    bool new_assertions;
     do {
-        new_assertions = false;
-        while(qhead < trail.size()) {
-            confl = propagateBool();
-            if (confl != CRef_Undef) break;
-            confl = theoryCheck(effort);
-            if (confl != CRef_Undef) break;
-        }
+        do {
+          // Propagate on the clauses
+          confl = propagateBool();
+
+          // If no conflict, do the theory check
+          if (confl == CRef_Undef) {
+              // Do the theory check
+              theoryCheck(effort);
+              // If there are lemmas (or conflicts) update them
+              if (lemmas.size() > 0) {
+                  confl = updateLemmas();
+              }
+          }
+        } while (confl == CRef_Undef && qhead < trail.size());
 
+        // If still consistent do some theory propagation
         if (confl == CRef_Undef && type == CHECK_WITH_PROPAGATION_STANDARD) {
-          new_assertions = propagateTheory();
-          if (!new_assertions) break;
+          propagateTheory();
+          if (lemmas.size() > 0) {
+              confl = updateLemmas();
+          }
         }
-    } while (new_assertions);
+
+    } while (confl == CRef_Undef && qhead < trail.size());
 
     return confl;
 }
 
-bool Solver::propagateTheory() {
+void Solver::propagateTheory() {
   std::vector<Lit> propagatedLiterals;
   proxy->theoryPropagate(propagatedLiterals);
   const unsigned i_end = propagatedLiterals.size();
@@ -705,7 +646,6 @@ bool Solver::propagateTheory() {
     uncheckedEnqueue(propagatedLiterals[i], CRef_Lazy);
   }
   proxy->clearPropagatedLiterals();
-  return propagatedLiterals.size() > 0;
 }
 
 /*_________________________________________________________________________________________________
@@ -718,43 +658,9 @@ bool Solver::propagateTheory() {
 |
 |    Note: the propagation queue might be NOT empty
 |________________________________________________________________________________________________@*/
-CRef Solver::theoryCheck(CVC4::theory::Theory::Effort effort)
+void Solver::theoryCheck(CVC4::theory::Theory::Effort effort)
 {
-  CRef c = CRef_Undef;
-  SatClause clause;
-  proxy->theoryCheck(effort, clause);
-  int clause_size = clause.size();
-  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) {
-      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;
-    }
-    // Unit conflict, we just duplicate the first literal
-    if (clause_size == 1) {
-      clause.push(clause[0]);
-      Debug("unit-conflict") << "Unit conflict" << proxy->getNode(clause[0]) << std::endl;
-    }
-    // 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;
-    Assert(max_level <= decisionLevel(), "What is going on, can't get literals of a higher level as conflict!");
-    if (max_level < decisionLevel()) {
-      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 (level 0)
-    c = ca.alloc(max_intro_level, clause, true);
-    learnts.push(c);
-    attachClause(c);
-  }
-  return c;
+  proxy->theoryCheck(effort);
 }
 
 /*_________________________________________________________________________________________________
@@ -848,19 +754,19 @@ struct reduceDB_lt {
 void Solver::reduceDB()
 {
     int     i, j;
-    double  extra_lim = cla_inc / learnts.size();    // Remove any clause below this activity
+    double  extra_lim = cla_inc / clauses_removable.size();    // Remove any clause below this activity
 
-    sort(learnts, reduceDB_lt(ca));
+    sort(clauses_removable, reduceDB_lt(ca));
     // Don't delete binary or locked clauses. From the rest, delete clauses from the first half
     // and clauses with activity smaller than 'extra_lim':
-    for (i = j = 0; i < learnts.size(); i++){
-        Clause& c = ca[learnts[i]];
-        if (c.size() > 2 && !locked(c) && (i < learnts.size() / 2 || c.activity() < extra_lim))
-            removeClause(learnts[i]);
+    for (i = j = 0; i < clauses_removable.size(); i++){
+        Clause& c = ca[clauses_removable[i]];
+        if (c.size() > 2 && !locked(c) && (i < clauses_removable.size() / 2 || c.activity() < extra_lim))
+            removeClause(clauses_removable[i]);
         else
-            learnts[j++] = learnts[i];
+            clauses_removable[j++] = clauses_removable[i];
     }
-    learnts.shrink(i - j);
+    clauses_removable.shrink(i - j);
     checkGarbage();
 }
 
@@ -920,9 +826,9 @@ bool Solver::simplify()
         return true;
 
     // Remove satisfied clauses:
-    removeSatisfied(learnts);
+    removeSatisfied(clauses_removable);
     if (remove_satisfied)        // Can be turned off.
-        removeSatisfied(clauses);
+        removeSatisfied(clauses_persistent);
     checkGarbage();
     rebuildOrderHeap();
 
@@ -955,57 +861,33 @@ lbool Solver::search(int nof_conflicts)
     starts++;
 
     TheoryCheckType check_type = CHECK_WITH_PROPAGATION_STANDARD;
-    for (;;){
+    for (;;) {
 
-        // If we have more assertions from lemmas, we continue
-        if (problem_extended) {
-
-          Debug("minisat::lemmas") << "Problem extended with lemmas, adding propagations." << std::endl;
+        // Propagate and call the theory solvers
+        CRef confl = propagate(check_type);
+        Assert(lemmas.size() == 0);
 
-          for (int i = 0, i_end = lemma_propagated_literals.size(); i < i_end; ++ i) {
-            if (value(var(lemma_propagated_literals[i])) == l_Undef) {
-              Debug("minisat::lemmas") << "Lemma propagating: " << proxy->getNode(lemma_propagated_literals[i]) << std::endl;
-              uncheckedEnqueue(lemma_propagated_literals[i], lemma_propagated_reasons[i]);
-            }
-          }
+        if (confl != CRef_Undef) {
 
-          lemma_propagated_literals.clear();
-          lemma_propagated_reasons.clear();
+          conflicts++; conflictC++;
 
-          check_type = CHECK_WITH_PROPAGATION_STANDARD;
-          problem_extended = false;
-        }
+          if (decisionLevel() == 0) return l_False;
 
-        CRef confl = propagate(check_type);
-        if (confl != CRef_Undef){
-            // Clear the propagated literals
-            lemma_propagated_literals.clear();
-            lemma_propagated_reasons.clear();
-
-            // CONFLICT
-            while (confl != CRef_Undef) {
-              conflicts++; conflictC++;
-              if (decisionLevel() == 0) return l_False;
-
-              // Analyze the conflict
-              learnt_clause.clear();
-              int max_level = analyze(confl, learnt_clause, backtrack_level);
-              cancelUntil(backtrack_level, false);
-
-              // Assert the conflict clause and the asserting literal
-              if (learnt_clause.size() == 1){
-                  uncheckedEnqueue(learnt_clause[0]);
-              }else{
-                  CRef cr = ca.alloc(max_level, learnt_clause, true);
-                  learnts.push(cr);
-                  attachClause(cr);
-                  claBumpActivity(ca[cr]);
-                  uncheckedEnqueue(learnt_clause[0], cr);
-              }
+            // Analyze the conflict
+            learnt_clause.clear();
+            int max_level = analyze(confl, learnt_clause, backtrack_level);
+            cancelUntil(backtrack_level);
 
-              // We repropagate lemmas
-              confl = rePropagate(backtrack_level);
-            };
+            // Assert the conflict clause and the asserting literal
+            if (learnt_clause.size() == 1) {
+                uncheckedEnqueue(learnt_clause[0]);
+            } else {
+                CRef cr = ca.alloc(max_level, learnt_clause, true);
+                clauses_removable.push(cr);
+                attachClause(cr);
+                claBumpActivity(ca[cr]);
+                uncheckedEnqueue(learnt_clause[0], cr);
+            }
 
             varDecayActivity();
             claDecayActivity();
@@ -1022,52 +904,59 @@ 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 (problem_extended)
-              continue;
+        } else {
 
 	    // If this was a final check, we are satisfiable
-            if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL)
-              return l_True;
+            if (check_type == CHECK_WITHOUTH_PROPAGATION_FINAL) {
+              // Unless a lemma has added more stuff to the queues
+              if (!order_heap.empty() || qhead < trail.size()) {
+                check_type = CHECK_WITH_PROPAGATION_STANDARD;
+                continue;
+              } else {
+                // Yes, we're truly satisfiable
+                return l_True;
+              }
+            }
 
-            if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()){
+            if (nof_conflicts >= 0 && conflictC >= nof_conflicts || !withinBudget()) {
                 // Reached bound on number of conflicts:
                 progress_estimate = progressEstimate();
                 cancelUntil(0);
                 // [mdeters] notify theory engine of restarts for deferred
                 // theory processing
                 proxy->notifyRestart();
-                return l_Undef; }
+                return l_Undef;
+            }
 
             // Simplify the set of problem clauses:
-            if (decisionLevel() == 0 && !simplify())
+            if (decisionLevel() == 0 && !simplify()) {
                 return l_False;
+            }
 
-            if (learnts.size()-nAssigns() >= max_learnts)
+            if (clauses_removable.size()-nAssigns() >= max_learnts) {
                 // Reduce the set of learnt clauses:
                 reduceDB();
+            }
 
             Lit next = lit_Undef;
-            while (decisionLevel() < assumptions.size()){
+            while (decisionLevel() < assumptions.size()) {
                 // Perform user provided assumption:
                 Lit p = assumptions[decisionLevel()];
-                if (value(p) == l_True){
+                if (value(p) == l_True) {
                     // Dummy decision level:
                     newDecisionLevel();
-                }else if (value(p) == l_False){
+                } else if (value(p) == l_False) {
                     analyzeFinal(~p, conflict);
                     return l_False;
-                }else{
+                } else {
                     next = p;
                     break;
                 }
             }
 
-            if (next == lit_Undef){
+            if (next == lit_Undef) {
                 // New variable decision:
                 decisions++;
                 next = pickBranchLit();
@@ -1138,12 +1027,12 @@ lbool Solver::solve_()
 {
     Debug("minisat") << "nvars = " << nVars() << std::endl;
 
-    in_solve = true;
+    ScopedBool scoped_bool(minisat_busy, true);
 
     model.clear();
     conflict.clear();
     if (!ok){
-      in_solve = false;
+      minisat_busy = false;
       return l_False;
     }
 
@@ -1187,8 +1076,6 @@ lbool Solver::solve_()
     // Cancel the trail downto previous push
     popTrail();
 
-    in_solve = false;
-
     return status;
 }
 
@@ -1240,13 +1127,13 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
     // Cannot use removeClauses here because it is not safe
     // to deallocate them at this point. Could be improved.
     int cnt = 0;
-    for (int i = 0; i < clauses.size(); i++)
-        if (!satisfied(ca[clauses[i]]))
+    for (int i = 0; i < clauses_persistent.size(); i++)
+        if (!satisfied(ca[clauses_persistent[i]]))
             cnt++;
         
-    for (int i = 0; i < clauses.size(); i++)
-        if (!satisfied(ca[clauses[i]])){
-            Clause& c = ca[clauses[i]];
+    for (int i = 0; i < clauses_persistent.size(); i++)
+        if (!satisfied(ca[clauses_persistent[i]])){
+            Clause& c = ca[clauses_persistent[i]];
             for (int j = 0; j < c.size(); j++)
                 if (value(c[j]) != l_False)
                     mapVar(var(c[j]), map, max);
@@ -1262,8 +1149,8 @@ void Solver::toDimacs(FILE* f, const vec<Lit>& assumps)
         fprintf(f, "%s%d 0\n", sign(assumptions[i]) ? "-" : "", mapVar(var(assumptions[i]), map, max)+1);
     }
 
-    for (int i = 0; i < clauses.size(); i++)
-        toDimacs(f, ca[clauses[i]], map, max);
+    for (int i = 0; i < clauses_persistent.size(); i++)
+        toDimacs(f, ca[clauses_persistent[i]], map, max);
 
     if (verbosity > 0)
         printf("Wrote %d clauses with %d variables.\n", cnt, max);
@@ -1293,26 +1180,19 @@ void Solver::relocAll(ClauseAllocator& to)
     for (int i = 0; i < trail.size(); i++){
         Var v = var(trail[i]);
 
-        if (hasReason(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
+        if (hasReasonClause(v) && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
             ca.reloc(vardata[v].reason, to);
     }
 
     // All learnt:
     //
-    for (int i = 0; i < learnts.size(); i++)
-        ca.reloc(learnts[i], to);
+    for (int i = 0; i < clauses_removable.size(); i++)
+        ca.reloc(clauses_removable[i], to);
 
     // All original:
     //
-    for (int i = 0; i < clauses.size(); i++)
-        ca.reloc(clauses[i], to);
-
-    // All lemmas
-    //
-    for (int i = 0; i < lemma_propagated_reasons.size(); i ++)
-      ca.reloc(lemma_propagated_reasons[i], to);
-    for (int i = 0; i < propagating_lemmas.size(); i ++)
-      ca.reloc(propagating_lemmas[i], to);
+    for (int i = 0; i < clauses_persistent.size(); i++)
+        ca.reloc(clauses_persistent[i], to);
 }
 
 
@@ -1342,8 +1222,8 @@ 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);
+    removeClausesAboveLevel(clauses_removable, assertionLevel);
+    removeClausesAboveLevel(clauses_persistent, assertionLevel);
 
     // Pop the user trail size
     popTrail();
@@ -1366,4 +1246,101 @@ void Solver::renewVar(Lit lit, int level) {
   setDecisionVar(v, true);
 }
 
+CRef Solver::updateLemmas() {
+
+  Debug("minisat::lemmas") << "Solver::updateLemmas()" << std::endl;
+
+  CRef conflict = CRef_Undef;
+
+  // Decision level to backtrack to
+  int backtrackLevel = decisionLevel();
+
+  // We use this comparison operator
+  lemma_lt lt(*this);
+
+  // Check for propagation and level to backtrack to
+  for (int i = 0; i < lemmas.size(); ++ i)
+  {
+    // The current lemma
+    vec<Lit>& lemma = lemmas[i];
+    // If it's an empty lemma, we have a conflict at zero level
+    if (lemma.size() == 0) {
+      conflict = CRef_Lazy;
+      backtrackLevel = 0;
+      Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl;
+      continue;
+    }
+    // Sort the lemma to be able to attach
+    sort(lemma, lt);
+    // See if the lemma propagates something
+    if (lemma.size() == 1 || value(lemma[1]) == l_False) {
+      // This lemma propagates, see which level we need to backtrack to
+      int currentBacktrackLevel = lemma.size() == 1 ? 0 : level(var(lemma[1]));
+      // Even if the first literal is true, we should propagate it at this level (unless it's set at a lower level)
+      if (value(lemma[0]) != l_True || level(var(lemma[0])) > currentBacktrackLevel) {
+        if (currentBacktrackLevel < backtrackLevel) {
+          backtrackLevel = currentBacktrackLevel;
+        }
+      }
+    }
+  }
+
+  // Pop so that propagation would be current
+  Debug("minisat::lemmas") << "Solver::updateLemmas(): backtracking to " << backtrackLevel << " from " << decisionLevel() << std::endl;
+  cancelUntil(backtrackLevel);
+
+  // Last index in the trail
+  int backtrack_index = trail.size();
+
+  // Attach all the clauses and enqueue all the propagations
+  for (int i = 0; i < lemmas.size(); ++ i)
+  {
+    // The current lemma
+    vec<Lit>& lemma = lemmas[i];
+    bool removable = lemmas_removable[i];
+
+    // Attach it if non-unit
+    CRef lemma_ref = CRef_Undef;
+    if (lemma.size() > 1) {
+      lemma_ref = ca.alloc(assertionLevel, lemma, removable);
+      if (removable) {
+        clauses_removable.push(lemma_ref);
+      } else {
+        clauses_persistent.push(lemma_ref);
+      }
+      attachClause(lemma_ref);
+    }
+
+    // If the lemma is propagating enqueue it's literal (or set the conflict)
+    if (conflict == CRef_Undef && value(lemma[0]) != l_True) {
+      if (lemma.size() == 1 || (value(lemma[1]) == l_False && trail_index(var(lemma[1])) < backtrack_index)) {
+        if (value(lemma[0]) == l_False) {
+          // We have a conflict
+          if (lemma.size() > 1) {
+            Debug("minisat::lemmas") << "Solver::updateLemmas(): conflict" << std::endl;
+            conflict = lemma_ref;
+          } else {
+            Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl;
+            conflict = CRef_Lazy;
+          }
+        } else {
+//          if (Debug.isOn("minisat::lemmas")) {
+//          	Debug("minisat::lemmas") << "Solver::updateLemmas(): " << lemma[0] << " from ";
+//          	Clause& c = ca[lemma_ref];
+//          	for (int i = 0; i < c.size(); ++ i) {
+//          	   Debug("minisat::lemmas") << c[i] << "(" << value(c[i]) << "," << level(var(c[i])) << "," << trail_index(var(c[i])) << ") "; 
+//          	} 
+//			Debug("minisat::lemmas") << std::endl; 
+//          }
+          uncheckedEnqueue(lemma[0], lemma_ref);
+        }
+      }
+    }
+  }
+
+  // Clear the lemmas
+  lemmas.clear();
+  lemmas_removable.clear();
 
+  return conflict;
+}
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 1eb407c62..8eb82d9f1 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -65,22 +65,17 @@ protected:
   /** 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;
+  vec< vec<Lit> > lemmas;
+
+  /** Is the lemma removable */
+  vec<bool> lemmas_removable;
 
   /** Shrink 'cs' to contain only clauses below given level */
   void removeClausesAboveLevel(vec<CRef>& cs, int level); 
 
   /** True if we are currently solving. */
-  bool in_solve;
+  bool minisat_busy;
 
 public:
 
@@ -93,16 +88,35 @@ public:
     //
     Var     newVar    (bool polarity = true, bool dvar = true, bool theoryAtom = false); // Add a new variable with parameters specifying variable mode.
 
-    // Types of clauses
-    enum ClauseType {
-      // Clauses defined by the problem
-      CLAUSE_PROBLEM,
-      // Lemma clauses added by the theories
-      CLAUSE_LEMMA,
-      // Conflict clauses
-      CLAUSE_CONFLICT
+    // Less than for literals in a lemma
+    struct lemma_lt {
+        Solver& solver;
+        lemma_lt(Solver& solver) : solver(solver) {}
+        bool operator () (Lit x, Lit y) {
+          lbool x_value = solver.value(x);
+          lbool y_value = solver.value(y);
+          // Two unassigned literals are sorted arbitrarily
+          if (x_value == l_Undef && y_value == l_Undef) {
+            return x < y;
+          }
+          // Unassigned literals are put to front
+          if (x_value == l_Undef) return true;
+          if (y_value == l_Undef) return false;
+          // Literals of the same value are sorted by decreasing levels
+          if (x_value == y_value) {
+            return solver.trail_index(var(x)) > solver.trail_index(var(y));
+          } else {
+            // True literals go up front
+            if (x_value == l_True) {
+              return true;
+            } else {
+              return false;
+            }
+          }
+        }
     };
 
+
     // CVC4 context push/pop
     void          push                     ();
     void          pop                      ();
@@ -110,12 +124,12 @@ public:
     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. 
-    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);                     // Add a clause to the solver without making superflous internal copy. Will
+    bool    addClause (const vec<Lit>& ps, bool removable);                     // Add a clause to the solver.
+    bool    addEmptyClause(bool removable);                                     // Add the empty clause, making the solver contradictory.
+    bool    addClause (Lit p, bool removable);                                  // Add a unit clause to the solver.
+    bool    addClause (Lit p, Lit q, bool removable);                           // Add a binary clause to the solver.
+    bool    addClause (Lit p, Lit q, Lit r, bool removable);                    // Add a ternary clause to the solver.
+    bool    addClause_(      vec<Lit>& ps, bool removable);                     // Add a clause to the solver without making superflous internal copy. Will
                                                                                  // change the passed vector 'ps'.
 
     // Solving:
@@ -207,8 +221,8 @@ protected:
 
     // Helper structures:
     //
-    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 VarData { CRef reason; int level; int intro_level; int trail_index; };
+    static inline VarData mkVarData(CRef cr, int l, int intro_l, int trail_i){ VarData d = {cr, l, intro_l, trail_i}; return d; }
 
     struct Watcher {
         CRef cref;
@@ -233,28 +247,28 @@ protected:
 
     // Solver state:
     //
-    bool                ok;               // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
-    vec<CRef>           clauses;          // List of problem clauses.
-    vec<CRef>           learnts;          // List of learnt clauses.
-    double              cla_inc;          // Amount to bump next clause with.
-    vec<double>         activity;         // A heuristic measurement of the activity of a variable.
-    double              var_inc;          // Amount to bump next variable with.
+    bool                ok;                 // If FALSE, the constraints are already unsatisfiable. No part of the solver state may be used!
+    vec<CRef>           clauses_persistent; // List of problem clauses.
+    vec<CRef>           clauses_removable;  // List of learnt clauses.
+    double              cla_inc;            // Amount to bump next clause with.
+    vec<double>         activity;           // A heuristic measurement of the activity of a variable.
+    double              var_inc;            // Amount to bump next variable with.
     OccLists<Lit, vec<Watcher>, WatcherDeleted>
-                        watches;          // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
-    vec<lbool>          assigns;          // The current assignments.
-    vec<char>           polarity;         // The preferred polarity of each variable.
-    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()'.
-    int64_t             simpDB_props;     // Remaining number of propagations that must be made before next execution of 'simplify()'.
-    vec<Lit>            assumptions;      // Current set of assumptions provided to solve by the user.
-    Heap<VarOrderLt>    order_heap;       // A priority queue of variables ordered with respect to the variable activity.
-    double              progress_estimate;// Set by 'search()'.
-    bool                remove_satisfied; // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
+                        watches;            // 'watches[lit]' is a list of constraints watching 'lit' (will go there if literal becomes true).
+    vec<lbool>          assigns;            // The current assignments.
+    vec<char>           polarity;           // The preferred polarity of each variable.
+    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()'.
+    int64_t             simpDB_props;       // Remaining number of propagations that must be made before next execution of 'simplify()'.
+    vec<Lit>            assumptions;        // Current set of assumptions provided to solve by the user.
+    Heap<VarOrderLt>    order_heap;         // A priority queue of variables ordered with respect to the variable activity.
+    double              progress_estimate;  // Set by 'search()'.
+    bool                remove_satisfied;   // Indicates whether possibly inefficient linear scan for satisfied clauses should be performed in 'simplify'.
 
     ClauseAllocator     ca;
 
@@ -297,10 +311,10 @@ protected:
     bool     enqueue          (Lit p, CRef from = CRef_Undef);                         // Test if fact 'p' contradicts current state, enqueue otherwise.
     CRef     propagate        (TheoryCheckType type);                                  // Perform Boolean and Theory. Returns possibly conflicting clause.
     CRef     propagateBool    ();                                                      // Perform Boolean propagation. Returns possibly conflicting clause.
-    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, bool re_propagate = true);                   // Backtrack until a certain level.
-    CRef     rePropagate      (int level);                                             // Re-propagate on lemmas, returns a concflict clause if it introduces a conflict
+    void     propagateTheory  ();                                                      // Perform Theory propagation.
+    void     theoryCheck      (CVC4::theory::Theory::Effort effort);                   // Perform a theory satisfiability check. Adds lemmas.
+    CRef     updateLemmas     ();                                                      // Add the lemmas, backtraking if necessary and return a conflict if there is one
+    void     cancelUntil      (int level);                                             // Backtrack until a certain level.
     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?
@@ -333,10 +347,14 @@ protected:
     //
     int      decisionLevel    ()      const; // Gives the current decisionlevel.
     uint32_t abstractLevel    (Var x) const; // Used to represent an abstraction of sets of decision levels.
-    CRef     reason           (Var x) const;
-    bool     hasReason        (Var x) const; // Does the variable have a reason
+    CRef     reason           (Var x); // Get the reason of the variable (non const as it might create the explanation on the fly)
+    bool     hasReasonClause  (Var x) const; // Does the variable have a reason
+    bool     isPropagated     (Var x) const; // Does the variable have a propagated variables
+    bool     isPropagatedBy   (Var x, const Clause& c) const; // Is the value of the variable propagated by the clause Clause C
+
     int      level            (Var x) const;
     int      intro_level      (Var x) const; // Level at which this variable was introduced
+    int      trail_index      (Var x) const; // Index in the trail
     double   progressEstimate ()      const; // DELETE THIS ?? IT'S NOT VERY USEFUL ...
     bool     withinBudget     ()      const;
 
@@ -360,12 +378,18 @@ protected:
 //=================================================================================================
 // Implementation of inline methods:
 
-inline bool Solver::hasReason(Var x) const { return vardata[x].reason != CRef_Undef && vardata[x].reason != CRef_Lazy; }
+inline bool Solver::hasReasonClause(Var x) const { return vardata[x].reason != CRef_Undef && vardata[x].reason != CRef_Lazy; }
+
+inline bool Solver::isPropagated(Var x) const { return vardata[x].reason != CRef_Undef; }
+
+inline bool Solver::isPropagatedBy(Var x, const Clause& c) const { return vardata[x].reason != CRef_Undef && vardata[x].reason != CRef_Lazy && ca.lea(vardata[var(c[0])].reason) == &c; }
 
 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 int  Solver::trail_index(Var x) const { return vardata[x].trail_index; }
+
 inline void Solver::insertVarOrder(Var x) {
     if (!order_heap.inHeap(x) && decision[x]) order_heap.insert(x); }
 
@@ -386,8 +410,8 @@ inline void Solver::claDecayActivity() { cla_inc *= (1 / clause_decay); }
 inline void Solver::claBumpActivity (Clause& c) {
         if ( (c.activity() += cla_inc) > 1e20 ) {
             // Rescale:
-            for (int i = 0; i < learnts.size(); i++)
-                ca[learnts[i]].activity() *= 1e-20;
+            for (int i = 0; i < clauses_removable.size(); i++)
+                ca[clauses_removable[i]].activity() *= 1e-20;
             cla_inc *= 1e-20; } }
 
 inline void Solver::checkGarbage(void){ return checkGarbage(garbage_frac); }
@@ -397,13 +421,13 @@ inline void Solver::checkGarbage(double gf){
 
 // NOTE: enqueue does not set the ok flag! (only public methods do)
 inline bool     Solver::enqueue         (Lit p, CRef from)      { return value(p) != l_Undef ? value(p) != l_False : (uncheckedEnqueue(p, from), true); }
-inline bool     Solver::addClause       (const vec<Lit>& ps, ClauseType type)    { ps.copyTo(add_tmp); return addClause_(add_tmp, type); }
-inline bool     Solver::addEmptyClause  (ClauseType type)                        { add_tmp.clear(); return addClause_(add_tmp, type); }
-inline bool     Solver::addClause       (Lit p, ClauseType type)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, 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()); propagating_lemmas_lim.push(propagating_lemmas.size()); context->push(); }
+inline bool     Solver::addClause       (const vec<Lit>& ps, bool removable)    { ps.copyTo(add_tmp); return addClause_(add_tmp, removable); }
+inline bool     Solver::addEmptyClause  (bool removable)                        { add_tmp.clear(); return addClause_(add_tmp, removable); }
+inline bool     Solver::addClause       (Lit p, bool removable)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable); }
+inline bool     Solver::addClause       (Lit p, Lit q, bool removable)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); }
+inline bool     Solver::addClause       (Lit p, Lit q, Lit r, bool removable)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); }
+inline bool     Solver::locked          (const Clause& c) const { return value(c[0]) == l_True && isPropagatedBy(var(c[0]), c); }
+inline void     Solver::newDecisionLevel()                      { trail_lim.push(trail.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); }
@@ -412,8 +436,8 @@ inline lbool    Solver::value         (Lit p) const   { return assigns[var(p)] ^
 inline lbool    Solver::modelValue    (Var x) const   { return model[x]; }
 inline lbool    Solver::modelValue    (Lit p) const   { return model[var(p)] ^ sign(p); }
 inline int      Solver::nAssigns      ()      const   { return trail.size(); }
-inline int      Solver::nClauses      ()      const   { return clauses.size(); }
-inline int      Solver::nLearnts      ()      const   { return learnts.size(); }
+inline int      Solver::nClauses      ()      const   { return clauses_persistent.size(); }
+inline int      Solver::nLearnts      ()      const   { return clauses_removable.size(); }
 inline int      Solver::nVars         ()      const   { return vardata.size(); }
 inline int      Solver::nFreeVars     ()      const   { return (int)dec_vars - (trail_lim.size() == 0 ? trail.size() : trail_lim[0]); }
 inline void     Solver::setPolarity   (Var v, bool b) { polarity[v] = b; }
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index 5fdabb2f1..1aff5094d 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -124,7 +124,7 @@ typedef RegionAllocator<uint32_t>::Ref CRef;
 class Clause {
     struct {
         unsigned mark      : 2;
-        unsigned learnt    : 1;
+        unsigned removable : 1;
         unsigned has_extra : 1;
         unsigned reloced   : 1;
         unsigned size      : 27;
@@ -135,9 +135,9 @@ class Clause {
 
     // NOTE: This constructor cannot be used directly (doesn't allocate enough memory).
     template<class V>
-    Clause(const V& ps, bool use_extra, bool learnt, int level) {
+    Clause(const V& ps, bool use_extra, bool removable, int level) {
         header.mark      = 0;
-        header.learnt    = learnt;
+        header.removable = removable;
         header.has_extra = use_extra;
         header.reloced   = 0;
         header.size      = ps.size();
@@ -147,7 +147,7 @@ class Clause {
             data[i].lit = ps[i];
 
         if (header.has_extra){
-            if (header.learnt)
+            if (header.removable)
                 data[header.size].act = 0; 
             else 
                 calcAbstraction(); }
@@ -166,7 +166,7 @@ public:
     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); }
-    bool         learnt      ()      const   { return header.learnt; }
+    bool         removable   ()      const   { return header.removable; }
     bool         has_extra   ()      const   { return header.has_extra; }
     uint32_t     mark        ()      const   { return header.mark; }
     void         mark        (uint32_t m)    { header.mark = m; }
@@ -211,14 +211,14 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
         RegionAllocator<uint32_t>::moveTo(to); }
 
     template<class Lits>
-    CRef alloc(int level, const Lits& ps, bool learnt = false)
+    CRef alloc(int level, const Lits& ps, bool removable = false)
     {
         assert(sizeof(Lit)      == sizeof(uint32_t));
         assert(sizeof(float)    == sizeof(uint32_t));
-        bool use_extra = learnt | extra_clause_field;
+        bool use_extra = removable | extra_clause_field;
 
         CRef cid = RegionAllocator<uint32_t>::alloc(clauseWord32Size(ps.size(), use_extra));
-        new (lea(cid)) Clause(ps, use_extra, learnt, level);
+        new (lea(cid)) Clause(ps, use_extra, removable, level);
 
         return cid;
     }
@@ -244,13 +244,13 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
         
         if (c.reloced()) { cr = c.relocation(); return; }
         
-        cr = to.alloc(c.level(), c, c.learnt());
+        cr = to.alloc(c.level(), c, c.removable());
         c.relocate(cr);
         
         // Copy extra data-fields: 
         // (This could be cleaned-up. Generalize Clause-constructor to be applicable here instead?)
         to[cr].mark(c.mark());
-        if (to[cr].learnt())         to[cr].activity() = c.activity();
+        if (to[cr].removable())         to[cr].activity() = c.activity();
         else if (to[cr].has_extra()) to[cr].calcAbstraction();
     }
 };
@@ -380,7 +380,7 @@ inline Lit Clause::subsumes(const Clause& other) const
 
     //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);
+    assert(!header.removable);   assert(!other.header.removable);
     assert(header.has_extra); assert(other.header.has_extra);
     if (other.header.size < header.size || (data[header.size].abs & ~other.data[other.header.size].abs) != 0)
         return lit_Error;
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 8bcd9fe76..271aabb52 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -134,23 +134,23 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
 
 
 
-bool SimpSolver::addClause_(vec<Lit>& ps, ClauseType type)
+bool SimpSolver::addClause_(vec<Lit>& ps, bool removable)
 {
 #ifndef NDEBUG
     for (int i = 0; i < ps.size(); i++)
         assert(!isEliminated(var(ps[i])));
 #endif
 
-    int nclauses = clauses.size();
+    int nclauses = clauses_persistent.size();
 
     if (use_rcheck && implied(ps))
         return true;
 
-    if (!Solver::addClause_(ps, type))
+    if (!Solver::addClause_(ps, removable))
         return false;
 
-    if (use_simplification && clauses.size() == nclauses + 1){
-        CRef          cr = clauses.last();
+    if (use_simplification && clauses_persistent.size() == nclauses + 1){
+        CRef          cr = clauses_persistent.last();
         const Clause& c  = ca[cr];
 
         // NOTE: the clause is added to the queue immediately and then
@@ -516,9 +516,12 @@ bool SimpSolver::eliminateVar(Var v)
     // Produce clauses in cross product:
     vec<Lit>& resolvent = add_tmp;
     for (int i = 0; i < pos.size(); i++)
-        for (int j = 0; j < neg.size(); j++)
-            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, CLAUSE_CONFLICT))
+        for (int j = 0; j < neg.size(); j++) {
+            bool removable = ca[pos[i]].removable() && ca[pos[neg[j]]].removable();
+            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable)) {
                 return false;
+            }
+        }
 
     // Free occurs list for this variable:
     occurs[v].clear(true);
@@ -555,8 +558,9 @@ bool SimpSolver::substitute(Var v, Lit x)
 
         removeClause(cls[i]);
 
-        if (!addClause_(subst_clause, CLAUSE_PROBLEM))
+        if (!addClause_(subst_clause, c.removable())) {
             return ok = false;
+        }
     }
 
     return true;
@@ -669,10 +673,10 @@ void SimpSolver::cleanUpClauses()
 {
     occurs.cleanAll();
     int i,j;
-    for (i = j = 0; i < clauses.size(); i++)
-        if (ca[clauses[i]].mark() == 0)
-            clauses[j++] = clauses[i];
-    clauses.shrink(i - j);
+    for (i = j = 0; i < clauses_persistent.size(); i++)
+        if (ca[clauses_persistent[i]].mark() == 0)
+            clauses_persistent[j++] = clauses_persistent[i];
+    clauses_persistent.shrink(i - j);
 }
 
 
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index a7359e28e..9b5e5d45c 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -47,12 +47,12 @@ class SimpSolver : public Solver {
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true, bool theoryAtom = false);
-    bool    addClause (const vec<Lit>& ps, ClauseType type);
-    bool    addEmptyClause(ClauseType type);                  // Add the empty clause to the 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 (const vec<Lit>& ps, bool removable);
+    bool    addEmptyClause(bool removable);                  // Add the empty clause to the solver.
+    bool    addClause (Lit p, bool removable);               // Add a unit clause to the solver.
+    bool    addClause (Lit p, Lit q, bool removable);        // Add a binary clause to the solver.
+    bool    addClause (Lit p, Lit q, Lit r, bool removable); // Add a ternary clause to the solver.
+    bool    addClause_(vec<Lit>& ps, bool removable);
     bool    substitute(Var v, Lit x);  // Replace all occurences of v with x (may cause a contradiction).
 
     // Variable mode:
@@ -181,11 +181,11 @@ inline void SimpSolver::updateElimHeap(Var v) {
         elim_heap.update(v); }
 
 
-inline bool SimpSolver::addClause    (const vec<Lit>& ps, ClauseType type)    { ps.copyTo(add_tmp); return addClause_(add_tmp, type); }
-inline bool SimpSolver::addEmptyClause(ClauseType type)                       { add_tmp.clear(); return addClause_(add_tmp, type); }
-inline bool SimpSolver::addClause    (Lit p, ClauseType type)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, type); }
-inline bool SimpSolver::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 SimpSolver::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 SimpSolver::addClause    (const vec<Lit>& ps, bool removable)    { ps.copyTo(add_tmp); return addClause_(add_tmp, removable); }
+inline bool SimpSolver::addEmptyClause(bool removable)                       { add_tmp.clear(); return addClause_(add_tmp, removable); }
+inline bool SimpSolver::addClause    (Lit p, bool removable)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, bool removable)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r, bool removable)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); }
 inline void SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
 
 inline bool SimpSolver::solve        (                     bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; }
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 3aa014782..046e4ef7e 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -86,7 +86,7 @@ void PropEngine::assertFormula(TNode node) {
   d_cnfStream->convertAndAssert(d_theoryEngine->preprocess(node), false, false);
 }
 
-void PropEngine::assertLemma(TNode node) {
+void PropEngine::assertLemma(TNode node, bool negated, bool removable) {
   //Assert(d_inCheckSat, "Sat solver should be in solve()!");
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
 
@@ -102,7 +102,7 @@ void PropEngine::assertLemma(TNode node) {
 
   //TODO This comment is now false
   // Assert as removable
-  d_cnfStream->convertAndAssert(node, true, false);
+  d_cnfStream->convertAndAssert(node, removable, negated);
 }
 
 void PropEngine::printSatisfyingAssignment(){
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index f6e66bef1..599439987 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -99,7 +99,7 @@ public:
    *
    * @param node the formula to assert
    */
-  void assertLemma(TNode node);
+  void assertLemma(TNode node, bool negated, bool removable);
 
   /**
    * Checks the current context for satisfiability.
diff --git a/src/prop/sat.cpp b/src/prop/sat.cpp
index f34699e2b..62558cac1 100644
--- a/src/prop/sat.cpp
+++ b/src/prop/sat.cpp
@@ -27,33 +27,8 @@
 namespace CVC4 {
 namespace prop {
 
-void SatSolver::theoryCheck(theory::Theory::Effort effort, SatClause& conflict) {
-  Assert(conflict.size() == 0);
-  // Try theory propagation
-  bool ok = d_theoryEngine->check(effort);
-  // If in conflict construct the conflict clause
-  if (!ok) {
-    // We have a conflict, get it
-    Node conflictNode = d_theoryEngine->getConflict();
-    Debug("prop") << "SatSolver::theoryCheck() => conflict: " << conflictNode << std::endl;
-    if(conflictNode.getKind() == kind::AND) {
-      // Go through the literals and construct the conflict clause
-      Node::const_iterator literal_it = conflictNode.begin();
-      Node::const_iterator literal_end = conflictNode.end();
-      while (literal_it != literal_end) {
-        // Get the literal corresponding to the node
-        SatLiteral l = d_cnfStream->getLiteral(*literal_it);
-        // Add the negation to the conflict clause and continue
-        conflict.push(~l);
-        literal_it ++;
-      }
-    } else { // unit conflict
-      // Get the literal corresponding to the node
-      SatLiteral l = d_cnfStream->getLiteral(conflictNode);
-      // construct the unit conflict clause
-      conflict.push(~l);
-    }
-  }
+void SatSolver::theoryCheck(theory::Theory::Effort effort) {
+  d_theoryEngine->check(effort);
 }
 
 void SatSolver::theoryPropagate(std::vector<SatLiteral>& output) {
diff --git a/src/prop/sat.h b/src/prop/sat.h
index c00115cd8..2521f3ee7 100644
--- a/src/prop/sat.h
+++ b/src/prop/sat.h
@@ -101,7 +101,7 @@ public:
   /** Virtual destructor to make g++ happy */
   virtual ~SatInputInterface() { }
   /** Assert a clause in the solver. */
-  virtual void addClause(SatClause& clause, bool lemma) = 0;
+  virtual void addClause(SatClause& clause, bool removable) = 0;
   /** Create a new boolean variable in the solver. */
   virtual SatVariable newVar(bool theoryAtom = false) = 0;
   /** Get the current decision level of the solver */
@@ -212,11 +212,11 @@ public:
 
   bool solve();
 
-  void addClause(SatClause& clause, bool lemma);
+  void addClause(SatClause& clause, bool removable);
 
   SatVariable newVar(bool theoryAtom = false);
 
-  void theoryCheck(theory::Theory::Effort effort, SatClause& conflict);
+  void theoryCheck(theory::Theory::Effort effort);
 
   void explainPropagation(SatLiteral l, SatClause& explanation);
 
@@ -290,8 +290,8 @@ inline bool SatSolver::solve() {
   return d_minisat->solve();
 }
 
-inline void SatSolver::addClause(SatClause& clause, bool lemma) {
-  d_minisat->addClause(clause, lemma ? Minisat::Solver::CLAUSE_LEMMA : Minisat::Solver::CLAUSE_PROBLEM);
+inline void SatSolver::addClause(SatClause& clause, bool removable) {
+  d_minisat->addClause(clause, removable);
 }
 
 inline SatVariable SatSolver::newVar(bool theoryAtom) {
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 28d7ab2c0..b1b4d67dd 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -235,8 +235,8 @@ void TheoryEngine::preRegister(TNode preprocessed) {
  * Check all (currently-active) theories for conflicts.
  * @param effort the effort level to use
  */
-bool TheoryEngine::check(theory::Theory::Effort effort) {
-  d_theoryOut.d_conflictNode = Node::null();
+void TheoryEngine::check(theory::Theory::Effort effort) {
+
   d_theoryOut.d_propagatedLiterals.clear();
 
 #ifdef CVC4_FOR_EACH_THEORY_STATEMENT
@@ -245,8 +245,8 @@ bool TheoryEngine::check(theory::Theory::Effort effort) {
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
   if (theory::TheoryTraits<THEORY>::hasCheck && d_theoryIsActive[THEORY]) { \
      reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->check(effort); \
-     if (!d_theoryOut.d_conflictNode.get().isNull()) { \
-       return false; \
+     if (d_theoryOut.d_inConflict) { \
+       return; \
      } \
   }
 
@@ -256,8 +256,6 @@ bool TheoryEngine::check(theory::Theory::Effort effort) {
   } catch(const theory::Interrupted&) {
     Trace("theory") << "TheoryEngine::check() => conflict" << std::endl;
   }
-
-  return true;
 }
 
 void TheoryEngine::propagate() {
@@ -296,7 +294,6 @@ bool TheoryEngine::presolve() {
   // at doing something with the input formula, even if it wouldn't
   // otherwise be active.
 
-  d_theoryOut.d_conflictNode = Node::null();
   d_theoryOut.d_propagatedLiterals.clear();
 
   try {
@@ -307,7 +304,7 @@ bool TheoryEngine::presolve() {
 #define CVC4_FOR_EACH_THEORY_STATEMENT(THEORY) \
     if (theory::TheoryTraits<THEORY>::hasPresolve) { \
       reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(d_theoryTable[THEORY])->presolve(); \
-      if(!d_theoryOut.d_conflictNode.get().isNull()) { \
+      if(d_theoryOut.d_inConflict) { \
         return true; \
       } \
     }
@@ -318,7 +315,7 @@ bool TheoryEngine::presolve() {
     Trace("theory") << "TheoryEngine::presolve() => interrupted" << endl;
   }
   // return whether we have a conflict
-  return !d_theoryOut.d_conflictNode.get().isNull();
+  return false;
 }
 
 
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h
index 3507723f9..1e5653564 100644
--- a/src/theory/theory_engine.h
+++ b/src/theory/theory_engine.h
@@ -98,7 +98,7 @@ class TheoryEngine {
 
     TheoryEngine* d_engine;
     context::Context* d_context;
-    context::CDO<Node> d_conflictNode;
+    context::CDO<bool> d_inConflict;
     context::CDO<Node> d_explanationNode;
 
     /**
@@ -113,12 +113,29 @@ class TheoryEngine {
                    d_newFactTimer,
                    "theory::newFactTimer");
 
+    /**
+     * Check if the node is in conflict for debug purposes
+     */
+    bool isProperConflict(TNode conflictNode) {
+      bool value;
+      if (conflictNode.getKind() == kind::AND) {
+        for (unsigned i = 0; i < conflictNode.getNumChildren(); ++ i) {
+          if (!d_engine->getPropEngine()->hasValue(conflictNode[i], value)) return false;
+          if (!value) return false;
+        }
+      } else {
+        if (!d_engine->getPropEngine()->hasValue(conflictNode, value)) return false;
+        return value;
+      }
+      return true;
+    }
+
   public:
 
     EngineOutputChannel(TheoryEngine* engine, context::Context* context) :
       d_engine(engine),
       d_context(context),
-      d_conflictNode(context),
+      d_inConflict(context, false),
       d_explanationNode(context) {
     }
 
@@ -126,10 +143,15 @@ class TheoryEngine {
 
     void conflict(TNode conflictNode, bool safe)
       throw(theory::Interrupted, AssertionException) {
-      Trace("theory") << "EngineOutputChannel::conflict("
-                      << conflictNode << ")" << std::endl;
-      d_conflictNode = conflictNode;
+      Trace("theory") << "EngineOutputChannel::conflict(" << conflictNode << ")" << std::endl;
+      d_inConflict = true;
+
       ++(d_engine->d_statistics.d_statConflicts);
+
+      // Construct the lemma (note that no CNF caching should happen as all the literals already exists)
+      Assert(isProperConflict(conflictNode));
+      d_engine->newLemma(conflictNode, true, true);
+
       if(safe) {
         throw theory::Interrupted();
       }
@@ -143,12 +165,13 @@ class TheoryEngine {
       ++(d_engine->d_statistics.d_statPropagate);
     }
 
-    void lemma(TNode node, bool)
+    void lemma(TNode node, bool removable = false)
       throw(theory::Interrupted, AssertionException) {
       Trace("theory") << "EngineOutputChannel::lemma("
                       << node << ")" << std::endl;
       ++(d_engine->d_statistics.d_statLemma);
-      d_engine->newLemma(node);
+
+      d_engine->newLemma(node, false, removable);
     }
 
     void explanation(TNode explanationNode, bool)
@@ -387,7 +410,7 @@ public:
    * Check all (currently-active) theories for conflicts.
    * @param effort the effort level to use
    */
-  bool check(theory::Theory::Effort effort);
+  void check(theory::Theory::Effort effort);
 
   /**
    * Calls staticLearning() on all theories, accumulating their
@@ -414,23 +437,17 @@ public:
     d_theoryOut.d_propagatedLiterals.clear();
   }
 
-  inline void newLemma(TNode node) {
+  inline void newLemma(TNode node, bool negated, bool removable) {
     // Remove the ITEs and assert to prop engine
     std::vector<Node> additionalLemmas;
     additionalLemmas.push_back(node);
     RemoveITE::run(additionalLemmas);
-    for (unsigned i = 0; i < additionalLemmas.size(); ++ i) {
-      d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[i]));
+    d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[0]), negated, removable);
+    for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
+      d_propEngine->assertLemma(theory::Rewriter::rewrite(additionalLemmas[i]), false, removable);
     }
   }
 
-  /**
-   * Returns the last conflict (if any).
-   */
-  inline Node getConflict() {
-    return d_theoryOut.d_conflictNode;
-  }
-
   void propagate();
 
   inline Node getExplanation(TNode node, theory::Theory* theory) {
diff --git a/test/unit/prop/cnf_stream_black.h b/test/unit/prop/cnf_stream_black.h
index f6118d85c..0a49e6a3e 100644
--- a/test/unit/prop/cnf_stream_black.h
+++ b/test/unit/prop/cnf_stream_black.h
@@ -140,7 +140,7 @@ void testAnd() {
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(kind::AND, a, b, c), false);
+      d_nodeManager->mkNode(kind::AND, a, b, c), false, false);
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -161,13 +161,13 @@ void testComplexExpr() {
               d_nodeManager->mkNode(kind::OR, c, d),
               d_nodeManager->mkNode(
                   kind::NOT,
-                  d_nodeManager->mkNode(kind::XOR, e, f)))), false );
+                  d_nodeManager->mkNode(kind::XOR, e, f)))), false, false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
 void testFalse() {
   NodeManagerScope nms(d_nodeManager);
-  d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false );
+  d_cnfStream->convertAndAssert( d_nodeManager->mkConst(false), false, false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -176,7 +176,7 @@ void testIff() {
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(kind::IFF, a, b), false );
+      d_nodeManager->mkNode(kind::IFF, a, b), false, false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -185,7 +185,7 @@ void testImplies() {
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(kind::IMPLIES, a, b), false );
+      d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -201,7 +201,7 @@ void testIte() {
               d_nodeManager->mkVar(d_nodeManager->integerType())
           ),
           d_nodeManager->mkVar(d_nodeManager->integerType())
-                            ), false);
+                            ), false, false);
 
 }
 
@@ -209,7 +209,7 @@ void testNot() {
   NodeManagerScope nms(d_nodeManager);
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(kind::NOT, a), false );
+      d_nodeManager->mkNode(kind::NOT, a), false, false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -219,13 +219,13 @@ void testOr() {
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(kind::OR, a, b, c), false );
+      d_nodeManager->mkNode(kind::OR, a, b, c), false, false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
 void testTrue() {
   NodeManagerScope nms(d_nodeManager);
-  d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false );
+  d_cnfStream->convertAndAssert( d_nodeManager->mkConst(true), false, false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -233,10 +233,10 @@ void testVar() {
   NodeManagerScope nms(d_nodeManager);
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-  d_cnfStream->convertAndAssert(a, false);
+  d_cnfStream->convertAndAssert(a, false, false);
   TS_ASSERT( d_satSolver->addClauseCalled() );
   d_satSolver->reset();
-  d_cnfStream->convertAndAssert(b, false);
+  d_cnfStream->convertAndAssert(b, false, false);
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 
@@ -245,7 +245,7 @@ void testXor() {
   Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
   Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
   d_cnfStream->convertAndAssert(
-      d_nodeManager->mkNode(kind::XOR, a, b), false );
+      d_nodeManager->mkNode(kind::XOR, a, b), false, false );
   TS_ASSERT( d_satSolver->addClauseCalled() );
 }
 };