diff options
Diffstat (limited to 'test/regress/regress0/sets')
29 files changed, 29 insertions, 29 deletions
diff --git a/test/regress/regress0/sets/card-3sets.cvc b/test/regress/regress0/sets/card-3sets.cvc index cac10f39c..7422df91c 100644 --- a/test/regress/regress0/sets/card-3sets.cvc +++ b/test/regress/regress0/sets/card-3sets.cvc @@ -1,5 +1,5 @@ % EXPECT: sat -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; x : SET OF INT; y : SET OF INT; z : SET OF INT; diff --git a/test/regress/regress0/sets/card3-ground.smt2 b/test/regress/regress0/sets/card3-ground.smt2 index 54a9a5cfc..7b42b8a8a 100644 --- a/test/regress/regress0/sets/card3-ground.smt2 +++ b/test/regress/regress0/sets/card3-ground.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-fun S () (Set Int)) (assert (>= (card S) 3)) diff --git a/test/regress/regress0/sets/complement.cvc b/test/regress/regress0/sets/complement.cvc index 91388a56c..64df0790a 100644 --- a/test/regress/regress0/sets/complement.cvc +++ b/test/regress/regress0/sets/complement.cvc @@ -1,6 +1,6 @@ % EXPECT: sat OPTION "sets-ext"; -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; Atom: TYPE; a : SET OF [Atom]; b : SET OF [Atom]; diff --git a/test/regress/regress0/sets/complement2.cvc b/test/regress/regress0/sets/complement2.cvc index b8100bf5f..a3dd25477 100644 --- a/test/regress/regress0/sets/complement2.cvc +++ b/test/regress/regress0/sets/complement2.cvc @@ -1,6 +1,6 @@ % EXPECT: unsat
OPTION "sets-ext";
-OPTION "logic" "ALL_SUPPORTED";
+OPTION "logic" "ALL";
Atom: TYPE;
a : SET OF Atom;
b : SET OF Atom;
diff --git a/test/regress/regress0/sets/complement3.cvc b/test/regress/regress0/sets/complement3.cvc index fa0a31e40..762d186ed 100644 --- a/test/regress/regress0/sets/complement3.cvc +++ b/test/regress/regress0/sets/complement3.cvc @@ -1,6 +1,6 @@ % EXPECT: sat OPTION "sets-ext"; -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; Atom : TYPE; C32 : SET OF [Atom]; C2 : SET OF [Atom]; diff --git a/test/regress/regress0/sets/cvc-sample.cvc b/test/regress/regress0/sets/cvc-sample.cvc index 06d2b5049..11f9428c3 100644 --- a/test/regress/regress0/sets/cvc-sample.cvc +++ b/test/regress/regress0/sets/cvc-sample.cvc @@ -6,7 +6,7 @@ % EXPECT: unsat % EXPECT: not_entailed OPTION "incremental" true; -OPTION "logic" "ALL_SUPPORTED"; +OPTION "logic" "ALL"; SetInt : TYPE = SET OF INT; x : SET OF INT; y : SET OF INT; diff --git a/test/regress/regress0/sets/dt-simp-mem.smt2 b/test/regress/regress0/sets/dt-simp-mem.smt2 index 51400a05a..47bc7aa58 100644 --- a/test/regress/regress0/sets/dt-simp-mem.smt2 +++ b/test/regress/regress0/sets/dt-simp-mem.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (declare-datatypes ((D 0)) (((A (a Int))))) (declare-fun x1 () D) diff --git a/test/regress/regress0/sets/emptyset.smt2 b/test/regress/regress0/sets/emptyset.smt2 index 2b2322d46..7296fcc28 100644 --- a/test/regress/regress0/sets/emptyset.smt2 +++ b/test/regress/regress0/sets/emptyset.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (assert (member 5 (as emptyset (Set Int) ))) (check-sat) diff --git a/test/regress/regress0/sets/eqtest.smt2 b/test/regress/regress0/sets/eqtest.smt2 index cb816a306..06f86ae3c 100644 --- a/test/regress/regress0/sets/eqtest.smt2 +++ b/test/regress/regress0/sets/eqtest.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (declare-fun A () (Set Int) ) (declare-fun B () (Set Int) ) diff --git a/test/regress/regress0/sets/error2.smt2 b/test/regress/regress0/sets/error2.smt2 index 0b8c5ab65..7b8f78218 100644 --- a/test/regress/regress0/sets/error2.smt2 +++ b/test/regress/regress0/sets/error2.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (assert (= (as emptyset (Set Int)) (singleton 5))) (check-sat) diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 index 71bb8a3e6..448022a2e 100644 --- a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 +++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (define-sort Elt () Int) (define-sort mySet () (Set Elt )) diff --git a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 index 652307645..a7c2bec8d 100644 --- a/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 +++ b/test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-fun x () Int) diff --git a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 index c4ee3b710..ff83b0fb5 100644 --- a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 +++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (define-sort Elt () Int) (define-sort mySet () (Set Elt )) diff --git a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 index eb48b023a..90d3a6372 100644 --- a/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 +++ b/test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (define-sort Elt () Int) (define-sort mySet () (Set Elt )) diff --git a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 index 35110d831..b20fb4f3d 100644 --- a/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 +++ b/test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status sat) ; Observed behavior diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 index df659f0fb..1c28759b6 100644 --- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) ; Observed diff --git a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 index af67a69a7..8b879b3ec 100644 --- a/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 +++ b/test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2 @@ -1,4 +1,4 @@ -(set-logic QF_ALL_SUPPORTED) +(set-logic QF_ALL) (set-info :status unsat) (define-sort Elt () Int) (define-sort mySet () diff --git a/test/regress/regress0/sets/setel-eq.smt2 b/test/regress/regress0/sets/setel-eq.smt2 index b5d85c7e8..35b89645a 100644 --- a/test/regress/regress0/sets/setel-eq.smt2 +++ b/test/regress/regress0/sets/setel-eq.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-fun S () (Set Int)) (declare-fun T () (Set Int)) diff --git a/test/regress/regress0/sets/sets-equal.smt2 b/test/regress/regress0/sets/sets-equal.smt2 index 8fd29a244..adccd51c5 100644 --- a/test/regress/regress0/sets/sets-equal.smt2 +++ b/test/regress/regress0/sets/sets-equal.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-fun x () Int) (declare-fun y () Int) diff --git a/test/regress/regress0/sets/sets-inter.smt2 b/test/regress/regress0/sets/sets-inter.smt2 index d3d8a9044..2faf72768 100644 --- a/test/regress/regress0/sets/sets-inter.smt2 +++ b/test/regress/regress0/sets/sets-inter.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (define-sort SetInt () (Set Int)) (declare-fun a () (Set Int)) diff --git a/test/regress/regress0/sets/sets-new.smt2 b/test/regress/regress0/sets/sets-new.smt2 index 0f43ee10d..8ac414829 100644 --- a/test/regress/regress0/sets/sets-new.smt2 +++ b/test/regress/regress0/sets/sets-new.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (define-sort SetInt () (Set Int)) diff --git a/test/regress/regress0/sets/sets-sample.smt2 b/test/regress/regress0/sets/sets-sample.smt2 index 3bc2da065..b92c4b2cf 100644 --- a/test/regress/regress0/sets/sets-sample.smt2 +++ b/test/regress/regress0/sets/sets-sample.smt2 @@ -4,7 +4,7 @@ ; EXPECT: unsat ; EXPECT: unsat ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (define-sort SetInt () (Set Int)) ; Something simple to test parsing diff --git a/test/regress/regress0/sets/sets-sharing.smt2 b/test/regress/regress0/sets/sets-sharing.smt2 index caada9606..1ac2e1603 100644 --- a/test/regress/regress0/sets/sets-sharing.smt2 +++ b/test/regress/regress0/sets/sets-sharing.smt2 @@ -1,4 +1,4 @@ -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status unsat) (declare-fun S () (Set Int)) diff --git a/test/regress/regress0/sets/sets-union.smt2 b/test/regress/regress0/sets/sets-union.smt2 index 56ba520dc..b794633e3 100644 --- a/test/regress/regress0/sets/sets-union.smt2 +++ b/test/regress/regress0/sets/sets-union.smt2 @@ -1,7 +1,7 @@ ; COMMAND-LINE: --incremental ; EXPECT: sat ; EXPECT: unsat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (define-sort SetInt () (Set Int)) (declare-fun a () (Set Int)) (declare-fun b () (Set Int)) diff --git a/test/regress/regress0/sets/union-1a-flip.smt2 b/test/regress/regress0/sets/union-1a-flip.smt2 index 6a73c5b91..bb969f866 100644 --- a/test/regress/regress0/sets/union-1a-flip.smt2 +++ b/test/regress/regress0/sets/union-1a-flip.smt2 @@ -3,7 +3,7 @@ ; EXPECT: sat ; x not in A U B => x not in A -(set-logic ALL_SUPPORTED) +(set-logic ALL) (define-sort SetInt () (Set Int)) (declare-fun A () (Set Int)) (declare-fun B () (Set Int)) diff --git a/test/regress/regress0/sets/union-1a.smt2 b/test/regress/regress0/sets/union-1a.smt2 index 8636cb220..ad684070f 100644 --- a/test/regress/regress0/sets/union-1a.smt2 +++ b/test/regress/regress0/sets/union-1a.smt2 @@ -3,7 +3,7 @@ ; EXPECT: sat ; x not in A U B => x not in A -(set-logic ALL_SUPPORTED) +(set-logic ALL) (define-sort SetInt () (Set Int)) (declare-fun A () (Set Int)) (declare-fun B () (Set Int)) diff --git a/test/regress/regress0/sets/union-1b-flip.smt2 b/test/regress/regress0/sets/union-1b-flip.smt2 index e2b19b31a..228452f54 100644 --- a/test/regress/regress0/sets/union-1b-flip.smt2 +++ b/test/regress/regress0/sets/union-1b-flip.smt2 @@ -3,7 +3,7 @@ ; EXPECT: sat ; x not in A U B => x not in A -(set-logic ALL_SUPPORTED) +(set-logic ALL) (define-sort SetInt () (Set Int)) (declare-fun A () (Set Int)) (declare-fun B () (Set Int)) diff --git a/test/regress/regress0/sets/union-1b.smt2 b/test/regress/regress0/sets/union-1b.smt2 index c354923c9..8829b6152 100644 --- a/test/regress/regress0/sets/union-1b.smt2 +++ b/test/regress/regress0/sets/union-1b.smt2 @@ -3,7 +3,7 @@ ; EXPECT: sat ; x not in A U B => x not in A -(set-logic ALL_SUPPORTED) +(set-logic ALL) (define-sort SetInt () (Set Int)) (declare-fun A () (Set Int)) (declare-fun B () (Set Int)) diff --git a/test/regress/regress0/sets/union-2.smt2 b/test/regress/regress0/sets/union-2.smt2 index 6e2933975..52d2e7e8c 100644 --- a/test/regress/regress0/sets/union-2.smt2 +++ b/test/regress/regress0/sets/union-2.smt2 @@ -1,5 +1,5 @@ ; EXPECT: sat -(set-logic ALL_SUPPORTED) +(set-logic ALL) (set-info :status sat) (define-sort SetInt () (Set Int)) (declare-fun A () (Set Int)) |