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

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