1(benchmark fuzzsmt
2:logic QF_LRA
3:status sat
4:extrafuns ((v0 Real))
5:formula
6(let (?e1 12)
7(let (?e2 1)
8(let (?e3 (~ v0))
9(let (?e4 (+ v0 v0))
10(let (?e5 (/ ?e1 ?e1))
11(let (?e6 (+ ?e4 ?e3))
12(let (?e7 (* ?e6 ?e1))
13(let (?e8 (- ?e3 ?e6))
14(let (?e9 (~ ?e8))
15(let (?e10 (+ ?e8 ?e5))
16(let (?e11 (/ ?e2 (~ ?e1)))
17(flet ($e12 (> ?e7 ?e9))
18(flet ($e13 (< ?e4 ?e6))
19(flet ($e14 (distinct ?e9 ?e3))
20(flet ($e15 (<= ?e5 ?e8))
21(flet ($e16 (<= ?e8 ?e8))
22(flet ($e17 (distinct ?e5 v0))
23(flet ($e18 (>= ?e10 v0))
24(flet ($e19 (> ?e10 ?e7))
25(flet ($e20 (distinct ?e7 ?e9))
26(flet ($e21 (<= ?e6 ?e3))
27(flet ($e22 (<= ?e11 ?e4))
28(let (?e23 (ite $e12 ?e3 ?e4))
29(let (?e24 (ite $e19 ?e3 ?e11))
30(let (?e25 (ite $e20 v0 ?e5))
31(let (?e26 (ite $e18 ?e8 v0))
32(let (?e27 (ite $e19 ?e7 ?e8))
33(let (?e28 (ite $e20 ?e10 v0))
34(let (?e29 (ite $e13 ?e9 ?e3))
35(let (?e30 (ite $e20 ?e6 ?e6))
36(let (?e31 (ite $e20 ?e8 ?e24))
37(let (?e32 (ite $e21 ?e10 ?e4))
38(let (?e33 (ite $e18 ?e5 ?e10))
39(let (?e34 (ite $e16 ?e27 ?e5))
40(let (?e35 (ite $e13 ?e5 ?e26))
41(let (?e36 (ite $e19 ?e7 ?e6))
42(let (?e37 (ite $e15 ?e30 ?e31))
43(let (?e38 (ite $e17 ?e28 ?e37))
44(let (?e39 (ite $e22 ?e28 ?e9))
45(let (?e40 (ite $e14 ?e31 ?e28))
46(flet ($e41 (<= ?e4 ?e34))
47(flet ($e42 (<= ?e3 ?e3))
48(flet ($e43 (<= ?e31 ?e37))
49(flet ($e44 (distinct ?e28 ?e36))
50(flet ($e45 (>= v0 ?e26))
51(flet ($e46 (= ?e24 ?e30))
52(flet ($e47 (< ?e38 ?e32))
53(flet ($e48 (> ?e6 ?e29))
54(flet ($e49 (<= ?e25 ?e25))
55(flet ($e50 (> ?e30 ?e30))
56(flet ($e51 (> ?e11 v0))
57(flet ($e52 (<= ?e10 ?e31))
58(flet ($e53 (>= ?e28 ?e36))
59(flet ($e54 (>= v0 ?e33))
60(flet ($e55 (<= ?e33 ?e26))
61(flet ($e56 (distinct ?e37 ?e5))
62(flet ($e57 (distinct ?e10 ?e39))
63(flet ($e58 (> ?e8 ?e39))
64(flet ($e59 (< ?e24 ?e34))
65(flet ($e60 (<= v0 ?e25))
66(flet ($e61 (< ?e33 ?e31))
67(flet ($e62 (distinct ?e7 ?e25))
68(flet ($e63 (< ?e34 ?e4))
69(flet ($e64 (= ?e27 ?e37))
70(flet ($e65 (> ?e5 ?e30))
71(flet ($e66 (>= ?e11 ?e8))
72(flet ($e67 (> ?e6 ?e31))
73(flet ($e68 (<= ?e4 ?e3))
74(flet ($e69 (> ?e9 ?e37))
75(flet ($e70 (< ?e25 ?e6))
76(flet ($e71 (< ?e40 ?e34))
77(flet ($e72 (< ?e9 ?e29))
78(flet ($e73 (< ?e8 ?e35))
79(flet ($e74 (distinct ?e25 ?e5))
80(flet ($e75 (>= ?e8 ?e7))
81(flet ($e76 (<= ?e38 ?e37))
82(flet ($e77 (> ?e5 ?e39))
83(flet ($e78 (>= ?e34 v0))
84(flet ($e79 (>= ?e11 ?e5))
85(flet ($e80 (>= ?e40 ?e3))
86(flet ($e81 (= ?e23 ?e29))
87(flet ($e82 (implies $e52 $e15))
88(flet ($e83 (implies $e16 $e75))
89(flet ($e84 (or $e22 $e59))
90(flet ($e85 (or $e66 $e63))
91(flet ($e86 (xor $e78 $e43))
92(flet ($e87 (or $e73 $e71))
93(flet ($e88 (if_then_else $e18 $e80 $e55))
94(flet ($e89 (xor $e83 $e54))
95(flet ($e90 (if_then_else $e42 $e88 $e42))
96(flet ($e91 (not $e72))
97(flet ($e92 (or $e49 $e68))
98(flet ($e93 (and $e84 $e51))
99(flet ($e94 (iff $e70 $e19))
100(flet ($e95 (not $e93))
101(flet ($e96 (implies $e82 $e13))
102(flet ($e97 (iff $e69 $e64))
103(flet ($e98 (or $e87 $e76))
104(flet ($e99 (if_then_else $e94 $e20 $e96))
105(flet ($e100 (implies $e46 $e98))
106(flet ($e101 (or $e61 $e90))
107(flet ($e102 (or $e92 $e74))
108(flet ($e103 (implies $e97 $e62))
109(flet ($e104 (and $e89 $e77))
110(flet ($e105 (iff $e48 $e67))
111(flet ($e106 (if_then_else $e14 $e14 $e103))
112(flet ($e107 (xor $e58 $e102))
113(flet ($e108 (implies $e99 $e86))
114(flet ($e109 (or $e57 $e21))
115(flet ($e110 (implies $e12 $e108))
116(flet ($e111 (and $e17 $e101))
117(flet ($e112 (or $e107 $e81))
118(flet ($e113 (and $e44 $e44))
119(flet ($e114 (iff $e41 $e111))
120(flet ($e115 (implies $e60 $e56))
121(flet ($e116 (and $e79 $e115))
122(flet ($e117 (or $e114 $e53))
123(flet ($e118 (xor $e110 $e95))
124(flet ($e119 (xor $e104 $e105))
125(flet ($e120 (and $e117 $e85))
126(flet ($e121 (not $e50))
127(flet ($e122 (if_then_else $e120 $e47 $e119))
128(flet ($e123 (if_then_else $e112 $e100 $e91))
129(flet ($e124 (and $e45 $e121))
130(flet ($e125 (implies $e118 $e123))
131(flet ($e126 (xor $e106 $e113))
132(flet ($e127 (xor $e122 $e65))
133(flet ($e128 (implies $e127 $e116))
134(flet ($e129 (not $e125))
135(flet ($e130 (iff $e128 $e124))
136(flet ($e131 (and $e109 $e109))
137(flet ($e132 (and $e129 $e129))
138(flet ($e133 (xor $e131 $e130))
139(flet ($e134 (iff $e126 $e133))
140(flet ($e135 (implies $e132 $e132))
141(flet ($e136 (or $e134 $e134))
142(flet ($e137 (implies $e136 $e136))
143(flet ($e138 (or $e135 $e135))
144(flet ($e139 (implies $e138 $e137))
145$e139
146))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
147
148