from z3 import *
v3=Int('v3')
v4=Int('v4')
v5=Int('v5')
v6=Int('v6')
v7=Int('v7')
v8=Int('v8')
v9=Int('v9')
v10=Int('v10')
v11=Int('v11')
v12=Int('v12')
v13=Int('v13')
v14=Int('v14')
v15=Int('v15')
v16=Int('v16')
v17=Int('v17')
v18=Int('v18')
v19=Int('v19')
v20=Int('v20')
v21=Int('v21')
v22=Int('v22')
v23=Int('v23')
v24=Int('v24')
v25=Int('v25')
v26=Int('v26')
v27=Int('v27')
v28=Int('v28')
v29=Int('v29')
v30=Int('v30')
v31=Int('v31')
v32=Int('v32')
v33=Int('v33')
v34=Int('v34')
s=Solver()
s.add(48 * v34 + 174 * v33 + 111 * v32 + 108 * v31 + 92 * v30 + 194 * v29 + 124 * v28 + 240 * v27 + 126 * v26 + 81 * v25 + 144 * v24 + 103 * v23 + 161 * v22 + 50 * v21 + 67 * v20 + 15 * v19 + 127 * v18 + 232 * v17 + 188 * v16 + 19 * v15 + 233 * v14 + 153 * v13 + 231 * v12 + 40 * v11 + 112 * v10 + 106 * v9 + 135 * v8 + 90 * v7 + 67 * v6 + 20 * v5 + 248 * v4 + 45 * v3 == 359512)
s.add(13 * v34 + 101 * v33 + 78 * v32 + 227 * v31 + 195 * v30 + 81 * v29 + 10 * v28 + 248 * v27 + 186 * v26 + 171 * v25 + 148 * v24 + 194 * v23 + 40 * v22 + 180 * v21 + 17 * v20 + 212 * v19 + 104 * v18 + 90 * v17 + 178 * v16 + 26 * v15 + 225 * v14 + 209 * v13 + 32 * v12 + 169 * v11 + 94 * v10 + 156 * v9 + 154 * v8 + 56 * v7 + 244 * v6 + 149 * v5 + 120 * v4 + 131 * v3 == 387514)
s.add(240 * v34 + 53 * v33 + 44 * v32 + 83 * v31 + 95 * v30 + 131 * v29 + 30 * v28 + 55 * v27 + 46 * v26 + 36 * v25 + 67 * v24 + 109 * v23 + 69 * v22 + 8 * v20 + 248 * v19 + 40 * v18 + 154 * v17 + 86 * v15 + 251 * (v16 + v21) + 112 * v14 + 9 * v13 + 174 * v12 + 197 * v11 + 38 * v10 + 14 * v9 + 202 * v8 + 60 * v7 + 117 * v6 + 188 * v5 + 136 * v4 + 145 * v3 == 301487)
s.add(234 * (v34 + v15) + 25 * (v33 + v3) + 162 * v32 + 152 * v31 + 112 * v30 + 57 * v29 + 102 * v28 + 182 * v27 + 10 * v26 + 139 * v25 + 30 * v24 + 7 * v23 + 145 * v22 + 127 * v21 + 148 * v20 + 5 * v19 + 165 * v18 + 109 * v17 + 110 * v16 + 113 * v14 + 33 * v13 + 192 * v12 + 45 * v11 + 65 * v10 + 105 * v9 + 140 * v8 + 116 * v7 + 35 * v6 + 48 * v5 + 155 * v4 == 296549)
s.add(82 * v34 + 113 * v33 + 189 * v32 + 101 * v31 + 236 * v30 + 118 * v29 + 141 * v28 + 148 * v27 + 197 * v26 + 7 * v25 + 104 * v23 + 45 * v22 + 130 * v21 + 39 * v20 + 164 * v19 + 88 * v18 + 241 * v17 + 107 * v15 + 108 * (v16 + v24) + 76 * v14 + 34 * v13 + 210 * v12 + 29 * v11 + 156 * v10 + 90 * v9 + 139 * v8 + 151 * v7 + 10 * v6 + 97 * v5 + 209 * v4 + 46 * v3 == 344514)
s.add(179 * v34 + 72 * (v33 + v16) + 13 * v32 + 182 * v31 + 50 * v30 + 102 * v29 + 155 * v28 + 230 * v27 + 3 * v26 + 225 * v25 + 237 * v24 + 163 * v23 + 38 * v22 + 176 * v21 + 115 * v20 + 105 * v19 + 203 * v18 + 26 * v17 + 111 * v15 + 96 * v14 + 240 * v13 + 139 * v12 + 117 * v11 + 153 * v10 + 120 * v9 + 151 * v8 + 25 * v7 + 49 * v6 + 90 * v5 + 98 * v4 + 7 * v3 == 346892)
s.add(156 * v34 + 61 * v33 + 150 * v32 + 170 * v31 + 110 * v28 + 99 * v27 + 127 * v26 + 101 * (v25 + v29) + 203 * v24 + 209 * v23 + 100 * v21 + 226 * (v20 + v30) + 186 * v19 + 252 * v18 + 39 * v17 + 65 * v16 + 67 * v15 + 225 * v14 + 174 * v13 + v12 + 214 * v10 + 187 * (v11 + v22) + 22 * v9 + 74 * v8 + 99 * v7 + 129 * v6 + 254 * v5 + 13 * v4 + 97 * v3 == 386678)
s.add(154 * v34 + 117 * v33 + 88 * v32 + v31 + 118 * v30 + 232 * v29 + 60 * v28 + 252 * v27 + 133 * v26 + 177 * v25 + 185 * v24 + 222 * v23 + 32 * v22 + 48 * v21 + v20 + 242 * v19 + 240 * v18 + 218 * v17 + 81 * v16 + 22 * v15 + 73 * v14 + 171 * v13 + 139 * v12 + 72 * v11 + 106 * v10 + 62 * v9 + 156 * v8 + 134 * v7 + 220 * v6 + 19 * v5 + 77 * v4 + 94 * v3 == 348667)
s.add(220 * v34 + 151 * v33 + 173 * v32 + 189 * v31 + 41 * v30 + 39 * v29 + 26 * v28 + 232 * v27 + 75 * v26 + 75 * v25 + 95 * v24 + 7 * v23 + 117 * v22 + 96 * v21 + 211 * v20 + 130 * v19 + 228 * v18 + 143 * v17 + 91 * v16 + 247 * v15 + 43 * v14 + 122 * v13 + 131 * v12 + 52 * v11 + 48 * v10 + 29 * v9 + 111 * v8 + 38 * v7 + 19 * v6 + 242 * v5 + 162 * v4 + 70 * v3 == 316884)
s.add(231 * v34 + 92 * v33 + 136 * v32 + 236 * v31 + 147 * v30 + 104 * v29 + 79 * v28 + 204 * v27 + 220 * v26 + 25 * v25 + 38 * v24 + 233 * v23 + 165 * v22 + 20 * v21 + 174 * v20 + 120 * v19 + 214 * v18 + 18 * v17 + 233 * v16 + 119 * v15 + 244 * v14 + 143 * v13 + 126 * v12 + 226 * v11 + 77 * v10 + 33 * v9 + 189 * v8 + 5 * v7 + 150 * v6 + 160 * v5 + 14 * v4 + 112 * v3 == 372620)
s.add(50 * v34+ 203 * v33+ 38 * v32+ 191 * v31+ 193 * v30+ 250 * v29+ 212 * v28+ 175 * v27+ 39 * v26+ 94 * v25+ 183 * v24+ 172 * v23+ 171 * v22+ 163 * v21+ 129 * v20+ 165 * v19+ ((v18 * 64))+ 170 * v17+ 199 * v16+ 167 * v14+ 216 * v12+ 2 * (v13 + v15)+ 252 * v11+ 184 * v10+ 187 * v9+ 97 * v8+ 109 * v7+ 98 * v6+ 135 * v5+ 192 * v4+ 88 * v3 == 413102)
s.add(43 * v34+ 196 * v33+ 81 * v32+ 203 * v31+ 252 * v30+ 104 * v29+ 248 * v28+ 156 * v27+ 199 * v26+ 46 * v25+ 240 * v23+ 149 * v22+ 155 * v21+ 102 * v20+ 95 * v19+ 51 * v18+ 62 * v15+ 58 * v14+ 208 * (v17 + v24 + v16)+ 117 * v13+ 72 * v12+ 23 * v11+ 193 * v10+ 193 * v9+ 226 * v8+ 217 * v7+ 106 * v6+ 147 * v5+ 136 * v4+ 16 * v3 == 428661)
s.add(80 * v34+ 49 * v33+ 69 * v32+ 144 * v31+ 224 * v30+ 107 * v29+ 225 * v28+ 83 * v27+ 15 * v26+ 10 * v25+ 214 * v24+ 152 * v23+ 24 * v22+ 136 * v21+ 165 * v20+ 208 * v19+ 38 * v18+ 67 * v17+ 201 * v16+ 180 * v15+ 158 * v14+ 75 * v13+ 111 * v12+ 65 * v11+ 211 * v10+ 220 * v9+ 135 * v8+ 125 * v7+ 216 * v6+ 105 * v5+ 122 * v4+ 112 * v3 == 371484)
s.add(76 * v34+ 129 * v33+ 68 * v32+ 143 * v31+ 127 * v30+ 51 * v29+ 88 * v27+ 153 * v26+ 9 * v25+ 149 * v24+ 107 * v23+ 178 * v22+ 166 * v21+ 190 * v20+ 177 * v19+ 99 * v18+ 71 * v17+ 63 * v16+ 233 * v15+ 58 * v14+ 132 * v13+ 109 * v12+ 75 * v11+ 95 * v9+ 152 * (v10 + v28)+ 74 * v8+ 195 * v7+ 90 * v6+ 251 * v5+ 205 * v4+ 8 * v3 == 350848)
s.add(31 * v34+ 102 * v33+ 146 * v32+ 209 * v31+ 59 * v30+ 38 * v29+ 40 * v28+ 56 * v27+ 182 * v26+ 245 * v25+ 67 * v24+ 202 * v23+ 177 * v22+ 26 * v20+ 126 * v19+ 161 * v18+ 95 * v17+ 133 * v16+ 123 * v15+ 163 * v14+ 30 * v13+ 88 * v12+ 219 * v11+ 5 * v10+ 86 * v9+ 156 * v7+ 183 * (v8 + v21)+ 253 * v6+ 97 * v5+ 43 * v4+ (v3 * 128) == 334408)
s.add(91 * v34+ 136 * v33+ 223 * v32+ 146 * v31+ 137 * v30+ 228 * v29+ 226 * v28+ 155 * v27+ 170 * v26+ 92 * v25+ 77 * v24+ 17 * v23+ 22 * v22+ (v21 * 128)+ 20 * v20+ 171 * v19+ 142 * v18+ 170 * v17+ 192 * v16+ 49 * v15+ 200 * v14+ 178 * v13+ 154 * v12+ 42 * v11+ 5 * v10+ 159 * v9+ 251 * v8+ 152 * v7+ 7 * v6+ 247 * v5+ 145 * v4+ 39 * v3 == 382822)
s.add(121 * v34+ 205 * (v33 + v25)+ 204 * v32+ 169 * v31+ 244 * v30+ 26 * v29+ 77 * v28+ 134 * v27+ 221 * v26+ 149 * v24+ 47 * v23+ v22+ 197 * v21+ 82 * v20+ 195 * v19+ 123 * v18+ 219 * v17+ 116 * v16+ 80 * v15+ 13 * v14+ 231 * v13+ 173 * v12+ 192 * v11+ 220 * v10+ 224 * v9+ 108 * v8+ 104 * v7+ 56 * v6+ 152 * v5+ 84 * v4+ 226 * v3 == 420160)
s.add(73 * v34+ 95 * v33+ 45 * v32+ 184 * v31+ 176 * v30+ 161 * v27+ 142 * v26+ 171 * v25+ 215 * v24+ 83 * v23+ 233 * v22+ 184 * v21+ 171 * v20+ 182 * v19+ 126 * (v18 + v29)+ 111 * v17+ 118 * (v16 + v28)+ 67 * v15+ 92 * v14+ 219 * v13+ 70 * v12+ 252 * v11+ 194 * v10+ 21 * v9+ 245 * v8+ 204 * v7+ 48 * v6+ 150 * v5+ 39 * v4+ 85 * v3 == 402263)
s.add(170 * v34+ 120 * v33+ 224 * v32+ 48 * v31+ 164 * v30+ 138 * v29+ 92 * v28+ 3 * v27+ 191 * v26+ 94 * v25+ 19 * v24+ 50 * v23+ 34 * v22+ 167 * v21+ 75 * v20+ 72 * v19+ 238 * v18+ 15 * v17+ 111 * v16+ 216 * v15+ 84 * v14+ 40 * v13+ 145 * v12+ 112 * v11+ 140 * v10+ 204 * v9+ 154 * v8+ 195 * v7+ 175 * v6+ 250 * v5+ 202 * v4+ 169 * v3 == 366968)
s.add(170 * v34+ 68 * v33+ 189 * v30+ 112 * v31+ 50 * v29+ 247 * v28+ 240 * v27+ 164 * v26+ 5 * v25+ 139 * v24+ 56 * v23+ 19 * (v22 + v32)+ 4 * v21+ 23 * v20+ 96 * v18+ 254 * v17+ 63 * v16+ 247 * v15+ 149 * v14+ 183 * v13+ (v12 * 128)+ 147 * v11+ 213 * v10+ 243 * v9+ 172 * (v8 + v19)+ 144 * v7+ 246 * v6+ 25 * v5+ 106 * v4+ 176 * v3 == 384909)
s.add(31 * v33+ 41 * (v34 + v8)+ 22 * v32+ 184 * v31+ 183 * v30+ (v29 * 128)+ 149 * v28+ 227 * v26+ 113 * v25+ 65 * v24+ 159 * v23+ 74 * v22+ 170 * v21+ 186 * v20+ 174 * (v19 + v27)+ 211 * v18+ v17+ 156 * v15+ 253 * v14+ 223 * (v13 + v16)+ 241 * v12+ 252 * v11+ 148 * v10+ 93 * v9+ 125 * v7+ 27 * v6+ 136 * v5+ 78 * v4+ 248 * v3 == 425203)
s.add(82 * v34+ 39 * v33+ 237 * v32+ 155 * v31+ 242 * v30+ 145 * v28+ 99 * v27+ 239 * v26+ 3 * v24+ 43 * v23+ 46 * v22+ 155 * v21+ 208 * v20+ 75 * v19+ 181 * v17+ 197 * v16+ 140 * (v15 + v18)+ 10 * (v14 + v29)+ 170 * v13+ 142 * v12+ 212 * v11+ 186 * v10+ 27 * v9+ 105 * (v8 + v25)+ 118 * v7+ 198 * v6+ 243 * v5+ 13 * v4+ 113 * v3 == 372162)
s.add(50 * v33+ 136 * (v34 + v9)+ 206 * v32+ 207 * v31+ 127 * v30+ 58 * v29+ 91 * v28+ 7 * v26+ 17 * v25+ 63 * v24+ 180 * v23+ 40 * v22+ 96 * v21+ 202 * v20+ 185 * v19+ 68 * v18+ 72 * v17+ 240 * v16+ 36 * v15+ 139 * v14+ 199 * v13+ 76 * v12+ 229 * v11+ 159 * v10+ 94 * v8+ 19 * v7+ 3 * v6+ 45 * v4+ 87 * (v5 + v27)+ 6 * v3 == 297509)
s.add(90 * v34+ 12 * v33+ 215 * v32+ 115 * v31+ 40 * v30+ 166 * v29+ 87 * v28+ 83 * v27+ 74 * v26+ 202 * v25+ 149 * v23+ 114 * v22+ 76 * v21+ 204 * v20+ 218 * v19+ 63 * v18+ 123 * v17+ 9 * v16+ 172 * v15+ 38 * v14+ 138 * v13+ 35 * v12+ 200 * v11+ 221 * v10+ 144 * v9+ 108 * v7+ v6+ 235 * (v8 + v24)+ 245 * v5+ 153 * v4+ 184 * v3 == 372215)
s.add(114 * v34+ 36 * v33+ 190 * v32+ 123 * v31+ 55 * v30+ 180 * v29+ 84 * v28+ 231 * v27+ 81 * v26+ 116 * v25+ 61 * v24+ 3 * v23+ 94 * v22+ 190 * v20+ 187 * v19+ 142 * v18+ 62 * v17+ 225 * v16+ 240 * v15+ 179 * v14+ 150 * v13+ 77 * v12+ 196 * v10+ 85 * (v11 + v21)+ 12 * v9+ 144 * v8+ 122 * v7+ 28 * v6+ 224 * v5+ 248 * v4+ 143 * v3 == 370337)
s.add(190 * v34+ 122 * (v33 + v21)+ 202 * v32+ 2 * v31+ 40 * v30+ 224 * v29+ 154 * v28+ 65 * v27+ 241 * v25+ 13 * v24+ 213 * v23+ 176 * v22+ 30 * (v20 + v26)+ 14 * v18+ 191 * v17+ 80 * v16+ 116 * v15+ 74 * v14+ 70 * v13+ 32 * v12+ 189 * v11+ 76 * v10+ 95 * v9+ 103 * v7+ 158 * (v8 + v19)+ 7 * v6+ 201 * v5+ 204 * v4+ 91 * v3 == 314564)
s.add(5 * v34+ 176 * v33+ 154 * v32+ 42 * v31+ 223 * v30+ 165 * v29+ 155 * v28+ 101 * v27+ 75 * v26+ 95 * v25+ 253 * v24+ 14 * v23+ 158 * v22+ 199 * v21+ 110 * v20+ 89 * v19+ 205 * v18+ 202 * v17+ 162 * v15+ 67 * v14+ 30 * v13+ 115 * v12+ 27 * v10+ 83 * (v11 + v16)+ 31 * v9+ 118 * v8+ 160 * v7+ 248 * v6+ 66 * v5+ 88 * v4+ 44 * v3 == 325974)
s.add(84 * v33+ 125 * (v34 + v16)+ 168 * v32+ 34 * v31+ 160 * v29+ 243 * v28+ 41 * v27+ 146 * v26+ 62 * v24+ 235 * v23+ 185 * v22+ 180 * v21+ 10 * v20+ 150 * v19+ 140 * v17+ 114 * v15+ 35 * v14+ 34 * v13+ 38 * v12+ 123 * v11+ 163 * v10+ 5 * v8+ 208 * (v9 + v18)+ 29 * (v7 + v25)+ 207 * v6+ 111 * v5+ 72 * (v4 + v30)+ 65 * v3 == 307088)
s.add(140 * v34+ 197 * v33+ 11 * v32+ 18 * v31+ 175 * v29+ 44 * v28+ (v27 * 128)+ 32 * v26+ 100 * v25+ 116 * v23+ 253 * v22+ 213 * v21+ 67 * v20+ 16 * v19+ 171 * v18+ 178 * v17+ 7 * v15+ 162 * v14+ 152 * v13+ 78 * v12+ 167 * v11+ 177 * v10+ 97 * (v9 + v16)+ 26 * (v8 + v30)+ 155 * v7+ 127 * v6+ 21 * (v5 + v24)+ 243 * v4+ 188 * v3 == 322340)
s.add(152 * v34+ 7 * (v33 + v5)+ 110 * v32+ 140 * v31+ 164 * v30+ 208 * v29+ 72 * v28+ 113 * v27+ 9 * v26+ 47 * v25+ 179 * v24+ 166 * v23+ 51 * v22+ 34 * v21+ 91 * v20+ 184 * v19+ 89 * v18+ 162 * v17+ 233 * v16+ 156 * v14+ 244 * v12+ 127 * (v13 + v15)+ 183 * v11+ 193 * v10+ 138 * v9+ 242 * v8+ 90 * v7+ 193 * v6+ 252 * v4+ 113 * v3 == 380716)
s.add(197 * v34+ 75 * (v33 + v30)+ 105 * v32+ 133 * v31+ 146 * v29+ 173 * v28+ 27 * v27+ 97 * v26+ 142 * v25+ 164 * v24+ 15 * v23+ 10 * v22+ 177 * v21+ 239 * v20+ 141 * v19+ 189 * v18+ 67 * v17+ 153 * v16+ 108 * v15+ 206 * v14+ 210 * v13+ 171 * v12+ 252 * v11+ 84 * v10+ 249 * v9+ 7 * v8+ 168 * v7+ 100 * v6+ 30 * v5+ 196 * v4+ 244 * v3 == 393331)
s.add(53 * v34+ 79 * v33+ 221 * v32+ 147 * v31+ 57 * v30+ 186 * v29+ 69 * v28+ 230 * v27+ 167 * v26+ 3 * v25+ 220 * v24+ 63 * v23+ 235 * v21+ 156 * v20+ 146 * v19+ 75 * v18+ 198 * v17+ 204 * v16+ 197 * v15+ 59 * v14+ 61 * v13+ 179 * v12+ 47 * v11+ 221 * v10+ 127 * v9+ 210 * v8+ 241 * v6+ 218 * (v7 + v22)+ 135 * v5+ 196 * v4+ 185 * v3 == 430295)

print s.check()
print s.model()

v31 = buf[0] = buf[0] ^= 0x18;
        v32 = buf[1] = buf[1] ^= 0x9;
        v30 = buf[2] = buf[2] ^= 0x3;
        v29 = buf[3] = buf[3] ^= 0x6B;

        v28 = buf[4] = buf[4] ^= 0x1;
        v27 = buf[5] = buf[5] ^= 0x5a;
        v26 = buf[6] = buf[6] ^= 0x32;
        v25 = buf[7] = buf[7] ^= 0x57;

        v24 = buf[8] = buf[8] ^= 0x30;
        v23 = buf[9] = buf[9] ^= 0x5d;
        v22 = buf[10] = buf[10] ^= 0x40;
        v21 = buf[11] = buf[11] ^= 0x46;

        v20 = buf[12] = buf[12] ^= 0x2b;
        v19 = buf[13] = buf[13] ^= 0x46;
        v18 = buf[14] = buf[14] ^= 0x56;
        v17 = buf[15] = buf[15] ^= 0x3d;

        v16 = buf[16] = buf[16] ^= 0x2;
        v15 = buf[17] = buf[17] ^= 0x43;
        v14 = buf[18] = buf[18] ^= 0x17;


        v12 = buf[20] = buf[20] ^= 0x32;
        v11 = buf[21] = buf[21] ^= 0x53;
        v10 = buf[22] = buf[22] ^= 0x1f;
        v9 = buf[23] = buf[23] ^= 0x26;

        v8 = buf[24] = buf[24] ^= 0x2a;
        v7 = buf[25] = buf[25] ^= 0x1;

        v5 = buf[27] = buf[27] ^= 0x10;

        v4 = buf[28] = buf[28] ^= 0x10;
        v3 = buf[29] = buf[29] ^= 0x1e;
        v34 = buf[30] = buf[30] ^= 0x40;