[Regressions] Do not test `--check-proofs` anymore (#4914)

In preparation of removing the old proof module, this commit changes the
regression runner to not add the flag --check-proofs anymore when
running the regressions.

20 files changed, 24 insertions, 97 deletions

diff --git a/test/regress/regress0/bv/ackermann2.smt2 b/test/regress/regress0/bv/ackermann2.smt2
index 1799df63c..3b50b025d 100644
--- a/test/regress/regress0/bv/ackermann2.smt2
+++ b/test/regress/regress0/bv/ackermann2.smt2
@@ -1,9 +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
+; 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
 ; EXPECT: unsat
 (set-logic QF_UFBV)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/bv/ackermann3.smt2 b/test/regress/regress0/bv/ackermann3.smt2
index 8e47c8840..ec3efeedd 100644
--- a/test/regress/regress0/bv/ackermann3.smt2
+++ b/test/regress/regress0/bv/ackermann3.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_ABV)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/bv/ackermann4.smt2 b/test/regress/regress0/bv/ackermann4.smt2
index 0c1e323d5..05ffef452 100644
--- a/test/regress/regress0/bv/ackermann4.smt2
+++ b/test/regress/regress0/bv/ackermann4.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --bitblast=eager --no-check-models --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_UFBV)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/bv/ackermann5.smt2 b/test/regress/regress0/bv/ackermann5.smt2
index d29311109..240691cd3 100644
--- a/test/regress/regress0/bv/ackermann5.smt2
+++ b/test/regress/regress0/bv/ackermann5.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_UFBV)
 
diff --git a/test/regress/regress0/bv/ackermann6.smt2 b/test/regress/regress0/bv/ackermann6.smt2
index 846339f52..20e0c638c 100644
--- a/test/regress/regress0/bv/ackermann6.smt2
+++ b/test/regress/regress0/bv/ackermann6.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_UFBV)
 
diff --git a/test/regress/regress0/bv/ackermann7.smt2 b/test/regress/regress0/bv/ackermann7.smt2
index 174ad747a..3b901d552 100644
--- a/test/regress/regress0/bv/ackermann7.smt2
+++ b/test/regress/regress0/bv/ackermann7.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores
 ; EXPECT: sat
 (set-logic QF_UFBV)
 
diff --git a/test/regress/regress0/bv/ackermann8.smt2 b/test/regress/regress0/bv/ackermann8.smt2
index 2a424e085..91c13b056 100644
--- a/test/regress/regress0/bv/ackermann8.smt2
+++ b/test/regress/regress0/bv/ackermann8.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --ackermann --no-check-models --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_UFBV)
 
diff --git a/test/regress/regress0/bv/bv-int-collapse1.smt2 b/test/regress/regress0/bv/bv-int-collapse1.smt2
index 5b631a7fd..942cdffde 100644
--- a/test/regress/regress0/bv/bv-int-collapse1.smt2
+++ b/test/regress/regress0/bv/bv-int-collapse1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
diff --git a/test/regress/regress0/bv/bv-int-collapse2.smt2 b/test/regress/regress0/bv/bv-int-collapse2.smt2
index a630049cb..65c9d2673 100644
--- a/test/regress/regress0/bv/bv-int-collapse2.smt2
+++ b/test/regress/regress0/bv/bv-int-collapse2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic ALL_SUPPORTED)
 (set-info :status unsat)
diff --git a/test/regress/regress0/bv/bv-options1.smt2 b/test/regress/regress0/bv/bv-options1.smt2
deleted file mode 100644
index b1e87fc7e..000000000
--- a/test/regress/regress0/bv/bv-options1.smt2
+++ /dev/null
@@ -1,24 +0,0 @@
-; SCRUBBER: sed -e 's/(error \"Error.in.option.parsing.*$/Error in option parsing/'
-; EXPECT: Error in option parsing
-; COMMAND-LINE: --check-proofs --bv-algebraic-solver
-; EXIT: 1
-(set-logic QF_BV)
-(set-info :smt-lib-version 2.0)
-(set-info :category "crafted")
-(declare-fun v0 () (_ BitVec 16))
-(declare-fun v1 () (_ BitVec 16))
-(declare-fun v2 () (_ BitVec 16))
-(declare-fun v3 () (_ BitVec 16))
-(declare-fun v4 () (_ BitVec 16))
-(declare-fun v5 () (_ BitVec 16))
-(assert (and
-	 (bvult v2 v4)
-	 (bvult v3 v4)
-	 (bvult v0 v1)
-	 (bvult v1 v2)
-	 (bvult v1 v3)
-	 (bvult v4 v5)
-	 (bvult v5 v1)
-	 ))
-(check-sat)
-(exit)
diff --git a/test/regress/regress0/bv/bv-options2.smt2 b/test/regress/regress0/bv/bv-options2.smt2
deleted file mode 100644
index d1ee44084..000000000
--- a/test/regress/regress0/bv/bv-options2.smt2
+++ /dev/null
@@ -1,24 +0,0 @@
-; SCRUBBER: sed -e 's/(error \"Error.in.option.parsing.*$/Error in option parsing/'
-; EXPECT: Error in option parsing
-; COMMAND-LINE: --check-proofs --bv-eq-solver
-; EXIT: 1
-(set-logic QF_BV)
-(set-info :smt-lib-version 2.0)
-(set-info :category "crafted")
-(declare-fun v0 () (_ BitVec 16))
-(declare-fun v1 () (_ BitVec 16))
-(declare-fun v2 () (_ BitVec 16))
-(declare-fun v3 () (_ BitVec 16))
-(declare-fun v4 () (_ BitVec 16))
-(declare-fun v5 () (_ BitVec 16))
-(assert (and
-	 (bvult v2 v4)
-	 (bvult v3 v4)
-	 (bvult v0 v1)
-	 (bvult v1 v2)
-	 (bvult v1 v3)
-	 (bvult v4 v5)
-	 (bvult v5 v1)
-	 ))
-(check-sat)
-(exit)
diff --git a/test/regress/regress0/bv/bv-options3.smt2 b/test/regress/regress0/bv/bv-options3.smt2
deleted file mode 100644
index 4d16230b4..000000000
--- a/test/regress/regress0/bv/bv-options3.smt2
+++ /dev/null
@@ -1,24 +0,0 @@
-; SCRUBBER: sed -e 's/(error \"Error.in.option.parsing.*$/Error in option parsing/'
-; EXPECT: Error in option parsing
-; COMMAND-LINE: --check-proofs --bv-inequality-solver
-; EXIT: 1
-(set-logic QF_BV)
-(set-info :smt-lib-version 2.0)
-(set-info :category "crafted")
-(declare-fun v0 () (_ BitVec 16))
-(declare-fun v1 () (_ BitVec 16))
-(declare-fun v2 () (_ BitVec 16))
-(declare-fun v3 () (_ BitVec 16))
-(declare-fun v4 () (_ BitVec 16))
-(declare-fun v5 () (_ BitVec 16))
-(assert (and
-	 (bvult v2 v4)
-	 (bvult v3 v4)
-	 (bvult v0 v1)
-	 (bvult v1 v2)
-	 (bvult v1 v3)
-	 (bvult v4 v5)
-	 (bvult v5 v1)
-	 ))
-(check-sat)
-(exit)
diff --git a/test/regress/regress0/bv/bv-options4.smt2 b/test/regress/regress0/bv/bv-options4.smt2
index 842650ebd..b7a78e3b5 100644
--- a/test/regress/regress0/bv/bv-options4.smt2
+++ b/test/regress/regress0/bv/bv-options4.smt2
@@ -1,6 +1,5 @@
 ; SCRUBBER: sed -e 's/unsat.*/unsat/'
 ; EXPECT: unsat
-; COMMAND-LINE: --check-proofs 
 ; EXIT: 0
 (set-logic QF_BV)
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/bv/bv_to_int1.smt2 b/test/regress/regress0/bv/bv_to_int1.smt2
index d9190128e..f812ccbc8 100644
--- a/test/regress/regress0/bv/bv_to_int1.smt2
+++ b/test/regress/regress0/bv/bv_to_int1.smt2
@@ -1,7 +1,7 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores --no-check-proofs 
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-models  --no-check-unsat-cores --no-check-proofs
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-models  --no-check-unsat-cores --no-check-proofs
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=2 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=3 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=4 --no-check-models  --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun x () (_ BitVec 4))
diff --git a/test/regress/regress0/bv/bv_to_int_bitwise.smt2 b/test/regress/regress0/bv/bv_to_int_bitwise.smt2
index 4bcbac20c..6f08c2e8d 100644
--- a/test/regress/regress0/bv/bv_to_int_bitwise.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bitwise.smt2
@@ -1,5 +1,5 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=5 --no-check-models  --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun s () (_ BitVec 4))
diff --git a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2 b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
index 05cd312d7..4e940b5df 100644
--- a/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
+++ b/test/regress/regress0/bv/bv_to_int_bvmul2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun T4_180 () (_ BitVec 32))
diff --git a/test/regress/regress0/bv/bv_to_int_zext.smt2 b/test/regress/regress0/bv/bv_to_int_zext.smt2
index 5c6be19b5..ab09d7341 100644
--- a/test/regress/regress0/bv/bv_to_int_zext.smt2
+++ b/test/regress/regress0/bv/bv_to_int_zext.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-check-models  --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun T1_31078 () (_ BitVec 8))
diff --git a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2 b/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2
index 3db8e87ee..6196b2bb9 100644
--- a/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2
+++ b/test/regress/regress0/bv/bvuf_to_intuf_smtlib.smt2
@@ -1,4 +1,4 @@
-;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-models --no-produce-unsat-cores --no-check-proofs
+;COMMAND-LINE: --solve-bv-as-int=sum --bvand-integer-granularity=1 --no-produce-models --no-produce-unsat-cores
 ;EXPECT: unsat
 
 (set-logic QF_UFBV)
diff --git a/test/regress/regress0/bv/core/slice-12.smtv1.smt2 b/test/regress/regress0/bv/core/slice-12.smtv1.smt2
index 90c01500d..3e26d9f18 100644
--- a/test/regress/regress0/bv/core/slice-12.smtv1.smt2
+++ b/test/regress/regress0/bv/core/slice-12.smtv1.smt2
@@ -1,8 +1,8 @@
 ; 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
+; 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
 ; EXPECT: unsat
 (set-option :incremental false)
 (set-info :status unsat)
diff --git a/test/regress/regress0/bv/test-bv_intro_pow2.smt2 b/test/regress/regress0/bv/test-bv_intro_pow2.smt2
index 96779d3a6..465937b28 100644
--- a/test/regress/regress0/bv/test-bv_intro_pow2.smt2
+++ b/test/regress/regress0/bv/test-bv_intro_pow2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --bv-intro-pow2 --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --bv-intro-pow2 --no-check-unsat-cores
 (set-info :smt-lib-version 2.6)
 (set-logic QF_BV)
 (set-info :status unsat)