blob: 87cceb8e8ea16901b76b8cc6084bf424710f07a4 (
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
108
109
110
111
112
113
114
115
116
117
|
(benchmark fuzzsmt
:logic QF_BV
:extrafuns ((v2 BitVec[4]))
:extrafuns ((v4 BitVec[4]))
:extrafuns ((v1 BitVec[4]))
:extrafuns ((v0 BitVec[4]))
:extrafuns ((v6 BitVec[4]))
:status unsat
:formula
(let (?n1 bv1[1])
(let (?n2 (extract[1:1] v2))
(flet ($n3 (= ?n1 ?n2))
(let (?n4 bv0[4])
(let (?n5 bv1[4])
(let (?n6 (ite $n3 ?n4 ?n5))
(let (?n7 (bvlshr v2 v4))
(flet ($n8 (bvule ?n6 ?n7))
(let (?n9 bv0[1])
(let (?n10 (ite $n8 ?n1 ?n9))
(flet ($n11 (distinct ?n1 ?n10))
(let (?n12 (ite $n11 ?n1 ?n9))
(let (?n13 (sign_extend[3] ?n12))
(flet ($n14 (bvuge ?n13 ?n5))
(flet ($n15 (bvuge v1 v6))
(let (?n16 (ite $n15 ?n1 ?n9))
(let (?n17 (sign_extend[3] ?n16))
(let (?n18 (bvand v1 ?n17))
(flet ($n19 (bvult ?n18 ?n5))
(let (?n20 (ite $n19 ?n1 ?n9))
(flet ($n21 (bvslt ?n1 ?n20))
(let (?n22 (ite $n21 ?n1 ?n9))
(let (?n23 (zero_extend[1] ?n22))
(let (?n24 bv0[2])
(flet ($n25 (bvsgt ?n23 ?n24))
(let (?n26 (ite $n25 ?n1 ?n9))
(let (?n27 (sign_extend[3] ?n26))
(flet ($n28 (bvsle v2 ?n27))
(let (?n29 (rotate_left[3] v4))
(let (?n30 (bvnot ?n29))
(flet ($n31 (bvslt ?n4 ?n30))
(let (?n32 (ite $n31 ?n1 ?n9))
(let (?n33 (zero_extend[3] ?n32))
(flet ($n34 (bvsge ?n5 ?n33))
(let (?n35 (bvsub ?n5 ?n30))
(let (?n36 bv4[4])
(flet ($n37 (bvule ?n35 ?n36))
(flet ($n38 false)
(flet ($n39 (bvult v0 ?n5))
(let (?n40 (bvshl ?n36 v1))
(let (?n41 (bvmul v4 ?n18))
(flet ($n42 (distinct ?n40 ?n41))
(let (?n43 (ite $n42 ?n1 ?n9))
(let (?n44 bv1[2])
(let (?n45 (bvnor v1 ?n30))
(flet ($n46 (bvuge ?n45 v6))
(let (?n47 (ite $n46 ?n1 ?n9))
(let (?n48 (sign_extend[3] ?n47))
(flet ($n49 (bvult ?n4 ?n48))
(let (?n50 (ite $n49 ?n1 ?n9))
(let (?n51 (sign_extend[1] ?n50))
(flet ($n52 (bvule ?n44 ?n51))
(let (?n53 (ite $n52 ?n1 ?n9))
(flet ($n54 (= ?n43 ?n53))
(let (?n55 (ite $n54 ?n1 ?n9))
(let (?n56 (sign_extend[3] ?n55))
(flet ($n57 (bvugt ?n5 ?n56))
(flet ($n58 (or $n38 $n39 $n57))
(let (?n59 (sign_extend[3] ?n1))
(let (?n60 (bvmul v2 ?n36))
(let (?n61 (bvnor ?n5 ?n60))
(let (?n62 (bvadd ?n59 ?n61))
(flet ($n63 (bvsge ?n62 ?n4))
(flet ($n64 (bvugt ?n59 v2))
(flet ($n65 (bvsge v6 ?n61))
(let (?n66 (ite $n65 ?n1 ?n9))
(let (?n67 (bvshl v1 v0))
(flet ($n68 (bvuge ?n4 ?n40))
(let (?n69 (ite $n68 ?n1 ?n9))
(let (?n70 (bvxnor ?n9 ?n69))
(let (?n71 (sign_extend[3] ?n70))
(flet ($n72 (bvuge v6 ?n71))
(let (?n73 (ite $n72 ?n1 ?n9))
(let (?n74 (zero_extend[3] ?n73))
(flet ($n75 (bvsle ?n67 ?n74))
(let (?n76 (ite $n75 ?n1 ?n9))
(flet ($n77 (bvugt ?n66 ?n76))
(flet ($n78 (or $n38 $n64 $n77))
(flet ($n79 (bvult ?n4 ?n18))
(let (?n80 (ite $n79 ?n1 ?n9))
(flet ($n81 (bvule ?n1 ?n80))
(flet ($n82 (not $n81))
(let (?n83 (sign_extend[1] ?n66))
(flet ($n84 (= ?n24 ?n83))
(flet ($n85 (or $n38 $n82 $n84))
(flet ($n86 (bvuge ?n29 ?n62))
(flet ($n87 (bvsgt ?n45 ?n4))
(let (?n88 (ite $n87 ?n1 ?n9))
(flet ($n89 (bvsge ?n10 ?n88))
(flet ($n90 (bvsgt ?n4 v0))
(let (?n91 (ite $n90 ?n1 ?n9))
(let (?n92 (zero_extend[3] ?n91))
(flet ($n93 (bvsgt v0 ?n92))
(flet ($n94 (or $n38 $n89 $n93))
(let (?n95 (bvcomp ?n4 ?n7))
(let (?n96 (sign_extend[3] ?n95))
(flet ($n97 (bvugt ?n96 ?n5))
(let (?n98 (ite $n97 ?n1 ?n9))
(flet ($n99 (bvsgt ?n98 ?n1))
(flet ($n100 (bvule ?n45 ?n5))
(let (?n101 (ite $n100 ?n1 ?n9))
(flet ($n102 (bvslt ?n101 ?n9))
(flet ($n103 (bvsge v2 ?n59))
(let (?n104 (ite $n103 ?n1 ?n9))
(flet ($n105 (bvugt ?n104 ?n9))
(flet ($n106 (and $n14 $n28 $n34 $n37 $n58 $n63 $n78 $n85 $n86 $n94 $n99 $n102 $n105))
$n106
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
|
