blob: c6b87adebbd26ff8bf323d9fd0539b983d37e630 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
; COMMAND-LINE: --symmetry-breaker-exp
(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 (subset A (insert y (singleton z))))
(check-sat)
|
