Unsat core infrastruture and API (SMT-LIB compliance to come).

46 files changed, 976 insertions, 555 deletions

diff --git a/NEWS b/NEWS
index 64ded5339..2589fda87 100644
--- a/NEWS
+++ b/NEWS
@@ -3,7 +3,8 @@ This file contains a summary of important user-visible changes.
 Changes since 1.4
 =================
 
-* nothing yet
+* Support for unsat cores.
+* Simplification mode "incremental" no longer supported.
 
 Changes since 1.3
 =================
diff --git a/src/expr/command.cpp b/src/expr/command.cpp
index 33be85d11..a07076281 100644
--- a/src/expr/command.cpp
+++ b/src/expr/command.cpp
@@ -189,8 +189,8 @@ std::string EchoCommand::getCommandName() const throw() {
 
 /* class AssertCommand */
 
-AssertCommand::AssertCommand(const Expr& e) throw() :
-  d_expr(e) {
+AssertCommand::AssertCommand(const Expr& e, bool inUnsatCore) throw() :
+  d_expr(e), d_inUnsatCore(inUnsatCore) {
 }
 
 Expr AssertCommand::getExpr() const throw() {
@@ -199,7 +199,7 @@ Expr AssertCommand::getExpr() const throw() {
 
 void AssertCommand::invoke(SmtEngine* smtEngine) throw() {
   try {
-    smtEngine->assertFormula(d_expr);
+    smtEngine->assertFormula(d_expr, d_inUnsatCore);
     d_commandStatus = CommandSuccess::instance();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
@@ -207,18 +207,17 @@ void AssertCommand::invoke(SmtEngine* smtEngine) throw() {
 }
 
 Command* AssertCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  return new AssertCommand(d_expr.exportTo(exprManager, variableMap));
+  return new AssertCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
 }
 
 Command* AssertCommand::clone() const {
-  return new AssertCommand(d_expr);
+  return new AssertCommand(d_expr, d_inUnsatCore);
 }
 
 std::string AssertCommand::getCommandName() const throw() {
   return "assert";
 }
 
-
 /* class PushCommand */
 
 void PushCommand::invoke(SmtEngine* smtEngine) throw() {
@@ -271,8 +270,8 @@ CheckSatCommand::CheckSatCommand() throw() :
   d_expr() {
 }
 
-CheckSatCommand::CheckSatCommand(const Expr& expr) throw() :
-  d_expr(expr) {
+CheckSatCommand::CheckSatCommand(const Expr& expr, bool inUnsatCore) throw() :
+  d_expr(expr), d_inUnsatCore(inUnsatCore) {
 }
 
 Expr CheckSatCommand::getExpr() const throw() {
@@ -301,13 +300,13 @@ void CheckSatCommand::printResult(std::ostream& out, uint32_t verbosity) const t
 }
 
 Command* CheckSatCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap));
+  CheckSatCommand* c = new CheckSatCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
   c->d_result = d_result;
   return c;
 }
 
 Command* CheckSatCommand::clone() const {
-  CheckSatCommand* c = new CheckSatCommand(d_expr);
+  CheckSatCommand* c = new CheckSatCommand(d_expr, d_inUnsatCore);
   c->d_result = d_result;
   return c;
 }
@@ -318,8 +317,8 @@ std::string CheckSatCommand::getCommandName() const throw() {
 
 /* class QueryCommand */
 
-QueryCommand::QueryCommand(const Expr& e) throw() :
-  d_expr(e) {
+QueryCommand::QueryCommand(const Expr& e, bool inUnsatCore) throw() :
+  d_expr(e), d_inUnsatCore(inUnsatCore) {
 }
 
 Expr QueryCommand::getExpr() const throw() {
@@ -348,13 +347,13 @@ void QueryCommand::printResult(std::ostream& out, uint32_t verbosity) const thro
 }
 
 Command* QueryCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
-  QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap));
+  QueryCommand* c = new QueryCommand(d_expr.exportTo(exprManager, variableMap), d_inUnsatCore);
   c->d_result = d_result;
   return c;
 }
 
 Command* QueryCommand::clone() const {
-  QueryCommand* c = new QueryCommand(d_expr);
+  QueryCommand* c = new QueryCommand(d_expr, d_inUnsatCore);
   c->d_result = d_result;
   return c;
 }
@@ -1123,35 +1122,31 @@ GetUnsatCoreCommand::GetUnsatCoreCommand() throw() {
 }
 
 void GetUnsatCoreCommand::invoke(SmtEngine* smtEngine) throw() {
-  /*
   try {
     d_result = smtEngine->getUnsatCore();
     d_commandStatus = CommandSuccess::instance();
   } catch(exception& e) {
     d_commandStatus = new CommandFailure(e.what());
   }
-  */
-  d_commandStatus = new CommandUnsupported();
 }
 
 void GetUnsatCoreCommand::printResult(std::ostream& out, uint32_t verbosity) const throw() {
   if(! ok()) {
     this->Command::printResult(out, verbosity);
   } else {
-    //do nothing -- unsat cores not yet supported
-    // d_result->toStream(out);
+    d_result.toStream(out);
   }
 }
 
 Command* GetUnsatCoreCommand::exportTo(ExprManager* exprManager, ExprManagerMapCollection& variableMap) {
   GetUnsatCoreCommand* c = new GetUnsatCoreCommand();
-  //c->d_result = d_result;
+  c->d_result = d_result;
   return c;
 }
 
 Command* GetUnsatCoreCommand::clone() const {
   GetUnsatCoreCommand* c = new GetUnsatCoreCommand();
-  //c->d_result = d_result;
+  c->d_result = d_result;
   return c;
 }
 
diff --git a/src/expr/command.h b/src/expr/command.h
index c4e7fbf89..e84c53d09 100644
--- a/src/expr/command.h
+++ b/src/expr/command.h
@@ -35,6 +35,7 @@
 #include "util/sexpr.h"
 #include "util/datatype.h"
 #include "util/proof.h"
+#include "util/unsat_core.h"
 
 namespace CVC4 {
 
@@ -309,8 +310,9 @@ public:
 class CVC4_PUBLIC AssertCommand : public Command {
 protected:
   Expr d_expr;
+  bool d_inUnsatCore;
 public:
-  AssertCommand(const Expr& e) throw();
+  AssertCommand(const Expr& e, bool inUnsatCore = true) throw();
   ~AssertCommand() throw() {}
   Expr getExpr() const throw();
   void invoke(SmtEngine* smtEngine) throw();
@@ -457,9 +459,10 @@ class CVC4_PUBLIC CheckSatCommand : public Command {
 protected:
   Expr d_expr;
   Result d_result;
+  bool d_inUnsatCore;
 public:
   CheckSatCommand() throw();
-  CheckSatCommand(const Expr& expr) throw();
+  CheckSatCommand(const Expr& expr, bool inUnsatCore = true) throw();
   ~CheckSatCommand() throw() {}
   Expr getExpr() const throw();
   void invoke(SmtEngine* smtEngine) throw();
@@ -474,8 +477,9 @@ class CVC4_PUBLIC QueryCommand : public Command {
 protected:
   Expr d_expr;
   Result d_result;
+  bool d_inUnsatCore;
 public:
-  QueryCommand(const Expr& e) throw();
+  QueryCommand(const Expr& e, bool inUnsatCore = true) throw();
   ~QueryCommand() throw() {}
   Expr getExpr() const throw();
   void invoke(SmtEngine* smtEngine) throw();
@@ -597,7 +601,7 @@ public:
 
 class CVC4_PUBLIC GetUnsatCoreCommand : public Command {
 protected:
-  //UnsatCore* d_result;
+  UnsatCore d_result;
 public:
   GetUnsatCoreCommand() throw();
   ~GetUnsatCoreCommand() throw() {}
diff --git a/src/parser/smt2/Smt2.g b/src/parser/smt2/Smt2.g
index bd7c96dce..e1547d23d 100644
--- a/src/parser/smt2/Smt2.g
+++ b/src/parser/smt2/Smt2.g
@@ -378,7 +378,9 @@ command returns [CVC4::Command* cmd = NULL]
   | /* assertion */
     ASSERT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     term[expr, expr2]
-    { cmd = new AssertCommand(expr); }
+    { cmd = new AssertCommand(expr, /* inUnsatCore */ PARSER_STATE->lastNamedTerm() == expr);
+      PARSER_STATE->setLastNamedTerm(Expr());
+    }
   | /* check-sat */
     CHECKSAT_TOK { PARSER_STATE->checkThatLogicIsSet(); }
     ( term[expr, expr2]
@@ -684,7 +686,7 @@ rewriterulesCommand[CVC4::Command*& cmd]
       };
       args.push_back(expr);
       expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
-      cmd = new AssertCommand(expr); }
+      cmd = new AssertCommand(expr, false); }
     /* propagation rule */
   | rewritePropaKind[kind]
     LPAREN_TOK sortedVarList[sortedVarNames] RPAREN_TOK
@@ -735,7 +737,7 @@ rewriterulesCommand[CVC4::Command*& cmd]
       };
       args.push_back(expr);
       expr = MK_EXPR(CVC4::kind::REWRITE_RULE, args);
-      cmd = new AssertCommand(expr); }
+      cmd = new AssertCommand(expr, false); }
   ;
 
 rewritePropaKind[CVC4::Kind& kind]
@@ -1035,8 +1037,8 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
 
     /* attributed expressions */
   | LPAREN_TOK ATTRIBUTE_TOK term[expr, f2]
-    ( attribute[expr, attexpr,attr]
-      { if( attr == ":pattern" && ! attexpr.isNull()) {
+    ( attribute[expr, attexpr, attr]
+      { if(attr == ":pattern" && ! attexpr.isNull()) {
           patexprs.push_back( attexpr );
         }
       }
@@ -1074,7 +1076,7 @@ term[CVC4::Expr& expr, CVC4::Expr& expr2]
           }
         }
         expr2 = MK_EXPR(kind::INST_PATTERN_LIST, patexprs);
-      }else{
+      } else {
         expr2 = f2;
       }
     }
@@ -1210,6 +1212,8 @@ attribute[CVC4::Expr& expr,CVC4::Expr& retExpr, std::string& attr]
       PARSER_STATE->reserveSymbolAtAssertionLevel(name);
       // define it
       Expr func = PARSER_STATE->mkFunction(name, expr.getType());
+      // remember the last term to have been given a :named attribute
+      PARSER_STATE->setLastNamedTerm(expr);
       // bind name to expr with define-fun
       Command* c =
         new DefineNamedFunctionCommand(name, func, std::vector<Expr>(), expr);
diff --git a/src/parser/smt2/smt2.h b/src/parser/smt2/smt2.h
index 71161be94..7ecd2e5b1 100644
--- a/src/parser/smt2/smt2.h
+++ b/src/parser/smt2/smt2.h
@@ -54,6 +54,7 @@ private:
   bool d_logicSet;
   LogicInfo d_logic;
   std::hash_map<std::string, Kind, StringHashFunction> operatorKindMap;
+  Expr d_lastNamedTerm;
 
 protected:
   Smt2(ExprManager* exprManager, Input* input, bool strictMode = false, bool parseOnly = false);
@@ -105,6 +106,14 @@ public:
 
   void includeFile(const std::string& filename);
 
+  void setLastNamedTerm(Expr e) {
+    d_lastNamedTerm = e;
+  }
+
+  Expr lastNamedTerm() {
+    return d_lastNamedTerm;
+  }
+
   bool isAbstractValue(const std::string& name) {
     return name.length() >= 2 && name[0] == '@' && name[1] != '0' &&
       name.find_first_not_of("0123456789", 1) == std::string::npos;
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index c9db1eece..766db729a 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -702,6 +702,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
      tryToStream<GetAssignmentCommand>(out, c) ||
      tryToStream<GetAssertionsCommand>(out, c) ||
      tryToStream<GetProofCommand>(out, c) ||
+     tryToStream<GetUnsatCoreCommand>(out, c) ||
      tryToStream<SetBenchmarkStatusCommand>(out, c) ||
      tryToStream<SetBenchmarkLogicCommand>(out, c, d_variant) ||
      tryToStream<SetInfoCommand>(out, c) ||
@@ -1025,6 +1026,10 @@ static void toStream(std::ostream& out, const GetProofCommand* c) throw() {
   out << "(get-proof)";
 }
 
+static void toStream(std::ostream& out, const GetUnsatCoreCommand* c) throw() {
+  out << "(get-unsat-core)";
+}
+
 static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() {
   out << "(set-info :status " << c->getStatus() << ")";
 }
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 3dfb61428..22a40ff69 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -30,6 +30,8 @@ CnfProof::CnfProof(CnfStream* stream)
   : d_cnfStream(stream)
 {}
 
+CnfProof::~CnfProof() {
+}
 
 Expr CnfProof::getAtom(prop::SatVariable var) {
   prop::SatLiteral lit (var);
@@ -38,34 +40,33 @@ Expr CnfProof::getAtom(prop::SatVariable var) {
   return atom;
 }
 
-CnfProof::~CnfProof() {
-}
-
-LFSCCnfProof::iterator LFSCCnfProof::begin_atom_mapping() {
-  return iterator(*this, ProofManager::currentPM()->begin_vars());
+prop::SatLiteral CnfProof::getLiteral(TNode atom) {
+  return d_cnfStream->getLiteral(atom);
 }
 
-LFSCCnfProof::iterator LFSCCnfProof::end_atom_mapping() {
-  return iterator(*this, ProofManager::currentPM()->end_vars());
+Expr CnfProof::getAssertion(uint64_t id) {
+  return d_cnfStream->getAssertion(id).toExpr();
 }
 
-void LFSCCnfProof::printAtomMapping(std::ostream& os, std::ostream& paren) {
-  ProofManager::var_iterator it = ProofManager::currentPM()->begin_vars();
-  ProofManager::var_iterator end = ProofManager::currentPM()->end_vars();
-
-  for (;it != end;  ++it) {
-    os << "(decl_atom ";
-
-    if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) {
-      Expr atom = getAtom(*it);
-      LFSCTheoryProof::printTerm(atom, os);
-    } else {
-      // print fake atoms for all other logics
-      os << "true ";
+void LFSCCnfProof::printAtomMapping(const prop::SatClause* clause, std::ostream& os, std::ostream& paren) {
+  for (unsigned i = 0; i < clause->size(); ++i) {
+    prop::SatLiteral lit = clause->operator[](i);
+    if(d_atomsDeclared.find(lit.getSatVariable()) == d_atomsDeclared.end()) {
+      d_atomsDeclared.insert(lit.getSatVariable());
+      os << "(decl_atom ";
+      if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0 ||
+          ProofManager::currentPM()->getLogic().compare("QF_AX") == 0 ||
+          ProofManager::currentPM()->getLogic().compare("QF_SAT") == 0) {
+        Expr atom = getAtom(lit.getSatVariable());
+        LFSCTheoryProof::printTerm(atom, os);
+      } else {
+        // print fake atoms for all other logics (for now)
+        os << "true ";
+      }
+
+      os << " (\\ " << ProofManager::getVarName(lit.getSatVariable()) << " (\\ " << ProofManager::getAtomName(lit.getSatVariable()) << "\n";
+      paren << ")))";
     }
-
-    os << " (\\ " << ProofManager::getVarName(*it) << " (\\ " << ProofManager::getAtomName(*it) << "\n";
-    paren << ")))";
   }
 }
 
@@ -75,36 +76,93 @@ void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) {
 }
 
 void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) {
-  os << " ;; Input Clauses \n";
+  os << " ;; Clauses\n";
   ProofManager::clause_iterator it = ProofManager::currentPM()->begin_input_clauses();
   ProofManager::clause_iterator end = ProofManager::currentPM()->end_input_clauses();
 
   for (; it != end; ++it) {
     ClauseId id = it->first;
     const prop::SatClause* clause = it->second;
+    printAtomMapping(clause, os, paren);
     os << "(satlem _ _ ";
     std::ostringstream clause_paren;
     printClause(*clause, os, clause_paren);
-    os << " (clausify_false trust)" << clause_paren.str();
-    os << "( \\ " << ProofManager::getInputClauseName(id) << "\n";
+    os << "(clausify_false trust)" << clause_paren.str()
+       << " (\\ " << ProofManager::getInputClauseName(id) << "\n";
     paren << "))";
   }
 }
 
-
 void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) {
-  os << " ;; Theory Lemmas \n";
-  ProofManager::clause_iterator it = ProofManager::currentPM()->begin_lemmas();
-  ProofManager::clause_iterator end = ProofManager::currentPM()->end_lemmas();
+  os << " ;; Theory Lemmas\n";
+  ProofManager::ordered_clause_iterator it = ProofManager::currentPM()->begin_lemmas();
+  ProofManager::ordered_clause_iterator end = ProofManager::currentPM()->end_lemmas();
+
+  for(size_t n = 0; it != end; ++it, ++n) {
+    if(n % 100 == 0) {
+      Chat() << "proving theory conflicts...(" << n << "/" << ProofManager::currentPM()->num_lemmas() << ")" << std::endl;
+    }
 
-  for (; it != end; ++it) {
     ClauseId id = it->first;
     const prop::SatClause* clause = it->second;
+    NodeBuilder<> c(kind::AND);
+    for(unsigned i = 0; i < clause->size(); ++i) {
+      prop::SatLiteral lit = (*clause)[i];
+      prop::SatVariable var = lit.getSatVariable();
+      if(lit.isNegated()) {
+        c << Node::fromExpr(getAtom(var));
+      } else {
+        c << Node::fromExpr(getAtom(var)).notNode();
+      }
+    }
+    Node cl = c;
+    if(ProofManager::getSatProof()->d_lemmaClauses.find(id) != ProofManager::getSatProof()->d_lemmaClauses.end()) {
+      uint64_t proof_id = ProofManager::getSatProof()->d_lemmaClauses[id];
+      TNode orig = d_cnfStream->getAssertion(proof_id & 0xffffffff);
+      if(((proof_id >> 32) & 0xffffffff) == RULE_ARRAYS_EXT) {
+        Debug("cores") << "; extensional lemma!" << std::endl;
+        Assert(cl.getKind() == kind::AND && cl.getNumChildren() == 2 && cl[0].getKind() == kind::EQUAL && cl[0][0].getKind() == kind::SELECT);
+        TNode myk = cl[0][0][1];
+        Debug("cores") << "; so my skolemized k is " << myk << std::endl;
+        os << "(ext _ _ " << orig[0][0] << " " << orig[0][1] << " (\\ " << myk << " (\\ " << ProofManager::getLemmaName(id) << "\n";
+        paren << ")))";
+      }
+    }
+    printAtomMapping(clause, os, paren);
     os << "(satlem _ _ ";
     std::ostringstream clause_paren;
     printClause(*clause, os, clause_paren);
-    os << " (clausify_false trust)" << clause_paren.str();
-    os << "( \\ " << ProofManager::getLemmaClauseName(id) <<"\n";
+
+    Debug("cores") << "\n;id is " << id << std::endl;
+    if(ProofManager::getSatProof()->d_lemmaClauses.find(id) != ProofManager::getSatProof()->d_lemmaClauses.end()) {
+      uint64_t proof_id = ProofManager::getSatProof()->d_lemmaClauses[id];
+      Debug("cores") << ";getting id " << int32_t(proof_id & 0xffffffff) << std::endl;
+      Assert(int32_t(proof_id & 0xffffffff) != -1);
+      TNode orig = d_cnfStream->getAssertion(proof_id & 0xffffffff);
+      Debug("cores") << "; ID is " << id << " and that's a lemma with " << ((proof_id >> 32) & 0xffffffff) << " / " << (proof_id & 0xffffffff) << std::endl;
+      Debug("cores") << "; that means the lemma was " << orig << std::endl;
+      if(((proof_id >> 32) & 0xffffffff) == RULE_ARRAYS_EXT) {
+        Debug("cores") << "; extensional" << std::endl;
+        os << "(clausify_false trust)\n";
+      } else if(proof_id == 0) {
+        // theory propagation caused conflict
+        //ProofManager::currentPM()->printProof(os, cl);
+        os << "(clausify_false trust)\n";
+      } else if(((proof_id >> 32) & 0xffffffff) == RULE_CONFLICT) {
+        os << "\n;; need to generate a (conflict) proof of " << cl << "\n";
+        //ProofManager::currentPM()->printProof(os, cl);
+        os << "(clausify_false trust)\n";
+      } else {
+        os << "\n;; need to generate a (lemma) proof of " << cl;
+        os << "\n;; DON'T KNOW HOW !!\n";
+        os << "(clausify_false trust)\n";
+      }
+    } else {
+      os << "\n;; need to generate a (conflict) proof of " << cl << "\n";
+      ProofManager::currentPM()->printProof(os, cl);
+    }
+    os << clause_paren.str()
+       << " (\\ " << ProofManager::getLemmaClauseName(id) << "\n";
     paren << "))";
   }
 }
@@ -114,10 +172,10 @@ void LFSCCnfProof::printClause(const prop::SatClause& clause, std::ostream& os,
     prop::SatLiteral lit = clause[i];
     prop::SatVariable var = lit.getSatVariable();
     if (lit.isNegated()) {
-      os << "(ast _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " ";
+      os << "(ast _ _ _ " << ProofManager::getAtomName(var) << " (\\ " << ProofManager::getLitName(lit) << " ";
       paren << "))";
     } else {
-      os << "(asf _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " ";
+      os << "(asf _ _ _ " << ProofManager::getAtomName(var) << " (\\ " << ProofManager::getLitName(lit) << " ";
       paren << "))";
     }
   }
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index b2c35c4f7..459815e60 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -30,62 +30,38 @@
 namespace CVC4 {
 namespace prop {
   class CnfStream;
-}
+}/* CVC4::prop namespace */
 
 class CnfProof;
 
-class AtomIterator {
-  CnfProof& d_cnf;
-  ProofManager::var_iterator d_it;
-
-public:
-  AtomIterator(CnfProof& cnf, const ProofManager::var_iterator& it)
-    : d_cnf(cnf), d_it(it)
-  {}
-  inline Expr operator*();
-  AtomIterator& operator++() { ++d_it; return *this; }
-  AtomIterator operator++(int) { AtomIterator x = *this; ++d_it; return x; }
-  bool operator==(const AtomIterator& it) const { return &d_cnf == &it.d_cnf && d_it == it.d_it; }
-  bool operator!=(const AtomIterator& it) const { return !(*this == it); }
-};/* class AtomIterator */
-
 class CnfProof {
 protected:
   CVC4::prop::CnfStream* d_cnfStream;
-  Expr getAtom(prop::SatVariable var);
-  friend class AtomIterator;
+  VarSet d_atomsDeclared;
 public:
   CnfProof(CVC4::prop::CnfStream* cnfStream);
 
-  typedef AtomIterator iterator;
-  virtual iterator begin_atom_mapping() = 0;
-  virtual iterator end_atom_mapping() = 0;
+  Expr getAtom(prop::SatVariable var);
+  Expr getAssertion(uint64_t id);
+  prop::SatLiteral getLiteral(TNode atom);
 
-  virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0;
   virtual void printClauses(std::ostream& os, std::ostream& paren) = 0;
   virtual ~CnfProof();
-};
+};/* class CnfProof */
 
 class LFSCCnfProof : public CnfProof {
   void printInputClauses(std::ostream& os, std::ostream& paren);
   void printTheoryLemmas(std::ostream& os, std::ostream& paren);
   void printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren);
+  virtual void printAtomMapping(const prop::SatClause* clause, std::ostream& os, std::ostream& paren);
 
 public:
   LFSCCnfProof(CVC4::prop::CnfStream* cnfStream)
     : CnfProof(cnfStream)
   {}
 
-  virtual iterator begin_atom_mapping();
-  virtual iterator end_atom_mapping();
-
-  virtual void printAtomMapping(std::ostream& os, std::ostream& paren);
   virtual void printClauses(std::ostream& os, std::ostream& paren);
-};
-
-inline Expr AtomIterator::operator*() {
-  return d_cnf.getAtom(*d_it);
-}
+};/* class LFSCCnfProof */
 
 } /* CVC4 namespace */
 
diff --git a/src/proof/proof.h b/src/proof/proof.h
index 174913755..440279dbc 100644
--- a/src/proof/proof.h
+++ b/src/proof/proof.h
@@ -22,9 +22,9 @@
 #include "smt/options.h"
 
 #ifdef CVC4_PROOF
-#  define PROOF(x) if(options::proof()) { x; }
-#  define NULLPROOF(x) (options::proof()) ? x : NULL
-#  define PROOF_ON() options::proof()
+#  define PROOF(x) if(options::proof() || options::unsatCores()) { x; }
+#  define NULLPROOF(x) (options::proof() || options::unsatCores()) ? x : NULL
+#  define PROOF_ON() (options::proof() || options::unsatCores())
 #else /* CVC4_PROOF */
 #  define PROOF(x)
 #  define NULLPROOF(x) NULL
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 680e57d39..0cca16574 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -23,6 +23,15 @@
 #include "util/cvc4_assert.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "theory/output_channel.h"
+#include "theory/valuation.h"
+#include "util/node_visitor.h"
+#include "theory/term_registration_visitor.h"
+#include "theory/uf/theory_uf.h"
+#include "theory/uf/equality_engine.h"
+#include "theory/arrays/theory_arrays.h"
+#include "context/context.h"
+#include "util/hash.h"
 
 namespace CVC4 {
 
@@ -37,7 +46,8 @@ ProofManager::ProofManager(ProofFormat format):
   d_cnfProof(NULL),
   d_theoryProof(NULL),
   d_fullProof(NULL),
-  d_format(format)
+  d_format(format),
+  d_deps()
 {
 }
 
@@ -53,7 +63,7 @@ ProofManager::~ProofManager() {
     delete it->second;
   }
 
-  for(IdToClause::iterator it = d_theoryLemmas.begin();
+  for(OrderedIdToClause::iterator it = d_theoryLemmas.begin();
       it != d_theoryLemmas.end();
       ++it) {
     delete it->second;
@@ -91,11 +101,10 @@ CnfProof* ProofManager::getCnfProof() {
 }
 
 TheoryProof* ProofManager::getTheoryProof() {
-  Assert (currentPM()->d_theoryProof);
+  //Assert (currentPM()->d_theoryProof);
   return currentPM()->d_theoryProof;
 }
 
-
 void ProofManager::initSatProof(Minisat::Solver* solver) {
   Assert (currentPM()->d_satProof == NULL);
   Assert(currentPM()->d_format == LFSC);
@@ -114,35 +123,101 @@ void ProofManager::initTheoryProof() {
   currentPM()->d_theoryProof = new LFSCTheoryProof();
 }
 
-
-std::string ProofManager::getInputClauseName(ClauseId id) {return append("pb", id); }
-std::string ProofManager::getLemmaClauseName(ClauseId id) { return append("lem", id); }
+std::string ProofManager::getInputClauseName(ClauseId id) { return append("pb", id); }
+std::string ProofManager::getLemmaName(ClauseId id) { return append("lem", id); }
+std::string ProofManager::getLemmaClauseName(ClauseId id) { return append("lemc", id); }
 std::string ProofManager::getLearntClauseName(ClauseId id) { return append("cl", id); }
-std::string ProofManager::getVarName(prop::SatVariable var) { return append("v", var); }
-std::string ProofManager::getAtomName(prop::SatVariable var) { return append("a", var); }
-std::string ProofManager::getLitName(prop::SatLiteral lit) {return append("l", lit.toInt()); }
+std::string ProofManager::getVarName(prop::SatVariable var) { return append("var", var); }
+std::string ProofManager::getAtomName(prop::SatVariable var) { return append("atom", var); }
+std::string ProofManager::getLitName(prop::SatLiteral lit) { return append("lit", lit.toInt()); }
+
+std::string ProofManager::getAtomName(TNode atom) {
+  prop::SatLiteral lit = currentPM()->d_cnfProof->getLiteral(atom);
+  Assert(!lit.isNegated());
+  return getAtomName(lit.getSatVariable());
+}
+std::string ProofManager::getLitName(TNode lit) {
+  return getLitName(currentPM()->d_cnfProof->getLiteral(lit));
+}
+
+void ProofManager::traceDeps(TNode n) {
+  Debug("cores") << "trace deps " << n << std::endl;
+  if(d_inputCoreFormulas.find(n.toExpr()) != d_inputCoreFormulas.end()) {
+    // originating formula was in core set
+    Debug("cores") << " -- IN INPUT CORE LIST!" << std::endl;
+    d_outputCoreFormulas.insert(n.toExpr());
+  } else {
+    Debug("cores") << " -- NOT IN INPUT CORE LIST!" << std::endl;
+    if(d_deps.find(n) == d_deps.end()) {
+      InternalError("Cannot trace dependence information back to input assertion:\n`%s'", n.toString().c_str());
+    }
+    Assert(d_deps.find(n) != d_deps.end());
+    std::vector<Node> deps = (*d_deps.find(n)).second;
+    for(std::vector<Node>::const_iterator i = deps.begin(); i != deps.end(); ++i) {
+      Debug("cores") << " + tracing deps: " << n << " -deps-on- " << *i << std::endl;
+      traceDeps(*i);
+    }
+  }
+}
 
 void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) {
-  for (unsigned i = 0; i < clause->size(); ++i) {
+  /*for (unsigned i = 0; i < clause->size(); ++i) {
     prop::SatLiteral lit = clause->operator[](i);
     d_propVars.insert(lit.getSatVariable());
-  }
+  }*/
   if (kind == INPUT) {
     d_inputClauses.insert(std::make_pair(id, clause));
-    return;
+    Assert(d_satProof->d_inputClauses.find(id) != d_satProof->d_inputClauses.end());
+    Debug("cores") << "core id is " << d_satProof->d_inputClauses[id] << std::endl;
+    if(d_satProof->d_inputClauses[id] == uint64_t(-1)) {
+      Debug("cores") << " + constant unit (true or false)" << std::endl;
+    } else if(options::unsatCores()) {
+      Expr e = d_cnfProof->getAssertion(d_satProof->d_inputClauses[id] & 0xffffffff);
+      Debug("cores") << "core input assertion from CnfStream is " << e << std::endl;
+      Debug("cores") << "with proof rule " << ((d_satProof->d_inputClauses[id] & 0xffffffff00000000) >> 32) << std::endl;
+      // Invalid proof rules are currently used for parts of CVC4 that don't
+      // support proofs (these are e.g. unproven theory lemmas) or don't need
+      // proofs (e.g. split lemmas).  We can ignore these safely when
+      // constructing unsat cores.
+      if(((d_satProof->d_inputClauses[id] & 0xffffffff00000000) >> 32) != RULE_INVALID) {
+        // trace dependences back to actual assertions
+        traceDeps(Node::fromExpr(e));
+      }
+    }
+  } else {
+    Assert(kind == THEORY_LEMMA);
+    d_theoryLemmas.insert(std::make_pair(id, clause));
   }
-  Assert (kind == THEORY_LEMMA);
-  d_theoryLemmas.insert(std::make_pair(id, clause));
 }
 
-void ProofManager::addAssertion(Expr formula) {
+void ProofManager::addAssertion(Expr formula, bool inUnsatCore) {
+  Debug("cores") << "assert: " << formula << std::endl;
   d_inputFormulas.insert(formula);
+  d_deps[Node::fromExpr(formula)]; // empty vector of deps
+  if(inUnsatCore || options::dumpUnsatCores()) {
+    Debug("cores") << "adding to input core forms: " << formula << std::endl;
+    d_inputCoreFormulas.insert(formula);
+  }
 }
 
-void ProofManager::setLogic(const std::string& logic_string) {
-  d_logic = logic_string;
+void ProofManager::addDependence(TNode n, TNode dep) {
+  if(dep != n) {
+    Debug("cores") << "dep: " << n << " : " << dep << std::endl;
+    if(d_deps.find(dep) == d_deps.end()) {
+      Debug("cores") << "WHERE DID " << dep << " come from ??" << std::endl;
+    }
+    //Assert(d_deps.find(dep) != d_deps.end());
+    d_deps[n].push_back(dep);
+  }
+}
+
+void ProofManager::setLogic(const LogicInfo& logic) {
+  d_logic = logic;
 }
 
+void ProofManager::printProof(std::ostream& os, TNode n) {
+  // no proofs here yet
+}
 
 LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory)
   : d_satProof(sat)
@@ -157,17 +232,18 @@ void LFSCProof::toStream(std::ostream& out) {
   smt::SmtScope scope(d_smtEngine);
   std::ostringstream paren;
   out << "(check\n";
+  out << " ;; Declarations\n";
   if (d_theoryProof == NULL) {
     d_theoryProof = new LFSCTheoryProof();
   }
-  for(LFSCCnfProof::iterator i = d_cnfProof->begin_atom_mapping();
+  /*for(LFSCCnfProof::iterator i = d_cnfProof->begin_atom_mapping();
       i != d_cnfProof->end_atom_mapping();
       ++i) {
     d_theoryProof->addDeclaration(*i);
-  }
+  }*/
   d_theoryProof->printAssertions(out, paren);
+  out << " ;; Proof of empty clause follows\n";
   out << "(: (holds cln)\n";
-  d_cnfProof->printAtomMapping(out, paren);
   d_cnfProof->printClauses(out, paren);
   d_satProof->printResolutions(out, paren);
   paren <<")))\n;;";
@@ -175,5 +251,4 @@ void LFSCProof::toStream(std::ostream& out) {
   out << "\n";
 }
 
-
 } /* CVC4  namespace */
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index f428de36d..d60a3f6e3 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -20,9 +20,12 @@
 #define __CVC4__PROOF_MANAGER_H
 
 #include <iostream>
+#include <map>
 #include "proof/proof.h"
 #include "util/proof.h"
-
+#include "expr/node.h"
+#include "theory/logic_info.h"
+#include "theory/substitutions.h"
 
 // forward declarations
 namespace Minisat {
@@ -63,6 +66,7 @@ enum ProofFormat {
 std::string append(const std::string& str, uint64_t num);
 
 typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause;
+typedef std::map < ClauseId, const prop::SatClause* > OrderedIdToClause;
 typedef __gnu_cxx::hash_set<prop::SatVariable > VarSet;
 typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
 
@@ -74,6 +78,18 @@ enum ClauseKind {
   LEARNT
 };/* enum ClauseKind */
 
+enum ProofRule {
+  RULE_GIVEN,       /* input assertion */
+  RULE_DERIVED,     /* a "macro" rule */
+  RULE_RECONSTRUCT, /* prove equivalence using another method */
+  RULE_TRUST,       /* trust without evidence (escape hatch until proofs are fully supported) */
+  RULE_INVALID,     /* assert-fail if this is ever needed in proof; use e.g. for split lemmas */
+  RULE_CONFLICT,    /* re-construct as a conflict */
+
+  RULE_ARRAYS_EXT,  /* arrays, extensional */
+  RULE_ARRAYS_ROW,  /* arrays, read-over-write */
+};/* enum ProofRules */
+
 class ProofManager {
   SatProof*    d_satProof;
   CnfProof*    d_cnfProof;
@@ -81,15 +97,25 @@ class ProofManager {
 
   // information that will need to be shared across proofs
   IdToClause d_inputClauses;
-  IdToClause d_theoryLemmas;
+  OrderedIdToClause d_theoryLemmas;
+  IdToClause d_theoryPropagations;
   ExprSet    d_inputFormulas;
-  VarSet     d_propVars;
+  ExprSet    d_inputCoreFormulas;
+  ExprSet    d_outputCoreFormulas;
+  //VarSet     d_propVars;
+
+  int d_nextId;
 
   Proof* d_fullProof;
   ProofFormat d_format; // used for now only in debug builds
 
+  __gnu_cxx::hash_map< Node, std::vector<Node>, NodeHashFunction > d_deps;
+
+  // trace dependences back to unsat core
+  void traceDeps(TNode n);
+
 protected:
-  std::string d_logic;
+  LogicInfo d_logic;
 
 public:
   ProofManager(ProofFormat format = LFSC);
@@ -109,35 +135,50 @@ public:
 
   // iterators over data shared by proofs
   typedef IdToClause::const_iterator clause_iterator;
+  typedef OrderedIdToClause::const_iterator ordered_clause_iterator;
   typedef ExprSet::const_iterator assertions_iterator;
   typedef VarSet::const_iterator var_iterator;
 
   clause_iterator begin_input_clauses() const { return d_inputClauses.begin(); }
   clause_iterator end_input_clauses() const { return d_inputClauses.end(); }
+  size_t num_input_clauses() const { return d_inputClauses.size(); }
 
-  clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); }
-  clause_iterator end_lemmas() const { return d_theoryLemmas.end(); }
+  ordered_clause_iterator begin_lemmas() const { return d_theoryLemmas.begin(); }
+  ordered_clause_iterator end_lemmas() const { return d_theoryLemmas.end(); }
+  size_t num_lemmas() const { return d_theoryLemmas.size(); }
 
   assertions_iterator begin_assertions() const { return d_inputFormulas.begin(); }
   assertions_iterator end_assertions() const { return d_inputFormulas.end(); }
+  size_t num_assertions() const { return d_inputFormulas.size(); }
 
-  var_iterator begin_vars() const { return d_propVars.begin(); }
-  var_iterator end_vars() const { return d_propVars.end(); }
+  void printProof(std::ostream& os, TNode n);
 
-  void addAssertion(Expr formula);
+  void addAssertion(Expr formula, bool inUnsatCore);
   void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind);
+  // note that n depends on dep (for cores)
+  void addDependence(TNode n, TNode dep);
+
+  assertions_iterator begin_unsat_core() const { return d_outputCoreFormulas.begin(); }
+  assertions_iterator end_unsat_core() const { return d_outputCoreFormulas.end(); }
+  size_t size_unsat_core() const { return d_outputCoreFormulas.size(); }
+
+  int nextId() { return d_nextId++; }
 
   // variable prefixes
   static std::string getInputClauseName(ClauseId id);
+  static std::string getLemmaName(ClauseId id);
   static std::string getLemmaClauseName(ClauseId id);
   static std::string getLearntClauseName(ClauseId id);
 
   static std::string getVarName(prop::SatVariable var);
   static std::string getAtomName(prop::SatVariable var);
+  static std::string getAtomName(TNode atom);
   static std::string getLitName(prop::SatLiteral lit);
+  static std::string getLitName(TNode lit);
+
+  void setLogic(const LogicInfo& logic);
+  const std::string getLogic() const { return d_logic.getLogicString(); }
 
-  void setLogic(const std::string& logic_string);
-  const std::string getLogic() const { return d_logic; }
 };/* class ProofManager */
 
 class LFSCProof : public Proof {
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index 0ace84b4d..f7b9c4889 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -57,9 +57,6 @@ void printDebug (Minisat::Clause& c) {
   Debug("proof:sat") << endl;
 }
 
-
-int SatProof::d_idCounter = 0;
-
 /**
  * Converts the clause associated to id to a set of literals
  *
@@ -274,7 +271,7 @@ ClauseId SatProof::getClauseId(::Minisat::Lit lit) {
 
 Minisat::CRef SatProof::getClauseRef(ClauseId id) {
   if (d_idClause.find(id) == d_idClause.end()) {
-    Debug("proof:sat") << "proof:getClauseRef cannot find clause "<<id<<" "
+    Debug("proof:sat") << "proof:getClauseRef cannot find clause " << id << " "
                        << ((d_deleted.find(id) != d_deleted.end()) ? "deleted" : "")
                        << (isUnit(id)? "Unit" : "") << endl;
   }
@@ -318,16 +315,14 @@ bool SatProof::isLemmaClause(ClauseId id) {
   return (d_lemmaClauses.find(id) != d_lemmaClauses.end());
 }
 
-
 void SatProof::print(ClauseId id) {
   if (d_deleted.find(id) != d_deleted.end()) {
-    Debug("proof:sat") << "del"<<id;
+    Debug("proof:sat") << "del" << id;
   } else if (isUnit(id)) {
     printLit(getUnit(id));
   } else if (id == d_emptyClauseId) {
-    Debug("proof:sat") << "empty "<< endl;
-  }
-  else {
+    Debug("proof:sat") << "empty " << endl;
+  } else {
     CRef ref = getClauseRef(id);
     printClause(getClause(ref));
   }
@@ -335,7 +330,7 @@ void SatProof::print(ClauseId id) {
 
 void SatProof::printRes(ClauseId id) {
   Assert(hasResolution(id));
-  Debug("proof:sat") << "id "<< id <<": ";
+  Debug("proof:sat") << "id " << id << ": ";
   printRes(d_resChains[id]);
 }
 
@@ -364,42 +359,44 @@ void SatProof::printRes(ResChain* res) {
 
 /// registration methods
 
-ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind) {
+ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind, uint64_t proof_id) {
+  Debug("cores") << "registerClause " << proof_id << std::endl;
   Assert(clause != CRef_Undef);
   ClauseIdMap::iterator it = d_clauseId.find(clause);
   if (it == d_clauseId.end()) {
-    ClauseId newId = d_idCounter++;
+    ClauseId newId = ProofManager::currentPM()->nextId();
     d_clauseId[clause] = newId;
     d_idClause[newId] = clause;
     if (kind == INPUT) {
       Assert(d_inputClauses.find(newId) == d_inputClauses.end());
-      d_inputClauses.insert(newId);
+      d_inputClauses[newId] = proof_id;
     }
     if (kind == THEORY_LEMMA) {
       Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
-      d_lemmaClauses.insert(newId);
+      d_lemmaClauses[newId] = proof_id;
     }
   }
-  Debug("proof:sat:detailed") <<"registerClause CRef:" << clause <<" id:" << d_clauseId[clause] << " " << kind << "\n";
+  Debug("proof:sat:detailed") << "registerClause CRef:" << clause << " id:" << d_clauseId[clause] << " " << kind << " " << int32_t((proof_id >> 32) & 0xffffffff) << "\n";
   return d_clauseId[clause];
 }
 
-ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind) {
+ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id) {
+  Debug("cores") << "registerUnitClause " << kind << " " << proof_id << std::endl;
   UnitIdMap::iterator it = d_unitId.find(toInt(lit));
   if (it == d_unitId.end()) {
-    ClauseId newId = d_idCounter++;
+    ClauseId newId = ProofManager::currentPM()->nextId();
     d_unitId[toInt(lit)] = newId;
     d_idUnit[newId] = lit;
     if (kind == INPUT) {
       Assert(d_inputClauses.find(newId) == d_inputClauses.end());
-      d_inputClauses.insert(newId);
+      d_inputClauses[newId] = proof_id;
     }
     if (kind == THEORY_LEMMA) {
       Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
-      d_lemmaClauses.insert(newId);
+      d_lemmaClauses[newId] = proof_id;
     }
   }
-  Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << kind <<"\n";
+  Debug("proof:sat:detailed") << "registerUnitClause " << d_unitId[toInt(lit)] << " " << kind << "\n";
   return d_unitId[toInt(lit)];
 }
 
@@ -445,7 +442,7 @@ void SatProof::removeRedundantFromRes(ResChain* res, ClauseId id) {
     removedDfs(*it, removed, removeStack, inClause, seen);
   }
 
-  for (int i = removeStack.size()-1; i >= 0; --i) {
+  for (int i = removeStack.size() - 1; i >= 0; --i) {
     Lit lit = removeStack[i];
     CRef reason_ref = d_solver->reason(var(lit));
     ClauseId reason_id;
@@ -454,7 +451,7 @@ void SatProof::removeRedundantFromRes(ResChain* res, ClauseId id) {
       Assert(isUnit(~lit));
       reason_id = getUnitId(~lit);
     } else {
-      reason_id = registerClause(reason_ref);
+      reason_id = registerClause(reason_ref, LEARNT, uint64_t(-1));
     }
     res->addStep(lit, reason_id, !sign(lit));
   }
@@ -486,14 +483,14 @@ void SatProof::startResChain(::Minisat::CRef start) {
 }
 
 void SatProof::addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign) {
-  ClauseId id = registerClause(clause);
+  ClauseId id = registerClause(clause, LEARNT, uint64_t(-1));
   ResChain* res = d_resStack.back();
   res->addStep(lit, id, sign);
 }
 
 void SatProof::endResChain(CRef clause) {
   Assert(d_resStack.size() > 0);
-  ClauseId id = registerClause(clause);
+  ClauseId id = registerClause(clause, LEARNT, uint64_t(-1));
   ResChain* res = d_resStack.back();
   registerResolution(id, res);
   d_resStack.pop_back();
@@ -502,7 +499,7 @@ void SatProof::endResChain(CRef clause) {
 
 void SatProof::endResChain(::Minisat::Lit lit) {
   Assert(d_resStack.size() > 0);
-  ClauseId id = registerUnitClause(lit);
+  ClauseId id = registerUnitClause(lit, LEARNT, uint64_t(-1));
   ResChain* res = d_resStack.back();
   registerResolution(id, res);
   d_resStack.pop_back();
@@ -523,6 +520,7 @@ void SatProof::resolveOutUnit(::Minisat::Lit lit) {
 }
 
 void SatProof::storeUnitResolution(::Minisat::Lit lit) {
+  Debug("cores") << "STORE UNIT RESOLUTION" << std::endl;
   resolveUnit(lit);
 }
 
@@ -536,7 +534,7 @@ ClauseId SatProof::resolveUnit(::Minisat::Lit lit) {
   CRef reason_ref = d_solver->reason(var(lit));
   Assert(reason_ref != CRef_Undef);
 
-  ClauseId reason_id = registerClause(reason_ref);
+  ClauseId reason_id = registerClause(reason_ref, LEARNT, uint64_t(-1));
 
   ResChain* res = new ResChain(reason_id);
   // Here, the call to resolveUnit() can reallocate memory in the
@@ -551,7 +549,7 @@ ClauseId SatProof::resolveUnit(::Minisat::Lit lit) {
       res->addStep(l, res_id, !sign(l));
     }
   }
-  ClauseId unit_id = registerUnitClause(lit);
+  ClauseId unit_id = registerUnitClause(lit, LEARNT, uint64_t(-1));
   registerResolution(unit_id, res);
   return unit_id;
 }
@@ -561,11 +559,12 @@ void SatProof::toStream(std::ostream& out) {
   Unimplemented("native proof printing not supported yet");
 }
 
-void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind) {
+void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind, uint64_t proof_id) {
+  Debug("cores") << "STORE UNIT CONFLICT" << std::endl;
   Assert(!d_storedUnitConflict);
-  d_unitConflictId = registerUnitClause(conflict_lit, kind);
+  d_unitConflictId = registerUnitClause(conflict_lit, kind, proof_id);
   d_storedUnitConflict = true;
-  Debug("proof:sat:detailed") <<"storeUnitConflict " << d_unitConflictId << "\n";
+  Debug("proof:sat:detailed") << "storeUnitConflict " << d_unitConflictId << "\n";
 }
 
 void SatProof::finalizeProof(::Minisat::CRef conflict_ref) {
@@ -586,7 +585,7 @@ void SatProof::finalizeProof(::Minisat::CRef conflict_ref) {
     return;
   } else {
     Assert(!d_storedUnitConflict);
-    conflict_id = registerClause(conflict_ref); //FIXME
+    conflict_id = registerClause(conflict_ref, LEARNT, uint64_t(-1)); //FIXME
   }
 
   if(Debug.isOn("proof:sat")) {
@@ -652,11 +651,10 @@ std::string SatProof::clauseName(ClauseId id) {
   if (isInputClause(id)) {
     os << ProofManager::getInputClauseName(id);
     return os.str();
-  } else
-  if (isLemmaClause(id)) {
+  } else if (isLemmaClause(id)) {
     os << ProofManager::getLemmaClauseName(id);
     return os.str();
-  }else {
+  } else {
     os << ProofManager::getLearntClauseName(id);
     return os.str();
   }
@@ -728,10 +726,9 @@ void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream&
   ResChain* res = d_resChains[id];
   ResSteps& steps = res->getSteps();
 
-  for (int i = steps.size()-1; i >= 0; i--) {
+  for (int i = steps.size() - 1; i >= 0; --i) {
     out << "(";
     out << (steps[i].sign? "R" : "Q") << " _ _ ";
-
   }
 
   ClauseId start_id = res->getStart();
@@ -742,11 +739,13 @@ void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream&
   out << clauseName(start_id) << " ";
 
   for(unsigned i = 0; i < steps.size(); i++) {
-    out << clauseName(steps[i].id) << " "<<ProofManager::getVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit))) <<")";
+    out << clauseName(steps[i].id) << " "
+        << ProofManager::getVarName(MinisatSatSolver::toSatVariable(var(steps[i].lit)))
+        << ") ";
   }
 
   if (id == d_emptyClauseId) {
-    out <<"(\\empty empty)";
+    out << "(\\empty empty)";
     return;
   }
 
@@ -763,6 +762,4 @@ void LFSCSatProof::printResolutions(std::ostream& out, std::ostream& paren) {
   printResolution(d_emptyClauseId, out, paren);
 }
 
-
 } /* CVC4 namespace */
-
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 7795dfa9c..ef4e7a5aa 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -86,6 +86,7 @@ typedef std::hash_map < ClauseId, ::Minisat::Lit>   IdUnitMap;
 typedef std::hash_map < int, ClauseId>            UnitIdMap; //FIXME
 typedef std::hash_map < ClauseId, ResChain*>      IdResMap;
 typedef std::hash_set < ClauseId >                IdHashSet;
+typedef std::hash_map < ClauseId, uint64_t >      IdProofRuleMap;
 typedef std::vector   < ResChain* >               ResStack;
 typedef std::hash_map <ClauseId, prop::SatClause* >     IdToSatClause;
 typedef std::set < ClauseId >                     IdSet;
@@ -115,14 +116,15 @@ protected:
   UnitIdMap           d_unitId;
   IdHashSet           d_deleted;
   IdToSatClause       d_deletedTheoryLemmas;
-  IdHashSet           d_inputClauses;
-  IdHashSet           d_lemmaClauses;
+public:
+  IdProofRuleMap      d_inputClauses;
+  IdProofRuleMap      d_lemmaClauses;
+protected:
   // resolutions
   IdResMap            d_resChains;
   ResStack            d_resStack;
   bool                d_checkRes;
 
-  static ClauseId     d_idCounter;
   const ClauseId      d_emptyClauseId;
   const ClauseId      d_nullId;
   // proxy class to break circular dependencies
@@ -144,6 +146,7 @@ protected:
   void printRes(ResChain* res);
 
   bool isInputClause(ClauseId id);
+  bool isTheoryConflict(ClauseId id);
   bool isLemmaClause(ClauseId id);
   bool isUnit(ClauseId id);
   bool isUnit(::Minisat::Lit lit);
@@ -207,10 +210,10 @@ public:
   void finalizeProof(::Minisat::CRef conflict);
 
   /// clause registration methods
-  ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind = LEARNT);
-  ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind = LEARNT);
+  ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind, uint64_t proof_id);
+  ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id);
 
-  void storeUnitConflict(::Minisat::Lit lit, ClauseKind kind = LEARNT);
+  void storeUnitConflict(::Minisat::Lit lit, ClauseKind kind, uint64_t proof_id);
 
   /**
    * Marks the deleted clauses as deleted. Note we may still use them in the final
@@ -242,6 +245,7 @@ public:
 protected:
   IdSet              d_seenLearnt;
   IdHashSet          d_seenInput;
+  IdHashSet          d_seenTheoryConflicts;
   IdHashSet          d_seenLemmas;
 
   inline std::string varName(::Minisat::Lit lit);
diff --git a/src/prop/bvminisat/bvminisat.cpp b/src/prop/bvminisat/bvminisat.cpp
index 2121d7366..498b31ce5 100644
--- a/src/prop/bvminisat/bvminisat.cpp
+++ b/src/prop/bvminisat/bvminisat.cpp
@@ -5,7 +5,7 @@
  ** Major contributors:
  ** Minor contributors (to current version):
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -45,7 +45,7 @@ void BVMinisatSatSolver::setNotify(Notify* notify) {
   d_minisat->setNotify(d_minisatNotify);
 }
 
-void BVMinisatSatSolver::addClause(SatClause& clause, bool removable) {
+void BVMinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) {
   Debug("sat::minisat") << "Add clause " << clause <<"\n";
   BVMinisat::vec<BVMinisat::Lit> minisat_clause;
   toMinisatClause(clause, minisat_clause);
diff --git a/src/prop/bvminisat/bvminisat.h b/src/prop/bvminisat/bvminisat.h
index 0101c5d62..04f21e761 100644
--- a/src/prop/bvminisat/bvminisat.h
+++ b/src/prop/bvminisat/bvminisat.h
@@ -5,7 +5,7 @@
  ** Major contributors:
  ** Minor contributors (to current version):
  ** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2014  The Analysis of Computer Systems Group (ACSys)
  ** Courant Institute of Mathematical Sciences
  ** New York University
  ** See the file COPYING in the top-level source directory for licensing
@@ -76,7 +76,7 @@ public:
 
   void setNotify(Notify* notify);
 
-  void addClause(SatClause& clause, bool removable);
+  void addClause(SatClause& clause, bool removable, uint64_t proof_id);
 
   SatValue propagate();
 
diff --git a/src/prop/cnf_stream.cpp b/src/prop/cnf_stream.cpp
index e0697735f..0d133aa13 100644
--- a/src/prop/cnf_stream.cpp
+++ b/src/prop/cnf_stream.cpp
@@ -44,7 +44,6 @@ using namespace CVC4::kind;
 namespace CVC4 {
 namespace prop {
 
-
 CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, context::Context* context, bool fullLitToNodeMap) :
   d_satSolver(satSolver),
   d_booleanVariables(context),
@@ -52,6 +51,7 @@ CnfStream::CnfStream(SatSolver *satSolver, Registrar* registrar, context::Contex
   d_literalToNodeMap(context),
   d_fullLitToNodeMap(fullLitToNodeMap),
   d_registrar(registrar),
+  d_assertionTable(context),
   d_removable(false) {
 }
 
@@ -74,7 +74,7 @@ void CnfStream::assertClause(TNode node, SatClause& c) {
       Dump("clauses") << AssertCommand(Expr(n.toExpr()));
     }
   }
-  d_satSolver->addClause(c, d_removable);
+  d_satSolver->addClause(c, d_removable, d_proofId);
 }
 
 void CnfStream::assertClause(TNode node, SatLiteral a) {
@@ -104,9 +104,9 @@ bool CnfStream::hasLiteral(TNode n) const {
 }
 
 void TseitinCnfStream::ensureLiteral(TNode n) {
-
-  // These are not removable
+  // 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)) {
@@ -188,9 +188,12 @@ SatLiteral CnfStream::newLiteral(TNode node, bool isTheoryAtom, bool preRegister
 
   // If a theory literal, we pre-register it
   if (preRegister) {
-    bool backup = d_removable;
+    // In case we are re-entered due to lemmas, save our state
+    bool backupRemovable = d_removable;
+    uint64_t backupProofId= d_proofId;
     d_registrar->preRegister(node);
-    d_removable = backup;
+    d_removable = backupRemovable;
+    d_proofId = backupProofId;
   }
 
   // Here, you can have it
@@ -642,9 +645,20 @@ void TseitinCnfStream::convertAndAssertIte(TNode node, bool negated) {
 // At the top level we must ensure that all clauses that are asserted are
 // not unit, except for the direct assertions. This allows us to remove the
 // clauses later when they are not needed anymore (lemmas for example).
-void TseitinCnfStream::convertAndAssert(TNode node, bool removable, bool negated) {
+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) & 0xffffffff00000000) == 0 && (assertionTableIndex & 0xffffffff00000000) == 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 ix " << 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);
 }
 
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h
index 266362ef5..b76051279 100644
--- a/src/prop/cnf_stream.h
+++ b/src/prop/cnf_stream.h
@@ -28,6 +28,7 @@
 #include "expr/node.h"
 #include "prop/theory_proxy.h"
 #include "prop/registrar.h"
+#include "proof/proof_manager.h"
 #include "context/cdlist.h"
 #include "context/cdinsert_hashmap.h"
 
@@ -36,7 +37,6 @@
 namespace CVC4 {
 namespace prop {
 
-
 class PropEngine;
 
 /**
@@ -77,6 +77,9 @@ protected:
   /** The "registrar" for pre-registration of terms */
   Registrar* d_registrar;
 
+  /** A table of assertions, used for regenerating proofs. */
+  context::CDList<Node> d_assertionTable;
+
   /**
    * How many literals were already mapped at the top-level when we
    * tried to convertAndAssert() something.  This
@@ -104,10 +107,18 @@ 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 as
-   * removable.
+   * need to be passed on over the stack.  Only pure clauses can be asserted
+   * as removable.
    */
   bool d_removable;
 
@@ -190,7 +201,7 @@ public:
    * @param removable whether the sat solver can choose to remove the clauses
    * @param negated whether we are asserting the node negated
    */
-  virtual void convertAndAssert(TNode node, bool removable, bool negated) = 0;
+  virtual void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null()) = 0;
 
   /**
    * Get the node that is represented by the given SatLiteral.
@@ -223,6 +234,13 @@ 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;
@@ -258,7 +276,7 @@ public:
    * @param removable is this something that can be erased
    * @param negated true if negated
    */
-  void convertAndAssert(TNode node, bool removable, bool negated);
+  void convertAndAssert(TNode node, bool removable, bool negated, ProofRule proof_id, TNode from = TNode::null());
 
   /**
    * Constructs the stream to use the given sat solver.
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index b0d710d66..5403b992e 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -135,8 +135,8 @@ 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); )
-  PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT); )
+  PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varTrue, false), INPUT, uint64_t(-1)); )
+  PROOF( ProofManager::getSatProof()->registerUnitClause(mkLit(varFalse, true), INPUT, uint64_t(-1)); )
 }
 
 
@@ -263,7 +263,7 @@ CRef Solver::reason(Var x) {
 
     // Construct the reason
     CRef real_reason = ca.alloc(explLevel, explanation, true);
-    PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA); );
+    PROOF (ProofManager::getSatProof()->registerClause(real_reason, THEORY_LEMMA, (uint64_t(RULE_CONFLICT) << 32)); );
     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 +271,7 @@ CRef Solver::reason(Var x) {
     return real_reason;
 }
 
-bool Solver::addClause_(vec<Lit>& ps, bool removable)
+bool Solver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
 {
     if (!ok) return false;
 
@@ -321,6 +321,8 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
       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);
     } else {
       // If all false, we're in conflict
       if (ps.size() == falseLiteralsCount) {
@@ -329,7 +331,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
           // 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( ProofManager::getSatProof()->storeUnitConflict(ps[0], INPUT, proof_id); )
             PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); )
             return ok = false;
           }
@@ -351,7 +353,7 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
 	attachClause(cr);
 
         if(PROOF_ON()) {
-          PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT); )
+          PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT, proof_id); )
           if(ps.size() == falseLiteralsCount) {
             PROOF( ProofManager::getSatProof()->finalizeProof(cr); )
             return ok = false;
@@ -364,11 +366,12 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
         if(assigns[var(ps[0])] == l_Undef) {
           assert(assigns[var(ps[0])] != l_False);
           uncheckedEnqueue(ps[0], cr);
-          PROOF( if(ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT); } );
+          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); } );
           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( ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT, proof_id); );
               PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); )
             } else {
               PROOF( ProofManager::getSatProof()->finalizeProof(confl); );
@@ -842,7 +845,7 @@ CRef Solver::propagate(TheoryCheckType type)
             propagateTheory();
             // If there are lemmas (or conflicts) update them
             if (lemmas.size() > 0) {
-                confl = updateLemmas();
+              confl = updateLemmas();
             }
         } else {
           // Even though in conflict, we still need to discharge the lemmas
@@ -891,7 +894,7 @@ void Solver::propagateTheory() {
         proxy->explainPropagation(MinisatSatSolver::toSatLiteral(p), explanation_cl);
         vec<Lit> explanation;
         MinisatSatSolver::toMinisatClause(explanation_cl, explanation);
-        addClause(explanation, true);
+        addClause(explanation, true, 0);
       }
     }
   }
@@ -1645,6 +1648,8 @@ CRef Solver::updateLemmas() {
     // 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;
@@ -1659,7 +1664,7 @@ CRef Solver::updateLemmas() {
       }
 
       lemma_ref = ca.alloc(clauseLevel, lemma, removable);
-      PROOF( ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA); );
+      PROOF( ProofManager::getSatProof()->registerClause(lemma_ref, THEORY_LEMMA, proof_id); );
       if (removable) {
         clauses_removable.push(lemma_ref);
       } else {
@@ -1667,7 +1672,7 @@ CRef Solver::updateLemmas() {
       }
       attachClause(lemma_ref);
     } else {
-      PROOF( ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); );
+      PROOF( ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA, proof_id); );
     }
 
     // If the lemma is propagating enqueue its literal (or set the conflict)
@@ -1681,7 +1686,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]); );
+            PROOF( ProofManager::getSatProof()->storeUnitConflict(lemma[0], LEARNT, proof_id); );
           }
         } else {
           Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;
@@ -1694,6 +1699,7 @@ CRef Solver::updateLemmas() {
   // Clear the lemmas
   lemmas.clear();
   lemmas_removable.clear();
+  lemmas_proof_id.clear();
 
   if (conflict != CRef_Undef) {
     theoryConflict = true;
diff --git a/src/prop/minisat/core/Solver.h b/src/prop/minisat/core/Solver.h
index 7831f211b..2d70cfeef 100644
--- a/src/prop/minisat/core/Solver.h
+++ b/src/prop/minisat/core/Solver.h
@@ -37,12 +37,11 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #include "expr/command.h"
 
 namespace CVC4 {
-class SatProof;
-
-namespace prop {
-  class TheoryProxy;
-}/* CVC4::prop namespace */
+  class SatProof;
 
+  namespace prop {
+    class TheoryProxy;
+  }/* CVC4::prop namespace */
 }/* CVC4 namespace */
 
 namespace Minisat {
@@ -85,6 +84,9 @@ protected:
   /** Is the lemma removable */
   vec<bool> lemmas_removable;
 
+  /** Proof IDs for lemmas */
+  vec<uint64_t> lemmas_proof_id;
+
   /** Do a another check if FULL_EFFORT was the last one */
   bool recheck;
 
@@ -154,12 +156,14 @@ public:
     void          push                     ();
     void          pop                      ();
 
-    bool    addClause (const vec<Lit>& ps, bool removable);                     // Add a clause to the solver.
+    // 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);                                  // Add a unit clause to the solver.
-    bool    addClause (Lit p, Lit q, bool removable);                           // Add a binary clause to the solver.
-    bool    addClause (Lit p, Lit q, Lit r, bool removable);                    // Add a ternary clause to the solver.
-    bool    addClause_(      vec<Lit>& ps, bool removable);                     // Add a clause to the solver without making superflous internal copy. Will
+    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
                                                                                  // change the passed vector 'ps'.
 
     // Solving:
@@ -489,11 +493,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)    { ps.copyTo(add_tmp); return addClause_(add_tmp, removable); }
-inline bool     Solver::addEmptyClause  (bool removable)                        { add_tmp.clear(); return addClause_(add_tmp, removable); }
-inline bool     Solver::addClause       (Lit p, bool removable)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable); }
-inline bool     Solver::addClause       (Lit p, Lit q, bool removable)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); }
-inline bool     Solver::addClause       (Lit p, Lit q, Lit r, bool removable)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); }
+inline bool     Solver::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::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/minisat.cpp b/src/prop/minisat/minisat.cpp
index 4a192d0d2..b50c1c09f 100644
--- a/src/prop/minisat/minisat.cpp
+++ b/src/prop/minisat/minisat.cpp
@@ -149,10 +149,10 @@ void MinisatSatSolver::setupOptions() {
   d_minisat->restart_inc = options::satRestartInc();
 }
 
-void MinisatSatSolver::addClause(SatClause& clause, bool removable) {
+void MinisatSatSolver::addClause(SatClause& clause, bool removable, uint64_t proof_id) {
   Minisat::vec<Minisat::Lit> minisat_clause;
   toMinisatClause(clause, minisat_clause);
-  d_minisat->addClause(minisat_clause, removable);
+  d_minisat->addClause(minisat_clause, removable, proof_id);
 }
 
 SatVariable MinisatSatSolver::newVar(bool isTheoryAtom, bool preRegister, bool canErase) {
@@ -228,7 +228,7 @@ void MinisatSatSolver::push() {
   d_minisat->push();
 }
 
-void MinisatSatSolver::pop(){
+void MinisatSatSolver::pop() {
   d_minisat->pop();
 }
 
diff --git a/src/prop/minisat/minisat.h b/src/prop/minisat/minisat.h
index b37371d98..3992f1adb 100644
--- a/src/prop/minisat/minisat.h
+++ b/src/prop/minisat/minisat.h
@@ -53,7 +53,7 @@ public:
   static void  toSatClause    (const Minisat::Clause& clause, SatClause& sat_clause);
   void initialize(context::Context* context, TheoryProxy* theoryProxy);
 
-  void addClause(SatClause& clause, bool removable);
+  void addClause(SatClause& clause, bool removable, uint64_t proof_id);
 
   SatVariable newVar(bool isTheoryAtom, bool preRegister, bool canErase);
   SatVariable trueVar() { return d_minisat->trueVar(); }
diff --git a/src/prop/minisat/simp/SimpSolver.cc b/src/prop/minisat/simp/SimpSolver.cc
index 6dcdb76c7..71e747f72 100644
--- a/src/prop/minisat/simp/SimpSolver.cc
+++ b/src/prop/minisat/simp/SimpSolver.cc
@@ -159,7 +159,7 @@ lbool SimpSolver::solve_(bool do_simp, bool turn_off_simp)
 
 
 
-bool SimpSolver::addClause_(vec<Lit>& ps, bool removable)
+bool SimpSolver::addClause_(vec<Lit>& ps, bool removable, uint64_t proof_id)
 {
 #ifndef NDEBUG
     if (use_simplification) {
@@ -173,7 +173,7 @@ bool SimpSolver::addClause_(vec<Lit>& ps, bool removable)
     if (use_rcheck && implied(ps))
         return true;
 
-    if (!Solver::addClause_(ps, removable))
+    if (!Solver::addClause_(ps, removable, proof_id))
         return false;
 
     if (use_simplification && clauses_persistent.size() == nclauses + 1){
@@ -545,7 +545,7 @@ bool SimpSolver::eliminateVar(Var v)
     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)) {
+            if (merge(ca[pos[i]], ca[neg[j]], v, resolvent) && !addClause_(resolvent, removable, uint64_t(-1))) {
                 return false;
             }
         }
@@ -585,7 +585,7 @@ bool SimpSolver::substitute(Var v, Lit x)
 
         removeClause(cls[i]);
 
-        if (!addClause_(subst_clause, c.removable())) {
+        if (!addClause_(subst_clause, c.removable(), uint64_t(-1))) {
             return ok = false;
         }
     }
diff --git a/src/prop/minisat/simp/SimpSolver.h b/src/prop/minisat/simp/SimpSolver.h
index 878d799a5..041309546 100644
--- a/src/prop/minisat/simp/SimpSolver.h
+++ b/src/prop/minisat/simp/SimpSolver.h
@@ -47,12 +47,12 @@ class SimpSolver : public Solver {
     // Problem specification:
     //
     Var     newVar    (bool polarity = true, bool dvar = true, bool isTheoryAtom = false, bool preRegister = false, bool canErase = true);
-    bool    addClause (const vec<Lit>& ps, bool removable);
-    bool    addEmptyClause(bool removable);                  // Add the empty clause to the solver.
-    bool    addClause (Lit p, bool removable);               // Add a unit clause to the solver.
-    bool    addClause (Lit p, Lit q, bool removable);        // Add a binary clause to the solver.
-    bool    addClause (Lit p, Lit q, Lit r, bool removable); // Add a ternary clause to the solver.
-    bool    addClause_(vec<Lit>& ps, bool removable);
+    bool    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    substitute(Var v, Lit x);  // Replace all occurences of v with x (may cause a contradiction).
 
     // Variable mode:
@@ -182,11 +182,15 @@ inline void SimpSolver::updateElimHeap(Var v) {
         elim_heap.update(v); }
 
 
-inline bool SimpSolver::addClause    (const vec<Lit>& ps, bool removable)    { ps.copyTo(add_tmp); return addClause_(add_tmp, removable); }
-inline bool SimpSolver::addEmptyClause(bool removable)                       { add_tmp.clear(); return addClause_(add_tmp, removable); }
-inline bool SimpSolver::addClause    (Lit p, bool removable)                 { add_tmp.clear(); add_tmp.push(p); return addClause_(add_tmp, removable); }
-inline bool SimpSolver::addClause    (Lit p, Lit q, bool removable)          { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); return addClause_(add_tmp, removable); }
-inline bool SimpSolver::addClause    (Lit p, Lit q, Lit r, bool removable)   { add_tmp.clear(); add_tmp.push(p); add_tmp.push(q); add_tmp.push(r); return addClause_(add_tmp, removable); }
+inline 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 void SimpSolver::setFrozen    (Var v, bool b) { frozen[v] = (char)b; if (use_simplification && !b) { updateElimHeap(v); } }
 
 inline bool SimpSolver::solve        (                     bool do_simp, bool turn_off_simp)  { budgetOff(); assumptions.clear(); return solve_(do_simp, turn_off_simp) == l_True; }
diff --git a/src/prop/prop_engine.cpp b/src/prop/prop_engine.cpp
index 82c0bae1a..a02e40e32 100644
--- a/src/prop/prop_engine.cpp
+++ b/src/prop/prop_engine.cpp
@@ -25,6 +25,7 @@
 #include "decision/options.h"
 #include "theory/theory_engine.h"
 #include "theory/theory_registrar.h"
+#include "proof/proof_manager.h"
 #include "util/cvc4_assert.h"
 #include "options/options.h"
 #include "smt/options.h"
@@ -109,15 +110,15 @@ void PropEngine::assertFormula(TNode node) {
   Assert(!d_inCheckSat, "Sat solver in solve()!");
   Debug("prop") << "assertFormula(" << node << ")" << endl;
   // Assert as non-removable
-  d_cnfStream->convertAndAssert(node, false, false);
+  d_cnfStream->convertAndAssert(node, false, false, RULE_GIVEN);
 }
 
-void PropEngine::assertLemma(TNode node, bool negated, bool removable) {
+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;
 
-  // Assert as removable
-  d_cnfStream->convertAndAssert(node, removable, negated);
+  // Assert as (possibly) removable
+  d_cnfStream->convertAndAssert(node, removable, negated, rule, from);
 }
 
 void PropEngine::requirePhase(TNode n, bool phase) {
diff --git a/src/prop/prop_engine.h b/src/prop/prop_engine.h
index a5132e3da..ed022a64f 100644
--- a/src/prop/prop_engine.h
+++ b/src/prop/prop_engine.h
@@ -25,6 +25,7 @@
 #include "options/options.h"
 #include "util/result.h"
 #include "smt/modal_exception.h"
+#include "proof/proof_manager.h"
 #include <sys/time.h>
 
 namespace CVC4 {
@@ -199,7 +200,7 @@ public:
    * @param removable whether this lemma can be quietly removed based
    * on an activity heuristic (or not)
    */
-  void assertLemma(TNode node, bool negated, bool removable);
+  void assertLemma(TNode node, bool negated, bool removable, ProofRule rule, TNode from = TNode::null());
 
   /**
    * If ever n is decided upon, it must be in the given phase.  This
diff --git a/src/prop/sat_solver.h b/src/prop/sat_solver.h
index 8e7e53474..e3b0f3449 100644
--- a/src/prop/sat_solver.h
+++ b/src/prop/sat_solver.h
@@ -24,6 +24,7 @@
 #include "util/statistics_registry.h"
 #include "context/cdlist.h"
 #include "prop/sat_solver_types.h"
+#include "expr/node.h"
 
 namespace CVC4 {
 namespace prop {
@@ -38,7 +39,7 @@ public:
   virtual ~SatSolver() { }
 
   /** Assert a clause in the solver. */
-  virtual void addClause(SatClause& clause, bool removable) = 0;
+  virtual void addClause(SatClause& clause, bool removable, uint64_t proof_id) = 0;
 
   /**
    * Create a new boolean variable in the solver.
diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp
index 67325cb18..2bcd48099 100644
--- a/src/prop/theory_proxy.cpp
+++ b/src/prop/theory_proxy.cpp
@@ -122,7 +122,7 @@ void TheoryProxy::notifyRestart() {
           if(lemmaCount % 1 == 0) {
             Debug("shared") << "=) " << asNode << std::endl;
           }
-          d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true);
+          d_propEngine->assertLemma(d_theoryEngine->preprocess(asNode), false, true, RULE_INVALID);
         } else {
           Debug("shared") << "=(" << asNode << std::endl;
         }
diff --git a/src/smt/options b/src/smt/options
index 9c7eea12f..3ee3dbecb 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -37,9 +37,11 @@ option dumpProofs --dump-proofs bool :default false :link --proof
  output proofs after every UNSAT/VALID response
 option dumpInstantiations --dump-instantiations bool :default false
  output instantiations of quantified formulas after every UNSAT/VALID response
-# this is just a placeholder for later; it doesn't show up in command-line options listings
-undocumented-option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::unsatCoresEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
- turn on unsat core generation (NOT YET SUPPORTED)
+option unsatCores produce-unsat-cores --produce-unsat-cores bool :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+ turn on unsat core generation
+option dumpUnsatCores --dump-unsat-cores bool :default false :link --produce-unsat-cores :link-smt produce-unsat-cores :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+ output unsat cores after every UNSAT/VALID response
+
 option produceAssignments produce-assignments --produce-assignments bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  support the get-assignment command
 
diff --git a/src/smt/options_handlers.h b/src/smt/options_handlers.h
index 61e17801d..fcd625267 100644
--- a/src/smt/options_handlers.h
+++ b/src/smt/options_handlers.h
@@ -153,10 +153,6 @@ batch (default) \n\
   (MiniSat) propagation for all of them only after reaching a querying command\n\
   (CHECKSAT or QUERY or predicate SUBTYPE declaration)\n\
 \n\
-incremental\n\
-+ run nonclausal simplification and clausal propagation at each ASSERT\n\
-  (and at CHECKSAT/QUERY/SUBTYPE)\n\
-\n\
 none\n\
 + do not perform nonclausal simplification\n\
 ";
@@ -283,8 +279,6 @@ inline LogicInfo stringToLogicInfo(std::string option, std::string optarg, SmtEn
 inline SimplificationMode stringToSimplificationMode(std::string option, std::string optarg, SmtEngine* smt) throw(OptionException) {
   if(optarg == "batch") {
     return SIMPLIFICATION_MODE_BATCH;
-  } else if(optarg == "incremental") {
-    return SIMPLIFICATION_MODE_INCREMENTAL;
   } else if(optarg == "none") {
     return SIMPLIFICATION_MODE_NONE;
   } else if(optarg == "help") {
@@ -316,12 +310,6 @@ inline void proofEnabledBuild(std::string option, bool value, SmtEngine* smt) th
 #endif /* CVC4_PROOF */
 }
 
-inline void unsatCoresEnabledBuild(std::string option, bool value, SmtEngine* smt) throw(OptionException) {
-  if(value) {
-    throw UnrecognizedOptionException("CVC4 does not yet have support for unsatisfiable cores");
-  }
-}
-
 // This macro is used for setting :regular-output-channel and :diagnostic-output-channel
 // to redirect a stream.  It maintains all attributes set on the stream.
 #define __CVC4__SMT__OUTPUTCHANNELS__SETSTREAM__(__channel_get, __channel_set) \
diff --git a/src/smt/simplification_mode.cpp b/src/smt/simplification_mode.cpp
index f728fa862..be46badfc 100644
--- a/src/smt/simplification_mode.cpp
+++ b/src/smt/simplification_mode.cpp
@@ -21,9 +21,6 @@ namespace CVC4 {
 
 std::ostream& operator<<(std::ostream& out, SimplificationMode mode) {
   switch(mode) {
-  case SIMPLIFICATION_MODE_INCREMENTAL:
-    out << "SIMPLIFICATION_MODE_INCREMENTAL";
-    break;
   case SIMPLIFICATION_MODE_BATCH:
     out << "SIMPLIFICATION_MODE_BATCH";
     break;
diff --git a/src/smt/simplification_mode.h b/src/smt/simplification_mode.h
index 2242e8bdf..b0b78d318 100644
--- a/src/smt/simplification_mode.h
+++ b/src/smt/simplification_mode.h
@@ -26,8 +26,6 @@ namespace CVC4 {
 
 /** Enumeration of simplification modes (when to simplify). */
 typedef enum {
-  /** Simplify the assertions as they come in */
-  SIMPLIFICATION_MODE_INCREMENTAL,
   /** Simplify the assertions all together once a check is requested */
   SIMPLIFICATION_MODE_BATCH,
   /** Don't do simplification */
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 77ee362c0..7b1f99403 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -48,6 +48,7 @@
 #include "theory/bv/theory_bv_rewriter.h"
 #include "proof/proof_manager.h"
 #include "main/options.h"
+#include "util/unsat_core.h"
 #include "util/proof.h"
 #include "proof/proof.h"
 #include "proof/proof_manager.h"
@@ -137,6 +138,30 @@ public:
   Node getFormula() const { return d_formula; }
 };/* class DefinedFunction */
 
+class AssertionPipeline {
+  vector<Node> d_nodes;
+
+public:
+
+  size_t size() const { return d_nodes.size(); }
+
+  void resize(size_t n) { d_nodes.resize(n); }
+  void clear() { d_nodes.clear(); }
+
+  Node& operator[](size_t i) { return d_nodes[i]; }
+  const Node& operator[](size_t i) const { return d_nodes[i]; }
+  void push_back(Node n) { d_nodes.push_back(n); }
+
+  vector<Node>& ref() { return d_nodes; }
+  const vector<Node>& ref() const { return d_nodes; }
+
+  void replace(size_t i, Node n) {
+    PROOF( ProofManager::currentPM()->addDependence(n, d_nodes[i]); );
+    d_nodes[i] = n;
+  }
+
+};/* class AssertionPipeline */
+
 struct SmtEngineStatistics {
   /** time spent in definition-expansion */
   TimerStat d_definitionExpansionTime;
@@ -160,6 +185,8 @@ struct SmtEngineStatistics {
   TimerStat d_iteRemovalTime;
   /** time spent in theory preprocessing */
   TimerStat d_theoryPreprocessTime;
+  /** time spent in theory preprocessing */
+  TimerStat d_rewriteApplyToConstTime;
   /** time spent converting to CNF */
   TimerStat d_cnfConversionTime;
   /** Num of assertions before ite removal */
@@ -192,6 +219,7 @@ struct SmtEngineStatistics {
     d_unconstrainedSimpTime("smt::SmtEngine::unconstrainedSimpTime"),
     d_iteRemovalTime("smt::SmtEngine::iteRemovalTime"),
     d_theoryPreprocessTime("smt::SmtEngine::theoryPreprocessTime"),
+    d_rewriteApplyToConstTime("smt::SmtEngine::rewriteApplyToConstTime"),
     d_cnfConversionTime("smt::SmtEngine::cnfConversionTime"),
     d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
     d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
@@ -214,10 +242,12 @@ struct SmtEngineStatistics {
     StatisticsRegistry::registerStat(&d_unconstrainedSimpTime);
     StatisticsRegistry::registerStat(&d_iteRemovalTime);
     StatisticsRegistry::registerStat(&d_theoryPreprocessTime);
+    StatisticsRegistry::registerStat(&d_rewriteApplyToConstTime);
     StatisticsRegistry::registerStat(&d_cnfConversionTime);
     StatisticsRegistry::registerStat(&d_numAssertionsPre);
     StatisticsRegistry::registerStat(&d_numAssertionsPost);
     StatisticsRegistry::registerStat(&d_checkModelTime);
+    StatisticsRegistry::registerStat(&d_checkProofTime);
     StatisticsRegistry::registerStat(&d_solveTime);
     StatisticsRegistry::registerStat(&d_pushPopTime);
     StatisticsRegistry::registerStat(&d_processAssertionsTime);
@@ -236,10 +266,12 @@ struct SmtEngineStatistics {
     StatisticsRegistry::unregisterStat(&d_unconstrainedSimpTime);
     StatisticsRegistry::unregisterStat(&d_iteRemovalTime);
     StatisticsRegistry::unregisterStat(&d_theoryPreprocessTime);
+    StatisticsRegistry::unregisterStat(&d_rewriteApplyToConstTime);
     StatisticsRegistry::unregisterStat(&d_cnfConversionTime);
     StatisticsRegistry::unregisterStat(&d_numAssertionsPre);
     StatisticsRegistry::unregisterStat(&d_numAssertionsPost);
     StatisticsRegistry::unregisterStat(&d_checkModelTime);
+    StatisticsRegistry::unregisterStat(&d_checkProofTime);
     StatisticsRegistry::unregisterStat(&d_solveTime);
     StatisticsRegistry::unregisterStat(&d_pushPopTime);
     StatisticsRegistry::unregisterStat(&d_processAssertionsTime);
@@ -264,9 +296,6 @@ struct SmtEngineStatistics {
 class SmtEnginePrivate : public NodeManagerListener {
   SmtEngine& d_smt;
 
-  /** The assertions yet to be preprocessed */
-  vector<Node> d_assertionsToPreprocess;
-
   /** Learned literals */
   vector<Node> d_nonClausalLearnedLiterals;
 
@@ -281,8 +310,8 @@ class SmtEnginePrivate : public NodeManagerListener {
   bool d_propagatorNeedsFinish;
   std::vector<Node> d_boolVars;
 
-  /** Assertions to push to sat */
-  vector<Node> d_assertionsToCheck;
+  /** Assertions in the preprocessing pipeline */
+  AssertionPipeline d_assertions;
 
   /** Whether any assertions have been processed */
   CDO<bool> d_assertionsProcessed;
@@ -319,7 +348,7 @@ class SmtEnginePrivate : public NodeManagerListener {
 
 public:
   /**
-   * Map from skolem variables to index in d_assertionsToCheck containing
+   * Map from skolem variables to index in d_assertions containing
    * corresponding introduced Boolean ite
    */
   IteSkolemMap d_iteSkolemMap;
@@ -375,7 +404,7 @@ private:
   bool simpITE();
 
   // Simplify based on unconstrained values
-  void unconstrainedSimp(std::vector<Node>& assertions);
+  void unconstrainedSimp();
 
   // Ensures the assertions asserted after before now
   // effectively come before d_realAssertionsEnd
@@ -386,7 +415,7 @@ private:
    * (predicate subtype or integer subrange type) must be constrained
    * to be in that type.
    */
-  void constrainSubtypes(TNode n, std::vector<Node>& assertions)
+  void constrainSubtypes(TNode n, AssertionPipeline& assertions)
     throw();
 
   // trace nodes back to their assertions using CircuitPropagator's BackEdgesMap
@@ -410,13 +439,12 @@ public:
 
   SmtEnginePrivate(SmtEngine& smt) :
     d_smt(smt),
-    d_assertionsToPreprocess(),
     d_nonClausalLearnedLiterals(),
     d_realAssertionsEnd(0),
     d_booleanTermConverter(NULL),
     d_propagator(d_nonClausalLearnedLiterals, true, true),
     d_propagatorNeedsFinish(false),
-    d_assertionsToCheck(),
+    d_assertions(),
     d_assertionsProcessed(smt.d_userContext, false),
     d_substitutionsIndex(smt.d_userContext, 0),
     d_fakeContext(),
@@ -508,9 +536,8 @@ public:
    * someone does a push-assert-pop without a check-sat.
    */
   void notifyPop() {
-    d_assertionsToPreprocess.clear();
+    d_assertions.clear();
     d_nonClausalLearnedLiterals.clear();
-    d_assertionsToCheck.clear();
     d_realAssertionsEnd = 0;
     d_iteSkolemMap.clear();
   }
@@ -546,7 +573,7 @@ public:
     hash_map<Node, Node, NodeHashFunction> cache;
     Node n = expandDefinitions(in, cache).toExpr();
     // Make sure we've done all preprocessing, etc.
-    Assert(d_assertionsToCheck.size() == 0 && d_assertionsToPreprocess.size() == 0);
+    Assert(d_assertions.size() == 0);
     return applySubstitutions(n).toExpr();
   }
 
@@ -919,6 +946,64 @@ void SmtEngine::setDefaults() {
     }
   }
 
+  if(options::unsatCores()) {
+    if(options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
+      if(options::simplificationMode.wasSetByUser()) {
+        throw OptionException("simplification not supported with unsat cores");
+      }
+      Notice() << "SmtEngine: turning off simplification to support unsat-cores" << endl;
+      options::simplificationMode.set(SIMPLIFICATION_MODE_NONE);
+    }
+
+    if(options::unconstrainedSimp()) {
+      if(options::unconstrainedSimp.wasSetByUser()) {
+        throw OptionException("unconstrained simplification not supported with unsat cores");
+      }
+      Notice() << "SmtEngine: turning off unconstrained simplification to support unsat-cores" << endl;
+      options::unconstrainedSimp.set(false);
+    }
+
+    if(options::pbRewrites()) {
+      if(options::pbRewrites.wasSetByUser()) {
+        throw OptionException("pseudoboolean rewrites not supported with unsat cores");
+      }
+      Notice() << "SmtEngine: turning off pseudoboolean rewrites to support unsat-cores" << endl;
+      setOption("pb-rewrites", false);
+    }
+
+    if(options::sortInference()) {
+      if(options::sortInference.wasSetByUser()) {
+        throw OptionException("sort inference not supported with unsat cores");
+      }
+      Notice() << "SmtEngine: turning off sort inference to support unsat-cores" << endl;
+      options::sortInference.set(false);
+    }
+
+    if(options::preSkolemQuant()) {
+      if(options::preSkolemQuant.wasSetByUser()) {
+        throw OptionException("pre-skolemization not supported with unsat cores");
+      }
+      Notice() << "SmtEngine: turning off pre-skolemization to support unsat-cores" << endl;
+      options::preSkolemQuant.set(false);
+    }
+
+    if(options::bitvectorToBool()) {
+      if(options::bitvectorToBool.wasSetByUser()) {
+        throw OptionException("bv-to-bool not supported with unsat cores");
+      }
+      Notice() << "SmtEngine: turning off bitvector-to-bool support unsat-cores" << endl;
+      options::bitvectorToBool.set(false);
+    }
+
+    if(options::bvIntroducePow2()) {
+      if(options::bvIntroducePow2.wasSetByUser()) {
+        throw OptionException("bv-intro-pow2 not supported with unsat cores");
+      }
+      Notice() << "SmtEngine: turning off bv-introduce-pow2 to support unsat-cores" << endl;
+      setOption("bv-intro-pow2", false);
+    }
+  }
+
   if(options::produceAssignments() && !options::produceModels()) {
     Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl;
     setOption("produce-models", SExpr("true"));
@@ -1626,11 +1711,10 @@ void SmtEnginePrivate::removeITEs() {
   Trace("simplify") << "SmtEnginePrivate::removeITEs()" << endl;
 
   // Remove all of the ITE occurrences and normalize
-  d_iteRemover.run(d_assertionsToCheck, d_iteSkolemMap);
-  for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
-    d_assertionsToCheck[i] = Rewriter::rewrite(d_assertionsToCheck[i]);
+  d_iteRemover.run(d_assertions.ref(), d_iteSkolemMap, true);
+  for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+    d_assertions.replace(i, Rewriter::rewrite(d_assertions[i]));
   }
-
 }
 
 void SmtEnginePrivate::staticLearning() {
@@ -1640,22 +1724,21 @@ void SmtEnginePrivate::staticLearning() {
 
   Trace("simplify") << "SmtEnginePrivate::staticLearning()" << endl;
 
-  for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
+  for (unsigned i = 0; i < d_assertions.size(); ++ i) {
 
     NodeBuilder<> learned(kind::AND);
-    learned << d_assertionsToCheck[i];
-    d_smt.d_theoryEngine->ppStaticLearn(d_assertionsToCheck[i], learned);
+    learned << d_assertions[i];
+    d_smt.d_theoryEngine->ppStaticLearn(d_assertions[i], learned);
     if(learned.getNumChildren() == 1) {
       learned.clear();
     } else {
-      d_assertionsToCheck[i] = learned;
+      d_assertions.replace(i, learned);
     }
   }
 }
 
 // do dumping (before/after any preprocessing pass)
-static void dumpAssertions(const char* key,
-                           const std::vector<Node>& assertionList) {
+static void dumpAssertions(const char* key, const AssertionPipeline& assertionList) {
   if( Dump.isOn("assertions") &&
       Dump.isOn(string("assertions:") + key) ) {
     // Push the simplified assertions to the dump output stream
@@ -1684,14 +1767,15 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   // Assert all the assertions to the propagator
   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                     << "asserting to propagator" << endl;
-  for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
-    Assert(Rewriter::rewrite(d_assertionsToPreprocess[i]) == d_assertionsToPreprocess[i]);
+  for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+    Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]);
     // Don't reprocess substitutions
     if (d_substitutionsIndex > 0 && i == d_substitutionsIndex) {
       continue;
     }
-    Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertionsToPreprocess[i] << endl;
-    d_propagator.assertTrue(d_assertionsToPreprocess[i]);
+    Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): asserting " << d_assertions[i] << endl;
+    Debug("cores") << "d_propagator assertTrue: " << d_assertions[i] << std::endl;
+    d_propagator.assertTrue(d_assertions[i]);
   }
 
   Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
@@ -1700,8 +1784,10 @@ bool SmtEnginePrivate::nonClausalSimplify() {
     // If in conflict, just return false
     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                       << "conflict in non-clausal propagation" << endl;
-    d_assertionsToPreprocess.clear();
-    d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
+    Node falseNode = NodeManager::currentNM()->mkConst<bool>(false);
+    Assert(!options::unsatCores());
+    d_assertions.clear();
+    d_assertions.push_back(falseNode);
     d_propagatorNeedsFinish = true;
     return false;
   }
@@ -1738,8 +1824,9 @@ bool SmtEnginePrivate::nonClausalSimplify() {
         Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                           << "conflict with "
                           << d_nonClausalLearnedLiterals[i] << endl;
-        d_assertionsToPreprocess.clear();
-        d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
+        Assert(!options::unsatCores());
+        d_assertions.clear();
+        d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(false));
         d_propagatorNeedsFinish = true;
         return false;
       }
@@ -1773,8 +1860,9 @@ bool SmtEnginePrivate::nonClausalSimplify() {
         Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                           << "conflict while solving "
                           << learnedLiteral << endl;
-        d_assertionsToPreprocess.clear();
-        d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
+        Assert(!options::unsatCores());
+        d_assertions.clear();
+        d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(false));
         d_propagatorNeedsFinish = true;
         return false;
       default:
@@ -1799,8 +1887,8 @@ bool SmtEnginePrivate::nonClausalSimplify() {
           // constantPropagations.simplifyLHS(t, c, equations, true);
           // if (!equations.empty()) {
           //   Assert(equations[0].first.isConst() && equations[0].second.isConst() && equations[0].first != equations[0].second);
-          //   d_assertionsToPreprocess.clear();
-          //   d_assertionsToCheck.push_back(NodeManager::currentNM()->mkConst<bool>(false));
+          //   d_assertions.clear();
+          //   d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(false));
           //   return;
           // }
           // d_topLevelSubstitutions.simplifyRHS(constantPropagations);
@@ -1849,8 +1937,8 @@ bool SmtEnginePrivate::nonClausalSimplify() {
 
   hash_set<TNode, TNodeHashFunction> s;
   Trace("debugging") << "NonClausal simplify pre-preprocess\n";
-  for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
-    Node assertion = d_assertionsToPreprocess[i];
+  for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+    Node assertion = d_assertions[i];
     Node assertionNew = newSubstitutions.apply(assertion);
     Trace("debugging") << "assertion = " << assertion << endl;
     Trace("debugging") << "assertionNew = " << assertionNew << endl;
@@ -1871,17 +1959,16 @@ bool SmtEnginePrivate::nonClausalSimplify() {
     }
     Trace("debugging") << "\n";
     s.insert(assertion);
-    d_assertionsToCheck.push_back(assertion);
+    d_assertions.replace(i, assertion);
     Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
                       << "non-clausal preprocessed: "
                       << assertion << endl;
   }
-  d_assertionsToPreprocess.clear();
 
   // If in incremental mode, add substitutions to the list of assertions
   if (d_substitutionsIndex > 0) {
     NodeBuilder<> substitutionsBuilder(kind::AND);
-    substitutionsBuilder << d_assertionsToCheck[d_substitutionsIndex];
+    substitutionsBuilder << d_assertions[d_substitutionsIndex];
     pos = newSubstitutions.begin();
     for (; pos != newSubstitutions.end(); ++pos) {
       // Add back this substitution as an assertion
@@ -1891,8 +1978,8 @@ bool SmtEnginePrivate::nonClausalSimplify() {
       Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): will notify SAT layer of substitution: " << n << endl;
     }
     if (substitutionsBuilder.getNumChildren() > 1) {
-      d_assertionsToCheck[d_substitutionsIndex] =
-        Rewriter::rewrite(Node(substitutionsBuilder));
+      d_assertions.replace(d_substitutionsIndex,
+        Rewriter::rewrite(Node(substitutionsBuilder)));
     }
   } else {
     // If not in incremental mode, must add substitutions to model
@@ -1908,8 +1995,8 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   }
 
   NodeBuilder<> learnedBuilder(kind::AND);
-  Assert(d_realAssertionsEnd <= d_assertionsToCheck.size());
-  learnedBuilder << d_assertionsToCheck[d_realAssertionsEnd - 1];
+  Assert(d_realAssertionsEnd <= d_assertions.size());
+  learnedBuilder << d_assertions[d_realAssertionsEnd - 1];
 
   for (unsigned i = 0; i < d_nonClausalLearnedLiterals.size(); ++ i) {
     Node learned = d_nonClausalLearnedLiterals[i];
@@ -1938,7 +2025,6 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   }
   d_nonClausalLearnedLiterals.clear();
 
-
   for (pos = constantPropagations.begin(); pos != constantPropagations.end(); ++pos) {
     Node cProp = (*pos).first.eqNode((*pos).second);
     Assert(d_topLevelSubstitutions.apply(cProp) == cProp);
@@ -1963,8 +2049,8 @@ bool SmtEnginePrivate::nonClausalSimplify() {
   d_topLevelSubstitutions.addSubstitutions(newSubstitutions);
 
   if(learnedBuilder.getNumChildren() > 1) {
-    d_assertionsToCheck[d_realAssertionsEnd - 1] =
-      Rewriter::rewrite(Node(learnedBuilder));
+    d_assertions.replace(d_realAssertionsEnd - 1,
+      Rewriter::rewrite(Node(learnedBuilder)));
   }
 
   d_propagatorNeedsFinish = true;
@@ -1974,9 +2060,9 @@ bool SmtEnginePrivate::nonClausalSimplify() {
 void SmtEnginePrivate::bvAbstraction() {
   Trace("bv-abstraction") << "SmtEnginePrivate::bvAbstraction()" << endl;
   std::vector<Node> new_assertions;
-  bool changed = d_smt.d_theoryEngine->ppBvAbstraction(d_assertionsToPreprocess, new_assertions);
-  for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
-    d_assertionsToPreprocess[i] = Rewriter::rewrite(new_assertions[i]);
+  bool changed = d_smt.d_theoryEngine->ppBvAbstraction(d_assertions.ref(), new_assertions);
+  for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+    d_assertions.replace(i, Rewriter::rewrite(new_assertions[i]));
   }
   // if we are using the lazy solver and the abstraction
   // applies, then UF symbols were introduced
@@ -1991,9 +2077,9 @@ void SmtEnginePrivate::bvAbstraction() {
 void SmtEnginePrivate::bvToBool() {
   Trace("bv-to-bool") << "SmtEnginePrivate::bvToBool()" << endl;
   std::vector<Node> new_assertions;
-  d_smt.d_theoryEngine->ppBvToBool(d_assertionsToPreprocess, new_assertions);
-  for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
-    d_assertionsToPreprocess[i] = Rewriter::rewrite(new_assertions[i]);
+  d_smt.d_theoryEngine->ppBvToBool(d_assertions.ref(), new_assertions);
+  for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+    d_assertions.replace(i, Rewriter::rewrite(new_assertions[i]));
   }
 }
 
@@ -2002,23 +2088,23 @@ bool SmtEnginePrivate::simpITE() {
 
   Trace("simplify") << "SmtEnginePrivate::simpITE()" << endl;
 
-  unsigned numAssertionOnEntry = d_assertionsToCheck.size();
-  for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) {
-    Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertionsToCheck[i]);
-    d_assertionsToCheck[i] = result;
+  unsigned numAssertionOnEntry = d_assertions.size();
+  for (unsigned i = 0; i < d_assertions.size(); ++i) {
+    Node result = d_smt.d_theoryEngine->ppSimpITE(d_assertions[i]);
+    d_assertions.replace(i, result);
     if(result.isConst() && !result.getConst<bool>()){
       return false;
     }
   }
-  bool result = d_smt.d_theoryEngine->donePPSimpITE(d_assertionsToCheck);
-  if(numAssertionOnEntry < d_assertionsToCheck.size()){
+  bool result = d_smt.d_theoryEngine->donePPSimpITE(d_assertions.ref());
+  if(numAssertionOnEntry < d_assertions.size()){
     compressBeforeRealAssertions(numAssertionOnEntry);
   }
   return result;
 }
 
 void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){
-  size_t curr = d_assertionsToCheck.size();
+  size_t curr = d_assertions.size();
   if(before >= curr ||
      d_realAssertionsEnd <= 0 ||
      d_realAssertionsEnd >= curr){
@@ -2038,24 +2124,24 @@ void SmtEnginePrivate::compressBeforeRealAssertions(size_t before){
 
   std::vector<Node> intoConjunction;
   for(size_t i = before; i<curr; ++i){
-    intoConjunction.push_back(d_assertionsToCheck[i]);
+    intoConjunction.push_back(d_assertions[i]);
   }
-  d_assertionsToCheck.resize(before);
+  d_assertions.resize(before);
   size_t lastBeforeItes = d_realAssertionsEnd - 1;
-  intoConjunction.push_back(d_assertionsToCheck[lastBeforeItes]);
+  intoConjunction.push_back(d_assertions[lastBeforeItes]);
   Node newLast = util::NaryBuilder::mkAssoc(kind::AND, intoConjunction);
-  d_assertionsToCheck[lastBeforeItes] = newLast;
-  Assert(d_assertionsToCheck.size() == before);
+  d_assertions.replace(lastBeforeItes, newLast);
+  Assert(d_assertions.size() == before);
 }
 
-void SmtEnginePrivate::unconstrainedSimp(std::vector<Node>& assertions) {
+void SmtEnginePrivate::unconstrainedSimp() {
   TimerStat::CodeTimer unconstrainedSimpTimer(d_smt.d_stats->d_unconstrainedSimpTime);
   Trace("simplify") << "SmtEnginePrivate::unconstrainedSimp()" << endl;
-  d_smt.d_theoryEngine->ppUnconstrainedSimp(assertions);
+  d_smt.d_theoryEngine->ppUnconstrainedSimp(d_assertions.ref());
 }
 
 
-void SmtEnginePrivate::constrainSubtypes(TNode top, std::vector<Node>& assertions)
+void SmtEnginePrivate::constrainSubtypes(TNode top, AssertionPipeline& assertions)
   throw() {
 
   Trace("constrainSubtypes") << "constrainSubtypes(): looking at " << top << endl;
@@ -2177,8 +2263,7 @@ size_t SmtEnginePrivate::removeFromConjunction(Node& n, const std::hash_set<unsi
 }
 
 void SmtEnginePrivate::doMiplibTrick() {
-  Assert(d_assertionsToPreprocess.empty());
-  Assert(d_realAssertionsEnd == d_assertionsToCheck.size());
+  Assert(d_realAssertionsEnd == d_assertions.size());
   Assert(!options::incrementalSolving());
 
   const booleans::CircuitPropagator::BackEdgesMap& backEdges = d_propagator.getBackEdges();
@@ -2409,7 +2494,7 @@ void SmtEnginePrivate::doMiplibTrick() {
               Node newVar = nm->mkSkolem(ss.str(), nm->integerType(), "a variable introduced due to scrubbing a miplib encoding", NodeManager::SKOLEM_EXACT_NAME);
               Node geq = Rewriter::rewrite(nm->mkNode(kind::GEQ, newVar, zero));
               Node leq = Rewriter::rewrite(nm->mkNode(kind::LEQ, newVar, one));
-              d_assertionsToCheck.push_back(Rewriter::rewrite(geq.andNode(leq)));
+              d_assertions.push_back(Rewriter::rewrite(geq.andNode(leq)));
               SubstitutionMap nullMap(&d_fakeContext);
               Theory::PPAssertStatus status CVC4_UNUSED; // just for assertions
               status = d_smt.d_theoryEngine->solve(geq, nullMap);
@@ -2460,7 +2545,7 @@ void SmtEnginePrivate::doMiplibTrick() {
           }
           newAssertion = Rewriter::rewrite(newAssertion);
           Debug("miplib") << "  " << newAssertion << endl;
-          d_assertionsToCheck.push_back(newAssertion);
+          d_assertions.push_back(newAssertion);
           Debug("miplib") << "  assertions to remove: " << endl;
           for(vector<TNode>::const_iterator k = asserts[pos_var].begin(), k_end = asserts[pos_var].end(); k != k_end; ++k) {
             Debug("miplib") << "    " << *k << endl;
@@ -2473,26 +2558,26 @@ void SmtEnginePrivate::doMiplibTrick() {
   if(!removeAssertions.empty()) {
     Debug("miplib") << "SmtEnginePrivate::simplify(): scrubbing miplib encoding..." << endl;
     for(size_t i = 0; i < d_realAssertionsEnd; ++i) {
-      if(removeAssertions.find(d_assertionsToCheck[i].getId()) != removeAssertions.end()) {
-        Debug("miplib") << "SmtEnginePrivate::simplify(): - removing " << d_assertionsToCheck[i] << endl;
-        d_assertionsToCheck[i] = d_true;
+      if(removeAssertions.find(d_assertions[i].getId()) != removeAssertions.end()) {
+        Debug("miplib") << "SmtEnginePrivate::simplify(): - removing " << d_assertions[i] << endl;
+        d_assertions[i] = d_true;
         ++d_smt.d_stats->d_numMiplibAssertionsRemoved;
-      } else if(d_assertionsToCheck[i].getKind() == kind::AND) {
-        size_t removals = removeFromConjunction(d_assertionsToCheck[i], removeAssertions);
+      } else if(d_assertions[i].getKind() == kind::AND) {
+        size_t removals = removeFromConjunction(d_assertions[i], removeAssertions);
         if(removals > 0) {
-          Debug("miplib") << "SmtEnginePrivate::simplify(): - reduced " << d_assertionsToCheck[i] << endl;
+          Debug("miplib") << "SmtEnginePrivate::simplify(): - reduced " << d_assertions[i] << endl;
           Debug("miplib") << "SmtEnginePrivate::simplify(): -      by " << removals << " conjuncts" << endl;
           d_smt.d_stats->d_numMiplibAssertionsRemoved += removals;
         }
       }
-      Debug("miplib") << "had: " << d_assertionsToCheck[i] << endl;
-      d_assertionsToCheck[i] = Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToCheck[i]));
-      Debug("miplib") << "now: " << d_assertionsToCheck[i] << endl;
+      Debug("miplib") << "had: " << d_assertions[i] << endl;
+      d_assertions[i] = Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i]));
+      Debug("miplib") << "now: " << d_assertions[i] << endl;
     }
   } else {
     Debug("miplib") << "SmtEnginePrivate::simplify(): miplib pass found nothing." << endl;
   }
-  d_realAssertionsEnd = d_assertionsToCheck.size();
+  d_realAssertionsEnd = d_assertions.size();
 }
 
 
@@ -2526,7 +2611,7 @@ bool SmtEnginePrivate::simplifyAssertions()
           // we add new assertions and need this (in practice, this
           // restriction only disables miplib processing during
           // re-simplification, which we don't expect to be useful anyway)
-          d_realAssertionsEnd == d_assertionsToCheck.size() ) {
+          d_realAssertionsEnd == d_assertions.size() ) {
         Chat() << "...fixing miplib encodings..." << endl;
         Trace("simplify") << "SmtEnginePrivate::simplify(): "
                           << "looking for miplib pseudobooleans..." << endl;
@@ -2538,18 +2623,16 @@ bool SmtEnginePrivate::simplifyAssertions()
         Trace("simplify") << "SmtEnginePrivate::simplify(): "
                           << "skipping miplib pseudobooleans pass (either incrementalSolving is on, or miplib pbs are turned off)..." << endl;
       }
-    } else {
-      Assert(d_assertionsToCheck.empty());
-      d_assertionsToCheck.swap(d_assertionsToPreprocess);
     }
 
-    dumpAssertions("post-nonclausal", d_assertionsToCheck);
+    dumpAssertions("post-nonclausal", d_assertions);
     Trace("smt") << "POST nonClausalSimplify" << endl;
-    Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
-    Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+    Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
     // before ppRewrite check if only core theory for BV theory
-    d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertionsToCheck);
+    d_smt.d_theoryEngine->staticInitializeBVOptions(d_assertions.ref());
+
+    dumpAssertions("pre-theorypp", d_assertions);
 
     // Theory preprocessing
     if (d_smt.d_earlyTheoryPP) {
@@ -2557,17 +2640,16 @@ bool SmtEnginePrivate::simplifyAssertions()
       TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime);
       // Call the theory preprocessors
       d_smt.d_theoryEngine->preprocessStart();
-      for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
-        Assert(Rewriter::rewrite(d_assertionsToCheck[i]) == d_assertionsToCheck[i]);
-        d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]);
-        Assert(Rewriter::rewrite(d_assertionsToCheck[i]) == d_assertionsToCheck[i]);
+      for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+        Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]);
+        d_assertions.replace(i, d_smt.d_theoryEngine->preprocess(d_assertions[i]));
+        Assert(Rewriter::rewrite(d_assertions[i]) == d_assertions[i]);
       }
     }
 
-    dumpAssertions("post-theorypp", d_assertionsToCheck);
+    dumpAssertions("post-theorypp", d_assertions);
     Trace("smt") << "POST theoryPP" << endl;
-    Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
-    Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+    Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
     // ITE simplification
     if(options::doITESimp() &&
@@ -2580,38 +2662,33 @@ bool SmtEnginePrivate::simplifyAssertions()
       }
     }
 
-    dumpAssertions("post-itesimp", d_assertionsToCheck);
+    dumpAssertions("post-itesimp", d_assertions);
     Trace("smt") << "POST iteSimp" << endl;
-    Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
-    Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+    Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
     // Unconstrained simplification
     if(options::unconstrainedSimp()) {
       Chat() << "...doing unconstrained simplification..." << endl;
-      unconstrainedSimp(d_assertionsToCheck);
+      unconstrainedSimp();
     }
 
-    dumpAssertions("post-unconstrained", d_assertionsToCheck);
+    dumpAssertions("post-unconstrained", d_assertions);
     Trace("smt") << "POST unconstrainedSimp" << endl;
-    Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
-    Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+    Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
     if(options::repeatSimp() && options::simplificationMode() != SIMPLIFICATION_MODE_NONE) {
       Chat() << "...doing another round of nonclausal simplification..." << endl;
       Trace("simplify") << "SmtEnginePrivate::simplify(): "
                         << " doing repeated simplification" << endl;
-      d_assertionsToCheck.swap(d_assertionsToPreprocess);
-      Assert(d_assertionsToCheck.empty());
       bool noConflict = nonClausalSimplify();
       if(!noConflict) {
         return false;
       }
     }
 
-    dumpAssertions("post-repeatsimp", d_assertionsToCheck);
+    dumpAssertions("post-repeatsimp", d_assertions);
     Trace("smt") << "POST repeatSimp" << endl;
-    Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
-    Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+    Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
   } catch(TypeCheckingExceptionPrivate& tcep) {
     // Calls to this function should have already weeded out any
@@ -2797,52 +2874,45 @@ void SmtEnginePrivate::processAssertions() {
   Assert(d_smt.d_pendingPops == 0);
 
   // Dump the assertions
-  dumpAssertions("pre-everything", d_assertionsToPreprocess);
+  dumpAssertions("pre-everything", d_assertions);
 
   Trace("smt") << "SmtEnginePrivate::processAssertions()" << endl;
 
-  Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
-  Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
-
-  Assert(d_assertionsToCheck.size() == 0);
+  Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
-  if (d_assertionsToPreprocess.size() == 0) {
+  if (d_assertions.size() == 0) {
     // nothing to do
     return;
   }
 
-  if (d_assertionsProcessed &&
-      ( options::incrementalSolving() ||
-        options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL )) {
+  if (d_assertionsProcessed && options::incrementalSolving()) {
     // Placeholder for storing substitutions
-    d_substitutionsIndex = d_assertionsToPreprocess.size();
-    d_assertionsToPreprocess.push_back(NodeManager::currentNM()->mkConst<bool>(true));
+    d_substitutionsIndex = d_assertions.size();
+    d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(true));
   }
 
   // Add dummy assertion in last position - to be used as a
   // placeholder for any new assertions to get added
-  d_assertionsToPreprocess.push_back(NodeManager::currentNM()->mkConst<bool>(true));
+  d_assertions.push_back(NodeManager::currentNM()->mkConst<bool>(true));
   // any assertions added beyond realAssertionsEnd must NOT affect the
   // equisatisfiability
-  d_realAssertionsEnd = d_assertionsToPreprocess.size();
+  d_realAssertionsEnd = d_assertions.size();
 
   // Assertions are NOT guaranteed to be rewritten by this point
 
-  dumpAssertions("pre-definition-expansion", d_assertionsToPreprocess);
+  dumpAssertions("pre-definition-expansion", d_assertions);
   {
     Chat() << "expanding definitions..." << endl;
     Trace("simplify") << "SmtEnginePrivate::simplify(): expanding definitions" << endl;
     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_definitionExpansionTime);
     hash_map<Node, Node, NodeHashFunction> cache;
-    for(unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
-      d_assertionsToPreprocess[i] =
-        expandDefinitions(d_assertionsToPreprocess[i], cache);
+    for(unsigned i = 0; i < d_assertions.size(); ++ i) {
+      d_assertions.replace(i, expandDefinitions(d_assertions[i], cache));
     }
   }
-  dumpAssertions("post-definition-expansion", d_assertionsToPreprocess);
+  dumpAssertions("post-definition-expansion", d_assertions);
 
-  Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
-  Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+  Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER &&
       !d_smt.d_logic.isPure(THEORY_BV)) {
@@ -2852,146 +2922,153 @@ void SmtEnginePrivate::processAssertions() {
   }
 
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    d_smt.d_theoryEngine->mkAckermanizationAsssertions(d_assertionsToPreprocess);
+    d_smt.d_theoryEngine->mkAckermanizationAsssertions(d_assertions.ref());
   }
 
   if ( options::bvAbstraction() &&
       !options::incrementalSolving()) {
-    dumpAssertions("pre-bv-abstraction", d_assertionsToPreprocess);
+    dumpAssertions("pre-bv-abstraction", d_assertions);
     bvAbstraction();
-    dumpAssertions("post-bv-abstraction", d_assertionsToPreprocess);
+    dumpAssertions("post-bv-abstraction", d_assertions);
   }
 
-  dumpAssertions("pre-boolean-terms", d_assertionsToPreprocess);
+  dumpAssertions("pre-boolean-terms", d_assertions);
   {
     Chat() << "rewriting Boolean terms..." << endl;
-    for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
-      d_assertionsToPreprocess[i] = rewriteBooleanTerms(d_assertionsToPreprocess[i]);
+    for(unsigned i = 0, i_end = d_assertions.size(); i != i_end; ++i) {
+      d_assertions.replace(i, rewriteBooleanTerms(d_assertions[i]));
     }
   }
-  dumpAssertions("post-boolean-terms", d_assertionsToPreprocess);
+  dumpAssertions("post-boolean-terms", d_assertions);
 
-  Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
-  Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+  Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
-  dumpAssertions("pre-constrain-subtypes", d_assertionsToPreprocess);
+  dumpAssertions("pre-constrain-subtypes", d_assertions);
   {
     // Any variables of subtype types need to be constrained properly.
     // Careful, here: constrainSubtypes() adds to the back of
-    // d_assertionsToPreprocess, but we don't need to reprocess those.
+    // d_assertions, but we don't need to reprocess those.
     // We also can't use an iterator, because the vector may be moved in
     // memory during this loop.
     Chat() << "constraining subtypes..." << endl;
-    for(unsigned i = 0, i_end = d_assertionsToPreprocess.size(); i != i_end; ++i) {
-      constrainSubtypes(d_assertionsToPreprocess[i], d_assertionsToPreprocess);
+    for(unsigned i = 0, i_end = d_assertions.size(); i != i_end; ++i) {
+      constrainSubtypes(d_assertions[i], d_assertions);
     }
   }
-  dumpAssertions("post-constrain-subtypes", d_assertionsToPreprocess);
+  dumpAssertions("post-constrain-subtypes", d_assertions);
 
-  Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
-  Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+  Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
+  bool noConflict = true;
 
   // Unconstrained simplification
   if(options::unconstrainedSimp()) {
-    dumpAssertions("pre-unconstrained-simp", d_assertionsToPreprocess);
+    dumpAssertions("pre-unconstrained-simp", d_assertions);
     Chat() << "...doing unconstrained simplification..." << endl;
-    unconstrainedSimp(d_assertionsToPreprocess);
-    dumpAssertions("post-unconstrained-simp", d_assertionsToPreprocess);
+    unconstrainedSimp();
+    dumpAssertions("post-unconstrained-simp", d_assertions);
   }
 
   if(options::bvIntroducePow2()){
-    theory::bv::BVIntroducePow2::pow2Rewrite(d_assertionsToPreprocess);
+    theory::bv::BVIntroducePow2::pow2Rewrite(d_assertions.ref());
   }
 
-  dumpAssertions("pre-substitution", d_assertionsToPreprocess);
+  dumpAssertions("pre-substitution", d_assertions);
 
-  // Apply the substitutions we already have, and normalize
-  Chat() << "applying substitutions..." << endl;
-  Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
-                    << "applying substitutions" << endl;
-  for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
-    Trace("simplify") << "applying to " << d_assertionsToPreprocess[i] << endl;
-    d_assertionsToPreprocess[i] =
-      Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertionsToPreprocess[i]));
-    Trace("simplify") << "  got " << d_assertionsToPreprocess[i] << endl;
+  if(options::unsatCores()) {
+    // special rewriting pass for unsat cores, since many of the passes below are skipped
+    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+      d_assertions.replace(i, Rewriter::rewrite(d_assertions[i]));
+    }
+  } else {
+    // Apply the substitutions we already have, and normalize
+    if(!options::unsatCores()) {
+      Chat() << "applying substitutions..." << endl;
+      Trace("simplify") << "SmtEnginePrivate::nonClausalSimplify(): "
+                        << "applying substitutions" << endl;
+      for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+        Trace("simplify") << "applying to " << d_assertions[i] << endl;
+        d_assertions.replace(i, Rewriter::rewrite(d_topLevelSubstitutions.apply(d_assertions[i])));
+        Trace("simplify") << "  got " << d_assertions[i] << endl;
+      }
+    }
   }
-  dumpAssertions("post-substitution", d_assertionsToPreprocess);
 
-  // Assertions ARE guaranteed to be rewritten by this point
+  dumpAssertions("post-substitution", d_assertions);
 
+  // Assertions ARE guaranteed to be rewritten by this point
 
   // Lift bit-vectors of size 1 to bool
   if(options::bitvectorToBool()) {
-    dumpAssertions("pre-bv-to-bool", d_assertionsToPreprocess);
+    dumpAssertions("pre-bv-to-bool", d_assertions);
     Chat() << "...doing bvToBool..." << endl;
     bvToBool();
-    dumpAssertions("post-bv-to-bool", d_assertionsToPreprocess);
+    dumpAssertions("post-bv-to-bool", d_assertions);
   }
 
   if( d_smt.d_logic.isTheoryEnabled(THEORY_STRINGS) ) {
-    dumpAssertions("pre-strings-pp", d_assertionsToPreprocess);
+    dumpAssertions("pre-strings-pp", d_assertions);
     CVC4::theory::strings::StringsPreprocess sp;
     std::vector<Node> newNodes;
-    newNodes.push_back(d_assertionsToPreprocess[d_realAssertionsEnd - 1]);
-    sp.simplify( d_assertionsToPreprocess, newNodes );
+    newNodes.push_back(d_assertions[d_realAssertionsEnd - 1]);
+    sp.simplify( d_assertions.ref(), newNodes );
     if(newNodes.size() > 1) {
-      d_assertionsToPreprocess[d_realAssertionsEnd - 1] = NodeManager::currentNM()->mkNode(kind::AND, newNodes);
+      d_assertions[d_realAssertionsEnd - 1] = NodeManager::currentNM()->mkNode(kind::AND, newNodes);
     }
-    for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
-      d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] );
+    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+      d_assertions[i] = Rewriter::rewrite( d_assertions[i] );
     }
-    dumpAssertions("post-strings-pp", d_assertionsToPreprocess);
+    dumpAssertions("post-strings-pp", d_assertions);
   }
   if( d_smt.d_logic.isQuantified() ){
     //remove rewrite rules
-    for( unsigned i=0; i < d_assertionsToPreprocess.size(); i++ ) {
-      if( d_assertionsToPreprocess[i].getKind() == kind::REWRITE_RULE ){
-        Node prev = d_assertionsToPreprocess[i];
+    for( unsigned i=0; i < d_assertions.size(); i++ ) {
+      if( d_assertions[i].getKind() == kind::REWRITE_RULE ){
+        Node prev = d_assertions[i];
         Trace("quantifiers-rewrite-debug") << "Rewrite rewrite rule " << prev << "..." << std::endl;
-        d_assertionsToPreprocess[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertionsToPreprocess[i] ) );
+        d_assertions[i] = Rewriter::rewrite( quantifiers::QuantifiersRewriter::rewriteRewriteRule( d_assertions[i] ) );
         Trace("quantifiers-rewrite") << "*** rr-rewrite " << prev << endl;
-        Trace("quantifiers-rewrite") << "   ...got " << d_assertionsToPreprocess[i] << endl;
+        Trace("quantifiers-rewrite") << "   ...got " << d_assertions[i] << endl;
       }
     }
 
-    dumpAssertions("pre-skolem-quant", d_assertionsToPreprocess);
+    dumpAssertions("pre-skolem-quant", d_assertions);
     if( options::preSkolemQuant() ){
       //apply pre-skolemization to existential quantifiers
-      for (unsigned i = 0; i < d_assertionsToPreprocess.size(); ++ i) {
-        Node prev = d_assertionsToPreprocess[i];
+      for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+        Node prev = d_assertions[i];
         Trace("quantifiers-rewrite-debug") << "Pre-skolemize " << prev << "..." << std::endl;
         vector< TypeNode > fvTypes;
         vector< TNode > fvs;
-        d_assertionsToPreprocess[i] = quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs );
-        if( prev!=d_assertionsToPreprocess[i] ){
-          d_assertionsToPreprocess[i] = Rewriter::rewrite( d_assertionsToPreprocess[i] );
+        d_assertions.replace(i, quantifiers::QuantifiersRewriter::preSkolemizeQuantifiers( prev, true, fvTypes, fvs ));
+        if( prev!=d_assertions[i] ){
+          d_assertions.replace(i, Rewriter::rewrite( d_assertions[i] ));
           Trace("quantifiers-rewrite") << "*** Pre-skolemize " << prev << endl;
-          Trace("quantifiers-rewrite") << "   ...got " << d_assertionsToPreprocess[i] << endl;
+          Trace("quantifiers-rewrite") << "   ...got " << d_assertions[i] << endl;
         }
       }
     }
-    dumpAssertions("post-skolem-quant", d_assertionsToPreprocess);
+    dumpAssertions("post-skolem-quant", d_assertions);
     if( options::macrosQuant() ){
       //quantifiers macro expansion
       bool success;
       do{
         quantifiers::QuantifierMacros qm;
-        success = qm.simplify( d_assertionsToPreprocess, true );
+        success = qm.simplify( d_assertions.ref(), true );
       }while( success );
     }
 
     Trace("fo-rsn-enable") << std::endl;
     if( options::foPropQuant() ){
       quantifiers::FirstOrderPropagation fop;
-      fop.simplify( d_assertionsToPreprocess );
+      fop.simplify( d_assertions.ref() );
     }
   }
 
   if( options::sortInference() ){
     //sort inference technique
     SortInference * si = d_smt.d_theoryEngine->getSortInference();
-    si->simplify( d_assertionsToPreprocess );
+    si->simplify( d_assertions.ref() );
     for( std::map< Node, Node >::iterator it = si->d_model_replace_f.begin(); it != si->d_model_replace_f.end(); ++it ){
       d_smt.setPrintFuncInModel( it->first.toExpr(), false );
       d_smt.setPrintFuncInModel( it->second.toExpr(), true );
@@ -2999,25 +3076,25 @@ void SmtEnginePrivate::processAssertions() {
   }
 
   //if( options::quantConflictFind() ){
-  //  d_smt.d_theoryEngine->getQuantConflictFind()->registerAssertions( d_assertionsToPreprocess );
+  //  d_smt.d_theoryEngine->getQuantConflictFind()->registerAssertions( d_assertions );
   //}
 
   if( options::pbRewrites() ){
-    d_pbsProcessor.learn(d_assertionsToPreprocess);
+    d_pbsProcessor.learn(d_assertions.ref());
     if(d_pbsProcessor.likelyToHelp()){
-      d_pbsProcessor.applyReplacements(d_assertionsToPreprocess);
+      d_pbsProcessor.applyReplacements(d_assertions.ref());
     }
   }
 
-  dumpAssertions("pre-simplify", d_assertionsToPreprocess);
+  dumpAssertions("pre-simplify", d_assertions);
   Chat() << "simplifying assertions..." << endl;
-  bool noConflict = simplifyAssertions();
+  noConflict = simplifyAssertions();
   if(!noConflict){
     ++(d_smt.d_stats->d_simplifiedToFalse);
   }
-  dumpAssertions("post-simplify", d_assertionsToCheck);
+  dumpAssertions("post-simplify", d_assertions);
 
-  dumpAssertions("pre-static-learning", d_assertionsToCheck);
+  dumpAssertions("pre-static-learning", d_assertions);
   if(options::doStaticLearning()) {
     // Perform static learning
     Chat() << "doing static learning..." << endl;
@@ -3025,27 +3102,25 @@ void SmtEnginePrivate::processAssertions() {
                       << "performing static learning" << endl;
     staticLearning();
   }
-  dumpAssertions("post-static-learning", d_assertionsToCheck);
+  dumpAssertions("post-static-learning", d_assertions);
 
   Trace("smt") << "POST bvToBool" << endl;
-  Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
-  Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+  Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
 
-  dumpAssertions("pre-ite-removal", d_assertionsToCheck);
+  dumpAssertions("pre-ite-removal", d_assertions);
   {
     Chat() << "removing term ITEs..." << endl;
     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_iteRemovalTime);
     // Remove ITEs, updating d_iteSkolemMap
-    d_smt.d_stats->d_numAssertionsPre += d_assertionsToCheck.size();
+    d_smt.d_stats->d_numAssertionsPre += d_assertions.size();
     removeITEs();
-    d_smt.d_stats->d_numAssertionsPost += d_assertionsToCheck.size();
+    d_smt.d_stats->d_numAssertionsPost += d_assertions.size();
   }
-  dumpAssertions("post-ite-removal", d_assertionsToCheck);
+  dumpAssertions("post-ite-removal", d_assertions);
 
-  dumpAssertions("pre-repeat-simplify", d_assertionsToCheck);
+  dumpAssertions("pre-repeat-simplify", d_assertions);
   if(options::repeatSimp()) {
-    d_assertionsToCheck.swap(d_assertionsToPreprocess);
     Chat() << "re-simplifying assertions..." << endl;
     ScopeCounter depth(d_simplifyAssertionsDepth);
     noConflict &= simplifyAssertions();
@@ -3074,11 +3149,11 @@ void SmtEnginePrivate::processAssertions() {
       IteSkolemMap::iterator it = d_iteSkolemMap.begin();
       IteSkolemMap::iterator iend = d_iteSkolemMap.end();
       NodeBuilder<> builder(kind::AND);
-      builder << d_assertionsToCheck[d_realAssertionsEnd - 1];
+      builder << d_assertions[d_realAssertionsEnd - 1];
       vector<TNode> toErase;
       for (; it != iend; ++it) {
         if (skolemSet.find((*it).first) == skolemSet.end()) {
-          TNode iteExpr = d_assertionsToCheck[(*it).second];
+          TNode iteExpr = d_assertions[(*it).second];
           if (iteExpr.getKind() == kind::ITE &&
               iteExpr[1].getKind() == kind::EQUAL &&
               iteExpr[1][0] == (*it).first &&
@@ -3094,8 +3169,8 @@ void SmtEnginePrivate::processAssertions() {
           }
         }
         // Move this iteExpr into the main assertions
-        builder << d_assertionsToCheck[(*it).second];
-        d_assertionsToCheck[(*it).second] = NodeManager::currentNM()->mkConst<bool>(true);
+        builder << d_assertions[(*it).second];
+        d_assertions[(*it).second] = NodeManager::currentNM()->mkConst<bool>(true);
         toErase.push_back((*it).first);
       }
       if(builder.getNumChildren() > 1) {
@@ -3103,60 +3178,58 @@ void SmtEnginePrivate::processAssertions() {
           d_iteSkolemMap.erase(toErase.back());
           toErase.pop_back();
         }
-        d_assertionsToCheck[d_realAssertionsEnd - 1] =
+        d_assertions[d_realAssertionsEnd - 1] =
           Rewriter::rewrite(Node(builder));
       }
       // For some reason this is needed for some benchmarks, such as
       // http://cvc4.cs.nyu.edu/benchmarks/smtlib2/QF_AUFBV/dwp_formulas/try5_small_difret_functions_dwp_tac.re_node_set_remove_at.il.dwp.smt2
       // Figure it out later
       removeITEs();
-      //      Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size());
+      //      Assert(iteRewriteAssertionsEnd == d_assertions.size());
     }
   }
-  dumpAssertions("post-repeat-simplify", d_assertionsToCheck);
+  dumpAssertions("post-repeat-simplify", d_assertions);
 
-  dumpAssertions("pre-rewrite-apply-to-const", d_assertionsToCheck);
+  dumpAssertions("pre-rewrite-apply-to-const", d_assertions);
   if(options::rewriteApplyToConst()) {
     Chat() << "Rewriting applies to constants..." << endl;
-    TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime);
-    for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
-      d_assertionsToCheck[i] = Rewriter::rewrite(rewriteApplyToConst(d_assertionsToCheck[i]));
+    TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_rewriteApplyToConstTime);
+    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+      d_assertions[i] = Rewriter::rewrite(rewriteApplyToConst(d_assertions[i]));
     }
   }
-  dumpAssertions("post-rewrite-apply-to-const", d_assertionsToCheck);
+  dumpAssertions("post-rewrite-apply-to-const", d_assertions);
 
   // begin: INVARIANT to maintain: no reordering of assertions or
   // introducing new ones
 #ifdef CVC4_ASSERTIONS
-  unsigned iteRewriteAssertionsEnd = d_assertionsToCheck.size();
+  unsigned iteRewriteAssertionsEnd = d_assertions.size();
 #endif
 
-  Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
-  Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+  Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
   Debug("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl;
-  Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
-  Debug("smt") << " d_assertionsToCheck     : " << d_assertionsToCheck.size() << endl;
+  Debug("smt") << " d_assertions     : " << d_assertions.size() << endl;
 
-  dumpAssertions("pre-theory-preprocessing", d_assertionsToCheck);
+  dumpAssertions("pre-theory-preprocessing", d_assertions);
   {
     Chat() << "theory preprocessing..." << endl;
     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_theoryPreprocessTime);
     // Call the theory preprocessors
     d_smt.d_theoryEngine->preprocessStart();
-    for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
-      d_assertionsToCheck[i] = d_smt.d_theoryEngine->preprocess(d_assertionsToCheck[i]);
+    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+      d_assertions.replace(i, d_smt.d_theoryEngine->preprocess(d_assertions[i]));
     }
   }
-  dumpAssertions("post-theory-preprocessing", d_assertionsToCheck);
+  dumpAssertions("post-theory-preprocessing", d_assertions);
 
   // If we are using eager bit-blasting wrap assertions in fake atom so that
   // everything gets bit-blasted to internal SAT solver
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER) {
-    for (unsigned i = 0; i < d_assertionsToCheck.size(); ++i) {
-      TNode atom = d_assertionsToCheck[i];
+    for (unsigned i = 0; i < d_assertions.size(); ++i) {
+      TNode atom = d_assertions[i];
       Node eager_atom = NodeManager::currentNM()->mkNode(kind::BITVECTOR_EAGER_ATOM, atom);
-      d_assertionsToCheck[i] = eager_atom;
+      d_assertions.replace(i, eager_atom);
       TheoryModel* m = d_smt.d_theoryEngine->getModel();
       m->addSubstitution(eager_atom, atom);
     }
@@ -3165,36 +3238,36 @@ void SmtEnginePrivate::processAssertions() {
   // Push the formula to decision engine
   if(noConflict) {
     Chat() << "pushing to decision engine..." << endl;
-    Assert(iteRewriteAssertionsEnd == d_assertionsToCheck.size());
+    Assert(iteRewriteAssertionsEnd == d_assertions.size());
     d_smt.d_decisionEngine->addAssertions
-      (d_assertionsToCheck, d_realAssertionsEnd, d_iteSkolemMap);
+      (d_assertions.ref(), d_realAssertionsEnd, d_iteSkolemMap);
   }
 
   // end: INVARIANT to maintain: no reordering of assertions or
   // introducing new ones
 
-  dumpAssertions("post-everything", d_assertionsToCheck);
+  dumpAssertions("post-everything", d_assertions);
   
   //set instantiation level of everything to zero
   if( options::instLevelInputOnly() && options::instMaxLevel()!=-1 ){
-    for( unsigned i=0; i < d_assertionsToCheck.size(); i++ ) {
-      theory::QuantifiersEngine::setInstantiationLevelAttr( d_assertionsToCheck[i], 0 );
+    for( unsigned i=0; i < d_assertions.size(); i++ ) {
+      theory::QuantifiersEngine::setInstantiationLevelAttr( d_assertions[i], 0 );
     }
   }
   
-
   // Push the formula to SAT
   {
     Chat() << "converting to CNF..." << endl;
     TimerStat::CodeTimer codeTimer(d_smt.d_stats->d_cnfConversionTime);
-    for (unsigned i = 0; i < d_assertionsToCheck.size(); ++ i) {
-      d_smt.d_propEngine->assertFormula(d_assertionsToCheck[i]);
+    for (unsigned i = 0; i < d_assertions.size(); ++ i) {
+      Chat() << "+ " << d_assertions[i] << std::endl;
+      d_smt.d_propEngine->assertFormula(d_assertions[i]);
     }
   }
 
   d_assertionsProcessed = true;
 
-  d_assertionsToCheck.clear();
+  d_assertions.clear();
   d_iteSkolemMap.clear();
 }
 
@@ -3209,13 +3282,8 @@ void SmtEnginePrivate::addFormula(TNode n)
   Trace("smt") << "SmtEnginePrivate::addFormula(" << n << ")" << endl;
 
   // Add the normalized formula to the queue
-  d_assertionsToPreprocess.push_back(n);
-  //d_assertionsToPreprocess.push_back(Rewriter::rewrite(n));
-
-  // If the mode of processing is incremental prepreocess and assert immediately
-  if (options::simplificationMode() == SIMPLIFICATION_MODE_INCREMENTAL) {
-    processAssertions();
-  }
+  d_assertions.push_back(n);
+  //d_assertions.push_back(Rewriter::rewrite(n));
 }
 
 void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) {
@@ -3230,7 +3298,7 @@ void SmtEngine::ensureBoolean(const Expr& e) throw(TypeCheckingException) {
   }
 }
 
-Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalException, LogicException) {
+Result SmtEngine::checkSat(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) {
   Assert(ex.isNull() || ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
@@ -3251,7 +3319,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
     // Ensure expr is type-checked at this point.
     ensureBoolean(e);
     // Give it to proof manager
-    PROOF( ProofManager::currentPM()->addAssertion(e); );
+    PROOF( ProofManager::currentPM()->addAssertion(e, inUnsatCore); );
   }
 
   // check to see if a postsolve() is pending
@@ -3313,7 +3381,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
   return r;
 }/* SmtEngine::checkSat() */
 
-Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalException, LogicException) {
+Result SmtEngine::query(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, ModalException, LogicException) {
   Assert(!ex.isNull());
   Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
@@ -3332,7 +3400,7 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
   // Ensure that the expression is type-checked at this point, and Boolean
   ensureBoolean(e);
   // Give it to proof manager
-  PROOF( ProofManager::currentPM()->addAssertion(e.notExpr()); );
+  PROOF( ProofManager::currentPM()->addAssertion(e.notExpr(), inUnsatCore); );
 
   // check to see if a postsolve() is pending
   if(d_needPostsolve) {
@@ -3391,13 +3459,13 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
   return r;
 }/* SmtEngine::query() */
 
-Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, LogicException) {
+Result SmtEngine::assertFormula(const Expr& ex, bool inUnsatCore) throw(TypeCheckingException, LogicException) {
   Assert(ex.getExprManager() == d_exprManager);
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();
 
-  PROOF( ProofManager::currentPM()->addAssertion(ex); );
+  PROOF( ProofManager::currentPM()->addAssertion(ex, inUnsatCore); );
 
   Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl;
 
@@ -3410,7 +3478,7 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log
   }
   d_private->addFormula(e.getNode());
   return quickCheck().asValidityResult();
-}
+}/* SmtEngine::assertFormula() */
 
 Node SmtEngine::postprocess(TNode node, TypeNode expectedType) const {
   ModelPostprocessor mpost;
@@ -3880,6 +3948,30 @@ void SmtEngine::checkModel(bool hardFailure) {
   Notice() << "SmtEngine::checkModel(): all assertions checked out OK !" << endl;
 }
 
+UnsatCore SmtEngine::getUnsatCore() throw(ModalException) {
+  Trace("smt") << "SMT getUnsatCore()" << endl;
+  SmtScope smts(this);
+  finalOptionsAreSet();
+  if(Dump.isOn("benchmark")) {
+    Dump("benchmark") << GetUnsatCoreCommand();
+  }
+#ifdef CVC4_PROOF
+  if(!options::unsatCores()) {
+    throw ModalException("Cannot get an unsat core when produce-unsat-cores option is off.");
+  }
+  if(d_status.isNull() ||
+     d_status.asSatisfiabilityResult() != Result::UNSAT ||
+     d_problemExtended) {
+    throw ModalException("Cannot get an unsat core unless immediately preceded by UNSAT/VALID response.");
+  }
+
+  delete d_proofManager->getProof(this);// just to trigger core creation
+  return UnsatCore(d_proofManager->begin_unsat_core(), d_proofManager->end_unsat_core());
+#else /* CVC4_PROOF */
+  throw ModalException("This build of CVC4 doesn't have proof support (required for unsat cores).");
+#endif /* CVC4_PROOF */
+}
+
 Proof* SmtEngine::getProof() throw(ModalException) {
   Trace("smt") << "SMT getProof()" << endl;
   SmtScope smts(this);
@@ -3889,16 +3981,12 @@ Proof* SmtEngine::getProof() throw(ModalException) {
   }
 #ifdef CVC4_PROOF
   if(!options::proof()) {
-    const char* msg =
-      "Cannot get a proof when produce-proofs option is off.";
-    throw ModalException(msg);
+    throw ModalException("Cannot get a proof when produce-proofs option is off.");
   }
   if(d_status.isNull() ||
      d_status.asSatisfiabilityResult() != Result::UNSAT ||
      d_problemExtended) {
-    const char* msg =
-      "Cannot get a proof unless immediately preceded by UNSAT/VALID response.";
-    throw ModalException(msg);
+    throw ModalException("Cannot get a proof unless immediately preceded by UNSAT/VALID response.");
   }
 
   return ProofManager::getProof(this);
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 1671654d1..ac0170f3b 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -28,6 +28,7 @@
 #include "expr/expr.h"
 #include "expr/expr_manager.h"
 #include "util/proof.h"
+#include "util/unsat_core.h"
 #include "smt/modal_exception.h"
 #include "smt/logic_exception.h"
 #include "options/options.h"
@@ -255,7 +256,7 @@ class CVC4_PUBLIC SmtEngine {
   smt::SmtEnginePrivate* d_private;
 
   /**
-   * Check that a generated Proof (via getProof()) checks.
+   * Check that a generated proof (via getProof()) checks.
    */
   void checkProof();
 
@@ -424,8 +425,8 @@ public:
   /**
    * Add a formula to the current context: preprocess, do per-theory
    * setup, use processAssertionList(), asserting to T-solver for
-   * literals and conjunction of literals.  Returns false iff
-   * inconsistent.
+   * literals and conjunction of literals.  Returns false if
+   * immediately determined to be inconsistent.
    */
   void defineFunction(Expr func,
                       const std::vector<Expr>& formals,
@@ -434,23 +435,25 @@ public:
   /**
    * Add a formula to the current context: preprocess, do per-theory
    * setup, use processAssertionList(), asserting to T-solver for
-   * literals and conjunction of literals.  Returns false iff
-   * inconsistent.
+   * literals and conjunction of literals.  Returns false if
+   * immediately determined to be inconsistent.  This version
+   * takes a Boolean flag to determine whether to include this asserted
+   * formula in an unsat core (if one is later requested).
    */
-  Result assertFormula(const Expr& e) throw(TypeCheckingException, LogicException);
+  Result assertFormula(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, LogicException);
 
   /**
    * Check validity of an expression with respect to the current set
    * of assertions by asserting the query expression's negation and
    * calling check().  Returns valid, invalid, or unknown result.
    */
-  Result query(const Expr& e) throw(TypeCheckingException, ModalException, LogicException);
+  Result query(const Expr& e, bool inUnsatCore = true) throw(TypeCheckingException, ModalException, LogicException);
 
   /**
    * Assert a formula (if provided) to the current context and call
    * check().  Returns sat, unsat, or unknown result.
    */
-  Result checkSat(const Expr& e = Expr()) throw(TypeCheckingException, ModalException, LogicException);
+  Result checkSat(const Expr& e = Expr(), bool inUnsatCore = true) throw(TypeCheckingException, ModalException, LogicException);
 
   /**
    * Simplify a formula without doing "much" work.  Does not involve
@@ -507,6 +510,13 @@ public:
   void printInstantiations( std::ostream& out );
 
   /**
+   * Get an unsatisfiable core (only if immediately preceded by an
+   * UNSAT or VALID query).  Only permitted if CVC4 was built with
+   * unsat-core support and produce-unsat-cores is on.
+   */
+  UnsatCore getUnsatCore() throw(ModalException);
+
+  /**
    * Get the current set of assertions.  Only permitted if the
    * SmtEngine is set to operate interactively.
    */
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index 54b9fa1d0..fb5810fd5 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -40,9 +40,14 @@ inline SmtEngine* currentSmtEngine() {
 }
 
 inline ProofManager* currentProofManager() {
-  Assert(PROOF_ON());
+#ifdef CVC4_PROOF
+  Assert(options::proof() || options::unsatCores());
   Assert(s_smtEngine_current != NULL);
   return s_smtEngine_current->d_proofManager;
+#else /* CVC4_PROOF */
+  InternalError("proofs/unsat cores are not on, but ProofManager requested");
+  return NULL;
+#endif /* CVC4_PROOF */
 }
 
 class SmtScope : public NodeManagerScope {
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h
index 7dbef4041..169ac6fa7 100644
--- a/src/theory/booleans/circuit_propagator.h
+++ b/src/theory/booleans/circuit_propagator.h
@@ -144,7 +144,7 @@ private:
       }
     }
 
-    // Get the current assignement
+    // Get the current assignment
     AssignmentStatus state = d_state[n];
 
     if(state != UNASSIGNED) {
diff --git a/src/theory/bv/eager_bitblaster.cpp b/src/theory/bv/eager_bitblaster.cpp
index 38b9a1a0a..877baec4e 100644
--- a/src/theory/bv/eager_bitblaster.cpp
+++ b/src/theory/bv/eager_bitblaster.cpp
@@ -56,7 +56,7 @@ EagerBitblaster::~EagerBitblaster() {
 }
 
 void EagerBitblaster::bbFormula(TNode node) {
-  d_cnfStream->convertAndAssert(node, false, false); 
+  d_cnfStream->convertAndAssert(node, false, false, RULE_INVALID, TNode::null());
 }
 
 /**
@@ -85,7 +85,7 @@ void EagerBitblaster::bbAtom(TNode node) {
 
   AlwaysAssert (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER); 
   storeBBAtom(node, atom_definition);
-  d_cnfStream->convertAndAssert(atom_definition, false, false);
+  d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
 }
 
 void EagerBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
diff --git a/src/theory/bv/lazy_bitblaster.cpp b/src/theory/bv/lazy_bitblaster.cpp
index 101d8b082..f8927284f 100644
--- a/src/theory/bv/lazy_bitblaster.cpp
+++ b/src/theory/bv/lazy_bitblaster.cpp
@@ -114,7 +114,7 @@ void TLazyBitblaster::bbAtom(TNode node) {
     Assert (!atom_bb.isNull()); 
     Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
     storeBBAtom(node, atom_bb);
-    d_cnfStream->convertAndAssert(atom_definition, false, false); 
+    d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
     return; 
   }
 
@@ -126,7 +126,7 @@ void TLazyBitblaster::bbAtom(TNode node) {
   // asserting that the atom is true iff the definition holds
   Node atom_definition = utils::mkNode(kind::IFF, node, atom_bb);
   storeBBAtom(node, atom_bb);
-  d_cnfStream->convertAndAssert(atom_definition, false, false);
+  d_cnfStream->convertAndAssert(atom_definition, false, false, RULE_INVALID, TNode::null());
 }
 
 void TLazyBitblaster::storeBBAtom(TNode atom, Node atom_bb) {
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 1b0270b94..53a529325 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -34,6 +34,8 @@
 
 #include "smt/logic_exception.h"
 
+#include "proof/proof_manager.h"
+
 #include "util/node_visitor.h"
 #include "util/ite_removal.h"
 
@@ -168,7 +170,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
 
-  PROOF (ProofManager::currentPM()->initTheoryProof(); );
+  PROOF (ProofManager::initTheoryProof(); );
 
   d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor());
 
@@ -1385,10 +1387,10 @@ theory::LemmaStatus TheoryEngine::lemma(TNode node, bool negated, bool removable
   }
 
   // assert to prop engine
-  d_propEngine->assertLemma(additionalLemmas[0], negated, removable);
+  d_propEngine->assertLemma(additionalLemmas[0], negated, removable, RULE_INVALID, node);
   for (unsigned i = 1; i < additionalLemmas.size(); ++ i) {
     additionalLemmas[i] = theory::Rewriter::rewrite(additionalLemmas[i]);
-    d_propEngine->assertLemma(additionalLemmas[i], false, removable);
+    d_propEngine->assertLemma(additionalLemmas[i], false, removable, RULE_INVALID, node);
   }
 
   // WARNING: Below this point don't assume additionalLemmas[0] to be not negated.
diff --git a/src/util/Makefile.am b/src/util/Makefile.am
index 5cf5da1e0..fc9192dd9 100644
--- a/src/util/Makefile.am
+++ b/src/util/Makefile.am
@@ -97,7 +97,9 @@ libutil_la_SOURCES = \
 	regexp.cpp \
 	bin_heap.h \
 	didyoumean.h \
-	didyoumean.cpp
+	didyoumean.cpp \
+	unsat_core.h \
+	unsat_core.cpp
 
 libstatistics_la_SOURCES = \
 	statistics_registry.h \
@@ -156,7 +158,8 @@ EXTRA_DIST = \
 	uninterpreted_constant.i \
 	chain.i \
 	regexp.i \
-	proof.i
+	proof.i \
+	unsat_core.i
 
 DISTCLEANFILES = \
 	integer.h.tmp \
diff --git a/src/util/ite_removal.cpp b/src/util/ite_removal.cpp
index 68d7d9a34..97a6338ce 100644
--- a/src/util/ite_removal.cpp
+++ b/src/util/ite_removal.cpp
@@ -19,6 +19,7 @@
 #include "util/ite_removal.h"
 #include "expr/command.h"
 #include "theory/ite_utilities.h"
+#include "proof/proof_manager.h"
 
 using namespace CVC4;
 using namespace std;
@@ -47,13 +48,23 @@ size_t RemoveITE::collectedCacheSizes() const{
   return d_containsVisitor->cache_size() + d_iteCache.size();
 }
 
-void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap)
+void RemoveITE::run(std::vector<Node>& output, IteSkolemMap& iteSkolemMap, bool reportDeps)
 {
+  size_t n = output.size();
   for (unsigned i = 0, i_end = output.size(); i < i_end; ++ i) {
     // Do this in two steps to avoid Node problems(?)
     // Appears related to bug 512, splitting this into two lines
     // fixes the bug on clang on Mac OS
     Node itesRemoved = run(output[i], output, iteSkolemMap, false);
+    // In some calling contexts, not necessary to report dependence information.
+    if(reportDeps && options::unsatCores()) {
+      // new assertions have a dependence on the node
+      PROOF( ProofManager::currentPM()->addDependence(itesRemoved, output[i]); )
+      while(n < output.size()) {
+        PROOF( ProofManager::currentPM()->addDependence(output[n], output[i]); )
+        ++n;
+      }
+    }
     output[i] = itesRemoved;
   }
 }
diff --git a/src/util/ite_removal.h b/src/util/ite_removal.h
index 83c55dab7..d71f9b13d 100644
--- a/src/util/ite_removal.h
+++ b/src/util/ite_removal.h
@@ -50,8 +50,11 @@ public:
    * contains a map from introduced skolem variables to the index in
    * assertions containing the new Boolean ite created in conjunction
    * with that skolem variable.
+   *
+   * With reportDeps true, report reasoning dependences to the proof
+   * manager (for unsat cores).
    */
-  void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap);
+  void run(std::vector<Node>& assertions, IteSkolemMap& iteSkolemMap, bool reportDeps = false);
 
   /**
    * Removes the ITE from the node by introducing skolem
diff --git a/src/util/unsat_core.cpp b/src/util/unsat_core.cpp
new file mode 100644
index 000000000..27261635d
--- /dev/null
+++ b/src/util/unsat_core.cpp
@@ -0,0 +1,41 @@
+/*********************                                                        */
+/*! \file unsat_core.cpp
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief Representation of unsat cores
+ **
+ ** Representation of unsat cores.
+ **/
+
+#include "util/unsat_core.h"
+#include "expr/command.h"
+
+namespace CVC4 {
+
+UnsatCore::const_iterator UnsatCore::begin() const {
+  return d_core.begin();
+}
+
+UnsatCore::const_iterator UnsatCore::end() const {
+  return d_core.end();
+}
+
+void UnsatCore::toStream(std::ostream& out) const {
+  for(UnsatCore::const_iterator i = begin(); i != end(); ++i) {
+    out << AssertCommand(*i) << std::endl;
+  }
+}
+
+std::ostream& operator<<(std::ostream& out, const UnsatCore& core) {
+  core.toStream(out);
+  return out;
+}
+
+}/* CVC4 namespace */
diff --git a/src/util/unsat_core.h b/src/util/unsat_core.h
new file mode 100644
index 000000000..51724b33b
--- /dev/null
+++ b/src/util/unsat_core.h
@@ -0,0 +1,54 @@
+/*********************                                                        */
+/*! \file unsat_core.h
+ ** \verbatim
+ ** Original author: Morgan Deters
+ ** Major contributors: none
+ ** Minor contributors (to current version): none
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2014  New York University and The University of Iowa
+ ** See the file COPYING in the top-level source directory for licensing
+ ** information.\endverbatim
+ **
+ ** \brief [[ Add one-line brief description here ]]
+ **
+ ** [[ Add lengthier description here ]]
+ ** \todo document this file
+ **/
+
+#include "cvc4_public.h"
+
+#ifndef __CVC4__UNSAT_CORE_H
+#define __CVC4__UNSAT_CORE_H
+
+#include <iostream>
+#include <vector>
+#include "expr/expr.h"
+
+namespace CVC4 {
+
+class CVC4_PUBLIC UnsatCore {
+  std::vector<Expr> d_core;
+
+public:
+  UnsatCore() {}
+
+  template <class T>
+  UnsatCore(T begin, T end) : d_core(begin, end) {}
+
+  ~UnsatCore() {}
+
+  typedef std::vector<Expr>::const_iterator iterator;
+  typedef std::vector<Expr>::const_iterator const_iterator;
+
+  const_iterator begin() const;
+  const_iterator end() const;
+
+  void toStream(std::ostream& out) const;
+
+};/* class UnsatCore */
+
+std::ostream& operator<<(std::ostream& out, const UnsatCore& core) CVC4_PUBLIC;
+
+}/* CVC4 namespace */
+
+#endif /* __CVC4__UNSAT_CORE_H */
diff --git a/src/util/unsat_core.i b/src/util/unsat_core.i
new file mode 100644
index 000000000..78b1360e7
--- /dev/null
+++ b/src/util/unsat_core.i
@@ -0,0 +1,5 @@
+%{
+#include "util/unsat_core.h"
+%}
+
+%include "util/unsat_core.h"
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index 5e57e9b67..86fc8fdff 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -105,7 +105,6 @@ CVC_TESTS = \
 	wiki.19.cvc \
 	wiki.20.cvc \
 	wiki.21.cvc \
-	simplification_bug3.cvc \
 	queries0.cvc \
 	print_lambda.cvc
 
diff --git a/test/regress/regress0/simplification_bug3.cvc b/test/regress/regress0/simplification_bug3.cvc
deleted file mode 100644
index 3f0ddc537..000000000
--- a/test/regress/regress0/simplification_bug3.cvc
+++ /dev/null
@@ -1,7 +0,0 @@
-% COMMAND-LINE: --simplification=incremental
-x, y: BOOLEAN;
-ASSERT x OR y;
-ASSERT NOT x;
-ASSERT NOT y;
-% EXPECT: unsat
-CHECKSAT;