summaryrefslogtreecommitdiff
path: root/test/regress/regress0/uflra/neq-deltacomp.smt
blob: 9185a18c82fc8dd92116585e458f676f5253d9f0 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12
13
14

(benchmark fuzzsmt
:logic QF_UFLRA
:extrafuns ((v2 Real))
:extrafuns ((v1 Real))
:extrafuns ((v0 Real))
:status sat
:formula
(let (?n1 (~ v1))
(flet ($n2 (>= ?n1 v0))
(let (?n3 1)
(let (?n4 (ite $n2 v1 ?n3))
(flet ($n5 (<= ?n4 v2))
$n5
))))))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback