blob: f1abfed11012b5cd638f5540dcc547c5c9c881f7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
|
(benchmark fuzzsmt
:logic QF_AUFBV
:extrafuns ((a8 Array[14:12]))
:extrafuns ((v1 BitVec[5]))
:status sat
:formula
(let (?n1 bv1[14])
(let (?n2 bv1[12])
(let (?n3 (store a8 ?n1 ?n2))
(flet ($n4 (bvugt v1 v1))
(let (?n5 bv1[1])
(let (?n6 bv0[1])
(let (?n7 (ite $n4 ?n5 ?n6))
(let (?n8 (sign_extend[13] ?n7))
(let (?n9 (store ?n3 ?n8 ?n2))
(let (?n10 bv0[12])
(let (?n11 (store ?n9 ?n1 ?n10))
(let (?n12 bv0[14])
(let (?n13 (select ?n3 ?n12))
(let (?n14 (zero_extend[2] ?n13))
(let (?n15 (store ?n11 ?n14 ?n10))
(let (?n16 (select ?n15 ?n12))
(flet ($n17 (bvsgt ?n16 ?n10))
(let (?n18 (bvnor ?n2 ?n10))
(let (?n19 (zero_extend[2] ?n18))
(let (?n20 (store ?n9 ?n19 ?n10))
(flet ($n21 (= a8 ?n9))
(let (?n22 (ite $n21 ?n5 ?n6))
(let (?n23 (sign_extend[13] ?n22))
(let (?n24 (select ?n20 ?n23))
(let (?n25 (zero_extend[2] ?n24))
(let (?n26 (select ?n3 ?n25))
(flet ($n27 (bvuge ?n10 ?n26))
(flet ($n28 (= ?n9 ?n15))
(flet ($n29 false)
(flet ($n30 (bvsle ?n24 ?n10))
(flet ($n31 (if_then_else $n28 $n29 $n30))
(let (?n32 (sign_extend[11] ?n5))
(flet ($n33 (= ?n9 ?n20))
(let (?n34 (ite $n33 ?n5 ?n6))
(let (?n35 (sign_extend[13] ?n34))
(let (?n36 (select ?n3 ?n35))
(let (?n37 (bvor ?n18 ?n36))
(flet ($n38 (bvsge ?n32 ?n37))
(flet ($n39 (if_then_else $n31 $n38 $n31))
(flet ($n40 (implies $n27 $n39))
(let (?n41 (store a8 ?n12 ?n10))
(flet ($n42 (= ?n3 ?n41))
(flet ($n43 (or $n40 $n42))
(flet ($n44 (implies $n17 $n43))
$n44
)))))))))))))))))))))))))))))))))))))))))))))
|
