Removes old proof code (#4964)

This deletes much of the old proof code. Basically everything but the minimal necessary infra-structure for producing unsat cores. That includes dependency tracking in preprocessing, the prop engine proof and the unsat core computation code in the old proof manager. These should also go once we fully integrate into master the new proof infrastructure.

It also cleans interfaces that were using old-proof-code-specific constructs (such as LemmaProofRecipe). When possible or when it made sense standalone local proof production code was kept, but deactivated (such is in the equality engine and in the arithmetic solver).

16 files changed, 32 insertions, 976 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 4de32a426..1a33ee3a5 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -622,7 +622,6 @@ set(regress_0_tests
   regress0/nl/very-easy-sat.smt2
   regress0/nl/very-simple-unsat.smt2
   regress0/options/invalid_dump.smt2
-  regress0/options/invalid_option_inc_proofs.smt2
   regress0/opt-abd-no-use.smt2
   regress0/parallel-let.smt2
   regress0/parser/as.smt2
@@ -872,7 +871,7 @@ set(regress_0_tests
   regress0/seq/seq-nth.smt2
   regress0/seq/seq-nth-uf.smt2
   regress0/seq/seq-nth-uf-z.smt2
-  regress0/seq/seq-nth-undef.smt2        
+  regress0/seq/seq-nth-undef.smt2
   regress0/seq/seq-rewrites.smt2
   regress0/sets/abt-min.smt2
   regress0/sets/abt-te-exh.smt2
diff --git a/test/regress/regress0/bug217.smt2 b/test/regress/regress0/bug217.smt2
index 30c87333e..4d2e828b5 100644
--- a/test/regress/regress0/bug217.smt2
+++ b/test/regress/regress0/bug217.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --fewer-preprocessing-holes
 ; EXPECT: unsat
 (set-logic QF_UF)
 (set-info :status unsat)
diff --git a/test/regress/regress0/options/invalid_option_inc_proofs.smt2 b/test/regress/regress0/options/invalid_option_inc_proofs.smt2
deleted file mode 100644
index f63dbd27f..000000000
--- a/test/regress/regress0/options/invalid_option_inc_proofs.smt2
+++ /dev/null
@@ -1,6 +0,0 @@
-; REQUIRES: proof
-; COMMAND-LINE: --incremental --proof
-; EXPECT: (error "Error in option parsing: --incremental is not supported with proofs")
-; EXIT: 1
-(set-logic QF_BV)
-(check-sat)
diff --git a/test/regress/regress1/bv/bench_38.delta.smt2 b/test/regress/regress1/bv/bench_38.delta.smt2
index 760614348..3f809716a 100644
--- a/test/regress/regress1/bv/bench_38.delta.smt2
+++ b/test/regress/regress1/bv/bench_38.delta.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --fewer-preprocessing-holes --check-proof --quiet
+; COMMAND-LINE: --quiet
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun x () (_ BitVec 4))
diff --git a/test/regress/regress1/non-fatal-errors.smt2 b/test/regress/regress1/non-fatal-errors.smt2
index 1e1865883..ec3d02927 100644
--- a/test/regress/regress1/non-fatal-errors.smt2
+++ b/test/regress/regress1/non-fatal-errors.smt2
@@ -2,11 +2,10 @@
 ; EXPECT: success
 ; EXPECT: success
 ; EXPECT: success
+; EXPECT: unsupported
 ; EXPECT: success
 ; EXPECT: success
 ; EXPECT: success
-; EXPECT: success
-; EXPECT: (error "")
 ; EXPECT: (error "")
 ; EXPECT: (error "")
 ; EXPECT: (error "")
@@ -22,7 +21,6 @@
 (declare-fun p () Bool)
 (get-unsat-core)
 (get-value (p))
-(get-proof)
 (get-model)
 (get-assignment)
 (assert true)
diff --git a/test/regress/regress1/quantifiers/dump-inst-proof.smt2 b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
index 9edc4df2b..f900e78a9 100644
--- a/test/regress/regress1/quantifiers/dump-inst-proof.smt2
+++ b/test/regress/regress1/quantifiers/dump-inst-proof.smt2
@@ -1,5 +1,5 @@
 ; REQUIRES: proof
-; COMMAND-LINE: --dump-instantiations --proof --print-inst-full
+; COMMAND-LINE: --dump-instantiations --produce-unsat-cores --print-inst-full
 ; EXPECT: unsat
 ; EXPECT: (instantiations (forall ((x Int)) (or (P x) (Q x)) )
 ; EXPECT:   ( 2 )
@@ -21,7 +21,7 @@
 (assert (forall ((x Int)) (or (not (S x)) (not (Q x)))))
 (assert (and (not (R 0)) (not (R 10)) (not (S 1)) (not (P 2))))
 (assert (S 2))
-; This tests that --proof minimizes the instantiations printed out.
-; This regression should require only the 2 instantiations above, but
-; may try more.
+; This tests that --produce-unsat-cores minimizes the instantiations
+; printed out.  This regression should require only the 2
+; instantiations above, but may try more.
 (check-sat)
diff --git a/test/unit/CMakeLists.txt b/test/unit/CMakeLists.txt
index bd7c1ea22..bd7029c54 100644
--- a/test/unit/CMakeLists.txt
+++ b/test/unit/CMakeLists.txt
@@ -107,7 +107,6 @@ add_subdirectory(expr)
 add_subdirectory(main)
 add_subdirectory(parser)
 add_subdirectory(prop)
-add_subdirectory(proof)
 add_subdirectory(theory)
 add_subdirectory(preprocessing)
 add_subdirectory(util)
diff --git a/test/unit/proof/CMakeLists.txt b/test/unit/proof/CMakeLists.txt
deleted file mode 100644
index 315c78d6f..000000000
--- a/test/unit/proof/CMakeLists.txt
+++ /dev/null
@@ -1,7 +0,0 @@
-#-----------------------------------------------------------------------------#
-# Add unit tests
-
-cvc4_add_unit_test_black(drat_proof_black proof)
-cvc4_add_unit_test_black(er_proof_black proof)
-cvc4_add_unit_test_black(lrat_proof_black proof)
-cvc4_add_unit_test_black(lfsc_proof_printer_black proof)
diff --git a/test/unit/proof/drat_proof_black.h b/test/unit/proof/drat_proof_black.h
deleted file mode 100644
index 4b593a588..000000000
--- a/test/unit/proof/drat_proof_black.h
+++ /dev/null
@@ -1,187 +0,0 @@
-/*********************                                                        */
-/*! \file drat_proof_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Alex Ozdemir, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 Black box testing of the DRAT proof class
- **
- ** In particular, tests DRAT binary parsing.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <cctype>
-
-#include "proof/drat/drat_proof.h"
-
-using namespace CVC4::proof::drat;
-
-class DratProofBlack : public CxxTest::TestSuite
-{
- public:
-  void setUp() override {}
-  void tearDown() override {}
-
-  void testParseOneAdd();
-  void testParseOneMediumAdd();
-  void testParseOneBigAdd();
-  void testParseLiteralIsTooBig();
-  void testParseLiteralOverflow();
-  void testParseClauseOverflow();
-
-  void testParseTwo();
-
-  void testOutputTwoAsText();
-  void testOutputTwoAsLfsc();
-};
-
-void DratProofBlack::testParseOneAdd()
-{
-  // a 1;
-  std::string input("a\x02\x00", 3);
-  DratProof proof = DratProof::fromBinary(input);
-
-  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_kind, ADDITION);
-  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause.size(), 1);
-  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[0],
-                   SatLiteral(0, false));
-}
-
-void DratProofBlack::testParseOneMediumAdd()
-{
-  // a -255;
-  std::string input("a\xff\x01\x00", 4);
-  DratProof proof = DratProof::fromBinary(input);
-
-  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_kind, ADDITION);
-  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause.size(), 1);
-  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[0],
-                   SatLiteral(126, true));
-}
-
-void DratProofBlack::testParseOneBigAdd()
-{
-  // a -2199023255551;
-  std::string input("a\xff\xff\xff\xff\xff\x7f\x00", 8);
-  DratProof proof = DratProof::fromBinary(input);
-
-  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_kind, ADDITION);
-  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause.size(), 1);
-  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[0],
-                   SatLiteral(2199023255550, true));
-}
-
-void DratProofBlack::testParseLiteralIsTooBig()
-{
-  std::string input("a\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\xff\x7f\x00",
-                    14);
-  TS_ASSERT_THROWS(DratProof::fromBinary(input), InvalidDratProofException&);
-}
-
-void DratProofBlack::testParseLiteralOverflow()
-{
-  std::string input("a\x80", 2);
-  TS_ASSERT_THROWS(DratProof::fromBinary(input), InvalidDratProofException&);
-}
-
-void DratProofBlack::testParseClauseOverflow()
-{
-  std::string input("a\x80\x01", 3);
-  TS_ASSERT_THROWS(DratProof::fromBinary(input), InvalidDratProofException&);
-}
-
-void DratProofBlack::testParseTwo()
-{
-  // d -63 -8193
-  // 129 -8191
-  std::string input("\x64\x7f\x83\x80\x01\x00\x61\x82\x02\xff\x7f\x00", 12);
-  DratProof proof = DratProof::fromBinary(input);
-
-  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_kind, DELETION);
-  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause.size(), 2);
-  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[0],
-                   SatLiteral(62, true));
-  TS_ASSERT_EQUALS(proof.getInstructions()[0].d_clause[1],
-                   SatLiteral(8192, true));
-
-  TS_ASSERT_EQUALS(proof.getInstructions()[1].d_kind, ADDITION);
-  TS_ASSERT_EQUALS(proof.getInstructions()[1].d_clause.size(), 2);
-  TS_ASSERT_EQUALS(proof.getInstructions()[1].d_clause[0],
-                   SatLiteral(128, false));
-  TS_ASSERT_EQUALS(proof.getInstructions()[1].d_clause[1],
-                   SatLiteral(8190, true));
-}
-
-void DratProofBlack::testOutputTwoAsText()
-{
-  // d -63 -8193
-  // 129 -8191
-  std::string input("\x64\x7f\x83\x80\x01\x00\x61\x82\x02\xff\x7f\x00", 12);
-  DratProof proof = DratProof::fromBinary(input);
-
-  std::ostringstream output;
-  proof.outputAsText(output);
-
-  std::istringstream tokens(output.str());
-  std::string token;
-
-  tokens >> token;
-  TS_ASSERT_EQUALS(token, "d");
-
-  tokens >> token;
-  TS_ASSERT_EQUALS(token, "-63");
-
-  tokens >> token;
-  TS_ASSERT_EQUALS(token, "-8193");
-
-  tokens >> token;
-  TS_ASSERT_EQUALS(token, "0");
-
-  tokens >> token;
-  TS_ASSERT_EQUALS(token, "129");
-
-  tokens >> token;
-  TS_ASSERT_EQUALS(token, "-8191");
-
-  tokens >> token;
-  TS_ASSERT_EQUALS(token, "0");
-}
-
-void DratProofBlack::testOutputTwoAsLfsc()
-{
-  // d -63 -8193
-  // 129 -8191
-  std::string input("\x64\x7f\x83\x80\x01\x00\x61\x82\x02\xff\x7f\x00", 12);
-  DratProof proof = DratProof::fromBinary(input);
-  std::ostringstream lfsc;
-  proof.outputAsLfsc(lfsc, 2);
-  std::ostringstream lfscWithoutWhitespace;
-  for (char c : lfsc.str())
-  {
-    if (!std::isspace(c))
-    {
-      lfscWithoutWhitespace << c;
-    }
-  }
-  std::string expectedLfsc =
-      "(DRATProofd (clc (neg bb.v62)  (clc (neg bb.v8192) cln))"
-      "(DRATProofa (clc (pos bb.v128) (clc (neg bb.v8190) cln))"
-      "DRATProofn))";
-  std::ostringstream expectedLfscWithoutWhitespace;
-  for (char c : expectedLfsc)
-  {
-    if (!std::isspace(c))
-    {
-      expectedLfscWithoutWhitespace << c;
-    }
-  }
-
-  TS_ASSERT_EQUALS(lfscWithoutWhitespace.str(),
-                   expectedLfscWithoutWhitespace.str());
-}
diff --git a/test/unit/proof/er_proof_black.h b/test/unit/proof/er_proof_black.h
deleted file mode 100644
index d9178e34e..000000000
--- a/test/unit/proof/er_proof_black.h
+++ /dev/null
@@ -1,464 +0,0 @@
-/*********************                                                        */
-/*! \file er_proof_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Alex Ozdemir
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 Black box testing of the ER proof class
- **
- ** In particular, tests TRACECHECK parsing and ER LFSC output.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <algorithm>
-#include <cctype>
-#include <iostream>
-#include <iterator>
-#include <string>
-#include <unordered_map>
-#include <vector>
-
-#include "base/configuration_private.h"
-#include "proof/clause_id.h"
-#include "proof/er/er_proof.h"
-#include "prop/sat_solver_types.h"
-#include "utils.h"
-
-#if IS_LFSC_BUILD
-#include "lfscc.h"
-
-namespace CVC4 {
-namespace proof {
-extern const char* const plf_signatures;
-}  // namespace proof
-}  // namespace CVC4
-#endif
-
-
-using namespace CVC4;
-using namespace CVC4::proof::er;
-using namespace CVC4::prop;
-
-class ErProofBlack : public CxxTest::TestSuite
-{
- public:
-  void setUp() override {}
-  void tearDown() override {}
-
-  void testTraceCheckParse1Line();
-  void testTraceCheckParse5Lines();
-  void testErTraceCheckParse();
-  void testErTraceCheckOutput();
-  void testErTraceCheckOutputMedium();
-};
-
-/**
- * @brief Add a new clause to the clause store and list of used clauses
- *
- * @param clauses the clause store
- * @param usedIds the used clauses
- * @param id the id of the new clause
- * @param clause the clause itself
- */
-void addClause(std::unordered_map<ClauseId, SatClause>& clauses,
-               std::vector<ClauseId>& usedIds,
-               ClauseId id,
-               SatClause&& clause)
-{
-  clauses.emplace(id, std::move(clause));
-  usedIds.push_back(id);
-}
-
-void ErProofBlack::testTraceCheckParse1Line()
-{
-  std::string tracecheckText = "1 -2 3 0 4 2 0\n";
-  std::istringstream stream(tracecheckText);
-  TraceCheckProof pf = TraceCheckProof::fromText(stream);
-  TS_ASSERT_EQUALS(pf.d_lines.size(), 1);
-
-  TS_ASSERT_EQUALS(pf.d_lines[0].d_idx, 1);
-  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause.size(), 2);
-  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[0], SatLiteral(1, true));
-  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[1], SatLiteral(2, false));
-  TS_ASSERT_EQUALS(pf.d_lines[0].d_chain.size(), 2);
-  TS_ASSERT_EQUALS(pf.d_lines[0].d_chain[0], 4);
-  TS_ASSERT_EQUALS(pf.d_lines[0].d_chain[1], 2);
-}
-
-void ErProofBlack::testTraceCheckParse5Lines()
-{
-  std::string tracecheckText =
-      "1 1 -2 3 0 0\n"
-      "2 -1 0 0\n"
-      "3 2 0 0\n"
-      "4 -3 0 0\n"
-      "5 0 1 2 4 3 0\n";
-  std::istringstream stream(tracecheckText);
-  TraceCheckProof pf = TraceCheckProof::fromText(stream);
-  TS_ASSERT_EQUALS(pf.d_lines.size(), 5);
-
-  TS_ASSERT_EQUALS(pf.d_lines[0].d_idx, 1);
-  TS_ASSERT_EQUALS(pf.d_lines[4].d_idx, 5);
-
-  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause.size(), 3);
-  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[0], SatLiteral(0, false));
-  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[1], SatLiteral(1, true));
-  TS_ASSERT_EQUALS(pf.d_lines[0].d_clause[2], SatLiteral(2, false));
-  TS_ASSERT_EQUALS(pf.d_lines[0].d_chain.size(), 0);
-
-  TS_ASSERT_EQUALS(pf.d_lines[4].d_chain.size(), 4);
-  TS_ASSERT_EQUALS(pf.d_lines[4].d_chain[0], 1);
-  TS_ASSERT_EQUALS(pf.d_lines[4].d_chain[1], 2);
-  TS_ASSERT_EQUALS(pf.d_lines[4].d_chain[2], 4);
-  TS_ASSERT_EQUALS(pf.d_lines[4].d_chain[3], 3);
-  TS_ASSERT_EQUALS(pf.d_lines[4].d_clause.size(), 0);
-}
-
-void ErProofBlack::testErTraceCheckParse()
-{
-  std::string tracecheckText =
-      "1  1  2 -3 0 0\n"
-      "2 -1 -2  3 0 0\n"
-      "3  2  3 -4 0 0\n"
-      "4 -2 -3  4 0 0\n"
-      "5 -1 -3 -4 0 0\n"
-      "6  1  3  4 0 0\n"
-      "7 -1  2  4 0 0\n"
-      "8  1 -2 -4 0 0\n"
-      "9 5 0 0\n"
-      "10 5 1 0 0\n"
-      "11 4 5 2 0 10 7 0\n"
-      "12 -4 5 -3 0 10 5 0\n"
-      "13 3 5 -2 0 10 2 0\n"
-      "14 -2 -4 0 2 5 8 0\n"
-      "15 4 3 0 7 2 6 0\n"
-      "16 2 -3 0 7 5 1 0\n"
-      "17 2 0 3 15 16 0\n"
-      "18 0 4 15 14 17 0\n";
-  std::istringstream stream(tracecheckText);
-  TraceCheckProof tc = TraceCheckProof::fromText(stream);
-
-  std::unordered_map<ClauseId, SatClause> clauses;
-  std::vector<ClauseId> usedIds;
-  addClause(
-      clauses,
-      usedIds,
-      1,
-      std::vector<SatLiteral>{
-          SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
-  addClause(
-      clauses,
-      usedIds,
-      2,
-      std::vector<SatLiteral>{
-          SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
-  addClause(
-      clauses,
-      usedIds,
-      3,
-      std::vector<SatLiteral>{
-          SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
-  addClause(
-      clauses,
-      usedIds,
-      4,
-      std::vector<SatLiteral>{
-          SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)});
-  addClause(clauses,
-            usedIds,
-            5,
-            std::vector<SatLiteral>{
-                SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
-  addClause(
-      clauses,
-      usedIds,
-      6,
-      std::vector<SatLiteral>{
-          SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
-  addClause(
-      clauses,
-      usedIds,
-      7,
-      std::vector<SatLiteral>{
-          SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
-  addClause(
-      clauses,
-      usedIds,
-      8,
-      std::vector<SatLiteral>{
-          SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
-  ErProof pf(clauses, usedIds, std::move(tc));
-
-  TS_ASSERT_EQUALS(pf.getInputClauseIds()[0], 1);
-  TS_ASSERT_EQUALS(pf.getInputClauseIds()[7], 8);
-
-  TS_ASSERT_EQUALS(pf.getDefinitions().size(), 1)
-  TS_ASSERT_EQUALS(pf.getDefinitions()[0].d_newVariable, SatVariable(4));
-  TS_ASSERT_EQUALS(pf.getDefinitions()[0].d_oldLiteral, SatLiteral(0, true));
-  TS_ASSERT_EQUALS(pf.getDefinitions()[0].d_otherLiterals.size(), 0);
-  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines.size(), 18);
-
-  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_idx, 1);
-  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_idx, 17);
-
-  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause.size(), 3);
-  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[0],
-                   SatLiteral(0, false));
-  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[1],
-                   SatLiteral(1, false));
-  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_clause[2],
-                   SatLiteral(2, true));
-  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[0].d_chain.size(), 0);
-
-  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_clause.size(), 1);
-  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_clause[0],
-                   SatLiteral(1, false));
-  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain.size(), 3);
-  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain[0], 3);
-  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain[1], 15);
-  TS_ASSERT_EQUALS(pf.getTraceCheckProof().d_lines[16].d_chain[2], 16);
-}
-
-void ErProofBlack::testErTraceCheckOutput()
-{
-  std::string tracecheckText =
-      "1  1  2 -3 0 0\n"
-      "2 -1 -2  3 0 0\n"
-      "3  2  3 -4 0 0\n"
-      "4 -2 -3  4 0 0\n"
-      "5 -1 -3 -4 0 0\n"
-      "6  1  3  4 0 0\n"
-      "7 -1  2  4 0 0\n"
-      "8  1 -2 -4 0 0\n"
-      "9 5 0 0\n"
-      "10 5 1 0 0\n"
-      "11 4 5 2 0 10 7 0\n"
-      "12 -4 5 -3 0 10 5 0\n"
-      "13 3 5 -2 0 10 2 0\n"
-      "14 -2 -4 0 2 5 8 0\n"
-      "15 4 3 0 7 2 6 0\n"
-      "16 2 -3 0 7 5 1 0\n"
-      "17 2 0 3 15 16 0\n"
-      "18 0 4 15 14 17 0\n";
-  std::istringstream stream(tracecheckText);
-  TraceCheckProof tc = TraceCheckProof::fromText(stream);
-
-  std::unordered_map<ClauseId, SatClause> clauses;
-  std::vector<ClauseId> usedIds;
-  addClause(
-      clauses,
-      usedIds,
-      1,
-      std::vector<SatLiteral>{
-          SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
-  addClause(
-      clauses,
-      usedIds,
-      2,
-      std::vector<SatLiteral>{
-          SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
-  addClause(
-      clauses,
-      usedIds,
-      3,
-      std::vector<SatLiteral>{
-          SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
-  addClause(
-      clauses,
-      usedIds,
-      4,
-      std::vector<SatLiteral>{
-          SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)});
-  addClause(clauses,
-            usedIds,
-            5,
-            std::vector<SatLiteral>{
-                SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
-  addClause(
-      clauses,
-      usedIds,
-      6,
-      std::vector<SatLiteral>{
-          SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
-  addClause(
-      clauses,
-      usedIds,
-      7,
-      std::vector<SatLiteral>{
-          SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
-  addClause(
-      clauses,
-      usedIds,
-      8,
-      std::vector<SatLiteral>{
-          SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
-  ErProof pf(clauses, usedIds, std::move(tc));
-
-  std::ostringstream lfsc;
-  pf.outputAsLfsc(lfsc);
-
-  std::string out = R"EOF(
-    (decl_definition
-      (neg bb.v0)
-      cln
-      (\ er.v4
-      (\ er.def4
-        (clausify_definition _ _ _ er.def4 _
-          (\ er.c9
-          (\ er.c10
-          (\ er.cnf4
-            (satlem_simplify _ _ _
-              (R _ _ er.c10 bb.pb7 bb.v0) (\ er.c11
-            (satlem_simplify _ _ _
-              (R _ _ er.c10 bb.pb5 bb.v0) (\ er.c12
-            (satlem_simplify _ _ _
-              (R _ _ er.c10 bb.pb2 bb.v0) (\ er.c13
-            (satlem_simplify _ _ _
-              (Q _ _ (R _ _ bb.pb2 bb.pb5 bb.v2) bb.pb8 bb.v0) (\ er.c14
-            (satlem_simplify _ _ _
-              (Q _ _ (R _ _ bb.pb7 bb.pb2 bb.v1) bb.pb6 bb.v0) (\ er.c15
-            (satlem_simplify _ _ _
-              (Q _ _ (R _ _ bb.pb7 bb.pb5 bb.v3) bb.pb1 bb.v0) (\ er.c16
-            (satlem_simplify _ _ _
-              (R _ _ (Q _ _ bb.pb3 er.c15 bb.v3) er.c16 bb.v2) (\ er.c17
-            (satlem_simplify _ _ _
-              (Q _ _ (R _ _ (Q _ _ bb.pb4 er.c15 bb.v2) er.c14 bb.v3)
-                  er.c17 bb.v1) (\ er.c18
-              er.c18 ; (holds cln)
-            ))))))))))))))))
-          )))
-        )
-      ))
-    )
-    )EOF";
-
-  TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()), filterWhitespace(out));
-}
-
-/**
- * This proof has been specially constructed to stress-test the proof
- * machinery, while still being short. It's a bit meandering...
- */
-void ErProofBlack::testErTraceCheckOutputMedium()
-{
-  std::string tracecheckText =
-      "1  1  2 -3 0 0\n"
-      "2 -1 -2  3 0 0\n"
-      "3  2  3 -4 0 0\n"
-      "4 -2 -3  4 0 0\n"
-      "5 -1 -3 -4 0 0\n"
-      "6  1  3  4 0 0\n"
-      "7 -1  2  4 0 0\n"
-      "8  1 -2 -4 0 0\n"
-
-      "9  5  2  4 0 0\n"  // Definition with 2 other variables
-      "10 5  1  0 0\n"
-      "11 2 -5 -1 0 0\n"
-      "12 4 -5 -1 0 0\n"
-
-      "13 6  0 0\n"  // Definition with no other variables
-      "14 6  -3  0 0\n"
-
-      "15 -3 4 0 11 1 10 7 4 0\n"  // Chain w/ both def. and input clauses
-
-      "16 -2 -4 0 2 5 8 0\n"  // The useful bit of the proof
-      "17 4 3 0 7 2 6 0\n"
-      "18 2 -3 0 7 5 1 0\n"
-      "19 2 0 3 17 18 0\n"
-      "20 0 4 17 16 19 0\n";
-
-  std::istringstream stream(tracecheckText);
-  TraceCheckProof tc = TraceCheckProof::fromText(stream);
-
-  std::unordered_map<ClauseId, SatClause> clauses;
-  std::vector<ClauseId> usedIds;
-  addClause(
-      clauses,
-      usedIds,
-      1,
-      std::vector<SatLiteral>{
-          SatLiteral(0, false), SatLiteral(1, false), SatLiteral(2, true)});
-  addClause(
-      clauses,
-      usedIds,
-      2,
-      std::vector<SatLiteral>{
-          SatLiteral(0, true), SatLiteral(1, true), SatLiteral(2, false)});
-  addClause(
-      clauses,
-      usedIds,
-      3,
-      std::vector<SatLiteral>{
-          SatLiteral(1, false), SatLiteral(2, false), SatLiteral(3, true)});
-  addClause(
-      clauses,
-      usedIds,
-      4,
-      std::vector<SatLiteral>{
-          SatLiteral(1, true), SatLiteral(2, true), SatLiteral(3, false)});
-  addClause(clauses,
-            usedIds,
-            5,
-            std::vector<SatLiteral>{
-                SatLiteral(0, true), SatLiteral(2, true), SatLiteral(3, true)});
-  addClause(
-      clauses,
-      usedIds,
-      6,
-      std::vector<SatLiteral>{
-          SatLiteral(0, false), SatLiteral(2, false), SatLiteral(3, false)});
-  addClause(
-      clauses,
-      usedIds,
-      7,
-      std::vector<SatLiteral>{
-          SatLiteral(0, true), SatLiteral(1, false), SatLiteral(3, false)});
-  addClause(
-      clauses,
-      usedIds,
-      8,
-      std::vector<SatLiteral>{
-          SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, true)});
-  ErProof pf(clauses, usedIds, std::move(tc));
-
-  std::ostringstream actual_pf_body;
-  pf.outputAsLfsc(actual_pf_body);
-
-#if IS_LFSC_BUILD
-  std::string pf_header = R"EOF(
-    (check
-      (% bb.v0 var
-      (% bb.v1 var
-      (% bb.v2 var
-      (% bb.v3 var
-        (% bb.pb1 (holds (clc (pos bb.v0) (clc (pos bb.v1) (clc (neg bb.v2) cln))))
-        (% bb.pb2 (holds (clc (neg bb.v0) (clc (neg bb.v1) (clc (pos bb.v2) cln))))
-        (% bb.pb3 (holds (clc (pos bb.v1) (clc (pos bb.v2) (clc (neg bb.v3) cln))))
-        (% bb.pb4 (holds (clc (neg bb.v1) (clc (neg bb.v2) (clc (pos bb.v3) cln))))
-        (% bb.pb5 (holds (clc (neg bb.v0) (clc (neg bb.v2) (clc (neg bb.v3) cln))))
-        (% bb.pb6 (holds (clc (pos bb.v0) (clc (pos bb.v2) (clc (pos bb.v3) cln))))
-        (% bb.pb7 (holds (clc (neg bb.v0) (clc (pos bb.v1) (clc (pos bb.v3) cln))))
-        (% bb.pb8 (holds (clc (pos bb.v0) (clc (neg bb.v1) (clc (neg bb.v3) cln))))
-          (: (holds cln)
-    )EOF";
-
-  std::string pf_footer = R"EOF(
-          )
-        ))))))))
-      ))))
-    )
-    )EOF";
-
-  std::stringstream actual_pf;
-  actual_pf << proof::plf_signatures << pf_header << actual_pf_body.str() << pf_footer;
-
-  lfscc_init();
-  lfscc_check_file(actual_pf, false, false, false, false, false, false, false);
-#endif
-}
diff --git a/test/unit/proof/lfsc_proof_printer_black.h b/test/unit/proof/lfsc_proof_printer_black.h
deleted file mode 100644
index 74fda4996..000000000
--- a/test/unit/proof/lfsc_proof_printer_black.h
+++ /dev/null
@@ -1,118 +0,0 @@
-/*********************                                                        */
-/*! \file lfsc_proof_printer_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Alex Ozdemir
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 Black box testing of LFSC proof printing
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include "proof/lfsc_proof_printer.h"
-#include "prop/sat_solver_types.h"
-#include "proof/clause_id.h"
-
-using namespace CVC4::proof;
-using namespace CVC4::prop;
-
-class LfscProofPrinterBlack : public CxxTest::TestSuite
-{
- public:
-  void setUp() override {}
-  void tearDown() override {}
-
-  void testPrintClause();
-  void testPrintSatInputProof();
-  void testPrintCMapProof();
-};
-
-void LfscProofPrinterBlack::testPrintClause()
-{
-  SatClause clause{
-      SatLiteral(0, false), SatLiteral(1, true), SatLiteral(3, false)};
-  std::ostringstream lfsc;
-
-  LFSCProofPrinter::printSatClause(clause, lfsc, "");
-
-  std::string expectedLfsc =
-      "(clc (pos .v0) "
-      "(clc (neg .v1) "
-      "(clc (pos .v3) "
-      "cln)))";
-
-  TS_ASSERT_EQUALS(lfsc.str(), expectedLfsc);
-}
-
-void LfscProofPrinterBlack::testPrintSatInputProof()
-{
-  std::vector<CVC4::ClauseId> ids{2, 40, 3};
-  std::ostringstream lfsc;
-
-  LFSCProofPrinter::printSatInputProof(ids, lfsc, "");
-
-  std::string expectedLfsc =
-      "(cnfc_proof _ _ _ .pb2 "
-      "(cnfc_proof _ _ _ .pb40 "
-      "(cnfc_proof _ _ _ .pb3 "
-      "cnfn_proof)))";
-
-  std::ostringstream lfscWithoutWhitespace;
-  for (char c : lfsc.str())
-  {
-    if (!std::isspace(c))
-    {
-      lfscWithoutWhitespace << c;
-    }
-  }
-  std::ostringstream expectedLfscWithoutWhitespace;
-  for (char c : expectedLfsc)
-  {
-    if (!std::isspace(c))
-    {
-      expectedLfscWithoutWhitespace << c;
-    }
-  }
-
-  TS_ASSERT_EQUALS(lfscWithoutWhitespace.str(),
-                   expectedLfscWithoutWhitespace.str());
-}
-
-void LfscProofPrinterBlack::testPrintCMapProof()
-{
-  std::vector<CVC4::ClauseId> ids{2, 40, 3};
-  std::ostringstream lfsc;
-
-  LFSCProofPrinter::printCMapProof(ids, lfsc, "");
-
-  std::string expectedLfsc =
-      "(CMapc_proof 1 _ _ _ .pb2 "
-      "(CMapc_proof 2 _ _ _ .pb40 "
-      "(CMapc_proof 3 _ _ _ .pb3 "
-      "CMapn_proof)))";
-
-  std::ostringstream lfscWithoutWhitespace;
-  for (char c : lfsc.str())
-  {
-    if (!std::isspace(c))
-    {
-      lfscWithoutWhitespace << c;
-    }
-  }
-  std::ostringstream expectedLfscWithoutWhitespace;
-  for (char c : expectedLfsc)
-  {
-    if (!std::isspace(c))
-    {
-      expectedLfscWithoutWhitespace << c;
-    }
-  }
-
-  TS_ASSERT_EQUALS(lfscWithoutWhitespace.str(),
-                   expectedLfscWithoutWhitespace.str());
-}
diff --git a/test/unit/proof/lrat_proof_black.h b/test/unit/proof/lrat_proof_black.h
deleted file mode 100644
index 8d91fee33..000000000
--- a/test/unit/proof/lrat_proof_black.h
+++ /dev/null
@@ -1,97 +0,0 @@
-/*********************                                                        */
-/*! \file lrat_proof_black.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Alex Ozdemir, Andres Noetzli
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 Black box testing of the LRAT proof class
- **
- ** In particular, tests LRAT LFSC output.
- **/
-
-#include <cxxtest/TestSuite.h>
-
-#include <iostream>
-
-#include "proof/lrat/lrat_proof.h"
-#include "prop/sat_solver_types.h"
-#include "utils.h"
-
-using namespace CVC4;
-using namespace CVC4::proof::lrat;
-using namespace CVC4::prop;
-
-class LratProofBlack : public CxxTest::TestSuite
-{
- public:
-  void setUp() override {}
-  void tearDown() override {}
-
-  void testOutputAsLfsc();
-};
-
-void LratProofBlack::testOutputAsLfsc()
-{
-  std::vector<std::unique_ptr<LratInstruction>> instructions;
-
-  // 6   d 1 2
-  std::vector<ClauseIdx> clausesToDelete{1, 2};
-  std::unique_ptr<LratDeletion> deletion = std::unique_ptr<LratDeletion>(
-      new LratDeletion(6, std::move(clausesToDelete)));
-  instructions.push_back(std::move(deletion));
-
-  // 7   1 2 0  5 2 0
-  std::vector<SatLiteral> firstAddedClause{SatLiteral(1, false),
-                                           SatLiteral(2, false)};
-  LratUPTrace firstTrace{5, 2};
-  std::vector<std::pair<ClauseIdx, LratUPTrace>> firstHints;
-  std::unique_ptr<LratAddition> add1 =
-      std::unique_ptr<LratAddition>(new LratAddition(
-          7, std::move(firstAddedClause), std::move(firstTrace), firstHints));
-  instructions.push_back(std::move(add1));
-
-  // 8   2 0  -1 3  -5 2 0
-  std::vector<SatLiteral> secondAddedClause{SatLiteral(2, false)};
-  LratUPTrace secondTrace;
-  std::vector<std::pair<ClauseIdx, LratUPTrace>> secondHints;
-  LratUPTrace secondHints0Trace{3};
-  secondHints.emplace_back(1, secondHints0Trace);
-  LratUPTrace secondHints1Trace{2};
-  secondHints.emplace_back(5, secondHints1Trace);
-  std::unique_ptr<LratAddition> add2 = std::unique_ptr<LratAddition>(
-      new LratAddition(8,
-                       std::move(secondAddedClause),
-                       std::move(secondTrace),
-                       secondHints));
-  instructions.push_back(std::move(add2));
-
-  LratProof proof(std::move(instructions));
-
-  std::ostringstream lfsc;
-  proof.outputAsLfsc(lfsc);
-
-  // 6   d 1 2
-  // 7   1 2 0  5 2 0
-  // 8   2 0  -1 3  -5 2 0
-  std::string expectedLfsc =
-      "(LRATProofd (CIListc 1 (CIListc 2 CIListn)) "
-      "(LRATProofa 7 "
-      "  (clc (pos bb.v1) (clc (pos bb.v2) cln))"
-      "  (Tracec 5 (Tracec 2 Tracen))"
-      "  RATHintsn "
-      "(LRATProofa 8 "
-      "  (clc (pos bb.v2) cln)"
-      "  Tracen "
-      "  (RATHintsc 1 (Tracec 3 Tracen)"
-      "    (RATHintsc 5 (Tracec 2 Tracen)"
-      "    RATHintsn)) "
-      "LRATProofn)))";
-
-  TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()),
-                   filterWhitespace(expectedLfsc));
-}
diff --git a/test/unit/proof/utils.h b/test/unit/proof/utils.h
deleted file mode 100644
index 3db6e2171..000000000
--- a/test/unit/proof/utils.h
+++ /dev/null
@@ -1,34 +0,0 @@
-/*********************                                                        */
-/*! \file utils.h
- ** \verbatim
- ** Top contributors (to current version):
- **   Alex Ozdemir
- ** This file is part of the CVC4 project.
- ** Copyright (c) 2009-2020 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 Utilities for proof testing
- **/
-
-#include <algorithm>
-#include <string>
-#include <cctype>
-#include <iterator>
-
-/**
- * Creates a new stream with whitespace removed.
- *
- * @param s the source string
- *
- * @return a string without whitespace
- */
-std::string filterWhitespace(const std::string& s)
-{
-  std::string out;
-  std::copy_if(s.cbegin(), s.cend(), std::inserter(out, out.end()), [](char c) {
-    return !std::isspace(c);
-  });
-  return out;
-}
diff --git a/test/unit/prop/cnf_stream_white.h b/test/unit/prop/cnf_stream_white.h
index f0253fdbf..33fc15674 100644
--- a/test/unit/prop/cnf_stream_white.h
+++ b/test/unit/prop/cnf_stream_white.h
@@ -174,8 +174,8 @@ class CnfStreamWhite : public CxxTest::TestSuite {
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::AND, a, b, c),
-                                  false, false, RULE_INVALID, Node::null());
+    d_cnfStream->convertAndAssert(
+        d_nodeManager->mkNode(kind::AND, a, b, c), false, false);
     TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
@@ -189,26 +189,27 @@ class CnfStreamWhite : public CxxTest::TestSuite {
     Node f = d_nodeManager->mkVar(d_nodeManager->booleanType());
     d_cnfStream->convertAndAssert(
         d_nodeManager->mkNode(
-            kind::IMPLIES, d_nodeManager->mkNode(kind::AND, a, b),
+            kind::IMPLIES,
+            d_nodeManager->mkNode(kind::AND, a, b),
             d_nodeManager->mkNode(
-                kind::EQUAL, d_nodeManager->mkNode(kind::OR, c, d),
+                kind::EQUAL,
+                d_nodeManager->mkNode(kind::OR, c, d),
                 d_nodeManager->mkNode(kind::NOT,
                                       d_nodeManager->mkNode(kind::XOR, e, f)))),
-        false, false, RULE_INVALID, Node::null());
+        false,
+        false);
     TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
   void testTrue() {
     NodeManagerScope nms(d_nodeManager);
-    d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false,
-                                  RULE_INVALID, Node::null());
+    d_cnfStream->convertAndAssert(d_nodeManager->mkConst(true), false, false);
     TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
   void testFalse() {
     NodeManagerScope nms(d_nodeManager);
-    d_cnfStream->convertAndAssert(d_nodeManager->mkConst(false), false, false,
-                                  RULE_INVALID, Node::null());
+    d_cnfStream->convertAndAssert(d_nodeManager->mkConst(false), false, false);
     TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
@@ -216,8 +217,8 @@ class CnfStreamWhite : public CxxTest::TestSuite {
     NodeManagerScope nms(d_nodeManager);
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::EQUAL, a, b), false,
-                                  false, RULE_INVALID, Node::null());
+    d_cnfStream->convertAndAssert(
+        d_nodeManager->mkNode(kind::EQUAL, a, b), false, false);
     TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
@@ -225,33 +226,16 @@ class CnfStreamWhite : public CxxTest::TestSuite {
     NodeManagerScope nms(d_nodeManager);
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::IMPLIES, a, b),
-                                  false, false, RULE_INVALID, Node::null());
+    d_cnfStream->convertAndAssert(
+        d_nodeManager->mkNode(kind::IMPLIES, a, b), false, false);
     TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
-  // ITEs should be removed before going to CNF
-  // void testIte() {
-  //  NodeManagerScope nms(d_nodeManager);
-  //  d_cnfStream->convertAndAssert(
-  //      d_nodeManager->mkNode(
-  //          kind::EQUAL,
-  //          d_nodeManager->mkNode(
-  //              kind::ITE,
-  //              d_nodeManager->mkVar(d_nodeManager->booleanType()),
-  //              d_nodeManager->mkVar(d_nodeManager->integerType()),
-  //              d_nodeManager->mkVar(d_nodeManager->integerType())
-  //          ),
-  //          d_nodeManager->mkVar(d_nodeManager->integerType())
-  //                            ), false, false, RULE_INVALID, Node::null());
-  //
-  //}
-
   void testNot() {
     NodeManagerScope nms(d_nodeManager);
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::NOT, a), false,
-                                  false, RULE_INVALID, Node::null());
+    d_cnfStream->convertAndAssert(
+        d_nodeManager->mkNode(kind::NOT, a), false, false);
     TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
@@ -260,8 +244,8 @@ class CnfStreamWhite : public CxxTest::TestSuite {
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node c = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::OR, a, b, c),
-                                  false, false, RULE_INVALID, Node::null());
+    d_cnfStream->convertAndAssert(
+        d_nodeManager->mkNode(kind::OR, a, b, c), false, false);
     TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
@@ -269,10 +253,10 @@ class CnfStreamWhite : public CxxTest::TestSuite {
     NodeManagerScope nms(d_nodeManager);
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(a, false, false, RULE_INVALID, Node::null());
+    d_cnfStream->convertAndAssert(a, false, false);
     TS_ASSERT(d_satSolver->addClauseCalled());
     d_satSolver->reset();
-    d_cnfStream->convertAndAssert(b, false, false, RULE_INVALID, Node::null());
+    d_cnfStream->convertAndAssert(b, false, false);
     TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
@@ -280,8 +264,8 @@ class CnfStreamWhite : public CxxTest::TestSuite {
     NodeManagerScope nms(d_nodeManager);
     Node a = d_nodeManager->mkVar(d_nodeManager->booleanType());
     Node b = d_nodeManager->mkVar(d_nodeManager->booleanType());
-    d_cnfStream->convertAndAssert(d_nodeManager->mkNode(kind::XOR, a, b), false,
-                                  false, RULE_INVALID, Node::null());
+    d_cnfStream->convertAndAssert(
+        d_nodeManager->mkNode(kind::XOR, a, b), false, false);
     TS_ASSERT(d_satSolver->addClauseCalled());
   }
 
diff --git a/test/unit/theory/theory_engine_white.h b/test/unit/theory/theory_engine_white.h
index a67d0aeb2..ae4264aa2 100644
--- a/test/unit/theory/theory_engine_white.h
+++ b/test/unit/theory/theory_engine_white.h
@@ -41,7 +41,6 @@
 #include "theory/theory_rewriter.h"
 #include "theory/valuation.h"
 #include "util/integer.h"
-#include "util/proof.h"
 #include "util/rational.h"
 
 using namespace CVC4;
@@ -55,13 +54,9 @@ using namespace CVC4::theory::bv;
 using namespace std;
 
 class FakeOutputChannel : public OutputChannel {
-  void conflict(TNode n, std::unique_ptr<Proof> pf) override
-  {
-    Unimplemented();
-  }
+  void conflict(TNode n) override { Unimplemented(); }
   bool propagate(TNode n) override { Unimplemented(); }
   LemmaStatus lemma(TNode n,
-                    ProofRule rule,
                     LemmaProperty p = LemmaProperty::NONE) override
   {
     Unimplemented();
diff --git a/test/unit/theory/theory_white.h b/test/unit/theory/theory_white.h
index 9693000a3..e90bd56a2 100644
--- a/test/unit/theory/theory_white.h
+++ b/test/unit/theory/theory_white.h
@@ -26,7 +26,6 @@
 #include "smt/smt_engine_scope.h"
 #include "theory/theory.h"
 #include "theory/theory_engine.h"
-#include "util/proof.h"
 #include "util/resource_manager.h"
 
 using namespace CVC4;
@@ -48,10 +47,7 @@ class TestOutputChannel : public OutputChannel {
   ~TestOutputChannel() override {}
 
   void safePoint(ResourceManager::Resource r) override {}
-  void conflict(TNode n, std::unique_ptr<Proof> pf) override
-  {
-    push(CONFLICT, n);
-  }
+  void conflict(TNode n) override { push(CONFLICT, n); }
 
   bool propagate(TNode n) override {
     push(PROPAGATE, n);
@@ -59,7 +55,6 @@ class TestOutputChannel : public OutputChannel {
   }
 
   LemmaStatus lemma(TNode n,
-                    ProofRule rule,
                     LemmaProperty p = LemmaProperty::NONE) override
   {
     push(LEMMA, n);
@@ -298,7 +293,7 @@ class TheoryBlack : public CxxTest::TestSuite {
 
   void testOutputChannel() {
     Node n = atom0.orNode(atom1);
-    d_outputChannel.lemma(n, RULE_INVALID);
+    d_outputChannel.lemma(n);
     d_outputChannel.split(atom0);
     Node s = atom0.orNode(atom0.notNode());
     TS_ASSERT_EQUALS(d_outputChannel.d_callHistory.size(), 2u);