blob: b3fad3a2bf518528af27d25c0b4b363162ce95c7 (
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
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
|
(benchmark fuzzsmt
:logic QF_BV
:extrafuns ((v11 BitVec[8]))
:extrafuns ((v12 BitVec[8]))
:extrafuns ((v10 BitVec[12]))
:extrafuns ((v2 BitVec[10]))
:extrafuns ((v8 BitVec[11]))
:extrafuns ((v17 BitVec[8]))
:extrafuns ((v5 BitVec[13]))
:extrafuns ((v0 BitVec[15]))
:extrafuns ((v14 BitVec[14]))
:extrafuns ((v19 BitVec[10]))
:status unsat
:formula
(let (?n1 (sign_extend[2] v11))
(let (?n2 (sign_extend[6] ?n1))
(let (?n3 (zero_extend[2] v14))
(flet ($n4 (bvult ?n2 ?n3))
(flet ($n5 (not $n4))
(let (?n6 bv0[12])
(flet ($n7 (bvslt ?n6 v10))
(let (?n8 bv1[1])
(let (?n9 bv0[1])
(let (?n10 (ite $n7 ?n8 ?n9))
(let (?n11 (sign_extend[15] ?n10))
(let (?n12 bv0[10])
(flet ($n13 (bvslt ?n12 v19))
(let (?n14 (ite $n13 ?n8 ?n9))
(flet ($n15 (= ?n8 ?n14))
(let (?n16 bv0[14])
(let (?n17 (bvxnor v14 ?n16))
(let (?n18 (extract[9:0] v0))
(let (?n19 (sign_extend[4] ?n18))
(let (?n20 bv6240[14])
(let (?n21 (bvxnor ?n19 ?n20))
(let (?n22 (ite $n15 ?n17 ?n21))
(let (?n23 (zero_extend[2] ?n22))
(let (?n24 (bvsub ?n11 ?n23))
(let (?n25 bv0[16])
(flet ($n26 (bvugt ?n24 ?n25))
(flet ($n27 (not $n26))
(flet ($n28 false)
(let (?n29 (zero_extend[2] v8))
(let (?n30 bv0[15])
(flet ($n31 (bvsle v0 ?n30))
(let (?n32 (ite $n31 ?n8 ?n9))
(let (?n33 (zero_extend[12] ?n32))
(let (?n34 (bvshl ?n29 ?n33))
(flet ($n35 (bvsge ?n25 ?n3))
(let (?n36 (ite $n35 ?n8 ?n9))
(let (?n37 (zero_extend[12] ?n36))
(flet ($n38 (bvugt ?n34 ?n37))
(flet ($n39 (not $n38))
(flet ($n40 (distinct ?n3 ?n25))
(let (?n41 (ite $n40 ?n8 ?n9))
(let (?n42 (sign_extend[14] ?n41))
(flet ($n43 (bvsge ?n42 ?n30))
(flet ($n44 (or $n28 $n39 $n43))
(let (?n45 bv0[13])
(let (?n46 (sign_extend[2] v17))
(let (?n47 (zero_extend[3] ?n46))
(flet ($n48 (distinct ?n45 ?n47))
(let (?n49 (ite $n48 ?n8 ?n9))
(let (?n50 (sign_extend[14] ?n49))
(let (?n51 (bvnot ?n30))
(flet ($n52 (bvult ?n50 ?n51))
(let (?n53 (sign_extend[2] v14))
(flet ($n54 (bvuge ?n25 ?n53))
(flet ($n55 (not $n54))
(flet ($n56 (or $n28 $n52 $n55))
(let (?n57 (sign_extend[6] v12))
(flet ($n58 (bvsgt ?n57 ?n21))
(let (?n59 (ite $n58 ?n8 ?n9))
(flet ($n60 (bvugt ?n8 ?n59))
(let (?n61 (zero_extend[1] ?n29))
(let (?n62 (bvmul ?n20 ?n61))
(flet ($n63 (bvsgt ?n45 v5))
(let (?n64 (ite $n63 ?n8 ?n9))
(let (?n65 (zero_extend[13] ?n64))
(flet ($n66 (bvule ?n62 ?n65))
(flet ($n67 (not $n66))
(let (?n68 (sign_extend[4] v2))
(let (?n69 (bvxnor ?n16 ?n68))
(let (?n70 (zero_extend[2] ?n46))
(let (?n71 (zero_extend[2] ?n70))
(flet ($n72 (= ?n69 ?n71))
(let (?n73 (extract[6:3] ?n29))
(let (?n74 (sign_extend[12] ?n73))
(flet ($n75 (bvsle ?n25 ?n74))
(let (?n76 (sign_extend[9] ?n10))
(let (?n77 (bvxnor v2 ?n76))
(let (?n78 (extract[3:3] ?n77))
(flet ($n79 (= ?n8 ?n78))
(let (?n80 (ite $n79 ?n16 ?n57))
(flet ($n81 (bvugt ?n1 ?n12))
(let (?n82 (ite $n81 ?n8 ?n9))
(let (?n83 (bvnot ?n82))
(let (?n84 (zero_extend[13] ?n83))
(flet ($n85 (bvult ?n80 ?n84))
(let (?n86 (ite $n85 ?n8 ?n9))
(let (?n87 (zero_extend[12] ?n86))
(let (?n88 (zero_extend[1] ?n87))
(flet ($n89 (= ?n16 ?n88))
(flet ($n90 (or $n28 $n75 $n89))
(flet ($n91 (and $n5 $n27 $n44 $n56 $n60 $n67 $n72 $n90))
$n91
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
|
