** Calling: z3 -nw -in -smt2
[GOOD] ; Automatically generated by SBV. Do not edit.
[GOOD] (set-option :print-success true)
[GOOD] (set-option :global-declarations true)
[GOOD] (set-option :smtlib2_compliant true)
[GOOD] (set-option :diagnostic-output-channel "stdout")
[GOOD] (set-option :produce-models true)
[GOOD] (set-logic QF_UFBV) ; NB. User specified.
[GOOD] ; --- uninterpreted sorts ---
[GOOD] ; --- tuples ---
[GOOD] ; --- sums ---
[GOOD] ; --- literal constants ---
[GOOD] ; --- skolem constants ---
[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "i"
[GOOD] (declare-fun s1 () (_ BitVec 8)) ; tracks user variable "j"
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (define-fun s2 () (_ BitVec 8) #x00)
[GOOD] (define-fun s3 () (_ BitVec 8) #x01)
[GOOD] (define-fun s4 () (_ BitVec 8) #x02)
[GOOD] (define-fun s5 () (_ BitVec 8) #x03)
[GOOD] (define-fun s6 () (_ BitVec 8) #x04)
[GOOD] (define-fun s7 () (_ BitVec 8) #x05)
[GOOD] (define-fun s8 () (_ BitVec 8) #x06)
[GOOD] (define-fun s9 () (_ BitVec 8) #x07)
[GOOD] (define-fun s10 () (_ BitVec 8) #x08)
[GOOD] (define-fun s11 () (_ BitVec 8) #x09)
[GOOD] (define-fun s12 () (_ BitVec 8) #x0a)
[GOOD] (define-fun s13 () (_ BitVec 8) #x0b)
[GOOD] (define-fun s14 () (_ BitVec 8) #x0c)
[GOOD] (define-fun s15 () (_ BitVec 8) #x0d)
[GOOD] (define-fun s16 () (_ BitVec 8) #x0e)
[GOOD] (define-fun s17 () (_ BitVec 8) #x0f)
[GOOD] (define-fun s18 () (_ BitVec 8) #x10)
[GOOD] (define-fun s19 () (_ BitVec 8) #x11)
[GOOD] (define-fun s20 () (_ BitVec 8) #x12)
[GOOD] (define-fun s21 () (_ BitVec 8) #x13)
[GOOD] (define-fun s22 () (_ BitVec 8) #x14)
[GOOD] (define-fun s23 () (_ BitVec 8) #x15)
[GOOD] (define-fun s24 () (_ BitVec 8) #x16)
[GOOD] (define-fun s25 () (_ BitVec 8) #x17)
[GOOD] (define-fun s26 () (_ BitVec 8) #x18)
[GOOD] (define-fun s27 () (_ BitVec 8) #x19)
[GOOD] (define-fun s28 () (_ BitVec 8) #x1a)
[GOOD] (define-fun s29 () (_ BitVec 8) #x1b)
[GOOD] (define-fun s30 () (_ BitVec 8) #x1c)
[GOOD] (define-fun s31 () (_ BitVec 8) #x1d)
[GOOD] (define-fun s32 () (_ BitVec 8) #x1e)
[GOOD] (define-fun s33 () (_ BitVec 8) #x1f)
[GOOD] (define-fun s34 () (_ BitVec 8) #x20)
[GOOD] (define-fun s35 () (_ BitVec 8) #x21)
[GOOD] (define-fun s36 () (_ BitVec 8) #x22)
[GOOD] (define-fun s37 () (_ BitVec 8) #x23)
[GOOD] (define-fun s38 () (_ BitVec 8) #x24)
[GOOD] (define-fun s39 () (_ BitVec 8) #x25)
[GOOD] (define-fun s40 () (_ BitVec 8) #x26)
[GOOD] (define-fun s41 () (_ BitVec 8) #x27)
[GOOD] (define-fun s42 () (_ BitVec 8) #x28)
[GOOD] (define-fun s43 () (_ BitVec 8) #x29)
[GOOD] (define-fun s44 () (_ BitVec 8) #x2a)
[GOOD] (define-fun s45 () (_ BitVec 8) #x2b)
[GOOD] (define-fun s46 () (_ BitVec 8) #x2c)
[GOOD] (define-fun s47 () (_ BitVec 8) #x2d)
[GOOD] (define-fun s48 () (_ BitVec 8) #x2e)
[GOOD] (define-fun s49 () (_ BitVec 8) #x2f)
[GOOD] (define-fun s50 () (_ BitVec 8) #x30)
[GOOD] (define-fun s51 () (_ BitVec 8) #x31)
[GOOD] (define-fun s52 () (_ BitVec 8) #x32)
[GOOD] (define-fun s53 () (_ BitVec 8) #x33)
[GOOD] (define-fun s54 () (_ BitVec 8) #x34)
[GOOD] (define-fun s55 () (_ BitVec 8) #x35)
[GOOD] (define-fun s56 () (_ BitVec 8) #x36)
[GOOD] (define-fun s57 () (_ BitVec 8) #x37)
[GOOD] (define-fun s58 () (_ BitVec 8) #x38)
[GOOD] (define-fun s59 () (_ BitVec 8) #x39)
[GOOD] (define-fun s60 () (_ BitVec 8) #x3a)
[GOOD] (define-fun s61 () (_ BitVec 8) #x3b)
[GOOD] (define-fun s62 () (_ BitVec 8) #x3c)
[GOOD] (define-fun s63 () (_ BitVec 8) #x3d)
[GOOD] (define-fun s64 () (_ BitVec 8) #x3e)
[GOOD] (define-fun s65 () (_ BitVec 8) #x3f)
[GOOD] (define-fun s66 () (_ BitVec 8) #x40)
[GOOD] (define-fun s67 () (_ BitVec 8) #x41)
[GOOD] (define-fun s68 () (_ BitVec 8) #x42)
[GOOD] (define-fun s69 () (_ BitVec 8) #x43)
[GOOD] (define-fun s70 () (_ BitVec 8) #x44)
[GOOD] (define-fun s71 () (_ BitVec 8) #x45)
[GOOD] (define-fun s72 () (_ BitVec 8) #x46)
[GOOD] (define-fun s73 () (_ BitVec 8) #x47)
[GOOD] (define-fun s74 () (_ BitVec 8) #x48)
[GOOD] (define-fun s75 () (_ BitVec 8) #x49)
[GOOD] (define-fun s76 () (_ BitVec 8) #x4a)
[GOOD] (define-fun s77 () (_ BitVec 8) #x4b)
[GOOD] (define-fun s78 () (_ BitVec 8) #x4c)
[GOOD] (define-fun s79 () (_ BitVec 8) #x4d)
[GOOD] (define-fun s80 () (_ BitVec 8) #x4e)
[GOOD] (define-fun s81 () (_ BitVec 8) #x4f)
[GOOD] (define-fun s82 () (_ BitVec 8) #x50)
[GOOD] (define-fun s83 () (_ BitVec 8) #x51)
[GOOD] (define-fun s84 () (_ BitVec 8) #x52)
[GOOD] (define-fun s85 () (_ BitVec 8) #x53)
[GOOD] (define-fun s86 () (_ BitVec 8) #x54)
[GOOD] (define-fun s87 () (_ BitVec 8) #x55)
[GOOD] (define-fun s88 () (_ BitVec 8) #x56)
[GOOD] (define-fun s89 () (_ BitVec 8) #x57)
[GOOD] (define-fun s90 () (_ BitVec 8) #x58)
[GOOD] (define-fun s91 () (_ BitVec 8) #x59)
[GOOD] (define-fun s92 () (_ BitVec 8) #x5a)
[GOOD] (define-fun s93 () (_ BitVec 8) #x5b)
[GOOD] (define-fun s94 () (_ BitVec 8) #x5c)
[GOOD] (define-fun s95 () (_ BitVec 8) #x5d)
[GOOD] (define-fun s96 () (_ BitVec 8) #x5e)
[GOOD] (define-fun s97 () (_ BitVec 8) #x5f)
[GOOD] (define-fun s98 () (_ BitVec 8) #x60)
[GOOD] (define-fun s99 () (_ BitVec 8) #x61)
[GOOD] (define-fun s100 () (_ BitVec 8) #x62)
[GOOD] (define-fun s101 () (_ BitVec 8) #x63)
[GOOD] (define-fun s102 () (_ BitVec 8) #x64)
[GOOD] (define-fun s103 () (_ BitVec 8) #x65)
[GOOD] (define-fun s104 () (_ BitVec 8) #x66)
[GOOD] (define-fun s105 () (_ BitVec 8) #x67)
[GOOD] (define-fun s106 () (_ BitVec 8) #x68)
[GOOD] (define-fun s107 () (_ BitVec 8) #x69)
[GOOD] (define-fun s108 () (_ BitVec 8) #x6a)
[GOOD] (define-fun s109 () (_ BitVec 8) #x6b)
[GOOD] (define-fun s110 () (_ BitVec 8) #x6c)
[GOOD] (define-fun s111 () (_ BitVec 8) #x6d)
[GOOD] (define-fun s112 () (_ BitVec 8) #x6e)
[GOOD] (define-fun s113 () (_ BitVec 8) #x6f)
[GOOD] (define-fun s114 () (_ BitVec 8) #x70)
[GOOD] (define-fun s115 () (_ BitVec 8) #x71)
[GOOD] (define-fun s116 () (_ BitVec 8) #x72)
[GOOD] (define-fun s117 () (_ BitVec 8) #x73)
[GOOD] (define-fun s118 () (_ BitVec 8) #x74)
[GOOD] (define-fun s119 () (_ BitVec 8) #x75)
[GOOD] (define-fun s120 () (_ BitVec 8) #x76)
[GOOD] (define-fun s121 () (_ BitVec 8) #x77)
[GOOD] (define-fun s122 () (_ BitVec 8) #x78)
[GOOD] (define-fun s123 () (_ BitVec 8) #x79)
[GOOD] (define-fun s124 () (_ BitVec 8) #x7a)
[GOOD] (define-fun s125 () (_ BitVec 8) #x7b)
[GOOD] (define-fun s126 () (_ BitVec 8) #x7c)
[GOOD] (define-fun s127 () (_ BitVec 8) #x7d)
[GOOD] (define-fun s128 () (_ BitVec 8) #x7e)
[GOOD] (define-fun s129 () (_ BitVec 8) #x7f)
[GOOD] (define-fun s130 () (_ BitVec 8) #x80)
[GOOD] (define-fun s131 () (_ BitVec 8) #x81)
[GOOD] (define-fun s132 () (_ BitVec 8) #x82)
[GOOD] (define-fun s133 () (_ BitVec 8) #x83)
[GOOD] (define-fun s134 () (_ BitVec 8) #x84)
[GOOD] (define-fun s135 () (_ BitVec 8) #x85)
[GOOD] (define-fun s136 () (_ BitVec 8) #x86)
[GOOD] (define-fun s137 () (_ BitVec 8) #x87)
[GOOD] (define-fun s138 () (_ BitVec 8) #x88)
[GOOD] (define-fun s139 () (_ BitVec 8) #x89)
[GOOD] (define-fun s140 () (_ BitVec 8) #x8a)
[GOOD] (define-fun s141 () (_ BitVec 8) #x8b)
[GOOD] (define-fun s142 () (_ BitVec 8) #x8c)
[GOOD] (define-fun s143 () (_ BitVec 8) #x8d)
[GOOD] (define-fun s144 () (_ BitVec 8) #x8e)
[GOOD] (define-fun s145 () (_ BitVec 8) #x8f)
[GOOD] (define-fun s146 () (_ BitVec 8) #x90)
[GOOD] (define-fun s147 () (_ BitVec 8) #x91)
[GOOD] (define-fun s148 () (_ BitVec 8) #x92)
[GOOD] (define-fun s149 () (_ BitVec 8) #x93)
[GOOD] (define-fun s150 () (_ BitVec 8) #x94)
[GOOD] (define-fun s151 () (_ BitVec 8) #x95)
[GOOD] (define-fun s152 () (_ BitVec 8) #x96)
[GOOD] (define-fun s153 () (_ BitVec 8) #x97)
[GOOD] (define-fun s154 () (_ BitVec 8) #x98)
[GOOD] (define-fun s155 () (_ BitVec 8) #x99)
[GOOD] (define-fun s156 () (_ BitVec 8) #x9a)
[GOOD] (define-fun s157 () (_ BitVec 8) #x9b)
[GOOD] (define-fun s158 () (_ BitVec 8) #x9c)
[GOOD] (define-fun s159 () (_ BitVec 8) #x9d)
[GOOD] (define-fun s160 () (_ BitVec 8) #x9e)
[GOOD] (define-fun s161 () (_ BitVec 8) #x9f)
[GOOD] (define-fun s162 () (_ BitVec 8) #xa0)
[GOOD] (define-fun s163 () (_ BitVec 8) #xa1)
[GOOD] (define-fun s164 () (_ BitVec 8) #xa2)
[GOOD] (define-fun s165 () (_ BitVec 8) #xa3)
[GOOD] (define-fun s166 () (_ BitVec 8) #xa4)
[GOOD] (define-fun s167 () (_ BitVec 8) #xa5)
[GOOD] (define-fun s168 () (_ BitVec 8) #xa6)
[GOOD] (define-fun s169 () (_ BitVec 8) #xa7)
[GOOD] (define-fun s170 () (_ BitVec 8) #xa8)
[GOOD] (define-fun s171 () (_ BitVec 8) #xa9)
[GOOD] (define-fun s172 () (_ BitVec 8) #xaa)
[GOOD] (define-fun s173 () (_ BitVec 8) #xab)
[GOOD] (define-fun s174 () (_ BitVec 8) #xac)
[GOOD] (define-fun s175 () (_ BitVec 8) #xad)
[GOOD] (define-fun s176 () (_ BitVec 8) #xae)
[GOOD] (define-fun s177 () (_ BitVec 8) #xaf)
[GOOD] (define-fun s178 () (_ BitVec 8) #xb0)
[GOOD] (define-fun s179 () (_ BitVec 8) #xb1)
[GOOD] (define-fun s180 () (_ BitVec 8) #xb2)
[GOOD] (define-fun s181 () (_ BitVec 8) #xb3)
[GOOD] (define-fun s182 () (_ BitVec 8) #xb4)
[GOOD] (define-fun s183 () (_ BitVec 8) #xb5)
[GOOD] (define-fun s184 () (_ BitVec 8) #xb6)
[GOOD] (define-fun s185 () (_ BitVec 8) #xb7)
[GOOD] (define-fun s186 () (_ BitVec 8) #xb8)
[GOOD] (define-fun s187 () (_ BitVec 8) #xb9)
[GOOD] (define-fun s188 () (_ BitVec 8) #xba)
[GOOD] (define-fun s189 () (_ BitVec 8) #xbb)
[GOOD] (define-fun s190 () (_ BitVec 8) #xbc)
[GOOD] (define-fun s191 () (_ BitVec 8) #xbd)
[GOOD] (define-fun s192 () (_ BitVec 8) #xbe)
[GOOD] (define-fun s193 () (_ BitVec 8) #xbf)
[GOOD] (define-fun s194 () (_ BitVec 8) #xc0)
[GOOD] (define-fun s195 () (_ BitVec 8) #xc1)
[GOOD] (define-fun s196 () (_ BitVec 8) #xc2)
[GOOD] (define-fun s197 () (_ BitVec 8) #xc3)
[GOOD] (define-fun s198 () (_ BitVec 8) #xc4)
[GOOD] (define-fun s199 () (_ BitVec 8) #xc5)
[GOOD] (define-fun s200 () (_ BitVec 8) #xc6)
[GOOD] (define-fun s201 () (_ BitVec 8) #xc7)
[GOOD] (define-fun s202 () (_ BitVec 8) #xc8)
[GOOD] (define-fun s203 () (_ BitVec 8) #xc9)
[GOOD] (define-fun s204 () (_ BitVec 8) #xca)
[GOOD] (define-fun s205 () (_ BitVec 8) #xcb)
[GOOD] (define-fun s206 () (_ BitVec 8) #xcc)
[GOOD] (define-fun s207 () (_ BitVec 8) #xcd)
[GOOD] (define-fun s208 () (_ BitVec 8) #xce)
[GOOD] (define-fun s209 () (_ BitVec 8) #xcf)
[GOOD] (define-fun s210 () (_ BitVec 8) #xd0)
[GOOD] (define-fun s211 () (_ BitVec 8) #xd1)
[GOOD] (define-fun s212 () (_ BitVec 8) #xd2)
[GOOD] (define-fun s213 () (_ BitVec 8) #xd3)
[GOOD] (define-fun s214 () (_ BitVec 8) #xd4)
[GOOD] (define-fun s215 () (_ BitVec 8) #xd5)
[GOOD] (define-fun s216 () (_ BitVec 8) #xd6)
[GOOD] (define-fun s217 () (_ BitVec 8) #xd7)
[GOOD] (define-fun s218 () (_ BitVec 8) #xd8)
[GOOD] (define-fun s219 () (_ BitVec 8) #xd9)
[GOOD] (define-fun s220 () (_ BitVec 8) #xda)
[GOOD] (define-fun s221 () (_ BitVec 8) #xdb)
[GOOD] (define-fun s222 () (_ BitVec 8) #xdc)
[GOOD] (define-fun s223 () (_ BitVec 8) #xdd)
[GOOD] (define-fun s224 () (_ BitVec 8) #xde)
[GOOD] (define-fun s225 () (_ BitVec 8) #xdf)
[GOOD] (define-fun s226 () (_ BitVec 8) #xe0)
[GOOD] (define-fun s227 () (_ BitVec 8) #xe1)
[GOOD] (define-fun s228 () (_ BitVec 8) #xe2)
[GOOD] (define-fun s229 () (_ BitVec 8) #xe3)
[GOOD] (define-fun s230 () (_ BitVec 8) #xe4)
[GOOD] (define-fun s231 () (_ BitVec 8) #xe5)
[GOOD] (define-fun s232 () (_ BitVec 8) #xe6)
[GOOD] (define-fun s233 () (_ BitVec 8) #xe7)
[GOOD] (define-fun s234 () (_ BitVec 8) #xe8)
[GOOD] (define-fun s235 () (_ BitVec 8) #xe9)
[GOOD] (define-fun s236 () (_ BitVec 8) #xea)
[GOOD] (define-fun s237 () (_ BitVec 8) #xeb)
[GOOD] (define-fun s238 () (_ BitVec 8) #xec)
[GOOD] (define-fun s239 () (_ BitVec 8) #xed)
[GOOD] (define-fun s240 () (_ BitVec 8) #xee)
[GOOD] (define-fun s241 () (_ BitVec 8) #xef)
[GOOD] (define-fun s242 () (_ BitVec 8) #xf0)
[GOOD] (define-fun s243 () (_ BitVec 8) #xf1)
[GOOD] (define-fun s244 () (_ BitVec 8) #xf2)
[GOOD] (define-fun s245 () (_ BitVec 8) #xf3)
[GOOD] (define-fun s246 () (_ BitVec 8) #xf4)
[GOOD] (define-fun s247 () (_ BitVec 8) #xf5)
[GOOD] (define-fun s248 () (_ BitVec 8) #xf6)
[GOOD] (define-fun s249 () (_ BitVec 8) #xf7)
[GOOD] (define-fun s250 () (_ BitVec 8) #xf8)
[GOOD] (define-fun s251 () (_ BitVec 8) #xf9)
[GOOD] (define-fun s252 () (_ BitVec 8) #xfa)
[GOOD] (define-fun s253 () (_ BitVec 8) #xfb)
[GOOD] (define-fun s254 () (_ BitVec 8) #xfc)
[GOOD] (define-fun s255 () (_ BitVec 8) #xfd)
[GOOD] (define-fun s256 () (_ BitVec 8) #xfe)
[GOOD] (define-fun s257 () (_ BitVec 8) #xff)
[GOOD] (declare-fun table0 ((_ BitVec 8)) (_ BitVec 8))
[GOOD] (assert (= (table0 #x00) s2))
[GOOD] (assert (= (table0 #x01) s3))
[GOOD] (assert (= (table0 #x02) s4))
[GOOD] (assert (= (table0 #x03) s5))
[GOOD] (assert (= (table0 #x04) s6))
[GOOD] (assert (= (table0 #x05) s7))
[GOOD] (assert (= (table0 #x06) s8))
[GOOD] (assert (= (table0 #x07) s9))
[GOOD] (assert (= (table0 #x08) s10))
[GOOD] (assert (= (table0 #x09) s11))
[GOOD] (assert (= (table0 #x0a) s12))
[GOOD] (assert (= (table0 #x0b) s13))
[GOOD] (assert (= (table0 #x0c) s14))
[GOOD] (assert (= (table0 #x0d) s15))
[GOOD] (assert (= (table0 #x0e) s16))
[GOOD] (assert (= (table0 #x0f) s17))
[GOOD] (assert (= (table0 #x10) s18))
[GOOD] (assert (= (table0 #x11) s19))
[GOOD] (assert (= (table0 #x12) s20))
[GOOD] (assert (= (table0 #x13) s21))
[GOOD] (assert (= (table0 #x14) s22))
[GOOD] (assert (= (table0 #x15) s23))
[GOOD] (assert (= (table0 #x16) s24))
[GOOD] (assert (= (table0 #x17) s25))
[GOOD] (assert (= (table0 #x18) s26))
[GOOD] (assert (= (table0 #x19) s27))
[GOOD] (assert (= (table0 #x1a) s28))
[GOOD] (assert (= (table0 #x1b) s29))
[GOOD] (assert (= (table0 #x1c) s30))
[GOOD] (assert (= (table0 #x1d) s31))
[GOOD] (assert (= (table0 #x1e) s32))
[GOOD] (assert (= (table0 #x1f) s33))
[GOOD] (assert (= (table0 #x20) s34))
[GOOD] (assert (= (table0 #x21) s35))
[GOOD] (assert (= (table0 #x22) s36))
[GOOD] (assert (= (table0 #x23) s37))
[GOOD] (assert (= (table0 #x24) s38))
[GOOD] (assert (= (table0 #x25) s39))
[GOOD] (assert (= (table0 #x26) s40))
[GOOD] (assert (= (table0 #x27) s41))
[GOOD] (assert (= (table0 #x28) s42))
[GOOD] (assert (= (table0 #x29) s43))
[GOOD] (assert (= (table0 #x2a) s44))
[GOOD] (assert (= (table0 #x2b) s45))
[GOOD] (assert (= (table0 #x2c) s46))
[GOOD] (assert (= (table0 #x2d) s47))
[GOOD] (assert (= (table0 #x2e) s48))
[GOOD] (assert (= (table0 #x2f) s49))
[GOOD] (assert (= (table0 #x30) s50))
[GOOD] (assert (= (table0 #x31) s51))
[GOOD] (assert (= (table0 #x32) s52))
[GOOD] (assert (= (table0 #x33) s53))
[GOOD] (assert (= (table0 #x34) s54))
[GOOD] (assert (= (table0 #x35) s55))
[GOOD] (assert (= (table0 #x36) s56))
[GOOD] (assert (= (table0 #x37) s57))
[GOOD] (assert (= (table0 #x38) s58))
[GOOD] (assert (= (table0 #x39) s59))
[GOOD] (assert (= (table0 #x3a) s60))
[GOOD] (assert (= (table0 #x3b) s61))
[GOOD] (assert (= (table0 #x3c) s62))
[GOOD] (assert (= (table0 #x3d) s63))
[GOOD] (assert (= (table0 #x3e) s64))
[GOOD] (assert (= (table0 #x3f) s65))
[GOOD] (assert (= (table0 #x40) s66))
[GOOD] (assert (= (table0 #x41) s67))
[GOOD] (assert (= (table0 #x42) s68))
[GOOD] (assert (= (table0 #x43) s69))
[GOOD] (assert (= (table0 #x44) s70))
[GOOD] (assert (= (table0 #x45) s71))
[GOOD] (assert (= (table0 #x46) s72))
[GOOD] (assert (= (table0 #x47) s73))
[GOOD] (assert (= (table0 #x48) s74))
[GOOD] (assert (= (table0 #x49) s75))
[GOOD] (assert (= (table0 #x4a) s76))
[GOOD] (assert (= (table0 #x4b) s77))
[GOOD] (assert (= (table0 #x4c) s78))
[GOOD] (assert (= (table0 #x4d) s79))
[GOOD] (assert (= (table0 #x4e) s80))
[GOOD] (assert (= (table0 #x4f) s81))
[GOOD] (assert (= (table0 #x50) s82))
[GOOD] (assert (= (table0 #x51) s83))
[GOOD] (assert (= (table0 #x52) s84))
[GOOD] (assert (= (table0 #x53) s85))
[GOOD] (assert (= (table0 #x54) s86))
[GOOD] (assert (= (table0 #x55) s87))
[GOOD] (assert (= (table0 #x56) s88))
[GOOD] (assert (= (table0 #x57) s89))
[GOOD] (assert (= (table0 #x58) s90))
[GOOD] (assert (= (table0 #x59) s91))
[GOOD] (assert (= (table0 #x5a) s92))
[GOOD] (assert (= (table0 #x5b) s93))
[GOOD] (assert (= (table0 #x5c) s94))
[GOOD] (assert (= (table0 #x5d) s95))
[GOOD] (assert (= (table0 #x5e) s96))
[GOOD] (assert (= (table0 #x5f) s97))
[GOOD] (assert (= (table0 #x60) s98))
[GOOD] (assert (= (table0 #x61) s99))
[GOOD] (assert (= (table0 #x62) s100))
[GOOD] (assert (= (table0 #x63) s101))
[GOOD] (assert (= (table0 #x64) s102))
[GOOD] (assert (= (table0 #x65) s103))
[GOOD] (assert (= (table0 #x66) s104))
[GOOD] (assert (= (table0 #x67) s105))
[GOOD] (assert (= (table0 #x68) s106))
[GOOD] (assert (= (table0 #x69) s107))
[GOOD] (assert (= (table0 #x6a) s108))
[GOOD] (assert (= (table0 #x6b) s109))
[GOOD] (assert (= (table0 #x6c) s110))
[GOOD] (assert (= (table0 #x6d) s111))
[GOOD] (assert (= (table0 #x6e) s112))
[GOOD] (assert (= (table0 #x6f) s113))
[GOOD] (assert (= (table0 #x70) s114))
[GOOD] (assert (= (table0 #x71) s115))
[GOOD] (assert (= (table0 #x72) s116))
[GOOD] (assert (= (table0 #x73) s117))
[GOOD] (assert (= (table0 #x74) s118))
[GOOD] (assert (= (table0 #x75) s119))
[GOOD] (assert (= (table0 #x76) s120))
[GOOD] (assert (= (table0 #x77) s121))
[GOOD] (assert (= (table0 #x78) s122))
[GOOD] (assert (= (table0 #x79) s123))
[GOOD] (assert (= (table0 #x7a) s124))
[GOOD] (assert (= (table0 #x7b) s125))
[GOOD] (assert (= (table0 #x7c) s126))
[GOOD] (assert (= (table0 #x7d) s127))
[GOOD] (assert (= (table0 #x7e) s128))
[GOOD] (assert (= (table0 #x7f) s129))
[GOOD] (assert (= (table0 #x80) s130))
[GOOD] (assert (= (table0 #x81) s131))
[GOOD] (assert (= (table0 #x82) s132))
[GOOD] (assert (= (table0 #x83) s133))
[GOOD] (assert (= (table0 #x84) s134))
[GOOD] (assert (= (table0 #x85) s135))
[GOOD] (assert (= (table0 #x86) s136))
[GOOD] (assert (= (table0 #x87) s137))
[GOOD] (assert (= (table0 #x88) s138))
[GOOD] (assert (= (table0 #x89) s139))
[GOOD] (assert (= (table0 #x8a) s140))
[GOOD] (assert (= (table0 #x8b) s141))
[GOOD] (assert (= (table0 #x8c) s142))
[GOOD] (assert (= (table0 #x8d) s143))
[GOOD] (assert (= (table0 #x8e) s144))
[GOOD] (assert (= (table0 #x8f) s145))
[GOOD] (assert (= (table0 #x90) s146))
[GOOD] (assert (= (table0 #x91) s147))
[GOOD] (assert (= (table0 #x92) s148))
[GOOD] (assert (= (table0 #x93) s149))
[GOOD] (assert (= (table0 #x94) s150))
[GOOD] (assert (= (table0 #x95) s151))
[GOOD] (assert (= (table0 #x96) s152))
[GOOD] (assert (= (table0 #x97) s153))
[GOOD] (assert (= (table0 #x98) s154))
[GOOD] (assert (= (table0 #x99) s155))
[GOOD] (assert (= (table0 #x9a) s156))
[GOOD] (assert (= (table0 #x9b) s157))
[GOOD] (assert (= (table0 #x9c) s158))
[GOOD] (assert (= (table0 #x9d) s159))
[GOOD] (assert (= (table0 #x9e) s160))
[GOOD] (assert (= (table0 #x9f) s161))
[GOOD] (assert (= (table0 #xa0) s162))
[GOOD] (assert (= (table0 #xa1) s163))
[GOOD] (assert (= (table0 #xa2) s164))
[GOOD] (assert (= (table0 #xa3) s165))
[GOOD] (assert (= (table0 #xa4) s166))
[GOOD] (assert (= (table0 #xa5) s167))
[GOOD] (assert (= (table0 #xa6) s168))
[GOOD] (assert (= (table0 #xa7) s169))
[GOOD] (assert (= (table0 #xa8) s170))
[GOOD] (assert (= (table0 #xa9) s171))
[GOOD] (assert (= (table0 #xaa) s172))
[GOOD] (assert (= (table0 #xab) s173))
[GOOD] (assert (= (table0 #xac) s174))
[GOOD] (assert (= (table0 #xad) s175))
[GOOD] (assert (= (table0 #xae) s176))
[GOOD] (assert (= (table0 #xaf) s177))
[GOOD] (assert (= (table0 #xb0) s178))
[GOOD] (assert (= (table0 #xb1) s179))
[GOOD] (assert (= (table0 #xb2) s180))
[GOOD] (assert (= (table0 #xb3) s181))
[GOOD] (assert (= (table0 #xb4) s182))
[GOOD] (assert (= (table0 #xb5) s183))
[GOOD] (assert (= (table0 #xb6) s184))
[GOOD] (assert (= (table0 #xb7) s185))
[GOOD] (assert (= (table0 #xb8) s186))
[GOOD] (assert (= (table0 #xb9) s187))
[GOOD] (assert (= (table0 #xba) s188))
[GOOD] (assert (= (table0 #xbb) s189))
[GOOD] (assert (= (table0 #xbc) s190))
[GOOD] (assert (= (table0 #xbd) s191))
[GOOD] (assert (= (table0 #xbe) s192))
[GOOD] (assert (= (table0 #xbf) s193))
[GOOD] (assert (= (table0 #xc0) s194))
[GOOD] (assert (= (table0 #xc1) s195))
[GOOD] (assert (= (table0 #xc2) s196))
[GOOD] (assert (= (table0 #xc3) s197))
[GOOD] (assert (= (table0 #xc4) s198))
[GOOD] (assert (= (table0 #xc5) s199))
[GOOD] (assert (= (table0 #xc6) s200))
[GOOD] (assert (= (table0 #xc7) s201))
[GOOD] (assert (= (table0 #xc8) s202))
[GOOD] (assert (= (table0 #xc9) s203))
[GOOD] (assert (= (table0 #xca) s204))
[GOOD] (assert (= (table0 #xcb) s205))
[GOOD] (assert (= (table0 #xcc) s206))
[GOOD] (assert (= (table0 #xcd) s207))
[GOOD] (assert (= (table0 #xce) s208))
[GOOD] (assert (= (table0 #xcf) s209))
[GOOD] (assert (= (table0 #xd0) s210))
[GOOD] (assert (= (table0 #xd1) s211))
[GOOD] (assert (= (table0 #xd2) s212))
[GOOD] (assert (= (table0 #xd3) s213))
[GOOD] (assert (= (table0 #xd4) s214))
[GOOD] (assert (= (table0 #xd5) s215))
[GOOD] (assert (= (table0 #xd6) s216))
[GOOD] (assert (= (table0 #xd7) s217))
[GOOD] (assert (= (table0 #xd8) s218))
[GOOD] (assert (= (table0 #xd9) s219))
[GOOD] (assert (= (table0 #xda) s220))
[GOOD] (assert (= (table0 #xdb) s221))
[GOOD] (assert (= (table0 #xdc) s222))
[GOOD] (assert (= (table0 #xdd) s223))
[GOOD] (assert (= (table0 #xde) s224))
[GOOD] (assert (= (table0 #xdf) s225))
[GOOD] (assert (= (table0 #xe0) s226))
[GOOD] (assert (= (table0 #xe1) s227))
[GOOD] (assert (= (table0 #xe2) s228))
[GOOD] (assert (= (table0 #xe3) s229))
[GOOD] (assert (= (table0 #xe4) s230))
[GOOD] (assert (= (table0 #xe5) s231))
[GOOD] (assert (= (table0 #xe6) s232))
[GOOD] (assert (= (table0 #xe7) s233))
[GOOD] (assert (= (table0 #xe8) s234))
[GOOD] (assert (= (table0 #xe9) s235))
[GOOD] (assert (= (table0 #xea) s236))
[GOOD] (assert (= (table0 #xeb) s237))
[GOOD] (assert (= (table0 #xec) s238))
[GOOD] (assert (= (table0 #xed) s239))
[GOOD] (assert (= (table0 #xee) s240))
[GOOD] (assert (= (table0 #xef) s241))
[GOOD] (assert (= (table0 #xf0) s242))
[GOOD] (assert (= (table0 #xf1) s243))
[GOOD] (assert (= (table0 #xf2) s244))
[GOOD] (assert (= (table0 #xf3) s245))
[GOOD] (assert (= (table0 #xf4) s246))
[GOOD] (assert (= (table0 #xf5) s247))
[GOOD] (assert (= (table0 #xf6) s248))
[GOOD] (assert (= (table0 #xf7) s249))
[GOOD] (assert (= (table0 #xf8) s250))
[GOOD] (assert (= (table0 #xf9) s251))
[GOOD] (assert (= (table0 #xfa) s252))
[GOOD] (assert (= (table0 #xfb) s253))
[GOOD] (assert (= (table0 #xfc) s254))
[GOOD] (assert (= (table0 #xfd) s255))
[GOOD] (assert (= (table0 #xfe) s256))
[GOOD] (assert (= (table0 #xff) s257))
[GOOD] (define-fun s258 () (_ BitVec 8) (table0 s0))
[GOOD] (define-fun s259 () Bool (= s0 s258))
[GOOD] (assert s259)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 #x00))
[GOOD] (define-fun s260 () (_ BitVec 8) (table0 s1))
[GOOD] (define-fun s261 () Bool (= s1 s260))
[GOOD] (assert s261)
[GOOD] (define-fun s262 () (_ BitVec 8) (bvadd s0 s3))
[GOOD] (define-fun s263 () Bool (= s1 s262))
[GOOD] (assert s263)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s1))
[RECV] ((s1 #x01))
*** Solver   : Z3
*** Exit code: ExitSuccess

 FINAL:(0,1)
DONE!