summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bug288c.smt
blob: acf40ce07b5daf15e96191e4136059cbfcac7883 (plain) 
1
2
3
4
5
6
7
8
9

(benchmark delta
:logic QF_LIA
:extrafuns ((x Int))
:extrafuns ((y Int))
:extrafuns ((z Int))
:status sat
:formula
  (and (= z 0) (>= (+ (- (* 2 x) (* 2 y)) z) 1))
)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback