test/regress/regress0/sets/jan30/UniqueZipper.hs.fqout.minimized1832.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

(set-logic QF_ALL)
(set-info :status unsat)
(define-sort Elt () Int)
(define-sort mySet ()
  (Set Elt ))
(define-fun smt_set_emp () mySet (as emptyset mySet))

(declare-fun S () (Set Int))
(declare-fun T () (Set Int))
(declare-fun x () Int)

(assert (or (not (= S smt_set_emp)) (member x T)))

(assert (= smt_set_emp 
           (ite (member x T) 
                (union (union smt_set_emp (singleton x)) S) 
                S)))
(check-sat)