mirror of
https://github.com/Z3Prover/z3
synced 2025-11-04 05:19:11 +00:00
11 lines
No EOL
253 B
Text
11 lines
No EOL
253 B
Text
(benchmark ex
|
|
:logic AUFLIA
|
|
:extrafuns ((x Int) (y Int) (z Int))
|
|
:assumption (> x 0)
|
|
:assumption (<= x -1)
|
|
:assumption (or (> x 0) (< y 1))
|
|
:assumption (> y 2)
|
|
:assumption (> y 3)
|
|
:assumption (<= y -1)
|
|
:formula (= z (+ x y)))
|
|
|