summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bv/fuzz40.delta01.smt
blob: 3161c1675fcdf8ecae7a726aa613b61dbd899cb1 (plain) 
1
2
3
4
5
6
7
8
9
10
11
12

(benchmark fuzzsmt
:logic QF_BV
:extrafuns ((v0 BitVec[4]))
:status sat
:formula
(let (?n1 bv1[4])
(let (?n2 (bvmul ?n1 v0))
(let (?n3 (extract[3:0] ?n2))
(let (?n4 bv0[4])
(flet ($n5 (bvsge ?n3 ?n4))
$n5
))))))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback