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

(benchmark fuzzsmt
:logic QF_BV
:extrafuns ((v2 BitVec[4]))
:extrafuns ((v1 BitVec[4]))
:status sat
:formula
(let (?n1 (bvmul v1 v2))
(let (?n2 (bvneg ?n1))
(flet ($n3 (distinct ?n1 ?n2))
$n3
))))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback