forked from openkylin/z3
11 lines
247 B
Plaintext
11 lines
247 B
Plaintext
|
(declare-const x Int)
|
||
|
|
(declare-const y Int)
|
||
|
|
(declare-const z Int)
|
||
|
|
(assert-soft (> x 0))
|
||
|
|
(assert-soft (<= x -1))
|
||
|
|
(assert-soft (or (> x 0) (< y 1)))
|
||
|
|
(assert-soft (> y 2))
|
||
|
|
(assert-soft (> y 3))
|
||
|
|
(assert-soft (<= y -1))
|
||
|
|
(assert (= z (+ x y)))
|
||
|
|
|