From: Andres Noetzli Date: Wed, 19 Aug 2020 14:08:22 +0000 (-0700) Subject: [Regressions] Do not test `--check-proofs` anymore (#4914) X-Git-Tag: cvc5-1.0.0~2980 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=41f1a9a0036f3d18ec21ef6005fb218cf704fe60;p=cvc5.git [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 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 +