mergecav2019strings_countRewRed

46 files changed, 1069 insertions, 204 deletions

diff --git a/src/proof/arith_proof.cpp b/src/proof/arith_proof.cpp
index 0d2bb5be0..8b55c29db 100644
--- a/src/proof/arith_proof.cpp
+++ b/src/proof/arith_proof.cpp
@@ -2,9 +2,9 @@
 /*! \file arith_proof.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Guy Katz, Tim King, Andrew Reynolds
+ **   Alex Ozdemir, Guy Katz, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/proof/arith_proof.h b/src/proof/arith_proof.h
index 640d2db8d..a1df24fac 100644
--- a/src/proof/arith_proof.h
+++ b/src/proof/arith_proof.h
@@ -2,9 +2,9 @@
 /*! \file arith_proof.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Guy Katz, Mathias Preiner, Tim King
+ **   Alex Ozdemir, Guy Katz, Mathias Preiner
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__ARITH__PROOF_H
-#define __CVC4__ARITH__PROOF_H
+#ifndef CVC4__ARITH__PROOF_H
+#define CVC4__ARITH__PROOF_H
 
 #include <memory>
 #include <unordered_set>
@@ -172,4 +172,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__ARITH__PROOF_H */
+#endif /* CVC4__ARITH__PROOF_H */
diff --git a/src/proof/arith_proof_recorder.cpp b/src/proof/arith_proof_recorder.cpp
index 097fdb51e..c240f9582 100644
--- a/src/proof/arith_proof_recorder.cpp
+++ b/src/proof/arith_proof_recorder.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Alex Ozdemir
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/proof/arith_proof_recorder.h b/src/proof/arith_proof_recorder.h
index 2d0501332..3fff6968d 100644
--- a/src/proof/arith_proof_recorder.h
+++ b/src/proof/arith_proof_recorder.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Alex Ozdemir
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -42,8 +42,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF__ARITH_PROOF_RECORDER_H
-#define __CVC4__PROOF__ARITH_PROOF_RECORDER_H
+#ifndef CVC4__PROOF__ARITH_PROOF_RECORDER_H
+#define CVC4__PROOF__ARITH_PROOF_RECORDER_H
 
 #include <map>
 #include <set>
diff --git a/src/proof/array_proof.cpp b/src/proof/array_proof.cpp
index c22f36413..131fcd3b6 100644
--- a/src/proof/array_proof.cpp
+++ b/src/proof/array_proof.cpp
@@ -2,9 +2,9 @@
 /*! \file array_proof.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Guy Katz, Yoni Zohar, Tim King
+ **   Guy Katz, Yoni Zohar, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/proof/array_proof.h b/src/proof/array_proof.h
index 53b825522..372ad1f67 100644
--- a/src/proof/array_proof.h
+++ b/src/proof/array_proof.h
@@ -2,9 +2,9 @@
 /*! \file array_proof.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Guy Katz, Tim King
+ **   Tim King, Mathias Preiner, Guy Katz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__ARRAY__PROOF_H
-#define __CVC4__ARRAY__PROOF_H
+#ifndef CVC4__ARRAY__PROOF_H
+#define CVC4__ARRAY__PROOF_H
 
 #include <memory>
 #include <unordered_set>
@@ -117,4 +117,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__ARRAY__PROOF_H */
+#endif /* CVC4__ARRAY__PROOF_H */
diff --git a/src/proof/bitvector_proof.cpp b/src/proof/bitvector_proof.cpp
index 90c0c9b30..18e46a292 100644
--- a/src/proof/bitvector_proof.cpp
+++ b/src/proof/bitvector_proof.cpp
@@ -2,9 +2,9 @@
 /*! \file bitvector_proof.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Guy Katz, Paul Meng
+ **   Liana Hadarean, Guy Katz, Alex Ozdemir
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -221,6 +221,14 @@ void BitVectorProof::printOwnedTerm(Expr term,
   }
 }
 
+void BitVectorProof::printEmptyClauseProof(std::ostream& os,
+                                           std::ostream& paren)
+{
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
+         "the BV theory should only be proving bottom directly in the eager "
+         "bitblasting mode");
+}
+
 void BitVectorProof::printBitOf(Expr term,
                                 std::ostream& os,
                                 const ProofLetMap& map)
diff --git a/src/proof/bitvector_proof.h b/src/proof/bitvector_proof.h
index 4b897a6c6..f0a0717fa 100644
--- a/src/proof/bitvector_proof.h
+++ b/src/proof/bitvector_proof.h
@@ -2,9 +2,9 @@
 /*! \file bitvector_proof.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Mathias Preiner, Guy Katz
+ **   Alex Ozdemir, Mathias Preiner, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__BITVECTOR_PROOF_H
-#define __CVC4__BITVECTOR_PROOF_H
+#ifndef CVC4__BITVECTOR_PROOF_H
+#define CVC4__BITVECTOR_PROOF_H
 
 #include <set>
 #include <unordered_map>
@@ -167,7 +167,7 @@ class BitVectorProof : public TheoryProof
    * @param os the stream to print to
    * @param paren any parentheses to add to the end of the global proof
    */
-  virtual void printEmptyClauseProof(std::ostream& os, std::ostream& paren) = 0;
+  virtual void printEmptyClauseProof(std::ostream& os, std::ostream& paren);
 
   /**
    * Read the d_atomsInBitblastingProof member.
@@ -276,4 +276,4 @@ class BitVectorProof : public TheoryProof
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__BITVECTOR__PROOF_H */
+#endif /* CVC4__BITVECTOR__PROOF_H */
diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp
index bb875d1d8..eed295b1a 100644
--- a/src/proof/clausal_bitvector_proof.cpp
+++ b/src/proof/clausal_bitvector_proof.cpp
@@ -19,10 +19,13 @@
 #include <algorithm>
 #include <iterator>
 #include <set>
+
 #include "options/bv_options.h"
 #include "proof/clausal_bitvector_proof.h"
 #include "proof/drat/drat_proof.h"
+#include "proof/er/er_proof.h"
 #include "proof/lfsc_proof_printer.h"
+#include "proof/lrat/lrat_proof.h"
 #include "theory/bv/theory_bv.h"
 
 namespace CVC4 {
@@ -66,12 +69,12 @@ void ClausalBitVectorProof::initCnfProof(prop::CnfStream* cnfStream,
 void ClausalBitVectorProof::registerUsedClause(ClauseId id,
                                                prop::SatClause& clause)
 {
-  d_usedClauses.emplace_back(
-      id, std::unique_ptr<prop::SatClause>(new prop::SatClause(clause)));
+  d_usedClauses.emplace_back(id, clause);
 };
 
 void ClausalBitVectorProof::calculateAtomsInBitblastingProof()
 {
+  // Debug dump of DRAT Proof
   if (Debug.isOn("bv::clausal"))
   {
     std::string serializedDratProof = d_binaryDratProof.str();
@@ -84,7 +87,16 @@ void ClausalBitVectorProof::calculateAtomsInBitblastingProof()
     Debug("bv::clausal") << "Printing DRAT proof ... " << std::endl;
     dratProof.outputAsText(Debug("bv::clausal"));
   }
-  Unimplemented();
+
+  // Empty any old record of which atoms were used
+  d_atomsInBitblastingProof.clear();
+
+  // For each used clause, ask the CNF proof which atoms are used in it
+  for (const auto& usedIndexAndClause : d_usedClauses)
+  {
+    d_cnfProof->collectAtoms(&usedIndexAndClause.second,
+                             d_atomsInBitblastingProof);
+  }
 }
 
 void LfscClausalBitVectorProof::printTheoryLemmaProof(std::vector<Expr>& lemma,
@@ -101,13 +113,91 @@ void LfscClausalBitVectorProof::printBBDeclarationAndCnf(std::ostream& os,
                                                          std::ostream& paren,
                                                          ProofLetMap& letMap)
 {
-  Unimplemented();
+  os << "\n;; Bitblasting mappings\n";
+  printBitblasting(os, paren);
+
+  os << "\n;; BB-CNF mappings\n";
+  d_cnfProof->printAtomMapping(d_atomsInBitblastingProof, os, paren, letMap);
+
+  os << "\n;; BB-CNF proofs\n";
+  for (const auto& idAndClause : d_usedClauses)
+  {
+    d_cnfProof->printCnfProofForClause(
+        idAndClause.first, &idAndClause.second, os, paren);
+  }
 }
 
-void LfscClausalBitVectorProof::printEmptyClauseProof(std::ostream& os,
-                                                      std::ostream& paren)
+void LfscDratBitVectorProof::printEmptyClauseProof(std::ostream& os,
+                                                   std::ostream& paren)
 {
-  Unimplemented();
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
+         "the BV theory should only be proving bottom directly in the eager "
+         "bitblasting mode");
+
+  os << "\n;; Proof of input to SAT solver\n";
+  os << "(@ proofOfSatInput ";
+  paren << ")";
+  std::vector<ClauseId> usedIds;
+  usedIds.reserve(d_usedClauses.size());
+  for (const auto& idAnd : d_usedClauses)
+  {
+    usedIds.push_back(idAnd.first);
+  };
+  LFSCProofPrinter::printSatInputProof(usedIds, os, "bb");
+
+  os << "\n;; DRAT Proof Value\n";
+  os << "(@ dratProof ";
+  paren << ")";
+  drat::DratProof::fromBinary(d_binaryDratProof.str()).outputAsLfsc(os, 2);
+  os << "\n";
+
+  os << "\n;; Verification of DRAT Proof\n";
+  os << "(drat_proof_of_bottom _ proofOfSatInput dratProof "
+     << "\n)";
+}
+
+void LfscLratBitVectorProof::printEmptyClauseProof(std::ostream& os,
+                                                   std::ostream& paren)
+{
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
+         "the BV theory should only be proving bottom directly in the eager "
+         "bitblasting mode");
+
+  os << "\n;; Proof of input to SAT solver\n";
+  os << "(@ proofOfCMap ";
+  paren << ")";
+  std::vector<ClauseId> usedIds;
+  usedIds.reserve(d_usedClauses.size());
+  for (const auto& idAnd : d_usedClauses)
+  {
+    usedIds.push_back(idAnd.first);
+  };
+  LFSCProofPrinter::printCMapProof(usedIds, os, "bb");
+
+  os << "\n;; DRAT Proof Value\n";
+  os << "(@ lratProof ";
+  paren << ")";
+  lrat::LratProof pf =
+      lrat::LratProof::fromDratProof(d_usedClauses, d_binaryDratProof.str());
+  pf.outputAsLfsc(os);
+  os << "\n";
+
+  os << "\n;; Verification of DRAT Proof\n";
+  os << "(lrat_proof_of_bottom _ proofOfCMap lratProof "
+     << "\n)";
+}
+
+void LfscErBitVectorProof::printEmptyClauseProof(std::ostream& os,
+                                                 std::ostream& paren)
+{
+  Assert(options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER,
+         "the BV theory should only be proving bottom directly in the eager "
+         "bitblasting mode");
+
+  er::ErProof pf =
+      er::ErProof::fromBinaryDratProof(d_usedClauses, d_binaryDratProof.str());
+
+  pf.outputAsLfsc(os);
 }
 
 }  // namespace proof
diff --git a/src/proof/clausal_bitvector_proof.h b/src/proof/clausal_bitvector_proof.h
index 85e409e0d..b10b1ad1c 100644
--- a/src/proof/clausal_bitvector_proof.h
+++ b/src/proof/clausal_bitvector_proof.h
@@ -2,7 +2,7 @@
 /*! \file clausal_bitvector_proof.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Alex Ozdemir
+ **   Alex Ozdemir, Mathias Preiner
  ** This file is part of the CVC4 project.
  ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
@@ -18,8 +18,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
-#define __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
+#ifndef CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
+#define CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H
 
 #include <iostream>
 #include <sstream>
@@ -61,8 +61,7 @@ class ClausalBitVectorProof : public BitVectorProof
 
  protected:
   // A list of all clauses and their ids which are passed into the SAT solver
-  std::vector<std::pair<ClauseId, std::unique_ptr<prop::SatClause>>>
-      d_usedClauses;
+  std::vector<std::pair<ClauseId, prop::SatClause>> d_usedClauses;
   // Stores the proof recieved from the SAT solver.
   std::ostringstream d_binaryDratProof;
 };
@@ -77,7 +76,6 @@ class LfscClausalBitVectorProof : public ClausalBitVectorProof
                             TheoryProofEngine* proofEngine)
       : ClausalBitVectorProof(bv, proofEngine)
   {
-    // That's all!
   }
 
   void printTheoryLemmaProof(std::vector<Expr>& lemma,
@@ -87,6 +85,49 @@ class LfscClausalBitVectorProof : public ClausalBitVectorProof
   void printBBDeclarationAndCnf(std::ostream& os,
                                 std::ostream& paren,
                                 ProofLetMap& letMap) override;
+};
+
+/**
+ * A DRAT proof for a bit-vector problem
+ */
+class LfscDratBitVectorProof : public LfscClausalBitVectorProof
+{
+ public:
+  LfscDratBitVectorProof(theory::bv::TheoryBV* bv,
+                         TheoryProofEngine* proofEngine)
+      : LfscClausalBitVectorProof(bv, proofEngine)
+  {
+  }
+
+  void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
+};
+
+/**
+ * An LRAT proof for a bit-vector problem
+ */
+class LfscLratBitVectorProof : public LfscClausalBitVectorProof
+{
+ public:
+  LfscLratBitVectorProof(theory::bv::TheoryBV* bv,
+                         TheoryProofEngine* proofEngine)
+      : LfscClausalBitVectorProof(bv, proofEngine)
+  {
+  }
+
+  void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
+};
+
+/**
+ * An Extended Resolution proof for a bit-vector problem
+ */
+class LfscErBitVectorProof : public LfscClausalBitVectorProof
+{
+ public:
+  LfscErBitVectorProof(theory::bv::TheoryBV* bv, TheoryProofEngine* proofEngine)
+      : LfscClausalBitVectorProof(bv, proofEngine)
+  {
+  }
+
   void printEmptyClauseProof(std::ostream& os, std::ostream& paren) override;
 };
 
@@ -94,4 +135,4 @@ class LfscClausalBitVectorProof : public ClausalBitVectorProof
 
 }  // namespace CVC4
 
-#endif /* __CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H */
+#endif /* CVC4__PROOF__CLAUSAL_BITVECTOR_PROOF_H */
diff --git a/src/proof/clause_id.h b/src/proof/clause_id.h
index 384bc560c..4a9ebc74a 100644
--- a/src/proof/clause_id.h
+++ b/src/proof/clause_id.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Paul Meng
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF__CLAUSE_ID_H
-#define __CVC4__PROOF__CLAUSE_ID_H
+#ifndef CVC4__PROOF__CLAUSE_ID_H
+#define CVC4__PROOF__CLAUSE_ID_H
 
 namespace CVC4 {
 
@@ -30,4 +30,4 @@ typedef unsigned ClauseId;
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__PROOF__CLAUSE_ID_H */
+#endif /* CVC4__PROOF__CLAUSE_ID_H */
diff --git a/src/proof/cnf_proof.cpp b/src/proof/cnf_proof.cpp
index 4e8d20162..9c263e08f 100644
--- a/src/proof/cnf_proof.cpp
+++ b/src/proof/cnf_proof.cpp
@@ -2,9 +2,9 @@
 /*! \file cnf_proof.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Andrew Reynolds, Guy Katz
+ **   Liana Hadarean, Andrew Reynolds, Alex Ozdemir
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -349,6 +349,39 @@ void CnfProof::collectAssertionsForClauses(const IdToSatClause& clauses,
   }
 }
 
+// Detects whether a clause has x v ~x for some x
+// If so, returns the positive occurence's idx first, then the negative's
+Maybe<std::pair<size_t, size_t>> CnfProof::detectTrivialTautology(
+    const prop::SatClause& clause)
+{
+  // a map from a SatVariable to its previous occurence's polarity and location
+  std::map<prop::SatVariable, std::pair<bool, size_t>> varsToPolsAndIndices;
+  for (size_t i = 0; i < clause.size(); ++i)
+  {
+    prop::SatLiteral lit = clause[i];
+    prop::SatVariable var = lit.getSatVariable();
+    bool polarity = !lit.isNegated();
+
+    // Check if this var has already occured w/ opposite polarity
+    auto iter = varsToPolsAndIndices.find(var);
+    if (iter != varsToPolsAndIndices.end() && iter->second.first != polarity)
+    {
+      if (iter->second.first)
+      {
+        return Maybe<std::pair<size_t, size_t>>{
+            std::make_pair(iter->second.second, i)};
+      }
+      else
+      {
+        return Maybe<std::pair<size_t, size_t>>{
+            std::make_pair(i, iter->second.second)};
+      }
+    }
+    varsToPolsAndIndices[var] = std::make_pair(polarity, i);
+  }
+  return Maybe<std::pair<size_t, size_t>>{};
+}
+
 void LFSCCnfProof::printAtomMapping(const std::set<Node>& atoms,
                                     std::ostream& os,
                                     std::ostream& paren) {
@@ -431,61 +464,98 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
 
   Assert( clause->size()>0 );
 
-  Node base_assertion = getDefinitionForClause(id);
-
-  //get the assertion for the clause id
-  std::map<Node, unsigned > childIndex;
-  std::map<Node, bool > childPol;
-  Node assertion = clauseToNode( *clause, childIndex, childPol );
-  //if there is no reason, construct assertion directly.   This can happen for unit clauses.
-  if( base_assertion.isNull() ){
-    base_assertion = assertion;
+  // If the clause contains x v ~x, it's easy!
+  //
+  // It's important to check for this case, because our other logic for
+  // recording the location of variables in the clause assumes the clause is
+  // not tautological
+  Maybe<std::pair<size_t, size_t>> isTrivialTaut =
+      detectTrivialTautology(*clause);
+  if (isTrivialTaut.just())
+  {
+    size_t posIndexInClause = isTrivialTaut.value().first;
+    size_t negIndexInClause = isTrivialTaut.value().second;
+    Trace("cnf-pf") << "; Indices " << posIndexInClause << " (+) and "
+                    << negIndexInClause << " (-) make this clause a tautology"
+                    << std::endl;
+
+    std::string proofOfPos =
+        ProofManager::getLitName((*clause)[negIndexInClause], d_name);
+    std::string proofOfNeg =
+        ProofManager::getLitName((*clause)[posIndexInClause], d_name);
+    os << "(contra _ " << proofOfPos << " " << proofOfNeg << ")";
   }
-  //os_base is proof of base_assertion
-  std::stringstream os_base;
-
-  // checks if tautological definitional clause or top-level clause
-  // and prints the proof of the top-level formula
-  bool is_input = printProofTopLevel(base_assertion, os_base);
+  else
+  {
+    Node base_assertion = getDefinitionForClause(id);
+
+    // get the assertion for the clause id
+    std::map<Node, unsigned> childIndex;
+    std::map<Node, bool> childPol;
+    Node assertion = clauseToNode(*clause, childIndex, childPol);
+    // if there is no reason, construct assertion directly.   This can happen
+    // for unit clauses.
+    if (base_assertion.isNull())
+    {
+      base_assertion = assertion;
+    }
+    // os_base is proof of base_assertion
+    std::stringstream os_base;
+
+    // checks if tautological definitional clause or top-level clause
+    // and prints the proof of the top-level formula
+    bool is_input = printProofTopLevel(base_assertion, os_base);
+
+    if (is_input)
+    {
+      Debug("cnf-pf") << std::endl
+                      << "; base assertion is input. proof: " << os_base.str()
+                      << std::endl;
+    }
 
-  if (is_input) {
-    Debug("cnf-pf") << std::endl << "; base assertion is input. proof: " << os_base.str() << std::endl;
-  }
+    // get base assertion with polarity
+    bool base_pol = base_assertion.getKind() != kind::NOT;
+    base_assertion = base_assertion.getKind() == kind::NOT ? base_assertion[0]
+                                                           : base_assertion;
 
-  //get base assertion with polarity
-  bool base_pol = base_assertion.getKind()!=kind::NOT;
-  base_assertion = base_assertion.getKind()==kind::NOT ? base_assertion[0] : base_assertion;
-
-  std::map< Node, unsigned >::iterator itci = childIndex.find( base_assertion );
-  bool is_in_clause = itci!=childIndex.end();
-  unsigned base_index = is_in_clause ? itci->second : 0;
-  Trace("cnf-pf") << std::endl;
-  Trace("cnf-pf") << "; input = " << is_input << ", is_in_clause = " << is_in_clause << ", id = " << id << ", assertion = " << assertion << ", base assertion = " << base_assertion << std::endl;
-  if (!is_input){
-    Assert(is_in_clause);
-    prop::SatLiteral blit = (*clause)[ base_index ];
-    os_base << ProofManager::getLitName(blit, d_name);
-    base_pol = !childPol[base_assertion]; // WHY? if the case is =>
-  }
-  Trace("cnf-pf") << "; polarity of base assertion = " << base_pol << std::endl;
-  Trace("cnf-pf") << "; proof of base : " << os_base.str() << std::endl;
-
-  bool success = false;
-  if( is_input &&
-      is_in_clause &&
-      childPol[base_assertion]==base_pol ){
-    //if both in input and in clause, the proof is trivial.  this is the case for unit clauses.
-    Trace("cnf-pf") << "; trivial" << std::endl;
-    os << "(contra _ ";
-    success = true;
-    prop::SatLiteral lit = (*clause)[itci->second];
-    if( base_pol ){
-      os << os_base.str() << " " << ProofManager::getLitName(lit, d_name);
-    }else{
-      os << ProofManager::getLitName(lit, d_name) << " " << os_base.str();
+    std::map<Node, unsigned>::iterator itci = childIndex.find(base_assertion);
+    bool is_in_clause = itci != childIndex.end();
+    unsigned base_index = is_in_clause ? itci->second : 0;
+    Trace("cnf-pf") << std::endl;
+    Trace("cnf-pf") << "; input = " << is_input
+                    << ", is_in_clause = " << is_in_clause << ", id = " << id
+                    << ", assertion = " << assertion
+                    << ", base assertion = " << base_assertion << std::endl;
+    if (!is_input)
+    {
+      Assert(is_in_clause);
+      prop::SatLiteral blit = (*clause)[base_index];
+      os_base << ProofManager::getLitName(blit, d_name);
+      base_pol = !childPol[base_assertion];  // WHY? if the case is =>
     }
-    os << ")";
-  } else if ((base_assertion.getKind()==kind::AND && !base_pol) ||
+    Trace("cnf-pf") << "; polarity of base assertion = " << base_pol
+                    << std::endl;
+    Trace("cnf-pf") << "; proof of base : " << os_base.str() << std::endl;
+
+    bool success = false;
+    if (is_input && is_in_clause && childPol[base_assertion] == base_pol)
+    {
+      // if both in input and in clause, the proof is trivial.  this is the case
+      // for unit clauses.
+      Trace("cnf-pf") << "; trivial" << std::endl;
+      os << "(contra _ ";
+      success = true;
+      prop::SatLiteral lit = (*clause)[itci->second];
+      if (base_pol)
+      {
+        os << os_base.str() << " " << ProofManager::getLitName(lit, d_name);
+      }
+      else
+      {
+        os << ProofManager::getLitName(lit, d_name) << " " << os_base.str();
+      }
+      os << ")";
+    } else if ((base_assertion.getKind()==kind::AND && !base_pol) ||
            ((base_assertion.getKind()==kind::OR ||
              base_assertion.getKind()==kind::IMPLIES) && base_pol)) {
     Trace("cnf-pf") << "; and/or case 1" << std::endl;
@@ -776,6 +846,7 @@ void LFSCCnfProof::printCnfProofForClause(ClauseId id,
     Trace("cnf-pf") << std::endl;
     os << "trust-bad";
   }
+  }
 
   os << ")" << clause_paren.str()
      << " (\\ " << ProofManager::getInputClauseName(id, d_name) << "\n";
diff --git a/src/proof/cnf_proof.h b/src/proof/cnf_proof.h
index 78ddeebd0..e589950bc 100644
--- a/src/proof/cnf_proof.h
+++ b/src/proof/cnf_proof.h
@@ -2,9 +2,9 @@
 /*! \file cnf_proof.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Guy Katz, Tim King
+ **   Liana Hadarean, Guy Katz, Alex Ozdemir
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -18,8 +18,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__CNF_PROOF_H
-#define __CVC4__CNF_PROOF_H
+#ifndef CVC4__CNF_PROOF_H
+#define CVC4__CNF_PROOF_H
 
 #include <iosfwd>
 #include <unordered_map>
@@ -29,6 +29,7 @@
 #include "proof/clause_id.h"
 #include "proof/lemma_proof.h"
 #include "proof/sat_proof.h"
+#include "util/maybe.h"
 #include "util/proof.h"
 
 namespace CVC4 {
@@ -164,6 +165,10 @@ public:
                            std::ostream& paren,
                            ProofLetMap &letMap) = 0;
 
+  // Detects whether a clause has x v ~x for some x
+  // If so, returns the positive occurence's idx first, then the negative's
+  static Maybe<std::pair<size_t, size_t>> detectTrivialTautology(
+      const prop::SatClause& clause);
   virtual void printClause(const prop::SatClause& clause,
                            std::ostream& os,
                            std::ostream& paren) = 0;
@@ -207,4 +212,4 @@ public:
 
 } /* CVC4 namespace */
 
-#endif /* __CVC4__CNF_PROOF_H */
+#endif /* CVC4__CNF_PROOF_H */
diff --git a/src/proof/dimacs_printer.cpp b/src/proof/dimacs_printer.cpp
index 48199066e..04f880e11 100644
--- a/src/proof/dimacs_printer.cpp
+++ b/src/proof/dimacs_printer.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Alex Ozdemir
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/proof/dimacs_printer.h b/src/proof/dimacs_printer.h
index d11adea3f..2ae4abefa 100644
--- a/src/proof/dimacs_printer.h
+++ b/src/proof/dimacs_printer.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Alex Ozdemir
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF__DIMACS_PRINTER_H
-#define __CVC4__PROOF__DIMACS_PRINTER_H
+#ifndef CVC4__PROOF__DIMACS_PRINTER_H
+#define CVC4__PROOF__DIMACS_PRINTER_H
 
 #include <iosfwd>
 #include <memory>
@@ -63,4 +63,4 @@ void printDimacs(
 }  // namespace proof
 }  // namespace CVC4
 
-#endif  // __CVC4__PROOF__DIMACS_PRINTER_H
+#endif  // CVC4__PROOF__DIMACS_PRINTER_H
diff --git a/src/proof/drat/drat_proof.cpp b/src/proof/drat/drat_proof.cpp
index c2f2fa49e..5a01ffdfd 100644
--- a/src/proof/drat/drat_proof.cpp
+++ b/src/proof/drat/drat_proof.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Alex Ozdemir
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -259,12 +259,12 @@ void DratProof::outputAsLfsc(std::ostream& os, uint8_t indentation) const
     {
       case ADDITION:
       {
-        os << "DRATProofa";
+        os << "DRATProofa ";
         break;
       }
       case DELETION:
       {
-        os << "DRATProofd";
+        os << "DRATProofd ";
         break;
       }
       default: { Unreachable("Unrecognized DRAT instruction kind");
@@ -273,7 +273,7 @@ void DratProof::outputAsLfsc(std::ostream& os, uint8_t indentation) const
     for (const SatLiteral& l : i.d_clause)
     {
       os << "(clc (" << (l.isNegated() ? "neg " : "pos ")
-         << ProofManager::getVarName(l.getSatVariable()) << ") ";
+         << ProofManager::getVarName(l.getSatVariable(), "bb") << ") ";
     }
     os << "cln";
     std::fill_n(std::ostream_iterator<char>(os), i.d_clause.size(), ')');
diff --git a/src/proof/drat/drat_proof.h b/src/proof/drat/drat_proof.h
index 4715b38f4..082107d0a 100644
--- a/src/proof/drat/drat_proof.h
+++ b/src/proof/drat/drat_proof.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Alex Ozdemir
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -19,8 +19,8 @@
  **
  **/
 
-#ifndef __CVC4__PROOF__DRAT__DRAT_PROOF_H
-#define __CVC4__PROOF__DRAT__DRAT_PROOF_H
+#ifndef CVC4__PROOF__DRAT__DRAT_PROOF_H
+#define CVC4__PROOF__DRAT__DRAT_PROOF_H
 
 #include "cvc4_private.h"
 #include "prop/sat_solver.h"
@@ -137,4 +137,4 @@ class DratProof
 }  // namespace proof
 }  // namespace CVC4
 
-#endif  // __CVC4__PROOF__DRAT__DRAT_PROOF_H
+#endif  // CVC4__PROOF__DRAT__DRAT_PROOF_H
diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp
new file mode 100644
index 000000000..22903c3c9
--- /dev/null
+++ b/src/proof/er/er_proof.cpp
@@ -0,0 +1,391 @@
+/*********************                                                        */
+/*! \file er_proof.cpp
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief ER Proof Format
+ **
+ ** Declares C++ types that represent an ER/TRACECHECK proof.
+ ** Defines serialization for these types.
+ **
+ ** You can find details about the way ER is encoded in the TRACECHECK
+ ** format at these locations:
+ **    https://github.com/benjaminkiesl/drat2er
+ **    http://www.cs.utexas.edu/users/marijn/publications/ijcar18.pdf
+ **/
+
+#include "proof/er/er_proof.h"
+
+#include <unistd.h>
+#include <algorithm>
+#include <fstream>
+#include <iostream>
+#include <iterator>
+#include <unordered_set>
+
+#include "base/cvc4_assert.h"
+#include "base/map_util.h"
+#include "proof/dimacs_printer.h"
+#include "proof/lfsc_proof_printer.h"
+#include "proof/proof_manager.h"
+
+#if CVC4_USE_DRAT2ER
+#include "drat2er.h"
+#include "drat2er_options.h"
+#endif
+
+namespace CVC4 {
+namespace proof {
+namespace er {
+
+TraceCheckProof TraceCheckProof::fromText(std::istream& in)
+{
+  TraceCheckProof pf;
+  TraceCheckIdx idx = 0;
+  int64_t token = 0;
+
+  // For each line of the proof, start with the idx
+  // If there is no idx, then you're done!
+  in >> idx;
+  for (; !in.eof(); in >> idx)
+  {
+    Assert(in.good());
+
+    // Then parse the clause (it's 0-terminated)
+    std::vector<prop::SatLiteral> clause;
+    in >> token;
+    for (; token != 0; in >> token)
+    {
+      clause.emplace_back(std::abs(token) - 1, token < 0);
+    }
+
+    // Then parse the chain of literals (it's also 0-terminated)
+    std::vector<TraceCheckIdx> chain;
+    in >> token;
+    for (; token != 0; in >> token)
+    {
+      Assert(token > 0);
+      chain.push_back(token);
+    }
+
+    // Add the line to the proof
+    pf.d_lines.emplace_back(idx, std::move(clause), std::move(chain));
+  }
+  return pf;
+}
+
+ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
+                                     const std::string& dratBinary)
+{
+  std::ostringstream cmd;
+  char formulaFilename[] = "/tmp/cvc4-dimacs-XXXXXX";
+  char dratFilename[] = "/tmp/cvc4-drat-XXXXXX";
+  char tracecheckFilename[] = "/tmp/cvc4-tracecheck-er-XXXXXX";
+
+  int r;
+  r = mkstemp(formulaFilename);
+  AlwaysAssert(r > 0);
+  close(r);
+  r = mkstemp(dratFilename);
+  AlwaysAssert(r > 0);
+  close(r);
+  r = mkstemp(tracecheckFilename);
+  AlwaysAssert(r > 0);
+  close(r);
+
+  // Write the formula
+  std::ofstream formStream(formulaFilename);
+  printDimacs(formStream, usedClauses);
+  formStream.close();
+
+  // Write the (binary) DRAT proof
+  std::ofstream dratStream(dratFilename);
+  dratStream << dratBinary;
+  dratStream.close();
+
+  // Invoke drat2er
+#if CVC4_USE_DRAT2ER
+  drat2er::TransformDRATToExtendedResolution(formulaFilename,
+                                             dratFilename,
+                                             tracecheckFilename,
+                                             false,
+                                             drat2er::options::QUIET,
+                                             false);
+
+#else
+  Unimplemented(
+      "ER proof production requires drat2er.\n"
+      "Run contrib/get-drat2er, reconfigure with --drat2er, and rebuild");
+#endif
+
+  // Parse the resulting TRACECHECK proof into an ER proof.
+  std::ifstream tracecheckStream(tracecheckFilename);
+  ErProof proof(usedClauses, TraceCheckProof::fromText(tracecheckStream));
+  tracecheckStream.close();
+
+  remove(formulaFilename);
+  remove(dratFilename);
+  remove(tracecheckFilename);
+
+  return proof;
+}
+
+ErProof::ErProof(const ClauseUseRecord& usedClauses,
+                 TraceCheckProof&& tracecheck)
+    : d_inputClauseIds(), d_definitions(), d_tracecheck(tracecheck)
+{
+  // Step zero, save input clause Ids for future printing
+  std::transform(usedClauses.begin(),
+                 usedClauses.end(),
+                 std::back_inserter(d_inputClauseIds),
+                 [](const std::pair<ClauseId, prop::SatClause>& pair) {
+                   return pair.first;
+                 });
+
+  // Step one, verify the formula starts the proof
+  if (Configuration::isAssertionBuild())
+  {
+    for (size_t i = 0, n = usedClauses.size(); i < n; ++i)
+    {
+      Assert(d_tracecheck.d_lines[i].d_idx = i + 1);
+      Assert(d_tracecheck.d_lines[i].d_chain.size() == 0);
+      std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>
+          traceCheckClause{d_tracecheck.d_lines[i].d_clause.begin(),
+                           d_tracecheck.d_lines[i].d_clause.end()};
+      std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>
+          originalClause{usedClauses[i].second.begin(),
+                         usedClauses[i].second.end()};
+      Assert(traceCheckClause == originalClause);
+      Assert(d_tracecheck.d_lines[i].d_idx = i + 1);
+      Assert(d_tracecheck.d_lines[i].d_chain.size() == 0);
+      Assert(d_tracecheck.d_lines[i].d_clause.size()
+             == usedClauses[i].second.size());
+      for (size_t j = 0, m = usedClauses[i].second.size(); j < m; ++j)
+      {
+        Assert(usedClauses[i].second[j] == d_tracecheck.d_lines[i].d_clause[j]);
+      }
+    }
+  }
+
+  // Step two, identify definitions. They correspond to lines that follow the
+  // input lines, are in bounds, and have no justifying chain.
+  for (size_t i = usedClauses.size(), n = d_tracecheck.d_lines.size();
+       i < n && d_tracecheck.d_lines[i].d_chain.size() == 0;)
+  {
+    prop::SatClause c = d_tracecheck.d_lines[i].d_clause;
+    Assert(c.size() > 0);
+    Assert(!c[0].isNegated());
+
+    // Get the new variable of the definition -- the first variable of the
+    // first clause
+    prop::SatVariable newVar = c[0].getSatVariable();
+
+    // The rest of the literals in the clause of the 'other literals' of the def
+    std::vector<prop::SatLiteral> otherLiterals{++c.begin(), c.end()};
+
+    size_t nLinesForThisDef = 2 + otherLiterals.size();
+    // Look at the negation of the second literal in the second clause to get
+    // the old literal
+    AlwaysAssert(d_tracecheck.d_lines.size() > i + 1,
+                 "Malformed definition in TRACECHECK proof from drat2er");
+    d_definitions.emplace_back(newVar,
+                               ~d_tracecheck.d_lines[i + 1].d_clause[1],
+                               std::move(otherLiterals));
+
+    // Advance over the lines for this definition
+    i += nLinesForThisDef;
+  }
+}
+
+void ErProof::outputAsLfsc(std::ostream& os) const
+{
+  // How many parens to close?
+  size_t parenCount = 0;
+  std::unordered_set<prop::SatVariable> newVariables;
+
+  // Print Definitions
+  for (const ErDefinition& def : d_definitions)
+  {
+    os << "\n    (decl_rat_elimination_def ("
+       << (def.d_oldLiteral.isNegated() ? "neg " : "pos ")
+       << ProofManager::getVarName(def.d_oldLiteral.getSatVariable(), "bb")
+       << ") ";
+    LFSCProofPrinter::printSatClause(def.d_otherLiterals, os, "bb");
+    os << " (\\ er.v" << def.d_newVariable << " (\\ er.def"
+       << def.d_newVariable;
+    newVariables.insert(def.d_newVariable);
+  }
+  parenCount += 3 * d_definitions.size();
+
+  // Clausify Definitions
+  TraceCheckIdx firstDefClause = d_inputClauseIds.size() + 1;
+  for (const ErDefinition& def : d_definitions)
+  {
+    os << "\n    (clausify_rat_elimination_def _ _ _ "
+       << "er.def " << def.d_newVariable << " _ _ (\\ er.c" << firstDefClause
+       << " (\\ er.c" << (firstDefClause + 1) << " (\\ er.cnf"
+       << def.d_newVariable;
+
+    firstDefClause += 2 + def.d_otherLiterals.size();
+  }
+  parenCount += 4 * d_definitions.size();
+
+  // Unroll proofs of CNFs to proofs of clauses
+  firstDefClause = d_inputClauseIds.size() + 1;
+  for (const ErDefinition& def : d_definitions)
+  {
+    for (size_t i = 0, n = def.d_otherLiterals.size(); i < n; ++i)
+    {
+      os << "\n    (cnfc_unroll _ _ ";
+      os << "er.cnf" << def.d_newVariable;
+      if (i != 0)
+      {
+        os << ".u" << i;
+      }
+      os << " (\\ er.c" << (firstDefClause + 2 + i);
+      os << " (\\ er.cnf" << def.d_newVariable << ".u" << (i + 1);
+    }
+    parenCount += 3 * def.d_otherLiterals.size();
+
+    firstDefClause += 2 + def.d_otherLiterals.size();
+  }
+
+  // NB: At this point `firstDefClause` points to the first clause resulting
+  // from a resolution chain
+
+  // Now, elaborate each resolution chain
+  for (size_t cId = firstDefClause, nLines = d_tracecheck.d_lines.size();
+       cId <= nLines;
+       ++cId)
+  {
+    const std::vector<TraceCheckIdx>& chain =
+        d_tracecheck.d_lines[cId - 1].d_chain;
+    const std::vector<prop::SatLiteral> pivots = computePivotsForChain(chain);
+    Assert(chain.size() > 0);
+    Assert(chain.size() == pivots.size() + 1);
+
+    os << "\n    (satlem_simplify _ _ _ ";
+    parenCount += 1;
+
+    // Print resolution openings (reverse order)
+    for (int64_t i = pivots.size() - 1; i >= 0; --i)
+    {
+      prop::SatLiteral pivot = pivots[i];
+      os << "(" << (pivot.isNegated() ? 'Q' : 'R') << " _ _ ";
+    }
+
+    // Print resolution start
+    writeIdForClauseProof(os, chain[0]);
+    os << " ";
+
+    // Print resolution closings (forward order)
+    for (size_t i = 0, n = pivots.size(); i < n; ++i)
+    {
+      prop::SatVariable pivotVar = pivots[i].getSatVariable();
+      TraceCheckIdx clauseId = chain[i + 1];
+      writeIdForClauseProof(os, clauseId);
+      os << " ";
+      if (ContainsKey(newVariables, pivotVar))
+      {
+        // This is a defined variable
+        os << "er.v" << pivotVar;
+      }
+      else
+      {
+        os << ProofManager::getVarName(pivotVar, "bb");
+      }
+      os << ") ";
+    }
+    os << "(\\ er.c" << cId;
+    parenCount += 1;
+  }
+
+  // Write proof of bottom
+  Assert(d_tracecheck.d_lines.back().d_clause.size() == 0,
+         "The TRACECHECK proof from drat2er did not prove bottom.");
+  os << "\n      er.c" << d_tracecheck.d_lines.back().d_idx
+     << " ; (holds cln)\n";
+
+  // Finally, close the parentheses!
+  std::fill_n(std::ostream_iterator<char>(os), parenCount, ')');
+}
+
+namespace {
+/**
+ * Resolves two clauses
+ *
+ * @param dest one of the inputs, and the output too. **This is an input and
+ *             output**
+ * @param src the other input
+ *
+ * @return the unique literal that was resolved on, with the polarization that
+ *         it originally had in `dest`.
+ *
+ * For example, if dest = (1 3 -4 5) and src = (1 -3 5), then 3 is returned and
+ * after the call dest = (1 -4 5).
+ */
+prop::SatLiteral resolveModify(
+    std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>& dest,
+    const prop::SatClause& src)
+{
+  bool foundPivot = false;
+  prop::SatLiteral pivot(0, false);
+
+  for (prop::SatLiteral lit : src)
+  {
+    auto negationLocation = dest.find(~lit);
+    if (negationLocation != dest.end())
+    {
+      Assert(!foundPivot);
+      foundPivot = true;
+      dest.erase(negationLocation);
+      pivot = ~lit;
+    }
+    dest.insert(lit);
+  }
+
+  Assert(foundPivot);
+  return pivot;
+}
+}  // namespace
+
+std::vector<prop::SatLiteral> ErProof::computePivotsForChain(
+    const std::vector<TraceCheckIdx>& chain) const
+{
+  std::vector<prop::SatLiteral> pivots;
+
+  const prop::SatClause& first = d_tracecheck.d_lines[chain[0] - 1].d_clause;
+  std::unordered_set<prop::SatLiteral, prop::SatLiteralHashFunction>
+      runningClause{first.begin(), first.end()};
+
+  for (auto idx = ++chain.cbegin(), end = chain.cend(); idx != end; ++idx)
+  {
+    pivots.push_back(
+        resolveModify(runningClause, d_tracecheck.d_lines[*idx - 1].d_clause));
+  }
+  return pivots;
+}
+
+void ErProof::writeIdForClauseProof(std::ostream& o, TraceCheckIdx i) const
+{
+  if (i <= d_inputClauseIds.size())
+  {
+    // This clause is an input clause! Ask the ProofManager for its name
+    o << ProofManager::getInputClauseName(d_inputClauseIds[i - 1], "bb");
+  }
+  else
+  {
+    // This clause was introduced by a definition or resolution chain
+    o << "er.c" << i;
+  }
+}
+
+}  // namespace er
+}  // namespace proof
+}  // namespace CVC4
diff --git a/src/proof/er/er_proof.h b/src/proof/er/er_proof.h
new file mode 100644
index 000000000..f5af0783b
--- /dev/null
+++ b/src/proof/er/er_proof.h
@@ -0,0 +1,208 @@
+/*********************                                                        */
+/*! \file er_proof.h
+ ** \verbatim
+ ** Top contributors (to current version):
+ **   Alex Ozdemir
+ ** This file is part of the CVC4 project.
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
+ ** in the top-level source directory) and their institutional affiliations.
+ ** All rights reserved.  See the file COPYING in the top-level source
+ ** directory for licensing information.\endverbatim
+ **
+ ** \brief ER Proof Format
+ **
+ ** Declares C++ types that represent an ER/TRACECHECK proof.
+ ** Defines serialization for these types.
+ **
+ ** You can find details about the way ER is encoded in the TRACECHECK
+ ** format at these locations:
+ **    https://github.com/benjaminkiesl/drat2er
+ **    http://www.cs.utexas.edu/users/marijn/publications/ijcar18.pdf
+ **
+ **/
+
+#include "cvc4_private.h"
+
+#ifndef CVC4__PROOF__ER__ER_PROOF_H
+#define CVC4__PROOF__ER__ER_PROOF_H
+
+#include <memory>
+#include <vector>
+
+#include "proof/clause_id.h"
+#include "prop/sat_solver_types.h"
+
+namespace CVC4 {
+namespace proof {
+namespace er {
+
+using ClauseUseRecord = std::vector<std::pair<ClauseId, prop::SatClause>>;
+
+/**
+ * A definition of the form:
+ *    newVar <-> p v (~x_1 ^ ~x_2 ^ ... ^ ~x_n)
+ */
+struct ErDefinition
+{
+  ErDefinition(prop::SatVariable newVariable,
+               prop::SatLiteral oldLiteral,
+               std::vector<prop::SatLiteral>&& otherLiterals)
+      : d_newVariable(newVariable),
+        d_oldLiteral(oldLiteral),
+        d_otherLiterals(otherLiterals)
+  {
+  }
+
+  // newVar
+  prop::SatVariable d_newVariable;
+  // p
+  prop::SatLiteral d_oldLiteral;
+  // A list of the x_i's
+  std::vector<prop::SatLiteral> d_otherLiterals;
+};
+
+// For representing a clause's index within a TRACECHECK proof.
+using TraceCheckIdx = size_t;
+
+/**
+ * A single line in a TRACECHECK proof.
+ *
+ * Consists of the index of a new clause, the literals of that clause, and the
+ * indices for preceding clauses which can be combined in a resolution chain to
+ * produce this new clause.
+ */
+struct TraceCheckLine
+{
+  TraceCheckLine(TraceCheckIdx idx,
+                 std::vector<prop::SatLiteral>&& clause,
+                 std::vector<TraceCheckIdx>&& chain)
+      : d_idx(idx), d_clause(clause), d_chain(chain)
+  {
+  }
+
+  // The index of the new clause
+  TraceCheckIdx d_idx;
+  // The new clause
+  std::vector<prop::SatLiteral> d_clause;
+  /**
+   * Indices of clauses which must be resolved to produce this new clause.
+   * While the TRACECHECK format does not specify the order, we require them to
+   * be in resolution-order.
+   */
+  std::vector<TraceCheckIdx> d_chain;
+};
+
+/**
+ * A TRACECHECK proof -- just a list of lines
+ */
+struct TraceCheckProof
+{
+  static TraceCheckProof fromText(std::istream& in);
+  TraceCheckProof() : d_lines() {}
+
+  // The lines of this proof.
+  std::vector<TraceCheckLine> d_lines;
+};
+
+/**
+ * An extended resolution proof.
+ * It supports resolution, along with extensions of the form
+ *
+ *    newVar <-> p v (~x_1 ^ ~x_2 ^ ... ^ ~x_n)
+ */
+class ErProof
+{
+ public:
+  /**
+   * Construct an ER proof from a DRAT proof, using drat2er
+   *
+   * @param usedClauses The CNF formula that we're deriving bottom from.
+   * @param dratBinary  The DRAT proof from the SAT solver, as a binary stream.
+   */
+  static ErProof fromBinaryDratProof(const ClauseUseRecord& usedClauses,
+                                     const std::string& dratBinary);
+
+  /**
+   * Construct an ER proof from a TRACECHECK ER proof
+   *
+   * This basically just identifies groups of lines which correspond to
+   * definitions, and extracts them.
+   *
+   * @param usedClauses The CNF formula that we're deriving bottom from.
+   * @param tracecheck  The TRACECHECK proof, as a stream.
+   */
+  ErProof(const ClauseUseRecord& usedClauses, TraceCheckProof&& tracecheck);
+
+  /**
+   * Write the ER proof as an LFSC value of type (holds cln).
+   * The format is from the LFSC signature er.plf
+   *
+   * Reads the current `ProofManager` to determine what the variables should be
+   * named.
+   *
+   * @param os the stream to write to
+   */
+  void outputAsLfsc(std::ostream& os) const;
+
+  const std::vector<ClauseId>& getInputClauseIds() const
+  {
+    return d_inputClauseIds;
+  }
+
+  const std::vector<ErDefinition>& getDefinitions() const
+  {
+    return d_definitions;
+  }
+
+  const TraceCheckProof& getTraceCheckProof() const { return d_tracecheck; }
+
+ private:
+  /**
+   * Creates an empty ErProof.
+   */
+  ErProof() : d_inputClauseIds(), d_definitions(), d_tracecheck() {}
+
+  /**
+   * Computes the pivots on the basis of which an in-order resolution chain is
+   * resolved.
+   *
+   * c0   c1
+   *   \ /               Clauses c_i being resolved in a chain around
+   *    v1  c2           pivots v_i.
+   *     \ /
+   *      v2  c3
+   *       \ /
+   *        v3  c4
+   *         \ /
+   *          v4
+   *
+   *
+   * @param chain the chain, of N clause indices
+   *
+   * @return a list of N - 1 variables, the list ( v_i ) from i = 1 to N - 1
+   */
+  std::vector<prop::SatLiteral> computePivotsForChain(
+      const std::vector<TraceCheckIdx>& chain) const;
+
+  /**
+   * Write the LFSC identifier for the proof of a clause
+   *
+   * @param o where to write to
+   * @param i the TRACECHECK index for the clause whose proof identifier to
+   *        print
+   */
+  void writeIdForClauseProof(std::ostream& o, TraceCheckIdx i) const;
+
+  // A list of the Ids for the input clauses, in order.
+  std::vector<ClauseId> d_inputClauseIds;
+  // A list of new variable definitions, in order.
+  std::vector<ErDefinition> d_definitions;
+  // The underlying TRACECHECK proof.
+  TraceCheckProof d_tracecheck;
+};
+
+}  // namespace er
+}  // namespace proof
+}  // namespace CVC4
+
+#endif  // CVC4__PROOF__ER__ER_PROOF_H
diff --git a/src/proof/lemma_proof.cpp b/src/proof/lemma_proof.cpp
index 392805473..6bb2c2854 100644
--- a/src/proof/lemma_proof.cpp
+++ b/src/proof/lemma_proof.cpp
@@ -2,9 +2,9 @@
 /*! \file lemma_proof.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Guy Katz
+ **   Guy Katz, Alex Ozdemir
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/proof/lemma_proof.h b/src/proof/lemma_proof.h
index 857632083..7dfce57cf 100644
--- a/src/proof/lemma_proof.h
+++ b/src/proof/lemma_proof.h
@@ -2,9 +2,9 @@
 /*! \file lemma_proof.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Guy Katz
+ **   Guy Katz, Alex Ozdemir
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -15,8 +15,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__LEMMA_PROOF_H
-#define __CVC4__LEMMA_PROOF_H
+#ifndef CVC4__LEMMA_PROOF_H
+#define CVC4__LEMMA_PROOF_H
 
 #include "expr/expr.h"
 #include "proof/clause_id.h"
@@ -112,4 +112,4 @@ std::ostream& operator<<(std::ostream & out, const LemmaProofRecipe & recipe);
 
 } /* CVC4 namespace */
 
-#endif /* __CVC4__LEMMA_PROOF_H */
+#endif /* CVC4__LEMMA_PROOF_H */
diff --git a/src/proof/lfsc_proof_printer.cpp b/src/proof/lfsc_proof_printer.cpp
index be1259837..1a18d06a6 100644
--- a/src/proof/lfsc_proof_printer.cpp
+++ b/src/proof/lfsc_proof_printer.cpp
@@ -2,9 +2,9 @@
 /*! \file lfsc_proof_printer.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Andres Noetzli
+ **   Andres Noetzli, Alex Ozdemir, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/proof/lfsc_proof_printer.h b/src/proof/lfsc_proof_printer.h
index 36a3490f7..f2f55aa94 100644
--- a/src/proof/lfsc_proof_printer.h
+++ b/src/proof/lfsc_proof_printer.h
@@ -2,9 +2,9 @@
 /*! \file lfsc_proof_printer.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Andres Noetzli
+ **   Andres Noetzli, Alex Ozdemir
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF__LFSC_PROOF_PRINTER_H
-#define __CVC4__PROOF__LFSC_PROOF_PRINTER_H
+#ifndef CVC4__PROOF__LFSC_PROOF_PRINTER_H
+#define CVC4__PROOF__LFSC_PROOF_PRINTER_H
 
 #include <iosfwd>
 #include <string>
@@ -151,4 +151,4 @@ class LFSCProofPrinter
 }  // namespace proof
 }  // namespace CVC4
 
-#endif /* __CVC4__PROOF__LFSC_PROOF_PRINTER_H */
+#endif /* CVC4__PROOF__LFSC_PROOF_PRINTER_H */
diff --git a/src/proof/lrat/lrat_proof.cpp b/src/proof/lrat/lrat_proof.cpp
index 0b7af7aa5..a1939ec92 100644
--- a/src/proof/lrat/lrat_proof.cpp
+++ b/src/proof/lrat/lrat_proof.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Alex Ozdemir
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/proof/lrat/lrat_proof.h b/src/proof/lrat/lrat_proof.h
index a999e5ca6..33b2fad3f 100644
--- a/src/proof/lrat/lrat_proof.h
+++ b/src/proof/lrat/lrat_proof.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Alex Ozdemir
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -23,8 +23,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF__LRAT__LRAT_PROOF_H
-#define __CVC4__PROOF__LRAT__LRAT_PROOF_H
+#ifndef CVC4__PROOF__LRAT__LRAT_PROOF_H
+#define CVC4__PROOF__LRAT__LRAT_PROOF_H
 
 #include <iosfwd>
 #include <string>
diff --git a/src/proof/proof.h b/src/proof/proof.h
index 3ee8d66ef..9e7e20a22 100644
--- a/src/proof/proof.h
+++ b/src/proof/proof.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Tim King, Liana Hadarean, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF__PROOF_H
-#define __CVC4__PROOF__PROOF_H
+#ifndef CVC4__PROOF__PROOF_H
+#define CVC4__PROOF__PROOF_H
 
 #include "options/smt_options.h"
 
@@ -67,4 +67,4 @@
 # define PSTATS(x)
 #endif /* CVC4_PROOF_STATS */
 
-#endif /* __CVC4__PROOF__PROOF_H */
+#endif /* CVC4__PROOF__PROOF_H */
diff --git a/src/proof/proof_manager.cpp b/src/proof/proof_manager.cpp
index 9878972bf..005a23378 100644
--- a/src/proof/proof_manager.cpp
+++ b/src/proof/proof_manager.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Guy Katz, Liana Hadarean, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -30,6 +30,7 @@
 #include "proof/theory_proof.h"
 #include "smt/smt_engine.h"
 #include "smt/smt_engine_scope.h"
+#include "smt/smt_statistics_registry.h"
 #include "smt_util/node_visitor.h"
 #include "theory/arrays/theory_arrays.h"
 #include "theory/output_channel.h"
@@ -559,6 +560,9 @@ void LFSCProof::toStream(std::ostream& out, const ProofLetMap& map) const
 
 void LFSCProof::toStream(std::ostream& out) const
 {
+  TimerStat::CodeTimer proofProductionTimer(
+      *ProofManager::currentPM()->getProofProductionTime());
+
   Assert(!d_satProof->proofConstructed());
   d_satProof->constructProof();
 
@@ -730,8 +734,7 @@ void LFSCProof::toStream(std::ostream& out) const
 
   out << ";; Printing final unsat proof \n";
   if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER && ProofManager::getBitVectorProof()) {
-    proof::LFSCProofPrinter::printResolutionEmptyClause(
-        ProofManager::getBitVectorProof()->getSatProof(), out, paren);
+    ProofManager::getBitVectorProof()->printEmptyClauseProof(out, paren);
   } else {
     // print actual resolution proof
     proof::LFSCProofPrinter::printResolutions(d_satProof, out, paren);
@@ -1069,4 +1072,16 @@ void ProofManager::printTrustedTerm(Node term,
   tpe->printTheoryTerm(term.toExpr(), os, globalLetMap);
   if (tpe->printsAsBool(term)) os << ")";
 }
+
+ProofManager::ProofManagerStatistics::ProofManagerStatistics()
+    : d_proofProductionTime("proof::ProofManager::proofProductionTime")
+{
+  smtStatisticsRegistry()->registerStat(&d_proofProductionTime);
+}
+
+ProofManager::ProofManagerStatistics::~ProofManagerStatistics()
+{
+  smtStatisticsRegistry()->unregisterStat(&d_proofProductionTime);
+}
+
 } /* CVC4  namespace */
diff --git a/src/proof/proof_manager.h b/src/proof/proof_manager.h
index 82efbab0f..eb5942bea 100644
--- a/src/proof/proof_manager.h
+++ b/src/proof/proof_manager.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Liana Hadarean, Guy Katz, Morgan Deters
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,17 +16,17 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF_MANAGER_H
-#define __CVC4__PROOF_MANAGER_H
+#ifndef CVC4__PROOF_MANAGER_H
+#define CVC4__PROOF_MANAGER_H
 
 #include <iosfwd>
 #include <memory>
 #include <unordered_map>
 #include <unordered_set>
 
-#include "expr/node.h"
-#include "context/cdhashset.h"
 #include "context/cdhashmap.h"
+#include "context/cdhashset.h"
+#include "expr/node.h"
 #include "proof/clause_id.h"
 #include "proof/proof.h"
 #include "proof/proof_utils.h"
@@ -34,7 +34,7 @@
 #include "theory/logic_info.h"
 #include "theory/substitutions.h"
 #include "util/proof.h"
-
+#include "util/statistics_registry.h"
 
 namespace CVC4 {
 
@@ -298,9 +298,26 @@ public:
                          std::ostream& out,
                          std::ostringstream& paren);
 
-private:
+  TimerStat* getProofProductionTime() { return &d_stats.d_proofProductionTime; }
+
+ private:
   void constructSatProof();
   std::set<Node> satClauseToNodeSet(prop::SatClause* clause);
+
+  struct ProofManagerStatistics
+  {
+    ProofManagerStatistics();
+    ~ProofManagerStatistics();
+
+    /**
+     * Time spent producing proofs (i.e. generating the proof from the logging
+     * information)
+     */
+    TimerStat d_proofProductionTime;
+  }; /* struct ProofManagerStatistics */
+
+  ProofManagerStatistics d_stats;
+
 };/* class ProofManager */
 
 class LFSCProof : public Proof
@@ -334,4 +351,4 @@ std::ostream& operator<<(std::ostream& out, CVC4::ProofRule k);
 
 
 
-#endif /* __CVC4__PROOF_MANAGER_H */
+#endif /* CVC4__PROOF_MANAGER_H */
diff --git a/src/proof/proof_output_channel.cpp b/src/proof/proof_output_channel.cpp
index 1489e83bd..449e12225 100644
--- a/src/proof/proof_output_channel.cpp
+++ b/src/proof/proof_output_channel.cpp
@@ -2,9 +2,9 @@
 /*! \file proof_output_channel.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Guy Katz, Tim King
+ **   Guy Katz, Tim King, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/proof/proof_output_channel.h b/src/proof/proof_output_channel.h
index 8be434f50..ff84a3743 100644
--- a/src/proof/proof_output_channel.h
+++ b/src/proof/proof_output_channel.h
@@ -2,9 +2,9 @@
 /*! \file proof_output_channel.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Tim King, Guy Katz
+ **   Tim King, Guy Katz, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -13,8 +13,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF_OUTPUT_CHANNEL_H
-#define __CVC4__PROOF_OUTPUT_CHANNEL_H
+#ifndef CVC4__PROOF_OUTPUT_CHANNEL_H
+#define CVC4__PROOF_OUTPUT_CHANNEL_H
 
 #include <memory>
 #include <set>
@@ -74,4 +74,4 @@ public:
 
 } /* CVC4 namespace */
 
-#endif /* __CVC4__PROOF_OUTPUT_CHANNEL_H */
+#endif /* CVC4__PROOF_OUTPUT_CHANNEL_H */
diff --git a/src/proof/proof_utils.cpp b/src/proof/proof_utils.cpp
index ead70ddde..3342d421a 100644
--- a/src/proof/proof_utils.cpp
+++ b/src/proof/proof_utils.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Liana Hadarean, Andrew Reynolds, Guy Katz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/proof/proof_utils.h b/src/proof/proof_utils.h
index c24897c8d..cb509063d 100644
--- a/src/proof/proof_utils.h
+++ b/src/proof/proof_utils.h
@@ -2,9 +2,9 @@
 /*! \file proof_utils.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Guy Katz, Tim King
+ **   Liana Hadarean, Guy Katz, Dejan Jovanovic
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/proof/resolution_bitvector_proof.cpp b/src/proof/resolution_bitvector_proof.cpp
index 1db673949..505500d5e 100644
--- a/src/proof/resolution_bitvector_proof.cpp
+++ b/src/proof/resolution_bitvector_proof.cpp
@@ -2,9 +2,9 @@
 /*! \file resolution_bitvector_proof.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Guy Katz, Paul Meng
+ **   Alex Ozdemir, Liana Hadarean, Guy Katz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/proof/resolution_bitvector_proof.h b/src/proof/resolution_bitvector_proof.h
index 6c2ae589f..5fd11092f 100644
--- a/src/proof/resolution_bitvector_proof.h
+++ b/src/proof/resolution_bitvector_proof.h
@@ -2,9 +2,9 @@
 /*! \file resolution_bitvector_proof.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Mathias Preiner, Guy Katz
+ **   Alex Ozdemir, Mathias Preiner, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H
-#define __CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H
+#ifndef CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H
+#define CVC4__PROOF__RESOLUTION_BITVECTOR_PROOF_H
 
 #include <iosfwd>
 
@@ -110,4 +110,4 @@ class LfscResolutionBitVectorProof : public ResolutionBitVectorProof
 
 }  // namespace CVC4
 
-#endif /* __CVC4__PROOF__RESOLUTIONBITVECTORPROOF_H */
+#endif /* CVC4__PROOF__RESOLUTIONBITVECTORPROOF_H */
diff --git a/src/proof/sat_proof.h b/src/proof/sat_proof.h
index 8fd2cb9eb..ec0928c07 100644
--- a/src/proof/sat_proof.h
+++ b/src/proof/sat_proof.h
@@ -2,9 +2,9 @@
 /*! \file sat_proof.h
  ** \verbatim
  ** Top contributors (to current version):
- **   Liana Hadarean, Tim King, Guy Katz
+ **   Liana Hadarean, Tim King, Andres Noetzli
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__SAT__PROOF_H
-#define __CVC4__SAT__PROOF_H
+#ifndef CVC4__SAT__PROOF_H
+#define CVC4__SAT__PROOF_H
 
 #include <stdint.h>
 
@@ -373,4 +373,4 @@ void toSatClause(const typename Solver::TClause& minisat_cl,
 
 } /* CVC4 namespace */
 
-#endif /* __CVC4__SAT__PROOF_H */
+#endif /* CVC4__SAT__PROOF_H */
diff --git a/src/proof/sat_proof_implementation.h b/src/proof/sat_proof_implementation.h
index 96f99be47..d9c959ae4 100644
--- a/src/proof/sat_proof_implementation.h
+++ b/src/proof/sat_proof_implementation.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Liana Hadarean, Tim King, Guy Katz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__SAT__PROOF_IMPLEMENTATION_H
-#define __CVC4__SAT__PROOF_IMPLEMENTATION_H
+#ifndef CVC4__SAT__PROOF_IMPLEMENTATION_H
+#define CVC4__SAT__PROOF_IMPLEMENTATION_H
 
 #include "proof/clause_id.h"
 #include "proof/cnf_proof.h"
@@ -1081,4 +1081,4 @@ inline std::ostream& operator<<(std::ostream& out, CVC4::ClauseKind k) {
 
 } /* CVC4 namespace */
 
-#endif /* __CVC4__SAT__PROOF_IMPLEMENTATION_H */
+#endif /* CVC4__SAT__PROOF_IMPLEMENTATION_H */
diff --git a/src/proof/simplify_boolean_node.cpp b/src/proof/simplify_boolean_node.cpp
index 0ad6d0500..0fd69fc20 100644
--- a/src/proof/simplify_boolean_node.cpp
+++ b/src/proof/simplify_boolean_node.cpp
@@ -2,9 +2,9 @@
 /*! \file simplify_boolean_node.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Guy Katz
+ **   Guy Katz, Liana Hadarean, Andrew Reynolds
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/proof/simplify_boolean_node.h b/src/proof/simplify_boolean_node.h
index 1c479e38d..fe8b7174b 100644
--- a/src/proof/simplify_boolean_node.h
+++ b/src/proof/simplify_boolean_node.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Guy Katz
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -15,8 +15,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__SIMPLIFY_BOOLEAN_NODE_H
-#define __CVC4__SIMPLIFY_BOOLEAN_NODE_H
+#ifndef CVC4__SIMPLIFY_BOOLEAN_NODE_H
+#define CVC4__SIMPLIFY_BOOLEAN_NODE_H
 
 namespace CVC4 {
 
@@ -24,4 +24,4 @@ Node simplifyBooleanNode(const Node &n);
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__SIMPLIFY_BOOLEAN_NODE_H */
+#endif /* CVC4__SIMPLIFY_BOOLEAN_NODE_H */
diff --git a/src/proof/skolemization_manager.cpp b/src/proof/skolemization_manager.cpp
index f5fba4003..b0397d08c 100644
--- a/src/proof/skolemization_manager.cpp
+++ b/src/proof/skolemization_manager.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Paul Meng, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/proof/skolemization_manager.h b/src/proof/skolemization_manager.h
index d8feb959f..cb23268f3 100644
--- a/src/proof/skolemization_manager.h
+++ b/src/proof/skolemization_manager.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Guy Katz, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__SKOLEMIZATION_MANAGER_H
-#define __CVC4__SKOLEMIZATION_MANAGER_H
+#ifndef CVC4__SKOLEMIZATION_MANAGER_H
+#define CVC4__SKOLEMIZATION_MANAGER_H
 
 #include <iostream>
 #include <unordered_map>
@@ -52,4 +52,4 @@ private:
 
 
 
-#endif /* __CVC4__SKOLEMIZATION_MANAGER_H */
+#endif /* CVC4__SKOLEMIZATION_MANAGER_H */
diff --git a/src/proof/theory_proof.cpp b/src/proof/theory_proof.cpp
index fe9acfef3..c66aa59e4 100644
--- a/src/proof/theory_proof.cpp
+++ b/src/proof/theory_proof.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Guy Katz, Liana Hadarean, Yoni Zohar
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -85,8 +85,27 @@ void TheoryProofEngine::registerTheory(theory::Theory* th) {
         if (options::bitblastMode() == theory::bv::BITBLAST_MODE_EAGER
             && options::bvSatSolver() == theory::bv::SAT_SOLVER_CRYPTOMINISAT)
         {
-          proof::BitVectorProof* bvp =
-              new proof::LfscClausalBitVectorProof(thBv, this);
+          proof::BitVectorProof* bvp = nullptr;
+          switch (options::bvProofFormat())
+          {
+            case theory::bv::BvProofFormat::BITVECTOR_PROOF_DRAT:
+            {
+              bvp = new proof::LfscDratBitVectorProof(thBv, this);
+              break;
+            }
+            case theory::bv::BvProofFormat::BITVECTOR_PROOF_LRAT:
+            {
+              bvp = new proof::LfscLratBitVectorProof(thBv, this);
+              break;
+            }
+            case theory::bv::BvProofFormat::BITVECTOR_PROOF_ER:
+            {
+              bvp = new proof::LfscErBitVectorProof(thBv, this);
+              break;
+            }
+            default: { Unreachable("Invalid BvProofFormat");
+            }
+          };
           d_theoryProofTable[id] = bvp;
         }
         else
diff --git a/src/proof/theory_proof.h b/src/proof/theory_proof.h
index 2f2ce83fd..b487b62a8 100644
--- a/src/proof/theory_proof.h
+++ b/src/proof/theory_proof.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Liana Hadarean, Guy Katz, Yoni Zohar
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__THEORY_PROOF_H
-#define __CVC4__THEORY_PROOF_H
+#ifndef CVC4__THEORY_PROOF_H
+#define CVC4__THEORY_PROOF_H
 
 #include <iosfwd>
 #include <unordered_map>
@@ -401,4 +401,4 @@ public:
 
 } /* CVC4 namespace */
 
-#endif /* __CVC4__THEORY_PROOF_H */
+#endif /* CVC4__THEORY_PROOF_H */
diff --git a/src/proof/uf_proof.cpp b/src/proof/uf_proof.cpp
index 5d4a1ce11..10823693d 100644
--- a/src/proof/uf_proof.cpp
+++ b/src/proof/uf_proof.cpp
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Liana Hadarean, Guy Katz, Yoni Zohar
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -141,7 +141,7 @@ Node ProofUF::toStreamRecLFSC(std::ostream& out,
 
     return Node();
   }
-
+  // TODO (#2965): improve this code, which is highly complicated.
   switch(pf.d_id) {
   case theory::eq::MERGED_THROUGH_CONGRUENCE: {
     Debug("pf::uf") << "\nok, looking at congruence:\n";
diff --git a/src/proof/uf_proof.h b/src/proof/uf_proof.h
index 6f69a3d00..ca8b3f90e 100644
--- a/src/proof/uf_proof.h
+++ b/src/proof/uf_proof.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Liana Hadarean, Mathias Preiner, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -16,8 +16,8 @@
 
 #include "cvc4_private.h"
 
-#ifndef __CVC4__UF__PROOF_H
-#define __CVC4__UF__PROOF_H
+#ifndef CVC4__UF__PROOF_H
+#define CVC4__UF__PROOF_H
 
 #include <memory>
 #include <unordered_set>
@@ -102,4 +102,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__UF__PROOF_H */
+#endif /* CVC4__UF__PROOF_H */
diff --git a/src/proof/unsat_core.cpp b/src/proof/unsat_core.cpp
index 0321ccd29..4212331af 100644
--- a/src/proof/unsat_core.cpp
+++ b/src/proof/unsat_core.cpp
@@ -2,9 +2,9 @@
 /*! \file unsat_core.cpp
  ** \verbatim
  ** Top contributors (to current version):
- **   Morgan Deters, Tim King, Clark Barrett
+ **   Morgan Deters, Clark Barrett, Tim King
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
diff --git a/src/proof/unsat_core.h b/src/proof/unsat_core.h
index 77f65e24a..0217b6326 100644
--- a/src/proof/unsat_core.h
+++ b/src/proof/unsat_core.h
@@ -4,7 +4,7 @@
  ** Top contributors (to current version):
  **   Morgan Deters, Andrew Reynolds, Liana Hadarean
  ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2018 by the authors listed in the file AUTHORS
+ ** Copyright (c) 2009-2019 by the authors listed in the file AUTHORS
  ** in the top-level source directory) and their institutional affiliations.
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
@@ -17,8 +17,8 @@
 
 #include "cvc4_public.h"
 
-#ifndef __CVC4__UNSAT_CORE_H
-#define __CVC4__UNSAT_CORE_H
+#ifndef CVC4__UNSAT_CORE_H
+#define CVC4__UNSAT_CORE_H
 
 #include <iosfwd>
 #include <vector>
@@ -71,4 +71,4 @@ public:
 
 }/* CVC4 namespace */
 
-#endif /* __CVC4__UNSAT_CORE_H */
+#endif /* CVC4__UNSAT_CORE_H */