blob: b7898b810219252aaceebfc7e4f835acd48bab4f (
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
118
|
(benchmark fuzzsmt
:logic QF_BV
:status sat
:extrafuns ((v0 BitVec[4]))
:extrafuns ((v1 BitVec[4]))
:formula
(let (?e2 bv1[4])
(let (?e3 bv9[4])
(let (?e4 bv12[4])
(let (?e5 bv9[4])
(let (?e6 bv3[4])
(let (?e7 (zero_extend[0] v0))
(let (?e8 (extract[3:2] v1))
(let (?e9 (ite (= ?e6 ?e7) bv1[1] bv0[1]))
(let (?e10 (bvnot v0))
(let (?e11 (ite (= bv1[1] (extract[0:0] ?e4)) ?e10 ?e3))
(let (?e12 (bvadd ?e7 (zero_extend[3] ?e9)))
(let (?e13 (ite (bvule ?e5 ?e4) bv1[1] bv0[1]))
(let (?e14 (bvadd ?e10 ?e3))
(let (?e15 (ite (bvuge ?e3 ?e14) bv1[1] bv0[1]))
(let (?e16 (bvsub ?e10 ?e10))
(let (?e17 (repeat[1] ?e16))
(let (?e18 (rotate_right[0] ?e13))
(let (?e19 (ite (bvugt (zero_extend[3] ?e13) ?e3) bv1[1] bv0[1]))
(let (?e20 (ite (bvsle v0 (zero_extend[3] ?e13)) bv1[1] bv0[1]))
(let (?e21 (bvlshr ?e17 ?e14))
(let (?e22 (sign_extend[0] ?e3))
(let (?e23 (bvsub ?e3 ?e6))
(let (?e24 (bvnot ?e17))
(let (?e25 (bvand ?e4 v0))
(let (?e26 (bvnor ?e14 ?e21))
(let (?e27 (extract[3:1] ?e4))
(let (?e28 (bvmul ?e24 (zero_extend[3] ?e20)))
(let (?e29 (bvneg ?e8))
(let (?e30 (ite (bvuge ?e5 ?e10) bv1[1] bv0[1]))
(let (?e31 (ite (bvugt (sign_extend[3] ?e30) ?e28) bv1[1] bv0[1]))
(let (?e32 (bvlshr ?e6 ?e25))
(let (?e33 (ite (bvslt ?e4 ?e6) bv1[1] bv0[1]))
(let (?e34 (ite (distinct (zero_extend[3] ?e33) ?e24) bv1[1] bv0[1]))
(let (?e35 (ite (= bv1[1] (extract[0:0] ?e14)) ?e11 ?e2))
(flet ($e36 (bvugt ?e8 ?e8))
(flet ($e37 (bvule ?e2 (zero_extend[2] ?e29)))
(flet ($e38 (bvslt ?e21 v0))
(flet ($e39 (distinct (zero_extend[1] ?e27) ?e26))
(flet ($e40 (bvuge ?e25 (zero_extend[3] ?e13)))
(flet ($e41 (bvslt ?e8 ?e29))
(flet ($e42 (bvuge ?e22 ?e28))
(flet ($e43 (bvsgt ?e30 ?e31))
(flet ($e44 (bvsle ?e3 (sign_extend[3] ?e19)))
(flet ($e45 (distinct ?e35 (zero_extend[3] ?e18)))
(flet ($e46 (bvuge ?e3 ?e16))
(flet ($e47 (bvsge ?e28 ?e5))
(flet ($e48 (bvuge ?e16 (zero_extend[3] ?e9)))
(flet ($e49 (= (sign_extend[3] ?e33) ?e24))
(flet ($e50 (bvuge ?e14 (sign_extend[3] ?e9)))
(flet ($e51 (bvsle ?e5 (zero_extend[3] ?e31)))
(flet ($e52 (bvult ?e11 ?e4))
(flet ($e53 (= ?e17 (zero_extend[3] ?e30)))
(flet ($e54 (bvsge ?e28 (sign_extend[3] ?e9)))
(flet ($e55 (bvuge (zero_extend[3] ?e9) ?e25))
(flet ($e56 (bvuge v1 (zero_extend[3] ?e20)))
(flet ($e57 (bvuge ?e6 ?e24))
(flet ($e58 (bvsle ?e3 (zero_extend[3] ?e18)))
(flet ($e59 (= (sign_extend[3] ?e18) ?e4))
(flet ($e60 (bvsge ?e29 ?e8))
(flet ($e61 (bvule (zero_extend[2] ?e8) ?e21))
(flet ($e62 (bvsgt ?e23 ?e16))
(flet ($e63 (bvuge v0 v0))
(flet ($e64 (bvslt ?e12 ?e26))
(flet ($e65 (bvsle (sign_extend[3] ?e9) ?e6))
(flet ($e66 (bvugt ?e32 (sign_extend[3] ?e31)))
(flet ($e67 (bvult ?e11 (zero_extend[3] ?e20)))
(flet ($e68 (bvule ?e2 ?e32))
(flet ($e69 (bvule ?e6 (sign_extend[2] ?e29)))
(flet ($e70 (bvugt ?e24 ?e10))
(flet ($e71 (distinct ?e26 ?e17))
(flet ($e72 (bvslt (sign_extend[3] ?e30) ?e11))
(flet ($e73 (distinct ?e21 (sign_extend[3] ?e31)))
(flet ($e74 (= v0 (sign_extend[1] ?e27)))
(flet ($e75 (bvult (sign_extend[3] ?e18) ?e24))
(flet ($e76 (bvule ?e12 ?e14))
(flet ($e77 (bvsle v1 ?e7))
(flet ($e78 (bvule ?e16 ?e17))
(flet ($e79 (bvuge ?e32 ?e2))
(flet ($e80 (bvslt (sign_extend[2] ?e15) ?e27))
(flet ($e81 (distinct ?e10 ?e21))
(flet ($e82 (bvugt ?e26 (sign_extend[2] ?e8)))
(flet ($e83 (bvule ?e32 (sign_extend[3] ?e34)))
(flet ($e84
(and
(or $e42 (not $e41) $e77)
(or $e53 (not $e47) $e78)
(or (not $e56) $e58 $e43)
(or $e41 $e45 (not $e77))
(or (not $e45) (not $e73) (not $e68))
(or $e68 $e41 (not $e42))
(or (not $e81) (not $e80) (not $e66))
(or $e81 $e67 (not $e42))
(or (not $e66) $e47 (not $e81))
(or (not $e56) (not $e62) (not $e59))
(or (not $e45) (not $e71) $e52)
(or $e58 $e50 (not $e48))
(or $e45 $e56 $e56)
(or $e37 $e61 $e78)
(or (not $e76) (not $e50) (not $e80))
(or (not $e44) (not $e42) $e62)
(or (not $e45) (not $e77) (not $e53))
(or $e41 (not $e68) $e55)
(or $e75 (not $e45) $e65)
(or (not $e58) $e83 (not $e64))
(or $e40 $e78 $e64)
(or (not $e46) $e56 (not $e55))
(or (not $e61) (not $e64) (not $e43))
(or (not $e82) $e48 (not $e73))
))
$e84
))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
|
