test/regress/regress1/sym/sym3.smt2


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 w () Int)
(declare-fun u () Int)
(declare-fun v () Int)

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


(assert (or (> (+ x y z) 3) (< (p x (+ (* 3 y) (* 3 z))) 5)))
(assert (set.subset A (set.insert y (set.singleton z))))


(check-sat)