Successful z3 run (< 2 mins)

prob1.smt

(set-option :mbqi true)
(set-option :produce-models true)
; --- literal constants ---
(define-fun s_2 () (_ BitVec 1) #b0)
(define-fun s_1 () (_ BitVec 1) #b1)
(define-fun s68 () (_ BitVec 8) #x00)
(define-fun s83 () (_ BitVec 8) #x01)
(define-fun s89 () (_ BitVec 8) #x02)
(define-fun s95 () (_ BitVec 8) #x03)
(define-fun s101 () (_ BitVec 8) #x04)
(define-fun s107 () (_ BitVec 8) #x05)
(define-fun s113 () (_ BitVec 8) #x06)
(define-fun s119 () (_ BitVec 8) #x07)
(define-fun s125 () (_ BitVec 8) #x08)
(define-fun s131 () (_ BitVec 8) #x09)
(define-fun s137 () (_ BitVec 8) #x0a)
(define-fun s143 () (_ BitVec 8) #x0b)
(define-fun s149 () (_ BitVec 8) #x0c)
(define-fun s155 () (_ BitVec 8) #x0d)
(define-fun s161 () (_ BitVec 8) #x0e)
(define-fun s167 () (_ BitVec 8) #x0f)
(define-fun s173 () (_ BitVec 8) #x10)
(define-fun s179 () (_ BitVec 8) #x11)
(define-fun s185 () (_ BitVec 8) #x12)
(define-fun s191 () (_ BitVec 8) #x13)
(define-fun s197 () (_ BitVec 8) #x14)
(define-fun s203 () (_ BitVec 8) #x15)
(define-fun s209 () (_ BitVec 8) #x16)
(define-fun s215 () (_ BitVec 8) #x17)
(define-fun s221 () (_ BitVec 8) #x18)
(define-fun s227 () (_ BitVec 8) #x19)
(define-fun s233 () (_ BitVec 8) #x1a)
(define-fun s239 () (_ BitVec 8) #x1b)
(define-fun s245 () (_ BitVec 8) #x1c)
(define-fun s251 () (_ BitVec 8) #x1d)
(define-fun s257 () (_ BitVec 8) #x1e)
(define-fun s263 () (_ BitVec 8) #x1f)
(define-fun s269 () (_ BitVec 8) #x20)
(define-fun s275 () (_ BitVec 8) #x21)
(define-fun s281 () (_ BitVec 8) #x22)
(define-fun s287 () (_ BitVec 8) #x23)
(define-fun s293 () (_ BitVec 8) #x24)
(define-fun s299 () (_ BitVec 8) #x25)
(define-fun s305 () (_ BitVec 8) #x26)
(define-fun s311 () (_ BitVec 8) #x27)
(define-fun s317 () (_ BitVec 8) #x28)
(define-fun s323 () (_ BitVec 8) #x29)
(define-fun s329 () (_ BitVec 8) #x2a)
(define-fun s335 () (_ BitVec 8) #x2b)
(define-fun s341 () (_ BitVec 8) #x2c)
(define-fun s347 () (_ BitVec 8) #x2d)
(define-fun s353 () (_ BitVec 8) #x2e)
(define-fun s359 () (_ BitVec 8) #x2f)
(define-fun s365 () (_ BitVec 8) #x30)
(define-fun s371 () (_ BitVec 8) #x31)
(define-fun s377 () (_ BitVec 8) #x32)
(define-fun s383 () (_ BitVec 8) #x33)
(define-fun s389 () (_ BitVec 8) #x34)
(define-fun s395 () (_ BitVec 8) #x35)
(define-fun s401 () (_ BitVec 8) #x36)
(define-fun s407 () (_ BitVec 8) #x37)
(define-fun s413 () (_ BitVec 8) #x38)
(define-fun s419 () (_ BitVec 8) #x39)
(define-fun s425 () (_ BitVec 8) #x3a)
(define-fun s431 () (_ BitVec 8) #x3b)
(define-fun s437 () (_ BitVec 8) #x3c)
(define-fun s443 () (_ BitVec 8) #x3d)
(define-fun s449 () (_ BitVec 8) #x3e)
(define-fun s455 () (_ BitVec 8) #x3f)
(define-fun s461 () (_ BitVec 8) #x40)
(define-fun s462 () (_ BitVec 8) #x41)
(define-fun s66 () (_ BitVec 64) #x0000000000000000)
(define-fun s74 () (_ BitVec 64) #x0000000000000001)
; --- skolem constants ---
(declare-fun s0 () (_ BitVec 64))
(declare-fun s1 () (_ BitVec 8))
(declare-fun s2 () (_ BitVec 8))
(declare-fun s3 () (_ BitVec 8))
(declare-fun s4 () (_ BitVec 8))
(declare-fun s5 () (_ BitVec 8))
(declare-fun s6 () (_ BitVec 8))
(declare-fun s7 () (_ BitVec 8))
(declare-fun s8 () (_ BitVec 8))
(declare-fun s9 () (_ BitVec 8))
(declare-fun s10 () (_ BitVec 8))
(declare-fun s11 () (_ BitVec 8))
(declare-fun s12 () (_ BitVec 8))
(declare-fun s13 () (_ BitVec 8))
(declare-fun s14 () (_ BitVec 8))
(declare-fun s15 () (_ BitVec 8))
(declare-fun s16 () (_ BitVec 8))
(declare-fun s17 () (_ BitVec 8))
(declare-fun s18 () (_ BitVec 8))
(declare-fun s19 () (_ BitVec 8))
(declare-fun s20 () (_ BitVec 8))
(declare-fun s21 () (_ BitVec 8))
(declare-fun s22 () (_ BitVec 8))
(declare-fun s23 () (_ BitVec 8))
(declare-fun s24 () (_ BitVec 8))
(declare-fun s25 () (_ BitVec 8))
(declare-fun s26 () (_ BitVec 8))
(declare-fun s27 () (_ BitVec 8))
(declare-fun s28 () (_ BitVec 8))
(declare-fun s29 () (_ BitVec 8))
(declare-fun s30 () (_ BitVec 8))
(declare-fun s31 () (_ BitVec 8))
(declare-fun s32 () (_ BitVec 8))
(declare-fun s33 () (_ BitVec 8))
(declare-fun s34 () (_ BitVec 8))
(declare-fun s35 () (_ BitVec 8))
(declare-fun s36 () (_ BitVec 8))
(declare-fun s37 () (_ BitVec 8))
(declare-fun s38 () (_ BitVec 8))
(declare-fun s39 () (_ BitVec 8))
(declare-fun s40 () (_ BitVec 8))
(declare-fun s41 () (_ BitVec 8))
(declare-fun s42 () (_ BitVec 8))
(declare-fun s43 () (_ BitVec 8))
(declare-fun s44 () (_ BitVec 8))
(declare-fun s45 () (_ BitVec 8))
(declare-fun s46 () (_ BitVec 8))
(declare-fun s47 () (_ BitVec 8))
(declare-fun s48 () (_ BitVec 8))
(declare-fun s49 () (_ BitVec 8))
(declare-fun s50 () (_ BitVec 8))
(declare-fun s51 () (_ BitVec 8))
(declare-fun s52 () (_ BitVec 8))
(declare-fun s53 () (_ BitVec 8))
(declare-fun s54 () (_ BitVec 8))
(declare-fun s55 () (_ BitVec 8))
(declare-fun s56 () (_ BitVec 8))
(declare-fun s57 () (_ BitVec 8))
(declare-fun s58 () (_ BitVec 8))
(declare-fun s59 () (_ BitVec 8))
(declare-fun s60 () (_ BitVec 8))
(declare-fun s61 () (_ BitVec 8))
(declare-fun s62 () (_ BitVec 8))
(declare-fun s63 () (_ BitVec 8))
(declare-fun s64 () (_ BitVec 8))
; --- constant tables ---
; --- skolemized tables ---
(declare-fun table0 ((_ BitVec 64)) (Array (_ BitVec 64) (_ BitVec 8)))
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(assert (forall ((s65 (_ BitVec 64)))
            (let ((s67 (bvcomp s65 s66)))
            (let ((s69 (bvsub s66 s65)))
            (let ((s70 (bvand s65 s69)))
            (let ((s71 (bvmul s0 s70)))
            (let ((s72 (bvlshr s71 #x000000000000003a)))
            (let ((s73 (ite (bvule #x0000000000000040 s72) s68 (select (table0 s65) s72))))
            (let ((s75 (bvand s65 s74)))
            (let ((s76 (bvnot (bvcomp s66 s75))))
            (let ((s77 (bvor s67 s76)))
            (let ((s78 (bvlshr s65 #x0000000000000001)))
            (let ((s79 (bvcomp s66 s78)))
            (let ((s80 (bvand s74 s78)))
            (let ((s81 (bvnot (bvcomp s66 s80))))
            (let ((s82 (bvor s79 s81)))
            (let ((s84 (bvlshr s78 #x0000000000000001)))
            (let ((s85 (bvcomp s66 s84)))
            (let ((s86 (bvand s74 s84)))
            (let ((s87 (bvnot (bvcomp s66 s86))))
            (let ((s88 (bvor s85 s87)))
            (let ((s90 (bvlshr s84 #x0000000000000001)))
            (let ((s91 (bvcomp s66 s90)))
            (let ((s92 (bvand s74 s90)))
            (let ((s93 (bvnot (bvcomp s66 s92))))
            (let ((s94 (bvor s91 s93)))
            (let ((s96 (bvlshr s90 #x0000000000000001)))
            (let ((s97 (bvcomp s66 s96)))
            (let ((s98 (bvand s74 s96)))
            (let ((s99 (bvnot (bvcomp s66 s98))))
            (let ((s100 (bvor s97 s99)))
            (let ((s102 (bvlshr s96 #x0000000000000001)))
            (let ((s103 (bvcomp s66 s102)))
            (let ((s104 (bvand s74 s102)))
            (let ((s105 (bvnot (bvcomp s66 s104))))
            (let ((s106 (bvor s103 s105)))
            (let ((s108 (bvlshr s102 #x0000000000000001)))
            (let ((s109 (bvcomp s66 s108)))
            (let ((s110 (bvand s74 s108)))
            (let ((s111 (bvnot (bvcomp s66 s110))))
            (let ((s112 (bvor s109 s111)))
            (let ((s114 (bvlshr s108 #x0000000000000001)))
            (let ((s115 (bvcomp s66 s114)))
            (let ((s116 (bvand s74 s114)))
            (let ((s117 (bvnot (bvcomp s66 s116))))
            (let ((s118 (bvor s115 s117)))
            (let ((s120 (bvlshr s114 #x0000000000000001)))
            (let ((s121 (bvcomp s66 s120)))
            (let ((s122 (bvand s74 s120)))
            (let ((s123 (bvnot (bvcomp s66 s122))))
            (let ((s124 (bvor s121 s123)))
            (let ((s126 (bvlshr s120 #x0000000000000001)))
            (let ((s127 (bvcomp s66 s126)))
            (let ((s128 (bvand s74 s126)))
            (let ((s129 (bvnot (bvcomp s66 s128))))
            (let ((s130 (bvor s127 s129)))
            (let ((s132 (bvlshr s126 #x0000000000000001)))
            (let ((s133 (bvcomp s66 s132)))
            (let ((s134 (bvand s74 s132)))
            (let ((s135 (bvnot (bvcomp s66 s134))))
            (let ((s136 (bvor s133 s135)))
            (let ((s138 (bvlshr s132 #x0000000000000001)))
            (let ((s139 (bvcomp s66 s138)))
            (let ((s140 (bvand s74 s138)))
            (let ((s141 (bvnot (bvcomp s66 s140))))
            (let ((s142 (bvor s139 s141)))
            (let ((s144 (bvlshr s138 #x0000000000000001)))
            (let ((s145 (bvcomp s66 s144)))
            (let ((s146 (bvand s74 s144)))
            (let ((s147 (bvnot (bvcomp s66 s146))))
            (let ((s148 (bvor s145 s147)))
            (let ((s150 (bvlshr s144 #x0000000000000001)))
            (let ((s151 (bvcomp s66 s150)))
            (let ((s152 (bvand s74 s150)))
            (let ((s153 (bvnot (bvcomp s66 s152))))
            (let ((s154 (bvor s151 s153)))
            (let ((s156 (bvlshr s150 #x0000000000000001)))
            (let ((s157 (bvcomp s66 s156)))
            (let ((s158 (bvand s74 s156)))
            (let ((s159 (bvnot (bvcomp s66 s158))))
            (let ((s160 (bvor s157 s159)))
            (let ((s162 (bvlshr s156 #x0000000000000001)))
            (let ((s163 (bvcomp s66 s162)))
            (let ((s164 (bvand s74 s162)))
            (let ((s165 (bvnot (bvcomp s66 s164))))
            (let ((s166 (bvor s163 s165)))
            (let ((s168 (bvlshr s162 #x0000000000000001)))
            (let ((s169 (bvcomp s66 s168)))
            (let ((s170 (bvand s74 s168)))
            (let ((s171 (bvnot (bvcomp s66 s170))))
            (let ((s172 (bvor s169 s171)))
            (let ((s174 (bvlshr s168 #x0000000000000001)))
            (let ((s175 (bvcomp s66 s174)))
            (let ((s176 (bvand s74 s174)))
            (let ((s177 (bvnot (bvcomp s66 s176))))
            (let ((s178 (bvor s175 s177)))
            (let ((s180 (bvlshr s174 #x0000000000000001)))
            (let ((s181 (bvcomp s66 s180)))
            (let ((s182 (bvand s74 s180)))
            (let ((s183 (bvnot (bvcomp s66 s182))))
            (let ((s184 (bvor s181 s183)))
            (let ((s186 (bvlshr s180 #x0000000000000001)))
            (let ((s187 (bvcomp s66 s186)))
            (let ((s188 (bvand s74 s186)))
            (let ((s189 (bvnot (bvcomp s66 s188))))
            (let ((s190 (bvor s187 s189)))
            (let ((s192 (bvlshr s186 #x0000000000000001)))
            (let ((s193 (bvcomp s66 s192)))
            (let ((s194 (bvand s74 s192)))
            (let ((s195 (bvnot (bvcomp s66 s194))))
            (let ((s196 (bvor s193 s195)))
            (let ((s198 (bvlshr s192 #x0000000000000001)))
            (let ((s199 (bvcomp s66 s198)))
            (let ((s200 (bvand s74 s198)))
            (let ((s201 (bvnot (bvcomp s66 s200))))
            (let ((s202 (bvor s199 s201)))
            (let ((s204 (bvlshr s198 #x0000000000000001)))
            (let ((s205 (bvcomp s66 s204)))
            (let ((s206 (bvand s74 s204)))
            (let ((s207 (bvnot (bvcomp s66 s206))))
            (let ((s208 (bvor s205 s207)))
            (let ((s210 (bvlshr s204 #x0000000000000001)))
            (let ((s211 (bvcomp s66 s210)))
            (let ((s212 (bvand s74 s210)))
            (let ((s213 (bvnot (bvcomp s66 s212))))
            (let ((s214 (bvor s211 s213)))
            (let ((s216 (bvlshr s210 #x0000000000000001)))
            (let ((s217 (bvcomp s66 s216)))
            (let ((s218 (bvand s74 s216)))
            (let ((s219 (bvnot (bvcomp s66 s218))))
            (let ((s220 (bvor s217 s219)))
            (let ((s222 (bvlshr s216 #x0000000000000001)))
            (let ((s223 (bvcomp s66 s222)))
            (let ((s224 (bvand s74 s222)))
            (let ((s225 (bvnot (bvcomp s66 s224))))
            (let ((s226 (bvor s223 s225)))
            (let ((s228 (bvlshr s222 #x0000000000000001)))
            (let ((s229 (bvcomp s66 s228)))
            (let ((s230 (bvand s74 s228)))
            (let ((s231 (bvnot (bvcomp s66 s230))))
            (let ((s232 (bvor s229 s231)))
            (let ((s234 (bvlshr s228 #x0000000000000001)))
            (let ((s235 (bvcomp s66 s234)))
            (let ((s236 (bvand s74 s234)))
            (let ((s237 (bvnot (bvcomp s66 s236))))
            (let ((s238 (bvor s235 s237)))
            (let ((s240 (bvlshr s234 #x0000000000000001)))
            (let ((s241 (bvcomp s66 s240)))
            (let ((s242 (bvand s74 s240)))
            (let ((s243 (bvnot (bvcomp s66 s242))))
            (let ((s244 (bvor s241 s243)))
            (let ((s246 (bvlshr s240 #x0000000000000001)))
            (let ((s247 (bvcomp s66 s246)))
            (let ((s248 (bvand s74 s246)))
            (let ((s249 (bvnot (bvcomp s66 s248))))
            (let ((s250 (bvor s247 s249)))
            (let ((s252 (bvlshr s246 #x0000000000000001)))
            (let ((s253 (bvcomp s66 s252)))
            (let ((s254 (bvand s74 s252)))
            (let ((s255 (bvnot (bvcomp s66 s254))))
            (let ((s256 (bvor s253 s255)))
            (let ((s258 (bvlshr s252 #x0000000000000001)))
            (let ((s259 (bvcomp s66 s258)))
            (let ((s260 (bvand s74 s258)))
            (let ((s261 (bvnot (bvcomp s66 s260))))
            (let ((s262 (bvor s259 s261)))
            (let ((s264 (bvlshr s258 #x0000000000000001)))
            (let ((s265 (bvcomp s66 s264)))
            (let ((s266 (bvand s74 s264)))
            (let ((s267 (bvnot (bvcomp s66 s266))))
            (let ((s268 (bvor s265 s267)))
            (let ((s270 (bvlshr s264 #x0000000000000001)))
            (let ((s271 (bvcomp s66 s270)))
            (let ((s272 (bvand s74 s270)))
            (let ((s273 (bvnot (bvcomp s66 s272))))
            (let ((s274 (bvor s271 s273)))
            (let ((s276 (bvlshr s270 #x0000000000000001)))
            (let ((s277 (bvcomp s66 s276)))
            (let ((s278 (bvand s74 s276)))
            (let ((s279 (bvnot (bvcomp s66 s278))))
            (let ((s280 (bvor s277 s279)))
            (let ((s282 (bvlshr s276 #x0000000000000001)))
            (let ((s283 (bvcomp s66 s282)))
            (let ((s284 (bvand s74 s282)))
            (let ((s285 (bvnot (bvcomp s66 s284))))
            (let ((s286 (bvor s283 s285)))
            (let ((s288 (bvlshr s282 #x0000000000000001)))
            (let ((s289 (bvcomp s66 s288)))
            (let ((s290 (bvand s74 s288)))
            (let ((s291 (bvnot (bvcomp s66 s290))))
            (let ((s292 (bvor s289 s291)))
            (let ((s294 (bvlshr s288 #x0000000000000001)))
            (let ((s295 (bvcomp s66 s294)))
            (let ((s296 (bvand s74 s294)))
            (let ((s297 (bvnot (bvcomp s66 s296))))
            (let ((s298 (bvor s295 s297)))
            (let ((s300 (bvlshr s294 #x0000000000000001)))
            (let ((s301 (bvcomp s66 s300)))
            (let ((s302 (bvand s74 s300)))
            (let ((s303 (bvnot (bvcomp s66 s302))))
            (let ((s304 (bvor s301 s303)))
            (let ((s306 (bvlshr s300 #x0000000000000001)))
            (let ((s307 (bvcomp s66 s306)))
            (let ((s308 (bvand s74 s306)))
            (let ((s309 (bvnot (bvcomp s66 s308))))
            (let ((s310 (bvor s307 s309)))
            (let ((s312 (bvlshr s306 #x0000000000000001)))
            (let ((s313 (bvcomp s66 s312)))
            (let ((s314 (bvand s74 s312)))
            (let ((s315 (bvnot (bvcomp s66 s314))))
            (let ((s316 (bvor s313 s315)))
            (let ((s318 (bvlshr s312 #x0000000000000001)))
            (let ((s319 (bvcomp s66 s318)))
            (let ((s320 (bvand s74 s318)))
            (let ((s321 (bvnot (bvcomp s66 s320))))
            (let ((s322 (bvor s319 s321)))
            (let ((s324 (bvlshr s318 #x0000000000000001)))
            (let ((s325 (bvcomp s66 s324)))
            (let ((s326 (bvand s74 s324)))
            (let ((s327 (bvnot (bvcomp s66 s326))))
            (let ((s328 (bvor s325 s327)))
            (let ((s330 (bvlshr s324 #x0000000000000001)))
            (let ((s331 (bvcomp s66 s330)))
            (let ((s332 (bvand s74 s330)))
            (let ((s333 (bvnot (bvcomp s66 s332))))
            (let ((s334 (bvor s331 s333)))
            (let ((s336 (bvlshr s330 #x0000000000000001)))
            (let ((s337 (bvcomp s66 s336)))
            (let ((s338 (bvand s74 s336)))
            (let ((s339 (bvnot (bvcomp s66 s338))))
            (let ((s340 (bvor s337 s339)))
            (let ((s342 (bvlshr s336 #x0000000000000001)))
            (let ((s343 (bvcomp s66 s342)))
            (let ((s344 (bvand s74 s342)))
            (let ((s345 (bvnot (bvcomp s66 s344))))
            (let ((s346 (bvor s343 s345)))
            (let ((s348 (bvlshr s342 #x0000000000000001)))
            (let ((s349 (bvcomp s66 s348)))
            (let ((s350 (bvand s74 s348)))
            (let ((s351 (bvnot (bvcomp s66 s350))))
            (let ((s352 (bvor s349 s351)))
            (let ((s354 (bvlshr s348 #x0000000000000001)))
            (let ((s355 (bvcomp s66 s354)))
            (let ((s356 (bvand s74 s354)))
            (let ((s357 (bvnot (bvcomp s66 s356))))
            (let ((s358 (bvor s355 s357)))
            (let ((s360 (bvlshr s354 #x0000000000000001)))
            (let ((s361 (bvcomp s66 s360)))
            (let ((s362 (bvand s74 s360)))
            (let ((s363 (bvnot (bvcomp s66 s362))))
            (let ((s364 (bvor s361 s363)))
            (let ((s366 (bvlshr s360 #x0000000000000001)))
            (let ((s367 (bvcomp s66 s366)))
            (let ((s368 (bvand s74 s366)))
            (let ((s369 (bvnot (bvcomp s66 s368))))
            (let ((s370 (bvor s367 s369)))
            (let ((s372 (bvlshr s366 #x0000000000000001)))
            (let ((s373 (bvcomp s66 s372)))
            (let ((s374 (bvand s74 s372)))
            (let ((s375 (bvnot (bvcomp s66 s374))))
            (let ((s376 (bvor s373 s375)))
            (let ((s378 (bvlshr s372 #x0000000000000001)))
            (let ((s379 (bvcomp s66 s378)))
            (let ((s380 (bvand s74 s378)))
            (let ((s381 (bvnot (bvcomp s66 s380))))
            (let ((s382 (bvor s379 s381)))
            (let ((s384 (bvlshr s378 #x0000000000000001)))
            (let ((s385 (bvcomp s66 s384)))
            (let ((s386 (bvand s74 s384)))
            (let ((s387 (bvnot (bvcomp s66 s386))))
            (let ((s388 (bvor s385 s387)))
            (let ((s390 (bvlshr s384 #x0000000000000001)))
            (let ((s391 (bvcomp s66 s390)))
            (let ((s392 (bvand s74 s390)))
            (let ((s393 (bvnot (bvcomp s66 s392))))
            (let ((s394 (bvor s391 s393)))
            (let ((s396 (bvlshr s390 #x0000000000000001)))
            (let ((s397 (bvcomp s66 s396)))
            (let ((s398 (bvand s74 s396)))
            (let ((s399 (bvnot (bvcomp s66 s398))))
            (let ((s400 (bvor s397 s399)))
            (let ((s402 (bvlshr s396 #x0000000000000001)))
            (let ((s403 (bvcomp s66 s402)))
            (let ((s404 (bvand s74 s402)))
            (let ((s405 (bvnot (bvcomp s66 s404))))
            (let ((s406 (bvor s403 s405)))
            (let ((s408 (bvlshr s402 #x0000000000000001)))
            (let ((s409 (bvcomp s66 s408)))
            (let ((s410 (bvand s74 s408)))
            (let ((s411 (bvnot (bvcomp s66 s410))))
            (let ((s412 (bvor s409 s411)))
            (let ((s414 (bvlshr s408 #x0000000000000001)))
            (let ((s415 (bvcomp s66 s414)))
            (let ((s416 (bvand s74 s414)))
            (let ((s417 (bvnot (bvcomp s66 s416))))
            (let ((s418 (bvor s415 s417)))
            (let ((s420 (bvlshr s414 #x0000000000000001)))
            (let ((s421 (bvcomp s66 s420)))
            (let ((s422 (bvand s74 s420)))
            (let ((s423 (bvnot (bvcomp s66 s422))))
            (let ((s424 (bvor s421 s423)))
            (let ((s426 (bvlshr s420 #x0000000000000001)))
            (let ((s427 (bvcomp s66 s426)))
            (let ((s428 (bvand s74 s426)))
            (let ((s429 (bvnot (bvcomp s66 s428))))
            (let ((s430 (bvor s427 s429)))
            (let ((s432 (bvlshr s426 #x0000000000000001)))
            (let ((s433 (bvcomp s66 s432)))
            (let ((s434 (bvand s74 s432)))
            (let ((s435 (bvnot (bvcomp s66 s434))))
            (let ((s436 (bvor s433 s435)))
            (let ((s438 (bvlshr s432 #x0000000000000001)))
            (let ((s439 (bvcomp s66 s438)))
            (let ((s440 (bvand s74 s438)))
            (let ((s441 (bvnot (bvcomp s66 s440))))
            (let ((s442 (bvor s439 s441)))
            (let ((s444 (bvlshr s438 #x0000000000000001)))
            (let ((s445 (bvcomp s66 s444)))
            (let ((s446 (bvand s74 s444)))
            (let ((s447 (bvnot (bvcomp s66 s446))))
            (let ((s448 (bvor s445 s447)))
            (let ((s450 (bvlshr s444 #x0000000000000001)))
            (let ((s451 (bvcomp s66 s450)))
            (let ((s452 (bvand s74 s450)))
            (let ((s453 (bvnot (bvcomp s66 s452))))
            (let ((s454 (bvor s451 s453)))
            (let ((s456 (bvlshr s450 #x0000000000000001)))
            (let ((s457 (bvcomp s66 s456)))
            (let ((s458 (bvand s74 s456)))
            (let ((s459 (bvnot (bvcomp s66 s458))))
            (let ((s460 (bvor s457 s459)))
            (let ((s463 (ite (= #b1 s460) s461 s462)))
            (let ((s464 (ite (= #b1 s454) s455 s463)))
            (let ((s465 (ite (= #b1 s448) s449 s464)))
            (let ((s466 (ite (= #b1 s442) s443 s465)))
            (let ((s467 (ite (= #b1 s436) s437 s466)))
            (let ((s468 (ite (= #b1 s430) s431 s467)))
            (let ((s469 (ite (= #b1 s424) s425 s468)))
            (let ((s470 (ite (= #b1 s418) s419 s469)))
            (let ((s471 (ite (= #b1 s412) s413 s470)))
            (let ((s472 (ite (= #b1 s406) s407 s471)))
            (let ((s473 (ite (= #b1 s400) s401 s472)))
            (let ((s474 (ite (= #b1 s394) s395 s473)))
            (let ((s475 (ite (= #b1 s388) s389 s474)))
            (let ((s476 (ite (= #b1 s382) s383 s475)))
            (let ((s477 (ite (= #b1 s376) s377 s476)))
            (let ((s478 (ite (= #b1 s370) s371 s477)))
            (let ((s479 (ite (= #b1 s364) s365 s478)))
            (let ((s480 (ite (= #b1 s358) s359 s479)))
            (let ((s481 (ite (= #b1 s352) s353 s480)))
            (let ((s482 (ite (= #b1 s346) s347 s481)))
            (let ((s483 (ite (= #b1 s340) s341 s482)))
            (let ((s484 (ite (= #b1 s334) s335 s483)))
            (let ((s485 (ite (= #b1 s328) s329 s484)))
            (let ((s486 (ite (= #b1 s322) s323 s485)))
            (let ((s487 (ite (= #b1 s316) s317 s486)))
            (let ((s488 (ite (= #b1 s310) s311 s487)))
            (let ((s489 (ite (= #b1 s304) s305 s488)))
            (let ((s490 (ite (= #b1 s298) s299 s489)))
            (let ((s491 (ite (= #b1 s292) s293 s490)))
            (let ((s492 (ite (= #b1 s286) s287 s491)))
            (let ((s493 (ite (= #b1 s280) s281 s492)))
            (let ((s494 (ite (= #b1 s274) s275 s493)))
            (let ((s495 (ite (= #b1 s268) s269 s494)))
            (let ((s496 (ite (= #b1 s262) s263 s495)))
            (let ((s497 (ite (= #b1 s256) s257 s496)))
            (let ((s498 (ite (= #b1 s250) s251 s497)))
            (let ((s499 (ite (= #b1 s244) s245 s498)))
            (let ((s500 (ite (= #b1 s238) s239 s499)))
            (let ((s501 (ite (= #b1 s232) s233 s500)))
            (let ((s502 (ite (= #b1 s226) s227 s501)))
            (let ((s503 (ite (= #b1 s220) s221 s502)))
            (let ((s504 (ite (= #b1 s214) s215 s503)))
            (let ((s505 (ite (= #b1 s208) s209 s504)))
            (let ((s506 (ite (= #b1 s202) s203 s505)))
            (let ((s507 (ite (= #b1 s196) s197 s506)))
            (let ((s508 (ite (= #b1 s190) s191 s507)))
            (let ((s509 (ite (= #b1 s184) s185 s508)))
            (let ((s510 (ite (= #b1 s178) s179 s509)))
            (let ((s511 (ite (= #b1 s172) s173 s510)))
            (let ((s512 (ite (= #b1 s166) s167 s511)))
            (let ((s513 (ite (= #b1 s160) s161 s512)))
            (let ((s514 (ite (= #b1 s154) s155 s513)))
            (let ((s515 (ite (= #b1 s148) s149 s514)))
            (let ((s516 (ite (= #b1 s142) s143 s515)))
            (let ((s517 (ite (= #b1 s136) s137 s516)))
            (let ((s518 (ite (= #b1 s130) s131 s517)))
            (let ((s519 (ite (= #b1 s124) s125 s518)))
            (let ((s520 (ite (= #b1 s118) s119 s519)))
            (let ((s521 (ite (= #b1 s112) s113 s520)))
            (let ((s522 (ite (= #b1 s106) s107 s521)))
            (let ((s523 (ite (= #b1 s100) s101 s522)))
            (let ((s524 (ite (= #b1 s94) s95 s523)))
            (let ((s525 (ite (= #b1 s88) s89 s524)))
            (let ((s526 (ite (= #b1 s82) s83 s525)))
            (let ((s527 (ite (= #b1 s77) s68 s526)))
            (let ((s528 (bvcomp s73 s527)))
            (let ((s529 (bvor s67 s528)))
            (and (= (select (table0 s65) #x0000000000000000) s1)
                 (= (select (table0 s65) #x0000000000000001) s2)
                 (= (select (table0 s65) #x0000000000000002) s3)
                 (= (select (table0 s65) #x0000000000000003) s4)
                 (= (select (table0 s65) #x0000000000000004) s5)
                 (= (select (table0 s65) #x0000000000000005) s6)
                 (= (select (table0 s65) #x0000000000000006) s7)
                 (= (select (table0 s65) #x0000000000000007) s8)
                 (= (select (table0 s65) #x0000000000000008) s9)
                 (= (select (table0 s65) #x0000000000000009) s10)
                 (= (select (table0 s65) #x000000000000000a) s11)
                 (= (select (table0 s65) #x000000000000000b) s12)
                 (= (select (table0 s65) #x000000000000000c) s13)
                 (= (select (table0 s65) #x000000000000000d) s14)
                 (= (select (table0 s65) #x000000000000000e) s15)
                 (= (select (table0 s65) #x000000000000000f) s16)
                 (= (select (table0 s65) #x0000000000000010) s17)
                 (= (select (table0 s65) #x0000000000000011) s18)
                 (= (select (table0 s65) #x0000000000000012) s19)
                 (= (select (table0 s65) #x0000000000000013) s20)
                 (= (select (table0 s65) #x0000000000000014) s21)
                 (= (select (table0 s65) #x0000000000000015) s22)
                 (= (select (table0 s65) #x0000000000000016) s23)
                 (= (select (table0 s65) #x0000000000000017) s24)
                 (= (select (table0 s65) #x0000000000000018) s25)
                 (= (select (table0 s65) #x0000000000000019) s26)
                 (= (select (table0 s65) #x000000000000001a) s27)
                 (= (select (table0 s65) #x000000000000001b) s28)
                 (= (select (table0 s65) #x000000000000001c) s29)
                 (= (select (table0 s65) #x000000000000001d) s30)
                 (= (select (table0 s65) #x000000000000001e) s31)
                 (= (select (table0 s65) #x000000000000001f) s32)
                 (= (select (table0 s65) #x0000000000000020) s33)
                 (= (select (table0 s65) #x0000000000000021) s34)
                 (= (select (table0 s65) #x0000000000000022) s35)
                 (= (select (table0 s65) #x0000000000000023) s36)
                 (= (select (table0 s65) #x0000000000000024) s37)
                 (= (select (table0 s65) #x0000000000000025) s38)
                 (= (select (table0 s65) #x0000000000000026) s39)
                 (= (select (table0 s65) #x0000000000000027) s40)
                 (= (select (table0 s65) #x0000000000000028) s41)
                 (= (select (table0 s65) #x0000000000000029) s42)
                 (= (select (table0 s65) #x000000000000002a) s43)
                 (= (select (table0 s65) #x000000000000002b) s44)
                 (= (select (table0 s65) #x000000000000002c) s45)
                 (= (select (table0 s65) #x000000000000002d) s46)
                 (= (select (table0 s65) #x000000000000002e) s47)
                 (= (select (table0 s65) #x000000000000002f) s48)
                 (= (select (table0 s65) #x0000000000000030) s49)
                 (= (select (table0 s65) #x0000000000000031) s50)
                 (= (select (table0 s65) #x0000000000000032) s51)
                 (= (select (table0 s65) #x0000000000000033) s52)
                 (= (select (table0 s65) #x0000000000000034) s53)
                 (= (select (table0 s65) #x0000000000000035) s54)
                 (= (select (table0 s65) #x0000000000000036) s55)
                 (= (select (table0 s65) #x0000000000000037) s56)
                 (= (select (table0 s65) #x0000000000000038) s57)
                 (= (select (table0 s65) #x0000000000000039) s58)
                 (= (select (table0 s65) #x000000000000003a) s59)
                 (= (select (table0 s65) #x000000000000003b) s60)
                 (= (select (table0 s65) #x000000000000003c) s61)
                 (= (select (table0 s65) #x000000000000003d) s62)
                 (= (select (table0 s65) #x000000000000003e) s63)
                 (= (select (table0 s65) #x000000000000003f) s64)
                 (= s529 #b1))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
(get-model)