1 files changed, 13 insertions, 8 deletions
diff --git a/src/proof/er/er_proof.h b/src/proof/er/er_proof.h
index f5af0783b..d6cbd9213 100644
--- a/src/proof/er/er_proof.h
+++ b/src/proof/er/er_proof.h
@@ -27,6 +27,7 @@
 #define CVC4__PROOF__ER__ER_PROOF_H
 
 #include <memory>
+#include <unordered_map>
 #include <vector>
 
 #include "proof/clause_id.h"
@@ -36,8 +37,6 @@ 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)
@@ -116,11 +115,14 @@ class ErProof
   /**
    * 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.
+   * @param clauses A store of clauses that might be in our formula
+   * @param usedIds the ids of clauses that are actually in our formula
+   * @param dratBinary  The DRAT proof from the SAT solver, as a binary stream
    */
-  static ErProof fromBinaryDratProof(const ClauseUseRecord& usedClauses,
-                                     const std::string& dratBinary);
+  static ErProof fromBinaryDratProof(
+      const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+      const std::vector<ClauseId>& usedIds,
+      const std::string& dratBinary);
 
   /**
    * Construct an ER proof from a TRACECHECK ER proof
@@ -128,10 +130,13 @@ class ErProof
    * 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 clauses A store of clauses that might be in our formula
+   * @param usedIds the ids of clauses that are actually in our formula
    * @param tracecheck  The TRACECHECK proof, as a stream.
    */
-  ErProof(const ClauseUseRecord& usedClauses, TraceCheckProof&& tracecheck);
+  ErProof(const std::unordered_map<ClauseId, prop::SatClause>& clauses,
+          const std::vector<ClauseId>& usedIds,
+          TraceCheckProof&& tracecheck);
 
   /**
    * Write the ER proof as an LFSC value of type (holds cln).