Merged bit-vector and uf proof branch.

20 files changed, 860 insertions, 367 deletions

diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index be266b6d8..936778e0d 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -19,6 +19,7 @@
 #include "prop/bvminisat/bvminisat.h"
 
 #include "prop/bvminisat/simp/SimpSolver.h"
+#include "proof/sat_proof.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -47,14 +48,18 @@ void BVMinisatSatSolver::setNotify(Notify* notify) {
   d_minisat->setNotify(d_minisatNotify);
 }
 
-void BVMinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) {
+ClauseId BVMinisatSatSolver::addClause(SatClause& clause,
+                                       bool removable) {
   Debug("sat::minisat") << "Add clause " << clause <<"\n";
   BVMinisat::vec<BVMinisat::Lit> minisat_clause;
   toMinisatClause(clause, minisat_clause);
   // for(unsigned i = 0; i < minisat_clause.size(); ++i) {
   //   d_minisat->setFrozen(BVMinisat::var(minisat_clause[i]), true);
   // }
-  d_minisat->addClause(minisat_clause);
+  ClauseId clause_id = ClauseIdError;
+  d_minisat->addClause(minisat_clause, clause_id);
+  THEORY_PROOF(Assert (clause_id != ClauseIdError););
+  return clause_id;
 }
 
 SatValue BVMinisatSatSolver::propagate() {
@@ -91,6 +96,10 @@ void BVMinisatSatSolver::popAssumption() {
   d_minisat->popAssumption();
 }
 
+void BVMinisatSatSolver::setProofLog( BitVectorProof * bvp ) {
+  d_minisat->setProofLog( bvp );
+}
+
 SatVariable BVMinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase){
   return d_minisat->newVar(true, true, !canErase);
 }
@@ -126,6 +135,10 @@ SatValue BVMinisatSatSolver::solve(long unsigned int& resource){
   return result;
 }
 
+bool BVMinisatSatSolver::ok() const {
+  return d_minisat->okay(); 
+}
+
 void BVMinisatSatSolver::getUnsatCore(SatClause& unsatCore) {
   // TODO add assertion to check the call was after an unsat call
   for (int i = 0; i < d_minisat->conflict.size(); ++i) {
@@ -199,8 +212,8 @@ void BVMinisatSatSolver::toMinisatClause(SatClause& clause,
   Assert(clause.size() == (unsigned)minisat_clause.size());
 }
 
-void BVMinisatSatSolver::toSatClause(BVMinisat::vec<BVMinisat::Lit>& clause,
-                                       SatClause& sat_clause) {
+void BVMinisatSatSolver::toSatClause(const BVMinisat::Clause& clause,
+                                     SatClause& sat_clause) {
   for (int i = 0; i < clause.size(); ++i) {
     sat_clause.push_back(toSatLiteral(clause[i]));
   }
@@ -281,3 +294,19 @@ void BVMinisatSatSolver::Statistics::init(BVMinisat::SimpSolver* minisat){
 
 } /* namespace CVC4::prop */
 } /* namespace CVC4 */
+
+namespace CVC4 {
+template<>
+prop::SatLiteral toSatLiteral< BVMinisat::Solver>(BVMinisat::Solver::TLit lit) {
+  return prop::BVMinisatSatSolver::toSatLiteral(lit);
+} 
+
+template<>
+void toSatClause< BVMinisat::Solver> (const BVMinisat::Solver::TClause& minisat_cl,
+                                        prop::SatClause& sat_cl) {
+  prop::BVMinisatSatSolver::toSatClause(minisat_cl, sat_cl);
+}
+
+}
+
+
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 986fbf339..383948e3e 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -43,7 +43,9 @@ private:
     }
     void notify(BVMinisat::vec<BVMinisat::Lit>& clause) {
       SatClause satClause;
-      toSatClause(clause, satClause);
+      for (int i = 0; i < clause.size(); ++i) {
+        satClause.push_back(toSatLiteral(clause[i])); 
+      }
       d_notify->notify(satClause);
     }
 
@@ -73,7 +75,7 @@ public:
 
   void setNotify(Notify* notify);
 
-  void addClause(SatClause& clause, bool removable, uint64_t proof_id);
+  ClauseId addClause(SatClause& clause, bool removable);
 
   SatValue propagate();
 
@@ -88,6 +90,7 @@ public:
 
   SatValue solve();
   SatValue solve(long unsigned int&);
+  bool ok() const; 
   void getUnsatCore(SatClause& unsatCore);
 
   SatValue value(SatLiteral l);
@@ -106,7 +109,7 @@ public:
   static SatValue toSatLiteralValue(BVMinisat::lbool res);
 
   static void  toMinisatClause(SatClause& clause, BVMinisat::vec<BVMinisat::Lit>& minisat_clause);
-  static void  toSatClause    (BVMinisat::vec<BVMinisat::Lit>& clause, SatClause& sat_clause);
+  static void  toSatClause    (const BVMinisat::Clause& clause, SatClause& sat_clause);
   void addMarkerLiteral(SatLiteral lit);
 
   void explain(SatLiteral lit, std::vector<SatLiteral>& explanation);
@@ -114,6 +117,8 @@ public:
   SatValue assertAssumption(SatLiteral lit, bool propagate);
 
   void popAssumption();
+  
+  void setProofLog( BitVectorProof * bvp );
 
 private:
   /* Disable the default constructor. */
diff --git a/src/prop/bvminisat/core/Solver.cc b/src/prop/bvminisat/core/Solver.cc
index 5a37da27c..2100160de 100644
--- a/src/prop/bvminisat/core/Solver.cc
+++ b/src/prop/bvminisat/core/Solver.cc
@@ -31,6 +31,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "options/bv_options.h"
 #include "options/smt_options.h"
 #include "theory/interrupted.h"
+#include "proof/proof_manager.h"
+#include "proof/bitvector_proof.h"
+#include "proof/sat_proof.h"
+#include "proof/sat_proof_implementation.h"
 #include "util/utility.h"
 
 namespace CVC4 {
@@ -60,19 +64,6 @@ std::ostream& operator << (std::ostream& out, const BVMinisat::Clause& c) {
 
 static const char* _cat = "CORE";
 
-// static DoubleOption  opt_var_decay         (_cat, "var-decay",   "The variable activity decay factor",            0.95,     DoubleRange(0, false, 1, false));
-// static DoubleOption  opt_clause_decay      (_cat, "cla-decay",   "The clause activity decay factor",              0.999,    DoubleRange(0, false, 1, false));
-// static DoubleOption  opt_random_var_freq   (_cat, "rnd-freq",    "The frequency with which the decision heuristic tries to choose a random variable", 0.0, DoubleRange(0, true, 1, true));
-// static DoubleOption  opt_random_seed       (_cat, "rnd-seed",    "Used by the random variable selection",         91648253, DoubleRange(0, false, HUGE_VAL, false));
-// static IntOption     opt_ccmin_mode        (_cat, "ccmin-mode",  "Controls conflict clause minimization (0=none, 1=basic, 2=deep)", 0, IntRange(0, 2));
-// static IntOption     opt_phase_saving      (_cat, "phase-saving", "Controls the level of phase saving (0=none, 1=limited, 2=full)", 2, IntRange(0, 2));
-// static BoolOption    opt_rnd_init_act      (_cat, "rnd-init",    "Randomize the initial activity", false);
-// static BoolOption    opt_luby_restart      (_cat, "luby",        "Use the Luby restart sequence", true);
-// static IntOption     opt_restart_first     (_cat, "rfirst",      "The base restart interval", 100, IntRange(1, INT32_MAX)); 
-// static DoubleOption  opt_restart_inc       (_cat, "rinc",        "Restart interval increase factor", 1.5, DoubleRange(1, false, HUGE_VAL, false));
-// 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));
-
-
 static DoubleOption  opt_var_decay         (_cat, "var-decay",   "The variable activity decay factor",            0.95,     DoubleRange(0, false, 1, false));
 static DoubleOption  opt_clause_decay      (_cat, "cla-decay",   "The clause activity decay factor",              0.999,    DoubleRange(0, false, 1, false));
 static DoubleOption  opt_random_var_freq   (_cat, "rnd-freq",    "The frequency with which the decision heuristic tries to choose a random variable", 0, DoubleRange(0, true, 1, true));
@@ -86,6 +77,12 @@ 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));
 
 //=================================================================================================
+// Proof declarations
+CRef Solver::TCRef_Undef = CRef_Undef;
+CRef Solver::TCRef_Lazy = CRef_Undef - 1; // no real lazy ref here
+
+
+//=================================================================================================
 // Constructor/Destructor:
 
 
@@ -150,6 +147,7 @@ Solver::Solver(CVC4::context::Context* c) :
   , conflict_budget    (-1)
   , propagation_budget (-1)
   , asynch_interrupt   (false)
+  , d_bvp              (NULL)
 {
   // Create the constant variables
   varTrue = newVar(true, false);
@@ -193,37 +191,114 @@ Var Solver::newVar(bool sign, bool dvar)
 }
 
 
-bool Solver::addClause_(vec<Lit>& ps)
+bool Solver::addClause_(vec<Lit>& ps, ClauseId& id)
 {
     if (decisionLevel() > 0) {
       cancelUntil(0);
     }
     
-    if (!ok) return false;
+    if (!ok) {
+      id = ClauseIdUndef;
+      return false;
+    }
 
     // Check if clause is satisfied and remove false/duplicate literals:
+    // TODO proof for duplicate literals removal?
     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)
-            return true;
-        else if (value(ps[i]) != l_False && ps[i] != p)
-            ps[j++] = p = ps[i];
+    int falseLiteralsCount = 0;
+    
+    for (i = j = 0, p = lit_Undef; i < ps.size(); i++) {
+      // tautologies are ignored
+      if (value(ps[i]) == l_True || ps[i] == ~p) {
+        id = ClauseIdUndef;
+        return true;
+      }
+
+      // Ignore repeated literals
+      if (ps[i] == p) {
+        continue;
+      }
+
+      if (value(ps[i]) == l_False) {
+        if (!THEORY_PROOF_ON())
+          continue;
+        ++falseLiteralsCount;
+      }
+      ps[j++] = p = ps[i];
+    }
+    
     ps.shrink(i - j);
 
     clause_added = true;
 
-    if (ps.size() == 0)
+    Assert(falseLiteralsCount == 0 || THEORY_PROOF_ON());
+    
+    if(falseLiteralsCount == 0) {
+      if (ps.size() == 0) {
+        Assert (!THEORY_PROOF_ON());
         return ok = false;
-    else if (ps.size() == 1){
+      }
+      else if (ps.size() == 1){
+        if(d_bvp){ id = d_bvp->getSatProof()->registerUnitClause(ps[0], INPUT);}
         uncheckedEnqueue(ps[0]);
-        return ok = (propagate() == CRef_Undef);
-    } else {
+        CRef confl_ref = propagate();
+        ok = (confl_ref == CRef_Undef);
+        if(d_bvp){ if (!ok) d_bvp->getSatProof()->finalizeProof(confl_ref); }
+        return ok;
+      } else {
         CRef cr = ca.alloc(ps, false);
         clauses.push(cr);
         attachClause(cr);
+        if(d_bvp){ id = d_bvp->getSatProof()->registerClause(cr, INPUT);}
+      }
+      return ok; 
     }
-    return ok; 
+    
+    if (falseLiteralsCount != 0 && THEORY_PROOF_ON()) {
+      // we are in a conflicting state
+      if (ps.size() == falseLiteralsCount && falseLiteralsCount == 1) {
+        if(d_bvp){ id = d_bvp->getSatProof()->storeUnitConflict(ps[0], INPUT); }
+        if(d_bvp){ d_bvp->getSatProof()->finalizeProof(CVC4::BVMinisat::CRef_Lazy); }
+        return ok = false;
+      }
+
+      assign_lt lt(*this);
+      sort(ps, lt);
+      
+      CRef cr = ca.alloc(ps, false);
+      clauses.push(cr);
+      attachClause(cr);
+      
+      if(d_bvp){id = d_bvp->getSatProof()->registerClause(cr, INPUT);}
+
+      if(ps.size() == falseLiteralsCount) {
+        if(d_bvp){ d_bvp->getSatProof()->finalizeProof(cr); }
+        return ok = false;
+      }
+      
+      // Check if it propagates
+      if (ps.size() == falseLiteralsCount + 1) {
+        Clause& cl = ca[cr];
+        
+        Assert (value(cl[0]) == l_Undef);
+        uncheckedEnqueue(cl[0], cr);
+        Assert (cl.size() > 1);
+        CRef confl = propagate();
+        ok = (confl == CRef_Undef);
+        if(!ok) {
+          if(d_bvp){
+            if(ca[confl].size() == 1) {
+              id = d_bvp->getSatProof()->storeUnitConflict(ca[confl][0], LEARNT);
+              d_bvp->getSatProof()->finalizeProof(CVC4::BVMinisat::CRef_Lazy);
+            } else {
+              d_bvp->getSatProof()->finalizeProof(confl);
+            }
+          }
+        }
+      }
+    }
+    return ok;
 }
 
 void Solver::attachClause(CRef cr) {
@@ -237,6 +312,8 @@ void Solver::attachClause(CRef cr) {
 
 void Solver::detachClause(CRef cr, bool strict) {
     const Clause& c = ca[cr];
+    if(d_bvp){ d_bvp->getSatProof()->markDeleted(cr); }
+    
     assert(c.size() > 1);
     
     if (strict){
@@ -342,6 +419,9 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
     int index   = trail.size() - 1;
 
     bool done = false;
+    
+    if(d_bvp){ d_bvp->getSatProof()->startResChain(confl); }
+
     do{
         assert(confl != CRef_Undef); // (otherwise should be UIP)
         Clause& c = ca[confl];
@@ -352,7 +432,7 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
         for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
             Lit q = c[j];
 
-            if (!seen[var(q)] && level(var(q)) > 0){
+            if (!seen[var(q)] && level(var(q)) > 0) {
                 varBumpActivity(var(q));
                 seen[var(q)] = 1;
                 if (level(var(q)) >= decisionLevel())
@@ -360,6 +440,10 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
                 else
                     out_learnt.push(q);
             }
+            
+            if (level(var(q)) == 0) {
+              if(d_bvp){ d_bvp->getSatProof()->resolveOutUnit(q); }
+            }
         }
         
         // Select next clause to look at:
@@ -369,6 +453,10 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
         seen[var(p)] = 0;
         pathC--;
 
+        if ( pathC > 0 && confl != CRef_Undef ) {
+          if(d_bvp){ d_bvp->getSatProof()->addResolutionStep(p, confl, sign(p));}
+        }
+
         switch (uip) {
         case UIP_FIRST:
           done = pathC == 0;
@@ -392,11 +480,22 @@ void Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel, UIP uip
         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
+              if (!litRedundant(out_learnt[i], abstract_level)) {
+                // Literal is not redundant
                 out_learnt[j++] = out_learnt[i];
+              } else {
+                if(d_bvp){ d_bvp->getSatProof()->storeLitRedundant(out_learnt[i]); }
+              }
+            }
+        }
         
     }else if (ccmin_mode == 1){
+        Unreachable();
         for (i = j = 1; i < out_learnt.size(); i++){
             Var x = var(out_learnt[i]);
 
@@ -452,10 +551,13 @@ bool Solver::litRedundant(Lit p, uint32_t abstract_levels)
     analyze_stack.clear(); analyze_stack.push(p);
     int top = analyze_toclear.size();
     while (analyze_stack.size() > 0){
-        assert(reason(var(analyze_stack.last())) != CRef_Undef);
-        Clause& c = ca[reason(var(analyze_stack.last()))]; analyze_stack.pop();
+        CRef c_reason = reason(var(analyze_stack.last()));
+        assert(c_reason != CRef_Undef);
+        Clause& c = ca[c_reason];
+        int c_size = c.size();
+        analyze_stack.pop();
 
-        for (int i = 1; i < c.size(); i++){
+        for (int i = 1; i < c_size; i++){
             Lit p  = c[i];
             if (!seen[var(p)] && level(var(p)) > 0){
                 if (reason(var(p)) != CRef_Undef && (abstractLevel(var(p)) & abstract_levels) != 0){
@@ -495,21 +597,36 @@ void Solver::analyzeFinal2(Lit p, CRef confl_clause, vec<Lit>& out_conflict) {
     seen[var(cl[i])] = 1;
   }
 
-  for (int i = trail.size() - 1; i >= trail_lim[0]; i--) {
+  int end = options::proof() ? 0 :  trail_lim[0];
+  for (int i = trail.size() - 1; i >= end; i--) {
     Var x = var(trail[i]);
     if (seen[x]) {
       if (reason(x) == CRef_Undef) {
         // we skip p if was a learnt unit
         if (x != var(p)) {
-          assert (marker[x] == 2);
-          assert (level(x) > 0);
-          out_conflict.push(~trail[i]);
+          if (marker[x] == 2) {
+            assert (level(x) > 0);
+            out_conflict.push(~trail[i]);
+          } else {
+            if(d_bvp){d_bvp->getSatProof()->resolveOutUnit(~(trail[i])); }
+          }
+        } else {
+          if(d_bvp){d_bvp->getSatProof()->resolveOutUnit(~p);} 
         }
       } else {
         Clause& c = ca[reason(x)];
-        for (int j = 1; j < c.size(); j++)
+        if(d_bvp){d_bvp->getSatProof()->addResolutionStep(trail[i],reason(x), sign(trail[i]));}
+
+        for (int j = 1; j < c.size(); j++) {
           if (level(var(c[j])) > 0)
             seen[var(c[j])] = 1;
+          if(d_bvp){
+            if (level(var(c[j])) == 0) {
+              d_bvp->getSatProof()->resolveOutUnit(c[j]);
+              seen[var(c[j])] = 0; // we don't need to resolve it out again
+            }
+          }
+        }
       }
       seen[x] = 0;
     }
@@ -534,12 +651,23 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
       out_conflict.push(p);
     }
 
-    if (decisionLevel() == 0)
-        return;
+    if(d_bvp){
+      if (level(var(p)) == 0 && d_bvp->isAssumptionConflict()) {
+        Assert ( marker[var(p)] == 2);
+        if (reason(var(p)) == CRef_Undef) {
+          d_bvp->startBVConflict(p);
+        }
+      }
+    }
+    
+    if (decisionLevel() == 0 && !options::proof()) {
+      return;
+    }
 
     seen[var(p)] = 1;
-
-    for (int i = trail.size()-1; i >= trail_lim[0]; i--){
+    int end = options::proof() ? 0 : trail_lim[0];
+    
+    for (int i = trail.size()-1; i >= end; i--){
         Var x = var(trail[i]);
         if (seen[x]) {
             if (reason(x) == CRef_Undef) {
@@ -548,9 +676,24 @@ void Solver::analyzeFinal(Lit p, vec<Lit>& out_conflict)
               out_conflict.push(~trail[i]);
             } else {
               Clause& c = ca[reason(x)];
-              for (int j = 1; j < c.size(); j++)
-                if (level(var(c[j])) > 0)
+              if(d_bvp){
+                    if (d_bvp->isAssumptionConflict() &&
+                        trail[i] == p) {
+                      d_bvp->startBVConflict(reason(x));
+                    } else {
+                      d_bvp->getSatProof()->addResolutionStep(trail[i], reason(x), sign(trail[i]));
+                    }
+              }
+              for (int j = 1; j < c.size(); j++) {
+                if (level(var(c[j])) > 0) {
                   seen[var(c[j])] = 1;
+                }
+                if(d_bvp){
+                  if (level(var(c[j])) == 0) {
+                    d_bvp->getSatProof()->resolveOutUnit(c[j]);
+                  }
+                }
+              }
             }
             seen[x] = 0;
         }
@@ -588,9 +731,12 @@ lbool Solver::propagateAssumptions() {
 }
 
 lbool Solver::assertAssumption(Lit p, bool propagate) {
+  // TODO need to somehow mark the assumption as unit in the current context?
+  // it's not always unit though, but this would be useful for debugging
   
   // assert(marker[var(p)] == 1);
 
+ 
   if (decisionLevel() > assumptions.size()) {
     cancelUntil(assumptions.size());
   }
@@ -601,7 +747,8 @@ lbool Solver::assertAssumption(Lit p, bool propagate) {
   if (c->getLevel() > 0) {
     assumptions.push(p);
   } else {
-    if (!addClause(p)) {
+    ClauseId id;
+    if (!addClause(p, id)) {
       conflict.push(~p);
       return l_False;
     }
@@ -618,6 +765,14 @@ lbool Solver::assertAssumption(Lit p, bool propagate) {
   }
 }
 
+void Solver::addMarkerLiteral(Var var) {
+  // make sure it wasn't already marked 
+  Assert(marker[var] == 0); 
+  marker[var] = 1;
+  if(d_bvp){d_bvp->getSatProof()->registerAssumption(var);}
+}
+
+
 /*_________________________________________________________________________________________________
 |
 |  propagate : [void]  ->  [Clause*]
@@ -730,8 +885,13 @@ void Solver::removeSatisfied(vec<CRef>& cs)
     int i, j;
     for (i = j = 0; i < cs.size(); i++){
         Clause& c = ca[cs[i]];
-        if (satisfied(c))
+        if (satisfied(c)) {
+          if (locked(c)) {
+            // store a resolution of the literal c propagated
+            if(d_bvp){ d_bvp->getSatProof()->storeUnitResolution(c[0]); }
+          }
             removeClause(cs[i]);
+        }
         else
             cs[j++] = cs[i];
     }
@@ -807,7 +967,12 @@ lbool Solver::search(int nof_conflicts, UIP uip)
         if (confl != CRef_Undef){
             // CONFLICT
             conflicts++; conflictC++;
-            if (decisionLevel() == 0) return l_False;
+
+            if (decisionLevel() == 0) {
+              // can this happen for bv?
+              if(d_bvp){ d_bvp->getSatProof()->finalizeProof(confl);}
+              return l_False;
+            }
 
             learnt_clause.clear();
             analyze(confl, learnt_clause, backtrack_level, uip);
@@ -821,15 +986,42 @@ lbool Solver::search(int nof_conflicts, UIP uip)
               learnts.push(cr);
               attachClause(cr);
               claBumpActivity(ca[cr]);
+              if(d_bvp){
+                 ClauseId id = d_bvp->getSatProof()->registerClause(cr, LEARNT);
+                 PSTATS(
+                 __gnu_cxx::hash_set<int> cl_levels;
+                 for (int i = 0; i < learnt_clause.size(); ++i) {
+                   cl_levels.insert(level(var(learnt_clause[i])));
+                 }
+                 if( d_bvp ){ d_bvp->getSatProof()->storeClauseGlue(id, cl_levels.size()); }
+                       )
+                 d_bvp->getSatProof()->endResChain(id);
+              }
             }
-
+            
+            if (learnt_clause.size() == 1) {
+              // learning a unit clause
+              if(d_bvp){ d_bvp->getSatProof()->endResChain(learnt_clause[0]);}
+            }
+            
             //  if the uip was an assumption we are unsat
             if (level(var(p)) <= assumptions.size()) {
               for (int i = 0; i < learnt_clause.size(); ++i) {
                 assert (level(var(learnt_clause[i])) <= decisionLevel()); 
                 seen[var(learnt_clause[i])] = 1;
               }
+
+              // Starting new resolution chain for bit-vector proof
+              if( d_bvp ){
+                if (cr == CRef_Undef) {
+                  d_bvp->startBVConflict(learnt_clause[0]);
+                }
+                else { 
+                  d_bvp->startBVConflict(cr);
+                }
+              }
               analyzeFinal(p, conflict);
+              if(d_bvp){ d_bvp->endBVConflict(conflict); }
               Debug("bvminisat::search") << OUTPUT_TAG << " conflict on assumptions " << std::endl;
               return l_False;
             }
@@ -843,7 +1035,10 @@ lbool Solver::search(int nof_conflicts, UIP uip)
                 CRef new_confl = propagate();
                 if (new_confl != CRef_Undef) {
                   // we have a conflict we now need to explain it
-                  analyzeFinal2(p, new_confl, conflict); 
+                  // TODO: proof for analyzeFinal2
+                  if(d_bvp){ d_bvp->startBVConflict(new_confl); }
+                  analyzeFinal2(p, new_confl, conflict);
+                  if(d_bvp){ d_bvp->endBVConflict(conflict); }
                   return l_False;
                 }
               }
@@ -912,7 +1107,10 @@ lbool Solver::search(int nof_conflicts, UIP uip)
                     newDecisionLevel();
                 }else if (value(p) == l_False){
                     marker[var(p)] = 2;
+                    
+                    if(d_bvp){  d_bvp->markAssumptionConflict(); }
                     analyzeFinal(~p, conflict);
+                    if(d_bvp){ d_bvp->endBVConflict(conflict); }
                     Debug("bvminisat::search") << OUTPUT_TAG << " assumption false, we're unsat" << std::endl;
                     return l_False;
                 }else{
@@ -1044,39 +1242,76 @@ lbool Solver::solve_()
 // 
 
 void Solver::explain(Lit p, std::vector<Lit>& explanation) {
-  vec<Lit> queue;
-  queue.push(p);
-
   Debug("bvminisat::explain") << OUTPUT_TAG << "starting explain of " << p << std::endl;
 
-   __gnu_cxx::hash_set<Var> visited;
-  visited.insert(var(p));
+  // top level fact, no explanation necessary
+  if (level(var(p)) == 0) {
+    if(d_bvp){
+          // the only way a marker variable is 
+       if (reason(var(p)) == CRef_Undef) {
+          d_bvp->startBVConflict(p);
+          vec<Lit> confl;
+          confl.push(p);
+          d_bvp->endBVConflict(confl);
+          return;
+       }
+    }
+    if (!THEORY_PROOF_ON())
+      return;
+  }
   
-  while(queue.size() > 0) {
-    Lit l = queue.last();
-
-    Debug("bvminisat::explain") << OUTPUT_TAG << "processing " << l << std::endl;
-
-    assert(value(l) == l_True);
-    queue.pop();
-    if (reason(var(l)) == CRef_Undef) {
-      if (level(var(l)) == 0) continue;
-      Assert(marker[var(l)] == 2);
-      explanation.push_back(l);
-      visited.insert(var(l));
-    } else {
-      Clause& c = ca[reason(var(l))];
-      for (int i = 1; i < c.size(); ++i) {
-        if (level(var(c[i])) > 0 && visited.count(var(c[i])) == 0) {
-          queue.push(~c[i]);
-          visited.insert(var(c[i]));
+  seen[var(p)] = 1;
+
+  // if we are called at decisionLevel = 0 trail_lim is empty
+  int bottom = options::proof() ? 0 : trail_lim[0];
+  for (int i = trail.size()-1; i >= bottom; i--){
+    Var x = var(trail[i]);
+    if (seen[x]) {
+      if (reason(x) == CRef_Undef) {
+        if (marker[x] == 2) {
+          assert(level(x) > 0);
+          explanation.push_back(trail[i]);
+        } else {
+          Assert (level(x) == 0);
+          if(d_bvp){ d_bvp->getSatProof()->resolveOutUnit(~(trail[i])); }
+         }
+        
+      } else {
+        Clause& c = ca[reason(x)];
+        if(d_bvp){
+          if (p == trail[i]) {
+            d_bvp->startBVConflict(reason(var(p)));
+          } else {
+            d_bvp->getSatProof()->addResolutionStep(trail[i], reason(x), sign(trail[i]));
+          }
+        }
+        for (int j = 1; j < c.size(); j++) {
+          if (level(var(c[j])) > 0 || options::proof()) {
+            seen[var(c[j])] = 1;
+          }
         }
       }
+      seen[x] = 0;
     }
   }
+  seen[var(p)] = 0;
+
+  if(d_bvp){
+    vec<Lit> conflict_clause;
+    conflict_clause.push(p);
+    for(unsigned i = 0; i < explanation.size(); ++i) {
+      conflict_clause.push(~explanation[i]);
+    }
+    d_bvp->endBVConflict(conflict_clause);
+  }
 }
 
-  
+void Solver::setProofLog( BitVectorProof * bvp ) {
+  d_bvp = bvp;
+  d_bvp->initSatProof(this);
+  d_bvp->getSatProof()->registerTrueLit(mkLit(varTrue, false));
+  d_bvp->getSatProof()->registerFalseLit(mkLit(varFalse, true));
+}
 
 //=================================================================================================
 // Writing CNF to DIMACS:
@@ -1171,7 +1406,7 @@ void Solver::relocAll(ClauseAllocator& to)
             // printf(" >>> RELOCING: %s%d\n", sign(p)?"-":"", var(p)+1);
             vec<Watcher>& ws = watches[p];
             for (int j = 0; j < ws.size(); j++)
-                ca.reloc(ws[j].cref, to);
+              ca.reloc(ws[j].cref, to, d_bvp ?  d_bvp->getSatProof()->getProxy() : NULL);
         }
 
     // All reasons:
@@ -1180,18 +1415,20 @@ void Solver::relocAll(ClauseAllocator& to)
         Var v = var(trail[i]);
 
         if (reason(v) != CRef_Undef && (ca[reason(v)].reloced() || locked(ca[reason(v)])))
-            ca.reloc(vardata[v].reason, to);
+            ca.reloc(vardata[v].reason, to, d_bvp ?  d_bvp->getSatProof()->getProxy() : NULL);
     }
 
     // All learnt:
     //
     for (int i = 0; i < learnts.size(); i++)
-        ca.reloc(learnts[i], to);
+        ca.reloc(learnts[i], to, d_bvp ?  d_bvp->getSatProof()->getProxy() : NULL);
 
     // All original:
     //
     for (int i = 0; i < clauses.size(); i++)
-        ca.reloc(clauses[i], to);
+        ca.reloc(clauses[i], to, d_bvp ?  d_bvp->getSatProof()->getProxy() : NULL);
+	
+    if(d_bvp){ d_bvp->getSatProof()->finishUpdateCRef(); }
 }
 
 
@@ -1208,5 +1445,25 @@ void Solver::garbageCollect()
     to.moveTo(ca);
 }
 
+void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::BVProofProxy* proxy)
+{
+  CRef old = cr;  // save the old reference
+
+  Clause& c = operator[](cr);
+  if (c.reloced()) { cr = c.relocation(); return; }
+  
+  cr = to.alloc(c, c.learnt());
+  c.relocate(cr);
+  if (proxy) {
+    proxy->updateCRef(old, 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();
+  else if (to[cr].has_extra()) to[cr].calcAbstraction();
+}
+
 } /* CVC4::BVMinisat namespace */
 } /* CVC4 namespace */
diff --git a/src/prop/bvminisat/core/Solver.h b/src/prop/bvminisat/core/Solver.h
index 214e425f9..019c09bcd 100644
--- a/src/prop/bvminisat/core/Solver.h
+++ b/src/prop/bvminisat/core/Solver.h
@@ -26,13 +26,21 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/bvminisat/mtl/Heap.h"
 #include "prop/bvminisat/mtl/Alg.h"
 #include "prop/bvminisat/utils/Options.h"
-
 #include "context/cdhashmap.h"
+#include "proof/sat_proof.h"
 
 #include <ext/hash_set>
 #include <vector>
 
 namespace CVC4 {
+
+typedef unsigned ClauseId;
+namespace BVMinisat {
+class Solver;
+}
+
+class BitVectorProof;
+
 namespace BVMinisat {
 
 /** Interface for minisat callbacks */
@@ -60,7 +68,17 @@ public:
 //=================================================================================================
 // Solver -- the main class:
 class Solver {
-
+    friend class CVC4::TSatProof< CVC4::BVMinisat::Solver>;
+public:
+    typedef Var TVar;
+    typedef Lit TLit;
+    typedef Clause TClause; 
+    typedef CRef TCRef;
+    typedef vec<Lit> TLitVec;
+
+    static CRef TCRef_Undef;
+    static CRef TCRef_Lazy;
+private:
     /** To notify */
     Notify* notify;
 
@@ -89,12 +107,12 @@ public:
     Var     falseVar() const { return varFalse; }
 
 
-    bool    addClause (const vec<Lit>& ps);                     // Add a clause to the solver. 
+    bool    addClause (const vec<Lit>& ps, ClauseId& id);                     // Add a clause to the solver. 
     bool    addEmptyClause();                                   // Add the empty clause, making the solver contradictory.
-    bool    addClause (Lit p);                                  // Add a unit clause to the solver. 
-    bool    addClause (Lit p, Lit q);                           // Add a binary clause to the solver. 
-    bool    addClause (Lit p, Lit q, Lit r);                    // Add a ternary clause to the solver. 
-    bool    addClause_(      vec<Lit>& ps);                     // Add a clause to the solver without making superflous internal copy. Will
+    bool    addClause (Lit p, ClauseId& id);                                  // Add a unit clause to the solver. 
+    bool    addClause (Lit p, Lit q, ClauseId& id);                           // Add a binary clause to the solver. 
+    bool    addClause (Lit p, Lit q, Lit r, ClauseId& id);                    // Add a ternary clause to the solver. 
+    bool    addClause_(      vec<Lit>& ps, ClauseId& id);                     // Add a clause to the solver without making superflous internal copy. Will
                                                                 // change the passed vector 'ps'.
 
     // Solving:
@@ -188,16 +206,14 @@ public:
     // Bitvector Propagations
     //
 
-    void addMarkerLiteral(Var var) {
-      // make sure it wasn't already marked 
-      Assert(marker[var] == 0); 
-      marker[var] = 1;
-    }
+    void addMarkerLiteral(Var var);
 
     bool need_to_propagate;             // true if we added new clauses, set to true in propagation 
     bool only_bcp;                      // solving mode in which only boolean constraint propagation is done
     void setOnlyBCP (bool val) { only_bcp = val;}
     void explain(Lit l, std::vector<Lit>& explanation);
+    
+    void setProofLog( CVC4::BitVectorProof * bvp );
 
 protected:
 
@@ -274,6 +290,9 @@ protected:
     int64_t             conflict_budget;    // -1 means no budget.
     int64_t             propagation_budget; // -1 means no budget.
     bool                asynch_interrupt;
+    
+    //proof log
+    CVC4::BitVectorProof * d_bvp;
 
     // Main internal methods:
     //
@@ -340,6 +359,35 @@ protected:
     // Returns a random integer 0 <= x < size. Seed must never be 0.
     static inline int irand(double& seed, int size) {
         return (int)(drand(seed) * size); }
+
+  // Less than for literals in an added clause when proofs are on.
+  struct assign_lt {
+    Solver& solver;
+    assign_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.level(var(x)) > solver.level(var(y));
+      } else {
+        // True literals go up front
+        if (x_value == l_True) {
+          return true;
+        } else {
+          return false;
+        }
+      }
+    }
+  };
+
 };
 
 
@@ -380,11 +428,11 @@ 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)    { ps.copyTo(add_tmp); return addClause_(add_tmp); }
-inline bool     Solver::addEmptyClause  ()                      { add_tmp.clear(); return addClause_(add_tmp); }
-inline bool     Solver::addClause       (Lit p)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
-inline bool     Solver::addClause       (Lit p, Lit q)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
-inline bool     Solver::addClause       (Lit p, Lit q, Lit r)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
+inline bool     Solver::addClause       (const vec<Lit>& ps, ClauseId& id)    { ps.copyTo(add_tmp); return addClause_(add_tmp, id); }
+inline bool     Solver::addEmptyClause  ()                      { add_tmp.clear(); ClauseId tmp; return addClause_(add_tmp, tmp); }
+inline bool     Solver::addClause       (Lit p, ClauseId& id)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, id); }
+inline bool     Solver::addClause       (Lit p, Lit q, ClauseId& id)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, id); }
+inline bool     Solver::addClause       (Lit p, Lit q, Lit r, ClauseId& id)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, id); }
 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()); }
 
diff --git a/src/prop/bvminisat/core/SolverTypes.h b/src/prop/bvminisat/core/SolverTypes.h
index aa0921b78..1fd7ac5a7 100644
--- a/src/prop/bvminisat/core/SolverTypes.h
+++ b/src/prop/bvminisat/core/SolverTypes.h
@@ -31,6 +31,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 namespace CVC4 {
 namespace BVMinisat {
+class Solver;
+}
+template <class Solver> class ProofProxy;
+typedef ProofProxy<BVMinisat::Solver> BVProofProxy;
+}
+
+namespace CVC4 {
+
+namespace BVMinisat {
 
 //=================================================================================================
 // Variables, literals, lifted booleans, clauses:
@@ -205,6 +214,8 @@ public:
 
 
 const CRef CRef_Undef = RegionAllocator<uint32_t>::Ref_Undef;
+const CRef CRef_Lazy  = RegionAllocator<uint32_t>::Ref_Undef - 1;
+
 class ClauseAllocator : public RegionAllocator<uint32_t>
 {
     static int clauseWord32Size(int size, bool has_extra){
@@ -245,21 +256,7 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
         RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra()));
     }
 
-    void reloc(CRef& cr, ClauseAllocator& to)
-    {
-        Clause& c = operator[](cr);
-        
-        if (c.reloced()) { cr = c.relocation(); return; }
-        
-        cr = to.alloc(c, c.learnt());
-        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();
-        else if (to[cr].has_extra()) to[cr].calcAbstraction();
-    }
+  void reloc(CRef& cr, ClauseAllocator& to, CVC4::BVProofProxy* proxy = NULL);
 };
 
 
diff --git a/src/prop/bvminisat/simp/SimpSolver.cc b/src/prop/bvminisat/simp/SimpSolver.cc
index c5b185c95..311ed1dd1 100644
--- a/src/prop/bvminisat/simp/SimpSolver.cc
+++ b/src/prop/bvminisat/simp/SimpSolver.cc
@@ -24,6 +24,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "options/bv_options.h"
 #include "options/smt_options.h"
 #include "utils/System.h"
+#include "proof/proof.h"
 
 namespace CVC4 {
 namespace BVMinisat {
@@ -62,7 +63,7 @@ SimpSolver::SimpSolver(CVC4::context::Context* c) :
   , asymm_lits         (0)
   , eliminated_vars    (0)
   , elimorder          (1)
-  , use_simplification (true)
+  , use_simplification (!PROOF_ON())
   , occurs             (ClauseDeleted(ca))
   , elim_heap          (ElimLt(n_occ))
   , bwdsub_assigns     (0)
@@ -162,7 +163,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
 
 
 
-bool SimpSolver::addClause_(vec<Lit>& ps)
+bool SimpSolver::addClause_(vec<Lit>& ps, ClauseId& id)
 {
 #ifndef NDEBUG
     for (int i = 0; i < ps.size(); i++)
@@ -174,7 +175,7 @@ bool SimpSolver::addClause_(vec<Lit>& ps)
     if (use_rcheck && implied(ps))
         return true;
 
-    if (!Solver::addClause_(ps))
+    if (!Solver::addClause_(ps, id))
         return false;
 
     if (use_simplification && clauses.size() == nclauses + 1){
@@ -544,9 +545,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))
-                return false;
+      for (int j = 0; j < neg.size(); j++) {
+        ClauseId id = -1;
+        if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) &&
+            !addClause_(resolvent, id))
+          return false;
+      }
 
     // Free occurs list for this variable:
     occurs[v].clear(true);
@@ -582,8 +586,8 @@ bool SimpSolver::substitute(Var v, Lit x)
         }
 
         removeClause(cls[i]);
-
-        if (!addClause_(subst_clause))
+        ClauseId id;
+        if (!addClause_(subst_clause, id))
             return ok = false;
     }
 
diff --git a/src/prop/bvminisat/simp/SimpSolver.h b/src/prop/bvminisat/simp/SimpSolver.h
index 85556e935..5f6f46b91 100644
--- a/src/prop/bvminisat/simp/SimpSolver.h
+++ b/src/prop/bvminisat/simp/SimpSolver.h
@@ -42,12 +42,12 @@ class SimpSolver : public Solver {
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true, bool freeze = false);
-    bool    addClause (const vec<Lit>& ps);
+    bool    addClause (const vec<Lit>& ps, ClauseId& id);
     bool    addEmptyClause();                // Add the empty clause to the solver.
-    bool    addClause (Lit p);               // Add a unit clause to the solver.
-    bool    addClause (Lit p, Lit q);        // Add a binary clause to the solver.
-    bool    addClause (Lit p, Lit q, Lit r); // Add a ternary clause to the solver.
-    bool    addClause_(      vec<Lit>& ps);
+    bool    addClause (Lit p, ClauseId& id);               // Add a unit clause to the solver.
+    bool    addClause (Lit p, Lit q, ClauseId& id);        // Add a binary clause to the solver.
+    bool    addClause (Lit p, Lit q, Lit r, ClauseId& id); // Add a ternary clause to the solver.
+    bool    addClause_( vec<Lit>& ps, ClauseId& id);
     bool    substitute(Var v, Lit x);  // Replace all occurences of v with x (may cause a contradiction).
 
     // Variable mode:
@@ -178,11 +178,11 @@ inline void SimpSolver::updateElimHeap(Var v) {
         elim_heap.update(v); }
 
 
-inline bool SimpSolver::addClause    (const vec<Lit>& ps)    { ps.copyTo(add_tmp); return addClause_(add_tmp); }
-inline bool SimpSolver::addEmptyClause()                     { add_tmp.clear(); return addClause_(add_tmp); }
-inline bool SimpSolver::addClause    (Lit p)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp); }
-inline bool SimpSolver::addClause    (Lit p, Lit q)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp); }
-inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp); }
+inline bool SimpSolver::addClause    (const vec<Lit>& ps, ClauseId& id)    { ps.copyTo(add_tmp); return addClause_(add_tmp, id); }
+inline bool SimpSolver::addEmptyClause()                     { add_tmp.clear(); ClauseId id; return addClause_(add_tmp, id); }
+inline bool SimpSolver::addClause    (Lit p, ClauseId& id)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, id); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, ClauseId& id)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, id); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r, ClauseId& id)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, id); }
 inline void SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
 
 inline lbool SimpSolver::solve        (                     bool do_simp, bool turn_off_simp)  {
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index b3666875d..a3d411738 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -24,6 +24,7 @@
 #include "options/bv_options.h"
 #include "proof/proof_manager.h"
 #include "proof/sat_proof.h"
+#include "proof/cnf_proof.h"
 #include "prop/cnf_stream.h"
 #include "prop/minisat/minisat.h"
 #include "prop/prop_engine.h"
@@ -47,7 +48,7 @@ namespace prop {
 
 CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar,
                      context::Context* context, SmtGlobals* globals,
-                     bool fullLitToNodeMap)
+                     bool fullLitToNodeMap, std::string name)
     : d_satSolver(satSolver),
       d_booleanVariables(context),
       d_nodeToLiteralMap(context),
@@ -55,19 +56,21 @@ CnfStream::CnfStream(SatSolver* satSolver, Registrar* registrar,
       d_fullLitToNodeMap(fullLitToNodeMap),
       d_convertAndAssertCounter(0),
       d_registrar(registrar),
-      d_assertionTable(context),
+      d_name(name),
+      d_cnfProof(NULL),
       d_globals(globals),
       d_removable(false) {
 }
 
 TseitinCnfStream::TseitinCnfStream(SatSolver* satSolver, Registrar* registrar,
                                    context::Context* context,
-                                   SmtGlobals* globals, bool fullLitToNodeMap)
-    : CnfStream(satSolver, registrar, context, globals, fullLitToNodeMap)
+                                   SmtGlobals* globals, bool fullLitToNodeMap,
+                                   std::string name)
+  : CnfStream(satSolver, registrar, context, globals, fullLitToNodeMap, name)
 {}
 
-void CnfStream::assertClause(TNode node, SatClause& c, ProofRule proof_id) {
-  Debug("cnf") << "Inserting into stream " << c << " node = " << node << ", proof id = " << proof_id << endl;
+void CnfStream::assertClause(TNode node, SatClause& c) {
+  Debug("cnf") << "Inserting into stream " << c << " node = " << node << endl;
   if(Dump.isOn("clauses")) {
     if(c.size() == 1) {
       Dump("clauses") << AssertCommand(Expr(getNode(c[0]).toExpr()));
@@ -81,31 +84,41 @@ void CnfStream::assertClause(TNode node, SatClause& c, ProofRule proof_id) {
       Dump("clauses") << AssertCommand(Expr(n.toExpr()));
     }
   }
-  //store map between clause and original formula
-  PROOF(ProofManager::currentPM()->setRegisteringFormula( node, proof_id ); );
-  d_satSolver->addClause(c, d_removable, d_proofId);
-  PROOF(ProofManager::currentPM()->setRegisteringFormula( Node::null(), RULE_INVALID ); );
+
+  PROOF(if (d_cnfProof) d_cnfProof->pushCurrentDefinition(node););
+
+  ClauseId clause_id = d_satSolver->addClause(c, d_removable);
+  if (clause_id == ClauseIdUndef) return; // nothing to store (no clause was added)
+
+  PROOF
+    (
+     if (d_cnfProof) {
+       Assert (clause_id != ClauseIdError);
+       d_cnfProof->registerConvertedClause(clause_id);
+       d_cnfProof->popCurrentDefinition();
+     }
+    );
 }
 
-void CnfStream::assertClause(TNode node, SatLiteral a, ProofRule proof_id) {
+void CnfStream::assertClause(TNode node, SatLiteral a) {
   SatClause clause(1);
   clause[0] = a;
-  assertClause(node, clause, proof_id);
+  assertClause(node, clause);
 }
 
-void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, ProofRule proof_id) {
+void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b) {
   SatClause clause(2);
   clause[0] = a;
   clause[1] = b;
-  assertClause(node, clause, proof_id);
+  assertClause(node, clause);
 }
 
-void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c, ProofRule proof_id) {
+void CnfStream::assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c) {
   SatClause clause(3);
   clause[0] = a;
   clause[1] = b;
   clause[2] = c;
-  assertClause(node, clause, proof_id);
+  assertClause(node, clause);
 }
 
 bool CnfStream::hasLiteral(TNode n) const {
@@ -116,7 +129,6 @@ bool CnfStream::hasLiteral(TNode n) const {
 void TseitinCnfStream::ensureLiteral(TNode n) {
   // These are not removable and have no proof ID
   d_removable = false;
-  d_proofId = uint64_t(-1);
 
   Debug("cnf") << "ensureLiteral(" << n << ")" << endl;
   if(hasLiteral(n)) {
@@ -165,7 +177,7 @@ void TseitinCnfStream::ensureLiteral(TNode n) {
 }
 
 SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister, bool canEliminate) {
-  Debug("cnf") << "newLiteral(" << node << ", " << isTheoryAtom << ")" << endl;
+  Debug("cnf") << d_name << "::newLiteral(" << node << ", " << isTheoryAtom << ")" << endl;
   Assert(node.getKind() != kind::NOT);
 
   // Get the literal for this node
@@ -200,10 +212,9 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister
   if (preRegister) {
     // In case we are re-entered due to lemmas, save our state
     bool backupRemovable = d_removable;
-    uint64_t backupProofId= d_proofId;
+    // Should be fine since cnfProof current assertion is stack based.
     d_registrar->preRegister(node);
     d_removable = backupRemovable;
-    d_proofId = backupProofId;
   }
 
   // Here, you can have it
@@ -225,6 +236,11 @@ void CnfStream::getBooleanVariables(std::vector<TNode>& outputVariables) const {
   }
 }
 
+void CnfStream::setProof(CnfProof* proof) {
+  Assert (d_cnfProof == NULL);
+  d_cnfProof = proof;
+}
+
 SatLiteral CnfStream::convertAtom(TNode node) {
   Debug("cnf") << "convertAtom(" << node << ")" << endl;
 
@@ -268,10 +284,10 @@ SatLiteral TseitinCnfStream::handleXor(TNode xorNode) {
 
   SatLiteral xorLit = newLiteral(xorNode);
 
-  assertClause(xorNode.negate(), a, b, ~xorLit, RULE_TSEITIN);
-  assertClause(xorNode.negate(), ~a, ~b, ~xorLit, RULE_TSEITIN);
-  assertClause(xorNode, a, ~b, xorLit, RULE_TSEITIN);
-  assertClause(xorNode, ~a, b, xorLit, RULE_TSEITIN);
+  assertClause(xorNode.negate(), a, b, ~xorLit);
+  assertClause(xorNode.negate(), ~a, ~b, ~xorLit);
+  assertClause(xorNode, a, ~b, xorLit);
+  assertClause(xorNode, ~a, b, xorLit);
 
   return xorLit;
 }
@@ -300,14 +316,14 @@ SatLiteral TseitinCnfStream::handleOr(TNode orNode) {
   // lit | ~(a_1 | a_2 | a_3 | ... | a_n)
   // (lit | ~a_1) & (lit | ~a_2) & (lit & ~a_3) & ... & (lit & ~a_n)
   for(unsigned i = 0; i < n_children; ++i) {
-    assertClause(orNode, orLit, ~clause[i], RULE_TSEITIN);
+    assertClause(orNode, orLit, ~clause[i]);
   }
 
   // lit -> (a_1 | a_2 | a_3 | ... | a_n)
   // ~lit | a_1 | a_2 | a_3 | ... | a_n
   clause[n_children] = ~orLit;
   // This needs to go last, as the clause might get modified by the SAT solver
-  assertClause(orNode.negate(), clause, RULE_TSEITIN);
+  assertClause(orNode.negate(), clause);
 
   // Return the literal
   return orLit;
@@ -337,7 +353,7 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
   // ~lit | (a_1 & a_2 & a_3 & ... & a_n)
   // (~lit | a_1) & (~lit | a_2) & ... & (~lit | a_n)
   for(unsigned i = 0; i < n_children; ++i) {
-    assertClause(andNode.negate(), ~andLit, ~clause[i], RULE_TSEITIN);
+    assertClause(andNode.negate(), ~andLit, ~clause[i]);
   }
 
   // lit <- (a_1 & a_2 & a_3 & ... a_n)
@@ -345,7 +361,7 @@ SatLiteral TseitinCnfStream::handleAnd(TNode andNode) {
   // lit | ~a_1 | ~a_2 | ~a_3 | ... | ~a_n
   clause[n_children] = andLit;
   // This needs to go last, as the clause might get modified by the SAT solver
-  assertClause(andNode, clause, RULE_TSEITIN);
+  assertClause(andNode, clause);
 
   return andLit;
 }
@@ -364,13 +380,13 @@ SatLiteral TseitinCnfStream::handleImplies(TNode impliesNode) {
 
   // lit -> (a->b)
   // ~lit | ~ a | b
-  assertClause(impliesNode.negate(), ~impliesLit, ~a, b, RULE_TSEITIN);
+  assertClause(impliesNode.negate(), ~impliesLit, ~a, b);
 
   // (a->b) -> lit
   // ~(~a | b) | lit
   // (a | l) & (~b | l)
-  assertClause(impliesNode, a, impliesLit, RULE_TSEITIN);
-  assertClause(impliesNode, ~b, impliesLit, RULE_TSEITIN);
+  assertClause(impliesNode, a, impliesLit);
+  assertClause(impliesNode, ~b, impliesLit);
 
   return impliesLit;
 }
@@ -393,16 +409,16 @@ SatLiteral TseitinCnfStream::handleIff(TNode iffNode) {
   // lit -> ((a-> b) & (b->a))
   // ~lit | ((~a | b) & (~b | a))
   // (~a | b | ~lit) & (~b | a | ~lit)
-  assertClause(iffNode.negate(), ~a, b, ~iffLit, RULE_TSEITIN);
-  assertClause(iffNode.negate(), a, ~b, ~iffLit, RULE_TSEITIN);
+  assertClause(iffNode.negate(), ~a, b, ~iffLit);
+  assertClause(iffNode.negate(), a, ~b, ~iffLit);
 
   // (a<->b) -> lit
   // ~((a & b) | (~a & ~b)) | lit
   // (~(a & b)) & (~(~a & ~b)) | lit
   // ((~a | ~b) & (a | b)) | lit
   // (~a | ~b | lit) & (a | b | lit)
-  assertClause(iffNode, ~a, ~b, iffLit, RULE_TSEITIN);
-  assertClause(iffNode, a, b, iffLit, RULE_TSEITIN);
+  assertClause(iffNode, ~a, ~b, iffLit);
+  assertClause(iffNode, a, b, iffLit);
 
   return iffLit;
 }
@@ -437,9 +453,9 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
   // lit -> (t | e) & (b -> t) & (!b -> e)
   // lit -> (t | e) & (!b | t) & (b | e)
   // (!lit | t | e) & (!lit | !b | t) & (!lit | b | e)
-  assertClause(iteNode.negate(), ~iteLit, thenLit, elseLit, RULE_TSEITIN);
-  assertClause(iteNode.negate(), ~iteLit, ~condLit, thenLit, RULE_TSEITIN);
-  assertClause(iteNode.negate(), ~iteLit, condLit, elseLit, RULE_TSEITIN);
+  assertClause(iteNode.negate(), ~iteLit, thenLit, elseLit);
+  assertClause(iteNode.negate(), ~iteLit, ~condLit, thenLit);
+  assertClause(iteNode.negate(), ~iteLit, condLit, elseLit);
 
   // If ITE is false then one of the branches is false and the condition
   // implies which one
@@ -447,9 +463,9 @@ SatLiteral TseitinCnfStream::handleIte(TNode iteNode) {
   // !lit -> (!t | !e) & (b -> !t) & (!b -> !e)
   // !lit -> (!t | !e) & (!b | !t) & (b | !e)
   // (lit | !t | !e) & (lit | !b | !t) & (lit | b | !e)
-  assertClause(iteNode, iteLit, ~thenLit, ~elseLit, RULE_TSEITIN);
-  assertClause(iteNode, iteLit, ~condLit, ~thenLit, RULE_TSEITIN);
-  assertClause(iteNode, iteLit, condLit, ~elseLit, RULE_TSEITIN);
+  assertClause(iteNode, iteLit, ~thenLit, ~elseLit);
+  assertClause(iteNode, iteLit, ~condLit, ~thenLit);
+  assertClause(iteNode, iteLit, condLit, ~elseLit);
 
   return iteLit;
 }
@@ -514,14 +530,14 @@ SatLiteral TseitinCnfStream::toCNF(TNode node, bool negated) {
   else return ~nodeLit;
 }
 
-void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated, ProofRule proof_id) {
+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 ) {
-      PROOF(ProofManager::currentPM()->setCnfDep( (*conjunct).toExpr(), node.toExpr() ) );
-      convertAndAssert(*conjunct, false, proof_id);
+      PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence(*conjunct, node););
+      convertAndAssert(*conjunct, false);
     }
   } else {
     // If the node is a disjunction, we construct a clause and assert it
@@ -533,11 +549,11 @@ void TseitinCnfStream::convertAndAssertAnd(TNode node, bool negated, ProofRule p
       clause[i] = toCNF(*disjunct, true);
     }
     Assert(disjunct == node.end());
-    assertClause(node.negate(), clause, proof_id);
+    assertClause(node.negate(), clause);
   }
 }
 
-void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated, ProofRule proof_id) {
+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
@@ -549,18 +565,18 @@ void TseitinCnfStream::convertAndAssertOr(TNode node, bool negated, ProofRule pr
       clause[i] = toCNF(*disjunct, false);
     }
     Assert(disjunct == node.end());
-    assertClause(node, clause, proof_id);
+    assertClause(node, clause);
   } else {
     // 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 ) {
-      PROOF(ProofManager::currentPM()->setCnfDep( (*conjunct).negate().toExpr(), node.negate().toExpr() ) );
-      convertAndAssert(*conjunct, true, proof_id);
+      PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence((*conjunct).negate(), node.negate()););
+      convertAndAssert(*conjunct, true);
     }
   }
 }
 
-void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated, ProofRule proof_id) {
+void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated) {
   if (!negated) {
     // p XOR q
     SatLiteral p = toCNF(node[0], false);
@@ -569,11 +585,11 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated, ProofRule p
     SatClause clause1(2);
     clause1[0] = ~p;
     clause1[1] = ~q;
-    assertClause(node, clause1, proof_id);
+    assertClause(node, clause1);
     SatClause clause2(2);
     clause2[0] = p;
     clause2[1] = q;
-    assertClause(node, clause2, proof_id);
+    assertClause(node, clause2);
   } else {
     // !(p XOR q) is the same as p <=> q
     SatLiteral p = toCNF(node[0], false);
@@ -582,15 +598,15 @@ void TseitinCnfStream::convertAndAssertXor(TNode node, bool negated, ProofRule p
     SatClause clause1(2);
     clause1[0] = ~p;
     clause1[1] = q;
-    assertClause(node.negate(), clause1, proof_id);
+    assertClause(node.negate(), clause1);
     SatClause clause2(2);
     clause2[0] = p;
     clause2[1] = ~q;
-    assertClause(node.negate(), clause2, proof_id);
+    assertClause(node.negate(), clause2);
   }
 }
 
-void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated, ProofRule proof_id) {
+void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated) {
   if (!negated) {
     // p <=> q
     SatLiteral p = toCNF(node[0], false);
@@ -599,11 +615,11 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated, ProofRule p
     SatClause clause1(2);
     clause1[0] = ~p;
     clause1[1] = q;
-    assertClause(node, clause1, proof_id);
+    assertClause(node, clause1);
     SatClause clause2(2);
     clause2[0] = p;
     clause2[1] = ~q;
-    assertClause(node, clause2, proof_id);
+    assertClause(node, clause2);
   } else {
     // !(p <=> q) is the same as p XOR q
     SatLiteral p = toCNF(node[0], false);
@@ -612,15 +628,15 @@ void TseitinCnfStream::convertAndAssertIff(TNode node, bool negated, ProofRule p
     SatClause clause1(2);
     clause1[0] = ~p;
     clause1[1] = ~q;
-    assertClause(node.negate(), clause1, proof_id);
+    assertClause(node.negate(), clause1);
     SatClause clause2(2);
     clause2[0] = p;
     clause2[1] = q;
-    assertClause(node.negate(), clause2, proof_id);
+    assertClause(node.negate(), clause2);
   }
 }
 
-void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated, ProofRule proof_id) {
+void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated) {
   if (!negated) {
     // p => q
     SatLiteral p = toCNF(node[0], false);
@@ -629,17 +645,17 @@ void TseitinCnfStream::convertAndAssertImplies(TNode node, bool negated, ProofRu
     SatClause clause(2);
     clause[0] = ~p;
     clause[1] = q;
-    assertClause(node, clause, proof_id);
+    assertClause(node, clause);
   } else {// Construct the
-    PROOF(ProofManager::currentPM()->setCnfDep( node[0].toExpr(), node.negate().toExpr() ) );
-    PROOF(ProofManager::currentPM()->setCnfDep( node[1].negate().toExpr(), node.negate().toExpr() ) );
+    PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence(node[0], node.negate()););
+    PROOF(if (d_cnfProof) d_cnfProof->setCnfDependence(node[1].negate(), node.negate()););
     // !(p => q) is the same as (p && ~q)
-    convertAndAssert(node[0], false, proof_id);
-    convertAndAssert(node[1], true, proof_id);
+    convertAndAssert(node[0], false);
+    convertAndAssert(node[1], true);
   }
 }
 
-void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated, ProofRule proof_id) {
+void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) {
   // ITE(p, q, r)
   SatLiteral p = toCNF(node[0], false);
   SatLiteral q = toCNF(node[1], negated);
@@ -653,35 +669,47 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated, ProofRule p
   SatClause clause1(2);
   clause1[0] = ~p;
   clause1[1] = q;
-  assertClause(nnode, clause1, proof_id);
+  assertClause(nnode, clause1);
   SatClause clause2(2);
   clause2[0] = p;
   clause2[1] = r;
-  assertClause(nnode, clause2, proof_id);
+  assertClause(nnode, clause2);
 }
 
 // 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 removable, bool negated, ProofRule proof_id, TNode from) {
-  Debug("cnf") << "convertAndAssert(" << node << ", removable = " << (removable ? "true" : "false") << ", negated = " << (negated ? "true" : "false") << ")" << endl;
+void TseitinCnfStream::convertAndAssert(TNode node,
+                                        bool removable,
+                                        bool negated,
+                                        ProofRule proof_id,
+                                        TNode from) {
+  Debug("cnf") << "convertAndAssert(" << node
+               << ", removable = " << (removable ? "true" : "false")
+               << ", negated = " << (negated ? "true" : "false") << ")" << endl;
   d_removable = removable;
-  if(options::proof() || options::unsatCores()) {
-    // Encode the assertion ID in the proof_id to store with generated clauses.
-    uint64_t assertionTableIndex = d_assertionTable.size();
-    Assert((uint64_t(proof_id) & 0xffffffff00000000llu) == 0 && (assertionTableIndex & 0xffffffff00000000llu) == 0, "proof_id/table_index collision");
-    d_proofId = assertionTableIndex | (uint64_t(proof_id) << 32);
-    d_assertionTable.push_back(from.isNull() ? node : from);
-    Debug("cores") << "; cnf is " << assertionTableIndex << " asst " << node << "  proof_id " << proof_id << " from " << from << endl;
-  } else {
-    // We aren't producing proofs or unsat cores; use an invalid proof id.
-    d_proofId = uint64_t(-1);
-  }
-  convertAndAssert(node, negated, proof_id);
+  PROOF
+    (if (d_cnfProof) {
+      Node assertion = negated ? node.notNode() : (Node)node;
+      Node from_assertion = negated? from.notNode() : (Node) from;
+
+      if (proof_id != RULE_INVALID) {
+        d_cnfProof->pushCurrentAssertion(from.isNull() ? assertion : from_assertion);
+        d_cnfProof->registerAssertion(from.isNull() ? assertion : from_assertion, proof_id);
+      }
+      else {
+        d_cnfProof->pushCurrentAssertion(assertion);
+        d_cnfProof->registerAssertion(assertion, proof_id);
+      }
+    });
+
+  convertAndAssert(node, negated);
+  PROOF(if (d_cnfProof) d_cnfProof->popCurrentAssertion(); );
 }
 
-void TseitinCnfStream::convertAndAssert(TNode node, bool negated, ProofRule proof_id) {
-  Debug("cnf") << "convertAndAssert(" << node << ", negated = " << (negated ? "true" : "false") << ")" << endl;
+void TseitinCnfStream::convertAndAssert(TNode node, bool negated) {
+  Debug("cnf") << "convertAndAssert(" << node
+               << ", negated = " << (negated ? "true" : "false") << ")" << endl;
 
   if (d_convertAndAssertCounter % ResourceManager::getFrequencyCount() == 0) {
     NodeManager::currentResourceManager()->spendResource(options::cnfStep());
@@ -691,25 +719,25 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated, ProofRule proo
 
   switch(node.getKind()) {
   case AND:
-    convertAndAssertAnd(node, negated, proof_id);
+    convertAndAssertAnd(node, negated);
     break;
   case OR:
-    convertAndAssertOr(node, negated, proof_id);
+    convertAndAssertOr(node, negated);
     break;
   case IFF:
-    convertAndAssertIff(node, negated, proof_id);
+    convertAndAssertIff(node, negated);
     break;
   case XOR:
-    convertAndAssertXor(node, negated, proof_id);
+    convertAndAssertXor(node, negated);
     break;
   case IMPLIES:
-    convertAndAssertImplies(node, negated, proof_id);
+    convertAndAssertImplies(node, negated);
     break;
   case ITE:
-    convertAndAssertIte(node, negated, proof_id);
+    convertAndAssertIte(node, negated);
     break;
   case NOT:
-    convertAndAssert(node[0], !negated, proof_id);
+    convertAndAssert(node[0], !negated);
     break;
   default:
   {
@@ -718,7 +746,7 @@ void TseitinCnfStream::convertAndAssert(TNode node, bool negated, ProofRule proo
       nnode = node.negate();
     }
     // Atoms
-    assertClause(nnode, toCNF(node, negated), proof_id);
+    assertClause(nnode, toCNF(node, negated));
   }
     break;
   }
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index cfab216fe..a07944a58 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -84,8 +84,11 @@ protected:
   /** The "registrar" for pre-registration of terms */
   Registrar* d_registrar;
 
-  /** A table of assertions, used for regenerating proofs. */
-  context::CDList<Node> d_assertionTable;
+  /** The name of this CNF stream*/
+  std::string d_name;
+
+  /** Pointer to the proof corresponding to this CnfStream */
+  CnfProof* d_cnfProof;
 
   /** Container for misc. globals. */
   SmtGlobals* d_globals;
@@ -117,14 +120,6 @@ protected:
   }
 
   /**
-   * A reference into the assertion table, used to map clauses back to
-   * their "original" input assertion/lemma.  This variable is manipulated
-   * by the top-level convertAndAssert().  This is needed in proofs-enabled
-   * runs, to justify where the SAT solver's clauses came from.
-   */
-  uint64_t d_proofId;
-
-  /**
    * Are we asserting a removable clause (true) or a permanent clause (false).
    * This is set at the beginning of convertAndAssert so that it doesn't
    * need to be passed on over the stack.  Only pure clauses can be asserted
@@ -137,14 +132,14 @@ protected:
    * @param node the node giving rise to this clause
    * @param clause the clause to assert
    */
-  void assertClause(TNode node, SatClause& clause, ProofRule proof_id);
+  void assertClause(TNode node, SatClause& clause);
 
   /**
    * Asserts the unit clause to the sat solver.
    * @param node the node giving rise to this clause
    * @param a the unit literal of the clause
    */
-  void assertClause(TNode node, SatLiteral a, ProofRule proof_id);
+  void assertClause(TNode node, SatLiteral a);
 
   /**
    * Asserts the binary clause to the sat solver.
@@ -152,7 +147,7 @@ protected:
    * @param a the first literal in the clause
    * @param b the second literal in the clause
    */
-  void assertClause(TNode node, SatLiteral a, SatLiteral b, ProofRule proof_id);
+  void assertClause(TNode node, SatLiteral a, SatLiteral b);
 
   /**
    * Asserts the ternary clause to the sat solver.
@@ -161,7 +156,7 @@ protected:
    * @param b the second literal in the clause
    * @param c the thirs literal in the clause
    */
-  void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c, ProofRule proof_id);
+  void assertClause(TNode node, SatLiteral a, SatLiteral b, SatLiteral c);
 
   /**
    * Acquires a new variable from the SAT solver to represent the node
@@ -193,9 +188,15 @@ public:
    * @param registrar the entity that takes care of preregistration of Nodes
    * @param context the context that the CNF should respect
    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
+   * @param name string identifier to distinguish between different instances
    * even for non-theory literals
    */
-  CnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, bool fullLitToNodeMap = false);
+  CnfStream(SatSolver* satSolver,
+            Registrar* registrar,
+            context::Context* context,
+            SmtGlobals* globals,
+            bool fullLitToNodeMap = false,
+            std::string name="");
 
   /**
    * Destructs a CnfStream.  This implementation does nothing, but we
@@ -244,13 +245,6 @@ public:
   SatLiteral getLiteral(TNode node);
 
   /**
-   * Get the assertion with a given ID.  (Used for reconstructing proofs.)
-   */
-  TNode getAssertion(uint64_t id) {
-    return d_assertionTable[id];
-  }
-
-  /**
    * Returns the Boolean variables from the input problem.
    */
   void getBooleanVariables(std::vector<TNode>& outputVariables) const;
@@ -263,6 +257,7 @@ public:
     return d_literalToNodeMap;
   }
 
+  void setProof(CnfProof* proof);
 };/* class CnfStream */
 
 
@@ -286,7 +281,8 @@ public:
    * @param removable is this something that can be erased
    * @param negated true if negated
    */
-  void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null());
+  void convertAndAssert(TNode node, bool removable,
+                        bool negated, ProofRule rule, TNode from = TNode::null());
 
   /**
    * Constructs the stream to use the given sat solver.
@@ -295,14 +291,14 @@ public:
    * @param fullLitToNodeMap maintain a full SAT-literal-to-Node mapping,
    * even for non-theory literals
    */
-  TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, bool fullLitToNodeMap = false);
+  TseitinCnfStream(SatSolver* satSolver, Registrar* registrar, context::Context* context, SmtGlobals* globals, bool fullLitToNodeMap = false, std::string name = "");
 
 private:
 
   /**
    * Same as above, except that removable is remembered.
    */
-  void convertAndAssert(TNode node, bool negated, ProofRule proof_id);
+  void convertAndAssert(TNode node, bool negated);
 
   // Each of these formulas handles takes care of a Node of each Kind.
   //
@@ -322,12 +318,12 @@ private:
   SatLiteral handleAnd(TNode node);
   SatLiteral handleOr(TNode node);
 
-  void convertAndAssertAnd(TNode node, bool negated, ProofRule proof_id);
-  void convertAndAssertOr(TNode node, bool negated, ProofRule proof_id);
-  void convertAndAssertXor(TNode node, bool negated, ProofRule proof_id);
-  void convertAndAssertIff(TNode node, bool negated, ProofRule proof_id);
-  void convertAndAssertImplies(TNode node, bool negated, ProofRule proof_id);
-  void convertAndAssertIte(TNode node, bool negated, ProofRule proof_id);
+  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 4c431a9b1..f4489c4be 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -25,6 +25,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "base/output.h"
 #include "options/prop_options.h"
 #include "proof/proof_manager.h"
+#include "proof/sat_proof_implementation.h"
 #include "proof/sat_proof.h"
 #include "prop/minisat/core/Solver.h"
 #include "prop/minisat/minisat.h"
@@ -32,6 +33,7 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "prop/theory_proxy.h"
 #include "smt_util/command.h"
 
+
 using namespace CVC4::prop;
 
 namespace CVC4 {
@@ -40,7 +42,6 @@ namespace Minisat {
 //=================================================================================================
 // Options:
 
-
 static const char* _cat = "CORE";
 
 static DoubleOption  opt_var_decay         (_cat, "var-decay",   "The variable activity decay factor",            0.95,     DoubleRange(0, false, 1, false));
@@ -55,6 +56,10 @@ static IntOption     opt_restart_first     (_cat, "rfirst",      "The base resta
 static DoubleOption  opt_restart_inc       (_cat, "rinc",        "Restart interval increase factor", 3, DoubleRange(1, false, HUGE_VAL, false));
 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));
 
+//=================================================================================================
+// Proof declarations
+CRef Solver::TCRef_Undef = CRef_Undef;
+CRef Solver::TCRef_Lazy = CRef_Lazy;
 
 class ScopedBool {
   bool& watch;
@@ -135,8 +140,12 @@ Solver::Solver(CVC4::prop::TheoryProxy* proxy, CVC4::context::Context* context,
   // Assert the constants
   uncheckedEnqueue(mkLit(varTrue, false));
   uncheckedEnqueue(mkLit(varFalse, true));
-  PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), INPUT, uint64_t(-1)); )
-  PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT, uint64_t(-1)); )
+  // FIXME: these should be axioms I believe
+  PROOF
+    (
+     ProofManager::getSatProof()->registerTrueLit(mkLit(varTrue, false));
+     ProofManager::getSatProof()->registerFalseLit(mkLit(varFalse, true));
+     );
 }
 
 
@@ -217,7 +226,9 @@ CRef Solver::reason(Var x) {
 
     // Get the explanation from the theory
     SatClause explanation_cl;
-    proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l), explanation_cl);
+    // FIXME: at some point return a tag with the theory that spawned you
+    proxy->explainPropagation(MinisatSatSolver::toSatLiteral(l),
+                              explanation_cl);
     vec<Lit> explanation;
     MinisatSatSolver::toMinisatClause(explanation_cl, explanation); 
 
@@ -263,7 +274,12 @@ CRef Solver::reason(Var x) {
 
     // Construct the reason
     CRef real_reason = ca.alloc(explLevel, explanation, true);
-    PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA, (uint64_t(RULE_CONFLICT) << 32)); );
+    // FIXME: at some point will need more information about where this explanation
+    // came from (ie. the theory/sharing)
+    PROOF (ClauseId id = ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA);
+           ProofManager::getCnfProof()->registerConvertedClause(id, true);
+           // no need to pop current assertion as this is not converted to cnf
+           );
     vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x));
     clauses_removable.push(real_reason);
     attachClause(real_reason);
@@ -271,7 +287,7 @@ CRef Solver::reason(Var x) {
     return real_reason;
 }
 
-bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
+bool Solver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 {
     if (!ok) return false;
 
@@ -289,11 +305,13 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
       clauseLevel = std::max(clauseLevel, intro_level(var(ps[i])));
       // Tautologies are ignored
       if (ps[i] == ~p) {
+        id = ClauseIdUndef;
         // Clause can be ignored
         return true;
       }
       // Clauses with 0-level true literals are also ignored
       if (value(ps[i]) == l_True && level(var(ps[i])) == 0 && user_level(var(ps[i])) == 0) {
+        id = ClauseIdUndef;
         return true;
       }
       // Ignore repeated literals
@@ -321,8 +339,19 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
       lemmas.push();
       ps.copyTo(lemmas.last());
       lemmas_removable.push(removable);
-      Debug("cores") << "lemma push " << proof_id << " " << (proof_id & 0xffffffff) << std::endl;
-      lemmas_proof_id.push(proof_id);
+      PROOF(
+            // Store the expression being converted to CNF until
+            // the clause is actually created
+            Node assertion = ProofManager::getCnfProof()->getCurrentAssertion();
+            Node def = ProofManager::getCnfProof()->getCurrentDefinition();
+            lemmas_cnf_assertion.push_back(std::make_pair(assertion, def));
+            id = ClauseIdUndef;
+        );
+      // does it have to always be a lemma?
+      // PROOF(id = ProofManager::getSatProof()->registerUnitClause(ps[0], THEORY_LEMMA););
+      // PROOF(id = ProofManager::getSatProof()->registerTheoryLemma(ps););
+      // Debug("cores") << "lemma push " << proof_id << " " << (proof_id & 0xffffffff) << std::endl;
+      // lemmas_proof_id.push(proof_id);
     } else {
       // If all false, we're in conflict
       if (ps.size() == falseLiteralsCount) {
@@ -331,7 +360,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
           // construct the clause below to give to the proof manager
           // as the final conflict.
           if(falseLiteralsCount == 1) {
-            PROOF( ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT, proof_id); )
+            PROOF( id = ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT); )
             PROOF( ProofManager::getSatProof()->finalizeProof(CVC4::Minisat::CRef_Lazy); )
             return ok = false;
           }
@@ -353,7 +382,9 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
 	attachClause(cr);
 
         if(PROOF_ON()) {
-          PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT, proof_id); )
+          PROOF(
+                id = ProofManager::getSatProof()->registerClause(cr, INPUT);
+                )
           if(ps.size() == falseLiteralsCount) {
             PROOF( ProofManager::getSatProof()->finalizeProof(cr); )
             return ok = false;
@@ -366,12 +397,16 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
         if(assigns[var(ps[0])] == l_Undef) {
           assert(assigns[var(ps[0])] != l_False);
           uncheckedEnqueue(ps[0], cr);
-          Debug("cores") << "i'm registering a unit clause, input, proof id " << proof_id << std::endl;
-          PROOF( if(ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT, proof_id); } );
+          Debug("cores") << "i'm registering a unit clause, input" << std::endl;
+          PROOF(
+                if(ps.size() == 1) {
+                  id = ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT);
+                }
+                );
           CRef confl = propagate(CHECK_WITHOUT_THEORY);
           if(! (ok = (confl == CRef_Undef)) ) {
             if(ca[confl].size() == 1) {
-              PROOF( ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT, proof_id); );
+              PROOF( id = ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT); );
               PROOF( ProofManager::getSatProof()->finalizeProof(CVC4::Minisat::CRef_Lazy); )
             } else {
               PROOF( ProofManager::getSatProof()->finalizeProof(confl); );
@@ -604,7 +639,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
         for (int j = (p == lit_Undef) ? 0 : 1; j < c.size(); j++){
             Lit q = c[j];
 
-            if (!seen[var(q)] && level(var(q)) > 0){
+            if (!seen[var(q)] && level(var(q)) > 0) {
                 varBumpActivity(var(q));
                 seen[var(q)] = 1;
                 if (level(var(q)) >= decisionLevel())
@@ -646,7 +681,7 @@ int Solver::analyze(CRef confl, vec<Lit>& out_learnt, int& out_btlevel)
         uint32_t abstract_level = 0;
         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) {
                 out_learnt[j++] = out_learnt[i];
@@ -901,7 +936,8 @@ void Solver::propagateTheory() {
         proxy->explainPropagation(MinisatSatSolver::toSatLiteral(p), explanation_cl);
         vec<Lit> explanation;
         MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
-        addClause(explanation, true, 0);
+        ClauseId id; // FIXME: mark it as explanation here somehow?
+        addClause(explanation, true, id);
       }
     }
   }
@@ -1159,8 +1195,17 @@ lbool Solver::search(int nof_conflicts)
                 attachClause(cr);
                 claBumpActivity(ca[cr]);
                 uncheckedEnqueue(learnt_clause[0], cr);
-
-                PROOF( ProofManager::getSatProof()->endResChain(cr); )
+                PROOF(
+                      ClauseId id = ProofManager::getSatProof()->registerClause(cr, LEARNT);
+                      PSTATS(
+                      __gnu_cxx::hash_set<int> cl_levels;
+                      for (int i = 0; i < learnt_clause.size(); ++i) {
+                        cl_levels.insert(level(var(learnt_clause[i])));
+                      }
+                      ProofManager::getSatProof()->storeClauseGlue(id, cl_levels.size());
+                            )
+                      ProofManager::getSatProof()->endResChain(id);
+                      );
             }
 
             varDecayActivity();
@@ -1650,14 +1695,14 @@ CRef Solver::updateLemmas() {
   // Last index in the trail
   int backtrack_index = trail.size();
 
+  PROOF(Assert (lemmas.size() == (int)lemmas_cnf_assertion.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];
-    uint64_t proof_id = lemmas_proof_id[i];
-    Debug("cores") << "pulled lemma proof id " << proof_id << " " << (proof_id & 0xffffffff) << std::endl;
 
     // Attach it if non-unit
     CRef lemma_ref = CRef_Undef;
@@ -1672,7 +1717,15 @@ CRef Solver::updateLemmas() {
       }
 
       lemma_ref = ca.alloc(clauseLevel, lemma, removable);
-      PROOF( ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA, proof_id); );
+      PROOF
+        (
+         TNode cnf_assertion = lemmas_cnf_assertion[i].first;
+         TNode cnf_def = lemmas_cnf_assertion[i].second;
+
+         ClauseId id = ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA);
+         ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
+         ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
+         );
       if (removable) {
         clauses_removable.push(lemma_ref);
       } else {
@@ -1680,7 +1733,15 @@ CRef Solver::updateLemmas() {
       }
       attachClause(lemma_ref);
     } else {
-      PROOF( ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA, proof_id); );
+      PROOF
+        (
+         Node cnf_assertion = lemmas_cnf_assertion[i].first;
+         Node cnf_def = lemmas_cnf_assertion[i].second;
+         
+         ClauseId id = ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA);
+         ProofManager::getCnfProof()->setClauseAssertion(id, cnf_assertion);
+         ProofManager::getCnfProof()->setClauseDefinition(id, cnf_def);
+         );
     }
 
     // If the lemma is propagating enqueue its literal (or set the conflict)
@@ -1694,7 +1755,7 @@ CRef Solver::updateLemmas() {
           } else {
             Debug("minisat::lemmas") << "Solver::updateLemmas(): unit conflict or empty clause" << std::endl;
             conflict = CRef_Lazy;
-            PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT, proof_id); );
+            PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT); );
           }
         } else {
           Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;
@@ -1704,10 +1765,11 @@ CRef Solver::updateLemmas() {
     }
   }
 
+  PROOF(Assert (lemmas.size() == (int)lemmas_cnf_assertion.size()););
   // Clear the lemmas
   lemmas.clear();
+  lemmas_cnf_assertion.clear();
   lemmas_removable.clear();
-  lemmas_proof_id.clear();
 
   if (conflict != CRef_Undef) {
     theoryConflict = true;
@@ -1718,6 +1780,28 @@ CRef Solver::updateLemmas() {
   return conflict;
 }
 
+void ClauseAllocator::reloc(CRef& cr, ClauseAllocator& to, CVC4::CoreProofProxy* proxy)
+{
+ 
+  // FIXME what is this CRef_lazy
+  if (cr == CRef_Lazy) return;
+  
+  CRef old = cr;  // save the old reference
+  Clause& c = operator[](cr);
+  if (c.reloced()) { cr = c.relocation(); return; }
+  
+  cr = to.alloc(c.level(), c, c.removable());
+  c.relocate(cr);
+  if (proxy) {
+    proxy->updateCRef(old, 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].removable())         to[cr].activity() = c.activity();
+  else if (to[cr].has_extra()) to[cr].calcAbstraction();
+}
+
 inline bool Solver::withinBudget(uint64_t ammount) const {
   Assert (proxy);
   // spendResource sets async_interrupt or throws UnsafeInterruptException
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 3be6b1b22..a239eba72 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -37,13 +37,15 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 
 
 namespace CVC4 {
-  class SatProof;
+template <class Solver> class TSatProof;
 
-  namespace prop {
-    class TheoryProxy;
-  }/* CVC4::prop namespace */
+namespace prop {
+  class TheoryProxy;
+}/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
+typedef unsigned ClauseId;
+
 namespace CVC4 {
 namespace Minisat {
 
@@ -54,7 +56,18 @@ class Solver {
 
   /** The only two CVC4 entry points to the private solver data */
   friend class CVC4::prop::TheoryProxy;
-  friend class CVC4::SatProof;
+  friend class CVC4::TSatProof<Minisat::Solver>;
+
+public:
+  static CRef TCRef_Undef;
+  static CRef TCRef_Lazy;
+
+  typedef Var TVar;
+  typedef Lit TLit;
+  typedef Clause TClause; 
+  typedef CRef TCRef;
+  typedef vec<Lit> TLitVec;
+  
 protected:
 
   /** The pointer to the proxy that provides interfaces to the SMT engine */
@@ -85,8 +98,8 @@ protected:
   /** Is the lemma removable */
   vec<bool> lemmas_removable;
 
-  /** Proof IDs for lemmas */
-  vec<uint64_t> lemmas_proof_id;
+  /** Nodes being converted to CNF */
+  std::vector< std::pair<CVC4::Node, CVC4::Node > >lemmas_cnf_assertion;
 
   /** Do a another check if FULL_EFFORT was the last one */
   bool recheck;
@@ -157,14 +170,14 @@ public:
     void          push                     ();
     void          pop                      ();
 
-    // CVC4 adds the "proof_id" here to refer to the input assertion/lemma
-    // that produced this clause
-    bool    addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id);  // Add a clause to the solver.
-    bool    addEmptyClause(bool removable);                                     // Add the empty clause, making the solver contradictory.
-    bool    addClause (Lit p, bool removable, uint64_t proof_id);               // Add a unit clause to the solver.
-    bool    addClause (Lit p, Lit q, bool removable, uint64_t proof_id);        // Add a binary clause to the solver.
-    bool    addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id); // Add a ternary clause to the solver.
-    bool    addClause_(      vec<Lit>& ps, bool removable, uint64_t proof_id);  // Add a clause to the solver without making superflous internal copy. Will
+    // addClause returns the ClauseId corresponding to the clause added in the
+    // reference parameter id.
+    bool    addClause (const vec<Lit>& ps, bool removable, ClauseId& id);  // Add a clause to the solver.
+    bool    addEmptyClause(bool removable);                                // Add the empty clause, making the solver contradictory.
+    bool    addClause (Lit p, bool removable, ClauseId& id);               // Add a unit clause to the solver.
+    bool    addClause (Lit p, Lit q, bool removable, ClauseId& id);        // Add a binary clause to the solver.
+    bool    addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id); // Add a ternary clause to the solver.
+    bool    addClause_(      vec<Lit>& ps, bool removable, ClauseId& id);  // Add a clause to the solver without making superflous internal copy. Will
                                                                                  // change the passed vector 'ps'.
 
     // Solving:
@@ -495,15 +508,15 @@ 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, bool removable, uint64_t proof_id)
-                                                                { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, proof_id); }
-inline bool     Solver::addEmptyClause  (bool removable)        { add_tmp.clear(); return addClause_(add_tmp, removable, uint64_t(-1)); }
-inline bool     Solver::addClause       (Lit p, bool removable, uint64_t proof_id)
-                                                                { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, proof_id); }
-inline bool     Solver::addClause       (Lit p, Lit q, bool removable, uint64_t proof_id)
-                                                                { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, proof_id); }
-inline bool     Solver::addClause       (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id)
-                                                                { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, proof_id); }
+inline bool     Solver::addClause       (const vec<Lit>& ps, bool removable, ClauseId& id)
+                                                                { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, id); }
+inline bool     Solver::addEmptyClause  (bool removable)        { add_tmp.clear(); ClauseId tmp; return addClause_(add_tmp, removable, tmp); }
+inline bool     Solver::addClause       (Lit p, bool removable, ClauseId& id)
+                                                                { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, id); }
+inline bool     Solver::addClause       (Lit p, Lit q, bool removable, ClauseId& id)
+                                                                { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, id); }
+inline bool     Solver::addClause       (Lit p, Lit q, Lit r, bool removable, ClauseId& id)
+                                                                { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, id); }
 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()); flipped.push(false); context->push(); if(Dump.isOn("state")) { Dump("state") << CVC4::PushCommand(); } }
 
diff --git a/src/prop/minisat/core/SolverTypes.h b/src/prop/minisat/core/SolverTypes.h
index b0d78242c..116a39a49 100644
--- a/src/prop/minisat/core/SolverTypes.h
+++ b/src/prop/minisat/core/SolverTypes.h
@@ -169,20 +169,22 @@ inline std::ostream& operator <<(std::ostream& out, Minisat::lbool val) {
 }
 
 
-} /* Minisat */
-}
-
+class Solver;
 
-
-namespace CVC4 {
 class ProofProxyAbstract {
 public:
   virtual ~ProofProxyAbstract() {}
   virtual void updateCRef(Minisat::CRef oldref, Minisat::CRef newref) = 0; 
 };
-}
+
+} /* namespace CVC4::Minisat */
+} /* namespace CVC4 */
 
 
+namespace CVC4 {
+template <class Solver> class ProofProxy;
+typedef ProofProxy<CVC4::Minisat::Solver> CoreProofProxy;
+} 
 
 namespace CVC4 {
 namespace Minisat{
@@ -305,27 +307,8 @@ class ClauseAllocator : public RegionAllocator<uint32_t>
         RegionAllocator<uint32_t>::free(clauseWord32Size(c.size(), c.has_extra()));
     }
 
-  void reloc(CRef& cr, ClauseAllocator& to, CVC4::ProofProxyAbstract* proxy = NULL)
-    {
-
-        // FIXME what is this CRef_lazy
-        if (cr == CRef_Lazy) return;
-
-        CRef old = cr;  // save the old reference
-        Clause& c = operator[](cr);
-        if (c.reloced()) { cr = c.relocation(); return; }
-        
-        cr = to.alloc(c.level(), c, c.removable());
-        c.relocate(cr);
-        if (proxy) {
-          proxy->updateCRef(old, 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].removable())         to[cr].activity() = c.activity();
-        else if (to[cr].has_extra()) to[cr].calcAbstraction();
-    }
+  void reloc(CRef& cr, ClauseAllocator& to, CVC4::CoreProofProxy* proxy = NULL);
+  // Implementation moved to Solver.cc.
 };
 
 
diff --git a/src/prop/minisat/minisat.cpp b/src/prop/minisat/minisat.cpp
index ce5c1eb92..739d9087a 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -23,6 +23,7 @@
 #include "options/prop_options.h"
 #include "options/smt_options.h"
 #include "prop/minisat/simp/SimpSolver.h"
+#include "proof/sat_proof.h"
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
@@ -94,14 +95,6 @@ void MinisatSatSolver::toMinisatClause(SatClause& clause,
   Assert(clause.size() == (unsigned)minisat_clause.size());
 }
 
-void MinisatSatSolver::toSatClause(Minisat::vec<Minisat::Lit>& clause,
-                                       SatClause& sat_clause) {
-  for (int i = 0; i < clause.size(); ++i) {
-    sat_clause.push_back(toSatLiteral(clause[i]));
-  }
-  Assert((unsigned)clause.size() == sat_clause.size());
-}
-
 void MinisatSatSolver::toSatClause(const Minisat::Clause& clause,
                                        SatClause& sat_clause) {
   for (int i = 0; i < clause.size(); ++i) {
@@ -149,10 +142,18 @@ void MinisatSatSolver::setupOptions() {
   d_minisat->restart_inc = options::satRestartInc();
 }
 
-void MinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) {
+ClauseId MinisatSatSolver::addClause(SatClause& clause, bool removable) {
   Minisat::vec<Minisat::Lit> minisat_clause;
   toMinisatClause(clause, minisat_clause);
-  d_minisat->addClause(minisat_clause, removable, proof_id);
+  ClauseId clause_id = ClauseIdError;
+  // FIXME: This relies on the invariant that when ok() is false
+  // the SAT solver does not add the clause (which is what Minisat currently does)
+  if (!ok()) {
+    return ClauseIdUndef; 
+  }
+  d_minisat->addClause(minisat_clause, removable, clause_id);
+  PROOF( Assert (clause_id != ClauseIdError););
+  return clause_id;
 }
 
 SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) {
@@ -182,6 +183,9 @@ SatValue MinisatSatSolver::solve() {
   return toSatLiteralValue(d_minisat->solve());
 }
 
+bool MinisatSatSolver::ok() const {
+  return d_minisat->okay(); 
+}
 
 void MinisatSatSolver::interrupt() {
   d_minisat->interrupt();
@@ -280,3 +284,20 @@ void MinisatSatSolver::Statistics::init(Minisat::SimpSolver* d_minisat){
 
 } /* namespace CVC4::prop */
 } /* namespace CVC4 */
+
+
+namespace CVC4 {
+template<>
+prop::SatLiteral toSatLiteral< CVC4::Minisat::Solver>(Minisat::Solver::TLit lit) {
+  return prop::MinisatSatSolver::toSatLiteral(lit);
+} 
+
+template<>
+void toSatClause< CVC4::Minisat::Solver> (const CVC4::Minisat::Solver::TClause& minisat_cl,
+                                      prop::SatClause& sat_cl) {
+  prop::MinisatSatSolver::toSatClause(minisat_cl, sat_cl);
+}
+
+} /* namespace CVC4 */
+
+
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index f279b3a5b..535ce1a47 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -40,11 +40,10 @@ public:
   //(Commented because not in use) static bool            tobool(SatValue val);
 
   static void  toMinisatClause(SatClause& clause, Minisat::vec<Minisat::Lit>& minisat_clause);
-  static void  toSatClause    (Minisat::vec<Minisat::Lit>& clause, SatClause& sat_clause);
   static void  toSatClause    (const Minisat::Clause& clause, SatClause& sat_clause);
   void initialize(context::Context* context, TheoryProxy* theoryProxy);
 
-  void addClause(SatClause& clause, bool removable, uint64_t proof_id);
+  ClauseId addClause(SatClause& clause, bool removable);
 
   SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase);
   SatVariable trueVar() { return d_minisat->trueVar(); }
@@ -53,6 +52,8 @@ public:
   SatValue solve();
   SatValue solve(long unsigned int&);
 
+  bool ok() const;
+  
   void interrupt();
 
   SatValue value(SatLiteral l);
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 235c97e8f..5bdaea950 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -160,7 +160,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
 
 
 
-bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
+bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, ClauseId& id)
 {
 #ifndef NDEBUG
     if (use_simplification) {
@@ -174,7 +174,7 @@ bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
     if (use_rcheck && implied(ps))
         return true;
 
-    if (!Solver::addClause_(ps, removable, proof_id))
+    if (!Solver::addClause_(ps, removable, id))
         return false;
 
     if (use_simplification && clauses_persistent.size() == nclauses + 1){
@@ -541,12 +541,14 @@ bool SimpSolver::eliminateVar(Var v)
     for (int i = 0; i < cls.size(); i++)
         removeClause(cls[i]); 
 
+    ClauseId id = ClauseIdUndef; 
     // 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++) {
             bool removable = ca[pos[i]].removable() && ca[pos[neg[j]]].removable();
-            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable, uint64_t(-1))) {
+            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) &&
+                !addClause_(resolvent, removable, id)) {
                 return false;
             }
         }
@@ -585,8 +587,8 @@ bool SimpSolver::substitute(Var v, Lit x)
         }
 
         removeClause(cls[i]);
-
-        if (!addClause_(subst_clause, c.removable(), uint64_t(-1))) {
+        ClauseId id = ClauseIdUndef;
+        if (!addClause_(subst_clause, c.removable(), id)) {
             return ok = false;
         }
     }
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 0c5062726..a19bec1ef 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -48,12 +48,12 @@ class SimpSolver : public Solver {
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true, bool isTheoryAtom = false, bool preRegister = false, bool canErase = true);
-    bool    addClause (const vec<Lit>& ps, bool removable, uint64_t proof_id);
-    bool    addEmptyClause(bool removable, uint64_t proof_id); // Add the empty clause to the solver.
-    bool    addClause (Lit p, bool removable, uint64_t proof_id); // Add a unit clause to the solver.
-    bool    addClause (Lit p, Lit q, bool removable, uint64_t proof_id); // Add a binary clause to the solver.
-    bool    addClause (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id); // Add a ternary clause to the solver.
-    bool    addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id);
+    bool    addClause (const vec<Lit>& ps, bool removable, ClauseId& id);
+    bool    addEmptyClause(bool removable); // Add the empty clause to the solver.
+    bool    addClause (Lit p, bool removable, ClauseId& id); // Add a unit clause to the solver.
+    bool    addClause (Lit p, Lit q, bool removable, ClauseId& id); // Add a binary clause to the solver.
+    bool    addClause (Lit p, Lit q, Lit r, bool removable, ClauseId& id); // Add a ternary clause to the solver.
+    bool    addClause_(vec<Lit>& ps, bool removable, ClauseId& id);
     bool    substitute(Var v, Lit x);  // Replace all occurences of v with x (may cause a contradiction).
 
     // Variable mode:
@@ -183,15 +183,15 @@ inline void SimpSolver::updateElimHeap(Var v) {
         elim_heap.update(v); }
 
 
-inline bool SimpSolver::addClause    (const vec<Lit>& ps, bool removable, uint64_t proof_id)
-                                                                             { ps.copyTo(add_tmp); return addClause_(add_tmp, removable, proof_id); }
-inline bool SimpSolver::addEmptyClause(bool removable, uint64_t proof_id)    { add_tmp.clear(); return addClause_(add_tmp, removable, proof_id); }
-inline bool SimpSolver::addClause    (Lit p, bool removable, uint64_t proof_id)
-                                                                             { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, proof_id); }
-inline bool SimpSolver::addClause    (Lit p, Lit q, bool removable, uint64_t proof_id)
-                                                                             { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, proof_id); }
-inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r, bool removable, uint64_t proof_id)
-                                                                             { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, proof_id); }
+inline bool SimpSolver::addClause(const vec<Lit>& ps, bool removable, ClauseId& id)
+{ ps.copyTo(add_tmp); return addClause_(add_tmp, removable, id); }
+inline bool SimpSolver::addEmptyClause(bool removable)    { add_tmp.clear(); ClauseId id=-1; return addClause_(add_tmp, removable, id); }
+inline bool SimpSolver::addClause    (Lit p, bool removable, ClauseId& id)
+                                                                             { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable, id); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, bool removable, ClauseId& id)
+                                                                             { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable, id); }
+inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r, bool removable, ClauseId& id)
+                                                                             { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable, id); }
 inline void SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
 
 // the solver can always return unknown due to resource limiting
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 9767ac7c7..593c522a8 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -99,7 +99,9 @@ PropEngine::PropEngine(TheoryEngine* te, DecisionEngine *de, Context* satContext
 
   d_decisionEngine->setSatSolver(d_satSolver);
   d_decisionEngine->setCnfStream(d_cnfStream);
-  PROOF (ProofManager::currentPM()->initCnfProof(d_cnfStream); );
+  PROOF (
+         ProofManager::currentPM()->initCnfProof(d_cnfStream, userContext);
+         );
 }
 
 PropEngine::~PropEngine() {
@@ -117,7 +119,10 @@ void PropEngine::assertFormula(TNode node) {
   d_cnfStream->convertAndAssert(node, false, false, RULE_GIVEN);
 }
 
-void PropEngine::assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from) {
+void PropEngine::assertLemma(TNode node, bool negated,
+                             bool removable,
+                             ProofRule rule,
+                             TNode from) {
   //Assert(d_inCheckSat, "Sat solver should be in solve()!");
   Debug("prop::lemmas") << "assertLemma(" << node << ")" << endl;
 
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 1c1dae410..1383308a3 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -30,10 +30,15 @@
 #include "util/statistics_registry.h"
 
 namespace CVC4 {
+  
+class BitVectorProof;
+
 namespace prop {
 
 class TheoryProxy;
 
+typedef unsigned ClauseId;
+
 class SatSolver {
 
 public:
@@ -42,7 +47,8 @@ public:
   virtual ~SatSolver() throw(AssertionException) { }
 
   /** Assert a clause in the solver. */
-  virtual void addClause(SatClause& clause, bool removable, uint64_t proof_id) = 0;
+  virtual ClauseId addClause(SatClause& clause,
+                             bool removable) = 0;
 
   /**
    * Create a new boolean variable in the solver.
@@ -77,6 +83,10 @@ public:
   /** Get the current assertion level */
   virtual unsigned getAssertionLevel() const = 0;
 
+  /** Check if the solver is in an inconsistent state */
+  virtual bool ok() const = 0;
+
+  
 };/* class SatSolver */
 
 
@@ -121,6 +131,10 @@ public:
 
   virtual void popAssumption() = 0;
 
+  virtual bool ok() const = 0;
+  
+  virtual void setProofLog( BitVectorProof * bvp ) {}
+
 };/* class BVSatSolverInterface */
 
 
@@ -139,7 +153,8 @@ public:
   virtual bool flipDecision() = 0;
 
   virtual bool isDecision(SatVariable decn) const = 0;
-
+  
+  virtual bool ok() const = 0;
 };/* class DPLLSatSolverInterface */
 
 inline std::ostream& operator <<(std::ostream& out, prop::SatLiteral lit) {
diff --git a/src/prop/sat_solver_factory.h b/src/prop/sat_solver_factory.h
index 434bf849d..6a3053a18 100644
--- a/src/prop/sat_solver_factory.h
+++ b/src/prop/sat_solver_factory.h
@@ -31,7 +31,9 @@ namespace prop {
 class SatSolverFactory {
 public:
 
-  static BVSatSolverInterface* createMinisat(context::Context* mainSatContext, StatisticsRegistry* registry, const std::string& name = "");
+  static BVSatSolverInterface* createMinisat(context::Context* mainSatContext,
+                                             StatisticsRegistry* registry,
+                                             const std::string& name = "");
   static DPLLSatSolverInterface* createDPLLMinisat(StatisticsRegistry* registry);
 
 };/* class SatSolverFactory */
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index e87046ad5..5304691a6 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -22,6 +22,7 @@
 #include "options/decision_options.h"
 #include "prop/cnf_stream.h"
 #include "prop/prop_engine.h"
+#include "proof/cnf_proof.h"
 #include "smt_util/lemma_input_channel.h"
 #include "smt_util/lemma_output_channel.h"
 #include "smt/smt_statistics_registry.h"
@@ -29,6 +30,7 @@
 #include "theory/theory_engine.h"
 #include "util/statistics_registry.h"
 
+
 namespace CVC4 {
 namespace prop {
 
@@ -100,6 +102,7 @@ void TheoryProxy::explainPropagation(SatLiteral l, SatClause& explanation) {
   TNode lNode = d_cnfStream->getNode(l);
   Debug("prop-explain") << "explainPropagation(" << lNode << ")" << std::endl;
   Node theoryExplanation = d_theoryEngine->getExplanation(lNode);
+  PROOF(ProofManager::getCnfProof()->pushCurrentAssertion(theoryExplanation); );
   Debug("prop-explain") << "explainPropagation() => " <<  theoryExplanation << std::endl;
   if (theoryExplanation.getKind() == kind::AND) {
     Node::const_iterator it = theoryExplanation.begin();