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

(benchmark simple_rdl
  :logic QF_RDL
  :status unsat
  :extrafuns ((x Real) (y Real))
  :formula (not (implies (< (- x y) 0) (< x y)))
)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback