test/regress/regress1/sym/sym7-uf.smt2


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

(set-logic ALL)
(set-info :status sat)
(declare-sort U 0)
(declare-fun x () U)
(declare-fun y () U)
(declare-fun z () U)
(declare-fun w () U)
(declare-fun u () U)
(declare-fun v () U)
(declare-fun a () U)
(declare-fun P (U) Bool)

(assert (distinct w u v a))
(assert (or (= x y) (= x z) (= y z)))
(assert (or (P x) (P y) (P z) (P w)))

; should get { x, y, z }, { w }, { u, v, a }
(check-sat)