summaryrefslogtreecommitdiff
path: root/test/regress/regress0/simple-lra.smt
blob: c80632a96b115fc6d0045dbb0245f7b699c16395 (plain) 
1
2
3
4
5
6

(benchmark simple_lra
  :logic QF_LRA
  :status unsat
  :extrafuns ((x Real) (y Real))
  :formula (not (implies (and (> x 0) (< (* 2 x) y)) (and (> y 0) (< x y))))
)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback