** 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] ; --- literal constants ---
[GOOD] ; --- skolem constants ---
[GOOD] (declare-fun s0 () (_ BitVec 8)) ; tracks user variable "i"
[GOOD] ; --- constant tables ---
[GOOD] ; --- skolemized tables ---
[GOOD] ; --- arrays ---
[GOOD] ; --- uninterpreted constants ---
[GOOD] ; --- user given axioms ---
[GOOD] ; --- formula ---
[GOOD] (define-fun s1 () (_ BitVec 8) #x00)
[GOOD] (declare-fun table0 ((_ BitVec 8)) (_ BitVec 8))
[GOOD] (assert (= (table0 #x00) s0))
[GOOD] (assert (= (table0 #x01) s0))
[GOOD] (assert (= (table0 #x02) s0))
[GOOD] (assert (= (table0 #x03) s0))
[GOOD] (assert (= (table0 #x04) s0))
[GOOD] (assert (= (table0 #x05) s0))
[GOOD] (assert (= (table0 #x06) s0))
[GOOD] (assert (= (table0 #x07) s0))
[GOOD] (assert (= (table0 #x08) s0))
[GOOD] (assert (= (table0 #x09) s0))
[GOOD] (assert (= (table0 #x0a) s0))
[GOOD] (assert (= (table0 #x0b) s0))
[GOOD] (assert (= (table0 #x0c) s0))
[GOOD] (assert (= (table0 #x0d) s0))
[GOOD] (assert (= (table0 #x0e) s0))
[GOOD] (assert (= (table0 #x0f) s0))
[GOOD] (assert (= (table0 #x10) s0))
[GOOD] (assert (= (table0 #x11) s0))
[GOOD] (assert (= (table0 #x12) s0))
[GOOD] (assert (= (table0 #x13) s0))
[GOOD] (assert (= (table0 #x14) s0))
[GOOD] (assert (= (table0 #x15) s0))
[GOOD] (assert (= (table0 #x16) s0))
[GOOD] (assert (= (table0 #x17) s0))
[GOOD] (assert (= (table0 #x18) s0))
[GOOD] (assert (= (table0 #x19) s0))
[GOOD] (assert (= (table0 #x1a) s0))
[GOOD] (assert (= (table0 #x1b) s0))
[GOOD] (assert (= (table0 #x1c) s0))
[GOOD] (assert (= (table0 #x1d) s0))
[GOOD] (assert (= (table0 #x1e) s0))
[GOOD] (assert (= (table0 #x1f) s0))
[GOOD] (assert (= (table0 #x20) s0))
[GOOD] (assert (= (table0 #x21) s0))
[GOOD] (assert (= (table0 #x22) s0))
[GOOD] (assert (= (table0 #x23) s0))
[GOOD] (assert (= (table0 #x24) s0))
[GOOD] (assert (= (table0 #x25) s0))
[GOOD] (assert (= (table0 #x26) s0))
[GOOD] (assert (= (table0 #x27) s0))
[GOOD] (assert (= (table0 #x28) s0))
[GOOD] (assert (= (table0 #x29) s0))
[GOOD] (assert (= (table0 #x2a) s0))
[GOOD] (assert (= (table0 #x2b) s0))
[GOOD] (assert (= (table0 #x2c) s0))
[GOOD] (assert (= (table0 #x2d) s0))
[GOOD] (assert (= (table0 #x2e) s0))
[GOOD] (assert (= (table0 #x2f) s0))
[GOOD] (assert (= (table0 #x30) s0))
[GOOD] (assert (= (table0 #x31) s0))
[GOOD] (assert (= (table0 #x32) s0))
[GOOD] (assert (= (table0 #x33) s0))
[GOOD] (assert (= (table0 #x34) s0))
[GOOD] (assert (= (table0 #x35) s0))
[GOOD] (assert (= (table0 #x36) s0))
[GOOD] (assert (= (table0 #x37) s0))
[GOOD] (assert (= (table0 #x38) s0))
[GOOD] (assert (= (table0 #x39) s0))
[GOOD] (assert (= (table0 #x3a) s0))
[GOOD] (assert (= (table0 #x3b) s0))
[GOOD] (assert (= (table0 #x3c) s0))
[GOOD] (assert (= (table0 #x3d) s0))
[GOOD] (assert (= (table0 #x3e) s0))
[GOOD] (assert (= (table0 #x3f) s0))
[GOOD] (assert (= (table0 #x40) s0))
[GOOD] (assert (= (table0 #x41) s0))
[GOOD] (assert (= (table0 #x42) s0))
[GOOD] (assert (= (table0 #x43) s0))
[GOOD] (assert (= (table0 #x44) s0))
[GOOD] (assert (= (table0 #x45) s0))
[GOOD] (assert (= (table0 #x46) s0))
[GOOD] (assert (= (table0 #x47) s0))
[GOOD] (assert (= (table0 #x48) s0))
[GOOD] (assert (= (table0 #x49) s0))
[GOOD] (assert (= (table0 #x4a) s0))
[GOOD] (assert (= (table0 #x4b) s0))
[GOOD] (assert (= (table0 #x4c) s0))
[GOOD] (assert (= (table0 #x4d) s0))
[GOOD] (assert (= (table0 #x4e) s0))
[GOOD] (assert (= (table0 #x4f) s0))
[GOOD] (assert (= (table0 #x50) s0))
[GOOD] (assert (= (table0 #x51) s0))
[GOOD] (assert (= (table0 #x52) s0))
[GOOD] (assert (= (table0 #x53) s0))
[GOOD] (assert (= (table0 #x54) s0))
[GOOD] (assert (= (table0 #x55) s0))
[GOOD] (assert (= (table0 #x56) s0))
[GOOD] (assert (= (table0 #x57) s0))
[GOOD] (assert (= (table0 #x58) s0))
[GOOD] (assert (= (table0 #x59) s0))
[GOOD] (assert (= (table0 #x5a) s0))
[GOOD] (assert (= (table0 #x5b) s0))
[GOOD] (assert (= (table0 #x5c) s0))
[GOOD] (assert (= (table0 #x5d) s0))
[GOOD] (assert (= (table0 #x5e) s0))
[GOOD] (assert (= (table0 #x5f) s0))
[GOOD] (assert (= (table0 #x60) s0))
[GOOD] (assert (= (table0 #x61) s0))
[GOOD] (assert (= (table0 #x62) s0))
[GOOD] (assert (= (table0 #x63) s0))
[GOOD] (assert (= (table0 #x64) s0))
[GOOD] (assert (= (table0 #x65) s0))
[GOOD] (assert (= (table0 #x66) s0))
[GOOD] (assert (= (table0 #x67) s0))
[GOOD] (assert (= (table0 #x68) s0))
[GOOD] (assert (= (table0 #x69) s0))
[GOOD] (assert (= (table0 #x6a) s0))
[GOOD] (assert (= (table0 #x6b) s0))
[GOOD] (assert (= (table0 #x6c) s0))
[GOOD] (assert (= (table0 #x6d) s0))
[GOOD] (assert (= (table0 #x6e) s0))
[GOOD] (assert (= (table0 #x6f) s0))
[GOOD] (assert (= (table0 #x70) s0))
[GOOD] (assert (= (table0 #x71) s0))
[GOOD] (assert (= (table0 #x72) s0))
[GOOD] (assert (= (table0 #x73) s0))
[GOOD] (assert (= (table0 #x74) s0))
[GOOD] (assert (= (table0 #x75) s0))
[GOOD] (assert (= (table0 #x76) s0))
[GOOD] (assert (= (table0 #x77) s0))
[GOOD] (assert (= (table0 #x78) s0))
[GOOD] (assert (= (table0 #x79) s0))
[GOOD] (assert (= (table0 #x7a) s0))
[GOOD] (assert (= (table0 #x7b) s0))
[GOOD] (assert (= (table0 #x7c) s0))
[GOOD] (assert (= (table0 #x7d) s0))
[GOOD] (assert (= (table0 #x7e) s0))
[GOOD] (assert (= (table0 #x7f) s0))
[GOOD] (assert (= (table0 #x80) s0))
[GOOD] (assert (= (table0 #x81) s0))
[GOOD] (assert (= (table0 #x82) s0))
[GOOD] (assert (= (table0 #x83) s0))
[GOOD] (assert (= (table0 #x84) s0))
[GOOD] (assert (= (table0 #x85) s0))
[GOOD] (assert (= (table0 #x86) s0))
[GOOD] (assert (= (table0 #x87) s0))
[GOOD] (assert (= (table0 #x88) s0))
[GOOD] (assert (= (table0 #x89) s0))
[GOOD] (assert (= (table0 #x8a) s0))
[GOOD] (assert (= (table0 #x8b) s0))
[GOOD] (assert (= (table0 #x8c) s0))
[GOOD] (assert (= (table0 #x8d) s0))
[GOOD] (assert (= (table0 #x8e) s0))
[GOOD] (assert (= (table0 #x8f) s0))
[GOOD] (assert (= (table0 #x90) s0))
[GOOD] (assert (= (table0 #x91) s0))
[GOOD] (assert (= (table0 #x92) s0))
[GOOD] (assert (= (table0 #x93) s0))
[GOOD] (assert (= (table0 #x94) s0))
[GOOD] (assert (= (table0 #x95) s0))
[GOOD] (assert (= (table0 #x96) s0))
[GOOD] (assert (= (table0 #x97) s0))
[GOOD] (assert (= (table0 #x98) s0))
[GOOD] (assert (= (table0 #x99) s0))
[GOOD] (assert (= (table0 #x9a) s0))
[GOOD] (assert (= (table0 #x9b) s0))
[GOOD] (assert (= (table0 #x9c) s0))
[GOOD] (assert (= (table0 #x9d) s0))
[GOOD] (assert (= (table0 #x9e) s0))
[GOOD] (assert (= (table0 #x9f) s0))
[GOOD] (assert (= (table0 #xa0) s0))
[GOOD] (assert (= (table0 #xa1) s0))
[GOOD] (assert (= (table0 #xa2) s0))
[GOOD] (assert (= (table0 #xa3) s0))
[GOOD] (assert (= (table0 #xa4) s0))
[GOOD] (assert (= (table0 #xa5) s0))
[GOOD] (assert (= (table0 #xa6) s0))
[GOOD] (assert (= (table0 #xa7) s0))
[GOOD] (assert (= (table0 #xa8) s0))
[GOOD] (assert (= (table0 #xa9) s0))
[GOOD] (assert (= (table0 #xaa) s0))
[GOOD] (assert (= (table0 #xab) s0))
[GOOD] (assert (= (table0 #xac) s0))
[GOOD] (assert (= (table0 #xad) s0))
[GOOD] (assert (= (table0 #xae) s0))
[GOOD] (assert (= (table0 #xaf) s0))
[GOOD] (assert (= (table0 #xb0) s0))
[GOOD] (assert (= (table0 #xb1) s0))
[GOOD] (assert (= (table0 #xb2) s0))
[GOOD] (assert (= (table0 #xb3) s0))
[GOOD] (assert (= (table0 #xb4) s0))
[GOOD] (assert (= (table0 #xb5) s0))
[GOOD] (assert (= (table0 #xb6) s0))
[GOOD] (assert (= (table0 #xb7) s0))
[GOOD] (assert (= (table0 #xb8) s0))
[GOOD] (assert (= (table0 #xb9) s0))
[GOOD] (assert (= (table0 #xba) s0))
[GOOD] (assert (= (table0 #xbb) s0))
[GOOD] (assert (= (table0 #xbc) s0))
[GOOD] (assert (= (table0 #xbd) s0))
[GOOD] (assert (= (table0 #xbe) s0))
[GOOD] (assert (= (table0 #xbf) s0))
[GOOD] (assert (= (table0 #xc0) s0))
[GOOD] (assert (= (table0 #xc1) s0))
[GOOD] (assert (= (table0 #xc2) s0))
[GOOD] (assert (= (table0 #xc3) s0))
[GOOD] (assert (= (table0 #xc4) s0))
[GOOD] (assert (= (table0 #xc5) s0))
[GOOD] (assert (= (table0 #xc6) s0))
[GOOD] (assert (= (table0 #xc7) s0))
[GOOD] (assert (= (table0 #xc8) s0))
[GOOD] (assert (= (table0 #xc9) s0))
[GOOD] (assert (= (table0 #xca) s0))
[GOOD] (assert (= (table0 #xcb) s0))
[GOOD] (assert (= (table0 #xcc) s0))
[GOOD] (assert (= (table0 #xcd) s0))
[GOOD] (assert (= (table0 #xce) s0))
[GOOD] (assert (= (table0 #xcf) s0))
[GOOD] (assert (= (table0 #xd0) s0))
[GOOD] (assert (= (table0 #xd1) s0))
[GOOD] (assert (= (table0 #xd2) s0))
[GOOD] (assert (= (table0 #xd3) s0))
[GOOD] (assert (= (table0 #xd4) s0))
[GOOD] (assert (= (table0 #xd5) s0))
[GOOD] (assert (= (table0 #xd6) s0))
[GOOD] (assert (= (table0 #xd7) s0))
[GOOD] (assert (= (table0 #xd8) s0))
[GOOD] (assert (= (table0 #xd9) s0))
[GOOD] (assert (= (table0 #xda) s0))
[GOOD] (assert (= (table0 #xdb) s0))
[GOOD] (assert (= (table0 #xdc) s0))
[GOOD] (assert (= (table0 #xdd) s0))
[GOOD] (assert (= (table0 #xde) s0))
[GOOD] (assert (= (table0 #xdf) s0))
[GOOD] (assert (= (table0 #xe0) s0))
[GOOD] (assert (= (table0 #xe1) s0))
[GOOD] (assert (= (table0 #xe2) s0))
[GOOD] (assert (= (table0 #xe3) s0))
[GOOD] (assert (= (table0 #xe4) s0))
[GOOD] (assert (= (table0 #xe5) s0))
[GOOD] (assert (= (table0 #xe6) s0))
[GOOD] (assert (= (table0 #xe7) s0))
[GOOD] (assert (= (table0 #xe8) s0))
[GOOD] (assert (= (table0 #xe9) s0))
[GOOD] (assert (= (table0 #xea) s0))
[GOOD] (assert (= (table0 #xeb) s0))
[GOOD] (assert (= (table0 #xec) s0))
[GOOD] (assert (= (table0 #xed) s0))
[GOOD] (assert (= (table0 #xee) s0))
[GOOD] (assert (= (table0 #xef) s0))
[GOOD] (assert (= (table0 #xf0) s0))
[GOOD] (assert (= (table0 #xf1) s0))
[GOOD] (assert (= (table0 #xf2) s0))
[GOOD] (assert (= (table0 #xf3) s0))
[GOOD] (assert (= (table0 #xf4) s0))
[GOOD] (assert (= (table0 #xf5) s0))
[GOOD] (assert (= (table0 #xf6) s0))
[GOOD] (assert (= (table0 #xf7) s0))
[GOOD] (assert (= (table0 #xf8) s0))
[GOOD] (assert (= (table0 #xf9) s0))
[GOOD] (assert (= (table0 #xfa) s0))
[GOOD] (assert (= (table0 #xfb) s0))
[GOOD] (assert (= (table0 #xfc) s0))
[GOOD] (assert (= (table0 #xfd) s0))
[GOOD] (assert (= (table0 #xfe) s0))
[GOOD] (assert (= (table0 #xff) s0))
[GOOD] (define-fun s2 () (_ BitVec 8) (table0 s0))
[GOOD] (define-fun s3 () Bool (= s0 s2))
[GOOD] (assert s3)
[SEND] (check-sat)
[RECV] sat
[SEND] (get-value (s0))
[RECV] ((s0 #x00))
*** Solver   : Z3
*** Exit code: ExitSuccess

 FINAL:0
DONE!