[Regressions] Fix regression issues related to BV proofs (#5029)

diff --git a/test/regress/regress0/bv/ackermann2.smt2 b/test/regress/regress0/bv/ackermann2.smt2
index 3b50b025dc4c9d8f86526b2701a09382352498e0..518faf597d9b3b1d94ea0438eb3de9d83cb49bb3 100644 (file)
--- a/test/regress/regress0/bv/ackermann2.smt2
+++ b/test/regress/regress0/bv/ackermann2.smt2
@@ -1,9 +1,7 @@
 ; 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 --no-check-unsat-cores
-; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=drat --no-check-unsat-cores
-; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=er --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --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.smtv1.smt2 b/test/regress/regress0/bv/core/slice-12.smtv1.smt2
index 3e26d9f185d42ec738c4799354c54f098c01ddd3..d66b27caa324d29353caef3c3009c87cb5145ed6 100644 (file)
--- a/test/regress/regress0/bv/core/slice-12.smtv1.smt2
+++ b/test/regress/regress0/bv/core/slice-12.smtv1.smt2
@@ -1,8 +1,6 @@
 ; REQUIRES: cryptominisat
 ; REQUIRES: drat2er
-; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=lrat --no-check-unsat-cores
-; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=drat --no-check-unsat-cores
-; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --bv-proof-format=er --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --bv-sat-solver=cryptominisat --no-check-unsat-cores
 ; EXPECT: unsat
 (set-option :incremental false)
 (set-info :status unsat)

diff --git a/test/regress/regress1/sygus-abduct-test-user.smt2 b/test/regress/regress1/sygus-abduct-test-user.smt2
index fed9bd2a6d2c9587c6379756c0435986a79238ed..ed1d5c8625f4301d4d60ff5bc9c6d2b846c19fe4 100644 (file)
--- a/test/regress/regress1/sygus-abduct-test-user.smt2
+++ b/test/regress/regress1/sygus-abduct-test-user.smt2
@@ -1,4 +1,4 @@
-; REQUIRES: proofs
+; REQUIRES: proof
 ; COMMAND-LINE: --produce-abducts
 ; COMMAND-LINE: --produce-abducts --sygus-core-connective
 ; SCRUBBER: grep -v -E '(\(define-fun)'