synesthesia-symbolic-loops-twobyte-reducedscstate-chunkloopbody-printable-expandedimplication-removedgeneralimplication.ys

; Loosen yices' arbitrary restriction on iteration count. (')
(set-param ef-max-iters 100000)
(set-param ef-max-samples 1000)
;(set-param ef-gen-mode projection)

(define-type Bit          (bitvector  1))
(define-type Nibble       (bitvector  4))
(define-type Byte         (bitvector  8))
(define-type Word         (bitvector 16))
(define-type Dword        (bitvector 32))

(define-type RegIdx       (bitvector  3))
(define R0Idx::RegIdx (mk-bv 3 0)) ; R0 = 0
(define R1Idx::RegIdx (mk-bv 3 1)) ; R1 = 1
(define R2Idx::RegIdx (mk-bv 3 2)) ; R2 = 2
(define R3Idx::RegIdx (mk-bv 3 3)) ; R3 = 3
(define R4Idx::RegIdx (mk-bv 3 4)) ; R4 = 4
(define R5Idx::RegIdx (mk-bv 3 5)) ; R5 = 5
(define R6Idx::RegIdx (mk-bv 3 6)) ; R6 = 6
(define R7Idx::RegIdx (mk-bv 3 7)) ; R7 = 7

(define-type Reg32State          (bitvector 256))
(define-type SCDoubleState       (bitvector 16)) ; 0x40-length shellcode, two-byte encoding
(define-type SCState             (bitvector 8)) ; 0x40-length shellcode, two-byte encoding
	
(define-type Mnem               (bitvector    4))
(define XorRegReg   ::Mnem (mk-bv 4 0))
(define AddRegReg   ::Mnem (mk-bv 4 1))
(define MovRegReg   ::Mnem (mk-bv 4 2))
(define GetscbyteReg::Mnem (mk-bv 4 3))
(define PutscbyteReg::Mnem (mk-bv 4 4))
(define NegReg      ::Mnem (mk-bv 4 5))
(define NotReg      ::Mnem (mk-bv 4 6))
(define AddRegImm   ::Mnem (mk-bv 4 7))
(define XorRegImm   ::Mnem (mk-bv 4 8))
(define MovRegImm   ::Mnem (mk-bv 4 9))
(define JnzRegImm   ::Mnem (mk-bv 4 10))

(define-type Instruction        (bitvector  42))
;   3   0: Mnem
;   6   4: LHSReg
;   9   7: RHSReg
;  41  10: Imm32

(define-type DecodedInstruction (bitvector 60))
;  41  0: Instruction
;  42 42: Bit [extra]
;  43 43: Bit [is-jcc]
;  51 44: Byte [length]
;  59 52: Byte [nexteip]
	
(define di-get-insn::(-> DecodedInstruction Instruction)
  (lambda (di::DecodedInstruction)
    (bv-extract 41 0 di)
  )
)

(define di-get-extra::(-> DecodedInstruction bool)
  (lambda (di::DecodedInstruction)
    (= 0b1 (bv-extract 42 42 di))
  )
)

(define di-is-jcc::(-> DecodedInstruction bool)
  (lambda (di::DecodedInstruction)
    (= 0b1 (bv-extract 43 43 di))
  )
)

(define di-get-len::(-> DecodedInstruction Byte)
  (lambda (di::DecodedInstruction)
    (bv-extract 51 44 di)
  )
)

(define di-get-next::(-> DecodedInstruction Byte)
  (lambda (di::DecodedInstruction)
    (bv-extract 59 52 di)
  )
)

(define WhichReg::RegIdx)

(define Eip0::Byte)
(define Eip1::Byte)
(define Eip2::Byte)
(define Eip3::Byte)
(define Eip4::Byte)
(define Eip5::Byte)
(define Eip6::Byte)
(define Eip7::Byte)
(define Eip8::Byte)
(define Eip9::Byte)
(define EipA::Byte)
(define EipLoopBeg::Byte Eip1)
(define EipLoopEnd::Byte EipA)

(define mk-label-pred::(-> Byte Bit)
	(lambda (next::Byte)
	  (ite (or
	    (= next Eip0)
	    (= next Eip1)
	    (= next Eip2)
	    (= next Eip3)
	    (= next Eip4)
	    (= next Eip5)
	    (= next Eip6)
	    (= next Eip7)
	    (= next Eip8)
	    (= next Eip9)
	    (= next EipA)
	  ) 0b1 0b0)
	)
)

(define Len0::Byte)
(define Len1::Byte)
(define Len2::Byte)
(define Len3::Byte)
(define Len4::Byte)
(define Len5::Byte)
(define Len6::Byte)
(define Len7::Byte)
(define Len8::Byte)
(define Len9::Byte)

(define DIC0::DecodedInstruction)
(define DIC1::DecodedInstruction)
(define DIC2::DecodedInstruction)
(define DIC3::DecodedInstruction)
(define DIC4::DecodedInstruction)
(define DIC5::DecodedInstruction)
(define DIC6::DecodedInstruction)
(define DIC7::DecodedInstruction)
(define DIC8::DecodedInstruction)
(define DIC9::DecodedInstruction)

(define Ins0::Instruction)
(define Ins1::Instruction)
(define Ins2::Instruction)
(define Ins3::Instruction)
(define Ins4::Instruction)
(define Ins5::Instruction)
(define Ins6::Instruction)
(define Ins7::Instruction)
(define Ins8::Instruction)
(define Ins9::Instruction)

(define-type RegAndSCState             (bitvector 272))

(define-type SecondaryMachineState     (bitvector 296)) 
;  255    0: Reg32State
;  271  256: SCDoubleState
;  279  272: Byte [scinptr]
;  287  280: Byte [scoutptr]
;  295  288: Byte [nexteip]

(define sms-getregstate::(-> SecondaryMachineState Reg32State)
  (lambda (mstate::SecondaryMachineState)
    (bv-extract 255 0 mstate)
  )
)

(define sms-getscstate::(-> SecondaryMachineState SCDoubleState)
  (lambda (mstate::SecondaryMachineState)
    (bv-extract 271 256 mstate)
  )
)

(define sms-getregandscstate::(-> SecondaryMachineState RegAndSCState)
  (lambda (mstate::SecondaryMachineState)
    (bv-extract 271 0 mstate)
  )
)

(define sms-getscinptr::(-> SecondaryMachineState Byte)
  (lambda (mstate::SecondaryMachineState)
    (bv-extract 279 272 mstate)
  )
)

(define sms-getscoutptr::(-> SecondaryMachineState Byte)
  (lambda (mstate::SecondaryMachineState)
    (bv-extract 287 280 mstate)
  )
)

(define sms-getnexteip::(-> SecondaryMachineState Byte)
  (lambda (mstate::SecondaryMachineState)
    (bv-extract 295 288 mstate)
  )
)

(define sms-incscinptr::(-> SecondaryMachineState SecondaryMachineState)
  (lambda (mstate::SecondaryMachineState)
    (let ((scinptr (sms-getscinptr mstate)))
    (bv-concat (sms-getnexteip mstate) (sms-getscoutptr mstate) (bv-add scinptr 0x01) (sms-getregandscstate mstate))
    )
  )
)

(define sms-setnexteip::(-> SecondaryMachineState Byte SecondaryMachineState)
  (lambda (mstate::SecondaryMachineState nexteip::Byte)
    (bv-concat nexteip (sms-getscoutptr mstate) (sms-getscinptr mstate) (sms-getregandscstate mstate))
  )
)

; getreg32(reg,state). Return the value of register 'reg' from state 'state'.
(define sms-getreg32::(-> RegIdx SecondaryMachineState Dword)
  (lambda (x::RegIdx s::SecondaryMachineState)
    (let ((z (sms-getregstate s)))
    (ite (= x R0Idx) (bv-extract 31    0 z)
    (ite (= x R1Idx) (bv-extract 63   32 z)
    (ite (= x R2Idx) (bv-extract 95   64 z)
    (ite (= x R3Idx) (bv-extract 127  96 z)
    (ite (= x R4Idx) (bv-extract 159 128 z)
    (ite (= x R5Idx) (bv-extract 191 160 z)
    (ite (= x R6Idx) (bv-extract 223 192 z)
                     (bv-extract 255 224 z)
    ))))))))
  )
)

(define scdouble-getbyte-byidx::(-> SCDoubleState Byte Byte)
  (lambda (sc::SCDoubleState idx::Byte)
    (ite (= (bv-extract 0 0 idx) 0b0) (bv-extract 7 0 sc) (bv-extract 15 8 sc))
  )
)	

(define sms-getscbyte-byidx::(-> SecondaryMachineState Byte Byte)
  (lambda (mstate::SecondaryMachineState idx::Byte)
    (scdouble-getbyte-byidx (sms-getscstate mstate) idx)
  )
)


(define sms-getscbyte::(-> SecondaryMachineState Byte)
  (lambda (mstate::SecondaryMachineState)
    (let ((scptr (sms-getscinptr mstate)))
    (sms-getscbyte-byidx mstate scptr)
  ))
)

(define sms-putscbyte::(-> SecondaryMachineState Byte SecondaryMachineState)
  (lambda (mstate::SecondaryMachineState b::Byte)
    (let ((sc (sms-getscstate mstate)))
    (let ((scptr (sms-getscoutptr mstate)))
    (let ((newsc 
      (ite (= 0b0 (bv-extract 0 0 scptr)) 
        (bv-concat (bv-extract 15 8 sc) b)
        (bv-concat b (bv-extract 7 0 sc)))))
    (bv-concat (sms-getnexteip mstate) (bv-add scptr 0x01) (sms-getscinptr mstate) newsc (sms-getregstate mstate))
  ))))
)

; putreg32(reg,state,value). Update register 'reg' to value 'value' in state
; 'state'; return the new state.
(define sms-putreg32::(-> RegIdx Dword SecondaryMachineState SecondaryMachineState)
  (lambda (x::RegIdx y::Dword s::SecondaryMachineState)
    (let ((z (sms-getregstate s)))
    (bv-concat (sms-getnexteip s) (sms-getscoutptr s) (sms-getscinptr s) (sms-getscstate s)
    (ite (= x 0b000) (bv-concat (bv-extract 255  32 z) y)
    (ite (= x 0b001) (bv-concat (bv-extract 255  64 z) y (bv-extract 31  0 z))
    (ite (= x 0b010) (bv-concat (bv-extract 255  96 z) y (bv-extract 63  0 z))
    (ite (= x 0b011) (bv-concat (bv-extract 255 128 z) y (bv-extract 95  0 z))
    (ite (= x 0b100) (bv-concat (bv-extract 255 160 z) y (bv-extract 127 0 z))
    (ite (= x 0b101) (bv-concat (bv-extract 255 192 z) y (bv-extract 159 0 z))
    (ite (= x 0b110) (bv-concat (bv-extract 255 224 z) y (bv-extract 191 0 z))
                     (bv-concat y (bv-extract 223 0 z))
    )))))))))
  )
)

(define bytecode00::Byte) (define bytecode01::Byte)
(define bytecode02::Byte) (define bytecode03::Byte)
(define bytecode04::Byte) (define bytecode05::Byte)
(define bytecode06::Byte) (define bytecode07::Byte)
(define bytecode08::Byte) (define bytecode09::Byte)
(define bytecode0A::Byte) (define bytecode0B::Byte)
(define bytecode0C::Byte) (define bytecode0D::Byte)
(define bytecode0E::Byte) (define bytecode0F::Byte)
(define bytecode10::Byte) (define bytecode11::Byte)
(define bytecode12::Byte) (define bytecode13::Byte)
(define bytecode14::Byte) (define bytecode15::Byte)
(define bytecode16::Byte) (define bytecode17::Byte)
(define bytecode18::Byte) (define bytecode19::Byte)
(define bytecode1A::Byte) (define bytecode1B::Byte)
(define bytecode1C::Byte) (define bytecode1D::Byte)
(define bytecode1E::Byte) (define bytecode1F::Byte)
(define bytecode20::Byte) (define bytecode21::Byte)
(define bytecode22::Byte) (define bytecode23::Byte)
(define bytecode24::Byte) (define bytecode25::Byte)
(define bytecode26::Byte) (define bytecode27::Byte)
(define bytecode28::Byte) (define bytecode29::Byte)
(define bytecode2A::Byte) (define bytecode2B::Byte)
(define bytecode2C::Byte) (define bytecode2D::Byte)
(define bytecode2E::Byte) (define bytecode2F::Byte)
(define bytecode30::Byte) (define bytecode31::Byte)
(define bytecode32::Byte) (define bytecode33::Byte)
(define bytecode34::Byte) (define bytecode35::Byte)
(define bytecode36::Byte) (define bytecode37::Byte)
(define bytecode38::Byte) (define bytecode39::Byte)
(define bytecode3A::Byte) (define bytecode3B::Byte)
(define bytecode3C::Byte) (define bytecode3D::Byte)
(define bytecode3E::Byte) (define bytecode3F::Byte)
(define bytecode40::Byte) (define bytecode41::Byte)
(define bytecode42::Byte) (define bytecode43::Byte)
(define bytecode44::Byte) (define bytecode45::Byte)
(define bytecode46::Byte) (define bytecode47::Byte)
(define bytecode48::Byte) (define bytecode49::Byte)
(define bytecode4A::Byte) (define bytecode4B::Byte)
(define bytecode4C::Byte) (define bytecode4D::Byte)
(define bytecode4E::Byte) (define bytecode4F::Byte)
(define bytecode50::Byte) (define bytecode51::Byte)
(define bytecode52::Byte) (define bytecode53::Byte)
(define bytecode54::Byte) (define bytecode55::Byte)
(define bytecode56::Byte) (define bytecode57::Byte)
(define bytecode58::Byte) (define bytecode59::Byte)
(define bytecode5A::Byte) (define bytecode5B::Byte)
(define bytecode5C::Byte) (define bytecode5D::Byte)
(define bytecode5E::Byte) (define bytecode5F::Byte)
(define bytecode60::Byte) (define bytecode61::Byte)
(define bytecode62::Byte) (define bytecode63::Byte)
(define bytecode64::Byte) (define bytecode65::Byte)
(define bytecode66::Byte) (define bytecode67::Byte)
(define bytecode68::Byte) (define bytecode69::Byte)
(define bytecode6A::Byte) (define bytecode6B::Byte)
(define bytecode6C::Byte) (define bytecode6D::Byte)
(define bytecode6E::Byte) (define bytecode6F::Byte)
(define bytecode70::Byte) (define bytecode71::Byte)
(define bytecode72::Byte) (define bytecode73::Byte)
(define bytecode74::Byte) (define bytecode75::Byte)
(define bytecode76::Byte) (define bytecode77::Byte)
(define bytecode78::Byte) (define bytecode79::Byte)
(define bytecode7A::Byte) (define bytecode7B::Byte)
(define bytecode7C::Byte) (define bytecode7D::Byte)
(define bytecode7E::Byte) (define bytecode7F::Byte)
(define bytecode80::Byte) (define bytecode81::Byte)
(define bytecode82::Byte) (define bytecode83::Byte)
(define bytecode84::Byte) (define bytecode85::Byte)
(define bytecode86::Byte) (define bytecode87::Byte)
(define bytecode88::Byte) (define bytecode89::Byte)
(define bytecode8A::Byte) (define bytecode8B::Byte)
(define bytecode8C::Byte) (define bytecode8D::Byte)
(define bytecode8E::Byte) (define bytecode8F::Byte)
(define bytecode90::Byte) (define bytecode91::Byte)
(define bytecode92::Byte) (define bytecode93::Byte)
(define bytecode94::Byte) (define bytecode95::Byte)
(define bytecode96::Byte) (define bytecode97::Byte)
(define bytecode98::Byte) (define bytecode99::Byte)
(define bytecode9A::Byte) (define bytecode9B::Byte)
(define bytecode9C::Byte) (define bytecode9D::Byte)
(define bytecode9E::Byte) (define bytecode9F::Byte)
(define bytecodeA0::Byte) (define bytecodeA1::Byte)
(define bytecodeA2::Byte) (define bytecodeA3::Byte)
(define bytecodeA4::Byte) (define bytecodeA5::Byte)
(define bytecodeA6::Byte) (define bytecodeA7::Byte)
(define bytecodeA8::Byte) (define bytecodeA9::Byte)
(define bytecodeAA::Byte) (define bytecodeAB::Byte)
(define bytecodeAC::Byte) (define bytecodeAD::Byte)
(define bytecodeAE::Byte) (define bytecodeAF::Byte)
(define bytecodeB0::Byte) (define bytecodeB1::Byte)
(define bytecodeB2::Byte) (define bytecodeB3::Byte)
(define bytecodeB4::Byte) (define bytecodeB5::Byte)
(define bytecodeB6::Byte) (define bytecodeB7::Byte)
(define bytecodeB8::Byte) (define bytecodeB9::Byte)
(define bytecodeBA::Byte) (define bytecodeBB::Byte)
(define bytecodeBC::Byte) (define bytecodeBD::Byte)
(define bytecodeBE::Byte) (define bytecodeBF::Byte)
(define bytecodeC0::Byte) (define bytecodeC1::Byte)
(define bytecodeC2::Byte) (define bytecodeC3::Byte)
(define bytecodeC4::Byte) (define bytecodeC5::Byte)
(define bytecodeC6::Byte) (define bytecodeC7::Byte)
(define bytecodeC8::Byte) (define bytecodeC9::Byte)
(define bytecodeCA::Byte) (define bytecodeCB::Byte)
(define bytecodeCC::Byte) (define bytecodeCD::Byte)
(define bytecodeCE::Byte) (define bytecodeCF::Byte)
(define bytecodeD0::Byte) (define bytecodeD1::Byte)
(define bytecodeD2::Byte) (define bytecodeD3::Byte)
(define bytecodeD4::Byte) (define bytecodeD5::Byte)
(define bytecodeD6::Byte) (define bytecodeD7::Byte)
(define bytecodeD8::Byte) (define bytecodeD9::Byte)
(define bytecodeDA::Byte) (define bytecodeDB::Byte)
(define bytecodeDC::Byte) (define bytecodeDD::Byte)
(define bytecodeDE::Byte) (define bytecodeDF::Byte)
(define bytecodeE0::Byte) (define bytecodeE1::Byte)
(define bytecodeE2::Byte) (define bytecodeE3::Byte)
(define bytecodeE4::Byte) (define bytecodeE5::Byte)
(define bytecodeE6::Byte) (define bytecodeE7::Byte)
(define bytecodeE8::Byte) (define bytecodeE9::Byte)
(define bytecodeEA::Byte) (define bytecodeEB::Byte)
(define bytecodeEC::Byte) (define bytecodeED::Byte)
(define bytecodeEE::Byte) (define bytecodeEF::Byte)
(define bytecodeF0::Byte) (define bytecodeF1::Byte)
(define bytecodeF2::Byte) (define bytecodeF3::Byte)
(define bytecodeF4::Byte) (define bytecodeF5::Byte)
(define bytecodeF6::Byte) (define bytecodeF7::Byte)
(define bytecodeF8::Byte) (define bytecodeF9::Byte)
(define bytecodeFA::Byte) (define bytecodeFB::Byte)
(define bytecodeFC::Byte) (define bytecodeFD::Byte)
(define bytecodeFE::Byte) (define bytecodeFF::Byte)

; Used instead of an array lookup. Pass in byte XX, get back the bytecodeXX
; variable.
(define get-byte::(-> Byte Byte) 
	(lambda (x::Byte)
    (ite (= x 0x00) bytecode00
    (ite (= x 0x01) bytecode01
    (ite (= x 0x02) bytecode02
    (ite (= x 0x03) bytecode03
    (ite (= x 0x04) bytecode04
    (ite (= x 0x05) bytecode05
    (ite (= x 0x06) bytecode06
    (ite (= x 0x07) bytecode07
    (ite (= x 0x08) bytecode08
    (ite (= x 0x09) bytecode09
    (ite (= x 0x0A) bytecode0A
    (ite (= x 0x0B) bytecode0B
    (ite (= x 0x0C) bytecode0C
    (ite (= x 0x0D) bytecode0D
    (ite (= x 0x0E) bytecode0E
    (ite (= x 0x0F) bytecode0F
    (ite (= x 0x10) bytecode10
    (ite (= x 0x11) bytecode11
    (ite (= x 0x12) bytecode12
    (ite (= x 0x13) bytecode13
    (ite (= x 0x14) bytecode14
    (ite (= x 0x15) bytecode15
    (ite (= x 0x16) bytecode16
    (ite (= x 0x17) bytecode17
    (ite (= x 0x18) bytecode18
    (ite (= x 0x19) bytecode19
    (ite (= x 0x1A) bytecode1A
    (ite (= x 0x1B) bytecode1B
    (ite (= x 0x1C) bytecode1C
    (ite (= x 0x1D) bytecode1D
    (ite (= x 0x1E) bytecode1E
    (ite (= x 0x1F) bytecode1F
    (ite (= x 0x20) bytecode20
    (ite (= x 0x21) bytecode21
    (ite (= x 0x22) bytecode22
    (ite (= x 0x23) bytecode23
    (ite (= x 0x24) bytecode24
    (ite (= x 0x25) bytecode25
    (ite (= x 0x26) bytecode26
    (ite (= x 0x27) bytecode27
    (ite (= x 0x28) bytecode28
    (ite (= x 0x29) bytecode29
    (ite (= x 0x2A) bytecode2A
    (ite (= x 0x2B) bytecode2B
    (ite (= x 0x2C) bytecode2C
    (ite (= x 0x2D) bytecode2D
    (ite (= x 0x2E) bytecode2E
    (ite (= x 0x2F) bytecode2F
    (ite (= x 0x30) bytecode30
    (ite (= x 0x31) bytecode31
    (ite (= x 0x32) bytecode32
    (ite (= x 0x33) bytecode33
    (ite (= x 0x34) bytecode34
    (ite (= x 0x35) bytecode35
    (ite (= x 0x36) bytecode36
    (ite (= x 0x37) bytecode37
    (ite (= x 0x38) bytecode38
    (ite (= x 0x39) bytecode39
    (ite (= x 0x3A) bytecode3A
    (ite (= x 0x3B) bytecode3B
    (ite (= x 0x3C) bytecode3C
    (ite (= x 0x3D) bytecode3D
    (ite (= x 0x3E) bytecode3E
    (ite (= x 0x3F) bytecode3F
    (ite (= x 0x40) bytecode40
    (ite (= x 0x41) bytecode41
    (ite (= x 0x42) bytecode42
    (ite (= x 0x43) bytecode43
    (ite (= x 0x44) bytecode44
    (ite (= x 0x45) bytecode45
    (ite (= x 0x46) bytecode46
    (ite (= x 0x47) bytecode47
    (ite (= x 0x48) bytecode48
    (ite (= x 0x49) bytecode49
    (ite (= x 0x4A) bytecode4A
    (ite (= x 0x4B) bytecode4B
    (ite (= x 0x4C) bytecode4C
    (ite (= x 0x4D) bytecode4D
    (ite (= x 0x4E) bytecode4E
    (ite (= x 0x4F) bytecode4F
    (ite (= x 0x50) bytecode50
    (ite (= x 0x51) bytecode51
    (ite (= x 0x52) bytecode52
    (ite (= x 0x53) bytecode53
    (ite (= x 0x54) bytecode54
    (ite (= x 0x55) bytecode55
    (ite (= x 0x56) bytecode56
    (ite (= x 0x57) bytecode57
    (ite (= x 0x58) bytecode58
    (ite (= x 0x59) bytecode59
    (ite (= x 0x5A) bytecode5A
    (ite (= x 0x5B) bytecode5B
    (ite (= x 0x5C) bytecode5C
    (ite (= x 0x5D) bytecode5D
    (ite (= x 0x5E) bytecode5E
    (ite (= x 0x5F) bytecode5F
    (ite (= x 0x60) bytecode60
    (ite (= x 0x61) bytecode61
    (ite (= x 0x62) bytecode62
    (ite (= x 0x63) bytecode63
    (ite (= x 0x64) bytecode64
    (ite (= x 0x65) bytecode65
    (ite (= x 0x66) bytecode66
    (ite (= x 0x67) bytecode67
    (ite (= x 0x68) bytecode68
    (ite (= x 0x69) bytecode69
    (ite (= x 0x6A) bytecode6A
    (ite (= x 0x6B) bytecode6B
    (ite (= x 0x6C) bytecode6C
    (ite (= x 0x6D) bytecode6D
    (ite (= x 0x6E) bytecode6E
    (ite (= x 0x6F) bytecode6F
    (ite (= x 0x70) bytecode70
    (ite (= x 0x71) bytecode71
    (ite (= x 0x72) bytecode72
    (ite (= x 0x73) bytecode73
    (ite (= x 0x74) bytecode74
    (ite (= x 0x75) bytecode75
    (ite (= x 0x76) bytecode76
    (ite (= x 0x77) bytecode77
    (ite (= x 0x78) bytecode78
    (ite (= x 0x79) bytecode79
    (ite (= x 0x7A) bytecode7A
    (ite (= x 0x7B) bytecode7B
    (ite (= x 0x7C) bytecode7C
    (ite (= x 0x7D) bytecode7D
    (ite (= x 0x7E) bytecode7E
    (ite (= x 0x7F) bytecode7F
    (ite (= x 0x80) bytecode80
    (ite (= x 0x81) bytecode81
    (ite (= x 0x82) bytecode82
    (ite (= x 0x83) bytecode83
    (ite (= x 0x84) bytecode84
    (ite (= x 0x85) bytecode85
    (ite (= x 0x86) bytecode86
    (ite (= x 0x87) bytecode87
    (ite (= x 0x88) bytecode88
    (ite (= x 0x89) bytecode89
    (ite (= x 0x8A) bytecode8A
    (ite (= x 0x8B) bytecode8B
    (ite (= x 0x8C) bytecode8C
    (ite (= x 0x8D) bytecode8D
    (ite (= x 0x8E) bytecode8E
    (ite (= x 0x8F) bytecode8F
    (ite (= x 0x90) bytecode90
    (ite (= x 0x91) bytecode91
    (ite (= x 0x92) bytecode92
    (ite (= x 0x93) bytecode93
    (ite (= x 0x94) bytecode94
    (ite (= x 0x95) bytecode95
    (ite (= x 0x96) bytecode96
    (ite (= x 0x97) bytecode97
    (ite (= x 0x98) bytecode98
    (ite (= x 0x99) bytecode99
    (ite (= x 0x9A) bytecode9A
    (ite (= x 0x9B) bytecode9B
    (ite (= x 0x9C) bytecode9C
    (ite (= x 0x9D) bytecode9D
    (ite (= x 0x9E) bytecode9E
    (ite (= x 0x9F) bytecode9F
    (ite (= x 0xA0) bytecodeA0
    (ite (= x 0xA1) bytecodeA1
    (ite (= x 0xA2) bytecodeA2
    (ite (= x 0xA3) bytecodeA3
    (ite (= x 0xA4) bytecodeA4
    (ite (= x 0xA5) bytecodeA5
    (ite (= x 0xA6) bytecodeA6
    (ite (= x 0xA7) bytecodeA7
    (ite (= x 0xA8) bytecodeA8
    (ite (= x 0xA9) bytecodeA9
    (ite (= x 0xAA) bytecodeAA
    (ite (= x 0xAB) bytecodeAB
    (ite (= x 0xAC) bytecodeAC
    (ite (= x 0xAD) bytecodeAD
    (ite (= x 0xAE) bytecodeAE
    (ite (= x 0xAF) bytecodeAF
    (ite (= x 0xB0) bytecodeB0
    (ite (= x 0xB1) bytecodeB1
    (ite (= x 0xB2) bytecodeB2
    (ite (= x 0xB3) bytecodeB3
    (ite (= x 0xB4) bytecodeB4
    (ite (= x 0xB5) bytecodeB5
    (ite (= x 0xB6) bytecodeB6
    (ite (= x 0xB7) bytecodeB7
    (ite (= x 0xB8) bytecodeB8
    (ite (= x 0xB9) bytecodeB9
    (ite (= x 0xBA) bytecodeBA
    (ite (= x 0xBB) bytecodeBB
    (ite (= x 0xBC) bytecodeBC
    (ite (= x 0xBD) bytecodeBD
    (ite (= x 0xBE) bytecodeBE
    (ite (= x 0xBF) bytecodeBF
    (ite (= x 0xC0) bytecodeC0
    (ite (= x 0xC1) bytecodeC1
    (ite (= x 0xC2) bytecodeC2
    (ite (= x 0xC3) bytecodeC3
    (ite (= x 0xC4) bytecodeC4
    (ite (= x 0xC5) bytecodeC5
    (ite (= x 0xC6) bytecodeC6
    (ite (= x 0xC7) bytecodeC7
    (ite (= x 0xC8) bytecodeC8
    (ite (= x 0xC9) bytecodeC9
    (ite (= x 0xCA) bytecodeCA
    (ite (= x 0xCB) bytecodeCB
    (ite (= x 0xCC) bytecodeCC
    (ite (= x 0xCD) bytecodeCD
    (ite (= x 0xCE) bytecodeCE
    (ite (= x 0xCF) bytecodeCF
    (ite (= x 0xD0) bytecodeD0
    (ite (= x 0xD1) bytecodeD1
    (ite (= x 0xD2) bytecodeD2
    (ite (= x 0xD3) bytecodeD3
    (ite (= x 0xD4) bytecodeD4
    (ite (= x 0xD5) bytecodeD5
    (ite (= x 0xD6) bytecodeD6
    (ite (= x 0xD7) bytecodeD7
    (ite (= x 0xD8) bytecodeD8
    (ite (= x 0xD9) bytecodeD9
    (ite (= x 0xDA) bytecodeDA
    (ite (= x 0xDB) bytecodeDB
    (ite (= x 0xDC) bytecodeDC
    (ite (= x 0xDD) bytecodeDD
    (ite (= x 0xDE) bytecodeDE
    (ite (= x 0xDF) bytecodeDF
    (ite (= x 0xE0) bytecodeE0
    (ite (= x 0xE1) bytecodeE1
    (ite (= x 0xE2) bytecodeE2
    (ite (= x 0xE3) bytecodeE3
    (ite (= x 0xE4) bytecodeE4
    (ite (= x 0xE5) bytecodeE5
    (ite (= x 0xE6) bytecodeE6
    (ite (= x 0xE7) bytecodeE7
    (ite (= x 0xE8) bytecodeE8
    (ite (= x 0xE9) bytecodeE9
    (ite (= x 0xEA) bytecodeEA
    (ite (= x 0xEB) bytecodeEB
    (ite (= x 0xEC) bytecodeEC
    (ite (= x 0xED) bytecodeED
    (ite (= x 0xEE) bytecodeEE
    (ite (= x 0xEF) bytecodeEF
    (ite (= x 0xF0) bytecodeF0
    (ite (= x 0xF1) bytecodeF1
    (ite (= x 0xF2) bytecodeF2
    (ite (= x 0xF3) bytecodeF3
    (ite (= x 0xF4) bytecodeF4
    (ite (= x 0xF5) bytecodeF5
    (ite (= x 0xF6) bytecodeF6
    (ite (= x 0xF7) bytecodeF7
    (ite (= x 0xF8) bytecodeF8
    (ite (= x 0xF9) bytecodeF9
    (ite (= x 0xFA) bytecodeFA
    (ite (= x 0xFB) bytecodeFB
    (ite (= x 0xFC) bytecodeFC
    (ite (= x 0xFD) bytecodeFD
    (ite (= x 0xFE) bytecodeFE
    (ite (= x 0xFF) bytecodeFF
    bytecode04))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  )
)



(define shellcode00::Byte) (define shellcode01::Byte)
(define shellcode02::Byte) (define shellcode03::Byte)
(define shellcode04::Byte) (define shellcode05::Byte)
(define shellcode06::Byte) (define shellcode07::Byte)
(define shellcode08::Byte) (define shellcode09::Byte)
(define shellcode0A::Byte) (define shellcode0B::Byte)
(define shellcode0C::Byte) (define shellcode0D::Byte)
(define shellcode0E::Byte) (define shellcode0F::Byte)
(define shellcode10::Byte) (define shellcode11::Byte)
(define shellcode12::Byte) (define shellcode13::Byte)
(define shellcode14::Byte) (define shellcode15::Byte)
(define shellcode16::Byte) (define shellcode17::Byte)
(define shellcode18::Byte) (define shellcode19::Byte)
(define shellcode1A::Byte) (define shellcode1B::Byte)
(define shellcode1C::Byte) (define shellcode1D::Byte)
(define shellcode1E::Byte) (define shellcode1F::Byte)
(define shellcode20::Byte) (define shellcode21::Byte)
(define shellcode22::Byte) (define shellcode23::Byte)
(define shellcode24::Byte) (define shellcode25::Byte)
(define shellcode26::Byte) (define shellcode27::Byte)
(define shellcode28::Byte) (define shellcode29::Byte)
(define shellcode2A::Byte) (define shellcode2B::Byte)
(define shellcode2C::Byte) (define shellcode2D::Byte)
(define shellcode2E::Byte) (define shellcode2F::Byte)
(define shellcode30::Byte) (define shellcode31::Byte)
(define shellcode32::Byte) (define shellcode33::Byte)
(define shellcode34::Byte) (define shellcode35::Byte)
(define shellcode36::Byte) (define shellcode37::Byte)
(define shellcode38::Byte) (define shellcode39::Byte)
(define shellcode3A::Byte) (define shellcode3B::Byte)
(define shellcode3C::Byte) (define shellcode3D::Byte)
(define shellcode3E::Byte) (define shellcode3F::Byte)
(define shellcode40::Byte) (define shellcode41::Byte)
(define shellcode42::Byte) (define shellcode43::Byte)
(define shellcode44::Byte) (define shellcode45::Byte)
(define shellcode46::Byte) (define shellcode47::Byte)
(define shellcode48::Byte) (define shellcode49::Byte)
(define shellcode4A::Byte) (define shellcode4B::Byte)
(define shellcode4C::Byte) (define shellcode4D::Byte)
(define shellcode4E::Byte) (define shellcode4F::Byte)
(define shellcode50::Byte) (define shellcode51::Byte)
(define shellcode52::Byte) (define shellcode53::Byte)
(define shellcode54::Byte) (define shellcode55::Byte)
(define shellcode56::Byte) (define shellcode57::Byte)
(define shellcode58::Byte) (define shellcode59::Byte)
(define shellcode5A::Byte) (define shellcode5B::Byte)
(define shellcode5C::Byte) (define shellcode5D::Byte)
(define shellcode5E::Byte) (define shellcode5F::Byte)
(define shellcode60::Byte) (define shellcode61::Byte)
(define shellcode62::Byte) (define shellcode63::Byte)
(define shellcode64::Byte) (define shellcode65::Byte)
(define shellcode66::Byte) (define shellcode67::Byte)
(define shellcode68::Byte) (define shellcode69::Byte)
(define shellcode6A::Byte) (define shellcode6B::Byte)
(define shellcode6C::Byte) (define shellcode6D::Byte)
(define shellcode6E::Byte) (define shellcode6F::Byte)
(define shellcode70::Byte) (define shellcode71::Byte)
(define shellcode72::Byte) (define shellcode73::Byte)
(define shellcode74::Byte) (define shellcode75::Byte)
(define shellcode76::Byte) (define shellcode77::Byte)
(define shellcode78::Byte) (define shellcode79::Byte)
(define shellcode7A::Byte) (define shellcode7B::Byte)
(define shellcode7C::Byte) (define shellcode7D::Byte)
(define shellcode7E::Byte) (define shellcode7F::Byte)

;(define initialsc::SCDoubleState (bv-concat shellcode7F shellcode7E shellcode7D shellcode7C shellcode7B shellcode7A shellcode79 shellcode78 shellcode77 shellcode76 shellcode75 shellcode74 shellcode73 shellcode72 shellcode71 shellcode70 shellcode6F shellcode6E shellcode6D shellcode6C shellcode6B shellcode6A shellcode69 shellcode68 shellcode67 shellcode66 shellcode65 shellcode64 shellcode63 shellcode62 shellcode61 shellcode60 shellcode5F shellcode5E shellcode5D shellcode5C shellcode5B shellcode5A shellcode59 shellcode58 shellcode57 shellcode56 shellcode55 shellcode54 shellcode53 shellcode52 shellcode51 shellcode50 shellcode4F shellcode4E shellcode4D shellcode4C shellcode4B shellcode4A shellcode49 shellcode48 shellcode47 shellcode46 shellcode45 shellcode44 shellcode43 shellcode42 shellcode41 shellcode40 shellcode3F shellcode3E shellcode3D shellcode3C shellcode3B shellcode3A shellcode39 shellcode38 shellcode37 shellcode36 shellcode35 shellcode34 shellcode33 shellcode32 shellcode31 shellcode30 shellcode2F shellcode2E shellcode2D shellcode2C shellcode2B shellcode2A shellcode29 shellcode28 shellcode27 shellcode26 shellcode25 shellcode24 shellcode23 shellcode22 shellcode21 shellcode20 shellcode1F shellcode1E shellcode1D shellcode1C shellcode1B shellcode1A shellcode19 shellcode18 shellcode17 shellcode16 shellcode15 shellcode14 shellcode13 shellcode12 shellcode11 shellcode10 shellcode0F shellcode0E shellcode0D shellcode0C shellcode0B shellcode0A shellcode09 shellcode08 shellcode07 shellcode06 shellcode05 shellcode04 shellcode03 shellcode02 shellcode01 shellcode00))

(define realscbyte00::Byte 0xA0)
(define realscbyte01::Byte 0x8C)
(define realscbyte02::Byte 0x1C)
(define realscbyte03::Byte 0x29)
(define realscbyte04::Byte 0xA1)
(define realscbyte05::Byte 0xCC)
(define realscbyte06::Byte 0x38)
(define realscbyte07::Byte 0xFD)
(define realscbyte08::Byte 0x8D)
(define realscbyte09::Byte 0xF4)
(define realscbyte0A::Byte 0x8E)
(define realscbyte0B::Byte 0x59)
(define realscbyte0C::Byte 0x86)
(define realscbyte0D::Byte 0xB7)
(define realscbyte0E::Byte 0xCA)
(define realscbyte0F::Byte 0xFF)
(define realscbyte10::Byte 0x33)
(define realscbyte11::Byte 0x29)
(define realscbyte12::Byte 0xD6)
(define realscbyte13::Byte 0xE3)
(define realscbyte14::Byte 0x6F)
(define realscbyte15::Byte 0x4B)
(define realscbyte16::Byte 0x19)
(define realscbyte17::Byte 0x71)
(define realscbyte18::Byte 0x5C)
(define realscbyte19::Byte 0xBB)
(define realscbyte1A::Byte 0x4E)
(define realscbyte1B::Byte 0x90)
(define realscbyte1C::Byte 0xC3)
(define realscbyte1D::Byte 0xF7)
(define realscbyte1E::Byte 0x41)
(define realscbyte1F::Byte 0x9E)
(define realscbyte20::Byte 0xA2)
(define realscbyte21::Byte 0x1C)
(define realscbyte22::Byte 0x22)
(define realscbyte23::Byte 0xBF)
(define realscbyte24::Byte 0x25)
(define realscbyte25::Byte 0x0F)
(define realscbyte26::Byte 0xFE)
(define realscbyte27::Byte 0xA6)
(define realscbyte28::Byte 0x81)
(define realscbyte29::Byte 0x10)
(define realscbyte2A::Byte 0x43)
(define realscbyte2B::Byte 0x38)
(define realscbyte2C::Byte 0x92)
(define realscbyte2D::Byte 0x95)
(define realscbyte2E::Byte 0x21)
(define realscbyte2F::Byte 0x2B)
(define realscbyte30::Byte 0xE3)
(define realscbyte31::Byte 0xA6)
(define realscbyte32::Byte 0xE9)
(define realscbyte33::Byte 0xAC)
(define realscbyte34::Byte 0x08)
(define realscbyte35::Byte 0x4D)
(define realscbyte36::Byte 0xBA)
(define realscbyte37::Byte 0x08)
(define realscbyte38::Byte 0x0B)
(define realscbyte39::Byte 0xAB)
(define realscbyte3A::Byte 0x22)
(define realscbyte3B::Byte 0x84)
(define realscbyte3C::Byte 0x6B)
(define realscbyte3D::Byte 0x1F)
(define realscbyte3E::Byte 0xAD)
(define realscbyte3F::Byte 0x05)
	
;(define realsc::SCState (bv-concat realscbyte3F realscbyte3E realscbyte3D realscbyte3C realscbyte3B realscbyte3A realscbyte39 realscbyte38 realscbyte37 realscbyte36 realscbyte35 realscbyte34 realscbyte33 realscbyte32 realscbyte31 realscbyte30 realscbyte2F realscbyte2E realscbyte2D realscbyte2C realscbyte2B realscbyte2A realscbyte29 realscbyte28 realscbyte27 realscbyte26 realscbyte25 realscbyte24 realscbyte23 realscbyte22 realscbyte21 realscbyte20 realscbyte1F realscbyte1E realscbyte1D realscbyte1C realscbyte1B realscbyte1A realscbyte19 realscbyte18 realscbyte17 realscbyte16 realscbyte15 realscbyte14 realscbyte13 realscbyte12 realscbyte11 realscbyte10 realscbyte0F realscbyte0E realscbyte0D realscbyte0C realscbyte0B realscbyte0A realscbyte09 realscbyte08 realscbyte07 realscbyte06 realscbyte05 realscbyte04 realscbyte03 realscbyte02 realscbyte01 realscbyte00))

(define getrealscbyte::(-> Byte Byte)
  (lambda (idx::Byte)
      (ite (= idx 0x00) realscbyte00
      (ite (= idx 0x01) realscbyte01
      (ite (= idx 0x02) realscbyte02
      (ite (= idx 0x03) realscbyte03
      (ite (= idx 0x04) realscbyte04
      (ite (= idx 0x05) realscbyte05
      (ite (= idx 0x06) realscbyte06
      (ite (= idx 0x07) realscbyte07
      (ite (= idx 0x08) realscbyte08
      (ite (= idx 0x09) realscbyte09
      (ite (= idx 0x0A) realscbyte0A
      (ite (= idx 0x0B) realscbyte0B
      (ite (= idx 0x0C) realscbyte0C
      (ite (= idx 0x0D) realscbyte0D
      (ite (= idx 0x0E) realscbyte0E
      (ite (= idx 0x0F) realscbyte0F
      (ite (= idx 0x10) realscbyte10
      (ite (= idx 0x11) realscbyte11
      (ite (= idx 0x12) realscbyte12
      (ite (= idx 0x13) realscbyte13
      (ite (= idx 0x14) realscbyte14
      (ite (= idx 0x15) realscbyte15
      (ite (= idx 0x16) realscbyte16
      (ite (= idx 0x17) realscbyte17
      (ite (= idx 0x18) realscbyte18
      (ite (= idx 0x19) realscbyte19
      (ite (= idx 0x1A) realscbyte1A
      (ite (= idx 0x1B) realscbyte1B
      (ite (= idx 0x1C) realscbyte1C
      (ite (= idx 0x1D) realscbyte1D
      (ite (= idx 0x1E) realscbyte1E
      (ite (= idx 0x1F) realscbyte1F
      (ite (= idx 0x20) realscbyte20
      (ite (= idx 0x21) realscbyte21
      (ite (= idx 0x22) realscbyte22
      (ite (= idx 0x23) realscbyte23
      (ite (= idx 0x24) realscbyte24
      (ite (= idx 0x25) realscbyte25
      (ite (= idx 0x26) realscbyte26
      (ite (= idx 0x27) realscbyte27
      (ite (= idx 0x28) realscbyte28
      (ite (= idx 0x29) realscbyte29
      (ite (= idx 0x2A) realscbyte2A
      (ite (= idx 0x2B) realscbyte2B
      (ite (= idx 0x2C) realscbyte2C
      (ite (= idx 0x2D) realscbyte2D
      (ite (= idx 0x2E) realscbyte2E
      (ite (= idx 0x2F) realscbyte2F
      (ite (= idx 0x30) realscbyte30
      (ite (= idx 0x31) realscbyte31
      (ite (= idx 0x32) realscbyte32
      (ite (= idx 0x33) realscbyte33
      (ite (= idx 0x34) realscbyte34
      (ite (= idx 0x35) realscbyte35
      (ite (= idx 0x36) realscbyte36
      (ite (= idx 0x37) realscbyte37
      (ite (= idx 0x38) realscbyte38
      (ite (= idx 0x39) realscbyte39
      (ite (= idx 0x3A) realscbyte3A
      (ite (= idx 0x3B) realscbyte3B
      (ite (= idx 0x3C) realscbyte3C
      (ite (= idx 0x3D) realscbyte3D
      (ite (= idx 0x3E) realscbyte3E
                        realscbyte3F  
      ))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  ))
)

; Used instead of an array lookup. Pass in byte XX, get back the bytecodeXX
; variable.
(define getencscbyte::(-> Byte Byte) 
	(lambda (x::Byte)
    (ite (= x 0x00) shellcode00
    (ite (= x 0x01) shellcode01
    (ite (= x 0x02) shellcode02
    (ite (= x 0x03) shellcode03
    (ite (= x 0x04) shellcode04
    (ite (= x 0x05) shellcode05
    (ite (= x 0x06) shellcode06
    (ite (= x 0x07) shellcode07
    (ite (= x 0x08) shellcode08
    (ite (= x 0x09) shellcode09
    (ite (= x 0x0A) shellcode0A
    (ite (= x 0x0B) shellcode0B
    (ite (= x 0x0C) shellcode0C
    (ite (= x 0x0D) shellcode0D
    (ite (= x 0x0E) shellcode0E
    (ite (= x 0x0F) shellcode0F
    (ite (= x 0x10) shellcode10
    (ite (= x 0x11) shellcode11
    (ite (= x 0x12) shellcode12
    (ite (= x 0x13) shellcode13
    (ite (= x 0x14) shellcode14
    (ite (= x 0x15) shellcode15
    (ite (= x 0x16) shellcode16
    (ite (= x 0x17) shellcode17
    (ite (= x 0x18) shellcode18
    (ite (= x 0x19) shellcode19
    (ite (= x 0x1A) shellcode1A
    (ite (= x 0x1B) shellcode1B
    (ite (= x 0x1C) shellcode1C
    (ite (= x 0x1D) shellcode1D
    (ite (= x 0x1E) shellcode1E
    (ite (= x 0x1F) shellcode1F
    (ite (= x 0x20) shellcode20
    (ite (= x 0x21) shellcode21
    (ite (= x 0x22) shellcode22
    (ite (= x 0x23) shellcode23
    (ite (= x 0x24) shellcode24
    (ite (= x 0x25) shellcode25
    (ite (= x 0x26) shellcode26
    (ite (= x 0x27) shellcode27
    (ite (= x 0x28) shellcode28
    (ite (= x 0x29) shellcode29
    (ite (= x 0x2A) shellcode2A
    (ite (= x 0x2B) shellcode2B
    (ite (= x 0x2C) shellcode2C
    (ite (= x 0x2D) shellcode2D
    (ite (= x 0x2E) shellcode2E
    (ite (= x 0x2F) shellcode2F
    (ite (= x 0x30) shellcode30
    (ite (= x 0x31) shellcode31
    (ite (= x 0x32) shellcode32
    (ite (= x 0x33) shellcode33
    (ite (= x 0x34) shellcode34
    (ite (= x 0x35) shellcode35
    (ite (= x 0x36) shellcode36
    (ite (= x 0x37) shellcode37
    (ite (= x 0x38) shellcode38
    (ite (= x 0x39) shellcode39
    (ite (= x 0x3A) shellcode3A
    (ite (= x 0x3B) shellcode3B
    (ite (= x 0x3C) shellcode3C
    (ite (= x 0x3D) shellcode3D
    (ite (= x 0x3E) shellcode3E
    (ite (= x 0x3F) shellcode3F
    (ite (= x 0x40) shellcode40
    (ite (= x 0x41) shellcode41
    (ite (= x 0x42) shellcode42
    (ite (= x 0x43) shellcode43
    (ite (= x 0x44) shellcode44
    (ite (= x 0x45) shellcode45
    (ite (= x 0x46) shellcode46
    (ite (= x 0x47) shellcode47
    (ite (= x 0x48) shellcode48
    (ite (= x 0x49) shellcode49
    (ite (= x 0x4A) shellcode4A
    (ite (= x 0x4B) shellcode4B
    (ite (= x 0x4C) shellcode4C
    (ite (= x 0x4D) shellcode4D
    (ite (= x 0x4E) shellcode4E
    (ite (= x 0x4F) shellcode4F
    (ite (= x 0x50) shellcode50
    (ite (= x 0x51) shellcode51
    (ite (= x 0x52) shellcode52
    (ite (= x 0x53) shellcode53
    (ite (= x 0x54) shellcode54
    (ite (= x 0x55) shellcode55
    (ite (= x 0x56) shellcode56
    (ite (= x 0x57) shellcode57
    (ite (= x 0x58) shellcode58
    (ite (= x 0x59) shellcode59
    (ite (= x 0x5A) shellcode5A
    (ite (= x 0x5B) shellcode5B
    (ite (= x 0x5C) shellcode5C
    (ite (= x 0x5D) shellcode5D
    (ite (= x 0x5E) shellcode5E
    (ite (= x 0x5F) shellcode5F
    (ite (= x 0x60) shellcode60
    (ite (= x 0x61) shellcode61
    (ite (= x 0x62) shellcode62
    (ite (= x 0x63) shellcode63
    (ite (= x 0x64) shellcode64
    (ite (= x 0x65) shellcode65
    (ite (= x 0x66) shellcode66
    (ite (= x 0x67) shellcode67
    (ite (= x 0x68) shellcode68
    (ite (= x 0x69) shellcode69
    (ite (= x 0x6A) shellcode6A
    (ite (= x 0x6B) shellcode6B
    (ite (= x 0x6C) shellcode6C
    (ite (= x 0x6D) shellcode6D
    (ite (= x 0x6E) shellcode6E
    (ite (= x 0x6F) shellcode6F
    (ite (= x 0x70) shellcode70
    (ite (= x 0x71) shellcode71
    (ite (= x 0x72) shellcode72
    (ite (= x 0x73) shellcode73
    (ite (= x 0x74) shellcode74
    (ite (= x 0x75) shellcode75
    (ite (= x 0x76) shellcode76
    (ite (= x 0x77) shellcode77
    (ite (= x 0x78) shellcode78
    (ite (= x 0x79) shellcode79
    (ite (= x 0x7A) shellcode7A
    (ite (= x 0x7B) shellcode7B
    (ite (= x 0x7C) shellcode7C
    (ite (= x 0x7D) shellcode7D
    (ite (= x 0x7E) shellcode7E
                    shellcode7F
    )))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
  )
)

(define finalize-normal-decode::(-> Byte Mnem RegIdx RegIdx Dword Byte DecodedInstruction)
	(lambda (eip::Byte mnem::Mnem lhs::RegIdx rhs::RegIdx imm32::Dword length::Byte)
		(bv-concat (bv-add eip length) length 0b0 0b1 imm32 rhs lhs mnem)
	)
)

(define finalize-conditional-jump::(-> Byte Mnem RegIdx Byte DecodedInstruction)
	(lambda (nexteip::Byte mnem::Mnem lhs::RegIdx length::Byte)
		(bv-concat nexteip length 0b1 (mk-label-pred nexteip) 0x00000000 0b000 lhs mnem)
	)
)

(define decode-insn::(-> (-> Byte Byte) Byte DecodedInstruction)
	(lambda (f-get-byte::(-> Byte Byte) eip::Byte)
    (let ((byte0 (f-get-byte eip)))
    (let ((byte1 (f-get-byte (bv-add 0x01 eip))))
    (let ((byte2 (f-get-byte (bv-add 0x02 eip))))
    (let ((byte3 (f-get-byte (bv-add 0x03 eip))))
    (let ((byte4 (f-get-byte (bv-add 0x04 eip))))
    (let ((eip-plus-one (bv-add eip 0x01)))
    (let ((eip-plus-two (bv-add eip 0x02)))
    (let ((eip-plus-five (bv-add eip 0x05)))
    (let ((lhsreg0 (bv-extract 5 3 byte0)))
    (let ((rhsreg0 (bv-extract 2 0 byte0)))
    ; xor reg, reg
    (ite (= (bv-and byte0 0xC0) 0x00)
      (finalize-normal-decode eip XorRegReg lhsreg0 rhsreg0 0x00000000 0x01)
    ; add reg, reg
    (ite (= (bv-and byte0 0xC0) 0x40)
      (finalize-normal-decode eip AddRegReg lhsreg0 rhsreg0 0x00000000 0x01)
    ; mov reg, reg
    (ite (= (bv-and byte0 0xC0) 0x80)
      (finalize-normal-decode eip MovRegReg lhsreg0 rhsreg0 0x00000000 0x01)
    ; complex 0xC0 case
      ; CHANGED: getscbyte rX
      (let ((opcode  (bv-extract 5 3 byte0)))
      (let ((lhsreg  rhsreg0))
      (let ((rhsval0 (bv-concat byte4 byte3 byte2 byte1)))
      (ite (= opcode 0b000)
        (finalize-normal-decode  eip GetscbyteReg lhsreg 0b000 0x00000000 0x01)
      ; CHANGED: putscbyte rX
      (ite (= opcode 0b001)
        (finalize-normal-decode  eip PutscbyteReg lhsreg 0b000 0x00000000 0x01)
      ; neg reg
      (ite (= opcode 0b010)
        (finalize-normal-decode  eip NegReg lhsreg 0b000 0x00000000 0x01)
      ; not reg
      (ite (= opcode 0b011)
        (finalize-normal-decode  eip NotReg lhsreg 0b000 0x00000000 0x01)
      (let ((rhsval0 (bv-concat byte4 byte3 byte2 byte1)))
      ; add reg, imm32
      (ite (= opcode 0b100)
        (finalize-normal-decode  eip AddRegImm lhsreg 0b000 rhsval0 0x05)
      ; xor reg, imm32
      (ite (= opcode 0b101)
        (finalize-normal-decode  eip XorRegImm lhsreg 0b000 rhsval0 0x05)
      ; CHANGED: mov reg, imm32
      (ite (= opcode 0b110)
        (finalize-normal-decode  eip MovRegImm lhsreg 0b000 rhsval0 0x05)
      ; opcode == 0b111
      ; CHANGED: jnz rel
        (let ((dest (bv-add eip-plus-two byte1)))
        (finalize-conditional-jump dest JnzRegImm lhsreg 0x02)
        )))))))))))))))
    ))))))))))
  )
) 

(define simulate-insn::(-> Instruction Byte Byte SecondaryMachineState SecondaryMachineState)
	(lambda (insn::Instruction nexteip::Byte desteip::Byte sms::SecondaryMachineState)
		(let ((mnem   (bv-extract  3  0 insn)))
		(let ((lhsreg (bv-extract  6  4 insn)))
		(let ((rhsreg (bv-extract  9  7 insn)))
		(let ((imm32  (bv-extract 41 10 insn)))
		(let ((regstate (sms-getregstate sms)))
		(let ((scstate  (sms-getscstate  sms)))
		(let ((scinptr  (sms-getscinptr  sms)))
		(let ((scoutptr (sms-getscoutptr sms)))
		(ite (= mnem XorRegReg   )
      (sms-putreg32 lhsreg (bv-xor (sms-getreg32 lhsreg sms) (sms-getreg32 rhsreg sms)) sms)
		(ite (= mnem AddRegReg   )
      (sms-putreg32 lhsreg (bv-add (sms-getreg32 lhsreg sms) (sms-getreg32 rhsreg sms)) sms)
		(ite (= mnem MovRegReg   )
      (sms-putreg32 lhsreg (sms-getreg32 rhsreg sms) sms)
		(ite (= mnem GetscbyteReg)
      (sms-incscinptr (sms-putreg32 lhsreg (bv-zero-extend (sms-getscbyte sms) 24) sms))
		(ite (= mnem PutscbyteReg)
      (sms-putscbyte sms (bv-extract 7 0 (sms-getreg32 lhsreg sms)))
		(ite (= mnem NegReg      )
      (sms-putreg32 lhsreg (bv-neg (sms-getreg32 rhsreg sms)) sms)
		(ite (= mnem NotReg      )
      (sms-putreg32 lhsreg (bv-not (sms-getreg32 rhsreg sms)) sms)
		(ite (= mnem AddRegImm   )
      (sms-putreg32 lhsreg (bv-add (sms-getreg32 lhsreg sms) imm32) sms)
		(ite (= mnem XorRegImm   )
      (sms-putreg32 lhsreg (bv-xor (sms-getreg32 lhsreg sms) imm32) sms)
		(ite (= mnem MovRegImm   )
      (sms-putreg32 lhsreg imm32 sms)
		; JnzRegImm
		(sms-setnexteip sms (ite (= (sms-getreg32 lhsreg sms) 0x00000000) nexteip desteip))
		))))))))))))))))))
  )
)

; Decode program
(assert
  (and
    (= Eip0 0x00)
    (= DIC0 (decode-insn get-byte Eip0))
    (= Len0 (di-get-len  DIC0))
    (= Ins0 (di-get-insn DIC0))

    (= Eip1 (bv-add Eip0 Len0))
    (= DIC1 (decode-insn get-byte Eip1))
    (= Len1 (di-get-len  DIC1))
    (= Ins1 (di-get-insn DIC1))

    (= Eip2 (bv-add Eip1 Len1))
    (= DIC2 (decode-insn get-byte Eip2))
    (= Len2 (di-get-len  DIC2))
    (= Ins2 (di-get-insn DIC2))

    (= Eip3 (bv-add Eip2 Len2))
    (= DIC3 (decode-insn get-byte Eip3))
    (= Len3 (di-get-len  DIC3))
    (= Ins3 (di-get-insn DIC3))

    (= Eip4 (bv-add Eip3 Len3))
    (= DIC4 (decode-insn get-byte Eip4))
    (= Len4 (di-get-len  DIC4))
    (= Ins4 (di-get-insn DIC4))

    (= Eip5 (bv-add Eip4 Len4))
    (= DIC5 (decode-insn get-byte Eip5))
    (= Len5 (di-get-len  DIC5))
    (= Ins5 (di-get-insn DIC5))

    (= Eip6 (bv-add Eip5 Len5))
    (= DIC6 (decode-insn get-byte Eip6))
    (= Len6 (di-get-len  DIC6))
    (= Ins6 (di-get-insn DIC6))

    (= Eip7 (bv-add Eip6 Len6))
    (= DIC7 (decode-insn get-byte Eip7))
    (= Len7 (di-get-len  DIC7))
    (= Ins7 (di-get-insn DIC7))

    (= Eip8 (bv-add Eip7 Len7))
    (= DIC8 (decode-insn get-byte Eip8))
    (= Len8 (di-get-len  DIC8))
    (= Ins8 (di-get-insn DIC8))

    (= Eip9 (bv-add Eip8 Len8))
    (= DIC9 (decode-insn get-byte Eip9))
    (= Len9 (di-get-len  DIC9))
    (= Ins9 (di-get-insn DIC9))

    (= EipA (bv-add Eip9 Len9))
    
    (di-get-extra DIC0)
    (di-get-extra DIC1)
    (di-get-extra DIC2)
    (di-get-extra DIC3)
    (di-get-extra DIC4)
    (di-get-extra DIC5)
    (di-get-extra DIC6)
    (di-get-extra DIC7)
    (di-get-extra DIC8)
    (di-get-extra DIC9)
  )
)

; Program shape: last instruction is Jnz to Eip1
(assert
  (and 
    (not (di-is-jcc DIC0))
    (not (di-is-jcc DIC1))
    (not (di-is-jcc DIC2))
    (not (di-is-jcc DIC3))
    (not (di-is-jcc DIC4))
    (not (di-is-jcc DIC5))
    (not (di-is-jcc DIC6))
    (not (di-is-jcc DIC7))
    (not (di-is-jcc DIC8))
    (and (di-is-jcc DIC9) (= EipLoopBeg (di-get-next DIC9)))
  )
)
 
(assert
  (and
    (and (bv-le 0x20 shellcode00) (bv-le shellcode00 0x7F)) 
    (and (bv-le 0x20 shellcode01) (bv-le shellcode01 0x7F)) 
    (and (bv-le 0x20 shellcode02) (bv-le shellcode02 0x7F)) 
    (and (bv-le 0x20 shellcode03) (bv-le shellcode03 0x7F)) 
    (and (bv-le 0x20 shellcode04) (bv-le shellcode04 0x7F)) 
    (and (bv-le 0x20 shellcode05) (bv-le shellcode05 0x7F)) 
    (and (bv-le 0x20 shellcode06) (bv-le shellcode06 0x7F)) 
    (and (bv-le 0x20 shellcode07) (bv-le shellcode07 0x7F)) 
    (and (bv-le 0x20 shellcode08) (bv-le shellcode08 0x7F)) 
    (and (bv-le 0x20 shellcode09) (bv-le shellcode09 0x7F)) 
    (and (bv-le 0x20 shellcode0A) (bv-le shellcode0A 0x7F)) 
    (and (bv-le 0x20 shellcode0B) (bv-le shellcode0B 0x7F)) 
    (and (bv-le 0x20 shellcode0C) (bv-le shellcode0C 0x7F)) 
    (and (bv-le 0x20 shellcode0D) (bv-le shellcode0D 0x7F)) 
    (and (bv-le 0x20 shellcode0E) (bv-le shellcode0E 0x7F)) 
    (and (bv-le 0x20 shellcode0F) (bv-le shellcode0F 0x7F)) 
    (and (bv-le 0x20 shellcode10) (bv-le shellcode10 0x7F)) 
    (and (bv-le 0x20 shellcode11) (bv-le shellcode11 0x7F)) 
    (and (bv-le 0x20 shellcode12) (bv-le shellcode12 0x7F)) 
    (and (bv-le 0x20 shellcode13) (bv-le shellcode13 0x7F)) 
    (and (bv-le 0x20 shellcode14) (bv-le shellcode14 0x7F)) 
    (and (bv-le 0x20 shellcode15) (bv-le shellcode15 0x7F)) 
    (and (bv-le 0x20 shellcode16) (bv-le shellcode16 0x7F)) 
    (and (bv-le 0x20 shellcode17) (bv-le shellcode17 0x7F)) 
    (and (bv-le 0x20 shellcode18) (bv-le shellcode18 0x7F)) 
    (and (bv-le 0x20 shellcode19) (bv-le shellcode19 0x7F)) 
    (and (bv-le 0x20 shellcode1A) (bv-le shellcode1A 0x7F)) 
    (and (bv-le 0x20 shellcode1B) (bv-le shellcode1B 0x7F)) 
    (and (bv-le 0x20 shellcode1C) (bv-le shellcode1C 0x7F)) 
    (and (bv-le 0x20 shellcode1D) (bv-le shellcode1D 0x7F)) 
    (and (bv-le 0x20 shellcode1E) (bv-le shellcode1E 0x7F)) 
    (and (bv-le 0x20 shellcode1F) (bv-le shellcode1F 0x7F)) 
    (and (bv-le 0x20 shellcode20) (bv-le shellcode20 0x7F)) 
    (and (bv-le 0x20 shellcode21) (bv-le shellcode21 0x7F)) 
    (and (bv-le 0x20 shellcode22) (bv-le shellcode22 0x7F)) 
    (and (bv-le 0x20 shellcode23) (bv-le shellcode23 0x7F)) 
    (and (bv-le 0x20 shellcode24) (bv-le shellcode24 0x7F)) 
    (and (bv-le 0x20 shellcode25) (bv-le shellcode25 0x7F)) 
    (and (bv-le 0x20 shellcode26) (bv-le shellcode26 0x7F)) 
    (and (bv-le 0x20 shellcode27) (bv-le shellcode27 0x7F)) 
    (and (bv-le 0x20 shellcode28) (bv-le shellcode28 0x7F)) 
    (and (bv-le 0x20 shellcode29) (bv-le shellcode29 0x7F)) 
    (and (bv-le 0x20 shellcode2A) (bv-le shellcode2A 0x7F)) 
    (and (bv-le 0x20 shellcode2B) (bv-le shellcode2B 0x7F)) 
    (and (bv-le 0x20 shellcode2C) (bv-le shellcode2C 0x7F)) 
    (and (bv-le 0x20 shellcode2D) (bv-le shellcode2D 0x7F)) 
    (and (bv-le 0x20 shellcode2E) (bv-le shellcode2E 0x7F)) 
    (and (bv-le 0x20 shellcode2F) (bv-le shellcode2F 0x7F)) 
    (and (bv-le 0x20 shellcode30) (bv-le shellcode30 0x7F)) 
    (and (bv-le 0x20 shellcode31) (bv-le shellcode31 0x7F)) 
    (and (bv-le 0x20 shellcode32) (bv-le shellcode32 0x7F)) 
    (and (bv-le 0x20 shellcode33) (bv-le shellcode33 0x7F)) 
    (and (bv-le 0x20 shellcode34) (bv-le shellcode34 0x7F)) 
    (and (bv-le 0x20 shellcode35) (bv-le shellcode35 0x7F)) 
    (and (bv-le 0x20 shellcode36) (bv-le shellcode36 0x7F)) 
    (and (bv-le 0x20 shellcode37) (bv-le shellcode37 0x7F)) 
    (and (bv-le 0x20 shellcode38) (bv-le shellcode38 0x7F)) 
    (and (bv-le 0x20 shellcode39) (bv-le shellcode39 0x7F)) 
    (and (bv-le 0x20 shellcode3A) (bv-le shellcode3A 0x7F)) 
    (and (bv-le 0x20 shellcode3B) (bv-le shellcode3B 0x7F)) 
    (and (bv-le 0x20 shellcode3C) (bv-le shellcode3C 0x7F)) 
    (and (bv-le 0x20 shellcode3D) (bv-le shellcode3D 0x7F)) 
    (and (bv-le 0x20 shellcode3E) (bv-le shellcode3E 0x7F)) 
    (and (bv-le 0x20 shellcode3F) (bv-le shellcode3F 0x7F)) 
    (and (bv-le 0x20 shellcode40) (bv-le shellcode40 0x7F)) 
    (and (bv-le 0x20 shellcode41) (bv-le shellcode41 0x7F)) 
    (and (bv-le 0x20 shellcode42) (bv-le shellcode42 0x7F)) 
    (and (bv-le 0x20 shellcode43) (bv-le shellcode43 0x7F)) 
    (and (bv-le 0x20 shellcode44) (bv-le shellcode44 0x7F)) 
    (and (bv-le 0x20 shellcode45) (bv-le shellcode45 0x7F)) 
    (and (bv-le 0x20 shellcode46) (bv-le shellcode46 0x7F)) 
    (and (bv-le 0x20 shellcode47) (bv-le shellcode47 0x7F)) 
    (and (bv-le 0x20 shellcode48) (bv-le shellcode48 0x7F)) 
    (and (bv-le 0x20 shellcode49) (bv-le shellcode49 0x7F)) 
    (and (bv-le 0x20 shellcode4A) (bv-le shellcode4A 0x7F)) 
    (and (bv-le 0x20 shellcode4B) (bv-le shellcode4B 0x7F)) 
    (and (bv-le 0x20 shellcode4C) (bv-le shellcode4C 0x7F)) 
    (and (bv-le 0x20 shellcode4D) (bv-le shellcode4D 0x7F)) 
    (and (bv-le 0x20 shellcode4E) (bv-le shellcode4E 0x7F)) 
    (and (bv-le 0x20 shellcode4F) (bv-le shellcode4F 0x7F)) 
    (and (bv-le 0x20 shellcode50) (bv-le shellcode50 0x7F)) 
    (and (bv-le 0x20 shellcode51) (bv-le shellcode51 0x7F)) 
    (and (bv-le 0x20 shellcode52) (bv-le shellcode52 0x7F)) 
    (and (bv-le 0x20 shellcode53) (bv-le shellcode53 0x7F)) 
    (and (bv-le 0x20 shellcode54) (bv-le shellcode54 0x7F)) 
    (and (bv-le 0x20 shellcode55) (bv-le shellcode55 0x7F)) 
    (and (bv-le 0x20 shellcode56) (bv-le shellcode56 0x7F)) 
    (and (bv-le 0x20 shellcode57) (bv-le shellcode57 0x7F)) 
    (and (bv-le 0x20 shellcode58) (bv-le shellcode58 0x7F)) 
    (and (bv-le 0x20 shellcode59) (bv-le shellcode59 0x7F)) 
    (and (bv-le 0x20 shellcode5A) (bv-le shellcode5A 0x7F)) 
    (and (bv-le 0x20 shellcode5B) (bv-le shellcode5B 0x7F)) 
    (and (bv-le 0x20 shellcode5C) (bv-le shellcode5C 0x7F)) 
    (and (bv-le 0x20 shellcode5D) (bv-le shellcode5D 0x7F)) 
    (and (bv-le 0x20 shellcode5E) (bv-le shellcode5E 0x7F)) 
    (and (bv-le 0x20 shellcode5F) (bv-le shellcode5F 0x7F)) 
    (and (bv-le 0x20 shellcode60) (bv-le shellcode60 0x7F)) 
    (and (bv-le 0x20 shellcode61) (bv-le shellcode61 0x7F)) 
    (and (bv-le 0x20 shellcode62) (bv-le shellcode62 0x7F)) 
    (and (bv-le 0x20 shellcode63) (bv-le shellcode63 0x7F)) 
    (and (bv-le 0x20 shellcode64) (bv-le shellcode64 0x7F)) 
    (and (bv-le 0x20 shellcode65) (bv-le shellcode65 0x7F)) 
    (and (bv-le 0x20 shellcode66) (bv-le shellcode66 0x7F)) 
    (and (bv-le 0x20 shellcode67) (bv-le shellcode67 0x7F)) 
    (and (bv-le 0x20 shellcode68) (bv-le shellcode68 0x7F)) 
    (and (bv-le 0x20 shellcode69) (bv-le shellcode69 0x7F)) 
    (and (bv-le 0x20 shellcode6A) (bv-le shellcode6A 0x7F)) 
    (and (bv-le 0x20 shellcode6B) (bv-le shellcode6B 0x7F)) 
    (and (bv-le 0x20 shellcode6C) (bv-le shellcode6C 0x7F)) 
    (and (bv-le 0x20 shellcode6D) (bv-le shellcode6D 0x7F)) 
    (and (bv-le 0x20 shellcode6E) (bv-le shellcode6E 0x7F)) 
    (and (bv-le 0x20 shellcode6F) (bv-le shellcode6F 0x7F)) 
    (and (bv-le 0x20 shellcode70) (bv-le shellcode70 0x7F)) 
    (and (bv-le 0x20 shellcode71) (bv-le shellcode71 0x7F)) 
    (and (bv-le 0x20 shellcode72) (bv-le shellcode72 0x7F)) 
    (and (bv-le 0x20 shellcode73) (bv-le shellcode73 0x7F)) 
    (and (bv-le 0x20 shellcode74) (bv-le shellcode74 0x7F)) 
    (and (bv-le 0x20 shellcode75) (bv-le shellcode75 0x7F)) 
    (and (bv-le 0x20 shellcode76) (bv-le shellcode76 0x7F)) 
    (and (bv-le 0x20 shellcode77) (bv-le shellcode77 0x7F)) 
    (and (bv-le 0x20 shellcode78) (bv-le shellcode78 0x7F)) 
    (and (bv-le 0x20 shellcode79) (bv-le shellcode79 0x7F)) 
    (and (bv-le 0x20 shellcode7A) (bv-le shellcode7A 0x7F)) 
    (and (bv-le 0x20 shellcode7B) (bv-le shellcode7B 0x7F)) 
    (and (bv-le 0x20 shellcode7C) (bv-le shellcode7C 0x7F)) 
    (and (bv-le 0x20 shellcode7D) (bv-le shellcode7D 0x7F)) 
    (and (bv-le 0x20 shellcode7E) (bv-le shellcode7E 0x7F)) 
    (and (bv-le 0x20 shellcode7F) (bv-le shellcode7F 0x7F))   
  )
)

; Loop
(assert
  (forall (r0::Dword r1::Dword r2::Dword r3::Dword r4::Dword r5::Dword r6::Dword r7::Dword scinptr::Byte sclow::Byte schigh::Byte)
    (let ((scoutptr (bv-lshr scinptr 0x01)))
    (let ((state0   (bv-concat Eip1 scoutptr scinptr schigh sclow r7 r6 r5 r4 r3 r2 r1 r0)))
    (let ((state1   (simulate-insn Ins0 Eip1 Eip1 state0)))
    (let ((state2   (simulate-insn Ins1 Eip2 Eip2 state0)))
    (let ((state3   (simulate-insn Ins2 Eip3 Eip3 state2)))
    (let ((state4   (simulate-insn Ins3 Eip4 Eip4 state3)))
    (let ((state5   (simulate-insn Ins4 Eip5 Eip5 state4)))
    (let ((state6   (simulate-insn Ins5 Eip6 Eip6 state5)))
    (let ((state7   (simulate-insn Ins6 Eip7 Eip7 state6)))
    (let ((state8   (simulate-insn Ins7 Eip8 Eip8 state7)))
    (let ((state9   (simulate-insn Ins8 Eip9 Eip9 state8)))
    (let ((stateA   (simulate-insn Ins9 EipLoopEnd EipLoopBeg state9)))
    (let ((begindecodestate state0))
    (let ((finaldecodestate state7))
    (let ((beginstorestate  state7))
    (let ((finalstorestate  state8))
    (let ((begindecstate    state8))
    (let ((finaldecstate    state9))
    (let ((finalloopstate   stateA))
    (let ((sclength  0x00000040))
    (let ((sclengthd 0x00000080))
    (let ((sclengthlow  (bv-extract 7 0 sclength)))
    (let ((sclengthdlow (bv-extract 7 0 sclengthd)))
    (let ((decodedbyte (sms-getscbyte-byidx finalstorestate scoutptr)))

    (and 
      ; INITIALIZATION BLOCK
      ; Some register contains the size of the shellcode
      (= (sms-getreg32 WhichReg state1) sclength)
      
      ; DECODE BLOCK
      ; The shellcode input pointer has increased by two, AND
      (= (sms-getscinptr finaldecodestate) (bv-add scinptr 0x02))
      (= (sms-getscoutptr finaldecodestate) (sms-getscoutptr begindecodestate))
      (= (sms-getreg32 WhichReg finaldecodestate) (sms-getreg32 WhichReg begindecodestate))
      (= (sms-getscstate finaldecodestate) (sms-getscstate begindecodestate))
      
      ; STORE BLOCK
      ; The shellcode output pointer has increased by one, AND
      (= (sms-getscoutptr finalstorestate) (bv-add scoutptr 0x01))
      (= (sms-getscinptr finalstorestate) (sms-getscinptr beginstorestate))
      (= (sms-getreg32 WhichReg finaldecodestate) (sms-getreg32 WhichReg begindecodestate))
      
      ; DECREMENT BLOCK
      ; The counter register has decreased by one, AND
      (= (bv-add (sms-getreg32 WhichReg finaldecstate) 0x00000001) (sms-getreg32 WhichReg begindecstate))
      (= (sms-getscinptr finaldecstate) (sms-getscinptr begindecstate))
      (= (sms-getscoutptr finaldecstate) (sms-getscoutptr begindecstate))
      (= (sms-getscstate finaldecstate) (sms-getscstate begindecstate))

      ; CONDITIONAL JUMP BLOCK
      ; The EIP after executing the block is either the one after the loop, or at its beginning, AND
      (= (sms-getnexteip finalloopstate) (ite (= 0x00000000 (sms-getreg32 WhichReg finalloopstate)) EipLoopEnd EipLoopBeg))

      ; DECODER LOGIC
      (=> (and (= 0x00 scinptr) (= sclow shellcode00) (= schigh shellcode01)) (= decodedbyte 0xA0))
      (=> (and (= 0x02 scinptr) (= sclow shellcode01) (= schigh shellcode02)) (= decodedbyte 0x8C))
      (=> (and (= 0x04 scinptr) (= sclow shellcode02) (= schigh shellcode03)) (= decodedbyte 0x1C))
      (=> (and (= 0x06 scinptr) (= sclow shellcode03) (= schigh shellcode04)) (= decodedbyte 0x29))
      (=> (and (= 0x08 scinptr) (= sclow shellcode04) (= schigh shellcode05)) (= decodedbyte 0xA1))
      (=> (and (= 0x0a scinptr) (= sclow shellcode05) (= schigh shellcode06)) (= decodedbyte 0xCC))
      (=> (and (= 0x0c scinptr) (= sclow shellcode06) (= schigh shellcode07)) (= decodedbyte 0x38))
      (=> (and (= 0x0e scinptr) (= sclow shellcode07) (= schigh shellcode08)) (= decodedbyte 0xFD))
      (=> (and (= 0x10 scinptr) (= sclow shellcode08) (= schigh shellcode09)) (= decodedbyte 0x8D))
      (=> (and (= 0x12 scinptr) (= sclow shellcode09) (= schigh shellcode0A)) (= decodedbyte 0xF4))
      (=> (and (= 0x14 scinptr) (= sclow shellcode0A) (= schigh shellcode0B)) (= decodedbyte 0x8E))
      (=> (and (= 0x16 scinptr) (= sclow shellcode0B) (= schigh shellcode0C)) (= decodedbyte 0x59))
      (=> (and (= 0x18 scinptr) (= sclow shellcode0C) (= schigh shellcode0D)) (= decodedbyte 0x86))
      (=> (and (= 0x1a scinptr) (= sclow shellcode0D) (= schigh shellcode0E)) (= decodedbyte 0xB7))
      (=> (and (= 0x1c scinptr) (= sclow shellcode0E) (= schigh shellcode0F)) (= decodedbyte 0xCA))
      (=> (and (= 0x1e scinptr) (= sclow shellcode0F) (= schigh shellcode10)) (= decodedbyte 0xFF))
      (=> (and (= 0x20 scinptr) (= sclow shellcode10) (= schigh shellcode11)) (= decodedbyte 0x33))
      (=> (and (= 0x22 scinptr) (= sclow shellcode11) (= schigh shellcode12)) (= decodedbyte 0x29))
      (=> (and (= 0x24 scinptr) (= sclow shellcode12) (= schigh shellcode13)) (= decodedbyte 0xD6))
      (=> (and (= 0x26 scinptr) (= sclow shellcode13) (= schigh shellcode14)) (= decodedbyte 0xE3))
      (=> (and (= 0x28 scinptr) (= sclow shellcode14) (= schigh shellcode15)) (= decodedbyte 0x6F))
      (=> (and (= 0x2a scinptr) (= sclow shellcode15) (= schigh shellcode16)) (= decodedbyte 0x4B))
      (=> (and (= 0x2c scinptr) (= sclow shellcode16) (= schigh shellcode17)) (= decodedbyte 0x19))
      (=> (and (= 0x2e scinptr) (= sclow shellcode17) (= schigh shellcode18)) (= decodedbyte 0x71))
      (=> (and (= 0x30 scinptr) (= sclow shellcode18) (= schigh shellcode19)) (= decodedbyte 0x5C))
      (=> (and (= 0x32 scinptr) (= sclow shellcode19) (= schigh shellcode1A)) (= decodedbyte 0xBB))
      (=> (and (= 0x34 scinptr) (= sclow shellcode1A) (= schigh shellcode1B)) (= decodedbyte 0x4E))
      (=> (and (= 0x36 scinptr) (= sclow shellcode1B) (= schigh shellcode1C)) (= decodedbyte 0x90))
      (=> (and (= 0x38 scinptr) (= sclow shellcode1C) (= schigh shellcode1D)) (= decodedbyte 0xC3))
      (=> (and (= 0x3a scinptr) (= sclow shellcode1D) (= schigh shellcode1E)) (= decodedbyte 0xF7))
      (=> (and (= 0x3c scinptr) (= sclow shellcode1E) (= schigh shellcode1F)) (= decodedbyte 0x41))
      (=> (and (= 0x3e scinptr) (= sclow shellcode1F) (= schigh shellcode20)) (= decodedbyte 0x9E))
      (=> (and (= 0x40 scinptr) (= sclow shellcode20) (= schigh shellcode21)) (= decodedbyte 0xA2))
      (=> (and (= 0x42 scinptr) (= sclow shellcode21) (= schigh shellcode22)) (= decodedbyte 0x1C))
      (=> (and (= 0x44 scinptr) (= sclow shellcode22) (= schigh shellcode23)) (= decodedbyte 0x22))
      (=> (and (= 0x46 scinptr) (= sclow shellcode23) (= schigh shellcode24)) (= decodedbyte 0xBF))
      (=> (and (= 0x48 scinptr) (= sclow shellcode24) (= schigh shellcode25)) (= decodedbyte 0x25))
      (=> (and (= 0x4a scinptr) (= sclow shellcode25) (= schigh shellcode26)) (= decodedbyte 0x0F))
      (=> (and (= 0x4c scinptr) (= sclow shellcode26) (= schigh shellcode27)) (= decodedbyte 0xFE))
      (=> (and (= 0x4e scinptr) (= sclow shellcode27) (= schigh shellcode28)) (= decodedbyte 0xA6))
      (=> (and (= 0x50 scinptr) (= sclow shellcode28) (= schigh shellcode29)) (= decodedbyte 0x81))
      (=> (and (= 0x52 scinptr) (= sclow shellcode29) (= schigh shellcode2A)) (= decodedbyte 0x10))
      (=> (and (= 0x54 scinptr) (= sclow shellcode2A) (= schigh shellcode2B)) (= decodedbyte 0x43))
      (=> (and (= 0x56 scinptr) (= sclow shellcode2B) (= schigh shellcode2C)) (= decodedbyte 0x38))
      (=> (and (= 0x58 scinptr) (= sclow shellcode2C) (= schigh shellcode2D)) (= decodedbyte 0x92))
      (=> (and (= 0x5a scinptr) (= sclow shellcode2D) (= schigh shellcode2E)) (= decodedbyte 0x95))
      (=> (and (= 0x5c scinptr) (= sclow shellcode2E) (= schigh shellcode2F)) (= decodedbyte 0x21))
      (=> (and (= 0x5e scinptr) (= sclow shellcode2F) (= schigh shellcode30)) (= decodedbyte 0x2B))
      (=> (and (= 0x60 scinptr) (= sclow shellcode30) (= schigh shellcode31)) (= decodedbyte 0xE3))
      (=> (and (= 0x62 scinptr) (= sclow shellcode31) (= schigh shellcode32)) (= decodedbyte 0xA6))
      (=> (and (= 0x64 scinptr) (= sclow shellcode32) (= schigh shellcode33)) (= decodedbyte 0xE9))
      (=> (and (= 0x66 scinptr) (= sclow shellcode33) (= schigh shellcode34)) (= decodedbyte 0xAC))
      (=> (and (= 0x68 scinptr) (= sclow shellcode34) (= schigh shellcode35)) (= decodedbyte 0x08))
      (=> (and (= 0x6a scinptr) (= sclow shellcode35) (= schigh shellcode36)) (= decodedbyte 0x4D))
      (=> (and (= 0x6c scinptr) (= sclow shellcode36) (= schigh shellcode37)) (= decodedbyte 0xBA))
      (=> (and (= 0x6e scinptr) (= sclow shellcode37) (= schigh shellcode38)) (= decodedbyte 0x08))
      (=> (and (= 0x70 scinptr) (= sclow shellcode38) (= schigh shellcode39)) (= decodedbyte 0x0B))
      (=> (and (= 0x72 scinptr) (= sclow shellcode39) (= schigh shellcode3A)) (= decodedbyte 0xAB))
      (=> (and (= 0x74 scinptr) (= sclow shellcode3A) (= schigh shellcode3B)) (= decodedbyte 0x22))
      (=> (and (= 0x76 scinptr) (= sclow shellcode3B) (= schigh shellcode3C)) (= decodedbyte 0x84))
      (=> (and (= 0x78 scinptr) (= sclow shellcode3C) (= schigh shellcode3D)) (= decodedbyte 0x6B))
      (=> (and (= 0x7a scinptr) (= sclow shellcode3D) (= schigh shellcode3E)) (= decodedbyte 0x1F))
      (=> (and (= 0x7c scinptr) (= sclow shellcode3E) (= schigh shellcode3F)) (= decodedbyte 0xAD))
      (=> (and (= 0x7e scinptr) (= sclow shellcode3F) (= schigh shellcode40)) (= decodedbyte 0x05))      
      
      
      
      ; ; THIS MIGHT BE SLOW; IT WOULD PAY TO INVESTIGATE WHETHER IT CAN BE SPED UP
      ; ; Implication:
    )
    ))))))))))))))))))))))) ; end let sequence
  ) ; end forall
) ; end assert

; Solve the constraint system
(ef-solve)

; Produce a model, i.e., values for bytecode00-bytecodeFF.
; This statement will crash yices if (ef-solve) returned unsatisfiable.
(show-model)