diff options
| author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-30 10:53:52 -0400 |
|---|---|---|
| committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-06-30 10:53:52 -0400 |
| commit | fa53ae111cd314f455456a884f1247bb9b8e2c7b (patch) | |
| tree | 2eb9d36e5e20d2160c7d49b6f89f162b54a20d64 /test/regress/regress0/sets/mar2014 | |
| parent | f4d031742d969c689d38c0756a5026a434ef89b3 (diff) | |
Use FS as the set-logic string for theory of sets
Diffstat (limited to 'test/regress/regress0/sets/mar2014')
| -rw-r--r-- | test/regress/regress0/sets/mar2014/sharing-preregister.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/sets/mar2014/small.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/sets/mar2014/smaller.smt2 | 2 |
3 files changed, 3 insertions, 3 deletions
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)) |