diff options
Diffstat (limited to 'test/regress/regress0/sets/univ-set-uf-elim.smt2')
| -rw-r--r-- | test/regress/regress0/sets/univ-set-uf-elim.smt2 | 16 |
1 files changed, 0 insertions, 16 deletions
diff --git a/test/regress/regress0/sets/univ-set-uf-elim.smt2 b/test/regress/regress0/sets/univ-set-uf-elim.smt2 deleted file mode 100644 index a22f2a44f..000000000 --- a/test/regress/regress0/sets/univ-set-uf-elim.smt2 +++ /dev/null @@ -1,16 +0,0 @@ -; EXPECT: (error "Extended set operators are not supported in default mode, try --sets-ext.") -; EXIT: 1 -(set-logic ALL) -(declare-fun a () Int) -(declare-fun f ((Set Bool)) Int) -(declare-fun s () (Set Bool)) - -(assert (member true s)) -(assert (member false s)) -(assert (= a (f (as univset (Set Bool))))) - -(assert (= (f (as emptyset (Set Bool))) 1)) -(assert (= (f (singleton true)) 2)) -(assert (= (f (singleton false)) 3)) -(assert (= (f (union (singleton true) (singleton false))) 4)) -(check-sat) |