gistfile1.txt

~/src/evm-semantics(exception-checker) $ ./kevm bugcheck tests/interactive/bug-checker/invalid-opcode.evm
== bug-checking: tests/interactive/bug-checker/invalid-opcode.evm
(error "line 12 column 35: Sorts Int and KItem are incompatible")
(error "line 12 column 35: Sorts Int and KItem are incompatible")
(error "line 13 column 35: Sorts Int and KItem are incompatible")
(error "line 13 column 35: Sorts Int and KItem are incompatible")
(error "line 13 column 35: Sorts Int and KItem are incompatible")
#accountExists ( V0 ) ==K true #And
Result ==K <generatedTop>
  <k>
    runVM ( V1 , V2 , V0 , V3 , V4 , V5 , V6 , V7 , V8 , V9 , V10 , V11 , V12 , V13 ) ~> #push ~> #pc [ PUSH ( 32 , chop ( V14 ) ) ] ~> #? #dropCallStack : #popCallStack ?# ~> #execute ~> exception ~> status EVMC_INVALID_INSTRUCTION clear .EthereumSimulation
  </k>
  <exit-code>
    1
  </exit-code>
  <mode>
    NORMAL
  </mode>
  <schedule>
    DEFAULT
  </schedule>
  <analysis>
    .Map
  </analysis>
  <ethereum>
    <evm>
      <output>
        .WordStack
      </output>
      <statusCode>
        .StatusCode
      </statusCode>
      <callStack>
        ListItem ( <callState>-fragment <program>
          0 |-> PUSH ( 32 , chop ( V14 ) ) ; PUSH ( 2 , 40 ) ; JUMPI ; INVALID ; .OpCodes
          38 |-> JUMPDEST ; STOP ; .OpCodes
        </program> <programBlock>
          PUSH ( 2 , 40 ) ; JUMPI ; INVALID ; .OpCodes
        </programBlock> <programBytes>
          .WordStack
        </programBytes> <id>
          0
        </id> <caller>
          0
        </caller> <callData>
          .WordStack
        </callData> <callValue>
          0
        </callValue> <wordStack>
          .WordStack
        </wordStack> <localMem>
          .Map
        </localMem> <pc>
          0
        </pc> <gas>
          100000000000
        </gas> <memoryUsed>
          0
        </memoryUsed> <callGas>
          0
        </callGas> <static>
          false
        </static> <callDepth>
          0
        </callDepth> </callState>-fragment )
      </callStack>
      <interimStates>
        .List
      </interimStates>
      <touchedAccounts>
        .Set
      </touchedAccounts>
      <callState>
        <program>
          0 |-> PUSH ( 32 , chop ( V14 ) ) ; PUSH ( 2 , 40 ) ; JUMPI ; INVALID ; .OpCodes
          38 |-> JUMPDEST ; STOP ; .OpCodes
        </program>
        <programBlock>
          PUSH ( 2 , 40 ) ; JUMPI ; INVALID ; .OpCodes
        </programBlock>
        <programBytes>
          .WordStack
        </programBytes>
        <id>
          0
        </id>
        <caller>
          0
        </caller>
        <callData>
          .WordStack
        </callData>
        <callValue>
          0
        </callValue>
        <wordStack>
          .WordStack
        </wordStack>
        <localMem>
          .Map
        </localMem>
        <pc>
          0
        </pc>
        <gas>
          99999999997
        </gas>
        <memoryUsed>
          0
        </memoryUsed>
        <callGas>
          0
        </callGas>
        <static>
          false
        </static>
        <callDepth>
          0
        </callDepth>
      </callState>
      <substate>
        <selfDestruct>
          .Set
        </selfDestruct>
        <log>
          .List
        </log>
        <refund>
          0
        </refund>
      </substate>
      <gasPrice>
        0
      </gasPrice>
      <origin>
        0
      </origin>
      <previousHash>
        0
      </previousHash>
      <ommersHash>
        0
      </ommersHash>
      <coinbase>
        0
      </coinbase>
      <stateRoot>
        0
      </stateRoot>
      <transactionsRoot>
        0
      </transactionsRoot>
      <receiptsRoot>
        0
      </receiptsRoot>
      <logsBloom>
        .WordStack
      </logsBloom>
      <difficulty>
        0
      </difficulty>
      <number>
        0
      </number>
      <gasLimit>
        0
      </gasLimit>
      <gasUsed>
        0
      </gasUsed>
      <timestamp>
        0
      </timestamp>
      <extraData>
        .WordStack
      </extraData>
      <mixHash>
        0
      </mixHash>
      <blockNonce>
        0
      </blockNonce>
      <ommerBlockHeaders>
        [ .JSONList ]
      </ommerBlockHeaders>
      <blockhash>
        .List
      </blockhash>
    </evm>
    <network>
      <activeAccounts>
        SetItem ( V0 )
      </activeAccounts>
      <accounts>
        <acctID>
          V0
        </acctID> |-> <account>
          <acctID>
            V0
          </acctID>
          <balance>
            #getBalance ( V0 )
          </balance>
          <code>
            #if #isCodeEmpty ( V0 ) #then .WordStack #else #unloaded #fi
          </code>
          <storage>
            .Map
          </storage>
          <nonce>
            #getNonce ( V0 )
          </nonce>
        </account>
      </accounts>
      <txOrder>
        .List
      </txOrder>
      <txPending>
        .List
      </txPending>
      <messages>
        .Map
      </messages>
    </network>
  </ethereum>
</generatedTop> #And
chop ( V14 ) ==K runVM ( V1 , V2 , V0 , V3 , V4 , V5 , V6 , V7 , V8 , V9 , V10 , V11 , V12 , V13 )
[Warning] Critical: failed to translate smtlib expression:
(declare-sort KItem)
(declare-sort WordStack)
(declare-fun sizeWordStackAux (WordStack Int) Int)
(declare-fun sizeWordStack (WordStack) Int)
(declare-fun smt_keccak (WordStack) Int)
(declare-fun asByteStack (Int WordStack) WordStack)
(declare-fun chop (Int) Int)
(declare-fun asWord (WordStack) Int)
(assert (forall ((|_391| Int)) (= (chop |_391|) (mod |_391|
115792089237316195423570985008687907853269984665640564039457584007913129639936))))
(declare-fun |_939| () Int)
(declare-fun |_2108| () KItem)
(assert (and (= (chop |_939|) _2108))) (unknown)
[Warning] Critical: failed to translate smtlib expression:
(declare-sort KItem)
(declare-sort WordStack)
(declare-fun sizeWordStackAux (WordStack Int) Int)
(declare-fun sizeWordStack (WordStack) Int)
(declare-fun smt_keccak (WordStack) Int) 
(declare-fun asByteStack (Int WordStack) WordStack)
(declare-fun chop (Int) Int)
(declare-fun asWord (WordStack) Int)
(assert (forall ((|_391| Int)) (= (chop |_391|) (mod |_391|
115792089237316195423570985008687907853269984665640564039457584007913129639936))))
(declare-fun |_939| () Int)
(declare-fun |_2126| () KItem)
(assert (and (= (chop |_939|) _2126))) (unknown)
[Warning] Critical: failed to translate smtlib expression:
(declare-sort KItem)
(declare-sort WordStack)
(declare-fun sizeWordStackAux (WordStack Int) Int)
(declare-fun sizeWordStack (WordStack) Int)
(declare-fun smt_keccak (WordStack) Int) 
(declare-fun asByteStack (Int WordStack) WordStack)
(declare-fun chop (Int) Int)
(declare-fun asWord (WordStack) Int)
(assert (forall ((|_391| Int)) (= (chop |_391|) (mod |_391|
115792089237316195423570985008687907853269984665640564039457584007913129639936))))
(declare-fun |_939| () Int)
(declare-fun |_2127| () KItem)
(declare-fun |_2128| () Bool)
(assert (and (= (chop |_939|) _2127) (= _2128 true))) (unknown)
[Warning] Critical: failed to translate smtlib expression:
(declare-sort KItem)
(declare-sort WordStack)
(declare-fun sizeWordStackAux (WordStack Int) Int)
(declare-fun sizeWordStack (WordStack) Int)
(declare-fun smt_keccak (WordStack) Int) 
(declare-fun asByteStack (Int WordStack) WordStack)
(declare-fun chop (Int) Int)
(declare-fun asWord (WordStack) Int)
(assert (forall ((|_391| Int)) (= (chop |_391|) (mod |_391|
115792089237316195423570985008687907853269984665640564039457584007913129639936))))
(declare-fun |_939| () Int)
(declare-fun |_2130| () KItem)
(declare-fun |_2131| () Bool)
(assert (and (= (chop |_939|) _2130) (= _2131 true))) (unknown)
[Warning] Critical: failed to translate smtlib expression:
(declare-sort KItem)
(declare-sort WordStack)
(declare-fun sizeWordStackAux (WordStack Int) Int)
(declare-fun sizeWordStack (WordStack) Int)
(declare-fun smt_keccak (WordStack) Int) 
(declare-fun asByteStack (Int WordStack) WordStack)
(declare-fun chop (Int) Int)
(declare-fun asWord (WordStack) Int)
(assert (forall ((|_391| Int)) (= (chop |_391|) (mod |_391|
115792089237316195423570985008687907853269984665640564039457584007913129639936))))
(declare-fun |_939| () Int)
(declare-fun |_2143| () KItem)
(declare-fun |_2144| () Bool)
(assert (and (= (chop |_939|) _2143) (= _2144 true))) (unknown)
[Warning] Critical: missing SMTLib translation for #accountExists (missing
SMTLib translation for #accountExists)