Skip to content

Instantly share code, notes, and snippets.

@desaperados

desaperados/heal.err.log

Created February 20, 2020 06:09
Show Gist options
  • Star 0 You must be signed in to star a gist
  • Fork 0 You must be signed in to fork a gist
  • Save desaperados/5e39b9e62c3c3130fb9daeda8d01fa71 to your computer and use it in GitHub Desktop.
Save desaperados/5e39b9e62c3c3130fb9daeda8d01fa71 to your computer and use it in GitHub Desktop.
Download ZIP
Raw
heal.err.log
==========================================
Top term when exception was thrown:
==========================================
<kevm>(<k>(#KSequence(#popCallStack_EVM(.KList), #popWorldState_EVM(.KList), Int(#"0"), #push_EVM(.KList), R_DotVar1_1984:K)),, <exit-code>(Int(#"1")),, <mode>(NORMAL(.KList)),, <schedule>(ISTANBUL_EVM(.KList)),, <ethereum>(<evm>(<output>(VOutput_1809:WordStack),, <statusCode>(EVMC_STACK_OVERFLOW_NETWORK(.KList)),, <callStack>(VCallStack_1807:List),, <interimStates>(_2_1871:List),, <touchedAccounts>(_3_1841:Set),, <callState>(<program>(_:_WS(Int(#"96"),, _:_WS(Int(#"128"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"82"),, _:_WS(Int(#"52"),, _:_WS(Int(#"128"),, _:_WS(Int(#"21"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"16"),, _:_WS(Int(#"87"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"128"),, _:_WS(Int(#"253"),, _:_WS(Int(#"91"),, _:_WS(Int(#"80"),, _:_WS(Int(#"96"),, _:_WS(Int(#"4"),, _:_WS(Int(#"54"),, _:_WS(Int(#"16"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"87"),, _:_WS(Int(#"87"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"53"),, _:_WS(Int(#"96"),, _:_WS(Int(#"224"),, _:_WS(Int(#"28"),, _:_WS(Int(#"128"),, _:_WS(Int(#"99"),, _:_WS(Int(#"13"),, _:_WS(Int(#"202"),, _:_WS(Int(#"89"),, _:_WS(Int(#"193"),, _:_WS(Int(#"20"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"92"),, _:_WS(Int(#"87"),, _:_WS(Int(#"128"),, _:_WS(Int(#"99"),, _:_WS(Int(#"45"),, _:_WS(Int(#"97"),, _:_WS(Int(#"163"),, _:_WS(Int(#"85"),, _:_WS(Int(#"20"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"122"),, _:_WS(Int(#"87"),, _:_WS(Int(#"128"),, _:_WS(Int(#"99"),, _:_WS(Int(#"73"),, _:_WS(Int(#"43"),, _:_WS(Int(#"9"),, _:_WS(Int(#"190"),, _:_WS(Int(#"20"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"152"),, _:_WS(Int(#"87"),, _:_WS(Int(#"128"),, _:_WS(Int(#"99"),, _:_WS(Int(#"108"),, _:_WS(Int(#"37"),, _:_WS(Int(#"179"),, _:_WS(Int(#"70"),, _:_WS(Int(#"20"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"198"),, _:_WS(Int(#"87"),, _:_WS(Int(#"128"),, _:_WS(Int(#"99"),, _:_WS(Int(#"240"),, _:_WS(Int(#"89"),, _:_WS(Int(#"33"),, _:_WS(Int(#"42"),, _:_WS(Int(#"20"),, _:_WS(Int(#"97"),, _:_WS(Int(#"1"),, _:_WS(Int(#"30"),, _:_WS(Int(#"87"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"128"),, _:_WS(Int(#"253"),, _:_WS(Int(#"91"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"100"),, _:_WS(Int(#"97"),, _:_WS(Int(#"1"),, _:_WS(Int(#"118"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"81"),, _:_WS(Int(#"128"),, _:_WS(Int(#"130"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"145"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"81"),, _:_WS(Int(#"128"),, _:_WS(Int(#"145"),, _:_WS(Int(#"3"),, _:_WS(Int(#"144"),, _:_WS(Int(#"243"),, _:_WS(Int(#"91"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"130"),, _:_WS(Int(#"97"),, _:_WS(Int(#"1"),, _:_WS(Int(#"124"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"81"),, _:_WS(Int(#"128"),, _:_WS(Int(#"130"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"145"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"81"),, _:_WS(Int(#"128"),, _:_WS(Int(#"145"),, _:_WS(Int(#"3"),, _:_WS(Int(#"144"),, _:_WS(Int(#"243"),, _:_WS(Int(#"91"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"196"),, _:_WS(Int(#"96"),, _:_WS(Int(#"4"),, _:_WS(Int(#"128"),, _:_WS(Int(#"54"),, _:_WS(Int(#"3"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"129"),, _:_WS(Int(#"16"),, _:_WS(Int(#"21"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"174"),, _:_WS(Int(#"87"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"128"),, _:_WS(Int(#"253"),, _:_WS(Int(#"91"),, _:_WS(Int(#"129"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"128"),, _:_WS(Int(#"128"),, _:_WS(Int(#"53"),, _:_WS(Int(#"144"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"146"),, _:_WS(Int(#"145"),, _:_WS(Int(#"144"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"97"),, _:_WS(Int(#"1"),, _:_WS(Int(#"130"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"0"),, _:_WS(Int(#"91"),, _:_WS(Int(#"97"),, _:_WS(Int(#"1"),, _:_WS(Int(#"8"),, _:_WS(Int(#"96"),, _:_WS(Int(#"4"),, _:_WS(Int(#"128"),, _:_WS(Int(#"54"),, _:_WS(Int(#"3"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"129"),, _:_WS(Int(#"16"),, _:_WS(Int(#"21"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"220"),, _:_WS(Int(#"87"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"128"),, _:_WS(Int(#"253"),, _:_WS(Int(#"91"),, _:_WS(Int(#"129"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"128"),, _:_WS(Int(#"128"),, _:_WS(Int(#"53"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"144"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"146"),, _:_WS(Int(#"145"),, _:_WS(Int(#"144"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"97"),, _:_WS(Int(#"2"),, _:_WS(Int(#"191"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"81"),, _:_WS(Int(#"128"),, _:_WS(Int(#"130"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"145"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"81"),, _:_WS(Int(#"128"),, _:_WS(Int(#"145"),, _:_WS(Int(#"3"),, _:_WS(Int(#"144"),, _:_WS(Int(#"243"),, _:_WS(Int(#"91"),, _:_WS(Int(#"97"),, _:_WS(Int(#"1"),, _:_WS(Int(#"96"),, _:_WS(Int(#"96"),, _:_WS(Int(#"4"),, _:_WS(Int(#"128"),, _:_WS(Int(#"54"),, _:_WS(Int(#"3"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"129"),, _:_WS(Int(#"16"),, _:_WS(Int(#"21"),, _:_WS(Int(#"97"),, _:_WS(Int(#"1"),, _:_WS(Int(#"52"),, _:_WS(Int(#"87"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"128"),, _:_WS(Int(#"253"),, _:_WS(Int(#"91"),, _:_WS(Int(#"129"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"128"),, _:_WS(Int(#"128"),, _:_WS(Int(#"53"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"144"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"146"),, _:_WS(Int(#"145"),, _:_WS(Int(#"144"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"97"),, _:_WS(Int(#"2"),, _:_WS(Int(#"215"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"81"),, _:_WS(Int(#"128"),, _:_WS(Int(#"130"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"145"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"81"),, _:_WS(Int(#"128"),, _:_WS(Int(#"145"),, _:_WS(Int(#"3"),, _:_WS(Int(#"144"),, _:_WS(Int(#"243"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"2"),, _:_WS(Int(#"84"),, _:_WS(Int(#"129"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"3"),, _:_WS(Int(#"84"),, _:_WS(Int(#"129"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"97"),, _:_WS(Int(#"1"),, _:_WS(Int(#"203"),, _:_WS(Int(#"96"),, _:_WS(Int(#"1"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"51"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"32"),, _:_WS(Int(#"84"),, _:_WS(Int(#"130"),, _:_WS(Int(#"97"),, _:_WS(Int(#"2"),, _:_WS(Int(#"239"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"1"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"51"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"32"),, _:_WS(Int(#"129"),, _:_WS(Int(#"144"),, _:_WS(Int(#"85"),, _:_WS(Int(#"80"),, _:_WS(Int(#"97"),, _:_WS(Int(#"2"),, _:_WS(Int(#"86"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"128"),, _:_WS(Int(#"51"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"32"),, _:_WS(Int(#"84"),, _:_WS(Int(#"130"),, _:_WS(Int(#"97"),, _:_WS(Int(#"2"),, _:_WS(Int(#"239"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"128"),, _:_WS(Int(#"51"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"32"),, _:_WS(Int(#"129"),, _:_WS(Int(#"144"),, _:_WS(Int(#"85"),, _:_WS(Int(#"80"),, _:_WS(Int(#"97"),, _:_WS(Int(#"2"),, _:_WS(Int(#"164"),, _:_WS(Int(#"96"),, _:_WS(Int(#"3"),, _:_WS(Int(#"84"),, _:_WS(Int(#"130"),, _:_WS(Int(#"97"),, _:_WS(Int(#"2"),, _:_WS(Int(#"239"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"3"),, _:_WS(Int(#"129"),, _:_WS(Int(#"144"),, _:_WS(Int(#"85"),, _:_WS(Int(#"80"),, _:_WS(Int(#"97"),, _:_WS(Int(#"2"),, _:_WS(Int(#"182"),, _:_WS(Int(#"96"),, _:_WS(Int(#"2"),, _:_WS(Int(#"84"),, _:_WS(Int(#"130"),, _:_WS(Int(#"97"),, _:_WS(Int(#"2"),, _:_WS(Int(#"239"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"2"),, _:_WS(Int(#"129"),, _:_WS(Int(#"144"),, _:_WS(Int(#"85"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"82"),, _:_WS(Int(#"128"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"32"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"145"),, _:_WS(Int(#"80"),, _:_WS(Int(#"144"),, _:_WS(Int(#"80"),, _:_WS(Int(#"84"),, _:_WS(Int(#"129"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"1"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"82"),, _:_WS(Int(#"128"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"32"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"145"),, _:_WS(Int(#"80"),, _:_WS(Int(#"144"),, _:_WS(Int(#"80"),, _:_WS(Int(#"84"),, _:_WS(Int(#"129"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"129"),, _:_WS(Int(#"131"),, _:_WS(Int(#"3"),, _:_WS(Int(#"144"),, _:_WS(Int(#"80"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"130"),, _:_WS(Int(#"19"),, _:_WS(Int(#"21"),, _:_WS(Int(#"128"),, _:_WS(Int(#"97"),, _:_WS(Int(#"3"),, _:_WS(Int(#"6"),, _:_WS(Int(#"87"),, _:_WS(Int(#"80"),, _:_WS(Int(#"130"),, _:_WS(Int(#"129"),, _:_WS(Int(#"17"),, _:_WS(Int(#"21"),, _:_WS(Int(#"91"),, _:_WS(Int(#"97"),, _:_WS(Int(#"3"),, _:_WS(Int(#"15"),, _:_WS(Int(#"87"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"128"),, _:_WS(Int(#"253"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"130"),, _:_WS(Int(#"18"),, _:_WS(Int(#"21"),, _:_WS(Int(#"128"),, _:_WS(Int(#"97"),, _:_WS(Int(#"3"),, _:_WS(Int(#"31"),, _:_WS(Int(#"87"),, _:_WS(Int(#"80"),, _:_WS(Int(#"130"),, _:_WS(Int(#"129"),, _:_WS(Int(#"16"),, _:_WS(Int(#"21"),, _:_WS(Int(#"91"),, _:_WS(Int(#"97"),, _:_WS(Int(#"3"),, _:_WS(Int(#"40"),, _:_WS(Int(#"87"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"128"),, _:_WS(Int(#"253"),, _:_WS(Int(#"91"),, _:_WS(Int(#"146"),, _:_WS(Int(#"145"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"86"),, _:_WS(Int(#"254"),, _:_WS(Int(#"162"),, _:_WS(Int(#"101"),, _:_WS(Int(#"98"),, _:_WS(Int(#"122"),, _:_WS(Int(#"122"),, _:_WS(Int(#"114"),, _:_WS(Int(#"48"),, _:_WS(Int(#"88"),, _:_WS(Int(#"32"),, _:_WS(Int(#"15"),, _:_WS(Int(#"58"),, _:_WS(Int(#"38"),, _:_WS(Int(#"126"),, _:_WS(Int(#"205"),, _:_WS(Int(#"204"),, _:_WS(Int(#"170"),, _:_WS(Int(#"102"),, _:_WS(Int(#"16"),, _:_WS(Int(#"47"),, _:_WS(Int(#"52"),, _:_WS(Int(#"251"),, _:_WS(Int(#"239"),, _:_WS(Int(#"217"),, _:_WS(Int(#"245"),, _:_WS(Int(#"46"),, _:_WS(Int(#"125"),, _:_WS(Int(#"176"),, _:_WS(Int(#"173"),, _:_WS(Int(#"29"),, _:_WS(Int(#"168"),, _:_WS(Int(#"108"),, _:_WS(Int(#"107"),, _:_WS(Int(#"227"),, _:_WS(Int(#"147"),, _:_WS(Int(#"154"),, _:_WS(Int(#"137"),, _:_WS(Int(#"111"),, _:_WS(Int(#"253"),, _:_WS(Int(#"211"),, _:_WS(Int(#"52"),, _:_WS(Int(#"134"),, _:_WS(Int(#"100"),, _:_WS(Int(#"115"),, _:_WS(Int(#"111"),, _:_WS(Int(#"108"),, _:_WS(Int(#"99"),, _:_WS(Int(#"67"),, _:_WS(Int(#"0"),, _:_WS(Int(#"5"),, _:_WS(Int(#"9"),, _:_WS(Int(#"0"),, _:_WS(Int(#"50"),, .WordStack_EVM-TYPES(.KList))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),, <jumpDests>(Int(#"386") Int(#"130") Int(#"196") Int(#"774") Int(#"198") Int(#"264") Int(#"459") Int(#"783") Int(#"16") Int(#"598") Int(#"727") Int(#"87") Int(#"152") Int(#"220") Int(#"92") Int(#"286") Int(#"799") Int(#"352") Int(#"676") Int(#"100") Int(#"808") Int(#"174") Int(#"751") Int(#"308") Int(#"694") Int(#"374") Int(#"122") Int(#"380") Int(#"703")),, <id>(ACCT_ID_1819:Int),, <caller>(CALLER_ID_1879:Int),, <callData>(_5_1886:WordStack),, <callValue>(VCallValue_1808:Int),, <wordStack>(_:_WS(#unsigned(ABI_y_1813:Int),, _:_WS(ABI_x_1812:Int,, _:_WS(JMPTO_1815:Int,, WS_1885:WordStack)))),, <localMem>(_7_1821:Map),, <pc>(Int(#"751")),, <gas>(VGas_1877:Int),, <memoryUsed>(VMemoryUsed_1806:Int),, <callGas>(_9_1845:Int),, <static>(_11_1892:Bool),, <callDepth>(VCallDepth_1883:Int)),, <substate>(<selfDestruct>(VSelfDestruct_1894:Set),, <log>(_12_1872:List),, <refund>(_13_1847:Int)),, <gasPrice>(_14_1848:Int),, <origin>(ORIGIN_ID_1891:Int),, <blockhashes>(_15_1873:List),, <block>(<previousHash>(_16_1849:Int),, <ommersHash>(_17_1850:Int),, <coinbase>(_18_1851:Int),, <stateRoot>(_19_1852:Int),, <transactionsRoot>(_20_1853:Int),, <receiptsRoot>(_21_1854:Int),, <logsBloom>(_22_1888:WordStack),, <difficulty>(_23_1855:Int),, <number>(BLOCK_NUMBER_1870:Int),, <gasLimit>(_24_1856:Int),, <gasUsed>(_25_1857:Int),, <timestamp>(TIME_1876:Int),, <extraData>(_26_1889:WordStack),, <mixHash>(_27_1858:Int),, <blockNonce>(_28_1859:Int),, <ommerBlockHeaders>(_29_1818:JSON))),, <network>(<chainID>(_30_1860:Int),, <activeAccounts>(Int(#"1") Int(#"2") Int(#"3") Int(#"4") Int(#"5") Int(#"6") Int(#"7") Int(#"8") ACCT_ID_1819:Int_31_1843:Set),, <accounts>(<acctID>(Int(#"7")) |-> <account>(<acctID>(Int(#"7")),, <balance>(ECMUL_BAL_1890:Int),, <code>(.WordStack_EVM-TYPES(.KList)),, <storage>(_53_1836:Map),, <origStorage>(_54_1837:Map),, <nonce>(_55_1868:Int)) <acctID>(Int(#"8")) |-> <account>(<acctID>(Int(#"8")),, <balance>(ECPAIRING_BAL_1895:Int),, <code>(.WordStack_EVM-TYPES(.KList)),, <storage>(_56_1838:Map),, <origStorage>(_57_1839:Map),, <nonce>(_58_1869:Int)) <acctID>(Int(#"3")) |-> <account>(<acctID>(Int(#"3")),, <balance>(RIP160_BAL_1816:Int),, <code>(.WordStack_EVM-TYPES(.KList)),, <storage>(_41_1828:Map),, <origStorage>(_42_1829:Map),, <nonce>(_43_1864:Int)) <acctID>(Int(#"4")) |-> <account>(<acctID>(Int(#"4")),, <balance>(ID_BAL_1811:Int),, <code>(.WordStack_EVM-TYPES(.KList)),, <storage>(_44_1830:Map),, <origStorage>(_45_1831:Map),, <nonce>(_46_1865:Int)) <acctID>(Int(#"5")) |-> <account>(<acctID>(Int(#"5")),, <balance>(MODEXP_BAL_1884:Int),, <code>(.WordStack_EVM-TYPES(.KList)),, <storage>(_47_1832:Map),, <origStorage>(_48_1833:Map),, <nonce>(_49_1866:Int)) <acctID>(Int(#"6")) |-> <account>(<acctID>(Int(#"6")),, <balance>(ECADD_BAL_1893:Int),, <code>(.WordStack_EVM-TYPES(.KList)),, <storage>(_50_1834:Map),, <origStorage>(_51_1835:Map),, <nonce>(_52_1867:Int)) <acctID>(Int(#"1")) |-> <account>(<acctID>(Int(#"1")),, <balance>(ECREC_BAL_1814:Int),, <code>(.WordStack_EVM-TYPES(.KList)),, <storage>(_35_1824:Map),, <origStorage>(_36_1825:Map),, <nonce>(_37_1862:Int)) <acctID>(Int(#"2")) |-> <account>(<acctID>(Int(#"2")),, <balance>(SHA256_BAL_1817:Int),, <code>(.WordStack_EVM-TYPES(.KList)),, <storage>(_38_1826:Map),, <origStorage>(_39_1827:Map),, <nonce>(_40_1863:Int)) <acctID>(ACCT_ID_1819:Int) |-> <account>(<acctID>(ACCT_ID_1819:Int),, <balance>(ACCT_ID_balance_1882:Int),, <code>(_:_WS(Int(#"96"),, _:_WS(Int(#"128"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"82"),, _:_WS(Int(#"52"),, _:_WS(Int(#"128"),, _:_WS(Int(#"21"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"16"),, _:_WS(Int(#"87"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"128"),, _:_WS(Int(#"253"),, _:_WS(Int(#"91"),, _:_WS(Int(#"80"),, _:_WS(Int(#"96"),, _:_WS(Int(#"4"),, _:_WS(Int(#"54"),, _:_WS(Int(#"16"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"87"),, _:_WS(Int(#"87"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"53"),, _:_WS(Int(#"96"),, _:_WS(Int(#"224"),, _:_WS(Int(#"28"),, _:_WS(Int(#"128"),, _:_WS(Int(#"99"),, _:_WS(Int(#"13"),, _:_WS(Int(#"202"),, _:_WS(Int(#"89"),, _:_WS(Int(#"193"),, _:_WS(Int(#"20"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"92"),, _:_WS(Int(#"87"),, _:_WS(Int(#"128"),, _:_WS(Int(#"99"),, _:_WS(Int(#"45"),, _:_WS(Int(#"97"),, _:_WS(Int(#"163"),, _:_WS(Int(#"85"),, _:_WS(Int(#"20"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"122"),, _:_WS(Int(#"87"),, _:_WS(Int(#"128"),, _:_WS(Int(#"99"),, _:_WS(Int(#"73"),, _:_WS(Int(#"43"),, _:_WS(Int(#"9"),, _:_WS(Int(#"190"),, _:_WS(Int(#"20"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"152"),, _:_WS(Int(#"87"),, _:_WS(Int(#"128"),, _:_WS(Int(#"99"),, _:_WS(Int(#"108"),, _:_WS(Int(#"37"),, _:_WS(Int(#"179"),, _:_WS(Int(#"70"),, _:_WS(Int(#"20"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"198"),, _:_WS(Int(#"87"),, _:_WS(Int(#"128"),, _:_WS(Int(#"99"),, _:_WS(Int(#"240"),, _:_WS(Int(#"89"),, _:_WS(Int(#"33"),, _:_WS(Int(#"42"),, _:_WS(Int(#"20"),, _:_WS(Int(#"97"),, _:_WS(Int(#"1"),, _:_WS(Int(#"30"),, _:_WS(Int(#"87"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"128"),, _:_WS(Int(#"253"),, _:_WS(Int(#"91"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"100"),, _:_WS(Int(#"97"),, _:_WS(Int(#"1"),, _:_WS(Int(#"118"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"81"),, _:_WS(Int(#"128"),, _:_WS(Int(#"130"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"145"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"81"),, _:_WS(Int(#"128"),, _:_WS(Int(#"145"),, _:_WS(Int(#"3"),, _:_WS(Int(#"144"),, _:_WS(Int(#"243"),, _:_WS(Int(#"91"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"130"),, _:_WS(Int(#"97"),, _:_WS(Int(#"1"),, _:_WS(Int(#"124"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"81"),, _:_WS(Int(#"128"),, _:_WS(Int(#"130"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"145"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"81"),, _:_WS(Int(#"128"),, _:_WS(Int(#"145"),, _:_WS(Int(#"3"),, _:_WS(Int(#"144"),, _:_WS(Int(#"243"),, _:_WS(Int(#"91"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"196"),, _:_WS(Int(#"96"),, _:_WS(Int(#"4"),, _:_WS(Int(#"128"),, _:_WS(Int(#"54"),, _:_WS(Int(#"3"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"129"),, _:_WS(Int(#"16"),, _:_WS(Int(#"21"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"174"),, _:_WS(Int(#"87"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"128"),, _:_WS(Int(#"253"),, _:_WS(Int(#"91"),, _:_WS(Int(#"129"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"128"),, _:_WS(Int(#"128"),, _:_WS(Int(#"53"),, _:_WS(Int(#"144"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"146"),, _:_WS(Int(#"145"),, _:_WS(Int(#"144"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"97"),, _:_WS(Int(#"1"),, _:_WS(Int(#"130"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"0"),, _:_WS(Int(#"91"),, _:_WS(Int(#"97"),, _:_WS(Int(#"1"),, _:_WS(Int(#"8"),, _:_WS(Int(#"96"),, _:_WS(Int(#"4"),, _:_WS(Int(#"128"),, _:_WS(Int(#"54"),, _:_WS(Int(#"3"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"129"),, _:_WS(Int(#"16"),, _:_WS(Int(#"21"),, _:_WS(Int(#"97"),, _:_WS(Int(#"0"),, _:_WS(Int(#"220"),, _:_WS(Int(#"87"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"128"),, _:_WS(Int(#"253"),, _:_WS(Int(#"91"),, _:_WS(Int(#"129"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"128"),, _:_WS(Int(#"128"),, _:_WS(Int(#"53"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"144"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"146"),, _:_WS(Int(#"145"),, _:_WS(Int(#"144"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"97"),, _:_WS(Int(#"2"),, _:_WS(Int(#"191"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"81"),, _:_WS(Int(#"128"),, _:_WS(Int(#"130"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"145"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"81"),, _:_WS(Int(#"128"),, _:_WS(Int(#"145"),, _:_WS(Int(#"3"),, _:_WS(Int(#"144"),, _:_WS(Int(#"243"),, _:_WS(Int(#"91"),, _:_WS(Int(#"97"),, _:_WS(Int(#"1"),, _:_WS(Int(#"96"),, _:_WS(Int(#"96"),, _:_WS(Int(#"4"),, _:_WS(Int(#"128"),, _:_WS(Int(#"54"),, _:_WS(Int(#"3"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"129"),, _:_WS(Int(#"16"),, _:_WS(Int(#"21"),, _:_WS(Int(#"97"),, _:_WS(Int(#"1"),, _:_WS(Int(#"52"),, _:_WS(Int(#"87"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"128"),, _:_WS(Int(#"253"),, _:_WS(Int(#"91"),, _:_WS(Int(#"129"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"128"),, _:_WS(Int(#"128"),, _:_WS(Int(#"53"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"144"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"146"),, _:_WS(Int(#"145"),, _:_WS(Int(#"144"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"97"),, _:_WS(Int(#"2"),, _:_WS(Int(#"215"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"81"),, _:_WS(Int(#"128"),, _:_WS(Int(#"130"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"145"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"81"),, _:_WS(Int(#"128"),, _:_WS(Int(#"145"),, _:_WS(Int(#"3"),, _:_WS(Int(#"144"),, _:_WS(Int(#"243"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"2"),, _:_WS(Int(#"84"),, _:_WS(Int(#"129"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"3"),, _:_WS(Int(#"84"),, _:_WS(Int(#"129"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"97"),, _:_WS(Int(#"1"),, _:_WS(Int(#"203"),, _:_WS(Int(#"96"),, _:_WS(Int(#"1"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"51"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"32"),, _:_WS(Int(#"84"),, _:_WS(Int(#"130"),, _:_WS(Int(#"97"),, _:_WS(Int(#"2"),, _:_WS(Int(#"239"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"1"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"51"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"32"),, _:_WS(Int(#"129"),, _:_WS(Int(#"144"),, _:_WS(Int(#"85"),, _:_WS(Int(#"80"),, _:_WS(Int(#"97"),, _:_WS(Int(#"2"),, _:_WS(Int(#"86"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"128"),, _:_WS(Int(#"51"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"32"),, _:_WS(Int(#"84"),, _:_WS(Int(#"130"),, _:_WS(Int(#"97"),, _:_WS(Int(#"2"),, _:_WS(Int(#"239"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"128"),, _:_WS(Int(#"51"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"115"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"255"),, _:_WS(Int(#"22"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"144"),, _:_WS(Int(#"129"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"1"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"32"),, _:_WS(Int(#"129"),, _:_WS(Int(#"144"),, _:_WS(Int(#"85"),, _:_WS(Int(#"80"),, _:_WS(Int(#"97"),, _:_WS(Int(#"2"),, _:_WS(Int(#"164"),, _:_WS(Int(#"96"),, _:_WS(Int(#"3"),, _:_WS(Int(#"84"),, _:_WS(Int(#"130"),, _:_WS(Int(#"97"),, _:_WS(Int(#"2"),, _:_WS(Int(#"239"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"3"),, _:_WS(Int(#"129"),, _:_WS(Int(#"144"),, _:_WS(Int(#"85"),, _:_WS(Int(#"80"),, _:_WS(Int(#"97"),, _:_WS(Int(#"2"),, _:_WS(Int(#"182"),, _:_WS(Int(#"96"),, _:_WS(Int(#"2"),, _:_WS(Int(#"84"),, _:_WS(Int(#"130"),, _:_WS(Int(#"97"),, _:_WS(Int(#"2"),, _:_WS(Int(#"239"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"2"),, _:_WS(Int(#"129"),, _:_WS(Int(#"144"),, _:_WS(Int(#"85"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"82"),, _:_WS(Int(#"128"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"32"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"145"),, _:_WS(Int(#"80"),, _:_WS(Int(#"144"),, _:_WS(Int(#"80"),, _:_WS(Int(#"84"),, _:_WS(Int(#"129"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"1"),, _:_WS(Int(#"96"),, _:_WS(Int(#"32"),, _:_WS(Int(#"82"),, _:_WS(Int(#"128"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"82"),, _:_WS(Int(#"96"),, _:_WS(Int(#"64"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"32"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"145"),, _:_WS(Int(#"80"),, _:_WS(Int(#"144"),, _:_WS(Int(#"80"),, _:_WS(Int(#"84"),, _:_WS(Int(#"129"),, _:_WS(Int(#"86"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"129"),, _:_WS(Int(#"131"),, _:_WS(Int(#"3"),, _:_WS(Int(#"144"),, _:_WS(Int(#"80"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"130"),, _:_WS(Int(#"19"),, _:_WS(Int(#"21"),, _:_WS(Int(#"128"),, _:_WS(Int(#"97"),, _:_WS(Int(#"3"),, _:_WS(Int(#"6"),, _:_WS(Int(#"87"),, _:_WS(Int(#"80"),, _:_WS(Int(#"130"),, _:_WS(Int(#"129"),, _:_WS(Int(#"17"),, _:_WS(Int(#"21"),, _:_WS(Int(#"91"),, _:_WS(Int(#"97"),, _:_WS(Int(#"3"),, _:_WS(Int(#"15"),, _:_WS(Int(#"87"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"128"),, _:_WS(Int(#"253"),, _:_WS(Int(#"91"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"130"),, _:_WS(Int(#"18"),, _:_WS(Int(#"21"),, _:_WS(Int(#"128"),, _:_WS(Int(#"97"),, _:_WS(Int(#"3"),, _:_WS(Int(#"31"),, _:_WS(Int(#"87"),, _:_WS(Int(#"80"),, _:_WS(Int(#"130"),, _:_WS(Int(#"129"),, _:_WS(Int(#"16"),, _:_WS(Int(#"21"),, _:_WS(Int(#"91"),, _:_WS(Int(#"97"),, _:_WS(Int(#"3"),, _:_WS(Int(#"40"),, _:_WS(Int(#"87"),, _:_WS(Int(#"96"),, _:_WS(Int(#"0"),, _:_WS(Int(#"128"),, _:_WS(Int(#"253"),, _:_WS(Int(#"91"),, _:_WS(Int(#"146"),, _:_WS(Int(#"145"),, _:_WS(Int(#"80"),, _:_WS(Int(#"80"),, _:_WS(Int(#"86"),, _:_WS(Int(#"254"),, _:_WS(Int(#"162"),, _:_WS(Int(#"101"),, _:_WS(Int(#"98"),, _:_WS(Int(#"122"),, _:_WS(Int(#"122"),, _:_WS(Int(#"114"),, _:_WS(Int(#"48"),, _:_WS(Int(#"88"),, _:_WS(Int(#"32"),, _:_WS(Int(#"15"),, _:_WS(Int(#"58"),, _:_WS(Int(#"38"),, _:_WS(Int(#"126"),, _:_WS(Int(#"205"),, _:_WS(Int(#"204"),, _:_WS(Int(#"170"),, _:_WS(Int(#"102"),, _:_WS(Int(#"16"),, _:_WS(Int(#"47"),, _:_WS(Int(#"52"),, _:_WS(Int(#"251"),, _:_WS(Int(#"239"),, _:_WS(Int(#"217"),, _:_WS(Int(#"245"),, _:_WS(Int(#"46"),, _:_WS(Int(#"125"),, _:_WS(Int(#"176"),, _:_WS(Int(#"173"),, _:_WS(Int(#"29"),, _:_WS(Int(#"168"),, _:_WS(Int(#"108"),, _:_WS(Int(#"107"),, _:_WS(Int(#"227"),, _:_WS(Int(#"147"),, _:_WS(Int(#"154"),, _:_WS(Int(#"137"),, _:_WS(Int(#"111"),, _:_WS(Int(#"253"),, _:_WS(Int(#"211"),, _:_WS(Int(#"52"),, _:_WS(Int(#"134"),, _:_WS(Int(#"100"),, _:_WS(Int(#"115"),, _:_WS(Int(#"111"),, _:_WS(Int(#"108"),, _:_WS(Int(#"99"),, _:_WS(Int(#"67"),, _:_WS(Int(#"0"),, _:_WS(Int(#"5"),, _:_WS(Int(#"9"),, _:_WS(Int(#"0"),, _:_WS(Int(#"50"),, .WordStack_EVM-TYPES(.KList))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))),, <storage>(_32_1822:Map),, <origStorage>(_33_1823:Map),, <nonce>(Nonce_Vat_1810:Int)) DotVar1_1896:Map),, <txOrder>(_59_1874:List),, <txPending>(_60_1875:List),, <messages>(_61_1840:Map))))
/\
ConjunctiveFormula(
init equalities:
_==K_(_<=Int_(ABI_x_1812:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(ABI_y_1813:Int,, Int(#"57896044618658097711785492504343953926634992332820282019728792003956564819967")),, Bool(#"true"))
_==K_(_<=Int_(ACCT_ID_1819:Int,, Int(#"1461501637330902918203684832716283019655932542975")),, Bool(#"true"))
_==K_(_<=Int_(ACCT_ID_balance_1882:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(CALLER_ID_1879:Int,, Int(#"1461501637330902918203684832716283019655932542975")),, Bool(#"true"))
_==K_(_<=Int_(ECADD_BAL_1893:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(ECMUL_BAL_1890:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(ECPAIRING_BAL_1895:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(ECREC_BAL_1814:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(ID_BAL_1811:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(Int(#"-57896044618658097711785492504343953926634992332820282019728792003956564819968"),, ABI_y_1813:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ABI_x_1812:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ACCT_ID_1819:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ACCT_ID_balance_1882:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, CALLER_ID_1879:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ECADD_BAL_1893:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ECMUL_BAL_1890:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ECPAIRING_BAL_1895:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ECREC_BAL_1814:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ID_BAL_1811:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, MODEXP_BAL_1884:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ORIGIN_ID_1891:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, RIP160_BAL_1816:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, SHA256_BAL_1817:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, TIME_1876:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, VCallValue_1808:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, VMemoryUsed_1806:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, _-Int_(ABI_x_1812:Int,, ABI_y_1813:Int)),, Bool(#"true"))
_==K_(_<=Int_(MODEXP_BAL_1884:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(ORIGIN_ID_1891:Int,, Int(#"1461501637330902918203684832716283019655932542975")),, Bool(#"true"))
_==K_(_<=Int_(RIP160_BAL_1816:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(SHA256_BAL_1817:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(TIME_1876:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(VCallDepth_1883:Int,, Int(#"1024")),, Bool(#"true"))
_==K_(_<=Int_(VCallValue_1808:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(VMemoryUsed_1806:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(_-Int_(ABI_x_1812:Int,, ABI_y_1813:Int),, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(sizeWordStackAux(WS_1885:WordStack,, Int(#"0")),, Int(#"1015")),, Bool(#"true"))
_==K_(_>=Int_(VGas_1877:Int,, Int(#"3000000")),, Bool(#"true"))
_==K_(_orBool_(_==K_(Int(#"0"),, ACCT_ID_1819:Int),, _andBool_(_<=Int_(Int(#"10"),, ACCT_ID_1819:Int),, _andBool_(_<=Int_(Int(#"0"),, ACCT_ID_1819:Int),, _<=Int_(ACCT_ID_1819:Int,, Int(#"1461501637330902918203684832716283019655932542975"))))),, Bool(#"true"))
new substitutions:
_==K_(CONTINUATION_1897:K,, #KSequence(#finishCodeDeposit___EVM(R__1_1987:Int,, R__2_1989:WordStack), R_DotVar1_1984:K))
new equalities:
_==K_(_>Int_(sizeWordStackAux(WS_1885:WordStack,, Int(#"3")),, Int(#"1024")),, Bool(#"true"))
)
SPEC ERROR: /Users/dbcurrin/dev/klab/examples/heal/out/specs/eeafb717d43bf1dd84c49c8f188576d5da03900a754defb4dae4c571136606d6.k Location(12,3,187,53)
==================================
Success execution paths: 0
Failed execution paths: 0
Paths in progress: 17
Longest path: 6 steps
Stats for each phase, time, used memory, implicit main GC time percentage:
Total : 149.427 s, 763 MB, gc: 1.496 %
JVM init : 0.047 s
Parsing : 146.338 s, 531 MB, gc: 1.527 %
Rewriter init : 0.722 s, 718 MB, gc: 0.000 %
Execution : 2.320 s, 763 MB, gc: 0.000 %
Init+Execution time: 3.042 s
query build time : 0.094 s, # 51
Z3 Regular rule implication time : 0.054 s, # 2
unknown : 2
Z3 Function rule implication time: 0.228 s, # 8
unknown : 8
Z3 Regular rule constraint time : 1.148 s, # 41
unknown : 40
timeouts: 1
Time and top-level event counts:
resolveFunctionAndAnywhere time : 0.581 s, # 2383
evaluateFunction time : 0.572 s, # 549
builtin evaluation : , # 56
function rule : , # 21
sort predicate : , # 4
no rule applicable : , # 465
no function rules : , # 3
applyAnywhereRules time : 0.000 s, # 1597
no anywhere rules : , # 1597
remaining time & # cached : 0.009 s, # 237
impliesSMT time : 0.312 s, # 10
Recursive event counts:
resolveFunctionAndAnywhere time : , # 24578
evaluateFunction time : , # 12997
builtin evaluation : , # 7780
function rule : , # 5124
sort predicate : , # 1
no rule applicable : , # 55
no function rules : , # 0
applyAnywhereRules time : , # 948
no anywhere rules : , # 948
# cached : , # 10633
Max memory : 9102 MB
==================================
[Error] Critical: Z3 crashed on input query:
(declare-sort WordStack)
(declare-sort KItem)
(declare-fun asByteStack (Int WordStack) WordStack)
(declare-fun asWord (WordStack) Int)
(declare-fun buf (Int Int) WordStack)
(declare-fun sizeWordStack (WordStack) Int)
(declare-fun _dotWS () WordStack)
(declare-fun andInt (Int Int) Int)
(declare-fun _plusWS_ (WordStack WordStack) WordStack)
(declare-fun _WS_ (Int WordStack) WordStack)
(declare-fun shlInt (Int Int) Int)
(declare-fun shrInt (Int Int) Int)
(declare-fun xorInt (Int Int) Int)
(declare-fun orInt (Int Int) Int)
(declare-fun chop (Int) Int)
(declare-fun smt_keccak (WordStack) Int)
(declare-fun smt_nthbyteof (Int Int Int) Int)
(declare-fun sizeWordStackAux (WordStack Int) Int)
(declare-fun notInt (Int) Int)
(assert (forall ((|R_I_316| Int)) (= (chop |R_I_316|) (mod |R_I_316| 115792089237316195423570985008687907853269984665640564039457584007913129639936))))
(assert (forall ((|R_WS_228| WordStack)) (= (>= (sizeWordStack |R_WS_228|) 0) true)))
(declare-fun |WS_1885| () WordStack)
(declare-fun |ACCT_ID_1819| () Int)
(declare-fun |CALLER_ID_1879| () Int)
(declare-fun |ORIGIN_ID_1891| () Int)
(declare-fun |TIME_1876| () Int)
(declare-fun |ACCT_ID_balance_1882| () Int)
(declare-fun |ECREC_BAL_1814| () Int)
(declare-fun |SHA256_BAL_1817| () Int)
(declare-fun |RIP160_BAL_1816| () Int)
(declare-fun |ID_BAL_1811| () Int)
(declare-fun |MODEXP_BAL_1884| () Int)
(declare-fun |ECADD_BAL_1893| () Int)
(declare-fun |ECMUL_BAL_1890| () Int)
(declare-fun |ECPAIRING_BAL_1895| () Int)
(declare-fun |VCallDepth_1883| () Int)
(declare-fun |VCallValue_1808| () Int)
(declare-fun |ABI_x_1812| () Int)
(declare-fun |ABI_y_1813| () Int)
(declare-fun |VMemoryUsed_1806| () Int)
(declare-fun |VGas_1877| () Int)
(declare-fun |_2057| () KItem)
(declare-fun |_2058| () KItem)
(assert (and
(= _2057 (smt_seq_elem _2058))
(= (> (sizeWordStackAux |WS_1885| 3) 1024) true)
(= (<= 0 |ACCT_ID_1819|) true)
(= (<= |ACCT_ID_1819| 1461501637330902918203684832716283019655932542975) true)
(= (or (= 0 |ACCT_ID_1819|) (and (<= 10 |ACCT_ID_1819|) (and (<= 0 |ACCT_ID_1819|) (<= |ACCT_ID_1819| 1461501637330902918203684832716283019655932542975)))) true)
(= (<= 0 |CALLER_ID_1879|) true)
(= (<= |CALLER_ID_1879| 1461501637330902918203684832716283019655932542975) true)
(= (<= 0 |ORIGIN_ID_1891|) true)
(= (<= |ORIGIN_ID_1891| 1461501637330902918203684832716283019655932542975) true)
(= (<= 0 |TIME_1876|) true)
(= (<= |TIME_1876| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |ACCT_ID_balance_1882|) true)
(= (<= |ACCT_ID_balance_1882| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |ECREC_BAL_1814|) true)
(= (<= |ECREC_BAL_1814| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |SHA256_BAL_1817|) true)
(= (<= |SHA256_BAL_1817| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |RIP160_BAL_1816|) true)
(= (<= |RIP160_BAL_1816| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |ID_BAL_1811|) true)
(= (<= |ID_BAL_1811| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |MODEXP_BAL_1884|) true)
(= (<= |MODEXP_BAL_1884| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |ECADD_BAL_1893|) true)
(= (<= |ECADD_BAL_1893| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |ECMUL_BAL_1890|) true)
(= (<= |ECMUL_BAL_1890| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |ECPAIRING_BAL_1895|) true)
(= (<= |ECPAIRING_BAL_1895| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= |VCallDepth_1883| 1024) true)
(= (<= 0 |VCallValue_1808|) true)
(= (<= |VCallValue_1808| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= 0 |ABI_x_1812|) true)
(= (<= |ABI_x_1812| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (<= -57896044618658097711785492504343953926634992332820282019728792003956564819968 |ABI_y_1813|) true)
(= (<= |ABI_y_1813| 57896044618658097711785492504343953926634992332820282019728792003956564819967) true)
(= (<= (sizeWordStackAux |WS_1885| 0) 1015) true)
(= (<= 0 |VMemoryUsed_1806|) true)
(= (<= |VMemoryUsed_1806| 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)
(= (>= |VGas_1877| 3000000) true)
(= (<= 0 (- |ABI_x_1812| |ABI_y_1813|)) true)
(= (<= (- |ABI_x_1812| |ABI_y_1813|) 115792089237316195423570985008687907853269984665640564039457584007913129639935) true)))
result:
(error "line 109 column 29: unknown function/constant smt_seq_elem")
unknown
while checking satisfiability for:
ConjunctiveFormula(
substitutions:
_==K_(CONTINUATION_1897:K,, #KSequence(#finishCodeDeposit___EVM(R__1_1987:Int,, R__2_1989:WordStack), R_DotVar1_1984:K))
_==K_(R_DotVar1:K,, #KSequence(#popWorldState_EVM(.KList), Int(#"0"), #push_EVM(.KList), R_DotVar1_1984:K))
_==K_(R_DotVar4:List,, List:range(VCallStack_1807:List,, Int(#"1"),, Int(#"0")))
_==K_(R__0:List,, VCallStack_1807:List)
equalities:
_==K_(List:get(VCallStack_1807:List,, Int(#"0")),, ListItem(<callState>-fragment(R__1:K,, R__2:K,, R__3:K,, R__4:K,, R__5:K,, R__6:K,, R__7:K,, R__8:K,, R__9:K,, R__10:K,, R__11:K,, R__12:K,, R__13:K,, R__14:K)))
_==K_(_<=Int_(ABI_x_1812:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(ABI_y_1813:Int,, Int(#"57896044618658097711785492504343953926634992332820282019728792003956564819967")),, Bool(#"true"))
_==K_(_<=Int_(ACCT_ID_1819:Int,, Int(#"1461501637330902918203684832716283019655932542975")),, Bool(#"true"))
_==K_(_<=Int_(ACCT_ID_balance_1882:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(CALLER_ID_1879:Int,, Int(#"1461501637330902918203684832716283019655932542975")),, Bool(#"true"))
_==K_(_<=Int_(ECADD_BAL_1893:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(ECMUL_BAL_1890:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(ECPAIRING_BAL_1895:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(ECREC_BAL_1814:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(ID_BAL_1811:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(Int(#"-57896044618658097711785492504343953926634992332820282019728792003956564819968"),, ABI_y_1813:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ABI_x_1812:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ACCT_ID_1819:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ACCT_ID_balance_1882:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, CALLER_ID_1879:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ECADD_BAL_1893:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ECMUL_BAL_1890:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ECPAIRING_BAL_1895:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ECREC_BAL_1814:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ID_BAL_1811:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, MODEXP_BAL_1884:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, ORIGIN_ID_1891:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, RIP160_BAL_1816:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, SHA256_BAL_1817:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, TIME_1876:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, VCallValue_1808:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, VMemoryUsed_1806:Int),, Bool(#"true"))
_==K_(_<=Int_(Int(#"0"),, _-Int_(ABI_x_1812:Int,, ABI_y_1813:Int)),, Bool(#"true"))
_==K_(_<=Int_(MODEXP_BAL_1884:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(ORIGIN_ID_1891:Int,, Int(#"1461501637330902918203684832716283019655932542975")),, Bool(#"true"))
_==K_(_<=Int_(RIP160_BAL_1816:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(SHA256_BAL_1817:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(TIME_1876:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(VCallDepth_1883:Int,, Int(#"1024")),, Bool(#"true"))
_==K_(_<=Int_(VCallValue_1808:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(VMemoryUsed_1806:Int,, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(_-Int_(ABI_x_1812:Int,, ABI_y_1813:Int),, Int(#"115792089237316195423570985008687907853269984665640564039457584007913129639935")),, Bool(#"true"))
_==K_(_<=Int_(sizeWordStackAux(WS_1885:WordStack,, Int(#"0")),, Int(#"1015")),, Bool(#"true"))
_==K_(_>=Int_(VGas_1877:Int,, Int(#"3000000")),, Bool(#"true"))
_==K_(_>Int_(sizeWordStackAux(WS_1885:WordStack,, Int(#"3")),, Int(#"1024")),, Bool(#"true"))
_==K_(_orBool_(_==K_(Int(#"0"),, ACCT_ID_1819:Int),, _andBool_(_<=Int_(Int(#"10"),, ACCT_ID_1819:Int),, _andBool_(_<=Int_(Int(#"0"),, ACCT_ID_1819:Int),, _<=Int_(ACCT_ID_1819:Int,, Int(#"1461501637330902918203684832716283019655932542975"))))),, Bool(#"true"))
)
[Warning] Critical: Found klabel keccaktIntList not defined in any production.
Note: this warning will become an error in subsequent releases.
Source(/Users/dbcurrin/dev/klab/examples/heal/out/rules.k)
Location(221,10,221,27)
[Warning] Critical: Found variable D on right hand side of rule, not bound on left hand side. Did you mean "?D"?
Note: this warning will become an error in subsequent releases.
Source(/Users/dbcurrin/dev/klab/examples/heal/out/rules.k)
Location(379,24,379,25)
[Warning] Critical: Found variable D on right hand side of rule, not bound on left hand side. Did you mean "?D"?
Note: this warning will become an error in subsequent releases.
Source(/Users/dbcurrin/dev/klab/examples/heal/out/rules.k)
Location(383,24,383,25)
[Warning] Critical: Found variable D on right hand side of rule, not bound on left hand side. Did you mean "?D"?
Note: this warning will become an error in subsequent releases.
Source(/Users/dbcurrin/dev/klab/examples/heal/out/rules.k)
Location(387,24,387,25)
[Warning] Critical: Found variable D on right hand side of rule, not bound on left hand side. Did you mean "?D"?
Note: this warning will become an error in subsequent releases.
Source(/Users/dbcurrin/dev/klab/examples/heal/out/rules.k)
Location(391,24,391,25)
[Warning] Critical: Found variable VLog on right hand side of rule, not bound on left hand side. Did you mean "?VLog"?
Note: this warning will become an error in subsequent releases.
Source(/Users/dbcurrin/dev/klab/examples/heal/out/specs/eeafb717d43bf1dd84c49c8f188576d5da03900a754defb4dae4c571136606d6.k)
Location(41,20,41,24)
[Warning] Critical: Found variable VRefund on right hand side of rule, not bound on left hand side. Did you mean "?VRefund"?
Note: this warning will become an error in subsequent releases.
Source(/Users/dbcurrin/dev/klab/examples/heal/out/specs/eeafb717d43bf1dd84c49c8f188576d5da03900a754defb4dae4c571136606d6.k)
Location(42,23,42,30)
[Warning] Critical: Found variable _ on right hand side of rule, not bound on left hand side. Did you mean "?_"?
Note: this warning will become an error in subsequent releases.
Source(/Users/dbcurrin/dev/klab/examples/heal/out/specs/eeafb717d43bf1dd84c49c8f188576d5da03900a754defb4dae4c571136606d6.k)
Location(19,25,19,26)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment