summaryrefslogtreecommitdiff
path: root/test/regress/regress0/ineq_slack.smt
blob: b3d79c5f27fc3b9448911ef0e6fca7eb5a59d2bf (plain) 
1
2
3
4
5
6
7
8
9
10
11

(benchmark ineq_basic
:status unsat
:logic QF_LRA
:extrafuns ((x Real))
:extrafuns ((y Real))
:formula
 (and (<= (+ x y) 0)
      (< 1 x)
      (<= 0 y)
 )
)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback