diff options
Diffstat (limited to 'test/regress/regress0')
34 files changed, 27 insertions, 131 deletions
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) |