[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.

53 files changed, 44 insertions, 169 deletions

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8ca9d74c3..870d83e7e 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -205,9 +205,6 @@ set(regress_0_tests
   regress0/bv/bv-abstr-bug2.smt2
   regress0/bv/bv-int-collapse1.smt2
   regress0/bv/bv-int-collapse2.smt2
-  regress0/bv/bv-options1.smt2
-  regress0/bv/bv-options2.smt2
-  regress0/bv/bv-options3.smt2
   regress0/bv/bv-options4.smt2
   regress0/bv/bv-to-bool1.smtv1.smt2
   regress0/bv/bv-to-bool2.smt2
@@ -681,7 +678,6 @@ set(regress_0_tests
   regress0/printer/let_shadowing.smt2
   regress0/printer/symbol_starting_w_digit.smt2
   regress0/printer/tuples_and_records.cvc
-  regress0/proof_no_support.smt2
   regress0/push-pop/boolean/fuzz_12.smt2
   regress0/push-pop/boolean/fuzz_13.smt2
   regress0/push-pop/boolean/fuzz_14.smt2
diff --git a/test/regress/regress0/arith/ite-lift.smt2 b/test/regress/regress0/arith/ite-lift.smt2
index bd2df3def..62fd4a745 100644
--- a/test/regress/regress0/arith/ite-lift.smt2
+++ b/test/regress/regress0/arith/ite-lift.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --check-proofs
 (set-option :incremental false)
 (set-info :status unsat)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/arrays/incorrect10.smtv1.smt2 b/test/regress/regress0/arrays/incorrect10.smtv1.smt2
index ea68f654a..3d51eddb9 100644
--- a/test/regress/regress0/arrays/incorrect10.smtv1.smt2
+++ b/test/regress/regress0/arrays/incorrect10.smtv1.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-proofs
 ; EXPECT: unsat
 (set-option :incremental false)
 (set-info :status unsat)
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)
diff --git a/test/regress/regress0/datatypes/empty_tuprec.cvc b/test/regress/regress0/datatypes/empty_tuprec.cvc
index b6950845e..185f7eca8 100644
--- a/test/regress/regress0/datatypes/empty_tuprec.cvc
+++ b/test/regress/regress0/datatypes/empty_tuprec.cvc
@@ -1,4 +1,4 @@
-% COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
+% COMMAND-LINE: --no-check-unsat-cores
 %
 OPTION "incremental";
 
diff --git a/test/regress/regress0/fmf/sort-infer-typed-082718.smt2 b/test/regress/regress0/fmf/sort-infer-typed-082718.smt2
index 6d026ff5b..9ee1fa5eb 100644
--- a/test/regress/regress0/fmf/sort-infer-typed-082718.smt2
+++ b/test/regress/regress0/fmf/sort-infer-typed-082718.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --sort-inference --finite-model-find --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --sort-inference --finite-model-find --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic ALL)
 (assert (not (exists ((X Int)) (not (= X 12)) )))
diff --git a/test/regress/regress0/get-value-ints.smt2 b/test/regress/regress0/get-value-ints.smt2
index 4497b7a80..97d8d1176 100644
--- a/test/regress/regress0/get-value-ints.smt2
+++ b/test/regress/regress0/get-value-ints.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE:
 ; EXPECT: sat
 ; EXPECT: ((pos 1) (zero 0) (neg (- 6)))
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/get-value-reals-ints.smt2 b/test/regress/regress0/get-value-reals-ints.smt2
index 8dec35073..b75f535d5 100644
--- a/test/regress/regress0/get-value-reals-ints.smt2
+++ b/test/regress/regress0/get-value-reals-ints.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE:
 ; EXPECT: sat
 ; EXPECT: ((pos_int 5) (pos_real_int_value (/ 3 1)) (pos_rat (/ 1 3)) (zero (/ 0 1)) (neg_rat (/ (- 2) 3)) (neg_real_int_value (/ (- 2) 1)) (neg_int (- 6)))
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/get-value-reals.smt2 b/test/regress/regress0/get-value-reals.smt2
index 6fa542668..09ec0917f 100644
--- a/test/regress/regress0/get-value-reals.smt2
+++ b/test/regress/regress0/get-value-reals.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE:
 ; EXPECT: sat
 ; EXPECT: ((pos_int (/ 3 1)) (pos_rat (/ 1 3)) (zero (/ 0 1)) (neg_rat (/ (- 2) 3)) (neg_int (/ (- 2) 1)))
 (set-info :smt-lib-version 2.0)
diff --git a/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smtv1.smt2 b/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smtv1.smt2
index 8101dfdeb..e43cc6e7e 100644
--- a/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smtv1.smt2
+++ b/test/regress/regress0/lemmas/sc_init_frame_gap.induction.smtv1.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE:
 (set-option :incremental false)
 (set-info :source "The Formal Verification of a Reintegration Protocol. Author: Lee Pike. Website: http://www.cs.indiana.edu/~lepike/pub_pages/emsoft.html.
 
diff --git a/test/regress/regress0/printer/bv_consts_bin.smt2 b/test/regress/regress0/printer/bv_consts_bin.smt2
index f910c2c96..e56c372fa 100644
--- a/test/regress/regress0/printer/bv_consts_bin.smt2
+++ b/test/regress/regress0/printer/bv_consts_bin.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE:
 ; EXPECT: sat
 ; EXPECT: ((x #b0001))
 (set-option :produce-models true)
diff --git a/test/regress/regress0/proof_no_support.smt2 b/test/regress/regress0/proof_no_support.smt2
deleted file mode 100644
index 3d19a109e..000000000
--- a/test/regress/regress0/proof_no_support.smt2
+++ /dev/null
@@ -1,21 +0,0 @@
-;COMMAND-LINE: --check-proofs
-;EXIT: 1
-;EXPECT: (error "Error in option parsing: Proofs are only supported for sub-logics of QF_AUFBVLIA.")
-(set-logic ALL)
-
-(declare-const a Int)
-
-(assert (and 
-          (=
-            a
-            (* a a)
-          )
-          (not (= a 0))
-          (not (= a 1))
-        )
-)
-
-(check-sat)
-
-
-
diff --git a/test/regress/regress0/quantifiers/lra-triv-gn.smt2 b/test/regress/regress0/quantifiers/lra-triv-gn.smt2
index 1598f7097..7cc9c2ea3 100644
--- a/test/regress/regress0/quantifiers/lra-triv-gn.smt2
+++ b/test/regress/regress0/quantifiers/lra-triv-gn.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --global-negate --no-check-unsat-cores --no-check-proofs
+; COMMAND-LINE: --global-negate --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic LRA)
 (set-info :status unsat)
diff --git a/test/regress/regress0/uflra/constants0.smtv1.smt2 b/test/regress/regress0/uflra/constants0.smtv1.smt2
index a692a7c4d..b87c92352 100644
--- a/test/regress/regress0/uflra/constants0.smtv1.smt2
+++ b/test/regress/regress0/uflra/constants0.smtv1.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-proofs
 (set-option :incremental false)
 (set-info :status unsat)
 (set-info :category "crafted")
diff --git a/test/regress/regress0/uflra/pb_real_10_0200_10_22.smtv1.smt2 b/test/regress/regress0/uflra/pb_real_10_0200_10_22.smtv1.smt2
index fd9d3f9c6..6c48006f9 100644
--- a/test/regress/regress0/uflra/pb_real_10_0200_10_22.smtv1.smt2
+++ b/test/regress/regress0/uflra/pb_real_10_0200_10_22.smtv1.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-proofs
 (set-option :incremental false)
 (set-info :source "MathSat group")
 (set-info :status unsat)
diff --git a/test/regress/regress0/uflra/pb_real_10_0200_10_26.smtv1.smt2 b/test/regress/regress0/uflra/pb_real_10_0200_10_26.smtv1.smt2
index 3d89b719e..6626a0c6f 100644
--- a/test/regress/regress0/uflra/pb_real_10_0200_10_26.smtv1.smt2
+++ b/test/regress/regress0/uflra/pb_real_10_0200_10_26.smtv1.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-proofs
 (set-option :incremental false)
 (set-info :source "MathSat group")
 (set-info :status unsat)
diff --git a/test/regress/regress1/bv/bv2nat-ground.smt2 b/test/regress/regress1/bv/bv2nat-ground.smt2
index bfc22850e..9d26a06ed 100644
--- a/test/regress/regress1/bv/bv2nat-ground.smt2
+++ b/test/regress/regress1/bv/bv2nat-ground.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BVLIA)
 (set-info :status unsat)
diff --git a/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2 b/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2
index 37accd35b..fd621171c 100644
--- a/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2
+++ b/test/regress/regress1/decision/quant-symmetric_unsat_7.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores --decision=justification
+; COMMAND-LINE: --no-check-unsat-cores --decision=justification
 ; EXPECT: unsat
 
 (set-logic AUFLIRA)
diff --git a/test/regress/regress1/fmf/PUZ001+1.smt2 b/test/regress/regress1/fmf/PUZ001+1.smt2
index f3db78491..607a79f0d 100644
--- a/test/regress/regress1/fmf/PUZ001+1.smt2
+++ b/test/regress/regress1/fmf/PUZ001+1.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --finite-model-find --no-check-proofs --no-check-unsat-core
+; COMMAND-LINE: --finite-model-find --no-check-unsat-core
 ; EXPECT: unsat
 ;%------------------------------------------------------------------------------
 ;% File     : PUZ001+1 : TPTP v5.4.0. Released v2.0.0.
diff --git a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2 b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2
index 731fd4431..edb55d756 100644
--- a/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2
+++ b/test/regress/regress1/ho/nested_lambdas-AGT034^2.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --uf-ho --no-check-unsat-cores --no-check-proofs --no-produce-models
+; COMMAND-LINE: --uf-ho --no-check-unsat-cores --no-produce-models
 ; EXPECT: unsat
 
 (set-logic ALL)
diff --git a/test/regress/regress1/lemmas/pursuit-safety-8.smtv1.smt2 b/test/regress/regress1/lemmas/pursuit-safety-8.smtv1.smt2
index 6187be7c1..a936046a5 100644
--- a/test/regress/regress1/lemmas/pursuit-safety-8.smtv1.smt2
+++ b/test/regress/regress1/lemmas/pursuit-safety-8.smtv1.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE:
 (set-option :incremental false)
 (set-info :source "SAL benchmark suite.  Created at SRI by Bruno Dutertre, John Rushby, Maria
 Sorea, and Leonardo de Moura.  Contact demoura@csl.sri.com for more
diff --git a/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2 b/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
index 4aa162f5b..038b63019 100644
--- a/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
+++ b/test/regress/regress1/lemmas/simple_startup_9nodes.abstract.base.smtv1.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE:
 (set-option :incremental false)
 (set-info :source "TTA Startup. Bruno Dutertre (bruno@csl.sri.com)")
 (set-info :status unsat)
diff --git a/test/regress/regress1/nl/nl_uf_lalt.smt2 b/test/regress/regress1/nl/nl_uf_lalt.smt2
index 8d73ff9eb..c5ccd322f 100644
--- a/test/regress/regress1/nl/nl_uf_lalt.smt2
+++ b/test/regress/regress1/nl/nl_uf_lalt.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --no-check-unsat-cores
 (set-logic QF_UFNIA)
 (set-info :status unsat)
 (declare-fun c (Int) Int)
diff --git a/test/regress/regress1/quantifiers/qe-partial.smt2 b/test/regress/regress1/quantifiers/qe-partial.smt2
index 6f414fb2c..0138a3288 100644
--- a/test/regress/regress1/quantifiers/qe-partial.smt2
+++ b/test/regress/regress1/quantifiers/qe-partial.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE:
 ; SCRUBBER: sed -e 's/(not (>= (+ .* (\* (- 1) .*)) 1))$/(not (>= (+ TERMA (\* (- 1) TERMB)) 1))/'
 ; EXPECT: (not (>= (+ TERMA (* (- 1) TERMB)) 1))
 (set-logic LIA)
diff --git a/test/regress/regress1/quantifiers/qe.smt2 b/test/regress/regress1/quantifiers/qe.smt2
index 96cdd2497..2f0e4267f 100644
--- a/test/regress/regress1/quantifiers/qe.smt2
+++ b/test/regress/regress1/quantifiers/qe.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE:
 ; EXPECT: (not (>= (+ a (* (- 1) b)) 1))
 (set-logic LIA)
 (declare-fun a () Int)
diff --git a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2 b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
index 6465e27d6..ebf1f080e 100644
--- a/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
+++ b/test/regress/regress1/quantifiers/symmetric_unsat_7.smt2
@@ -1,4 +1,4 @@
-; COMMAND-LINE: --no-check-proofs --no-check-unsat-cores
+; COMMAND-LINE: --no-check-unsat-cores
 (set-logic AUFLIRA)
 (set-info :source | Example extracted from Peter Baumgartner's talk at CADE-21: Logical Engineering with Instance-Based Methods.
 
diff --git a/test/regress/regress2/arith/pursuit-safety-11.smtv1.smt2 b/test/regress/regress2/arith/pursuit-safety-11.smtv1.smt2
index a00c403f5..d37294dd8 100644
--- a/test/regress/regress2/arith/pursuit-safety-11.smtv1.smt2
+++ b/test/regress/regress2/arith/pursuit-safety-11.smtv1.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-proofs
 (set-option :incremental false)
 (set-info :source "SAL benchmark suite.  Created at SRI by Bruno Dutertre, John Rushby, Maria
 Sorea, and Leonardo de Moura.  Contact demoura@csl.sri.com for more
diff --git a/test/regress/regress2/arith/pursuit-safety-12.smtv1.smt2 b/test/regress/regress2/arith/pursuit-safety-12.smtv1.smt2
index cb65e3334..181d6fa8e 100644
--- a/test/regress/regress2/arith/pursuit-safety-12.smtv1.smt2
+++ b/test/regress/regress2/arith/pursuit-safety-12.smtv1.smt2
@@ -1,4 +1,3 @@
-; COMMAND-LINE: --no-check-proofs
 (set-option :incremental false)
 (set-info :source "SAL benchmark suite.  Created at SRI by Bruno Dutertre, John Rushby, Maria
 Sorea, and Leonardo de Moura.  Contact demoura@csl.sri.com for more
diff --git a/test/regress/regress2/bv_to_int_ashr.smt2 b/test/regress/regress2/bv_to_int_ashr.smt2
index 3e0151076..3f2d90a00 100644
--- a/test/regress/regress2/bv_to_int_ashr.smt2
+++ b/test/regress/regress2/bv_to_int_ashr.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=8 --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=8 --no-check-models  --no-check-unsat-cores
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 8))
diff --git a/test/regress/regress2/bv_to_int_mask_array_1.smt2 b/test/regress/regress2/bv_to_int_mask_array_1.smt2
index a2d90be2d..394a1d876 100644
--- a/test/regress/regress2/bv_to_int_mask_array_1.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_1.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 ALL)
 (declare-fun A () (Array Int Int))
diff --git a/test/regress/regress2/bv_to_int_mask_array_2.smt2 b/test/regress/regress2/bv_to_int_mask_array_2.smt2
index 9bab0c71c..36eabdb28 100644
--- a/test/regress/regress2/bv_to_int_mask_array_2.smt2
+++ b/test/regress/regress2/bv_to_int_mask_array_2.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: sat
 (set-logic ALL)
 (declare-fun A () (Array Int Int))
diff --git a/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p b/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p
index b4e9e9bb7..a521fdddc 100644
--- a/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p
+++ b/test/regress/regress2/ho/partial_app_interpreted_SWW474^2.p
@@ -1,4 +1,4 @@
-% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim --no-check-unsat-cores --no-check-proofs
+% COMMAND-LINE: --uf-ho --full-saturate-quant --ho-elim --no-check-unsat-cores
 % EXPECT: % SZS status Theorem for partial_app_interpreted_SWW474^2
 
 %------------------------------------------------------------------------------
diff --git a/test/regress/regress3/bv_to_int_and_or.smt2 b/test/regress/regress3/bv_to_int_and_or.smt2
index 185f1b5ec..3dc179aea 100644
--- a/test/regress/regress3/bv_to_int_and_or.smt2
+++ b/test/regress/regress3/bv_to_int_and_or.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=2 --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
 ; EXPECT: unsat
 (set-logic QF_BV)
 (declare-fun a () (_ BitVec 4))
diff --git a/test/regress/run_regression.py b/test/regress/run_regression.py
index 83b9a872e..d328e28d3 100755
--- a/test/regress/run_regression.py
+++ b/test/regress/run_regression.py
@@ -327,10 +327,9 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code, wrapper,
                 '# Skipped command line options ({}): unsat cores not supported without proof support'
                 .format(all_args))
             continue
-        if not proofs and ('--check-proofs' in all_args
-                           or '--dump-proofs' in all_args):
+        if not proofs and '--dump-proofs' in all_args:
             print(
-                '# Skipped command line options ({}): checking proofs not supported without LFSC support'
+                '# Skipped command line options ({}): proof production not supported without LFSC support'
                 .format(all_args))
             continue
 
@@ -347,24 +346,14 @@ def run_regression(unsat_cores, proofs, dump, use_skip_return_code, wrapper,
            '--no-check-models' not in all_args and \
            '--debug-check-models' not in all_args:
             extra_command_line_args = ['--debug-check-models']
-        if proofs and re.search(r'^(unsat|valid)$', expected_output):
-            if '--no-check-proofs' not in all_args and \
-               '--check-proofs' not in all_args and \
-               '--incremental' not in all_args and \
-               '--unconstrained-simp' not in all_args and \
-               logic_supported_with_proofs(logic) and \
-               not cvc4_binary.endswith('pcvc4'):
-                extra_command_line_args = ['--check-proofs']
         if unsat_cores and re.search(r'^(unsat|valid)$', expected_output):
             if '--no-check-unsat-cores' not in all_args and \
                '--check-unsat-cores' not in all_args and \
                '--incremental' not in all_args and \
-               '--unconstrained-simp' not in all_args and \
-               not cvc4_binary.endswith('pcvc4'):
+               '--unconstrained-simp' not in all_args:
                 extra_command_line_args += ['--check-unsat-cores']
         if '--no-check-abducts' not in all_args and \
-            '--check-abducts' not in all_args and \
-            not cvc4_binary.endswith('pcvc4'):
+            '--check-abducts' not in all_args:
             extra_command_line_args += ['--check-abducts']
         if extra_command_line_args:
             command_line_args_configs.append(all_args +