Always assert that drat-trim exits successfully.

Also, removed unneeded (and sometimes violated) assertions.

2 files changed, 2 insertions, 9 deletions

diff --git a/src/proof/clausal_bitvector_proof.cpp b/src/proof/clausal_bitvector_proof.cpp
index 473429590..25e519bfb 100644
--- a/src/proof/clausal_bitvector_proof.cpp
+++ b/src/proof/clausal_bitvector_proof.cpp
@@ -133,8 +133,9 @@ void ClausalBitVectorProof::optimizeDratProof()
   dratStream.close();
 
 #if CVC4_USE_DRAT2ER
-  drat2er::drat_trim::OptimizeWithDratTrim(
+  int dratTrimExitCode = drat2er::drat_trim::OptimizeWithDratTrim(
       formulaFilename, dratFilename, optDratFilename, drat2er::options::QUIET);
+  AlwaysAssert(dratTrimExitCode == 0, "drat-trim exited with %d", dratTrimExitCode);
 #else
   Unimplemented(
       "Proof production when using CryptoMiniSat requires drat2er.\n"
diff --git a/src/proof/er/er_proof.cpp b/src/proof/er/er_proof.cpp
index c73fbee05..e441233d9 100644
--- a/src/proof/er/er_proof.cpp
+++ b/src/proof/er/er_proof.cpp
@@ -162,14 +162,6 @@ ErProof::ErProof(const ClauseUseRecord& usedClauses,
           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]);
-      }
     }
   }