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

diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 8ca9d74c34f710bc54e7b43bf10e368cf63acb2f..870d83e7e5badb97a30aa1d586598e4ea159ff8c 100644 (file)
--- 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 bd2df3def61c03673056e1c389467f6dace1f443..62fd4a745a66cf81caab642d6ab9f7aea5b3a32e 100644 (file)
--- 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 ea68f654a7dc85031461a709e3a414f83bcb0563..3d51eddb999ee03c5c7f0c71818a59cbe7a268f0 100644 (file)
--- 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 1799df63c12dc5a3407d8c2a90661a36d5025478..3b50b025dc4c9d8f86526b2701a09382352498e0 100644 (file)
--- 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 8e47c88401d39946c37892c690686f2ff8d1ffe4..ec3efeedda9721ecf6d0108257505e5f81fbbe0c 100644 (file)
--- 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 0c1e323d5b719ddc058ec452c2b0305428d5b402..05ffef452a14462e4637b96f78e48df360c39e4e 100644 (file)
--- 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 d29311109c489209e30f4c52e1b3fb73d0b16e98..240691cd38431d29fe878286f757c3ac8a0174fb 100644 (file)
--- 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 846339f5244b2b9d5762760f0466a015f09f9ca4..20e0c638c1b2b13869f84f9493895db6ac16a48a 100644 (file)
--- 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 174ad747aefea5fc2220ff7a660c708a30dc2327..3b901d5527d66b70285e721db433a58310e62973 100644 (file)
--- 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 2a424e0851d058c910df1353dfa580a45196e04d..91c13b056a78374f46f68f4a19e888025c39d112 100644 (file)
--- 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 5b631a7fd955eb3cae77b2cd12622377534b8bac..942cdffdecadd78979c59eb7648bbee59fcc5391 100644 (file)
--- 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 a630049cbb6c0fc5b44586c201cea5bd7a747f22..65c9d26735a36c5c5fecf51eb74bf62b8b1eb7ec 100644 (file)
--- 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 (file)
index b1e87fc..0000000
--- 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 (file)
index d1ee440..0000000
--- 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 (file)
index 4d16230..0000000
--- 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 842650ebd0f24be53a820e4d51a9c3e3f6f7576b..b7a78e3b55f2bf32826d6a4ac4625a6e5fc1e1a7 100644 (file)
--- 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 d9190128ee6e6cadfea8ca2f30e940ffad38b4fa..f812ccbc8300a44af2b37ec9b7c3acb5f55a06dd 100644 (file)
--- 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 4bcbac20cc1db78e896bb5c90d8409fb599f8697..6f08c2e8d0b3fe5a4bf3ea87c080c3f4545d95aa 100644 (file)
--- 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 05cd312d734c63f7b539180e5b4cfa6f421d92ec..4e940b5df60684a39d4fd34967616cb6df9531b4 100644 (file)
--- 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 5c6be19b5b2290e38bc36b43c794a0d12b6de6a8..ab09d73415f14386fcdf07c0b061779ffeb1ff5f 100644 (file)
--- 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 3db8e87ee3bdb6ba242c0d9c0436b60da5ac31e6..6196b2bb908a6d6b0ace378653e1823b2b66dee3 100644 (file)
--- 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 90c01500dae2ec88484e160e6d2c57a763cd53fb..3e26d9f185d42ec738c4799354c54f098c01ddd3 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,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 96779d3a60d436b9ec59b3b10d6164b227713f4b..465937b2822e7d5f1ecf17beafec45b6b4ce495c 100644 (file)
--- 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 b6950845e5edcb37cf00d9a13cd1fa8d7a3dc6ef..185f7eca85c55d4e9effef86423471bf168ce5a0 100644 (file)
--- 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 6d026ff5bb74fbb8e9dd64d5d68be9060cfd518d..9ee1fa5eb1c2b553bf0fffc4df02eb91b4c0309d 100644 (file)
--- 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 4497b7a80c8ba06aa2cdd3c4add4dc50b423812c..97d8d1176b01f20317d2916f8b0190ba50e000e2 100644 (file)
--- 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 8dec350733aa3876a6db944029fb3dd5ad3ee111..b75f535d5d92855ad8900256b9473b3c49dbb928 100644 (file)
--- 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 6fa5426682edc8bbc137dae7180b6c609e5cb56c..09ec0917f746514706d230ca28d65b602c5b3af9 100644 (file)
--- 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 8101dfdebdd2d2d5d0136ef7f6ef15eb39f45cb4..e43cc6e7e736fef448627a858feb86595550b9a8 100644 (file)
--- 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 f910c2c96334f47a7d4413ecc6bef9c20aa42e95..e56c372fa165e863a52303fb8b2883dc1e6becb0 100644 (file)
--- 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 (file)
index 3d19a10..0000000
--- 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 1598f7097eb42d67ff92d5ce05ceb0d9ea7e6313..7cc9c2ea3c9eb83e28f914839dce4b0a067b1655 100644 (file)
--- 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 a692a7c4da8fc62f5962987e23574ec0c915a780..b87c9235270a33af48ef589522e9e2f82779032c 100644 (file)
--- 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 fd9d3f9c66552d20998ce864f77c9df5750d1fa1..6c48006f99010bb5661b5d1148ff8c170055b91c 100644 (file)
--- 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 3d89b719ee934cacc6757f2e48d06ca80fd35de8..6626a0c6ff8508a9f245469f4997c9def94e2ee0 100644 (file)
--- 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 bfc22850e45eefbc7e410c63fa6825e7ea9a70fe..9d26a06edbfa8ee55adfd4e0295402cef934d7ce 100644 (file)
--- 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 37accd35b9f686ab012f30ccda1ce620b7929747..fd621171c76ea9ea041d66fe539c7a0077896318 100644 (file)
--- 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 f3db784912371f671a054325ed9141f7f510767b..607a79f0de1aab7669fc5774c3862c4530c7c9ac 100644 (file)
--- 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 731fd4431817412c85481e1ad9205271e6584897..edb55d756a1638337f3392f21d7c3b909db7dab4 100644 (file)
--- 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 6187be7c13cff7f5fcf84e38ac3f006727ddc2bd..a936046a54bb34781a2aa228719382236a7d3e81 100644 (file)
--- 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 4aa162f5b2b612135f8f206dd40776362255076b..038b630192b650ae83d44de92330296ef9fc7d5c 100644 (file)
--- 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 8d73ff9eb647262a0c16eab93d72dca015816463..c5ccd322f68ad5a5b234ca00397252c030679aad 100644 (file)
--- 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 6f414fb2c1beb7e35234437b69c1cd20a018febc..0138a3288b1e2676a97602efec04458da79965c2 100644 (file)
--- 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 96cdd2497523b614df083e3ad66d0db7ed646dc4..2f0e4267f937a294ac8383b625499f9532dc6e86 100644 (file)
--- 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 6465e27d68861b93fafc21953e637dcd67968624..ebf1f080e0535020232ca151bd6e6dc310b9e75a 100644 (file)
--- 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 a00c403f502c111a978568d1db370d7da5df357c..d37294dd8a6fe57e6186823f943760a708425927 100644 (file)
--- 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 cb65e3334d3d79134b62ce7411168d698c61ca08..181d6fa8ed57cd4fc7b65690f9da2603e26f8791 100644 (file)
--- 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 3e0151076d3535801c5011bc12fec45ed3cf25bc..3f2d90a0083677da1d76c2276236981eda0c6e52 100644 (file)
--- 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 a2d90be2d4a36dfe106455a9cb360c6186a3f140..394a1d8765b887cde00f0cc95465d8927f15e9a4 100644 (file)
--- 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 9bab0c71cb0f0ce67f2f676d172db50924622024..36eabdb28bf4c2d8dc72da348f7d6c1955cb5636 100644 (file)
--- 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 b4e9e9bb7c1068dc4982a680db8823071980d92c..a521fdddc9853514a3d7f72fa707706149218b7c 100644 (file)
--- 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 185f1b5ecad944d06d77fae03d2b275392445819..3dc179aea74b7ea0118892ef177ca5e5c618cf7c 100644 (file)
--- 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 83b9a872e952a41df37403235636fa19d9966c94..d328e28d3fd2a2baa4bd6e54507e0428057247a4 100755 (executable)
--- 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 +