Proof-checking code; fixups of segfaults and missing functionality in proof generation; fix bug 285.

* segfaults/assert-fails in proof-generation fixed, including bug 285
* added --check-proofs to automatically check proofs, like --check-models (but only for UF/SAT at present)
* proof generation now works in portfolio (but *not* --check-proofs, since LFSC code uses globals)
* proofs are *not* yet supported in incremental mode
* added --dump-proofs to dump out proofs, like --dump-models
* run_regression script now runs with --check-proofs where appropriate
* options scripts now support :link-smt for SMT options, like :link for command-line

24 files changed, 836 insertions, 528 deletions

diff --git a/src/Makefile.am b/src/Makefile.am
index 18382a8ab..c765d325a 100644
--- a/src/Makefile.am
+++ b/src/Makefile.am
@@ -396,7 +396,8 @@ libcvc4_la_LIBADD = \
 	@builddir@/prop/bvminisat/libbvminisat.la
 if CVC4_PROOF
 libcvc4_la_LIBADD += \
-	@top_builddir@/proofs/lfsc_checker/liblfsc_checker.la
+	@top_builddir@/proofs/lfsc_checker/liblfsc_checker.la \
+	@top_builddir@/proofs/signatures/libsignatures.la
 endif
 
 if CVC4_NEEDS_REPLACEMENT_FUNCTIONS
diff --git a/src/main/command_executor.cpp b/src/main/command_executor.cpp
index 467b150d3..485a478d8 100644
--- a/src/main/command_executor.cpp
+++ b/src/main/command_executor.cpp
@@ -76,14 +76,20 @@ bool CommandExecutor::doCommandSingleton(Command* cmd)
   if(q != NULL) {
     d_result = res = q->getResult();
   }
-  // dump the model if option is set
-  if( status &&
-      d_options[options::produceModels] &&
-      d_options[options::dumpModels] &&
-      ( res.asSatisfiabilityResult() == Result::SAT ||
-        (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) {
-    Command* gm = new GetModelCommand();
-    status = doCommandSingleton(gm);
+  // dump the model/proof if option is set
+  if(status) {
+    if( d_options[options::produceModels] &&
+        d_options[options::dumpModels] &&
+        ( res.asSatisfiabilityResult() == Result::SAT ||
+          (res.isUnknown() && res.whyUnknown() == Result::INCOMPLETE) ) ) {
+      Command* gm = new GetModelCommand();
+      status = doCommandSingleton(gm);
+    } else if( d_options[options::proof] &&
+               d_options[options::dumpProofs] &&
+               res.asSatisfiabilityResult() == Result::UNSAT ) {
+      Command* gp = new GetProofCommand();
+      status = doCommandSingleton(gp);
+    }
   }
   return status;
 }
diff --git a/src/main/command_executor_portfolio.cpp b/src/main/command_executor_portfolio.cpp
index 971aa2131..24469c668 100644
--- a/src/main/command_executor_portfolio.cpp
+++ b/src/main/command_executor_portfolio.cpp
@@ -213,7 +213,6 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
     if(d_lastWinner != 0) delete cmdExported;
     return ret;
   } else if(mode == 1) {               // portfolio
-
     d_seq->addCommand(cmd->clone());
 
     // We currently don't support changing number of threads for each
@@ -327,7 +326,26 @@ bool CommandExecutorPortfolio::doCommandSingleton(Command* cmd)
     lemmaSharingCleanup();
 
     delete[] fns;
-    return portfolioReturn.second;
+
+    bool status = portfolioReturn.second;
+
+    // dump the model/proof if option is set
+    if(status) {
+      if( d_options[options::produceModels] &&
+          d_options[options::dumpModels] &&
+          ( d_result.asSatisfiabilityResult() == Result::SAT ||
+            (d_result.isUnknown() && d_result.whyUnknown() == Result::INCOMPLETE) ) ) {
+        Command* gm = new GetModelCommand();
+        status = doCommandSingleton(gm);
+      } else if( d_options[options::proof] &&
+                 d_options[options::dumpProofs] &&
+                 d_result.asSatisfiabilityResult() == Result::UNSAT ) {
+        Command* gp = new GetProofCommand();
+        status = doCommandSingleton(gp);
+      }
+    }
+
+    return status;
   } else if(mode == 2) {
     Command* cmdExported = 
       d_lastWinner == 0 ?
diff --git a/src/main/driver_unified.cpp b/src/main/driver_unified.cpp
index d1baaa2e9..bf66629dd 100644
--- a/src/main/driver_unified.cpp
+++ b/src/main/driver_unified.cpp
@@ -108,6 +108,10 @@ int runCvc4(int argc, char* argv[], Options& opts) {
       ! opts[options::threadArgv].empty() ) {
     throw OptionException("Thread options cannot be used with sequential CVC4.  Please build and use the portfolio binary `pcvc4'.");
   }
+# else
+  if( opts[options::checkProofs] ) {
+    throw OptionException("Cannot run portfolio in check-proofs mode.");
+  }
 # endif
 
   progName = opts[options::binary_name].c_str();
@@ -201,8 +205,7 @@ int runCvc4(int argc, char* argv[], Options& opts) {
              << "Notice: ...the experimental --incremental-parallel option.\n";
     exprMgr = new ExprManager(opts);
     pExecutor = new CommandExecutor(*exprMgr, opts);
-  }
-  else {
+  } else {
     exprMgr = new ExprManager(threadOpts[0]);
     pExecutor = new CommandExecutorPortfolio(*exprMgr, opts, threadOpts);
   }
diff --git a/src/options/mkoptions b/src/options/mkoptions
index 2ff857a2f..8a3cec494 100755
--- a/src/options/mkoptions
+++ b/src/options/mkoptions
@@ -241,6 +241,7 @@ function handle_option {
   predicates=
   links=
   links_alternate=
+  smt_links=
 
   options_already_documented=false
   alternate_options_already_documented=false
@@ -412,10 +413,28 @@ function handle_option {
            links_alternate="${links_alternate} $(echo "${args[$i]}" | sed 's,[^/]*/,,')"
          else
            links="${links} ${args[$i]}"
-           links_alternate="${links_alternate} ${args[$i]}"
          fi
        done
        ;;
+    :link-smt)
+       j=0
+       while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
+         let ++i
+         let ++j
+         if [ $j -eq 3 ]; then
+           echo "$kf:$lineno: error: attribute :link-smt can only take two arguments" >&2
+           exit 1
+         fi
+         if expr "${args[$i]}" : '.*/' &>/dev/null; then
+           echo "$kf:$lineno: error: attribute :link-smt cannot take alternates" >&2
+           exit 1
+         fi
+         smt_links="${smt_links} ${args[$i]}"
+       done
+       if [ $j -eq 1 ]; then
+         smt_links="${smt_links} \"true\""
+       fi
+       ;;
     :include)
        while [ $(($i+1)) -lt ${#args[@]} ] && ! expr "${args[$(($i+1))]}" : '\:' &>/dev/null; do
          let ++i
@@ -544,14 +563,33 @@ template <> bool Options::wasSetByUser(options::${internal}__option_t) const { r
   fi
   run_links=
   run_links_alternate=
+  run_smt_links=
+  if [ -n "$links" -a -z "$smt_links" -a -n "$smtname" ]; then
+    echo "$kf:$lineno: warning: $smtname has no :link-smt, but equivalent command-line has :link" >&2
+  elif [ -n "$smt_links" -a -z "$links" ] && [ -n "$short_option" -o -n "$short_option_alternate" -o -n "$long_option" -o "$long_option_alternate" ]; then
+    echo "$kf:$lineno: warning: $smtname has a :link-smt, but equivalent command-line has no :link" >&2
+  fi
   if [ -n "$links" ]; then
+    # command-line links
     for link in $links; do
       run_links="$run_links
 #line $lineno \"$kf\"
       preemptGetopt(extra_argc, extra_argv, \"$link\");"
     done
   fi
+  if [ -n "$smt_links" ]; then
+    # smt links
+    smt_links=($smt_links)
+    i=0
+    while [ $i -lt ${#smt_links[@]} ]; do
+      run_smt_links="$run_smt_links
+#line $lineno \"$kf\"
+    smt->setOption(std::string(\"${smt_links[$i]}\"), SExpr(${smt_links[$(($i+1))]}));"
+      i=$((i+2))
+    done
+  fi
   if [ -n "$links_alternate" ]; then
+    # command-line links
     for link in $links_alternate; do
       run_links_alternate="$run_links_alternate
 #line $lineno \"$kf\"
@@ -732,7 +770,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
-    Options::current().assignBool(options::$internal, \"$smtname\", optionarg == \"true\", smt);$run_links
+    Options::current().assignBool(options::$internal, \"$smtname\", optionarg == \"true\", smt);$run_smt_links
     return;
   }"
     elif [ -n "$expect_arg" -a "$internal" != - ]; then
@@ -749,7 +787,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
-    Options::current().assign(options::$internal, \"$smtname\", optionarg, smt);$run_links
+    Options::current().assign(options::$internal, \"$smtname\", optionarg, smt);$run_smt_links
     return;
   }"
     elif [ -n "$expect_arg" ]; then
@@ -764,7 +802,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
-    $run_handlers$run_links
+    $run_handlers$run_smt_links
     return;
   }"
     else
@@ -779,7 +817,7 @@ template <> options::${internal}__option_t::type runHandlerAndPredicates(options
 #line $lineno \"$kf\"
   if(key == \"$smtname\") {
 #line $lineno \"$kf\"
-    $run_handlers$run_links
+    $run_handlers$run_smt_links
     return;
   }"
     fi
diff --git a/src/printer/ast/ast_printer.cpp b/src/printer/ast/ast_printer.cpp
index 8ab5c121d..72bfa5603 100644
--- a/src/printer/ast/ast_printer.cpp
+++ b/src/printer/ast/ast_printer.cpp
@@ -153,6 +153,7 @@ void AstPrinter::toStream(std::ostream& out, const Command* c,
      tryToStream<GetModelCommand>(out, c) ||
      tryToStream<GetAssignmentCommand>(out, c) ||
      tryToStream<GetAssertionsCommand>(out, c) ||
+     tryToStream<GetProofCommand>(out, c) ||
      tryToStream<SetBenchmarkStatusCommand>(out, c) ||
      tryToStream<SetBenchmarkLogicCommand>(out, c) ||
      tryToStream<SetInfoCommand>(out, c) ||
@@ -307,6 +308,9 @@ static void toStream(std::ostream& out, const GetAssignmentCommand* c) throw() {
 static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() {
   out << "GetAssertions()";
 }
+static void toStream(std::ostream& out, const GetProofCommand* c) throw() {
+  out << "GetProof()";
+}
 static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() {
   out << "SetBenchmarkStatus(" << c->getStatus() << ")";
 }
diff --git a/src/printer/cvc/cvc_printer.cpp b/src/printer/cvc/cvc_printer.cpp
index bd2626ddd..49ded4ecb 100644
--- a/src/printer/cvc/cvc_printer.cpp
+++ b/src/printer/cvc/cvc_printer.cpp
@@ -776,6 +776,7 @@ void CvcPrinter::toStream(std::ostream& out, const Command* c,
      tryToStream<GetModelCommand>(out, c) ||
      tryToStream<GetAssignmentCommand>(out, c) ||
      tryToStream<GetAssertionsCommand>(out, c) ||
+     tryToStream<GetProofCommand>(out, c) ||
      tryToStream<SetBenchmarkStatusCommand>(out, c) ||
      tryToStream<SetBenchmarkLogicCommand>(out, c) ||
      tryToStream<SetInfoCommand>(out, c) ||
@@ -1031,6 +1032,10 @@ static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() {
   out << "WHERE;";
 }
 
+static void toStream(std::ostream& out, const GetProofCommand* c) throw() {
+  out << "DUMP_PROOF;";
+}
+
 static void toStream(std::ostream& out, const SetBenchmarkStatusCommand* c) throw() {
   out << "% (set-info :status " << c->getStatus() << ")";
 }
diff --git a/src/printer/smt2/smt2_printer.cpp b/src/printer/smt2/smt2_printer.cpp
index b743ba70e..c56d87da6 100644
--- a/src/printer/smt2/smt2_printer.cpp
+++ b/src/printer/smt2/smt2_printer.cpp
@@ -577,6 +577,7 @@ void Smt2Printer::toStream(std::ostream& out, const Command* c,
      tryToStream<GetModelCommand>(out, c) ||
      tryToStream<GetAssignmentCommand>(out, c) ||
      tryToStream<GetAssertionsCommand>(out, c) ||
+     tryToStream<GetProofCommand>(out, c) ||
      tryToStream<SetBenchmarkStatusCommand>(out, c) ||
      tryToStream<SetBenchmarkLogicCommand>(out, c) ||
      tryToStream<SetInfoCommand>(out, c) ||
@@ -858,6 +859,10 @@ static void toStream(std::ostream& out, const GetAssertionsCommand* c) throw() {
   out << "(get-assertions)";
 }
 
+static void toStream(std::ostream& out, const GetProofCommand* c) throw() {
+  out << "(get-proof)";
+}
+
 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 8e9c4cd21..39e802b62 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -32,37 +32,45 @@ CnfProof::CnfProof(CnfStream* stream)
 
 
 Expr CnfProof::getAtom(prop::SatVariable var) {
-  prop::SatLiteral lit (var); 
-  Node node = d_cnfStream->getNode(lit); 
+  prop::SatLiteral lit (var);
+  Node node = d_cnfStream->getNode(lit);
   Expr atom = node.toExpr();
-  return atom; 
+  return atom;
 }
 
 CnfProof::~CnfProof() {
 }
 
+LFSCCnfProof::iterator LFSCCnfProof::begin_atom_mapping() {
+  return iterator(*this, ProofManager::currentPM()->begin_vars());
+}
+
+LFSCCnfProof::iterator LFSCCnfProof::end_atom_mapping() {
+  return iterator(*this, ProofManager::currentPM()->end_vars());
+}
+
 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::printFormula(atom, os);
+      LFSCTheoryProof::printTerm(atom, os);
     } else {
       // print fake atoms for all other logics
-      os << "true "; 
+      os << "true ";
     }
 
     os << " (\\ " << ProofManager::getVarName(*it) << " (\\ " << ProofManager::getAtomName(*it) << "\n";
-    paren << ")))"; 
+    paren << ")))";
   }
 }
 
 void LFSCCnfProof::printClauses(std::ostream& os, std::ostream& paren) {
-  printInputClauses(os, paren); 
+  printInputClauses(os, paren);
   printTheoryLemmas(os, paren);
 }
 
@@ -70,51 +78,49 @@ void LFSCCnfProof::printInputClauses(std::ostream& os, std::ostream& paren) {
   os << " ;; Input 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;
     os << "(satlem _ _ ";
-    std::ostringstream clause_paren; 
+    std::ostringstream clause_paren;
     printClause(*clause, os, clause_paren);
     os << " (clausify_false trust)" << clause_paren.str();
-    os << "( \\ " << ProofManager::getInputClauseName(id) << "\n"; 
-    paren << "))"; 
+    os << "( \\ " << ProofManager::getInputClauseName(id) << "\n";
+    paren << "))";
   }
 }
 
 
 void LFSCCnfProof::printTheoryLemmas(std::ostream& os, std::ostream& paren) {
-  os << " ;; Theory Lemmas \n";  
+  os << " ;; Theory Lemmas \n";
   ProofManager::clause_iterator it = ProofManager::currentPM()->begin_lemmas();
   ProofManager::clause_iterator end = ProofManager::currentPM()->end_lemmas();
-  
+
   for (; it != end; ++it) {
     ClauseId id = it->first;
     const prop::SatClause* clause = it->second;
     os << "(satlem _ _ ";
-    std::ostringstream clause_paren; 
+    std::ostringstream clause_paren;
     printClause(*clause, os, clause_paren);
     os << " (clausify_false trust)" << clause_paren.str();
-    os << "( \\ " << ProofManager::getLemmaClauseName(id) <<"\n"; 
-    paren << "))"; 
+    os << "( \\ " << ProofManager::getLemmaClauseName(id) <<"\n";
+    paren << "))";
   }
 }
 
 void LFSCCnfProof::printClause(const prop::SatClause& clause, std::ostream& os, std::ostream& paren) {
   for (unsigned i = 0; i < clause.size(); ++i) {
     prop::SatLiteral lit = clause[i];
-    prop::SatVariable var = lit.getSatVariable(); 
+    prop::SatVariable var = lit.getSatVariable();
     if (lit.isNegated()) {
       os << "(ast _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " ";
-      paren << "))"; 
+      paren << "))";
     } else {
       os << "(asf _ _ _ " << ProofManager::getAtomName(var) <<" (\\ " << ProofManager::getLitName(lit) << " ";
-      paren << "))"; 
+      paren << "))";
     }
   }
 }
 
-
 } /* CVC4 namespace */
-
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 9a2dbe655..0a932f906 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -13,7 +13,7 @@
  **
  ** A manager for CnfProofs.
  **
- ** 
+ **
  **/
 
 #ifndef __CVC4__CNF_PROOF_H
@@ -25,36 +25,68 @@
 
 #include <ext/hash_set>
 #include <ext/hash_map>
-#include <iostream> 
+#include <iostream>
 
 namespace CVC4 {
 namespace prop {
-class CnfStream;
+  class CnfStream;
 }
 
+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;
 public:
   CnfProof(CVC4::prop::CnfStream* cnfStream);
 
+  typedef AtomIterator iterator;
+  virtual iterator begin_atom_mapping() = 0;
+  virtual iterator end_atom_mapping() = 0;
+
   virtual void printAtomMapping(std::ostream& os, std::ostream& paren) = 0;
   virtual void printClauses(std::ostream& os, std::ostream& paren) = 0;
-  virtual ~CnfProof(); 
+  virtual ~CnfProof();
 };
 
-class LFSCCnfProof: public 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);
+
 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);
+}
+
 } /* CVC4 namespace */
+
 #endif /* __CVC4__CNF_PROOF_H */
diff --git a/src/proof/proof.h b/src/proof/proof.h
index 02f8f7684..e3b776cce 100644
--- a/src/proof/proof.h
+++ b/src/proof/proof.h
@@ -23,7 +23,7 @@
 
 #ifdef CVC4_PROOF
 #  define PROOF(x) if(options::proof()) { x; }
-#  define NULLPROOF(x) (options::proof())? x : NULL
+#  define NULLPROOF(x) (options::proof()) ? x : NULL
 #  define PROOF_ON() options::proof()
 #else /* CVC4_PROOF */
 #  define PROOF(x)
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 110e6b79a..14a82b17b 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -28,14 +28,10 @@ namespace CVC4 {
 
 std::string append(const std::string& str, uint64_t num) {
   std::ostringstream os;
-  os << str << num; 
-  return os.str(); 
+  os << str << num;
+  return os.str();
 }
 
-
-bool          ProofManager::isInitialized = false;
-ProofManager* ProofManager::proofManager = NULL;
-
 ProofManager::ProofManager(ProofFormat format):
   d_satProof(NULL),
   d_cnfProof(NULL),
@@ -50,41 +46,43 @@ ProofManager::~ProofManager() {
   delete d_cnfProof;
   delete d_theoryProof;
   delete d_fullProof;
-  for (IdToClause::iterator it = d_inputClauses.begin(); it != d_inputClauses.end(); ++it) {
-    delete it->second; 
+
+  for(IdToClause::iterator it = d_inputClauses.begin();
+      it != d_inputClauses.end();
+      ++it) {
+    delete it->second;
   }
-  for (IdToClause::iterator it = d_theoryLemmas.begin(); it != d_theoryLemmas.end(); ++it) {
-    delete it->second; 
+
+  for(IdToClause::iterator it = d_theoryLemmas.begin();
+      it != d_theoryLemmas.end();
+      ++it) {
+    delete it->second;
   }
-  // FIXME: memory leak because there are deleted theory lemmas that were not used in the
-  // SatProof 
+
+  // FIXME: memory leak because there are deleted theory lemmas that
+  // were not used in the SatProof
 }
 
 ProofManager* ProofManager::currentPM() {
-  if (isInitialized) {
-    return proofManager; 
-  } else {
-    proofManager = new ProofManager();
-    isInitialized = true; 
-    return proofManager; 
-  }
+  return smt::currentProofManager();
 }
 
 Proof* ProofManager::getProof(SmtEngine* smt) {
-  if (currentPM()->d_fullProof != NULL)
+  if (currentPM()->d_fullProof != NULL) {
     return currentPM()->d_fullProof;
+  }
   Assert (currentPM()->d_format == LFSC);
 
   currentPM()->d_fullProof = new LFSCProof(smt,
                                            (LFSCSatProof*)getSatProof(),
                                            (LFSCCnfProof*)getCnfProof(),
-                                           (LFSCTheoryProof*)getTheoryProof()); 
+                                           (LFSCTheoryProof*)getTheoryProof());
   return currentPM()->d_fullProof;
 }
 
 SatProof* ProofManager::getSatProof() {
   Assert (currentPM()->d_satProof);
-  return currentPM()->d_satProof; 
+  return currentPM()->d_satProof;
 }
 
 CnfProof* ProofManager::getCnfProof() {
@@ -107,7 +105,7 @@ void ProofManager::initSatProof(Minisat::Solver* solver) {
 void ProofManager::initCnfProof(prop::CnfStream* cnfStream) {
   Assert (currentPM()->d_cnfProof == NULL);
   Assert (currentPM()->d_format == LFSC);
-  currentPM()->d_cnfProof = new LFSCCnfProof(cnfStream); 
+  currentPM()->d_cnfProof = new LFSCCnfProof(cnfStream);
 }
 
 void ProofManager::initTheoryProof() {
@@ -126,8 +124,8 @@ std::string ProofManager::getLitName(prop::SatLiteral lit) {return append("l", l
 
 void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind) {
   for (unsigned i = 0; i < clause->size(); ++i) {
-    prop::SatLiteral lit = clause->operator[](i); 
-    d_propVars.insert(lit.getSatVariable()); 
+    prop::SatLiteral lit = clause->operator[](i);
+    d_propVars.insert(lit.getSatVariable());
   }
   if (kind == INPUT) {
     d_inputClauses.insert(std::make_pair(id, clause));
@@ -138,11 +136,11 @@ void ProofManager::addClause(ClauseId id, const prop::SatClause* clause, ClauseK
 }
 
 void ProofManager::addAssertion(Expr formula) {
-  d_inputFormulas.insert(formula); 
+  d_inputFormulas.insert(formula);
 }
 
 void ProofManager::setLogic(const std::string& logic_string) {
-  d_logic = logic_string; 
+  d_logic = logic_string;
 }
 
 
@@ -158,17 +156,24 @@ LFSCProof::LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf,
 void LFSCProof::toStream(std::ostream& out) {
   smt::SmtScope scope(d_smtEngine);
   std::ostringstream paren;
-  out << "(check \n";
-  if (ProofManager::currentPM()->getLogic().compare("QF_UF") == 0) {
-    d_theoryProof->printAssertions(out, paren);
+  out << "(check\n";
+  if (d_theoryProof == NULL) {
+    d_theoryProof = new LFSCTheoryProof();
+  }
+  for(LFSCCnfProof::iterator i = d_cnfProof->begin_atom_mapping();
+      i != d_cnfProof->end_atom_mapping();
+      ++i) {
+    d_theoryProof->addDeclaration(*i);
   }
-  out << "(: (holds cln) \n";
+  d_theoryProof->printAssertions(out, paren);
+  out << "(: (holds cln)\n";
   d_cnfProof->printAtomMapping(out, paren);
   d_cnfProof->printClauses(out, paren);
-  d_satProof->printResolutions(out, paren); 
+  d_satProof->printResolutions(out, paren);
   paren <<")))\n;;";
-  out << paren.str(); 
+  out << paren.str();
+  out << "\n";
 }
 
 
-} /* CVC4  namespace */ 
+} /* CVC4  namespace */
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index e33f1a63f..ab8a7b2bc 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -9,11 +9,9 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief A manager for Proofs.
+ ** \brief A manager for Proofs
  **
  ** A manager for Proofs.
- **
- ** 
  **/
 
 #include "cvc4_private.h"
@@ -21,7 +19,7 @@
 #ifndef __CVC4__PROOF_MANAGER_H
 #define __CVC4__PROOF_MANAGER_H
 
-#include <iostream> 
+#include <iostream>
 #include "proof/proof.h"
 #include "util/proof.h"
 
@@ -29,15 +27,15 @@
 // forward declarations
 namespace Minisat {
   class Solver;
-}
+}/* Minisat namespace */
 
 namespace CVC4 {
 
 namespace prop {
   class CnfStream;
-}
+}/* CVC4::prop namespace */
 
-class SmtEngine; 
+class SmtEngine;
 
 typedef int ClauseId;
 
@@ -51,10 +49,10 @@ class LFSCCnfProof;
 class LFSCTheoryProof;
 
 namespace prop {
-typedef uint64_t SatVariable;
-class SatLiteral;
-typedef std::vector<SatLiteral> SatClause; 
-}
+  typedef uint64_t SatVariable;
+  class SatLiteral;
+  typedef std::vector<SatLiteral> SatClause;
+}/* CVC4::prop namespace */
 
 // different proof modes
 enum ProofFormat {
@@ -64,7 +62,7 @@ enum ProofFormat {
 
 std::string append(const std::string& str, uint64_t num);
 
-typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause; 
+typedef __gnu_cxx::hash_map < ClauseId, const prop::SatClause* > IdToClause;
 typedef __gnu_cxx::hash_set<prop::SatVariable > VarSet;
 typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
 
@@ -74,35 +72,36 @@ enum ClauseKind {
   INPUT,
   THEORY_LEMMA,
   LEARNT
-};
+};/* enum ClauseKind */
 
 class ProofManager {
   SatProof*    d_satProof;
   CnfProof*    d_cnfProof;
-  TheoryProof* d_theoryProof; 
+  TheoryProof* d_theoryProof;
 
   // information that will need to be shared across proofs
   IdToClause d_inputClauses;
   IdToClause d_theoryLemmas;
   ExprSet    d_inputFormulas;
   VarSet     d_propVars;
-  
-  Proof* d_fullProof; 
+
+  Proof* d_fullProof;
   ProofFormat d_format;
-  
-  static ProofManager* proofManager; 
-  static bool isInitialized; 
-  ProofManager(ProofFormat format = LFSC);
-  ~ProofManager(); 
+
 protected:
   std::string d_logic;
+
 public:
+  ProofManager(ProofFormat format = LFSC);
+  ~ProofManager();
+
   static ProofManager* currentPM();
-  // initialization 
-  static void         initSatProof(Minisat::Solver* solver); 
+
+  // initialization
+  static void         initSatProof(Minisat::Solver* solver);
   static void         initCnfProof(CVC4::prop::CnfStream* cnfStream);
   static void         initTheoryProof();
-  
+
   static Proof*       getProof(SmtEngine* smt);
   static SatProof*    getSatProof();
   static CnfProof*    getCnfProof();
@@ -110,9 +109,9 @@ public:
 
   // iterators over data shared by proofs
   typedef IdToClause::const_iterator clause_iterator;
-  typedef ExprSet::const_iterator assertions_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(); }
 
@@ -124,10 +123,10 @@ public:
 
   var_iterator begin_vars() const { return d_propVars.begin(); }
   var_iterator end_vars() const { return d_propVars.end(); }
-  
+
   void addAssertion(Expr formula);
-  void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind); 
-  
+  void addClause(ClauseId id, const prop::SatClause* clause, ClauseKind kind);
+
   // variable prefixes
   static std::string getInputClauseName(ClauseId id);
   static std::string getLemmaClauseName(ClauseId id);
@@ -136,7 +135,7 @@ public:
   static std::string getVarName(prop::SatVariable var);
   static std::string getAtomName(prop::SatVariable var);
   static std::string getLitName(prop::SatLiteral lit);
-  
+
   void setLogic(const std::string& logic_string);
   const std::string getLogic() const { return d_logic; }
 };/* class ProofManager */
@@ -145,13 +144,13 @@ class LFSCProof : public Proof {
   LFSCSatProof* d_satProof;
   LFSCCnfProof* d_cnfProof;
   LFSCTheoryProof* d_theoryProof;
-  SmtEngine* d_smtEngine; 
+  SmtEngine* d_smtEngine;
 public:
-  LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory); 
+  LFSCProof(SmtEngine* smtEngine, LFSCSatProof* sat, LFSCCnfProof* cnf, LFSCTheoryProof* theory);
   virtual void toStream(std::ostream& out);
   virtual ~LFSCProof() {}
-};
-  
+};/* class LFSCProof */
+
 }/* CVC4 namespace */
 
 #endif /* __CVC4__PROOF_MANAGER_H */
diff --git a/src/proof/sat_proof.cpp b/src/proof/sat_proof.cpp
index da9df0d42..3b5509ffb 100644
--- a/src/proof/sat_proof.cpp
+++ b/src/proof/sat_proof.cpp
@@ -25,7 +25,7 @@ using namespace Minisat;
 using namespace CVC4::prop;
 namespace CVC4 {
 
-/// some helper functions 
+/// some helper functions
 
 void printLit (Minisat::Lit l) {
   Debug("proof:sat") << (sign(l) ? "-" : "") << var(l) + 1;
@@ -33,16 +33,16 @@ void printLit (Minisat::Lit l) {
 
 void printClause (Minisat::Clause& c) {
   for (int i = 0; i < c.size(); i++) {
-    Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; 
+    Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " ";
   }
 }
 
 void printLitSet(const LitSet& s) {
   for(LitSet::iterator it = s.begin(); it != s.end(); ++it) {
     printLit(*it);
-    Debug("proof:sat") << " "; 
+    Debug("proof:sat") << " ";
   }
-  Debug("proof:sat") << endl; 
+  Debug("proof:sat") << endl;
 }
 
 // purely debugging functions
@@ -52,39 +52,38 @@ void printDebug (Minisat::Lit l) {
 
 void printDebug (Minisat::Clause& c) {
   for (int i = 0; i < c.size(); i++) {
-    Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " "; 
+    Debug("proof:sat") << (sign(c[i]) ? "-" : "") << var(c[i]) + 1 << " ";
   }
   Debug("proof:sat") << endl;
 }
 
 
-int SatProof::d_idCounter = 0; 
+int SatProof::d_idCounter = 0;
 
-/** 
+/**
  * Converts the clause associated to id to a set of literals
- * 
+ *
  * @param id the clause id
- * @param set the clause converted to a set of literals 
+ * @param set the clause converted to a set of literals
  */
 void SatProof::createLitSet(ClauseId id, LitSet& set) {
-  Assert (set.empty());
+  Assert(set.empty());
   if(isUnit(id)) {
     set.insert(getUnit(id));
     return;
   }
   if ( id == d_emptyClauseId) {
-    return; 
+    return;
   }
   CRef ref = getClauseRef(id);
-  Assert (ref != CRef_Undef); 
-  Clause& c = d_solver->ca[ref];
+  Clause& c = getClause(ref);
   for (int i = 0; i < c.size(); i++) {
-    set.insert(c[i]); 
+    set.insert(c[i]);
   }
 }
 
 
-/** 
+/**
  * Resolves clause1 and clause2 on variable var and stores the
  * result in clause1
  * @param v
@@ -93,36 +92,40 @@ void SatProof::createLitSet(ClauseId id, LitSet& set) {
  */
 bool resolve(const Lit v, LitSet& clause1, LitSet& clause2, bool s) {
   Assert(!clause1.empty());
-  Assert(!clause2.empty()); 
-  Lit var = sign(v) ? ~v : v; 
+  Assert(!clause2.empty());
+  Lit var = sign(v) ? ~v : v;
   if (s) {
     // literal appears positive in the first clause
     if( !clause2.count(~var)) {
-      Debug("proof:sat") << "proof:resolve: Missing literal ";
-      printLit(var);
-      Debug("proof:sat") << endl; 
-      return false; 
+      if(Debug.isOn("proof:sat")) {
+        Debug("proof:sat") << "proof:resolve: Missing literal ";
+        printLit(var);
+        Debug("proof:sat") << endl;
+      }
+      return false;
     }
     clause1.erase(var);
     clause2.erase(~var);
     for (LitSet::iterator it = clause2.begin(); it!= clause2.end(); ++it) {
-      clause1.insert(*it); 
+      clause1.insert(*it);
     }
   } else {
     // literal appears negative in the first clause
     if( !clause1.count(~var) || !clause2.count(var)) {
-      Debug("proof:sat") << "proof:resolve: Missing literal ";
-      printLit(var);
-      Debug("proof:sat") << endl; 
-      return false; 
+      if(Debug.isOn("proof:sat")) {
+        Debug("proof:sat") << "proof:resolve: Missing literal ";
+        printLit(var);
+        Debug("proof:sat") << endl;
+      }
+      return false;
     }
     clause1.erase(~var);
     clause2.erase(var);
     for (LitSet::iterator it = clause2.begin(); it!= clause2.end(); ++it) {
-      clause1.insert(*it); 
+      clause1.insert(*it);
     }
   }
-  return true; 
+  return true;
 }
 
 /// ResChain
@@ -135,16 +138,16 @@ ResChain::ResChain(ClauseId start) :
 
 void ResChain::addStep(Lit lit, ClauseId id, bool sign) {
   ResStep step(lit, id, sign);
-  d_steps.push_back(step); 
+  d_steps.push_back(step);
 }
 
 
 void ResChain::addRedundantLit(Lit lit) {
   if (d_redundantLits) {
-    d_redundantLits->insert(lit); 
+    d_redundantLits->insert(lit);
   } else {
     d_redundantLits = new LitSet();
-    d_redundantLits->insert(lit); 
+    d_redundantLits->insert(lit);
   }
 }
 
@@ -156,7 +159,7 @@ ProofProxy::ProofProxy(SatProof* proof):
 {}
 
 void ProofProxy::updateCRef(CRef oldref, CRef newref) {
-  d_proof->updateCRef(oldref, newref); 
+  d_proof->updateCRef(oldref, newref);
 }
 
 
@@ -183,27 +186,27 @@ SatProof::SatProof(Minisat::Solver* solver, bool checkRes) :
     d_seenInput(),
     d_seenLemmas()
   {
-    d_proxy = new ProofProxy(this); 
+    d_proxy = new ProofProxy(this);
   }
 
-/** 
+/**
  * Returns true if the resolution chain corresponding to id
  * does resolve to the clause associated to id
- * @param id 
- * 
- * @return 
+ * @param id
+ *
+ * @return
  */
 bool SatProof::checkResolution(ClauseId id) {
   if(d_checkRes) {
-    bool validRes = true; 
-    Assert (d_resChains.find(id) != d_resChains.end());
+    bool validRes = true;
+    Assert(d_resChains.find(id) != d_resChains.end());
     ResChain* res = d_resChains[id];
     LitSet clause1;
     createLitSet(res->getStart(), clause1);
-    ResSteps& steps = res->getSteps(); 
+    ResSteps& steps = res->getSteps();
     for (unsigned i = 0; i < steps.size(); i++) {
       Lit    var = steps[i].lit;
-      LitSet clause2; 
+      LitSet clause2;
       createLitSet (steps[i].id, clause2);
       bool res = resolve (var, clause1, clause2, steps[i].sign);
       if(res == false) {
@@ -215,35 +218,38 @@ bool SatProof::checkResolution(ClauseId id) {
     if (isUnit(id)) {
       // special case if it was a unit clause
       Lit unit = getUnit(id);
-      validRes = clause1.size() == clause1.count(unit) && !clause1.empty(); 
-      return validRes; 
+      validRes = clause1.size() == clause1.count(unit) && !clause1.empty();
+      return validRes;
     }
     if (id == d_emptyClauseId) {
-      return clause1.empty(); 
+      return clause1.empty();
     }
     CRef ref = getClauseRef(id);
-    Assert (ref != CRef_Undef);
-    Clause& c = d_solver->ca[ref];
+    Clause& c = getClause(ref);
     for (int i = 0; i < c.size(); ++i) {
       int count = clause1.erase(c[i]);
       if (count == 0) {
-        Debug("proof:sat") << "proof:checkResolution::literal not in computed result ";
-        printLit(c[i]);
-        Debug("proof:sat") << "\n";
-        validRes = false; 
+        if(Debug.isOn("proof:sat")) {
+          Debug("proof:sat") << "proof:checkResolution::literal not in computed result ";
+          printLit(c[i]);
+          Debug("proof:sat") << "\n";
+        }
+        validRes = false;
       }
     }
     validRes = clause1.empty();
     if (! validRes) {
-      Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, unremoved literals: \n";
-      printLitSet(clause1);
-      Debug("proof:sat") << "proof:checkResolution:: result should be: \n";
-      printClause(c); 
+      if(Debug.isOn("proof:sat")) {
+        Debug("proof:sat") << "proof:checkResolution::Invalid Resolution, unremoved literals: \n";
+        printLitSet(clause1);
+        Debug("proof:sat") << "proof:checkResolution:: result should be: \n";
+        printClause(c);
+      }
     }
-    return validRes; 
-    
+    return validRes;
+
   } else {
-    return true; 
+    return true;
   }
 }
 
@@ -254,16 +260,16 @@ bool SatProof::checkResolution(ClauseId id) {
 
 ClauseId SatProof::getClauseId(::Minisat::CRef ref) {
   if(d_clauseId.find(ref) == d_clauseId.end()) {
-    Debug("proof:sat") << "Missing clause \n"; 
+    Debug("proof:sat") << "Missing clause \n";
   }
   Assert(d_clauseId.find(ref) != d_clauseId.end());
-  return d_clauseId[ref]; 
+  return d_clauseId[ref];
 }
 
 
 ClauseId SatProof::getClauseId(::Minisat::Lit lit) {
   Assert(d_unitId.find(toInt(lit)) != d_unitId.end());
-  return d_unitId[toInt(lit)]; 
+  return d_unitId[toInt(lit)];
 }
 
 Minisat::CRef SatProof::getClauseRef(ClauseId id) {
@@ -273,79 +279,85 @@ Minisat::CRef SatProof::getClauseRef(ClauseId id) {
                        << (isUnit(id)? "Unit" : "") << endl;
   }
   Assert(d_idClause.find(id) != d_idClause.end());
-  return d_idClause[id]; 
+  return d_idClause[id];
 }
 
 Clause& SatProof::getClause(CRef ref) {
-  return d_solver->ca[ref]; 
+  Assert(ref != CRef_Undef);
+  Assert(ref >= 0 && ref < d_solver->ca.size());
+  return d_solver->ca[ref];
 }
+
 Minisat::Lit SatProof::getUnit(ClauseId id) {
-  Assert (d_idUnit.find(id) != d_idUnit.end());
-  return d_idUnit[id]; 
+  Assert(d_idUnit.find(id) != d_idUnit.end());
+  return d_idUnit[id];
 }
 
 bool SatProof::isUnit(ClauseId id) {
-  return d_idUnit.find(id) != d_idUnit.end(); 
+  return d_idUnit.find(id) != d_idUnit.end();
 }
 
 bool SatProof::isUnit(::Minisat::Lit lit) {
-  return d_unitId.find(toInt(lit)) != d_unitId.end(); 
+  return d_unitId.find(toInt(lit)) != d_unitId.end();
 }
 
 ClauseId SatProof::getUnitId(::Minisat::Lit lit) {
-  Assert(isUnit(lit)); 
-  return d_unitId[toInt(lit)]; 
+  Assert(isUnit(lit));
+  return d_unitId[toInt(lit)];
 }
 
 bool SatProof::hasResolution(ClauseId id) {
-  return d_resChains.find(id) != d_resChains.end(); 
+  return d_resChains.find(id) != d_resChains.end();
 }
 
 bool SatProof::isInputClause(ClauseId id) {
-  return (d_inputClauses.find(id) != d_inputClauses.end()); 
+  return (d_inputClauses.find(id) != d_inputClauses.end());
 }
 
 bool SatProof::isLemmaClause(ClauseId id) {
-  return (d_lemmaClauses.find(id) != d_lemmaClauses.end()); 
+  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)); 
+    printLit(getUnit(id));
   } else if (id == d_emptyClauseId) {
-    Debug("proof:sat") << "empty "<< endl; 
+    Debug("proof:sat") << "empty "<< endl;
   }
   else {
-    CRef ref  = getClauseRef(id);
-    Assert (ref != CRef_Undef);
-    printClause(d_solver->ca[ref]);
+    CRef ref = getClauseRef(id);
+    printClause(getClause(ref));
   }
 }
 
 void SatProof::printRes(ClauseId id) {
   Assert(hasResolution(id));
   Debug("proof:sat") << "id "<< id <<": ";
-  printRes(d_resChains[id]); 
+  printRes(d_resChains[id]);
 }
 
 void SatProof::printRes(ResChain* res) {
   ClauseId start_id = res->getStart();
 
-  Debug("proof:sat") << "(";
-  print(start_id); 
+  if(Debug.isOn("proof:sat")) {
+    Debug("proof:sat") << "(";
+    print(start_id);
+  }
 
   ResSteps& steps = res->getSteps();
   for(unsigned i = 0; i < steps.size(); i++ ) {
     Lit v = steps[i].lit;
     ClauseId id = steps[i].id;
 
-    Debug("proof:sat") << "[";
-    printLit(v);
-    Debug("proof:sat") << "] ";
-    print(id); 
+    if(Debug.isOn("proof:sat")) {
+      Debug("proof:sat") << "[";
+      printLit(v);
+      Debug("proof:sat") << "] ";
+      print(id);
+    }
   }
   Debug("proof:sat") << ") \n";
 }
@@ -353,23 +365,23 @@ void SatProof::printRes(ResChain* res) {
 /// registration methods
 
 ClauseId SatProof::registerClause(::Minisat::CRef clause, ClauseKind kind) {
-  Assert(clause != CRef_Undef); 
+  Assert(clause != CRef_Undef);
   ClauseIdMap::iterator it = d_clauseId.find(clause);
-   if (it == d_clauseId.end()) {
-     ClauseId newId = d_idCounter++; 
-     d_clauseId[clause]= newId;
-     d_idClause[newId] =clause;
-     if (kind == INPUT) {
-       Assert (d_inputClauses.find(newId) == d_inputClauses.end()); 
-       d_inputClauses.insert(newId); 
-     }
-     if (kind == THEORY_LEMMA) {
-       Assert (d_lemmaClauses.find(newId) == d_lemmaClauses.end());
-       d_lemmaClauses.insert(newId); 
-     }
-   }
-   Debug("proof:sat:detailed") <<"registerClause CRef:" << clause <<" id:" << d_clauseId[clause] << " " << kind << "\n"; 
-   return d_clauseId[clause]; 
+  if (it == d_clauseId.end()) {
+    ClauseId newId = d_idCounter++;
+    d_clauseId[clause] = newId;
+    d_idClause[newId] = clause;
+    if (kind == INPUT) {
+      Assert(d_inputClauses.find(newId) == d_inputClauses.end());
+      d_inputClauses.insert(newId);
+    }
+    if (kind == THEORY_LEMMA) {
+      Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
+      d_lemmaClauses.insert(newId);
+    }
+  }
+  Debug("proof:sat:detailed") <<"registerClause CRef:" << clause <<" id:" << d_clauseId[clause] << " " << kind << "\n";
+  return d_clauseId[clause];
 }
 
 ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind) {
@@ -377,44 +389,42 @@ ClauseId SatProof::registerUnitClause(::Minisat::Lit lit, ClauseKind kind) {
   if (it == d_unitId.end()) {
     ClauseId newId = d_idCounter++;
     d_unitId[toInt(lit)] = newId;
-    d_idUnit[newId] = lit; 
+    d_idUnit[newId] = lit;
     if (kind == INPUT) {
-      Assert (d_inputClauses.find(newId) == d_inputClauses.end());
-      d_inputClauses.insert(newId); 
+      Assert(d_inputClauses.find(newId) == d_inputClauses.end());
+      d_inputClauses.insert(newId);
     }
     if (kind == THEORY_LEMMA) {
-      Assert (d_lemmaClauses.find(newId) == d_lemmaClauses.end());
-      d_lemmaClauses.insert(newId); 
+      Assert(d_lemmaClauses.find(newId) == d_lemmaClauses.end());
+      d_lemmaClauses.insert(newId);
     }
-
   }
-  Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << kind <<"\n"; 
-  return d_unitId[toInt(lit)]; 
+  Debug("proof:sat:detailed") <<"registerUnitClause " << d_unitId[toInt(lit)] << " " << kind <<"\n";
+  return d_unitId[toInt(lit)];
 }
 
 void SatProof::removedDfs(::Minisat::Lit lit, LitSet* removedSet, LitVector& removeStack, LitSet& inClause, LitSet& seen) {
   // if we already added the literal return
   if (seen.count(lit)) {
-    return; 
+    return;
   }
 
   CRef reason_ref = d_solver->reason(var(lit));
   if (reason_ref == CRef_Undef) {
     seen.insert(lit);
-    removeStack.push_back(lit); 
-    return; 
+    removeStack.push_back(lit);
+    return;
   }
 
-  Assert (reason_ref != CRef_Undef); 
-  int size = d_solver->ca[reason_ref].size();
+  int size = getClause(reason_ref).size();
   for (int i = 1; i < size; i++ ) {
-    Lit v = d_solver->ca[reason_ref][i];
+    Lit v = getClause(reason_ref)[i];
     if(inClause.count(v) == 0 && seen.count(v) == 0) {
       removedDfs(v, removedSet, removeStack, inClause, seen);
     }
   }
   if(seen.count(lit) == 0) {
-    seen.insert(lit); 
+    seen.insert(lit);
     removeStack.push_back(lit);
   }
 }
@@ -427,39 +437,41 @@ void SatProof::removeRedundantFromRes(ResChain* res, ClauseId id) {
   }
 
   LitSet inClause;
-  createLitSet(id, inClause); 
-  
+  createLitSet(id, inClause);
+
   LitVector removeStack;
-  LitSet seen; 
+  LitSet seen;
   for (LitSet::iterator it = removed->begin(); it != removed->end(); ++it) {
-    removedDfs(*it, removed, removeStack, inClause, seen); 
+    removedDfs(*it, removed, removeStack, inClause, seen);
   }
-  
+
   for (int i = removeStack.size()-1; i >= 0; --i) {
     Lit lit = removeStack[i];
     CRef reason_ref = d_solver->reason(var(lit));
-    ClauseId reason_id; 
+    ClauseId reason_id;
 
     if (reason_ref == CRef_Undef) {
       Assert(isUnit(~lit));
-      reason_id = getUnitId(~lit); 
+      reason_id = getUnitId(~lit);
     } else {
       reason_id = registerClause(reason_ref);
     }
     res->addStep(lit, reason_id, !sign(lit));
   }
-  removed->clear(); 
+  removed->clear();
 }
 
 void SatProof::registerResolution(ClauseId id, ResChain* res) {
   Assert(res != NULL);
 
   removeRedundantFromRes(res, id);
-  Assert(res->redundantRemoved()); 
+  Assert(res->redundantRemoved());
 
   d_resChains[id] = res;
-  printRes(id); 
-  if (d_checkRes) {
+  if(Debug.isOn("proof:sat")) {
+    printRes(id);
+  }
+  if(d_checkRes) {
     Assert(checkResolution(id));
   }
 }
@@ -468,48 +480,46 @@ void SatProof::registerResolution(ClauseId id, ResChain* res) {
 /// recording resolutions
 
 void SatProof::startResChain(::Minisat::CRef start) {
-  ClauseId id = getClauseId(start); 
+  ClauseId id = getClauseId(start);
   ResChain* res = new ResChain(id);
-  d_resStack.push_back(res); 
+  d_resStack.push_back(res);
 }
 
 void SatProof::addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign) {
   ClauseId id = registerClause(clause);
   ResChain* res = d_resStack.back();
-  res->addStep(lit, id, sign); 
+  res->addStep(lit, id, sign);
 }
 
 void SatProof::endResChain(CRef clause) {
   Assert(d_resStack.size() > 0);
-  ClauseId  id = registerClause(clause); 
+  ClauseId id = registerClause(clause);
   ResChain* res = d_resStack.back();
   registerResolution(id, res);
-  d_resStack.pop_back(); 
+  d_resStack.pop_back();
 }
 
 
 void SatProof::endResChain(::Minisat::Lit lit) {
   Assert(d_resStack.size() > 0);
-  ClauseId  id = registerUnitClause(lit); 
+  ClauseId id = registerUnitClause(lit);
   ResChain* res = d_resStack.back();
-  
-
   registerResolution(id, res);
-  d_resStack.pop_back(); 
+  d_resStack.pop_back();
 }
 
 void SatProof::storeLitRedundant(::Minisat::Lit lit) {
   Assert(d_resStack.size() > 0);
   ResChain* res = d_resStack.back();
-  res->addRedundantLit(lit);  
+  res->addRedundantLit(lit);
 }
 
-/// constructing resolutions 
+/// constructing resolutions
 
 void SatProof::resolveOutUnit(::Minisat::Lit lit) {
   ClauseId id = resolveUnit(~lit);
   ResChain* res = d_resStack.back();
-  res->addStep(lit, id, !sign(lit)); 
+  res->addStep(lit, id, !sign(lit));
 }
 
 void SatProof::storeUnitResolution(::Minisat::Lit lit) {
@@ -520,28 +530,30 @@ ClauseId SatProof::resolveUnit(::Minisat::Lit lit) {
   // first check if we already have a resolution for lit
   if(isUnit(lit)) {
     ClauseId id = getClauseId(lit);
-    if(hasResolution(id) || isInputClause(id)) {
-      return id; 
-    }
-    Assert (false); 
+    Assert(hasResolution(id) || isInputClause(id) || isLemmaClause(id));
+    return id;
   }
   CRef reason_ref = d_solver->reason(var(lit));
-  Assert (reason_ref != CRef_Undef);
-  
-  ClauseId reason_id = registerClause(reason_ref); 
-
-  ResChain* res = new ResChain(reason_id); 
-  Clause& reason  = d_solver->ca[reason_ref];
-  for (int i = 0; i < reason.size(); i++) {
-    Lit l = reason[i];
-    if(lit != l) { 
+  Assert(reason_ref != CRef_Undef);
+
+  ClauseId reason_id = registerClause(reason_ref);
+
+  ResChain* res = new ResChain(reason_id);
+  // Here, the call to resolveUnit() can reallocate memory in the
+  // clause allocator.  So reload reason ptr each time.
+  Clause* reason = &getClause(reason_ref);
+  for (int i = 0;
+       i < reason->size();
+       i++, reason = &getClause(reason_ref)) {
+    Lit l = (*reason)[i];
+    if(lit != l) {
       ClauseId res_id = resolveUnit(~l);
       res->addStep(l, res_id, !sign(l));
     }
   }
-  ClauseId unit_id = registerUnitClause(lit); 
+  ClauseId unit_id = registerUnitClause(lit);
   registerResolution(unit_id, res);
-  return unit_id; 
+  return unit_id;
 }
 
 void SatProof::toStream(std::ostream& out) {
@@ -549,50 +561,62 @@ void SatProof::toStream(std::ostream& out) {
   Unimplemented("native proof printing not supported yet");
 }
 
-void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit) {
-  Assert (!d_storedUnitConflict); 
-  d_unitConflictId = registerUnitClause(conflict_lit);
+void SatProof::storeUnitConflict(::Minisat::Lit conflict_lit, ClauseKind kind) {
+  Assert(!d_storedUnitConflict);
+  d_unitConflictId = registerUnitClause(conflict_lit, kind);
   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) {
   Assert(d_resStack.size() == 0);
-  Assert (conflict_ref != ::Minisat::CRef_Undef);
-  ClauseId conflict_id; 
+  Assert(conflict_ref != ::Minisat::CRef_Undef);
+  ClauseId conflict_id;
   if (conflict_ref == ::Minisat::CRef_Lazy) {
-    Assert (d_storedUnitConflict); 
-    conflict_id = d_unitConflictId; 
+    Assert(d_storedUnitConflict);
+    conflict_id = d_unitConflictId;
+
+    ResChain* res = new ResChain(conflict_id);
+    Lit lit = d_idUnit[conflict_id];
+    ClauseId res_id = resolveUnit(~lit);
+    res->addStep(lit, res_id, !sign(lit));
+
+    registerResolution(d_emptyClauseId, res);
+
+    return;
   } else {
-    Assert (!d_storedUnitConflict);
+    Assert(!d_storedUnitConflict);
     conflict_id = registerClause(conflict_ref); //FIXME
   }
 
-  Debug("proof:sat") << "proof::finalizeProof Final Conflict ";
-  print(conflict_id);
-  
+  if(Debug.isOn("proof:sat")) {
+    Debug("proof:sat") << "proof::finalizeProof Final Conflict ";
+    print(conflict_id);
+  }
+
   ResChain* res = new ResChain(conflict_id);
-  Clause& conflict = d_solver->ca[conflict_ref] ;
-  for (int i = 0; i < conflict.size(); ++i) {
-    Lit lit = conflict[i];
+  // Here, the call to resolveUnit() can reallocate memory in the
+  // clause allocator.  So reload conflict ptr each time.
+  Clause* conflict = &getClause(conflict_ref);
+  for (int i = 0;
+       i < conflict->size();
+       ++i, conflict = &getClause(conflict_ref)) {
+    Lit lit = (*conflict)[i];
     ClauseId res_id = resolveUnit(~lit);
-    res->addStep(lit, res_id, !sign(lit)); 
+    res->addStep(lit, res_id, !sign(lit));
   }
   registerResolution(d_emptyClauseId, res);
-  // // FIXME: massive hack
-  // Proof* proof = ProofManager::getProof();
-  // proof->toStream(std::cout); 
 }
 
 /// CRef manager
 
 void SatProof::updateCRef(::Minisat::CRef oldref, ::Minisat::CRef newref) {
   if (d_clauseId.find(oldref) == d_clauseId.end()) {
-    return; 
+    return;
   }
   ClauseId id = getClauseId(oldref);
-  Assert (d_temp_clauseId.find(newref) == d_temp_clauseId.end());
-  Assert (d_temp_idClause.find(id) == d_temp_idClause.end()); 
+  Assert(d_temp_clauseId.find(newref) == d_temp_clauseId.end());
+  Assert(d_temp_idClause.find(id) == d_temp_idClause.end());
   d_temp_clauseId[newref] = id;
   d_temp_idClause[id] = newref;
 }
@@ -602,39 +626,39 @@ void SatProof::finishUpdateCRef() {
   d_temp_clauseId.clear();
 
   d_idClause.swap(d_temp_idClause);
-  d_temp_idClause.clear(); 
+  d_temp_idClause.clear();
 }
 
 void SatProof::markDeleted(CRef clause) {
   if (d_clauseId.find(clause) != d_clauseId.end()) {
     ClauseId id = getClauseId(clause);
-    Assert (d_deleted.find(id) == d_deleted.end()); 
+    Assert(d_deleted.find(id) == d_deleted.end());
     d_deleted.insert(id);
     if (isLemmaClause(id)) {
       const Clause& minisat_cl = getClause(clause);
-      SatClause* sat_cl = new SatClause(); 
-      MinisatSatSolver::toSatClause(minisat_cl, *sat_cl);  
-      d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl)); 
+      SatClause* sat_cl = new SatClause();
+      MinisatSatSolver::toSatClause(minisat_cl, *sat_cl);
+      d_deletedTheoryLemmas.insert(std::make_pair(id, sat_cl));
     }
   }
 }
 
 void SatProof::constructProof() {
-  collectClauses(d_emptyClauseId); 
+  collectClauses(d_emptyClauseId);
 }
 
 std::string SatProof::clauseName(ClauseId id) {
   ostringstream os;
   if (isInputClause(id)) {
-    os << ProofManager::getInputClauseName(id); 
-    return os.str(); 
-  } else 
+    os << ProofManager::getInputClauseName(id);
+    return os.str();
+  } else
   if (isLemmaClause(id)) {
-    os << ProofManager::getLemmaClauseName(id); 
-    return os.str(); 
+    os << ProofManager::getLemmaClauseName(id);
+    return os.str();
   }else {
     os << ProofManager::getLearntClauseName(id);
-    return os.str(); 
+    return os.str();
   }
 }
 
@@ -643,58 +667,56 @@ void SatProof::addToProofManager(ClauseId id, ClauseKind kind) {
     Minisat::Lit lit = getUnit(id);
     prop::SatLiteral sat_lit = MinisatSatSolver::toSatLiteral(lit);
     prop::SatClause* clause = new SatClause();
-    clause->push_back(sat_lit); 
-    ProofManager::currentPM()->addClause(id, clause, kind); 
-    return; 
+    clause->push_back(sat_lit);
+    ProofManager::currentPM()->addClause(id, clause, kind);
+    return;
   }
-  
+
   if (isDeleted(id)) {
-    Assert (kind == THEORY_LEMMA);
+    Assert(kind == THEORY_LEMMA);
     SatClause* clause = d_deletedTheoryLemmas.find(id)->second;
-    ProofManager::currentPM()->addClause(id, clause, kind);  
-    return; 
+    ProofManager::currentPM()->addClause(id, clause, kind);
+    return;
   }
-  
+
   CRef ref = getClauseRef(id);
   const Clause& minisat_cl = getClause(ref);
   SatClause* clause = new SatClause();
-  MinisatSatSolver::toSatClause(minisat_cl, *clause);  
-  ProofManager::currentPM()->addClause(id, clause, kind); 
+  MinisatSatSolver::toSatClause(minisat_cl, *clause);
+  ProofManager::currentPM()->addClause(id, clause, kind);
 }
 
 void SatProof::collectClauses(ClauseId id) {
   if (d_seenLearnt.find(id) != d_seenLearnt.end()) {
-    return; 
+    return;
   }
   if (d_seenInput.find(id) != d_seenInput.end()) {
-    return; 
+    return;
   }
   if (d_seenLemmas.find(id) != d_seenLemmas.end()) {
-    return; 
+    return;
   }
 
   if (isInputClause(id)) {
-    addToProofManager(id, INPUT); 
+    addToProofManager(id, INPUT);
     d_seenInput.insert(id);
-    return; 
-  }
-  else if (isLemmaClause(id)) {
-    addToProofManager(id, THEORY_LEMMA); 
+    return;
+  } else if (isLemmaClause(id)) {
+    addToProofManager(id, THEORY_LEMMA);
     d_seenLemmas.insert(id);
-    return; 
-  } 
-  else {
-    d_seenLearnt.insert(id); 
+    return;
+  } else {
+    d_seenLearnt.insert(id);
   }
 
-  Assert (d_resChains.find(id) != d_resChains.end()); 
+  Assert(d_resChains.find(id) != d_resChains.end());
   ResChain* res = d_resChains[id];
   ClauseId start = res->getStart();
   collectClauses(start);
 
-  ResSteps steps = res->getSteps(); 
-  for(unsigned i = 0; i < steps.size(); i++) {
-    collectClauses(steps[i].id); 
+  ResSteps steps = res->getSteps();
+  for(size_t i = 0; i < steps.size(); i++) {
+    collectClauses(steps[i].id);
   }
 }
 
@@ -703,29 +725,29 @@ void SatProof::collectClauses(ClauseId id) {
 void LFSCSatProof::printResolution(ClauseId id, std::ostream& out, std::ostream& paren) {
   out << "(satlem_simplify _ _ _ ";
 
-  ResChain* res = d_resChains[id];  
+  ResChain* res = d_resChains[id];
   ResSteps& steps = res->getSteps();
-  
+
   for (int i = steps.size()-1; i >= 0; i--) {
     out << "(";
     out << (steps[i].sign? "R" : "Q") << " _ _ ";
-              
+
   }
-  
+
   ClauseId start_id = res->getStart();
   // WHY DID WE NEED THIS?
   // if(isInputClause(start_id)) {
-  //   d_seenInput.insert(start_id); 
+  //   d_seenInput.insert(start_id);
   // }
   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)";
-    return; 
+    return;
   }
 
   out << "(\\" << clauseName(id) << "\n";   // bind to lemma name
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index a4178f518..477eeeb99 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -9,7 +9,7 @@
  ** See the file COPYING in the top-level source directory for licensing
  ** information.\endverbatim
  **
- ** \brief Resolution proof 
+ ** \brief Resolution proof
  **
  ** Resolution proof
  **/
@@ -43,11 +43,11 @@ namespace std {
 
 namespace CVC4 {
 
-/** 
+/**
  * Helper debugging functions
  */
 void printDebug(::Minisat::Lit l);
-void printDebug(::Minisat::Clause& c); 
+void printDebug(::Minisat::Clause& c);
 
 struct ResStep {
   ::Minisat::Lit lit;
@@ -60,8 +60,8 @@ struct ResStep {
   {}
 };/* struct ResStep */
 
-typedef std::vector< ResStep > ResSteps; 
-typedef std::set < ::Minisat::Lit> LitSet; 
+typedef std::vector< ResStep > ResSteps;
+typedef std::set < ::Minisat::Lit> LitSet;
 
 class ResChain {
 private:
@@ -72,7 +72,7 @@ public:
   ResChain(ClauseId start);
   void addStep(::Minisat::Lit, ClauseId, bool);
   bool redundantRemoved() { return (d_redundantLits == NULL || d_redundantLits->empty()); }
-  void addRedundantLit(::Minisat::Lit lit); 
+  void addRedundantLit(::Minisat::Lit lit);
   ~ResChain();
   // accessor methods
   ClauseId  getStart()     { return d_start; }
@@ -83,16 +83,16 @@ public:
 typedef std::hash_map < ClauseId, ::Minisat::CRef > IdCRefMap;
 typedef std::hash_map < ::Minisat::CRef, ClauseId > ClauseIdMap;
 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_map < int, ClauseId>            UnitIdMap; //FIXME
+typedef std::hash_map < ClauseId, ResChain*>      IdResMap;
 typedef std::hash_set < ClauseId >                IdHashSet;
-typedef std::vector   < ResChain* >               ResStack; 
-typedef std::hash_map <ClauseId, prop::SatClause* >     IdToSatClause;             
-typedef std::set < ClauseId >                     IdSet; 
-typedef std::vector < ::Minisat::Lit >              LitVector; 
+typedef std::vector   < ResChain* >               ResStack;
+typedef std::hash_map <ClauseId, prop::SatClause* >     IdToSatClause;
+typedef std::set < ClauseId >                     IdSet;
+typedef std::vector < ::Minisat::Lit >              LitVector;
 typedef __gnu_cxx::hash_map<ClauseId, ::Minisat::Clause& > IdToMinisatClause;
 
-class SatProof; 
+class SatProof;
 
 class ProofProxy : public ProofProxyAbstract {
 private:
@@ -103,31 +103,31 @@ public:
 };/* class ProofProxy */
 
 
-class CnfProof; 
+class CnfProof;
 
 class SatProof {
 protected:
   ::Minisat::Solver*    d_solver;
-  // clauses 
+  // clauses
   IdCRefMap           d_idClause;
   ClauseIdMap         d_clauseId;
   IdUnitMap           d_idUnit;
   UnitIdMap           d_unitId;
   IdHashSet           d_deleted;
-  IdToSatClause       d_deletedTheoryLemmas; 
-  IdHashSet           d_inputClauses; 
-  IdHashSet           d_lemmaClauses; 
-  // resolutions 
+  IdToSatClause       d_deletedTheoryLemmas;
+  IdHashSet           d_inputClauses;
+  IdHashSet           d_lemmaClauses;
+  // resolutions
   IdResMap            d_resChains;
-  ResStack            d_resStack; 
+  ResStack            d_resStack;
   bool                d_checkRes;
-  
-  static ClauseId     d_idCounter; 
+
+  static ClauseId     d_idCounter;
   const ClauseId      d_emptyClauseId;
   const ClauseId      d_nullId;
-  // proxy class to break circular dependencies 
+  // proxy class to break circular dependencies
   ProofProxy*         d_proxy;
-  
+
   // temporary map for updating CRefs
   ClauseIdMap         d_temp_clauseId;
   IdCRefMap         d_temp_idClause;
@@ -135,43 +135,43 @@ protected:
   // unit conflict
   ClauseId d_unitConflictId;
   bool d_storedUnitConflict;
-public:  
+public:
   SatProof(::Minisat::Solver* solver, bool checkRes = false);
   virtual ~SatProof() {}
 protected:
-  void print(ClauseId id); 
+  void print(ClauseId id);
   void printRes(ClauseId id);
-  void printRes(ResChain* res); 
-  
+  void printRes(ResChain* res);
+
   bool isInputClause(ClauseId id);
   bool isLemmaClause(ClauseId id);
   bool isUnit(ClauseId id);
-  bool isUnit(::Minisat::Lit lit); 
-  bool hasResolution(ClauseId id); 
-  void createLitSet(ClauseId id, LitSet& set); 
+  bool isUnit(::Minisat::Lit lit);
+  bool hasResolution(ClauseId id);
+  void createLitSet(ClauseId id, LitSet& set);
   void registerResolution(ClauseId id, ResChain* res);
-  
+
   ClauseId      getClauseId(::Minisat::CRef clause);
-  ClauseId      getClauseId(::Minisat::Lit lit); 
+  ClauseId      getClauseId(::Minisat::Lit lit);
   ::Minisat::CRef getClauseRef(ClauseId id);
   ::Minisat::Lit  getUnit(ClauseId id);
-  ClauseId      getUnitId(::Minisat::Lit lit); 
+  ClauseId      getUnitId(::Minisat::Lit lit);
   ::Minisat::Clause& getClause(::Minisat::CRef ref);
   virtual void toStream(std::ostream& out);
 
   bool checkResolution(ClauseId id);
-  /** 
+  /**
    * Constructs a resolution tree that proves lit
    * and returns the ClauseId for the unit clause lit
    * @param lit the literal we are proving
-   * 
-   * @return 
+   *
+   * @return
    */
   ClauseId resolveUnit(::Minisat::Lit lit);
-  /** 
+  /**
    * Does a depth first search on removed literals and adds the literals
-   * to be removed in the proper order to the stack. 
-   * 
+   * to be removed in the proper order to the stack.
+   *
    * @param lit the literal we are recursing on
    * @param removedSet the previously computed set of redundant literals
    * @param removeStack the stack of literals in reverse order of resolution
@@ -181,71 +181,71 @@ protected:
 public:
   void startResChain(::Minisat::CRef start);
   void addResolutionStep(::Minisat::Lit lit, ::Minisat::CRef clause, bool sign);
-  /** 
+  /**
    * Pops the current resolution of the stack and stores it
    * in the resolution map. Also registers the 'clause' parameter
-   * @param clause the clause the resolution is proving 
+   * @param clause the clause the resolution is proving
    */
   void endResChain(::Minisat::CRef clause);
   void endResChain(::Minisat::Lit lit);
-  /** 
-   * Stores in the current derivation the redundant literals that were 
-   * eliminated from the conflict clause during conflict clause minimization. 
-   * @param lit the eliminated literal 
+  /**
+   * Stores in the current derivation the redundant literals that were
+   * eliminated from the conflict clause during conflict clause minimization.
+   * @param lit the eliminated literal
    */
   void storeLitRedundant(::Minisat::Lit lit);
 
   /// update the CRef Id maps when Minisat does memory reallocation x
   void updateCRef(::Minisat::CRef old_ref, ::Minisat::CRef new_ref);
   void finishUpdateCRef();
-  
-  /** 
+
+  /**
    * Constructs the empty clause resolution from the final conflict
-   * 
-   * @param conflict 
+   *
+   * @param conflict
    */
   void finalizeProof(::Minisat::CRef conflict);
 
-  /// clause registration methods 
+  /// clause registration methods
   ClauseId registerClause(const ::Minisat::CRef clause, ClauseKind kind = LEARNT);
   ClauseId registerUnitClause(const ::Minisat::Lit lit, ClauseKind kind = LEARNT);
 
-  void storeUnitConflict(::Minisat::Lit lit); 
-  
-  /** 
+  void storeUnitConflict(::Minisat::Lit lit, ClauseKind kind = LEARNT);
+
+  /**
    * Marks the deleted clauses as deleted. Note we may still use them in the final
-   * resolution. 
-   * @param clause 
+   * resolution.
+   * @param clause
    */
   void markDeleted(::Minisat::CRef clause);
   bool isDeleted(ClauseId id) { return d_deleted.find(id) != d_deleted.end(); }
-  /** 
+  /**
    * Constructs the resolution of ~q and resolves it with the current
    * resolution thus eliminating q from the current clause
    * @param q the literal to be resolved out
    */
   void     resolveOutUnit(::Minisat::Lit q);
-  /** 
+  /**
    * Constructs the resolution of the literal lit. Called when a clause
-   * containing lit becomes satisfied and is removed. 
-   * @param lit 
+   * containing lit becomes satisfied and is removed.
+   * @param lit
    */
-  void     storeUnitResolution(::Minisat::Lit lit); 
-  
+  void     storeUnitResolution(::Minisat::Lit lit);
+
   ProofProxy* getProxy() {return d_proxy; }
 
   /**
-     Constructs the SAT proof identifying the needed lemmas 
+     Constructs the SAT proof identifying the needed lemmas
    */
   void constructProof();
-  
+
 protected:
   IdSet              d_seenLearnt;
   IdHashSet          d_seenInput;
-  IdHashSet          d_seenLemmas; 
-  
+  IdHashSet          d_seenLemmas;
+
   inline std::string varName(::Minisat::Lit lit);
-  inline std::string clauseName(ClauseId id); 
+  inline std::string clauseName(ClauseId id);
 
   void collectClauses(ClauseId id);
   void addToProofManager(ClauseId id, ClauseKind kind);
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index 696bd8309..4ed00aaaa 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -26,9 +26,10 @@ TheoryProof::TheoryProof()
 {}
 
 void TheoryProof::addDeclaration(Expr term) {
-  if (d_declarationCache.count(term))
+  if (d_declarationCache.count(term)) {
     return;
-  
+  }
+
   Type type = term.getType();
   if (type.isSort())
     d_sortDeclarations.insert(type);
@@ -36,32 +37,14 @@ void TheoryProof::addDeclaration(Expr term) {
     Expr function = term.getOperator();
     d_termDeclarations.insert(function);
   } else if (term.isVariable()) {
-    Assert (type.isSort()); 
+    //Assert (type.isSort() || type.isBoolean());
     d_termDeclarations.insert(term);
   }
   // recursively declare all other terms
   for (unsigned i = 0; i < term.getNumChildren(); ++i) {
-    addDeclaration(term[i]); 
-  }
-  d_declarationCache.insert(term); 
-}
-
-void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) {
-  if (term.isVariable()) {
-    os << term; 
-    return;
-  }
-
-  Assert (term.getKind() == kind::APPLY_UF);
-  Expr func = term.getOperator();
-  for (unsigned i = 0; i < term.getNumChildren(); ++i) {
-    os<< "(apply _ _ ";
-  }
-  os << func << " "; 
-  for (unsigned i = 0; i < term.getNumChildren(); ++i) {
-    printTerm(term[i], os);
-    os << ")"; 
+    addDeclaration(term[i]);
   }
+  d_declarationCache.insert(term);
 }
 
 std::string toLFSCKind(Kind kind) {
@@ -70,71 +53,138 @@ std::string toLFSCKind(Kind kind) {
   case kind::AND: return "and";
   case kind::XOR: return "xor";
   case kind::EQUAL: return "=";
+  case kind::IFF: return "iff";
   case kind::IMPLIES: return "impl";
   case kind::NOT: return "not";
   default:
-    Unreachable(); 
+    Unreachable();
   }
 }
 
-void LFSCTheoryProof::printFormula(Expr atom, std::ostream& os) {
-  // should make this more general and overall sane
-  Assert (atom.getType().isBoolean() && "Only printing booleans." );
-  Kind kind = atom.getKind(); 
-  // this is the only predicate we have
-  if (kind == kind::EQUAL) {
-    os << "(";
-    os <<"= ";
-    os << atom[0].getType() <<" "; 
-    printTerm(atom[0], os);
-    os <<" "; 
-    printTerm(atom[1], os);
-    os <<")"; 
-  } else if ( kind == kind::DISTINCT) {
-    os <<"(not (= ";
-    os << atom[0].getType() <<" "; 
-    printTerm(atom[0], os);
-    os <<" "; 
-    printTerm(atom[1], os);
-    os <<"))"; 
-  } else if ( kind == kind::OR ||
-              kind == kind::AND ||
-              kind == kind::XOR ||
-              kind == kind::IMPLIES ||
-              kind == kind::NOT) {
-    // print the boolean operators
+void LFSCTheoryProof::printTerm(Expr term, std::ostream& os) {
+  if (term.isVariable()) {
+    if(term.getType().isBoolean()) {
+      os << "(p_app " << term << ")";
+    } else {
+      os << term;
+    }
+    return;
+  }
+
+  switch(Kind k = term.getKind()) {
+  case kind::APPLY_UF: {
+    if(term.getType().isBoolean()) {
+      os << "(p_app ";
+    }
+    Expr func = term.getOperator();
+    for (unsigned i = 0; i < term.getNumChildren(); ++i) {
+      os << "(apply _ _ ";
+    }
+    os << func << " ";
+    for (unsigned i = 0; i < term.getNumChildren(); ++i) {
+      printTerm(term[i], os);
+      os << ")";
+    }
+    if(term.getType().isBoolean()) {
+      os << ")";
+    }
+    return;
+  }
+
+  case kind::ITE:
+    os << (term.getType().isBoolean() ? "(ifte " : "(ite _ ");
+    printTerm(term[0], os);
+    os << " ";
+    printTerm(term[1], os);
+    os << " ";
+    printTerm(term[2], os);
+    os << ")";
+    return;
+
+  case kind::EQUAL:
     os << "(";
-    os << toLFSCKind(kind);
-    if (atom.getNumChildren() > 2) {
+    os << "= ";
+    os << term[0].getType() << " ";
+    printTerm(term[0], os);
+    os << " ";
+    printTerm(term[1], os);
+    os << ")";
+    return;
+
+  case kind::DISTINCT:
+    os << "(not (= ";
+    os << term[0].getType() << " ";
+    printTerm(term[0], os);
+    os << " ";
+    printTerm(term[1], os);
+    os << "))";
+    return;
+
+  case kind::OR:
+  case kind::AND:
+  case kind::XOR:
+  case kind::IFF:
+  case kind::IMPLIES:
+  case kind::NOT:
+    // print the Boolean operators
+    os << "(" << toLFSCKind(k);
+    if(term.getNumChildren() > 2) {
+      // LFSC doesn't allow declarations with variable numbers of
+      // arguments, so we have to flatten these N-ary versions.
       std::ostringstream paren;
       os << " ";
-      for (unsigned i =0; i < atom.getNumChildren(); ++i) {
-        printFormula(atom[i], os);
+      for (unsigned i = 0; i < term.getNumChildren(); ++i) {
+        printTerm(term[i], os);
         os << " ";
-        if (i < atom.getNumChildren() - 2) {
-          os << "("<< toLFSCKind(kind) << " "; 
-          paren << ")"; 
+        if(i < term.getNumChildren() - 2) {
+          os << "(" << toLFSCKind(k) << " ";
+          paren << ")";
         }
       }
-      os << paren.str() <<")"; 
+      os << paren.str() << ")";
     } else {
-      // this is for binary and unary operators 
-      for (unsigned i = 0; i < atom.getNumChildren(); ++i) {
-        os <<" ";
-        printFormula(atom[i], os); 
+      // this is for binary and unary operators
+      for (unsigned i = 0; i < term.getNumChildren(); ++i) {
+        os << " ";
+        printTerm(term[i], os);
+      }
+      os << ")";
+    }
+    return;
+
+  case kind::CONST_BOOLEAN:
+    os << (term.getConst<bool>() ? "true" : "false");
+    return;
+
+  case kind::CHAIN: {
+    // LFSC doesn't allow declarations with variable numbers of
+    // arguments, so we have to flatten chained operators, like =.
+    Kind op = term.getOperator().getConst<Chain>().getOperator();
+    size_t n = term.getNumChildren();
+    std::ostringstream paren;
+    for(size_t i = 1; i < n; ++i) {
+      if(i + 1 < n) {
+        os << "(" << toLFSCKind(kind::AND) << " ";
+        paren << ")";
+      }
+      os << "(" << toLFSCKind(op) << " ";
+      printTerm(term[i - 1], os);
+      os << " ";
+      printTerm(term[i], os);
+      os << ")";
+      if(i + 1 < n) {
+        os << " ";
       }
-      os <<")"; 
     }
-  } else if (kind == kind::CONST_BOOLEAN) {
-    if (atom.getConst<bool>())
-      os << "true";
-    else
-      os << "false"; 
+    os << paren.str();
+    return;
   }
-  else {
-    std::cout << kind << "\n"; 
-    Assert (false && "Unsupported kind"); 
+
+  default:
+    Unhandled(k);
   }
+
+  Unreachable();
 }
 
 void LFSCTheoryProof::printAssertions(std::ostream& os, std::ostream& paren) {
@@ -142,56 +192,57 @@ void LFSCTheoryProof::printAssertions(std::ostream& os, std::ostream& paren) {
   ProofManager::assertions_iterator it = ProofManager::currentPM()->begin_assertions();
   ProofManager::assertions_iterator end = ProofManager::currentPM()->end_assertions();
 
-  // collect declarations first 
+  // collect declarations first
   for(; it != end; ++it) {
-    addDeclaration(*it); 
+    addDeclaration(*it);
   }
   printDeclarations(os, paren);
 
   it = ProofManager::currentPM()->begin_assertions();
   for (; it != end; ++it) {
     os << "(% A" << counter++ << " (th_holds ";
-    printFormula(*it,  os);
+    printTerm(*it,  os);
     os << ")\n";
-    paren <<")"; 
+    paren << ")";
   }
 }
 
 void LFSCTheoryProof::printDeclarations(std::ostream& os, std::ostream& paren) {
   // declaring the sorts
   for (SortSet::const_iterator it = d_sortDeclarations.begin(); it != d_sortDeclarations.end(); ++it) {
-    os << "(% " << *it << " sort \n";
-    paren << ")"; 
+    os << "(% " << *it << " sort\n";
+    paren << ")";
   }
 
   // declaring the terms
   for (ExprSet::const_iterator it = d_termDeclarations.begin(); it != d_termDeclarations.end(); ++it) {
     Expr term = *it;
 
-    os << "(% " << term << " (term "; 
-    paren <<")"; 
+    os << "(% " << term << " ";
+    os << "(term ";
 
     Type type = term.getType();
     if (type.isFunction()) {
-      std::ostringstream fparen; 
+      std::ostringstream fparen;
       FunctionType ftype = (FunctionType)type;
       std::vector<Type> args = ftype.getArgTypes();
-      args.push_back(ftype.getRangeType()); 
-      os << "(arrow "; 
+      args.push_back(ftype.getRangeType());
+      os << "(arrow";
       for (unsigned i = 0; i < args.size(); i++) {
         Type arg_type = args[i];
-        Assert (arg_type.isSort());
-        os << arg_type << " ";  
+        //Assert (arg_type.isSort() || arg_type.isBoolean());
+        os << " " << arg_type;
         if (i < args.size() - 2) {
-          os << "(arrow ";
-          fparen <<")"; 
+          os << " (arrow";
+          fparen << ")";
         }
       }
-      os << fparen.str() << "))\n"; 
+      os << fparen.str() << "))\n";
     } else {
       Assert (term.isVariable());
-      Assert (type.isSort());
+      //Assert (type.isSort() || type.isBoolean());
       os << type << ")\n";
     }
+    paren << ")";
   }
-} 
+}
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 457023a59..739299b7d 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -13,7 +13,7 @@
  **
  ** A manager for UfProofs.
  **
- ** 
+ **
  **/
 
 
@@ -24,33 +24,32 @@
 #include "util/proof.h"
 #include "expr/expr.h"
 #include <ext/hash_set>
-#include <iostream> 
+#include <iostream>
 
 namespace CVC4 {
 
-  typedef __gnu_cxx::hash_set<Type, TypeHashFunction > SortSet; 
-  typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet; 
+  typedef __gnu_cxx::hash_set<Type, TypeHashFunction > SortSet;
+  typedef __gnu_cxx::hash_set<Expr, ExprHashFunction > ExprSet;
 
   class TheoryProof {
   protected:
     ExprSet d_termDeclarations;
-    SortSet d_sortDeclarations; 
+    SortSet d_sortDeclarations;
     ExprSet d_declarationCache;
-    
-    void addDeclaration(Expr atom); 
+
   public:
     TheoryProof();
     virtual ~TheoryProof() {}
     virtual void printAssertions(std::ostream& os, std::ostream& paren) = 0;
+    void addDeclaration(Expr atom);
   };
 
   class LFSCTheoryProof: public TheoryProof {
-    static void printTerm(Expr term, std::ostream& os);
     void printDeclarations(std::ostream& os, std::ostream& paren);
   public:
-    static void printFormula(Expr atom, std::ostream& os);
+    static void printTerm(Expr term, std::ostream& os);
     virtual void printAssertions(std::ostream& os, std::ostream& paren);
-  }; 
+  };
 } /* CVC4 namespace */
 
 #endif /* __CVC4__THEORY_PROOF_H */
diff --git a/src/prop/minisat/core/Solver.cc b/src/prop/minisat/core/Solver.cc
index 16fa3ba60..610023b70 100644
--- a/src/prop/minisat/core/Solver.cc
+++ b/src/prop/minisat/core/Solver.cc
@@ -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); );
     vardata[x] = VarData(real_reason, level(x), user_level(x), intro_level(x), trail_index(x));
     clauses_removable.push(real_reason);
     attachClause(real_reason);
@@ -324,7 +324,18 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
     } else {
       // If all false, we're in conflict
       if (ps.size() == falseLiteralsCount) {
+        if(PROOF_ON()) {
+          // Take care of false units here; otherwise, we need to
+          // 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()->finalizeProof(::Minisat::CRef_Lazy); )
+            return ok = false;
+          }
+        } else {
           return ok = false;
+        }
       }
 
       CRef cr = CRef_Undef;
@@ -339,7 +350,13 @@ bool Solver::addClause_(vec<Lit>& ps, bool removable)
         clauses_persistent.push(cr);
 	attachClause(cr);
 
-        PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT); )
+        if(PROOF_ON()) {
+          PROOF( ProofManager::getSatProof()->registerClause(cr, INPUT); )
+          if(ps.size() == falseLiteralsCount) {
+            PROOF( ProofManager::getSatProof()->finalizeProof(cr); )
+            return ok = false;
+          }
+        }
       }
 
       // Check if it propagates
@@ -347,8 +364,17 @@ 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); } )
-          return ok = (propagate(CHECK_WITHOUT_THEORY) == CRef_Undef);
+          PROOF( if(ps.size() == 1) { ProofManager::getSatProof()->registerUnitClause(ps[0], INPUT); } );
+          CRef confl = propagate(CHECK_WITHOUT_THEORY);
+          if(! (ok = (confl == CRef_Undef)) ) {
+            if(ca[confl].size() == 1) {
+              PROOF( ProofManager::getSatProof()->storeUnitConflict(ca[confl][0], LEARNT); );
+              PROOF( ProofManager::getSatProof()->finalizeProof(::Minisat::CRef_Lazy); )
+            } else {
+              PROOF( ProofManager::getSatProof()->finalizeProof(confl); );
+            }
+          }
+          return ok;
         } else return ok;
       }
     }
@@ -370,7 +396,7 @@ void Solver::attachClause(CRef cr) {
 
 void Solver::detachClause(CRef cr, bool strict) {
     const Clause& c = ca[cr];
-    PROOF( ProofManager::getSatProof()->markDeleted(cr); ) 
+    PROOF( ProofManager::getSatProof()->markDeleted(cr); );
     Debug("minisat") << "Solver::detachClause(" << c << ")" << std::endl;
     assert(c.size() > 1);
 
@@ -1580,7 +1606,7 @@ CRef Solver::updateLemmas() {
       vec<Lit>& lemma = lemmas[i];
       // If it's an empty lemma, we have a conflict at zero level
       if (lemma.size() == 0) {
-        Assert (! PROOF_ON()); 
+        Assert (! PROOF_ON());
         conflict = CRef_Lazy;
         backtrackLevel = 0;
         Debug("minisat::lemmas") << "Solver::updateLemmas(): found empty clause" << std::endl;
@@ -1630,13 +1656,15 @@ 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); );
       if (removable) {
         clauses_removable.push(lemma_ref);
       } else {
         clauses_persistent.push(lemma_ref);
       }
       attachClause(lemma_ref);
+    } else {
+      PROOF( ProofManager::getSatProof()->registerUnitClause(lemma[0], THEORY_LEMMA); );
     }
 
     // If the lemma is propagating enqueue its literal (or set the conflict)
@@ -1650,7 +1678,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]); );
           }
         } else {
           Debug("minisat::lemmas") << "lemma size is " << lemma.size() << std::endl;
diff --git a/src/smt/options b/src/smt/options
index 69b5102de..b76822caf 100644
--- a/src/smt/options
+++ b/src/smt/options
@@ -22,14 +22,16 @@ option expandDefinitions expand-definitions bool :default false
  always expand symbol definitions in output
 common-option produceModels produce-models -m --produce-models bool :default false :predicate CVC4::smt::beforeSearch :predicate-include "smt/smt_engine.h"
  support the get-value and get-model commands
-option checkProofs check-proofs --check-proofs bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
- after UNSAT/VALID, machine-check the generated proof
-option checkModels check-models --check-models bool :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+option checkModels check-models --check-models bool :link --produce-models --interactive :link-smt produce-models :link-smt interactive-mode :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  after SAT/INVALID/UNKNOWN, check that the generated model satisfies user assertions
-option dumpModels --dump-models bool :default false
+option dumpModels --dump-models bool :default false :link --produce-models
  output models after every SAT/INVALID/UNKNOWN response
 option proof produce-proofs --proof bool :default false :predicate CVC4::smt::proofEnabledBuild CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
  turn on proof generation
+option checkProofs check-proofs --check-proofs bool :link --proof :link-smt produce-proofs :predicate CVC4::smt::beforeSearch :predicate-include "smt/options_handlers.h"
+ after UNSAT/VALID, machine-check the generated proof
+option dumpProofs --dump-proofs bool :default false :link --proof
+ output proofs 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)
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 1f83bb547..ec37eaf26 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -46,8 +46,10 @@
 #include "theory/theory_engine.h"
 #include "theory/bv/theory_bv_rewriter.h"
 #include "proof/proof_manager.h"
+#include "main/options.h"
 #include "util/proof.h"
 #include "proof/proof.h"
+#include "proof/proof_manager.h"
 #include "util/boolean_simplification.h"
 #include "util/node_visitor.h"
 #include "util/configuration.h"
@@ -157,6 +159,8 @@ struct SmtEngineStatistics {
   IntStat d_numAssertionsPost;
   /** time spent in checkModel() */
   TimerStat d_checkModelTime;
+  /** time spent in checkProof() */
+  TimerStat d_checkProofTime;
   /** time spent in PropEngine::checkSat() */
   TimerStat d_solveTime;
   /** time spent in pushing/popping */
@@ -183,11 +187,11 @@ struct SmtEngineStatistics {
     d_numAssertionsPre("smt::SmtEngine::numAssertionsPreITERemoval", 0),
     d_numAssertionsPost("smt::SmtEngine::numAssertionsPostITERemoval", 0),
     d_checkModelTime("smt::SmtEngine::checkModelTime"),
+    d_checkProofTime("smt::SmtEngine::checkProofTime"),
     d_solveTime("smt::SmtEngine::solveTime"),
     d_pushPopTime("smt::SmtEngine::pushPopTime"),
     d_processAssertionsTime("smt::SmtEngine::processAssertionsTime"),
     d_simplifiedToFalse("smt::SmtEngine::simplifiedToFalse", 0)
-
  {
 
     StatisticsRegistry::registerStat(&d_definitionExpansionTime);
@@ -667,6 +671,7 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_decisionEngine(NULL),
   d_theoryEngine(NULL),
   d_propEngine(NULL),
+  d_proofManager(NULL),
   d_definedFunctions(NULL),
   d_assertionList(NULL),
   d_assignments(NULL),
@@ -696,6 +701,8 @@ SmtEngine::SmtEngine(ExprManager* em) throw() :
   d_statisticsRegistry = new StatisticsRegistry();
   d_stats = new SmtEngineStatistics();
 
+  PROOF( d_proofManager = new ProofManager(); );
+
   // We have mutual dependency here, so we add the prop engine to the theory
   // engine later (it is non-essential there)
   d_theoryEngine = new TheoryEngine(d_context, d_userContext, d_private->d_iteRemover, const_cast<const LogicInfo&>(d_logic));
@@ -763,6 +770,7 @@ void SmtEngine::finishInit() {
   if(options::cumulativeMillisecondLimit() != 0) {
     setTimeLimit(options::cumulativeMillisecondLimit(), true);
   }
+
   PROOF( ProofManager::currentPM()->setLogic(d_logic.getLogicString()); ); 
 }
 
@@ -777,16 +785,11 @@ void SmtEngine::finalOptionsAreSet() {
   }
 
   if(options::checkModels()) {
-    if(! options::produceModels()) {
-      Notice() << "SmtEngine: turning on produce-models to support check-model" << endl;
-      setOption("produce-models", SExpr("true"));
-    }
     if(! options::interactive()) {
-      Notice() << "SmtEngine: turning on interactive-mode to support check-model" << endl;
+      Notice() << "SmtEngine: turning on interactive-mode to support check-models" << endl;
       setOption("interactive-mode", SExpr("true"));
     }
   }
-
   if(options::produceAssignments() && !options::produceModels()) {
     Notice() << "SmtEngine: turning on produce-models to support produce-assignments" << endl;
     setOption("produce-models", SExpr("true"));
@@ -3291,9 +3294,6 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
   finalOptionsAreSet();
   doPendingPops();
 
-
-  PROOF( ProofManager::currentPM()->addAssertion(ex); ); 
-
   Trace("smt") << "SmtEngine::checkSat(" << ex << ")" << endl;
 
   if(d_queryMade && !options::incrementalSolving()) {
@@ -3308,6 +3308,8 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
     e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
     // Ensure expr is type-checked at this point.
     ensureBoolean(e);
+    // Give it to proof manager
+    PROOF( ProofManager::currentPM()->addAssertion(e); ); 
   }
 
   // check to see if a postsolve() is pending
@@ -3361,6 +3363,7 @@ Result SmtEngine::checkSat(const Expr& ex) throw(TypeCheckingException, ModalExc
   // Check that UNSAT results generate a proof correctly.
   if(options::checkProofs()) {
     if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
+      TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime);
       checkProof();
     }
   }
@@ -3384,9 +3387,10 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
 
   // Substitute out any abstract values in ex
   Expr e = d_private->substituteAbstractValues(Node::fromExpr(ex)).toExpr();
-
   // 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()); ); 
 
   // check to see if a postsolve() is pending
   if(d_needPostsolve) {
@@ -3437,6 +3441,7 @@ Result SmtEngine::query(const Expr& ex) throw(TypeCheckingException, ModalExcept
   // Check that UNSAT results generate a proof correctly.
   if(options::checkProofs()) {
     if(r.asSatisfiabilityResult().isSat() == Result::UNSAT) {
+      TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime);
       checkProof();
     }
   }
@@ -3449,7 +3454,9 @@ Result SmtEngine::assertFormula(const Expr& ex) throw(TypeCheckingException, Log
   SmtScope smts(this);
   finalOptionsAreSet();
   doPendingPops();
-  PROOF( ProofManager::currentPM()->addAssertion(ex);); 
+
+  PROOF( ProofManager::currentPM()->addAssertion(ex); ); 
+
   Trace("smt") << "SmtEngine::assertFormula(" << ex << ")" << endl;
 
   // Substitute out any abstract values in ex
diff --git a/src/smt/smt_engine.h b/src/smt/smt_engine.h
index 0781ac1c0..8e400468c 100644
--- a/src/smt/smt_engine.h
+++ b/src/smt/smt_engine.h
@@ -56,6 +56,8 @@ class SmtEngine;
 class DecisionEngine;
 class TheoryEngine;
 
+class ProofManager;
+
 class Model;
 class StatisticsRegistry;
 
@@ -83,6 +85,7 @@ namespace smt {
   class BooleanTermConverter;
 
   void beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
+  ProofManager* currentProofManager();
 
   struct CommandCleanup;
   typedef context::CDList<Command*, CommandCleanup> CommandList;
@@ -135,8 +138,11 @@ class CVC4_PUBLIC SmtEngine {
   TheoryEngine* d_theoryEngine;
   /** The propositional engine */
   prop::PropEngine* d_propEngine;
+  /** The proof manager */
+  ProofManager* d_proofManager;
   /** An index of our defined functions */
   DefinedFunctionMap* d_definedFunctions;
+
   /**
    * The assertion list (before any conversion) for supporting
    * getAssertions().  Only maintained if in interactive mode.
@@ -327,6 +333,7 @@ class CVC4_PUBLIC SmtEngine {
   friend class ::CVC4::smt::BooleanTermConverter;
   friend ::CVC4::StatisticsRegistry* ::CVC4::stats::getStatisticsRegistry(SmtEngine*);
   friend void ::CVC4::smt::beforeSearch(std::string, bool, SmtEngine*) throw(ModalException);
+  friend ProofManager* ::CVC4::smt::currentProofManager();
   // to access d_modelCommands
   friend class ::CVC4::Model;
   friend class ::CVC4::theory::TheoryModel;
diff --git a/src/smt/smt_engine_check_proof.cpp b/src/smt/smt_engine_check_proof.cpp
index e4de1029b..a731ff024 100644
--- a/src/smt/smt_engine_check_proof.cpp
+++ b/src/smt/smt_engine_check_proof.cpp
@@ -16,16 +16,75 @@
  **/
 
 #include "smt/smt_engine.h"
+#include "util/statistics_registry.h"
 #include "check.h"
 
+#include <cstdlib>
+#include <cstring>
+#include <fstream>
+#include <string>
+#include <unistd.h>
+
 using namespace CVC4;
 using namespace std;
 
+namespace CVC4 {
+
+namespace proof {
+  extern const char *const plf_signatures;
+}/* CVC4::proof namespace */
+
+namespace smt {
+
+class UnlinkProofFile {
+  string d_filename;
+public:
+  UnlinkProofFile(const char* filename) : d_filename(filename) {}
+  ~UnlinkProofFile() { unlink(d_filename.c_str()); }
+};/* class UnlinkProofFile */
+
+}/* CVC4::smt namespace */
+
+}/* CVC4 namespace */
+
 void SmtEngine::checkProof() {
 
 #ifdef CVC4_PROOF
 
-  //TimerStat::CodeTimer checkProofTimer(d_stats->d_checkProofTime);
+  Chat() << "generating proof..." << endl;
+
+  Proof* pf = getProof();
+
+  Chat() << "checking proof..." << endl;
+
+  if(!d_logic.isPure(theory::THEORY_BOOL) &&
+     !d_logic.isPure(theory::THEORY_UF)) {
+    // no checking for these yet
+    Notice() << "Notice: no proof-checking for non-UF proofs yet" << endl;
+    return;
+  }
+
+  char* pfFile = strdup("/tmp/cvc4_proof.XXXXXX");
+  int fd = mkstemp(pfFile);
+
+  // ensure this temp file is removed after
+  smt::UnlinkProofFile unlinker(pfFile);
+
+  ofstream pfStream(pfFile);
+  pfStream << proof::plf_signatures << endl;
+  pf->toStream(pfStream);
+  pfStream.close();
+  args a;
+  a.show_runs = false;
+  a.no_tail_calls = false;
+  a.compile_scc = false;
+  a.compile_scc_debug = false;
+  a.run_scc = false;
+  a.use_nested_app = false;
+  a.compile_lib = false;
+  init();
+  check_file(pfFile, args());
+  close(fd);
 
 #else /* CVC4_PROOF */
 
diff --git a/src/smt/smt_engine_scope.h b/src/smt/smt_engine_scope.h
index 21644d3f4..2389181b5 100644
--- a/src/smt/smt_engine_scope.h
+++ b/src/smt/smt_engine_scope.h
@@ -22,10 +22,14 @@
 #include "util/cvc4_assert.h"
 #include "expr/node_manager.h"
 #include "util/output.h"
+#include "proof/proof.h"
 
 #pragma once
 
 namespace CVC4 {
+
+class ProofManager;
+
 namespace smt {
 
 extern CVC4_THREADLOCAL(SmtEngine*) s_smtEngine_current;
@@ -35,6 +39,12 @@ inline SmtEngine* currentSmtEngine() {
   return s_smtEngine_current;
 }
 
+inline ProofManager* currentProofManager() {
+  Assert(PROOF_ON());
+  Assert(s_smtEngine_current != NULL);
+  return s_smtEngine_current->d_proofManager;
+}
+
 class SmtScope : public NodeManagerScope {
   /** The old NodeManager, to be restored on destruction. */
   SmtEngine* d_oldSmtEngine;
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 7cf4d7ad9..c598fd01b 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -146,6 +146,7 @@ TheoryEngine::TheoryEngine(context::Context* context,
   StatisticsRegistry::registerStat(&d_combineTheoriesTime);
   d_true = NodeManager::currentNM()->mkConst<bool>(true);
   d_false = NodeManager::currentNM()->mkConst<bool>(false);
+
   PROOF (ProofManager::currentPM()->initTheoryProof(); );
 
   d_iteUtilities = new ITEUtilities(d_iteRemover.getContainsVisitor());