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

(benchmark uart
:logic QF_LRA
:extrafuns ((x_1 Real))
:status unsat
:formula
(let (?n1 10)
(flet ($n2 (= x_1 ?n1))
(let (?n3 1)
(flet ($n4 (< x_1 ?n3))
(flet ($n5 (and $n2 $n4))
$n5
))))))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback