blob: 6d84c00cbc3c5b09445ac6ea2ef1a6e676971021 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
|
(benchmark fuzzsmt
:logic QF_BV
:extrafuns ((v1 BitVec[13]))
:status sat
:formula
(let (?n1 bv1[13])
(flet ($n2 (bvult v1 ?n1))
(let (?n3 bv1[1])
(let (?n4 bv0[1])
(let (?n5 (ite $n2 ?n3 ?n4))
(let (?n6 (zero_extend[12] ?n5))
(flet ($n7 (bvuge ?n6 v1))
(let (?n8 (ite $n7 ?n3 ?n4))
(let (?n9 (zero_extend[12] ?n8))
(flet ($n10 (bvult ?n9 ?n1))
(let (?n11 (ite $n10 ?n3 ?n4))
(let (?n12 (sign_extend[5] ?n5))
(let (?n13 bv0[6])
(flet ($n14 (bvsgt ?n12 ?n13))
(let (?n15 (ite $n14 ?n3 ?n4))
(flet ($n16 (= ?n11 ?n15))
$n16
)))))))))))))))))
|
