Friedrich's Christmas Hangover - X-MAS CTF 2018 Writeup

z3_solve.py

#! /usr/bin/python

from z3 import *

# Solution for Friedrich's Christmas Hangover Challenge for X-MAS CTF 2018

s = Solver()

i1 = Int('i1')
i2 = Int('i2')
i3 = Int('i3')
i4 = Int('i4')
i5 = Int('i5')
i6 = Int('i6')
i7 = Int('i7')
i8 = Int('i8')
i9 = Int('i9')
i10 = Int('i10')
i11 = Int('i11')
i12 = Int('i12')
i13 = Int('i13')
i14 = Int('i14')
i15 = Int('i15')
i16 = Int('i16')
i17 = Int('i17')
i18 = Int('i18')
i19 = Int('i19')
i20 = Int('i20')
i21 = Int('i21')
i22 = Int('i22')
i23 = Int('i23')
i24 = Int('i24')
i25 = Int('i25')
i26 = Int('i26')
i27 = Int('i27')
i28 = Int('i28')
i29 = Int('i29')
i30 = Int('i30')
i31 = Int('i31')
i32 = Int('i32')
i33 = Int('i33')
i34 = Int('i34')
i35 = Int('i35')
i36 = Int('i36')

s.add(i1 > 0x20)
s.add(i2 > 0x20)
s.add(i3 > 0x20)
s.add(i4 > 0x20)
s.add(i5 > 0x20)
s.add(i6 > 0x20)
s.add(i7 > 0x20)
s.add(i8 > 0x20)
s.add(i9 > 0x20)
s.add(i10 > 0x20)
s.add(i11 > 0x20)
s.add(i12 > 0x20)
s.add(i13 > 0x20)
s.add(i14 > 0x20)
s.add(i15 > 0x20)
s.add(i16 > 0x20)
s.add(i17 > 0x20)
s.add(i18 > 0x20)
s.add(i19 > 0x20)
s.add(i20 > 0x20)
s.add(i21 > 0x20)
s.add(i22 > 0x20)
s.add(i23 > 0x20)
s.add(i24 > 0x20)
s.add(i25 > 0x20)
s.add(i26 > 0x20)
s.add(i27 > 0x20)
s.add(i28 > 0x20)
s.add(i29 > 0x20)
s.add(i30 > 0x20)
s.add(i31 > 0x20)
s.add(i32 > 0x20)
s.add(i33 > 0x20)
s.add(i34 > 0x20)
s.add(i35 > 0x20)
s.add(i36 > 0x20)

s.add(i1 <= 0x7E)
s.add(i2 <= 0x7E)
s.add(i3 <= 0x7E)
s.add(i4 <= 0x7E)
s.add(i5 <= 0x7E)
s.add(i6 <= 0x7E)
s.add(i7 <= 0x7E)
s.add(i8 <= 0x7E)
s.add(i9 <= 0x7E)
s.add(i10 <= 0x7E)
s.add(i11 <= 0x7E)
s.add(i12 <= 0x7E)
s.add(i13 <= 0x7E)
s.add(i14 <= 0x7E)
s.add(i15 <= 0x7E)
s.add(i16 <= 0x7E)
s.add(i17 <= 0x7E)
s.add(i18 <= 0x7E)
s.add(i19 <= 0x7E)
s.add(i20 <= 0x7E)
s.add(i21 <= 0x7E)
s.add(i22 <= 0x7E)
s.add(i23 <= 0x7E)
s.add(i24 <= 0x7E)
s.add(i25 <= 0x7E)
s.add(i26 <= 0x7E)
s.add(i27 <= 0x7E)
s.add(i28 <= 0x7E)
s.add(i29 <= 0x7E)
s.add(i30 <= 0x7E)
s.add(i31 <= 0x7E)
s.add(i32 <= 0x7E)
s.add(i33 <= 0x7E)
s.add(i34 <= 0x7E)
s.add(i35 <= 0x7E)
s.add(i36 <= 0x7E)

s.add(i1 * 113 + i2 * 9 + i3 * 62 + i4 * 255 + i5 * 168 + i6 * 139 + i7 * 193 + i8 * 15 + i9 * 126 + i10 * 17 + i11 * 112 + i12 * 174 + i13 * 74 + i14 * 87 + i15 * 250 + i16 * 40 + i17 * 251 + i18 * 103 + i19 * 143 + i20 * 223 + i21 *176 + i22 * 100 + i23 * 33 + i24 * 196 + i25 * 206 + i26 * 168 + i27 * 49 + i28 * 49 + i29 * 75 + i30 * 25 + i31 * 154 + i32 * 82 + i33 * 157 + i34 * 161 + i35 * 27 + i36 * 130 == 0x606eb)

s.add(i1 * 173 + i2 * 186 + i3 * 213 + i4 * 80 + i5 * 242 + i6 * 178 + i7 * 173 + i8 * 241 + i9 * 225 + i10 * 151 + i11 * 230 + i12 * 56 + i13 * 83 + i14 * 215 + i15 * 3 + i16 * 188 + i17 * 236 + i18 * 237 + i19 * 59 + i20 * 252 + i21 * 55 + i22 * 38 + i23 * 194 + i24 * 170 + i25 * 236 + i26 * 15 + i27 * 141 + i28 * 61 + i29 * 254 + i30 * 47 + i31 * 169 + i32 * 12 + i33 * 160 + i34 * 9 + i35 * 27 + i36 * 237 == 0x6dcb8)

s.add(i1 * 71 + i2 * 211 + i3 * 212 + i4 * 104 + i5 * 214 + i6 * 94 + i7 * 80 + i8 * 199 + i9 * 62 + i10 * 224 + i11 * 31 + i12 * 160 + i13 * 113 + i14 * 105 + i15 * 51 + i16 * 148 + i17 * 193 + i18 * 33 + i19 * 112 + i20 * 27 + i21 * 40 + i22 * 36 + i23 * 220 + i24 * 197 + i25 * 78 + i26 * 234 + i27 * 82 + i28 * 58 + i29 * 235 + i30 * 50 + i31 * 39 + i32 * 38 + i33 * 236 + i34 * 227 + i35 * 15 + i36 * 42 == 0x5ac28)

s.add(i1 * 233 + i2 * 202 + i3 * 174 + i4 * 98 + i5 * 89 + i6 * 151 + i7 * 23 + i8 * 46 + i9 * 131 + i10 * 59 + i11 * 98 + i12 * 202 + i13 * 64 + i14 * 136 + i15 * 219 + i16 * 122 + i17 * 249 + i18 * 188 + i19 * 44 + i20 * 180 + i21 * 14 + i22 * 130 + i23 * 66 + i24 * 191 + i25 * 76 + i26 * 142 + i27 * 214 + i28 * 162 + i29 * 192 + i30 * 197 + i31 * 236 + i32 * 113 + i33 * 36 + i34 * 45 + i35 * 183 + i36 * 18 == 0x62b72)

s.add(i1 * 138 + i2 * 131 + i3 * 139 + i4 * 154 + i5 * 140 + i6 * 32 + i7 * 233 + i8 * 18 + i9 * 126 + i10 * 8 + i11 * 101 + i12 * 17 + i13 * 130 + i14 * 182 + i15 * 75 + i16 * 160 + i17 * 174 + i18 * 184 + i19 * 99 + i20 * 214 + i21 * 133 + i22 * 156 + i23 * 128 + i24 * 188 + i25 * 147 + i26 * 143 + i27 * 170 + i28 * 73 + i29 * 102 + i30 * 28 + i31 * 94 + i32 * 63 + i33 * 196 + i34 * 242 + i35 * 41 + i36 * 157 == 0x60332)

s.add(i1 * 7 + i2 * 34 + i3 * 46 + i4 * 228 + i5 * 108 + i6 * 214 + i7 * 27 + i8 * 192 + i9 * 193 + i10 * 254 + i11 * 148 + i12 * 133 + i13 * 181 + i14 * 213 + i15 * 193 + i16 * 181 + i17 * 159 + i18 * 222 + i19 * 245 + i20 * 159 + i21 * 142 + i22 * 207 + i23 * 146 + i24 * 88 + i25 * 180 + i26 * 254 + i27 * 238 + i28 * 103 + i29 * 206 + i30 * 254 + i31 * 219 + i32 * 78 + i33 * 176 + i34 * 235 + i35 * 157 + i36 * 250 == 0x8589f)

s.add(i1 * 72 + i2 * 213 + i3 * 201 + i4 * 174 + i5 * 240 + i6 * 243 + i7 * 75 + i8 * 197 + i9 * 108 + i10 * 48 + i11 * 32 + i12 * 75 + i13 * 44 + i14 * 249 + i15 * 206 + i16 * 26 + i17 * 135 + i18 * 101 + i19 * 230 + i20 * 71 + i21 * 243 + i22 * 251 + i23 * 204 + i24 * 220 + i25 * 254 + i26 * 168 + i27 * 13 + i28 * 208 + i29 * 54 + i30 * 167 + i31 * 195 + i32 * 138 + i33 * 105 + i34 * 173 + i35 * 135 + i36 * 170 == 0x75f44)

s.add(i1 * 184 + i2 * 158 + i3 * 169 + i4 * 136 + i5 * 39 + i6 * 31 + i7 * 67 + i8 * 28 + i9 * 72 + i10 * 148 + i11 * 85 + i12 * 140 + i13 * 147 + i14 * 217 + i15 * 213 + i16 * 237 + i17 * 32 + i18 * 181 + i19 * 69 + i20 * 30 + i21 * 85 + i22 * 23 + i23 * 66 + i24 * 216 + i25 * 158 + i26 * 22 + i27 * 1 + i28 * 138 + i29 * 248 + i30 * 213 + i31 * 250 + i32 * 247 + i33 * 11 + i34 * 75 + i35 * 167 + i36 * 37 == 0x5abc9)


s.add(i1 * 254 + i2 * 88 + i3 * 81 + i4 * 232 + i5 * 213 + i6 * 231 + i7 * 155 + i8 * 10 + i9 * 151 + i10 * 31 + i11 * 203 + i12 * 120 + i13 * 85 + i14 * 149 + i15 * 5 + i16 * 55 + i17 * 180 + i18 * 19 + i19 * 34 + i20 * 140 + i21 * 164 + i22 * 22 + i23 * 124 + i24 * 236 + i25 * 108 + i26 * 16 + i27 * 252 + i28 * 255 + i29 * 67 + i30 * 99 + i31 * 47 + i32 * 108 + i33 * 129 + i34 * 86 + i35 * 35 + i36 * 132 == 0x5eb6b)


s.add(i1 * 215 + i2 * 156 + i3 * 79 + i4 * 14 + i5 * 156 + i6 * 26 + i7 * 41 + i8 * 118 + i9 * 88 + i10 * 163 + i11 * 198 + i12 * 20 + i13 * 172 + i14 * 179 + i15 * 28 + i16 * 159 + i17 * 144 + i18 * 124 + i19 * 102 + i20 * 213 + i21 * 53 + i22 * 98 + i23 * 231 + i24 * 130 + i25 * 29 + i26 * 93 + i27 * 185 + i28 * 31 + i29 * 124 + i30 * 11 + i31 * 58 + i32 * 62 + i33 * 30 + i34 * 142 + i35 * 6 + i36 * 38 == 0x4ce54)


s.add(i1 * 154 + i2 * 94 + i3 * 115 + i4 * 10 + i5 * 180 + i6 * 243 + i7 * 159 + i8 * 38 + i9 * 151 + i10 * 121 + i11 * 87 + i12 * 162 + i13 * 218 + i14 * 229 + i15 * 78 + i16 * 113 + i17 * 155 + i18 * 188 + i19 * 9 + i20 * 106 + i21 * 157 + i22 * 130 + i23 * 159 + i24 * 180 + i25 * 152 + i26 * 91 + i27 * 199 + i28 * 184 + i29 * 108 + i30 * 237 + i31 * 229 + i32 * 203 + i33 * 139 + i34 * 205 + i35 * 32 + i36 * 18 == 0x6e0db)


s.add(i1 * 32 + i2 * 244 + i3 * 127 + i4 * 64 + i5 * 157 + i6 * 179 + i7 * 61 + i8 * 14 + i9 * 242 + i10 * 2 + i11 * 204 + i12 * 190 + i13 * 177 + i14 * 7 + i15 * 158 + i16 * 142 + i17 * 23 + i18 * 66 + i19 * 56 + i20 * 163 + i21 * 174 + i22 * 117 + i23 * 145 + i24 * 11 + i25 * 105 + i26 * 206 + i27 * 211 + i28 * 9 + i29 * 253 + i30 * 165 + i31 * 123 + i32 * 15 + i33 * 52 + i34 * 6 + i35 * 156 + i36 * 161 == 0x5fb34)


s.add(i1 * 43 + i2 * 116 + i3 * 177 + i4 * 113 + i5 * 61 + i6 * 39 + i7 * 230 + i8 * 70 + i9 * 100 + i10 * 227 + i11 * 6 + i12 * 83 + i13 * 252 + i14 * 56 + i15 * 183 + i16 * 235 + i17 * 66 + i18 * 159 + i19 * 160 + i20 * 155 + i21 * 76 + i22 * 19 + i23 * 33 + i24 * 177 + i25 * 115 + i26 * 199 + i27 * 20 + i28 * 104 + i29 * 217 + i30 * 180 + i31 * 244 + i32 * 105 + i33 * 49 + i34 * 56 + i35 * 64 + i36 * 11 == 0x573a5)


s.add(i1 * 196 + i2 * 88 + i3 * 189 + i4 * 111 + i5 * 151 + i6 * 137 + i7 * 3 + i8 * 136 + i9 * 121 + i10 * 180 + i11 * 10 + i12 * 24 + i13 * 24 + i14 * 17 + i15 * 189 + i16 * 51 + i17 * 85 + i18 * 42 + i19 * 154 + i20 * 137 + i21 * 125 + i22 * 227 + i23 * 95 + i24 * 247 + i25 * 168 + i26 * 95 + i27 * 193 + i28 * 141 + i29 * 77 + i30 * 199 + i31 * 42 + i32 * 144 + i33 * 51 + i34 * 190 + i35 * 202 + i36 * 254 == 0x621f7)


s.add(i1 * 154 + i2 * 61 + i3 * 70 + i4 * 20 + i5 * 239 + i6 * 16 + i7 * 2 + i8 * 203 + i9 * 174 + i10 * 218 + i11 * 49 + i12 * 103 + i13 * 169 + i14 * 91 + i15 * 114 + i16 * 110 + i17 * 11 + i18 * 94 + i19 * 207 + i20 * 156 + i21 * 7 + i22 * 189 + i23 * 233 + i24 * 126 + i25 * 251 + i26 * 194 + i27 * 4 + i28 * 176 + i29 * 55 + i30 * 161 + i31 * 96 + i32 * 73 + i33 * 22 + i34 * 160 + i35 * 47 + i36 * 157 == 0x5d0bd) 


s.add(i1 * 85 + i2 * 111 + i3 * 102 + i4 * 74 + i5 * 182 + i6 * 184 + i7 * 144 + i8 * 162 + i9 * 66 + i10 * 96 + i11 * 127 + i12 * 171 + i13 * 95 + i14 * 3 + i15 * 103 + i16 * 5 + i17 * 48 + i18 * 131 + i19 * 34 + i20 * 176 + i21 * 53 + i22 * 92 + i23 * 37 + i24 * 25 + i25 * 222 + i26 * 80 + i27 * 158 + i28 * 55 + i29 * 60 + i30 * 58 + i31 * 149 + i32 * 33 + i33 * 61 + i34 * 238 + i35 * 65 + i36 * 93 == 0x4c56b)


s.add(i1 * 199 + i2 * 152 + i3 * 139 + i4 * 149 + i5 * 229 + i6 * 218 + i7 * 188 + i8 * 7 + i9 * 199 + i10 * 134 + i11 * 246 + i12 * 143 + i13 * 72 + i14 * 9 + i15 * 97 + i16 * 108 + i17 * 52 + i18 * 10 + i19 * 67 + i20 * 250 + i21 * 207 + i22 * 181 + i23 * 16 + i24 * 68 + i25 * 166 + i26 * 188 + i27 * 224 + i28 * 143 + i29 * 105 + i30 * 192 + i31 * 179 + i32 * 81 + i33 * 184 + i34 * 48 + i35 * 188 + i36 * 57 == 0x6ae76)


s.add(i1 * 15 + i2 * 29 + i3 * 153 + i4 * 145 + i5 * 22 + i6 * 117 + i7 * 154 + i8 * 192 + i9 * 73 + i10 * 64 + i11 * 145 + i12 * 195 + i13 * 227 + i14 * 105 + i15 * 208 + i16 * 9 + i17 * 42 + i18 * 222 + i19 * 211 + i20 * 136 + i21 * 231 + i22 * 216 + i23 * 35 + i24 * 126 + i25 * 177 + i26 * 103 + i27 * 105 + i28 * 202 + i29 * 85 + i30 * 33 + i31 * 92 + i32 * 185 + i33 * 152 + i34 * 100 + i35 * 236 + i36 * 2 == 0x62309)


s.add(i1 * 7 + i2 * 78 + i3 * 147 + i4 * 214 + i5 * 88 + i6 * 139 + i7 * 77 + i8 * 240 + i9 * 46 + i10 * 65 + i11 * 245 + i12 * 39 + i13 * 211 + i14 * 82 + i15 * 111 + i16 * 198 + i17 * 37 + i18 * 126 + i19 * 13 + i20 * 157 + i21 * 249 + i22 * 0 + i23 * 96 + i24 * 89 + i25 * 156 + i26 * 97 + i27 * 68 + i28 * 184 + i29 * 218 + i30 * 129 + i31 * 128 + i32 * 149 + i33 * 240 + i34 * 233 + i35 * 239 + i36 * 239 == 0x6a537)


s.add(i1 * 212 + i2 * 2 + i3 * 231 + i4 * 249 + i5 * 72 + i6 * 90 + i7 * 139 + i8 * 192 + i9 * 10 + i10 * 228 + i11 * 37 + i12 * 147 + i13 * 30 + i14 * 108 + i15 * 206 + i16 * 200 + i17 * 200 + i18 * 124 + i19 * 81 + i20 * 134 + i21 * 107 + i22 * 13 + i23 * 101 + i24 * 154 + i25 * 195 + i26 * 63 + i27 * 233 + i28 * 187 + i29 * 137 + i30 * 190 + i31 * 95 + i32 * 77 + i33 * 7 + i34 * 159 + i35 * 204 + i36 * 68 == 0x60389)


s.add(i1 * 23 + i2 * 25 + i3 * 47 + i4 * 227 + i5 * 75 + i6 * 2 + i7 * 96 + i8 * 56 + i9 * 220 + i10 * 149 + i11 * 135 + i12 * 208 + i13 * 80 + i14 * 80 + i15 * 141 + i16 * 248 + i17 * 238 + i18 * 70 + i19 * 220 + i20 * 37 + i21 * 237 + i22 * 3 + i23 * 42 + i24 * 236 + i25 * 126 + i26 * 57 + i27 * 144 + i28 * 113 + i29 * 168 + i30 * 166 + i31 * 187 + i32 * 23 + i33 * 131 + i34 * 216 + i35 * 88 + i36 * 124 == 0x612d0)


s.add(i1 * 49 + i2 * 163 + i3 * 65 + i4 * 6 + i5 * 105 + i6 * 42 + i7 * 52 + i8 * 222 + i9 * 25 + i10 * 18 + i11 * 177 + i12 * 93 + i13 * 170 + i14 * 143 + i15 * 196 + i16 * 20 + i17 * 200 + i18 * 58 + i19 * 116 + i20 * 112 + i21 * 171 + i22 * 154 + i23 * 41 + i24 * 246 + i25 * 14 + i26 * 102 + i27 * 66 + i28 * 254 + i29 * 2 + i30 * 173 + i31 * 233 + i32 * 8 + i33 * 105 + i34 * 18 + i35 * 185 + i36 * 78 == 0x50a71)


s.add(i1 * 54 + i2 * 24 + i3 * 184 + i4 * 185 + i5 * 209 + i6 * 187 + i7 * 142 + i8 * 123 + i9 * 174 + i10 * 85 + i11 * 171 + i12 * 190 + i13 * 119 + i14 * 136 + i15 * 72 + i16 * 87 + i17 * 36 + i18 * 67 + i19 * 78 + i20 * 234 + i21 * 232 + i22 * 15 + i23 * 139 + i24 * 91 + i25 * 134 + i26 * 150 + i27 * 226 + i28 * 98 + i29 * 234 + i30 * 71 + i31 * 218 + i32 * 64 + i33 * 197 + i34 * 135 + i35 * 115 + i36 * 242 == 0x6ae39) 


s.add(i1 * 132 + i2 * 3 + i3 * 185 + i4 * 62 + i5 * 160 + i6 * 86 + i7 * 32 + i8 * 5 + i9 * 44 + i10 * 163 + i11 * 219 + i12 * 10 + i13 * 5 + i14 * 132 + i15 * 124 + i16 * 129 + i17 * 128 + i18 * 220 + i19 * 36 + i20 * 59 + i21 * 105 + i22 * 216 + i23 * 200 + i24 * 205 + i25 * 116 + i26 * 218 + i27 * 53 + i28 * 170 + i29 * 110 + i30 * 49 + i31 * 202 + i32 * 187 + i33 * 179 + i34 * 120 + i35 * 3 + i36 * 146 == 0x5d651)


s.add(i1 * 1 + i2 * 254 + i3 * 113 + i4 * 164 + i5 * 232 + i6 * 149 + i7 * 177 + i8 * 219 + i9 * 100 + i10 * 55 + i11 * 180 + i12 * 76 + i13 * 160 + i14 * 99 + i15 * 230 + i16 * 130 + i17 * 30 + i18 * 115 + i19 * 134 + i20 * 103 + i21 * 77 + i22 * 209 + i23 * 6 + i24 * 117 + i25 * 189 + i26 * 37 + i27 * 81 + i28 * 202 + i29 * 39 + i30 * 56 + i31 * 156 + i32 * 81 + i33 * 120 + i34 * 63 + i35 * 65 + i36 * 74 == 0x5b857)


s.add(i1 * 29 + i2 * 156 + i3 * 53 + i4 * 53 + i5 * 216 + i6 * 135 + i7 * 106 + i8 * 251 + i9 * 110 + i10 * 227 + i11 * 184 + i12 * 11 + i13 * 6 + i14 * 46 + i15 * 109 + i16 * 194 + i17 * 209 + i18 * 29 + i19 * 61 + i20 * 42 + i21 * 9 + i22 * 40 + i23 * 34 + i24 * 79 + i25 * 90 + i26 * 134 + i27 * 36 + i28 * 43 + i29 * 155 + i30 * 9 + i31 * 74 + i32 * 188 + i33 * 90 + i34 * 110 + i35 * 64 + i36 * 197 == 0x4e896)


s.add(i1 * 91 + i2 * 31 + i3 * 164 + i4 * 160 + i5 * 170 + i6 * 163 + i7 * 114 + i8 * 33 + i9 * 164 + i10 * 149 + i11 * 158 + i12 * 228 + i13 * 89 + i14 * 239 + i15 * 153 + i16 * 152 + i17 * 55 + i18 * 11 + i19 * 168 + i20 * 242 + i21 * 188 + i22 * 193 + i23 * 231 + i24 * 234 + i25 * 102 + i26 * 70 + i27 * 212 + i28 * 158 + i29 * 150 + i30 * 206 + i31 * 215 + i32 * 242 + i33 * 96 + i34 * 183 + i35 * 212 + i36 * 193 == 0x7a2eb)


s.add(i1 * 38 + i2 * 0 + i3 * 42 + i4 * 95 + i5 * 194 + i6 * 20 + i7 * 114 + i8 * 109 + i9 * 248 + i10 * 180 + i11 * 139 + i12 * 233 + i13 * 176 + i14 * 60 + i15 * 233 + i16 * 4 + i17 * 29 + i18 * 131 + i19 * 249 + i20 * 70 + i21 * 199 + i22 * 173 + i23 * 121 + i24 * 125 + i25 * 187 + i26 * 84 + i27 * 104 + i28 * 134 + i29 * 84 + i30 * 244 + i31 * 0 + i32 * 175 + i33 * 56 + i34 * 155 + i35 * 57 + i36 * 92 == 0x641c1) 


s.add(i1 * 101 + i2 * 74 + i3 * 47 + i4 * 229 + i5 * 36 + i6 * 179 + i7 * 156 + i8 * 76 + i9 * 29 + i10 * 74 + i11 * 65 + i12 * 99 + i13 * 36 + i14 * 215 + i15 * 243 + i16 * 109 + i17 * 211 + i18 * 74 + i19 * 188 + i20 * 213 + i21 * 19 + i22 * 216 + i23 * 25 + i24 * 31 + i25 * 0 + i26 * 11 + i27 * 66 + i28 * 202 + i29 * 60 + i30 * 144 + i31 * 8 + i32 * 101 + i33 * 229 + i34 * 84 + i35 * 184 + i36 * 177 == 0x5845e)


s.add(i1 * 226 + i2 * 211 + i3 * 81 + i4 * 244 + i5 * 173 + i6 * 197 + i7 * 186 + i8 * 217 + i9 * 106 + i10 * 146 + i11 * 36 + i12 * 77 + i13 * 192 + i14 * 171 + i15 * 152 + i16 * 139 + i17 * 198 + i18 * 250 + i19 * 90 + i20 * 216 + i21 * 33 + i22 * 165 + i23 * 213 + i24 * 9 + i25 * 226 + i26 * 59 + i27 * 93 + i28 * 197 + i29 * 15 + i30 * 64 + i31 * 205 + i32 * 21 + i33 * 221 + i34 * 147 + i35 * 205 + i36 * 48 == 0x6c126)


s.add(i1 * 82 + i2 * 108 + i3 * 244 + i4 * 161 + i5 * 181 + i6 * 24 + i7 * 181 + i8 * 237 + i9 * 150 + i10 * 134 + i11 * 208 + i12 * 238 + i13 * 204 + i14 * 70 + i15 * 53 + i16 * 53 + i17 * 128 + i18 * 43 + i19 * 137 + i20 * 98 + i21 * 95 + i22 * 45 + i23 * 182 + i24 * 117 + i25 * 77 + i26 * 252 + i27 * 115 + i28 * 168 + i29 * 137 + i30 * 246 + i31 * 200 + i32 * 32 + i33 * 166 + i34 * 12 + i35 * 25 + i36 * 140 == 0x66950)


s.add(i1 * 44 + i2 * 120 + i3 * 66 + i4 * 132 + i5 * 28 + i6 * 155 + i7 * 52 + i8 * 189 + i9 * 144 + i10 * 30 + i11 * 192 + i12 * 71 + i13 * 133 + i14 * 238 + i15 * 175 + i16 * 173 + i17 * 140 + i18 * 71 + i19 * 84 + i20 * 158 + i21 * 142 + i22 * 191 + i23 * 115 + i24 * 101 + i25 * 164 + i26 * 131 + i27 * 130 + i28 * 97 + i29 * 137 + i30 * 159 + i31 * 233 + i32 * 214 + i33 * 225 + i34 * 159 + i35 * 63 + i36 * 252 == 0x6e5d5)


s.add(i1 * 0 + i2 * 7 + i3 * 26 + i4 * 124 + i5 * 59 + i6 * 27 + i7 * 25 + i8 * 118 + i9 * 194 + i10 * 12 + i11 * 47 + i12 * 76 + i13 * 255 + i14 * 180 + i15 * 31 + i16 * 27 + i17 * 26 + i18 * 147 + i19 * 171 + i20 * 25 + i21 * 136 + i22 * 3 + i23 * 202 + i24 * 55 + i25 * 218 + i26 * 18 + i27 * 42 + i28 * 28 + i29 * 255 + i30 * 59 + i31 * 254 + i32 * 247 + i33 * 150 + i34 * 87 + i35 * 239 + i36 * 8 == 0x4e957)


s.add(i1 * 145 + i2 * 237 + i3 * 63 + i4 * 211 + i5 * 149 + i6 * 51 + i7 * 181 + i8 * 141 + i9 * 187 + i10 * 38 + i11 * 141 + i12 * 22 + i13 * 77 + i14 * 74 + i15 * 8 + i16 * 237 + i17 * 176 + i18 * 82 + i19 * 251 + i20 * 113 + i21 * 116 + i22 * 13 + i23 * 214 + i24 * 97 + i25 * 91 + i26 * 154 + i27 * 76 + i28 * 84 + i29 * 236 + i30 * 211 + i31 * 203 + i32 * 104 + i33 * 123 + i34 * 74 + i35 * 176 + i36 * 110 == 0x6379d)


s.add(i1 * 240 + i2 * 232 + i3 * 206 + i4 * 192 + i5 * 234 + i6 * 212 + i7 * 82 + i8 * 46 + i9 * 20 + i10 * 173 + i11 * 57 + i12 * 140 + i13 * 118 + i14 * 30 + i15 * 51 + i16 * 61 + i17 * 15 + i18 * 115 + i19 * 46 + i20 * 46 + i21 * 55 + i22 * 199 + i23 * 188 + i24 * 45 + i25 * 191 + i26 * 96 + i27 * 118 + i28 * 124 + i29 * 180 + i30 * 122 + i31 * 87 + i32 * 21 + i33 * 225 + i34 * 72 + i35 * 47 + i36 * 249 == 0x60298)


s.add(i1 * 219 + i2 * 121 + i3 * 84 + i4 * 210 + i5 * 24 + i6 * 14 + i7 * 202 + i8 * 11 + i9 * 84 + i10 * 244 + i11 * 227 + i12 * 83 + i13 * 128 + i14 * 88 + i15 * 155 + i16 * 215 + i17 * 218 + i18 * 57 + i19 * 114 + i20 * 243 + i21 * 76 + i22 * 4 + i23 * 211 + i24 * 251 + i25 * 71 + i26 * 200 + i27 * 134 + i28 * 251 + i29 * 207 + i30 * 47 + i31 * 115 + i32 * 47 + i33 * 167 + i34 * 81 + i35 * 83 + i36 * 24 == 0x633a4)

print s.check()
m = s.model()

result = chr(m[i1].as_long()) + chr(m[i2].as_long()) + chr(m[i3].as_long()) + chr(m[i4].as_long()) + chr(m[i5].as_long()) + chr(m[i6].as_long()) + chr(m[i7].as_long()) + chr(m[i8].as_long()) + chr(m[i9].as_long()) + chr(m[i10].as_long()) + chr(m[i11].as_long()) + chr(m[i12].as_long()) + chr(m[i13].as_long()) + chr(m[i14].as_long()) + chr(m[i15].as_long()) + chr(m[i16].as_long()) + chr(m[i17].as_long()) + chr(m[i18].as_long()) + chr(m[i19].as_long()) + chr(m[i20].as_long()) + chr(m[i21].as_long()) + chr(m[i22].as_long()) + chr(m[i23].as_long()) + chr(m[i24].as_long()) + chr(m[i25].as_long()) + chr(m[i26].as_long()) + chr(m[i27].as_long()) + chr(m[i28].as_long()) + chr(m[i29].as_long()) + chr(m[i30].as_long()) + chr(m[i31].as_long()) + chr(m[i32].as_long()) + chr(m[i33].as_long()) + chr(m[i34].as_long()) + chr(m[i35].as_long()) + chr(m[i36].as_long())

print "Flag is: %s" %(result)