summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sets
diff options
context:
space:
mode:
Diffstat (limited to 'test/regress/regress0/sets')
-rw-r--r--test/regress/regress0/sets/card-3sets.cvc2
-rw-r--r--test/regress/regress0/sets/card3-ground.smt22
-rw-r--r--test/regress/regress0/sets/complement.cvc2
-rw-r--r--test/regress/regress0/sets/complement2.cvc2
-rw-r--r--test/regress/regress0/sets/complement3.cvc2
-rw-r--r--test/regress/regress0/sets/cvc-sample.cvc2
-rw-r--r--test/regress/regress0/sets/dt-simp-mem.smt22
-rw-r--r--test/regress/regress0/sets/emptyset.smt22
-rw-r--r--test/regress/regress0/sets/eqtest.smt22
-rw-r--r--test/regress/regress0/sets/error2.smt22
-rw-r--r--test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.cvc4.47.smt22
-rw-r--r--test/regress/regress0/sets/jan24/deepmeas0.hs.fqout.small.smt22
-rw-r--r--test/regress/regress0/sets/jan27/ListConcat.hs.fqout.177minimized.smt22
-rw-r--r--test/regress/regress0/sets/jan27/ListConcat.hs.fqout.cvc4.177.smt22
-rw-r--r--test/regress/regress0/sets/jan28/TalkingAboutSets.hs.fqout.3577minimized.smt22
-rw-r--r--test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized10.smt22
-rw-r--r--test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt22
-rw-r--r--test/regress/regress0/sets/setel-eq.smt22
-rw-r--r--test/regress/regress0/sets/sets-equal.smt22
-rw-r--r--test/regress/regress0/sets/sets-inter.smt22
-rw-r--r--test/regress/regress0/sets/sets-new.smt22
-rw-r--r--test/regress/regress0/sets/sets-sample.smt22
-rw-r--r--test/regress/regress0/sets/sets-sharing.smt22
-rw-r--r--test/regress/regress0/sets/sets-union.smt22
-rw-r--r--test/regress/regress0/sets/union-1a-flip.smt22
-rw-r--r--test/regress/regress0/sets/union-1a.smt22
-rw-r--r--test/regress/regress0/sets/union-1b-flip.smt22
-rw-r--r--test/regress/regress0/sets/union-1b.smt22
-rw-r--r--test/regress/regress0/sets/union-2.smt22
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))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback