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

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