5 files changed, 15 insertions, 3 deletions
diff --git a/test/regress/regress0/bv/ackermann2.smt2 b/test/regress/regress0/bv/ackermann2.smt2
index b1aaa7d64..1799df63c 100644
--- a/test/regress/regress0/bv/ackermann2.smt2
+++ b/test/regress/regress0/bv/ackermann2.smt2
@@ -1,4 +1,9 @@
 ; COMMAND-LINE: --bitblast=eager --no-check-models  --no-check-unsat-cores
+; REQUIRES: cryptominisat
+; REQUIRES: drat2er
+; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=lrat --check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=drat --check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=er --check-proofs --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_UFBV)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/bv/core/slice-12.smt b/test/regress/regress0/bv/core/slice-12.smt
index 998dee663..261d55ec9 100644
--- a/test/regress/regress0/bv/core/slice-12.smt
+++ b/test/regress/regress0/bv/core/slice-12.smt
@@ -1,3 +1,9 @@
+; REQUIRES: cryptominisat
+; REQUIRES: drat2er
+; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=lrat --check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=drat --check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=er --check-proofs --no-check-unsat-cores
+; EXPECT: unsat
 (benchmark slice
   :status unsat
   :logic QF_BV
diff --git a/test/regress/regress0/bv/temp.lrat b/test/regress/regress0/bv/temp.lrat
new file mode 100644
index 000000000..e69de29bb
--- /dev/null
+++ b/test/regress/regress0/bv/temp.lrat
diff --git a/test/unit/proof/drat_proof_black.h b/test/unit/proof/drat_proof_black.h
index 946597bea..2859d0682 100644
--- a/test/unit/proof/drat_proof_black.h
+++ b/test/unit/proof/drat_proof_black.h
@@ -170,8 +170,8 @@ void DratProofBlack::testOutputTwoAsLfsc()
     }
   }
   std::string expectedLfsc =
-      "(DRATProofd (clc (neg .v62)  (clc (neg .v8192) cln))"
-      "(DRATProofa (clc (pos .v128) (clc (neg .v8190) cln))"
+      "(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)
diff --git a/test/unit/proof/lrat_proof_black.h b/test/unit/proof/lrat_proof_black.h
index 48f571841..398c551fe 100644
--- a/test/unit/proof/lrat_proof_black.h
+++ b/test/unit/proof/lrat_proof_black.h
@@ -91,5 +91,6 @@ void LfscProofBlack::testOutputAsLfsc()
       "    RATHintsn)) "
       "LRATProofn)))";
 
-  TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()), filterWhitespace(expectedLfsc));
+  TS_ASSERT_EQUALS(filterWhitespace(lfsc.str()),
+                   filterWhitespace(expectedLfsc));
 }