summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sym/sym1.smt2
blob: a468d6c87834b928a51091562b0201f8a885c598 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

(set-logic ALL)
(set-info :status sat)
(declare-fun x () Int)
(declare-fun y () Int)
(declare-fun z () Int)


(declare-fun p (Int) Bool)
(declare-fun A () (Set Int))
(declare-fun F () (Set Int))



(assert (= F (set.insert x y (set.singleton z))))
(assert (set.subset F A))
(assert (= x y))


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