From fa53ae111cd314f455456a884f1247bb9b8e2c7b Mon Sep 17 00:00:00 2001
From: Kshitij Bansal <kshitij@cs.nyu.edu>
Date: Mon, 30 Jun 2014 10:53:52 -0400
Subject: Use FS as the set-logic string for theory of sets

---
 test/regress/regress0/sets/copy_check_heap_access_33_4.smt2          | 2 +-
 test/regress/regress0/sets/error1.smt2                               | 2 +-
 test/regress/regress0/sets/fuzz14418.smt2                            | 2 +-
 test/regress/regress0/sets/fuzz15201.smt2                            | 2 +-
 test/regress/regress0/sets/fuzz31811.smt2                            | 2 +-
 test/regress/regress0/sets/insert.smt2                               | 2 +-
 test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2          | 2 +-
 test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2         | 2 +-
 test/regress/regress0/sets/mar2014/sharing-preregister.smt2          | 2 +-
 test/regress/regress0/sets/mar2014/small.smt2                        | 2 +-
 test/regress/regress0/sets/mar2014/smaller.smt2                      | 2 +-
 test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 | 2 +-
 test/regress/regress0/sets/setofsets-disequal.smt2                   | 2 +-
 test/regress/regress0/sets/sets-disequal.smt2                        | 2 +-
 test/regress/regress0/sets/sets-testlemma-ints.smt2                  | 2 +-
 test/regress/regress0/sets/sets-testlemma-reals.smt2                 | 2 +-
 test/regress/regress0/sets/sets-testlemma.smt2                       | 2 +-
 test/regress/regress0/sets/sharingbug.smt2                           | 2 +-
 18 files changed, 18 insertions(+), 18 deletions(-)

(limited to 'test')

diff --git a/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2 b/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2
index b4ddfec41..9af45c2dd 100644
--- a/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2
+++ b/test/regress/regress0/sets/copy_check_heap_access_33_4.smt2
@@ -1,7 +1,7 @@
 ; COMMAND-LINE: --full-saturate-quant
 ; EXPECT: unsat
 (set-option :print-success false)
-(set-logic AUFLIA_SETS)
+(set-logic AUFLIAFS)
 (set-info :status unsat)
 (declare-sort Loc 0)
 (define-sort SetLoc () (Set Loc))
diff --git a/test/regress/regress0/sets/error1.smt2 b/test/regress/regress0/sets/error1.smt2
index 1241b117f..bf1822305 100644
--- a/test/regress/regress0/sets/error1.smt2
+++ b/test/regress/regress0/sets/error1.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (set-info :status sat)
 (declare-fun A () (Set Int))
 (declare-fun C () (Set Int))
diff --git a/test/regress/regress0/sets/fuzz14418.smt2 b/test/regress/regress0/sets/fuzz14418.smt2
index e7a7be97a..24679749c 100644
--- a/test/regress/regress0/sets/fuzz14418.smt2
+++ b/test/regress/regress0/sets/fuzz14418.smt2
@@ -11,7 +11,7 @@
 (set-info :smt-lib-version 2.0)
 (set-info :category "random")
 (set-info :status sat)
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (define-sort Element () Int)
 (declare-fun f0 ( Int) Int)
 (declare-fun f1 ( (Set Element) (Set Element) (Set Element)) (Set Element))
diff --git a/test/regress/regress0/sets/fuzz15201.smt2 b/test/regress/regress0/sets/fuzz15201.smt2
index 650c0ead1..e12b74d18 100644
--- a/test/regress/regress0/sets/fuzz15201.smt2
+++ b/test/regress/regress0/sets/fuzz15201.smt2
@@ -4,7 +4,7 @@
 (set-info :smt-lib-version 2.0)
 (set-info :category "random")
 (set-info :status sat)
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (define-sort Element () Int)
 (declare-fun f0 ( Int) Int)
 (declare-fun f1 ( (Set Element)) (Set Element))
diff --git a/test/regress/regress0/sets/fuzz31811.smt2 b/test/regress/regress0/sets/fuzz31811.smt2
index 536d62d3d..5e7c032ea 100644
--- a/test/regress/regress0/sets/fuzz31811.smt2
+++ b/test/regress/regress0/sets/fuzz31811.smt2
@@ -9,7 +9,7 @@
 (set-info :smt-lib-version 2.0)
 (set-info :category "random")
 (set-info :status sat)
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (define-sort Element () Int)
 (declare-fun f0 ( Int Int Int) Int)
 (declare-fun f1 ( (Set Element) (Set Element)) (Set Element))
diff --git a/test/regress/regress0/sets/insert.smt2 b/test/regress/regress0/sets/insert.smt2
index 3a7b18179..b4936a32b 100644
--- a/test/regress/regress0/sets/insert.smt2
+++ b/test/regress/regress0/sets/insert.smt2
@@ -1,5 +1,5 @@
 (set-option :produce-models true)
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (set-info :status sat)
 (declare-fun X () (Set Int))
 (assert (= X (insert 1 2 (singleton 3))))
diff --git a/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2 b/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2
index 4a588aeb6..2ef07f920 100644
--- a/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2
+++ b/test/regress/regress0/sets/jan24/insert_invariant_37_2.smt2
@@ -1,5 +1,5 @@
 (set-option :print-success false)
-(set-logic AUFLIA_SETS)
+(set-logic AUFLIAFS)
 (set-info :status unsat)
 (declare-sort Loc 0)
 (define-sort SetLoc () (Set Loc))
diff --git a/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2 b/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2
index c10b14f2b..2bf2d4c62 100644
--- a/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2
+++ b/test/regress/regress0/sets/jan24/remove_check_free_31_6.smt2
@@ -1,5 +1,5 @@
 (set-option :print-success false)
-(set-logic AUFLIA_SETS)
+(set-logic AUFLIAFS)
 (set-info :status unsat)
 (declare-sort Loc 0)
 (define-sort SetLoc () (Set Loc))
diff --git a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2 b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2
index 61af2124d..d851ca35e 100644
--- a/test/regress/regress0/sets/mar2014/sharing-preregister.smt2
+++ b/test/regress/regress0/sets/mar2014/sharing-preregister.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: unsat
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (set-info :status sat)
 (declare-fun a () Int)
 (declare-fun b () Int)
diff --git a/test/regress/regress0/sets/mar2014/small.smt2 b/test/regress/regress0/sets/mar2014/small.smt2
index 896b13219..635c7959d 100644
--- a/test/regress/regress0/sets/mar2014/small.smt2
+++ b/test/regress/regress0/sets/mar2014/small.smt2
@@ -4,7 +4,7 @@
 ; demostrates core issue with UniqueZipper.hs.1030minimized.cvc4.smt2
 ; unlike original benchmark, this is unsat.
 
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (declare-fun x () Int)
 (declare-fun y () Int)
 (declare-fun z () Int)
diff --git a/test/regress/regress0/sets/mar2014/smaller.smt2 b/test/regress/regress0/sets/mar2014/smaller.smt2
index 22e029b69..d6565205b 100644
--- a/test/regress/regress0/sets/mar2014/smaller.smt2
+++ b/test/regress/regress0/sets/mar2014/smaller.smt2
@@ -4,7 +4,7 @@
 ; demostrates core issue with UniqueZipper.hs.1030minimized.cvc4.smt2
 ; fails check-model, even though answer is correct
 
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (declare-fun x () Int)
 (declare-fun y () Int)
 (declare-fun a () (Set Int))
diff --git a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2 b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
index e5defb2ac..61fbee11d 100644
--- a/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
+++ b/test/regress/regress0/sets/rec_copy_loop_check_heap_access_43_4.smt2
@@ -1,5 +1,5 @@
 (set-option :print-success false)
-(set-logic AUFLIA_SETS)
+(set-logic AUFLIAFS)
 (set-info :status unsat)
 (declare-sort Loc 0)
 (define-sort SetLoc () (Set Loc))
diff --git a/test/regress/regress0/sets/setofsets-disequal.smt2 b/test/regress/regress0/sets/setofsets-disequal.smt2
index 18ad053d6..1702aab27 100644
--- a/test/regress/regress0/sets/setofsets-disequal.smt2
+++ b/test/regress/regress0/sets/setofsets-disequal.smt2
@@ -1,7 +1,7 @@
 ; On a production build (as of 2014-05-16), takes several minutes
 ; to finish (2967466 decisions).
 
-(set-logic QF_BV_SETS)
+(set-logic QF_BVFS)
 (set-info :status unsat)
 
 (define-sort myset () (Set (Set (_ BitVec 1))))
diff --git a/test/regress/regress0/sets/sets-disequal.smt2 b/test/regress/regress0/sets/sets-disequal.smt2
index 65f55f3a6..3acf77108 100644
--- a/test/regress/regress0/sets/sets-disequal.smt2
+++ b/test/regress/regress0/sets/sets-disequal.smt2
@@ -3,7 +3,7 @@
 ; EXPECT: sat
 ; EXPECT: unsat
 ; EXIT: 0
-(set-logic QF_BV_SETS)
+(set-logic QF_BVFS)
 (declare-fun S1 () (Set (_ BitVec 1)))
 (declare-fun S2 () (Set (_ BitVec 1)))
 (declare-fun S3 () (Set (_ BitVec 1)))
diff --git a/test/regress/regress0/sets/sets-testlemma-ints.smt2 b/test/regress/regress0/sets/sets-testlemma-ints.smt2
index 9dd257401..e68520cbf 100644
--- a/test/regress/regress0/sets/sets-testlemma-ints.smt2
+++ b/test/regress/regress0/sets/sets-testlemma-ints.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (set-info :status sat)
 (declare-fun x () (Set Int))
 (declare-fun y () (Set Int))
diff --git a/test/regress/regress0/sets/sets-testlemma-reals.smt2 b/test/regress/regress0/sets/sets-testlemma-reals.smt2
index 16e7780b4..bc18235f0 100644
--- a/test/regress/regress0/sets/sets-testlemma-reals.smt2
+++ b/test/regress/regress0/sets/sets-testlemma-reals.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-(set-logic QF_UFLRA_SETS)
+(set-logic QF_UFLRAFS)
 (set-info :status sat)
 (declare-fun x () (Set Real))
 (declare-fun y () (Set Real))
diff --git a/test/regress/regress0/sets/sets-testlemma.smt2 b/test/regress/regress0/sets/sets-testlemma.smt2
index 183f54242..aee8c5937 100644
--- a/test/regress/regress0/sets/sets-testlemma.smt2
+++ b/test/regress/regress0/sets/sets-testlemma.smt2
@@ -1,5 +1,5 @@
 ; EXPECT: sat
-(set-logic QF_UFBV_SETS)
+(set-logic QF_UFBVFS)
 (set-info :status sat)
 (declare-fun x () (Set (_ BitVec 2)))
 (declare-fun y () (Set (_ BitVec 2)))
diff --git a/test/regress/regress0/sets/sharingbug.smt2 b/test/regress/regress0/sets/sharingbug.smt2
index b388bb534..b87579816 100644
--- a/test/regress/regress0/sets/sharingbug.smt2
+++ b/test/regress/regress0/sets/sharingbug.smt2
@@ -2,7 +2,7 @@
 (set-info :smt-lib-version 2.0)
 (set-info :category "random")
 (set-info :status sat)
-(set-logic QF_UFLIA_SETS)
+(set-logic QF_UFLIAFS)
 (define-sort Element () Int)
 (declare-fun f0 ( Int Int Int) Int)
 (declare-fun f1 ( (Set Element)) (Set Element))
-- 
cgit v1.2.3