test/regress/regress1/sym/sym6.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

; 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)


(assert (= (+ w y u) (+ v z)))

(assert (> (+ x (* 2 y)) (+ u v)))

(assert (= (- x) (- (- y))))


(assert (or (< (+ x y z) 10) (> (+ v u) 10)))


(check-sat)