mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-03 21:09:11 +00:00
Code Activity

fix example file to be smt2 format

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-11-29 19:38:47 -08:00
parent 0a67f6ee9b
commit 9f567a6215
1 changed files with 10 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

20
examples/maxsat/ex.smt
View file

@ -1,11 +1,11 @@
(benchmark ex (declare-const x Int)
:logic AUFLIA (declare-const y Int)
:extrafuns ((x Int) (y Int) (z Int)) (declare-const z Int)
:assumption (> x 0) (assert-soft (> x 0))
:assumption (<= x -1) (assert-soft (<= x -1))
:assumption (or (> x 0) (< y 1)) (assert-soft (or (> x 0) (< y 1)))
:assumption (> y 2) (assert-soft (> y 2))
:assumption (> y 3) (assert-soft (> y 3))
:assumption (<= y -1) (assert-soft (<= y -1))
:formula (= z (+ x y))) (assert (= z (+ x y)))