summaryrefslogtreecommitdiff
path: root/test/regress/regress1/sym/sym1.smt2
blob: 987b6c1f47a54d472e8612d6053fc7b8bb08114a (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 (insert x y (singleton z))))
(assert (subset F A))
(assert (= x y))


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