summaryrefslogtreecommitdiff
path: root/test/regress/regress0/sets/abt-te-exh.smt2
blob: f87429fc24116b63e27e7107a9c673ea3a7bd3e2 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13

; COMMAND-LINE: --finite-model-find
; EXPECT: sat
(set-logic ALL)
(declare-sort Atom 0)

(declare-fun j ((Set Atom)) Atom)
(declare-fun kk (Atom (Set Atom)) (Set Atom))
(declare-fun n () (Set Atom))

(assert (forall ((b Atom)) (= (as emptyset (Set Atom)) (kk (j (singleton b)) n))))

(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback