Enable CryptoMiniSat-backed BV proofs

* Connect the plumbing so that BV proofs are enabled when using
CryptoMiniSat
* Also fixed a bug in CNF-proof generation
   * Specifically, CNF proofs broke when proving tautological clauses.
     Now they don't.

1 files changed, 10 insertions, 3 deletions

diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp
index 452b64b11..63072ad96 100644
--- a/src/proof/er/er_proof.cpp
+++ b/src/proof/er/er_proof.cpp
@@ -132,8 +132,6 @@ ErProof ErProof::fromBinaryDratProof(const ClauseUseRecord& usedClauses,
   dratStream.close();
   tracecheckStream.close();
 
-
-
   return proof;
 }
 
@@ -156,6 +154,15 @@ ErProof::ErProof(const ClauseUseRecord& usedClauses,
     {
       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)
@@ -185,7 +192,7 @@ ErProof::ErProof(const ClauseUseRecord& usedClauses,
     // 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");
+                 "Malformed definition in TRACECHECK proof from drat2er");
     d_definitions.emplace_back(newVar,
                                ~d_tracecheck.d_lines[i + 1].d_clause[1],
                                std::move(otherLiterals));