Skip to content

Instantly share code, notes, and snippets.

@LeventErkok

LeventErkok/prob2.smt

Created September 21, 2011 17:41
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save LeventErkok/1232769 to your computer and use it in GitHub Desktop.
Save LeventErkok/1232769 to your computer and use it in GitHub Desktop.
Download ZIP
Takes too long, > 20 mins and z3 still running
Raw
prob2.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))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
; --- refuted-models ---
(assert (or (not (= s0 #x05387ed598de44ba))
(not (= s1 #x3f))
(not (= s2 #x00))
(not (= s3 #x01))
(not (= s4 #x0d))
(not (= s5 #x32))
(not (= s6 #x02))
(not (= s7 #x25))
(not (= s8 #x0e))
(not (= s9 #x2f))
(not (= s10 #x33))
(not (= s11 #x03))
(not (= s12 #x36))
(not (= s13 #x21))
(not (= s14 #x26))
(not (= s15 #x08))
(not (= s16 #x0f))
(not (= s17 #x3d))
(not (= s18 #x30))
(not (= s19 #x34))
(not (= s20 #x06))
(not (= s21 #x04))
(not (= s22 #x1a))
(not (= s23 #x1c))
(not (= s24 #x37))
(not (= s25 #x22))
(not (= s26 #x1e))
(not (= s27 #x17))
(not (= s28 #x27))
(not (= s29 #x09))
(not (= s30 #x39))
(not (= s31 #x2a))
(not (= s32 #x10))
(not (= s33 #x3e))
(not (= s34 #x0c))
(not (= s35 #x31))
(not (= s36 #x24))
(not (= s37 #x2e))
(not (= s38 #x35))
(not (= s39 #x20))
(not (= s40 #x07))
(not (= s41 #x3c))
(not (= s42 #x05))
(not (= s43 #x19))
(not (= s44 #x1b))
(not (= s45 #x1d))
(not (= s46 #x16))
(not (= s47 #x38))
(not (= s48 #x29))
(not (= s49 #x0b))
(not (= s50 #x23))
(not (= s51 #x2d))
(not (= s52 #x1f))
(not (= s53 #x3b))
(not (= s54 #x18))
(not (= s55 #x15))
(not (= s56 #x28))
(not (= s57 #x0a))
(not (= s58 #x2c))
(not (= s59 #x3a))
(not (= s60 #x14))
(not (= s61 #x2b))
(not (= s62 #x13))
(not (= s63 #x12))
(not (= s64 #x11))
))
(check-sat)
(get-model)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment