diff --git a/tests/specs/mcd-structured/flapper-yank-pass-rough-spec.json b/tests/specs/mcd-structured/flapper-yank-pass-rough-spec.json
deleted file mode 100644
index 03a5ef66e1..0000000000
--- a/tests/specs/mcd-structured/flapper-yank-pass-rough-spec.json
+++ /dev/null
@@ -1 +0,0 @@
-{"moduleList": {"node": "KFlatModuleList", "mainModule": "FLAPPER-YANK-PASS-ROUGH-SPEC", "term": [{"node": "KFlatModule", "name": "FLAPPER-YANK-PASS-ROUGH-SPEC", "localSentences": [{"node": "KClaim", "body": {"node": "KApply", "label": {"node": "KLabel", "name": "<generatedTop>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<kevm>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<k>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KSequence", "items": [{"node": "KApply", "label": {"node": "KLabel", "name": "execute", "params": []}, "args": [], "arity": 0, "variable": false}, {"node": "KVariable", "name": "CONTINUATION", "sort": {"node": "KSort", "name": "K"}}], "arity": 2}, "rhs": {"node": "KSequence", "items": [{"node": "KApply", "label": {"node": "KLabel", "name": "halt", "params": []}, "args": [], "arity": 0, "variable": false}, {"node": "KVariable", "name": "CONTINUATION", "sort": {"node": "KSort", "name": "K"}}], "arity": 2}}], "arity": 1, "variable": false}, {"node": "KVariable", "name": "_DotVar1", "sort": {"node": "KSort", "name": "ExitCodeCell"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "<mode>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "NORMAL", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<schedule>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "ISTANBUL_EVM", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<useGas>", "params": []}, "args": [{"node": "KToken", "token": "true", "sort": {"node": "KSort", "name": "Bool"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<ethereum>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<evm>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<output>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": ".Bytes_BYTES-HOOKED_Bytes", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<statusCode>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KVariable", "name": "_Gen0", "sort": {"node": "KSort", "name": "StatusCode"}}, "rhs": {"node": "KApply", "label": {"node": "KLabel", "name": "EVMC_SUCCESS_NETWORK_EndStatusCode", "params": []}, "args": [], "arity": 0, "variable": false}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<callStack>", "params": []}, "args": [{"node": "KVariable", "name": "_VCallStack", "sort": {"node": "KSort", "name": "List"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<interimStates>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen1", "sort": {"node": "KSort", "name": "List"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<touchedAccounts>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KVariable", "name": "_Gen2", "sort": {"node": "KSort", "name": "Set"}}, "rhs": {"node": "KVariable", "name": "?_Gen3", "sort": {"node": "KSort", "name": "Set"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<callState>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<program>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "parseByteStack", "params": []}, "args": [{"node": "KToken", "token": "\"0x608060405234801561001057600080fd5b50600436106101165760003560e01c8063957aa58c116100a2578063c959c42b11610071578063c959c42b14610479578063ca40c419146104a7578063cfc4af55146104f3578063cfdd330214610521578063fc7b6aee1461053f57610116565b8063957aa58c146103915780639c52a7f1146103af578063a2f91af2146103f3578063bf353dbb1461042157610116565b80634b43ed12116100e95780634b43ed12146102755780634e8b1dd5146102b757806365fae35e146102e55780637bd2bea7146103295780637d780d821461037357610116565b806326e027f11461011b57806329ae81141461014957806336569e77146101815780634423c5f1146101cb575b600080fd5b6101476004803603602081101561013157600080fd5b810190808035906020019092919050505061056d565b005b61017f6004803603604081101561015f57600080fd5b8101908080359060200190929190803590602001909291905050506108b4565b005b610189610ae7565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b6101f7600480360360208110156101e157600080fd5b8101908080359060200190929190505050610b0d565b604051808681526020018581526020018473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018365ffffffffffff1665ffffffffffff1681526020018265ffffffffffff1665ffffffffffff1681526020019550505050505060405180910390f35b6102b56004803603606081101561028b57600080fd5b81019080803590602001909291908035906020019092919080359060200190929190505050610b87565b005b6102bf6113d1565b604051808265ffffffffffff1665ffffffffffff16815260200191505060405180910390f35b610327600480360360208110156102fb57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291905050506113e9565b005b610331611517565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b61037b61153d565b6040518082815260200191505060405180910390f35b610399611543565b6040518082815260200191505060405180910390f35b6103f1600480360360208110156103c557600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050611549565b005b61041f6004803603602081101561040957600080fd5b8101908080359060200190929190505050611677565b005b6104636004803603602081101561043757600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919050505061185e565b6040518082815260200191505060405180910390f35b6104a56004803603602081101561048f57600080fd5b8101908080359060200190929190505050611876565b005b6104dd600480360360408110156104bd57600080fd5b810190808035906020019092919080359060200190929190505050611cd7565b6040518082815260200191505060405180910390f35b6104fb6120d0565b604051808265ffffffffffff1665ffffffffffff16815260200191505060405180910390f35b6105296120e8565b6040518082815260200191505060405180910390f35b61056b6004803603602081101561055557600080fd5b81019080803590602001909291905050506120ee565b005b6000600754146105e5576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f466c61707065722f7374696c6c2d6c697665000000000000000000000000000081525060200191505060405180910390fd5b600073ffffffffffffffffffffffffffffffffffffffff166001600083815260200190815260200160002060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1614156106be576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260138152602001807f466c61707065722f6775792d6e6f742d7365740000000000000000000000000081525060200191505060405180910390fd5b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b306001600085815260200190815260200160002060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1660016000868152602001908152602001600020600001546040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b1580156107e757600080fd5b505af11580156107fb573d6000803e3d6000fd5b505050506001600082815260200190815260200160002060008082016000905560018201600090556002820160006101000a81549073ffffffffffffffffffffffffffffffffffffffff02191690556002820160146101000a81549065ffffffffffff021916905560028201601a6101000a81549065ffffffffffff021916905550505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414610968576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260168152602001807f466c61707065722f6e6f742d617574686f72697a65640000000000000000000081525060200191505060405180910390fd5b7f626567000000000000000000000000000000000000000000000000000000000082141561099c5780600481905550610ab0565b7f74746c00000000000000000000000000000000000000000000000000000000008214156109ee5780600560006101000a81548165ffffffffffff021916908365ffffffffffff160217905550610aaf565b7f7461750000000000000000000000000000000000000000000000000000000000821415610a405780600560066101000a81548165ffffffffffff021916908365ffffffffffff160217905550610aae565b6040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601f8152602001807f466c61707065722f66696c652d756e7265636f676e697a65642d706172616d0081525060200191505060405180910390fd5b5b5b5961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a4505050565b600260009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b60016020528060005260406000206000915090508060000154908060010154908060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff16908060020160149054906101000a900465ffffffffffff169080600201601a9054906101000a900465ffffffffffff16905085565b600160075414610bff576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260108152602001807f466c61707065722f6e6f742d6c6976650000000000000000000000000000000081525060200191505060405180910390fd5b600073ffffffffffffffffffffffffffffffffffffffff166001600085815260200190815260200160002060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff161415610cd8576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260138152602001807f466c61707065722f6775792d6e6f742d7365740000000000000000000000000081525060200191505060405180910390fd5b426001600085815260200190815260200160002060020160149054906101000a900465ffffffffffff1665ffffffffffff161180610d46575060006001600085815260200190815260200160002060020160149054906101000a900465ffffffffffff1665ffffffffffff16145b610db8576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601c8152602001807f466c61707065722f616c72656164792d66696e69736865642d7469630000000081525060200191505060405180910390fd5b4260016000858152602001908152602001600020600201601a9054906101000a900465ffffffffffff1665ffffffffffff1611610e5d576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601c8152602001807f466c61707065722f616c72656164792d66696e69736865642d656e640000000081525060200191505060405180910390fd5b60016000848152602001908152602001600020600101548214610ee8576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260188152602001807f466c61707065722f6c6f742d6e6f742d6d61746368696e67000000000000000081525060200191505060405180910390fd5b60016000848152602001908152602001600020600001548111610f73576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260168152602001807f466c61707065722f6269642d6e6f742d6869676865720000000000000000000081525060200191505060405180910390fd5b610f9560045460016000868152602001908152602001600020600001546122c5565b610fa782670de0b6b3a76400006122c5565b101561101b576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601d8152602001807f466c61707065722f696e73756666696369656e742d696e63726561736500000081525060200191505060405180910390fd5b6001600084815260200190815260200160002060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff161461121b57600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b336001600087815260200190815260200160002060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1660016000888152602001908152602001600020600001546040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b1580156111ad57600080fd5b505af11580156111c1573d6000803e3d6000fd5b50505050336001600085815260200190815260200160002060020160006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff1602179055505b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b3330600160008881526020019081526020016000206000015485036040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b15801561131057600080fd5b505af1158015611324573d6000803e3d6000fd5b5050505080600160008581526020019081526020016000206000018190555061136142600560009054906101000a900465ffffffffffff166122f1565b6001600085815260200190815260200160002060020160146101000a81548165ffffffffffff021916908365ffffffffffff1602179055505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a450505050565b600560009054906101000a900465ffffffffffff1681565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541461149d576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260168152602001807f466c61707065722f6e6f742d617574686f72697a65640000000000000000000081525060200191505060405180910390fd5b60016000808373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b60045481565b60075481565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054146115fd576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260168152602001807f466c61707065722f6e6f742d617574686f72697a65640000000000000000000081525060200191505060405180910390fd5b60008060008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541461172b576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260168152602001807f466c61707065722f6e6f742d617574686f72697a65640000000000000000000081525060200191505060405180910390fd5b6000600781905550600260009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b3033846040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b15801561181057600080fd5b505af1158015611824573d6000803e3d6000fd5b505050505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b60006020528060005260406000206000915090505481565b6001600754146118ee576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260108152602001807f466c61707065722f6e6f742d6c6976650000000000000000000000000000000081525060200191505060405180910390fd5b60006001600083815260200190815260200160002060020160149054906101000a900465ffffffffffff1665ffffffffffff16141580156119985750426001600083815260200190815260200160002060020160149054906101000a900465ffffffffffff1665ffffffffffff16108061199757504260016000838152602001908152602001600020600201601a9054906101000a900465ffffffffffff1665ffffffffffff16105b5b611a0a576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f466c61707065722f6e6f742d66696e697368656400000000000000000000000081525060200191505060405180910390fd5b600260009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b306001600085815260200190815260200160002060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1660016000868152602001908152602001600020600101546040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b158015611b3357600080fd5b505af1158015611b47573d6000803e3d6000fd5b50505050600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16639dc29fac3060016000858152602001908152602001600020600001546040518363ffffffff1660e01b8152600401808373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200182815260200192505050600060405180830381600087803b158015611c0a57600080fd5b505af1158015611c1e573d6000803e3d6000fd5b505050506001600082815260200190815260200160002060008082016000905560018201600090556002820160006101000a81549073ffffffffffffffffffffffffffffffffffffffff02191690556002820160146101000a81549065ffffffffffff021916905560028201601a6101000a81549065ffffffffffff021916905550505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b600060016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414611d8d576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260168152602001807f466c61707065722f6e6f742d617574686f72697a65640000000000000000000081525060200191505060405180910390fd5b600160075414611e05576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260108152602001807f466c61707065722f6e6f742d6c6976650000000000000000000000000000000081525060200191505060405180910390fd5b7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff60065410611e9c576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260108152602001807f466c61707065722f6f766572666c6f770000000000000000000000000000000081525060200191505060405180910390fd5b6006600081546001019190508190559050816001600083815260200190815260200160002060000181905550826001600083815260200190815260200160002060010181905550336001600083815260200190815260200160002060020160006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff160217905550611f5642600560069054906101000a900465ffffffffffff166122f1565b60016000838152602001908152602001600020600201601a6101000a81548165ffffffffffff021916908365ffffffffffff160217905550600260009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b3330866040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b15801561206b57600080fd5b505af115801561207f573d6000803e3d6000fd5b505050507fe6dde59cbc017becba89714a037778d234a84ce7f0a137487142a007e580d60981848460405180848152602001838152602001828152602001935050505060405180910390a192915050565b600560069054906101000a900465ffffffffffff1681565b60065481565b4260016000838152602001908152602001600020600201601a9054906101000a900465ffffffffffff1665ffffffffffff1610612193576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f466c61707065722f6e6f742d66696e697368656400000000000000000000000081525060200191505060405180910390fd5b60006001600083815260200190815260200160002060020160149054906101000a900465ffffffffffff1665ffffffffffff1614612239576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601a8152602001807f466c61707065722f6269642d616c72656164792d706c6163656400000000000081525060200191505060405180910390fd5b61225742600560069054906101000a900465ffffffffffff166122f1565b60016000838152602001908152602001600020600201601a6101000a81548165ffffffffffff021916908365ffffffffffff1602179055505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b6000808214806122e257508282838502925082816122df57fe5b04145b6122eb57600080fd5b92915050565b60008265ffffffffffff1682840191508165ffffffffffff16101561231557600080fd5b9291505056fea265627a7a723158201acd0496ca3432003bac40639b3808573f9831f884ae4dc91d004d0deff68a7364736f6c634300050c0032\"", "sort": {"node": "KSort", "name": "String"}}], "arity": 1, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<jumpDests>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "computeValidJumpDests", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "parseByteStack", "params": []}, "args": [{"node": "KToken", "token": "\"0x608060405234801561001057600080fd5b50600436106101165760003560e01c8063957aa58c116100a2578063c959c42b11610071578063c959c42b14610479578063ca40c419146104a7578063cfc4af55146104f3578063cfdd330214610521578063fc7b6aee1461053f57610116565b8063957aa58c146103915780639c52a7f1146103af578063a2f91af2146103f3578063bf353dbb1461042157610116565b80634b43ed12116100e95780634b43ed12146102755780634e8b1dd5146102b757806365fae35e146102e55780637bd2bea7146103295780637d780d821461037357610116565b806326e027f11461011b57806329ae81141461014957806336569e77146101815780634423c5f1146101cb575b600080fd5b6101476004803603602081101561013157600080fd5b810190808035906020019092919050505061056d565b005b61017f6004803603604081101561015f57600080fd5b8101908080359060200190929190803590602001909291905050506108b4565b005b610189610ae7565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b6101f7600480360360208110156101e157600080fd5b8101908080359060200190929190505050610b0d565b604051808681526020018581526020018473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018365ffffffffffff1665ffffffffffff1681526020018265ffffffffffff1665ffffffffffff1681526020019550505050505060405180910390f35b6102b56004803603606081101561028b57600080fd5b81019080803590602001909291908035906020019092919080359060200190929190505050610b87565b005b6102bf6113d1565b604051808265ffffffffffff1665ffffffffffff16815260200191505060405180910390f35b610327600480360360208110156102fb57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291905050506113e9565b005b610331611517565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b61037b61153d565b6040518082815260200191505060405180910390f35b610399611543565b6040518082815260200191505060405180910390f35b6103f1600480360360208110156103c557600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050611549565b005b61041f6004803603602081101561040957600080fd5b8101908080359060200190929190505050611677565b005b6104636004803603602081101561043757600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919050505061185e565b6040518082815260200191505060405180910390f35b6104a56004803603602081101561048f57600080fd5b8101908080359060200190929190505050611876565b005b6104dd600480360360408110156104bd57600080fd5b810190808035906020019092919080359060200190929190505050611cd7565b6040518082815260200191505060405180910390f35b6104fb6120d0565b604051808265ffffffffffff1665ffffffffffff16815260200191505060405180910390f35b6105296120e8565b6040518082815260200191505060405180910390f35b61056b6004803603602081101561055557600080fd5b81019080803590602001909291905050506120ee565b005b6000600754146105e5576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f466c61707065722f7374696c6c2d6c697665000000000000000000000000000081525060200191505060405180910390fd5b600073ffffffffffffffffffffffffffffffffffffffff166001600083815260200190815260200160002060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1614156106be576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260138152602001807f466c61707065722f6775792d6e6f742d7365740000000000000000000000000081525060200191505060405180910390fd5b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b306001600085815260200190815260200160002060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1660016000868152602001908152602001600020600001546040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b1580156107e757600080fd5b505af11580156107fb573d6000803e3d6000fd5b505050506001600082815260200190815260200160002060008082016000905560018201600090556002820160006101000a81549073ffffffffffffffffffffffffffffffffffffffff02191690556002820160146101000a81549065ffffffffffff021916905560028201601a6101000a81549065ffffffffffff021916905550505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414610968576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260168152602001807f466c61707065722f6e6f742d617574686f72697a65640000000000000000000081525060200191505060405180910390fd5b7f626567000000000000000000000000000000000000000000000000000000000082141561099c5780600481905550610ab0565b7f74746c00000000000000000000000000000000000000000000000000000000008214156109ee5780600560006101000a81548165ffffffffffff021916908365ffffffffffff160217905550610aaf565b7f7461750000000000000000000000000000000000000000000000000000000000821415610a405780600560066101000a81548165ffffffffffff021916908365ffffffffffff160217905550610aae565b6040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601f8152602001807f466c61707065722f66696c652d756e7265636f676e697a65642d706172616d0081525060200191505060405180910390fd5b5b5b5961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a4505050565b600260009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b60016020528060005260406000206000915090508060000154908060010154908060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff16908060020160149054906101000a900465ffffffffffff169080600201601a9054906101000a900465ffffffffffff16905085565b600160075414610bff576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260108152602001807f466c61707065722f6e6f742d6c6976650000000000000000000000000000000081525060200191505060405180910390fd5b600073ffffffffffffffffffffffffffffffffffffffff166001600085815260200190815260200160002060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff161415610cd8576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260138152602001807f466c61707065722f6775792d6e6f742d7365740000000000000000000000000081525060200191505060405180910390fd5b426001600085815260200190815260200160002060020160149054906101000a900465ffffffffffff1665ffffffffffff161180610d46575060006001600085815260200190815260200160002060020160149054906101000a900465ffffffffffff1665ffffffffffff16145b610db8576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601c8152602001807f466c61707065722f616c72656164792d66696e69736865642d7469630000000081525060200191505060405180910390fd5b4260016000858152602001908152602001600020600201601a9054906101000a900465ffffffffffff1665ffffffffffff1611610e5d576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601c8152602001807f466c61707065722f616c72656164792d66696e69736865642d656e640000000081525060200191505060405180910390fd5b60016000848152602001908152602001600020600101548214610ee8576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260188152602001807f466c61707065722f6c6f742d6e6f742d6d61746368696e67000000000000000081525060200191505060405180910390fd5b60016000848152602001908152602001600020600001548111610f73576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260168152602001807f466c61707065722f6269642d6e6f742d6869676865720000000000000000000081525060200191505060405180910390fd5b610f9560045460016000868152602001908152602001600020600001546122c5565b610fa782670de0b6b3a76400006122c5565b101561101b576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601d8152602001807f466c61707065722f696e73756666696369656e742d696e63726561736500000081525060200191505060405180910390fd5b6001600084815260200190815260200160002060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff161461121b57600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b336001600087815260200190815260200160002060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1660016000888152602001908152602001600020600001546040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b1580156111ad57600080fd5b505af11580156111c1573d6000803e3d6000fd5b50505050336001600085815260200190815260200160002060020160006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff1602179055505b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b3330600160008881526020019081526020016000206000015485036040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b15801561131057600080fd5b505af1158015611324573d6000803e3d6000fd5b5050505080600160008581526020019081526020016000206000018190555061136142600560009054906101000a900465ffffffffffff166122f1565b6001600085815260200190815260200160002060020160146101000a81548165ffffffffffff021916908365ffffffffffff1602179055505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a450505050565b600560009054906101000a900465ffffffffffff1681565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541461149d576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260168152602001807f466c61707065722f6e6f742d617574686f72697a65640000000000000000000081525060200191505060405180910390fd5b60016000808373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b60045481565b60075481565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054146115fd576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260168152602001807f466c61707065722f6e6f742d617574686f72697a65640000000000000000000081525060200191505060405180910390fd5b60008060008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541461172b576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260168152602001807f466c61707065722f6e6f742d617574686f72697a65640000000000000000000081525060200191505060405180910390fd5b6000600781905550600260009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b3033846040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b15801561181057600080fd5b505af1158015611824573d6000803e3d6000fd5b505050505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b60006020528060005260406000206000915090505481565b6001600754146118ee576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260108152602001807f466c61707065722f6e6f742d6c6976650000000000000000000000000000000081525060200191505060405180910390fd5b60006001600083815260200190815260200160002060020160149054906101000a900465ffffffffffff1665ffffffffffff16141580156119985750426001600083815260200190815260200160002060020160149054906101000a900465ffffffffffff1665ffffffffffff16108061199757504260016000838152602001908152602001600020600201601a9054906101000a900465ffffffffffff1665ffffffffffff16105b5b611a0a576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f466c61707065722f6e6f742d66696e697368656400000000000000000000000081525060200191505060405180910390fd5b600260009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b306001600085815260200190815260200160002060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1660016000868152602001908152602001600020600101546040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b158015611b3357600080fd5b505af1158015611b47573d6000803e3d6000fd5b50505050600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16639dc29fac3060016000858152602001908152602001600020600001546040518363ffffffff1660e01b8152600401808373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200182815260200192505050600060405180830381600087803b158015611c0a57600080fd5b505af1158015611c1e573d6000803e3d6000fd5b505050506001600082815260200190815260200160002060008082016000905560018201600090556002820160006101000a81549073ffffffffffffffffffffffffffffffffffffffff02191690556002820160146101000a81549065ffffffffffff021916905560028201601a6101000a81549065ffffffffffff021916905550505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b600060016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414611d8d576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260168152602001807f466c61707065722f6e6f742d617574686f72697a65640000000000000000000081525060200191505060405180910390fd5b600160075414611e05576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260108152602001807f466c61707065722f6e6f742d6c6976650000000000000000000000000000000081525060200191505060405180910390fd5b7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff60065410611e9c576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260108152602001807f466c61707065722f6f766572666c6f770000000000000000000000000000000081525060200191505060405180910390fd5b6006600081546001019190508190559050816001600083815260200190815260200160002060000181905550826001600083815260200190815260200160002060010181905550336001600083815260200190815260200160002060020160006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff160217905550611f5642600560069054906101000a900465ffffffffffff166122f1565b60016000838152602001908152602001600020600201601a6101000a81548165ffffffffffff021916908365ffffffffffff160217905550600260009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b3330866040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b15801561206b57600080fd5b505af115801561207f573d6000803e3d6000fd5b505050507fe6dde59cbc017becba89714a037778d234a84ce7f0a137487142a007e580d60981848460405180848152602001838152602001828152602001935050505060405180910390a192915050565b600560069054906101000a900465ffffffffffff1681565b60065481565b4260016000838152602001908152602001600020600201601a9054906101000a900465ffffffffffff1665ffffffffffff1610612193576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f466c61707065722f6e6f742d66696e697368656400000000000000000000000081525060200191505060405180910390fd5b60006001600083815260200190815260200160002060020160149054906101000a900465ffffffffffff1665ffffffffffff1614612239576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601a8152602001807f466c61707065722f6269642d616c72656164792d706c6163656400000000000081525060200191505060405180910390fd5b61225742600560069054906101000a900465ffffffffffff166122f1565b60016000838152602001908152602001600020600201601a6101000a81548165ffffffffffff021916908365ffffffffffff1602179055505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b6000808214806122e257508282838502925082816122df57fe5b04145b6122eb57600080fd5b92915050565b60008265ffffffffffff1682840191508165ffffffffffff16101561231557600080fd5b9291505056fea265627a7a723158201acd0496ca3432003bac40639b3808573f9831f884ae4dc91d004d0deff68a7364736f6c634300050c0032\"", "sort": {"node": "KSort", "name": "String"}}], "arity": 1, "variable": false}], "arity": 1, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<id>", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<caller>", "params": []}, "args": [{"node": "KVariable", "name": "CALLER_ID", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<callData>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KApply", "label": {"node": "KLabel", "name": "_+Bytes__BYTES-HOOKED_Bytes_Bytes_Bytes", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "abiCallData", "params": []}, "args": [{"node": "KToken", "token": "\"yank\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "typedArgs", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "abi_type_uint256", "params": []}, "args": [{"node": "KVariable", "name": "ABI_id", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"typedArgs\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KVariable", "name": "CD", "sort": {"node": "KSort", "name": "Bytes"}}], "arity": 2, "variable": false}, "rhs": {"node": "KVariable", "name": "?_Gen4", "sort": {"node": "KSort", "name": "Bytes"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<callValue>", "params": []}, "args": [{"node": "KVariable", "name": "VCallValue", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<wordStack>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KApply", "label": {"node": "KLabel", "name": ".WordStack_EVM-TYPES_WordStack", "params": []}, "args": [], "arity": 0, "variable": false}, "rhs": {"node": "KVariable", "name": "?_Gen5", "sort": {"node": "KSort", "name": "WordStack"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<localMem>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KApply", "label": {"node": "KLabel", "name": ".Bytes_BYTES-HOOKED_Bytes", "params": []}, "args": [], "arity": 0, "variable": false}, "rhs": {"node": "KVariable", "name": "?_Gen6", "sort": {"node": "KSort", "name": "Bytes"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<pc>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, "rhs": {"node": "KVariable", "name": "?_Gen7", "sort": {"node": "KSort", "name": "Int"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<gas>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KApply", "label": {"node": "KLabel", "name": "infGas", "params": []}, "args": [{"node": "KVariable", "name": "VGas", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, "rhs": {"node": "KVariable", "name": "?_Gen8", "sort": {"node": "KSort", "name": "Gas"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<memoryUsed>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, "rhs": {"node": "KVariable", "name": "?_Gen9", "sort": {"node": "KSort", "name": "Int"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<callGas>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KVariable", "name": "_Gen10", "sort": {"node": "KSort", "name": "Gas"}}, "rhs": {"node": "KVariable", "name": "?_Gen11", "sort": {"node": "KSort", "name": "Gas"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<static>", "params": []}, "args": [{"node": "KToken", "token": "false", "sort": {"node": "KSort", "name": "Bool"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<callDepth>", "params": []}, "args": [{"node": "KVariable", "name": "VCallDepth", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}], "arity": 14, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<versionedHashes>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen12", "sort": {"node": "KSort", "name": "List"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<substate>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<selfDestruct>", "params": []}, "args": [{"node": "KVariable", "name": "_VSelfDestruct", "sort": {"node": "KSort", "name": "Set"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<log>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KVariable", "name": "_Gen13", "sort": {"node": "KSort", "name": "List"}}, "rhs": {"node": "KVariable", "name": "?_Gen14", "sort": {"node": "KSort", "name": "List"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<refund>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KVariable", "name": "_Vrefund", "sort": {"node": "KSort", "name": "Int"}}, "rhs": {"node": "KVariable", "name": "?_Gen15", "sort": {"node": "KSort", "name": "Int"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<accessedAccounts>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KVariable", "name": "_Gen16", "sort": {"node": "KSort", "name": "Set"}}, "rhs": {"node": "KVariable", "name": "?_Gen17", "sort": {"node": "KSort", "name": "Set"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<accessedStorage>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KVariable", "name": "_Gen18", "sort": {"node": "KSort", "name": "Map"}}, "rhs": {"node": "KVariable", "name": "?_Gen19", "sort": {"node": "KSort", "name": "Map"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<createdAccounts>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KVariable", "name": "_Gen20", "sort": {"node": "KSort", "name": "Set"}}, "rhs": {"node": "KVariable", "name": "?_Gen21", "sort": {"node": "KSort", "name": "Set"}}}], "arity": 1, "variable": false}], "arity": 6, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<gasPrice>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen22", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<origin>", "params": []}, "args": [{"node": "KVariable", "name": "ORIGIN_ID", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<blockhashes>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen23", "sort": {"node": "KSort", "name": "List"}}], "arity": 1, "variable": false}, {"node": "KVariable", "name": "_Gen3", "sort": {"node": "KSort", "name": "PreviousExcessBlobGasCell"}}, {"node": "KVariable", "name": "_Gen4", "sort": {"node": "KSort", "name": "PreviousBlobGasUsedCell"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "<block>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<previousHash>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen24", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<ommersHash>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen25", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<coinbase>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen26", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<stateRoot>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen27", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<transactionsRoot>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen28", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<receiptsRoot>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen29", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<logsBloom>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen30", "sort": {"node": "KSort", "name": "Bytes"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<difficulty>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen31", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<number>", "params": []}, "args": [{"node": "KVariable", "name": "_BLOCK_NUMBER", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<gasLimit>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen32", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<gasUsed>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen33", "sort": {"node": "KSort", "name": "Gas"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<timestamp>", "params": []}, "args": [{"node": "KVariable", "name": "TIME", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<extraData>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen34", "sort": {"node": "KSort", "name": "Bytes"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<mixHash>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen35", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<blockNonce>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen36", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<baseFee>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen37", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<withdrawalsRoot>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen39", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<blobGasUsed>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen40", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<excessBlobGas>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen41", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<beaconRoot>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen42", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<ommerBlockHeaders>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen38", "sort": {"node": "KSort", "name": "JSON"}}], "arity": 1, "variable": false}], "arity": 21, "variable": false}], "arity": 14, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<network>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<chainID>", "params": []}, "args": [{"node": "KVariable", "name": "VChainId", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<accounts>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_AccountCellMap_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_AccountCellMap_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<account>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<acctID>", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<balance>", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID_balance", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<code>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "parseByteStack", "params": []}, "args": [{"node": "KToken", "token": "\"0x608060405234801561001057600080fd5b50600436106101165760003560e01c8063957aa58c116100a2578063c959c42b11610071578063c959c42b14610479578063ca40c419146104a7578063cfc4af55146104f3578063cfdd330214610521578063fc7b6aee1461053f57610116565b8063957aa58c146103915780639c52a7f1146103af578063a2f91af2146103f3578063bf353dbb1461042157610116565b80634b43ed12116100e95780634b43ed12146102755780634e8b1dd5146102b757806365fae35e146102e55780637bd2bea7146103295780637d780d821461037357610116565b806326e027f11461011b57806329ae81141461014957806336569e77146101815780634423c5f1146101cb575b600080fd5b6101476004803603602081101561013157600080fd5b810190808035906020019092919050505061056d565b005b61017f6004803603604081101561015f57600080fd5b8101908080359060200190929190803590602001909291905050506108b4565b005b610189610ae7565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b6101f7600480360360208110156101e157600080fd5b8101908080359060200190929190505050610b0d565b604051808681526020018581526020018473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018365ffffffffffff1665ffffffffffff1681526020018265ffffffffffff1665ffffffffffff1681526020019550505050505060405180910390f35b6102b56004803603606081101561028b57600080fd5b81019080803590602001909291908035906020019092919080359060200190929190505050610b87565b005b6102bf6113d1565b604051808265ffffffffffff1665ffffffffffff16815260200191505060405180910390f35b610327600480360360208110156102fb57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291905050506113e9565b005b610331611517565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b61037b61153d565b6040518082815260200191505060405180910390f35b610399611543565b6040518082815260200191505060405180910390f35b6103f1600480360360208110156103c557600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050611549565b005b61041f6004803603602081101561040957600080fd5b8101908080359060200190929190505050611677565b005b6104636004803603602081101561043757600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919050505061185e565b6040518082815260200191505060405180910390f35b6104a56004803603602081101561048f57600080fd5b8101908080359060200190929190505050611876565b005b6104dd600480360360408110156104bd57600080fd5b810190808035906020019092919080359060200190929190505050611cd7565b6040518082815260200191505060405180910390f35b6104fb6120d0565b604051808265ffffffffffff1665ffffffffffff16815260200191505060405180910390f35b6105296120e8565b6040518082815260200191505060405180910390f35b61056b6004803603602081101561055557600080fd5b81019080803590602001909291905050506120ee565b005b6000600754146105e5576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f466c61707065722f7374696c6c2d6c697665000000000000000000000000000081525060200191505060405180910390fd5b600073ffffffffffffffffffffffffffffffffffffffff166001600083815260200190815260200160002060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1614156106be576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260138152602001807f466c61707065722f6775792d6e6f742d7365740000000000000000000000000081525060200191505060405180910390fd5b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b306001600085815260200190815260200160002060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1660016000868152602001908152602001600020600001546040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b1580156107e757600080fd5b505af11580156107fb573d6000803e3d6000fd5b505050506001600082815260200190815260200160002060008082016000905560018201600090556002820160006101000a81549073ffffffffffffffffffffffffffffffffffffffff02191690556002820160146101000a81549065ffffffffffff021916905560028201601a6101000a81549065ffffffffffff021916905550505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414610968576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260168152602001807f466c61707065722f6e6f742d617574686f72697a65640000000000000000000081525060200191505060405180910390fd5b7f626567000000000000000000000000000000000000000000000000000000000082141561099c5780600481905550610ab0565b7f74746c00000000000000000000000000000000000000000000000000000000008214156109ee5780600560006101000a81548165ffffffffffff021916908365ffffffffffff160217905550610aaf565b7f7461750000000000000000000000000000000000000000000000000000000000821415610a405780600560066101000a81548165ffffffffffff021916908365ffffffffffff160217905550610aae565b6040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601f8152602001807f466c61707065722f66696c652d756e7265636f676e697a65642d706172616d0081525060200191505060405180910390fd5b5b5b5961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a4505050565b600260009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b60016020528060005260406000206000915090508060000154908060010154908060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff16908060020160149054906101000a900465ffffffffffff169080600201601a9054906101000a900465ffffffffffff16905085565b600160075414610bff576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260108152602001807f466c61707065722f6e6f742d6c6976650000000000000000000000000000000081525060200191505060405180910390fd5b600073ffffffffffffffffffffffffffffffffffffffff166001600085815260200190815260200160002060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff161415610cd8576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260138152602001807f466c61707065722f6775792d6e6f742d7365740000000000000000000000000081525060200191505060405180910390fd5b426001600085815260200190815260200160002060020160149054906101000a900465ffffffffffff1665ffffffffffff161180610d46575060006001600085815260200190815260200160002060020160149054906101000a900465ffffffffffff1665ffffffffffff16145b610db8576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601c8152602001807f466c61707065722f616c72656164792d66696e69736865642d7469630000000081525060200191505060405180910390fd5b4260016000858152602001908152602001600020600201601a9054906101000a900465ffffffffffff1665ffffffffffff1611610e5d576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601c8152602001807f466c61707065722f616c72656164792d66696e69736865642d656e640000000081525060200191505060405180910390fd5b60016000848152602001908152602001600020600101548214610ee8576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260188152602001807f466c61707065722f6c6f742d6e6f742d6d61746368696e67000000000000000081525060200191505060405180910390fd5b60016000848152602001908152602001600020600001548111610f73576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260168152602001807f466c61707065722f6269642d6e6f742d6869676865720000000000000000000081525060200191505060405180910390fd5b610f9560045460016000868152602001908152602001600020600001546122c5565b610fa782670de0b6b3a76400006122c5565b101561101b576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601d8152602001807f466c61707065722f696e73756666696369656e742d696e63726561736500000081525060200191505060405180910390fd5b6001600084815260200190815260200160002060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff161461121b57600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b336001600087815260200190815260200160002060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1660016000888152602001908152602001600020600001546040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b1580156111ad57600080fd5b505af11580156111c1573d6000803e3d6000fd5b50505050336001600085815260200190815260200160002060020160006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff1602179055505b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b3330600160008881526020019081526020016000206000015485036040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b15801561131057600080fd5b505af1158015611324573d6000803e3d6000fd5b5050505080600160008581526020019081526020016000206000018190555061136142600560009054906101000a900465ffffffffffff166122f1565b6001600085815260200190815260200160002060020160146101000a81548165ffffffffffff021916908365ffffffffffff1602179055505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a450505050565b600560009054906101000a900465ffffffffffff1681565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541461149d576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260168152602001807f466c61707065722f6e6f742d617574686f72697a65640000000000000000000081525060200191505060405180910390fd5b60016000808373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b60045481565b60075481565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054146115fd576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260168152602001807f466c61707065722f6e6f742d617574686f72697a65640000000000000000000081525060200191505060405180910390fd5b60008060008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b60016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541461172b576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260168152602001807f466c61707065722f6e6f742d617574686f72697a65640000000000000000000081525060200191505060405180910390fd5b6000600781905550600260009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b3033846040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b15801561181057600080fd5b505af1158015611824573d6000803e3d6000fd5b505050505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b60006020528060005260406000206000915090505481565b6001600754146118ee576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260108152602001807f466c61707065722f6e6f742d6c6976650000000000000000000000000000000081525060200191505060405180910390fd5b60006001600083815260200190815260200160002060020160149054906101000a900465ffffffffffff1665ffffffffffff16141580156119985750426001600083815260200190815260200160002060020160149054906101000a900465ffffffffffff1665ffffffffffff16108061199757504260016000838152602001908152602001600020600201601a9054906101000a900465ffffffffffff1665ffffffffffff16105b5b611a0a576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f466c61707065722f6e6f742d66696e697368656400000000000000000000000081525060200191505060405180910390fd5b600260009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b306001600085815260200190815260200160002060020160009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1660016000868152602001908152602001600020600101546040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b158015611b3357600080fd5b505af1158015611b47573d6000803e3d6000fd5b50505050600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16639dc29fac3060016000858152602001908152602001600020600001546040518363ffffffff1660e01b8152600401808373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200182815260200192505050600060405180830381600087803b158015611c0a57600080fd5b505af1158015611c1e573d6000803e3d6000fd5b505050506001600082815260200190815260200160002060008082016000905560018201600090556002820160006101000a81549073ffffffffffffffffffffffffffffffffffffffff02191690556002820160146101000a81549065ffffffffffff021916905560028201601a6101000a81549065ffffffffffff021916905550505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b600060016000803373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414611d8d576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260168152602001807f466c61707065722f6e6f742d617574686f72697a65640000000000000000000081525060200191505060405180910390fd5b600160075414611e05576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260108152602001807f466c61707065722f6e6f742d6c6976650000000000000000000000000000000081525060200191505060405180910390fd5b7fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff60065410611e9c576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260108152602001807f466c61707065722f6f766572666c6f770000000000000000000000000000000081525060200191505060405180910390fd5b6006600081546001019190508190559050816001600083815260200190815260200160002060000181905550826001600083815260200190815260200160002060010181905550336001600083815260200190815260200160002060020160006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff160217905550611f5642600560069054906101000a900465ffffffffffff166122f1565b60016000838152602001908152602001600020600201601a6101000a81548165ffffffffffff021916908365ffffffffffff160217905550600260009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663bb35783b3330866040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018281526020019350505050600060405180830381600087803b15801561206b57600080fd5b505af115801561207f573d6000803e3d6000fd5b505050507fe6dde59cbc017becba89714a037778d234a84ce7f0a137487142a007e580d60981848460405180848152602001838152602001828152602001935050505060405180910390a192915050565b600560069054906101000a900465ffffffffffff1681565b60065481565b4260016000838152602001908152602001600020600201601a9054906101000a900465ffffffffffff1665ffffffffffff1610612193576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f466c61707065722f6e6f742d66696e697368656400000000000000000000000081525060200191505060405180910390fd5b60006001600083815260200190815260200160002060020160149054906101000a900465ffffffffffff1665ffffffffffff1614612239576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601a8152602001807f466c61707065722f6269642d616c72656164792d706c6163656400000000000081525060200191505060405180910390fd5b61225742600560069054906101000a900465ffffffffffff166122f1565b60016000838152602001908152602001600020600201601a6101000a81548165ffffffffffff021916908365ffffffffffff1602179055505961012081016040526020815260e0602082015260e0600060408301376024356004353360003560e01c60e01b61012085a45050565b6000808214806122e257508282838502925082816122df57fe5b04145b6122eb57600080fd5b92915050565b60008265ffffffffffff1682840191508165ffffffffffff16101561231557600080fd5b9291505056fea265627a7a723158201acd0496ca3432003bac40639b3808573f9831f884ae4dc91d004d0deff68a7364736f6c634300050c0032\"", "sort": {"node": "KSort", "name": "String"}}], "arity": 1, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<storage>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KToken", "token": "7", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Live", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KToken", "token": "3", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "DSToken", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_+Int_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "ABI_id", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KVariable", "name": "Bid", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_+Int_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "ABI_id", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KVariable", "name": "Lot", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_+Int_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "ABI_id", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KToken", "token": "2", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "#WordPackAddrUInt48UInt48(_,_,_)_WORD-PACK_Int_Int_Int_Int", "params": []}, "args": [{"node": "KVariable", "name": "Guy", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Tic", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "End", "sort": {"node": "KSort", "name": "Int"}}], "arity": 3, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KVariable", "name": "ACCT_ID_STORAGE", "sort": {"node": "KSort", "name": "Map"}}], "arity": 2, "variable": false}, "rhs": {"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KToken", "token": "7", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Live", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KToken", "token": "3", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "DSToken", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_+Int_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "ABI_id", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_+Int_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "ABI_id", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_+Int_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "ABI_id", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KToken", "token": "2", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KVariable", "name": "ACCT_ID_STORAGE", "sort": {"node": "KSort", "name": "Map"}}], "arity": 2, "variable": false}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<origStorage>", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID_ORIG_STORAGE", "sort": {"node": "KSort", "name": "Map"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<transientStorage>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen43", "sort": {"node": "KSort", "name": "Map"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<nonce>", "params": []}, "args": [{"node": "KVariable", "name": "Nonce_Flapper", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}], "arity": 7, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<account>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<acctID>", "params": []}, "args": [{"node": "KVariable", "name": "DSToken", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<balance>", "params": []}, "args": [{"node": "KVariable", "name": "DSToken_balance", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<code>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "parseByteStack", "params": []}, "args": [{"node": "KToken", "token": "\"0x608060405234801561001057600080fd5b50600436106101735760003560e01c80637a9e5e4b116100de578063b753a98c11610097578063bf7e214f11610071578063bf7e214f14610684578063daea85c5146106ce578063dd62ed3e1461072a578063f2d5d56b146107a257610173565b8063b753a98c146105be578063bb35783b1461060c578063be9a65551461067a57610173565b80637a9e5e4b146104305780638da5cb5b1461047457806395d89b41146104be5780639dc29fac146104dc578063a0712d681461052a578063a9059cbb1461055857610173565b8063313ce56711610130578063313ce567146102ee57806340c10f191461030c57806342966c681461035a5780635ac801fe1461038857806370a08231146103b657806375f12b211461040e57610173565b806306fdde031461017857806307da68f514610196578063095ea7b3146101a057806313af40351461020657806318160ddd1461024a57806323b872dd14610268575b600080fd5b6101806107f0565b6040518082815260200191505060405180910390f35b61019e6107f6565b005b6101ec600480360360408110156101b657600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050610970565b604051808215151515815260200191505060405180910390f35b6102486004803603602081101561021c57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050610a07565b005b610252610b50565b6040518082815260200191505060405180910390f35b6102d46004803603606081101561027e57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050610b59565b604051808215151515815260200191505060405180910390f35b6102f66110f1565b6040518082815260200191505060405180910390f35b6103586004803603604081101561032257600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803590602001909291905050506110f7565b005b6103866004803603602081101561037057600080fd5b810190808035906020019092919050505061130a565b005b6103b46004803603602081101561039e57600080fd5b8101908080359060200190929190505050611317565b005b6103f8600480360360208110156103cc57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291905050506113c1565b6040518082815260200191505060405180910390f35b61041661140a565b604051808215151515815260200191505060405180910390f35b6104726004803603602081101561044657600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919050505061141d565b005b61047c611566565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b6104c661158c565b6040518082815260200191505060405180910390f35b610528600480360360408110156104f257600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611592565b005b6105566004803603602081101561054057600080fd5b8101908080359060200190929190505050611b30565b005b6105a46004803603604081101561056e57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611b3d565b604051808215151515815260200191505060405180910390f35b61060a600480360360408110156105d457600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611b52565b005b6106786004803603606081101561062257600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611b62565b005b610682611b73565b005b61068c611ced565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b610710600480360360208110156106e457600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050611d13565b604051808215151515815260200191505060405180910390f35b61078c6004803603604081101561074057600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050611dc9565b6040518082815260200191505060405180910390f35b6107ee600480360360408110156107b857600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611e50565b005b60075481565b610824336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b610896576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b60008060006004359250602435915034905081833373ffffffffffffffffffffffffffffffffffffffff166000357fffffffff00000000000000000000000000000000000000000000000000000000167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19168460003660405180848152602001806020018281038252848482818152602001925080828437600081840152601f19601f82011690508083019250505094505050505060405180910390a46001600460146101000a81548160ff021916908315150217905550505050565b6000600460149054906101000a900460ff16156109f5576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b6109ff83836120bb565b905092915050565b610a35336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b610aa7576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b80600460006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff160217905550600460009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff167fce241d7ca1f669fee44b6fc00b8eba2df3bb514eed0f6f668f8f89096e81ed9460405160405180910390a250565b60008054905090565b6000600460149054906101000a900460ff1615610bde576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b3373ffffffffffffffffffffffffffffffffffffffff168473ffffffffffffffffffffffffffffffffffffffff1614158015610cb657507fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414155b15610eb45781600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015610dad576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601e8152602001807f64732d746f6b656e2d696e73756666696369656e742d617070726f76616c000081525060200191505060405180910390fd5b610e33600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054836121ad565b600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505b81600160008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015610f69576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601d8152602001807f64732d746f6b656e2d696e73756666696369656e742d62616c616e636500000081525060200191505060405180910390fd5b610fb2600160008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054836121ad565b600160008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000208190555061103e600160008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205483612230565b600160008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055508273ffffffffffffffffffffffffffffffffffffffff168473ffffffffffffffffffffffffffffffffffffffff167fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef846040518082815260200191505060405180910390a3600190509392505050565b60065481565b611125336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b611197576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b600460149054906101000a900460ff161561121a576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b611263600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205482612230565b600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055506112b260005482612230565b6000819055508173ffffffffffffffffffffffffffffffffffffffff167f0f6798a560793a54c3bcfe86a93cde1e73087d944c0ea20544137d4121396885826040518082815260200191505060405180910390a25050565b6113143382611592565b50565b611345336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b6113b7576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b8060078190555050565b6000600160008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020549050919050565b600460149054906101000a900460ff1681565b61144b336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b6114bd576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b80600360006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff160217905550600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff167f1abebea81bfa2637f28358c371278fb15ede7ea8dd28d2e03b112ff6d936ada460405160405180910390a250565b600460009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b60055481565b6115c0336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b611632576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b600460149054906101000a900460ff16156116b5576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b3373ffffffffffffffffffffffffffffffffffffffff168273ffffffffffffffffffffffffffffffffffffffff161415801561178d57507fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414155b1561198b5780600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015611884576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601e8152602001807f64732d746f6b656e2d696e73756666696369656e742d617070726f76616c000081525060200191505060405180910390fd5b61190a600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054826121ad565b600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505b80600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015611a40576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601d8152602001807f64732d746f6b656e2d696e73756666696369656e742d62616c616e636500000081525060200191505060405180910390fd5b611a89600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054826121ad565b600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002081905550611ad8600054826121ad565b6000819055508173ffffffffffffffffffffffffffffffffffffffff167fcc16f5dbb4873280815c1ee09dbd06736cffcc184412cf7a71a0fdb75d397ca5826040518082815260200191505060405180910390a25050565b611b3a33826110f7565b50565b6000611b4a338484610b59565b905092915050565b611b5d338383610b59565b505050565b611b6d838383610b59565b50505050565b611ba1336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b611c13576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b60008060006004359250602435915034905081833373ffffffffffffffffffffffffffffffffffffffff166000357fffffffff00000000000000000000000000000000000000000000000000000000167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19168460003660405180848152602001806020018281038252848482818152602001925080828437600081840152601f19601f82011690508083019250505094505050505060405180910390a46000600460146101000a81548160ff021916908315150217905550505050565b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b6000600460149054906101000a900460ff1615611d98576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b611dc2827fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff6120bb565b9050919050565b6000600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054905092915050565b611e5b823383610b59565b505050565b60003073ffffffffffffffffffffffffffffffffffffffff168373ffffffffffffffffffffffffffffffffffffffff161415611e9f57600190506120b5565b600460009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168373ffffffffffffffffffffffffffffffffffffffff161415611efe57600190506120b5565b600073ffffffffffffffffffffffffffffffffffffffff16600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff161415611f5e57600090506120b5565b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663b70096138430856040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001827bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19168152602001935050505060206040518083038186803b15801561207757600080fd5b505afa15801561208b573d6000803e3d6000fd5b505050506040513d60208110156120a157600080fd5b810190808051906020019092919050505090505b92915050565b600081600260003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055508273ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff167f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b925846040518082815260200191505060405180910390a36001905092915050565b600082828403915081111561222a576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260158152602001807f64732d6d6174682d7375622d756e646572666c6f77000000000000000000000081525060200191505060405180910390fd5b92915050565b60008282840191508110156122ad576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d6d6174682d6164642d6f766572666c6f7700000000000000000000000081525060200191505060405180910390fd5b9291505056fea265627a7a7231582042e4b52e52d434217b55a1ee90f412a7c49b1fd0406bb9ec1168e2a7c1fbad0e64736f6c634300050c0032\"", "sort": {"node": "KSort", "name": "String"}}], "arity": 1, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<storage>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KVariable", "name": "Gem_a", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "Guy", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KVariable", "name": "Gem_g", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KToken", "token": "4", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "#WordPackAddrUInt8(_,_)_WORD-PACK_Int_Int_Int", "params": []}, "args": [{"node": "KVariable", "name": "Owner", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Stopped", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KVariable", "name": "DSToken_STORAGE", "sort": {"node": "KSort", "name": "Map"}}], "arity": 2, "variable": false}, "rhs": {"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_-Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_a", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Bid", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "Guy", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_+Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_g", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Bid", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KToken", "token": "4", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "#WordPackAddrUInt8(_,_)_WORD-PACK_Int_Int_Int", "params": []}, "args": [{"node": "KVariable", "name": "Owner", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Stopped", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KVariable", "name": "DSToken_STORAGE", "sort": {"node": "KSort", "name": "Map"}}], "arity": 2, "variable": false}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<origStorage>", "params": []}, "args": [{"node": "KVariable", "name": "DSToken_ORIG_STORAGE", "sort": {"node": "KSort", "name": "Map"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<transientStorage>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen44", "sort": {"node": "KSort", "name": "Map"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<nonce>", "params": []}, "args": [{"node": "KVariable", "name": "Nonce_DSToken", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}], "arity": 7, "variable": false}], "arity": 2, "variable": false}, {"node": "KVariable", "name": "_DotVar4", "sort": {"node": "KSort", "name": "AccountCellMap"}}], "arity": 2, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<txOrder>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen45", "sort": {"node": "KSort", "name": "List"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<txPending>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen46", "sort": {"node": "KSort", "name": "List"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<messages>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen47", "sort": {"node": "KSort", "name": "MessageCellMap"}}], "arity": 1, "variable": false}, {"node": "KVariable", "name": "_Gen5", "sort": {"node": "KSort", "name": "WithdrawalsPendingCell"}}, {"node": "KVariable", "name": "_Gen6", "sort": {"node": "KSort", "name": "WithdrawalsOrderCell"}}, {"node": "KVariable", "name": "_Gen7", "sort": {"node": "KSort", "name": "WithdrawalsCell"}}], "arity": 8, "variable": false}], "arity": 2, "variable": false}], "arity": 6, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<generatedCounter>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KVariable", "name": "_Gen48", "sort": {"node": "KSort", "name": "Int"}}, "rhs": {"node": "KVariable", "name": "?_Gen49", "sort": {"node": "KSort", "name": "Int"}}}], "arity": 1, "variable": false}], "arity": 2, "variable": false}, "requires": {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ACCT_ID", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "1461501637330902918203684832716283019655932542976", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_=/=Int_", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "#notPrecompileAddress(_)_LEMMAS-MCD-SYNTAX_Bool_Int", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "CALLER_ID", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "CALLER_ID", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "1461501637330902918203684832716283019655932542976", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ORIGIN_ID", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "ORIGIN_ID", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "1461501637330902918203684832716283019655932542976", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "TIME", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "TIME", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ACCT_ID_balance", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID_balance", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KVariable", "name": "VCallDepth", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "1024", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "VCallValue", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "VCallValue", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "VChainId", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "VChainId", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ABI_id", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "ABI_id", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Live", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Live", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "DSToken", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "DSToken", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "1461501637330902918203684832716283019655932542976", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Bid", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Bid", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Lot", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Lot", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Guy", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Guy", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "1461501637330902918203684832716283019655932542976", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Tic", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Tic", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "281474976710656", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "End", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "End", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "281474976710656", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Gem_a", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_a", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Gem_g", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_g", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Stopped", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Stopped", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "2", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Owner", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Owner", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "1461501637330902918203684832716283019655932542976", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "DSToken_balance", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "DSToken_balance", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "lengthBytes(_)_BYTES-HOOKED_Int_Bytes", "params": []}, "args": [{"node": "KVariable", "name": "CD", "sort": {"node": "KSort", "name": "Bytes"}}], "arity": 1, "variable": false}, {"node": "KToken", "token": "1250000000", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "#notPrecompileAddress(_)_LEMMAS-MCD-SYNTAX_Bool_Int", "params": []}, "args": [{"node": "KVariable", "name": "DSToken", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "#notPrecompileAddress(_)_LEMMAS-MCD-SYNTAX_Bool_Int", "params": []}, "args": [{"node": "KVariable", "name": "Guy", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "#notPrecompileAddress(_)_LEMMAS-MCD-SYNTAX_Bool_Int", "params": []}, "args": [{"node": "KVariable", "name": "Owner", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_=/=Int_", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "DSToken", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_=/=Int_", "params": []}, "args": [{"node": "KVariable", "name": "DSToken", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_=/=Int_", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Guy", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_==Int_", "params": []}, "args": [{"node": "KVariable", "name": "Live", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_=/=Int_", "params": []}, "args": [{"node": "KVariable", "name": "Guy", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_==Int_", "params": []}, "args": [{"node": "KVariable", "name": "Stopped", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "VCallDepth", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "1024", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_==Int_", "params": []}, "args": [{"node": "KVariable", "name": "VCallValue", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "_-Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_a", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Bid", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_-Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_a", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Bid", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "_+Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_g", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Bid", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_+Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_g", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Bid", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Nonce_Flapper", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Nonce_Flapper", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "18446744073709551615", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Nonce_DSToken", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Nonce_DSToken", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "18446744073709551615", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, "ensures": {"node": "KToken", "token": "true", "sort": {"node": "KSort", "name": "Bool"}}, "att": {"node": "KAtt", "att": {"org.kframework.definition.Production": {"node": "KProduction", "klabel": {"node": "KLabel", "name": "#ruleRequires", "params": []}, "productionItems": [{"node": "KNonTerminal", "sort": {"node": "KSort", "name": "#RuleBody"}}, {"node": "KTerminal", "value": "requires"}, {"node": "KNonTerminal", "sort": {"node": "KSort", "name": "Bool"}}], "params": [], "sort": {"node": "KSort", "name": "#RuleContent"}, "att": {"node": "KAtt", "att": {"symbol": "#ruleRequires", "org.kframework.attributes.Location": [346, 27, 346, 94], "org.kframework.attributes.Source": "/nix/store/b9ydnz6rpq5gmya15cacdzhlsskadqsw-k-7.1.244-9922ec2536765c1370fd83914a006961d9149326/include/kframework/builtin/kast.md"}}}, "UNIQUE_ID": "80e358182b63686fae5cbb29398cdb8755aff61a20cd46eace552c2ffe61fe65", "label": "FLAPPER-YANK-PASS-ROUGH-SPEC.Flapper.yank.pass.rough", "org.kframework.attributes.Source": "/home/anvacaru/dev/evm-semantics/eip-7691/tests/specs/mcd-structured/flapper-yank-pass-rough-spec.k", "org.kframework.attributes.Location": [8, 7, 165, 42]}}}, {"node": "KClaim", "body": {"node": "KApply", "label": {"node": "KLabel", "name": "<generatedTop>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<kevm>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<k>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KSequence", "items": [{"node": "KApply", "label": {"node": "KLabel", "name": "execute", "params": []}, "args": [], "arity": 0, "variable": false}, {"node": "KVariable", "name": "CONTINUATION", "sort": {"node": "KSort", "name": "K"}}], "arity": 2}, "rhs": {"node": "KSequence", "items": [{"node": "KApply", "label": {"node": "KLabel", "name": "halt", "params": []}, "args": [], "arity": 0, "variable": false}, {"node": "KVariable", "name": "CONTINUATION", "sort": {"node": "KSort", "name": "K"}}], "arity": 2}}], "arity": 1, "variable": false}, {"node": "KVariable", "name": "_DotVar1", "sort": {"node": "KSort", "name": "ExitCodeCell"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "<mode>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "NORMAL", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<schedule>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "ISTANBUL_EVM", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<useGas>", "params": []}, "args": [{"node": "KToken", "token": "true", "sort": {"node": "KSort", "name": "Bool"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<ethereum>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<evm>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<output>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": ".Bytes_BYTES-HOOKED_Bytes", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<statusCode>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KVariable", "name": "_Gen0", "sort": {"node": "KSort", "name": "StatusCode"}}, "rhs": {"node": "KApply", "label": {"node": "KLabel", "name": "EVMC_SUCCESS_NETWORK_EndStatusCode", "params": []}, "args": [], "arity": 0, "variable": false}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<callStack>", "params": []}, "args": [{"node": "KVariable", "name": "_VCallStack", "sort": {"node": "KSort", "name": "List"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<interimStates>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen1", "sort": {"node": "KSort", "name": "List"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<touchedAccounts>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KVariable", "name": "_Gen2", "sort": {"node": "KSort", "name": "Set"}}, "rhs": {"node": "KVariable", "name": "?_Gen3", "sort": {"node": "KSort", "name": "Set"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<callState>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<program>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "parseByteStack", "params": []}, "args": [{"node": "KToken", "token": "\"0x608060405234801561001057600080fd5b50600436106101735760003560e01c80637a9e5e4b116100de578063b753a98c11610097578063bf7e214f11610071578063bf7e214f14610684578063daea85c5146106ce578063dd62ed3e1461072a578063f2d5d56b146107a257610173565b8063b753a98c146105be578063bb35783b1461060c578063be9a65551461067a57610173565b80637a9e5e4b146104305780638da5cb5b1461047457806395d89b41146104be5780639dc29fac146104dc578063a0712d681461052a578063a9059cbb1461055857610173565b8063313ce56711610130578063313ce567146102ee57806340c10f191461030c57806342966c681461035a5780635ac801fe1461038857806370a08231146103b657806375f12b211461040e57610173565b806306fdde031461017857806307da68f514610196578063095ea7b3146101a057806313af40351461020657806318160ddd1461024a57806323b872dd14610268575b600080fd5b6101806107f0565b6040518082815260200191505060405180910390f35b61019e6107f6565b005b6101ec600480360360408110156101b657600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050610970565b604051808215151515815260200191505060405180910390f35b6102486004803603602081101561021c57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050610a07565b005b610252610b50565b6040518082815260200191505060405180910390f35b6102d46004803603606081101561027e57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050610b59565b604051808215151515815260200191505060405180910390f35b6102f66110f1565b6040518082815260200191505060405180910390f35b6103586004803603604081101561032257600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803590602001909291905050506110f7565b005b6103866004803603602081101561037057600080fd5b810190808035906020019092919050505061130a565b005b6103b46004803603602081101561039e57600080fd5b8101908080359060200190929190505050611317565b005b6103f8600480360360208110156103cc57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291905050506113c1565b6040518082815260200191505060405180910390f35b61041661140a565b604051808215151515815260200191505060405180910390f35b6104726004803603602081101561044657600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919050505061141d565b005b61047c611566565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b6104c661158c565b6040518082815260200191505060405180910390f35b610528600480360360408110156104f257600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611592565b005b6105566004803603602081101561054057600080fd5b8101908080359060200190929190505050611b30565b005b6105a46004803603604081101561056e57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611b3d565b604051808215151515815260200191505060405180910390f35b61060a600480360360408110156105d457600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611b52565b005b6106786004803603606081101561062257600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611b62565b005b610682611b73565b005b61068c611ced565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b610710600480360360208110156106e457600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050611d13565b604051808215151515815260200191505060405180910390f35b61078c6004803603604081101561074057600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050611dc9565b6040518082815260200191505060405180910390f35b6107ee600480360360408110156107b857600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611e50565b005b60075481565b610824336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b610896576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b60008060006004359250602435915034905081833373ffffffffffffffffffffffffffffffffffffffff166000357fffffffff00000000000000000000000000000000000000000000000000000000167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19168460003660405180848152602001806020018281038252848482818152602001925080828437600081840152601f19601f82011690508083019250505094505050505060405180910390a46001600460146101000a81548160ff021916908315150217905550505050565b6000600460149054906101000a900460ff16156109f5576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b6109ff83836120bb565b905092915050565b610a35336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b610aa7576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b80600460006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff160217905550600460009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff167fce241d7ca1f669fee44b6fc00b8eba2df3bb514eed0f6f668f8f89096e81ed9460405160405180910390a250565b60008054905090565b6000600460149054906101000a900460ff1615610bde576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b3373ffffffffffffffffffffffffffffffffffffffff168473ffffffffffffffffffffffffffffffffffffffff1614158015610cb657507fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414155b15610eb45781600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015610dad576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601e8152602001807f64732d746f6b656e2d696e73756666696369656e742d617070726f76616c000081525060200191505060405180910390fd5b610e33600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054836121ad565b600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505b81600160008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015610f69576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601d8152602001807f64732d746f6b656e2d696e73756666696369656e742d62616c616e636500000081525060200191505060405180910390fd5b610fb2600160008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054836121ad565b600160008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000208190555061103e600160008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205483612230565b600160008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055508273ffffffffffffffffffffffffffffffffffffffff168473ffffffffffffffffffffffffffffffffffffffff167fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef846040518082815260200191505060405180910390a3600190509392505050565b60065481565b611125336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b611197576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b600460149054906101000a900460ff161561121a576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b611263600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205482612230565b600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055506112b260005482612230565b6000819055508173ffffffffffffffffffffffffffffffffffffffff167f0f6798a560793a54c3bcfe86a93cde1e73087d944c0ea20544137d4121396885826040518082815260200191505060405180910390a25050565b6113143382611592565b50565b611345336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b6113b7576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b8060078190555050565b6000600160008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020549050919050565b600460149054906101000a900460ff1681565b61144b336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b6114bd576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b80600360006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff160217905550600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff167f1abebea81bfa2637f28358c371278fb15ede7ea8dd28d2e03b112ff6d936ada460405160405180910390a250565b600460009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b60055481565b6115c0336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b611632576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b600460149054906101000a900460ff16156116b5576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b3373ffffffffffffffffffffffffffffffffffffffff168273ffffffffffffffffffffffffffffffffffffffff161415801561178d57507fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414155b1561198b5780600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015611884576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601e8152602001807f64732d746f6b656e2d696e73756666696369656e742d617070726f76616c000081525060200191505060405180910390fd5b61190a600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054826121ad565b600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505b80600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015611a40576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601d8152602001807f64732d746f6b656e2d696e73756666696369656e742d62616c616e636500000081525060200191505060405180910390fd5b611a89600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054826121ad565b600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002081905550611ad8600054826121ad565b6000819055508173ffffffffffffffffffffffffffffffffffffffff167fcc16f5dbb4873280815c1ee09dbd06736cffcc184412cf7a71a0fdb75d397ca5826040518082815260200191505060405180910390a25050565b611b3a33826110f7565b50565b6000611b4a338484610b59565b905092915050565b611b5d338383610b59565b505050565b611b6d838383610b59565b50505050565b611ba1336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b611c13576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b60008060006004359250602435915034905081833373ffffffffffffffffffffffffffffffffffffffff166000357fffffffff00000000000000000000000000000000000000000000000000000000167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19168460003660405180848152602001806020018281038252848482818152602001925080828437600081840152601f19601f82011690508083019250505094505050505060405180910390a46000600460146101000a81548160ff021916908315150217905550505050565b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b6000600460149054906101000a900460ff1615611d98576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b611dc2827fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff6120bb565b9050919050565b6000600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054905092915050565b611e5b823383610b59565b505050565b60003073ffffffffffffffffffffffffffffffffffffffff168373ffffffffffffffffffffffffffffffffffffffff161415611e9f57600190506120b5565b600460009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168373ffffffffffffffffffffffffffffffffffffffff161415611efe57600190506120b5565b600073ffffffffffffffffffffffffffffffffffffffff16600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff161415611f5e57600090506120b5565b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663b70096138430856040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001827bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19168152602001935050505060206040518083038186803b15801561207757600080fd5b505afa15801561208b573d6000803e3d6000fd5b505050506040513d60208110156120a157600080fd5b810190808051906020019092919050505090505b92915050565b600081600260003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055508273ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff167f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b925846040518082815260200191505060405180910390a36001905092915050565b600082828403915081111561222a576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260158152602001807f64732d6d6174682d7375622d756e646572666c6f77000000000000000000000081525060200191505060405180910390fd5b92915050565b60008282840191508110156122ad576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d6d6174682d6164642d6f766572666c6f7700000000000000000000000081525060200191505060405180910390fd5b9291505056fea265627a7a7231582042e4b52e52d434217b55a1ee90f412a7c49b1fd0406bb9ec1168e2a7c1fbad0e64736f6c634300050c0032\"", "sort": {"node": "KSort", "name": "String"}}], "arity": 1, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<jumpDests>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "computeValidJumpDests", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "parseByteStack", "params": []}, "args": [{"node": "KToken", "token": "\"0x608060405234801561001057600080fd5b50600436106101735760003560e01c80637a9e5e4b116100de578063b753a98c11610097578063bf7e214f11610071578063bf7e214f14610684578063daea85c5146106ce578063dd62ed3e1461072a578063f2d5d56b146107a257610173565b8063b753a98c146105be578063bb35783b1461060c578063be9a65551461067a57610173565b80637a9e5e4b146104305780638da5cb5b1461047457806395d89b41146104be5780639dc29fac146104dc578063a0712d681461052a578063a9059cbb1461055857610173565b8063313ce56711610130578063313ce567146102ee57806340c10f191461030c57806342966c681461035a5780635ac801fe1461038857806370a08231146103b657806375f12b211461040e57610173565b806306fdde031461017857806307da68f514610196578063095ea7b3146101a057806313af40351461020657806318160ddd1461024a57806323b872dd14610268575b600080fd5b6101806107f0565b6040518082815260200191505060405180910390f35b61019e6107f6565b005b6101ec600480360360408110156101b657600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050610970565b604051808215151515815260200191505060405180910390f35b6102486004803603602081101561021c57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050610a07565b005b610252610b50565b6040518082815260200191505060405180910390f35b6102d46004803603606081101561027e57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050610b59565b604051808215151515815260200191505060405180910390f35b6102f66110f1565b6040518082815260200191505060405180910390f35b6103586004803603604081101561032257600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803590602001909291905050506110f7565b005b6103866004803603602081101561037057600080fd5b810190808035906020019092919050505061130a565b005b6103b46004803603602081101561039e57600080fd5b8101908080359060200190929190505050611317565b005b6103f8600480360360208110156103cc57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291905050506113c1565b6040518082815260200191505060405180910390f35b61041661140a565b604051808215151515815260200191505060405180910390f35b6104726004803603602081101561044657600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919050505061141d565b005b61047c611566565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b6104c661158c565b6040518082815260200191505060405180910390f35b610528600480360360408110156104f257600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611592565b005b6105566004803603602081101561054057600080fd5b8101908080359060200190929190505050611b30565b005b6105a46004803603604081101561056e57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611b3d565b604051808215151515815260200191505060405180910390f35b61060a600480360360408110156105d457600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611b52565b005b6106786004803603606081101561062257600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611b62565b005b610682611b73565b005b61068c611ced565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b610710600480360360208110156106e457600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050611d13565b604051808215151515815260200191505060405180910390f35b61078c6004803603604081101561074057600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050611dc9565b6040518082815260200191505060405180910390f35b6107ee600480360360408110156107b857600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611e50565b005b60075481565b610824336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b610896576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b60008060006004359250602435915034905081833373ffffffffffffffffffffffffffffffffffffffff166000357fffffffff00000000000000000000000000000000000000000000000000000000167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19168460003660405180848152602001806020018281038252848482818152602001925080828437600081840152601f19601f82011690508083019250505094505050505060405180910390a46001600460146101000a81548160ff021916908315150217905550505050565b6000600460149054906101000a900460ff16156109f5576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b6109ff83836120bb565b905092915050565b610a35336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b610aa7576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b80600460006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff160217905550600460009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff167fce241d7ca1f669fee44b6fc00b8eba2df3bb514eed0f6f668f8f89096e81ed9460405160405180910390a250565b60008054905090565b6000600460149054906101000a900460ff1615610bde576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b3373ffffffffffffffffffffffffffffffffffffffff168473ffffffffffffffffffffffffffffffffffffffff1614158015610cb657507fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414155b15610eb45781600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015610dad576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601e8152602001807f64732d746f6b656e2d696e73756666696369656e742d617070726f76616c000081525060200191505060405180910390fd5b610e33600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054836121ad565b600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505b81600160008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015610f69576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601d8152602001807f64732d746f6b656e2d696e73756666696369656e742d62616c616e636500000081525060200191505060405180910390fd5b610fb2600160008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054836121ad565b600160008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000208190555061103e600160008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205483612230565b600160008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055508273ffffffffffffffffffffffffffffffffffffffff168473ffffffffffffffffffffffffffffffffffffffff167fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef846040518082815260200191505060405180910390a3600190509392505050565b60065481565b611125336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b611197576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b600460149054906101000a900460ff161561121a576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b611263600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205482612230565b600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055506112b260005482612230565b6000819055508173ffffffffffffffffffffffffffffffffffffffff167f0f6798a560793a54c3bcfe86a93cde1e73087d944c0ea20544137d4121396885826040518082815260200191505060405180910390a25050565b6113143382611592565b50565b611345336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b6113b7576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b8060078190555050565b6000600160008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020549050919050565b600460149054906101000a900460ff1681565b61144b336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b6114bd576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b80600360006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff160217905550600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff167f1abebea81bfa2637f28358c371278fb15ede7ea8dd28d2e03b112ff6d936ada460405160405180910390a250565b600460009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b60055481565b6115c0336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b611632576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b600460149054906101000a900460ff16156116b5576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b3373ffffffffffffffffffffffffffffffffffffffff168273ffffffffffffffffffffffffffffffffffffffff161415801561178d57507fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414155b1561198b5780600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015611884576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601e8152602001807f64732d746f6b656e2d696e73756666696369656e742d617070726f76616c000081525060200191505060405180910390fd5b61190a600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054826121ad565b600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505b80600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015611a40576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601d8152602001807f64732d746f6b656e2d696e73756666696369656e742d62616c616e636500000081525060200191505060405180910390fd5b611a89600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054826121ad565b600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002081905550611ad8600054826121ad565b6000819055508173ffffffffffffffffffffffffffffffffffffffff167fcc16f5dbb4873280815c1ee09dbd06736cffcc184412cf7a71a0fdb75d397ca5826040518082815260200191505060405180910390a25050565b611b3a33826110f7565b50565b6000611b4a338484610b59565b905092915050565b611b5d338383610b59565b505050565b611b6d838383610b59565b50505050565b611ba1336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b611c13576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b60008060006004359250602435915034905081833373ffffffffffffffffffffffffffffffffffffffff166000357fffffffff00000000000000000000000000000000000000000000000000000000167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19168460003660405180848152602001806020018281038252848482818152602001925080828437600081840152601f19601f82011690508083019250505094505050505060405180910390a46000600460146101000a81548160ff021916908315150217905550505050565b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b6000600460149054906101000a900460ff1615611d98576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b611dc2827fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff6120bb565b9050919050565b6000600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054905092915050565b611e5b823383610b59565b505050565b60003073ffffffffffffffffffffffffffffffffffffffff168373ffffffffffffffffffffffffffffffffffffffff161415611e9f57600190506120b5565b600460009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168373ffffffffffffffffffffffffffffffffffffffff161415611efe57600190506120b5565b600073ffffffffffffffffffffffffffffffffffffffff16600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff161415611f5e57600090506120b5565b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663b70096138430856040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001827bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19168152602001935050505060206040518083038186803b15801561207757600080fd5b505afa15801561208b573d6000803e3d6000fd5b505050506040513d60208110156120a157600080fd5b810190808051906020019092919050505090505b92915050565b600081600260003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055508273ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff167f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b925846040518082815260200191505060405180910390a36001905092915050565b600082828403915081111561222a576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260158152602001807f64732d6d6174682d7375622d756e646572666c6f77000000000000000000000081525060200191505060405180910390fd5b92915050565b60008282840191508110156122ad576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d6d6174682d6164642d6f766572666c6f7700000000000000000000000081525060200191505060405180910390fd5b9291505056fea265627a7a7231582042e4b52e52d434217b55a1ee90f412a7c49b1fd0406bb9ec1168e2a7c1fbad0e64736f6c634300050c0032\"", "sort": {"node": "KSort", "name": "String"}}], "arity": 1, "variable": false}], "arity": 1, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<id>", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<caller>", "params": []}, "args": [{"node": "KVariable", "name": "CALLER_ID", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<callData>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KApply", "label": {"node": "KLabel", "name": "_+Bytes__BYTES-HOOKED_Bytes_Bytes_Bytes", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "abiCallData", "params": []}, "args": [{"node": "KToken", "token": "\"move\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "typedArgs", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "abi_type_address", "params": []}, "args": [{"node": "KVariable", "name": "ABI_src", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "typedArgs", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "abi_type_address", "params": []}, "args": [{"node": "KVariable", "name": "ABI_dst", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "typedArgs", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "abi_type_uint256", "params": []}, "args": [{"node": "KVariable", "name": "ABI_wad", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"typedArgs\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KVariable", "name": "CD", "sort": {"node": "KSort", "name": "Bytes"}}], "arity": 2, "variable": false}, "rhs": {"node": "KVariable", "name": "?_Gen4", "sort": {"node": "KSort", "name": "Bytes"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<callValue>", "params": []}, "args": [{"node": "KVariable", "name": "VCallValue", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<wordStack>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KApply", "label": {"node": "KLabel", "name": ".WordStack_EVM-TYPES_WordStack", "params": []}, "args": [], "arity": 0, "variable": false}, "rhs": {"node": "KVariable", "name": "?_Gen5", "sort": {"node": "KSort", "name": "WordStack"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<localMem>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KApply", "label": {"node": "KLabel", "name": ".Bytes_BYTES-HOOKED_Bytes", "params": []}, "args": [], "arity": 0, "variable": false}, "rhs": {"node": "KVariable", "name": "?_Gen6", "sort": {"node": "KSort", "name": "Bytes"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<pc>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, "rhs": {"node": "KVariable", "name": "?_Gen7", "sort": {"node": "KSort", "name": "Int"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<gas>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KApply", "label": {"node": "KLabel", "name": "infGas", "params": []}, "args": [{"node": "KVariable", "name": "VGas", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, "rhs": {"node": "KApply", "label": {"node": "KLabel", "name": "ite", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_==Int_", "params": []}, "args": [{"node": "KVariable", "name": "Allowance", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639935", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "infGas", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_+Int_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_-Int_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_-Int_", "params": []}, "args": [{"node": "KVariable", "name": "VGas", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "Csstore", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "ISTANBUL_EVM", "params": []}, "args": [], "arity": 0, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_-Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_s", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ABI_wad", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KVariable", "name": "Gem_s", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Junk_1", "sort": {"node": "KSort", "name": "Int"}}], "arity": 4, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "Csstore", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "ISTANBUL_EVM", "params": []}, "args": [], "arity": 0, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_+Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_d", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ABI_wad", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KVariable", "name": "Gem_d", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Junk_2", "sort": {"node": "KSort", "name": "Int"}}], "arity": 4, "variable": false}], "arity": 2, "variable": false}, {"node": "KToken", "token": "-7281", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "infGas", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_+Int_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_-Int_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_-Int_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_-Int_", "params": []}, "args": [{"node": "KVariable", "name": "VGas", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "Csstore", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "ISTANBUL_EVM", "params": []}, "args": [], "arity": 0, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_-Int_", "params": []}, "args": [{"node": "KVariable", "name": "Allowance", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ABI_wad", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KVariable", "name": "Allowance", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Junk_0", "sort": {"node": "KSort", "name": "Int"}}], "arity": 4, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "Csstore", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "ISTANBUL_EVM", "params": []}, "args": [], "arity": 0, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_-Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_s", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ABI_wad", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KVariable", "name": "Gem_s", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Junk_1", "sort": {"node": "KSort", "name": "Int"}}], "arity": 4, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "Csstore", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "ISTANBUL_EVM", "params": []}, "args": [], "arity": 0, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_+Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_d", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ABI_wad", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KVariable", "name": "Gem_d", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Junk_2", "sort": {"node": "KSort", "name": "Int"}}], "arity": 4, "variable": false}], "arity": 2, "variable": false}, {"node": "KToken", "token": "-9538", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 1, "variable": false}], "arity": 3, "variable": false}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<memoryUsed>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, "rhs": {"node": "KVariable", "name": "?_Gen8", "sort": {"node": "KSort", "name": "Int"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<callGas>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KVariable", "name": "_Gen9", "sort": {"node": "KSort", "name": "Gas"}}, "rhs": {"node": "KVariable", "name": "?_Gen10", "sort": {"node": "KSort", "name": "Gas"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<static>", "params": []}, "args": [{"node": "KToken", "token": "false", "sort": {"node": "KSort", "name": "Bool"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<callDepth>", "params": []}, "args": [{"node": "KVariable", "name": "VCallDepth", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}], "arity": 14, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<versionedHashes>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen11", "sort": {"node": "KSort", "name": "List"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<substate>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<selfDestruct>", "params": []}, "args": [{"node": "KVariable", "name": "_VSelfDestruct", "sort": {"node": "KSort", "name": "Set"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<log>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KVariable", "name": "_Gen12", "sort": {"node": "KSort", "name": "List"}}, "rhs": {"node": "KVariable", "name": "?_Gen13", "sort": {"node": "KSort", "name": "List"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<refund>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KVariable", "name": "_Vrefund", "sort": {"node": "KSort", "name": "Int"}}, "rhs": {"node": "KVariable", "name": "?_Gen14", "sort": {"node": "KSort", "name": "Int"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<accessedAccounts>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KVariable", "name": "_Gen15", "sort": {"node": "KSort", "name": "Set"}}, "rhs": {"node": "KVariable", "name": "?_Gen16", "sort": {"node": "KSort", "name": "Set"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<accessedStorage>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KVariable", "name": "_Gen17", "sort": {"node": "KSort", "name": "Map"}}, "rhs": {"node": "KVariable", "name": "?_Gen18", "sort": {"node": "KSort", "name": "Map"}}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<createdAccounts>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KVariable", "name": "_Gen19", "sort": {"node": "KSort", "name": "Set"}}, "rhs": {"node": "KVariable", "name": "?_Gen20", "sort": {"node": "KSort", "name": "Set"}}}], "arity": 1, "variable": false}], "arity": 6, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<gasPrice>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen21", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<origin>", "params": []}, "args": [{"node": "KVariable", "name": "ORIGIN_ID", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<blockhashes>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen22", "sort": {"node": "KSort", "name": "List"}}], "arity": 1, "variable": false}, {"node": "KVariable", "name": "_Gen3", "sort": {"node": "KSort", "name": "PreviousExcessBlobGasCell"}}, {"node": "KVariable", "name": "_Gen4", "sort": {"node": "KSort", "name": "PreviousBlobGasUsedCell"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "<block>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<previousHash>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen23", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<ommersHash>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen24", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<coinbase>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen25", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<stateRoot>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen26", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<transactionsRoot>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen27", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<receiptsRoot>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen28", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<logsBloom>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen29", "sort": {"node": "KSort", "name": "Bytes"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<difficulty>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen30", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<number>", "params": []}, "args": [{"node": "KVariable", "name": "_BLOCK_NUMBER", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<gasLimit>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen31", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<gasUsed>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen32", "sort": {"node": "KSort", "name": "Gas"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<timestamp>", "params": []}, "args": [{"node": "KVariable", "name": "TIME", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<extraData>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen33", "sort": {"node": "KSort", "name": "Bytes"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<mixHash>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen34", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<blockNonce>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen35", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<baseFee>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen36", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<withdrawalsRoot>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen38", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<blobGasUsed>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen39", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<excessBlobGas>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen40", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<beaconRoot>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen41", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<ommerBlockHeaders>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen37", "sort": {"node": "KSort", "name": "JSON"}}], "arity": 1, "variable": false}], "arity": 21, "variable": false}], "arity": 14, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<network>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<chainID>", "params": []}, "args": [{"node": "KVariable", "name": "VChainId", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<accounts>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_AccountCellMap_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<account>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "<acctID>", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<balance>", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID_balance", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<code>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "parseByteStack", "params": []}, "args": [{"node": "KToken", "token": "\"0x608060405234801561001057600080fd5b50600436106101735760003560e01c80637a9e5e4b116100de578063b753a98c11610097578063bf7e214f11610071578063bf7e214f14610684578063daea85c5146106ce578063dd62ed3e1461072a578063f2d5d56b146107a257610173565b8063b753a98c146105be578063bb35783b1461060c578063be9a65551461067a57610173565b80637a9e5e4b146104305780638da5cb5b1461047457806395d89b41146104be5780639dc29fac146104dc578063a0712d681461052a578063a9059cbb1461055857610173565b8063313ce56711610130578063313ce567146102ee57806340c10f191461030c57806342966c681461035a5780635ac801fe1461038857806370a08231146103b657806375f12b211461040e57610173565b806306fdde031461017857806307da68f514610196578063095ea7b3146101a057806313af40351461020657806318160ddd1461024a57806323b872dd14610268575b600080fd5b6101806107f0565b6040518082815260200191505060405180910390f35b61019e6107f6565b005b6101ec600480360360408110156101b657600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050610970565b604051808215151515815260200191505060405180910390f35b6102486004803603602081101561021c57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050610a07565b005b610252610b50565b6040518082815260200191505060405180910390f35b6102d46004803603606081101561027e57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050610b59565b604051808215151515815260200191505060405180910390f35b6102f66110f1565b6040518082815260200191505060405180910390f35b6103586004803603604081101561032257600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803590602001909291905050506110f7565b005b6103866004803603602081101561037057600080fd5b810190808035906020019092919050505061130a565b005b6103b46004803603602081101561039e57600080fd5b8101908080359060200190929190505050611317565b005b6103f8600480360360208110156103cc57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff1690602001909291905050506113c1565b6040518082815260200191505060405180910390f35b61041661140a565b604051808215151515815260200191505060405180910390f35b6104726004803603602081101561044657600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919050505061141d565b005b61047c611566565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b6104c661158c565b6040518082815260200191505060405180910390f35b610528600480360360408110156104f257600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611592565b005b6105566004803603602081101561054057600080fd5b8101908080359060200190929190505050611b30565b005b6105a46004803603604081101561056e57600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611b3d565b604051808215151515815260200191505060405180910390f35b61060a600480360360408110156105d457600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611b52565b005b6106786004803603606081101561062257600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611b62565b005b610682611b73565b005b61068c611ced565b604051808273ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200191505060405180910390f35b610710600480360360208110156106e457600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050611d13565b604051808215151515815260200191505060405180910390f35b61078c6004803603604081101561074057600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff169060200190929190803573ffffffffffffffffffffffffffffffffffffffff169060200190929190505050611dc9565b6040518082815260200191505060405180910390f35b6107ee600480360360408110156107b857600080fd5b81019080803573ffffffffffffffffffffffffffffffffffffffff16906020019092919080359060200190929190505050611e50565b005b60075481565b610824336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b610896576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b60008060006004359250602435915034905081833373ffffffffffffffffffffffffffffffffffffffff166000357fffffffff00000000000000000000000000000000000000000000000000000000167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19168460003660405180848152602001806020018281038252848482818152602001925080828437600081840152601f19601f82011690508083019250505094505050505060405180910390a46001600460146101000a81548160ff021916908315150217905550505050565b6000600460149054906101000a900460ff16156109f5576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b6109ff83836120bb565b905092915050565b610a35336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b610aa7576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b80600460006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff160217905550600460009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff167fce241d7ca1f669fee44b6fc00b8eba2df3bb514eed0f6f668f8f89096e81ed9460405160405180910390a250565b60008054905090565b6000600460149054906101000a900460ff1615610bde576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b3373ffffffffffffffffffffffffffffffffffffffff168473ffffffffffffffffffffffffffffffffffffffff1614158015610cb657507fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414155b15610eb45781600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015610dad576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601e8152602001807f64732d746f6b656e2d696e73756666696369656e742d617070726f76616c000081525060200191505060405180910390fd5b610e33600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054836121ad565b600260008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505b81600160008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015610f69576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601d8152602001807f64732d746f6b656e2d696e73756666696369656e742d62616c616e636500000081525060200191505060405180910390fd5b610fb2600160008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054836121ad565b600160008673ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000208190555061103e600160008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205483612230565b600160008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055508273ffffffffffffffffffffffffffffffffffffffff168473ffffffffffffffffffffffffffffffffffffffff167fddf252ad1be2c89b69c2b068fc378daa952ba7f163c4a11628f55a4df523b3ef846040518082815260200191505060405180910390a3600190509392505050565b60065481565b611125336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b611197576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b600460149054906101000a900460ff161561121a576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b611263600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205482612230565b600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055506112b260005482612230565b6000819055508173ffffffffffffffffffffffffffffffffffffffff167f0f6798a560793a54c3bcfe86a93cde1e73087d944c0ea20544137d4121396885826040518082815260200191505060405180910390a25050565b6113143382611592565b50565b611345336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b6113b7576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b8060078190555050565b6000600160008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020549050919050565b600460149054906101000a900460ff1681565b61144b336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b6114bd576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b80600360006101000a81548173ffffffffffffffffffffffffffffffffffffffff021916908373ffffffffffffffffffffffffffffffffffffffff160217905550600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff167f1abebea81bfa2637f28358c371278fb15ede7ea8dd28d2e03b112ff6d936ada460405160405180910390a250565b600460009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b60055481565b6115c0336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b611632576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b600460149054906101000a900460ff16156116b5576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b3373ffffffffffffffffffffffffffffffffffffffff168273ffffffffffffffffffffffffffffffffffffffff161415801561178d57507fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020019081526020016000205414155b1561198b5780600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015611884576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601e8152602001807f64732d746f6b656e2d696e73756666696369656e742d617070726f76616c000081525060200191505060405180910390fd5b61190a600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054826121ad565b600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055505b80600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020541015611a40576040517f08c379a000000000000000000000000000000000000000000000000000000000815260040180806020018281038252601d8152602001807f64732d746f6b656e2d696e73756666696369656e742d62616c616e636500000081525060200191505060405180910390fd5b611a89600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054826121ad565b600160008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002081905550611ad8600054826121ad565b6000819055508173ffffffffffffffffffffffffffffffffffffffff167fcc16f5dbb4873280815c1ee09dbd06736cffcc184412cf7a71a0fdb75d397ca5826040518082815260200191505060405180910390a25050565b611b3a33826110f7565b50565b6000611b4a338484610b59565b905092915050565b611b5d338383610b59565b505050565b611b6d838383610b59565b50505050565b611ba1336000357fffffffff0000000000000000000000000000000000000000000000000000000016611e60565b611c13576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d617574682d756e617574686f72697a656400000000000000000000000081525060200191505060405180910390fd5b60008060006004359250602435915034905081833373ffffffffffffffffffffffffffffffffffffffff166000357fffffffff00000000000000000000000000000000000000000000000000000000167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19168460003660405180848152602001806020018281038252848482818152602001925080828437600081840152601f19601f82011690508083019250505094505050505060405180910390a46000600460146101000a81548160ff021916908315150217905550505050565b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1681565b6000600460149054906101000a900460ff1615611d98576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260128152602001807f64732d73746f702d69732d73746f70706564000000000000000000000000000081525060200191505060405180910390fd5b611dc2827fffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffffff6120bb565b9050919050565b6000600260008473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002054905092915050565b611e5b823383610b59565b505050565b60003073ffffffffffffffffffffffffffffffffffffffff168373ffffffffffffffffffffffffffffffffffffffff161415611e9f57600190506120b5565b600460009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168373ffffffffffffffffffffffffffffffffffffffff161415611efe57600190506120b5565b600073ffffffffffffffffffffffffffffffffffffffff16600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff161415611f5e57600090506120b5565b600360009054906101000a900473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1663b70096138430856040518463ffffffff1660e01b8152600401808473ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff1681526020018373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001827bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19167bffffffffffffffffffffffffffffffffffffffffffffffffffffffff19168152602001935050505060206040518083038186803b15801561207757600080fd5b505afa15801561208b573d6000803e3d6000fd5b505050506040513d60208110156120a157600080fd5b810190808051906020019092919050505090505b92915050565b600081600260003373ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff16815260200190815260200160002060008573ffffffffffffffffffffffffffffffffffffffff1673ffffffffffffffffffffffffffffffffffffffff168152602001908152602001600020819055508273ffffffffffffffffffffffffffffffffffffffff163373ffffffffffffffffffffffffffffffffffffffff167f8c5be1e5ebec7d5bd14f71427d1e84f3dd0314c0f7b2291e5b200ac8c7c3b925846040518082815260200191505060405180910390a36001905092915050565b600082828403915081111561222a576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260158152602001807f64732d6d6174682d7375622d756e646572666c6f77000000000000000000000081525060200191505060405180910390fd5b92915050565b60008282840191508110156122ad576040517f08c379a00000000000000000000000000000000000000000000000000000000081526004018080602001828103825260148152602001807f64732d6d6174682d6164642d6f766572666c6f7700000000000000000000000081525060200191505060405180910390fd5b9291505056fea265627a7a7231582042e4b52e52d434217b55a1ee90f412a7c49b1fd0406bb9ec1168e2a7c1fbad0e64736f6c634300050c0032\"", "sort": {"node": "KSort", "name": "String"}}], "arity": 1, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<storage>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "2", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "ABI_src", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "CALLER_ID", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KVariable", "name": "Allowance", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "ABI_src", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KVariable", "name": "Gem_s", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "ABI_dst", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KVariable", "name": "Gem_d", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KToken", "token": "4", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "#WordPackAddrUInt8(_,_)_WORD-PACK_Int_Int_Int", "params": []}, "args": [{"node": "KVariable", "name": "Owner", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Stopped", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KVariable", "name": "ACCT_ID_STORAGE", "sort": {"node": "KSort", "name": "Map"}}], "arity": 2, "variable": false}, "rhs": {"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "2", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "ABI_src", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "CALLER_ID", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "ite", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_==Int_", "params": []}, "args": [{"node": "KVariable", "name": "Allowance", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639935", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KVariable", "name": "Allowance", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "_-Int_", "params": []}, "args": [{"node": "KVariable", "name": "Allowance", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ABI_wad", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 3, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "ABI_src", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_-Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_s", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ABI_wad", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "ABI_dst", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_+Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_d", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ABI_wad", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KToken", "token": "4", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "#WordPackAddrUInt8(_,_)_WORD-PACK_Int_Int_Int", "params": []}, "args": [{"node": "KVariable", "name": "Owner", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Stopped", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KVariable", "name": "ACCT_ID_STORAGE", "sort": {"node": "KSort", "name": "Map"}}], "arity": 2, "variable": false}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<origStorage>", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_Map_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "2", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "ABI_src", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "CALLER_ID", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KVariable", "name": "Junk_0", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "ABI_src", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KVariable", "name": "Junk_1", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_|->_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "hashLoc", "params": []}, "args": [{"node": "KToken", "token": "\"Solidity\"", "sort": {"node": "KSort", "name": "String"}}, {"node": "KToken", "token": "1", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "intList", "params": []}, "args": [{"node": "KVariable", "name": "ABI_dst", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": ".List{\"intList\"}", "params": []}, "args": [], "arity": 0, "variable": false}], "arity": 2, "variable": false}], "arity": 3, "variable": false}, {"node": "KVariable", "name": "Junk_2", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KVariable", "name": "ACCT_ID_ORIG_STORAGE", "sort": {"node": "KSort", "name": "Map"}}], "arity": 2, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<transientStorage>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen42", "sort": {"node": "KSort", "name": "Map"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<nonce>", "params": []}, "args": [{"node": "KVariable", "name": "Nonce_DSToken", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}], "arity": 7, "variable": false}, {"node": "KVariable", "name": "_DotVar4", "sort": {"node": "KSort", "name": "AccountCellMap"}}], "arity": 2, "variable": false}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<txOrder>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen43", "sort": {"node": "KSort", "name": "List"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<txPending>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen44", "sort": {"node": "KSort", "name": "List"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<messages>", "params": []}, "args": [{"node": "KVariable", "name": "_Gen45", "sort": {"node": "KSort", "name": "MessageCellMap"}}], "arity": 1, "variable": false}, {"node": "KVariable", "name": "_Gen5", "sort": {"node": "KSort", "name": "WithdrawalsPendingCell"}}, {"node": "KVariable", "name": "_Gen6", "sort": {"node": "KSort", "name": "WithdrawalsOrderCell"}}, {"node": "KVariable", "name": "_Gen7", "sort": {"node": "KSort", "name": "WithdrawalsCell"}}], "arity": 8, "variable": false}], "arity": 2, "variable": false}], "arity": 6, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "<generatedCounter>", "params": []}, "args": [{"node": "KRewrite", "lhs": {"node": "KVariable", "name": "_Gen46", "sort": {"node": "KSort", "name": "Int"}}, "rhs": {"node": "KVariable", "name": "?_Gen47", "sort": {"node": "KSort", "name": "Int"}}}], "arity": 1, "variable": false}], "arity": 2, "variable": false}, "requires": {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ACCT_ID", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "1461501637330902918203684832716283019655932542976", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_=/=Int_", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "#notPrecompileAddress(_)_LEMMAS-MCD-SYNTAX_Bool_Int", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "CALLER_ID", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "CALLER_ID", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "1461501637330902918203684832716283019655932542976", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ORIGIN_ID", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "ORIGIN_ID", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "1461501637330902918203684832716283019655932542976", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "TIME", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "TIME", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ACCT_ID_balance", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "ACCT_ID_balance", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KVariable", "name": "VCallDepth", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "1024", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "VCallValue", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "VCallValue", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "VChainId", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "VChainId", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ABI_src", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "ABI_src", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "1461501637330902918203684832716283019655932542976", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ABI_dst", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "ABI_dst", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "1461501637330902918203684832716283019655932542976", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ABI_wad", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "ABI_wad", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Gem_s", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_s", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Gem_d", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_d", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Allowance", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Allowance", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Owner", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Owner", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "1461501637330902918203684832716283019655932542976", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Stopped", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Stopped", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "2", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "lengthBytes(_)_BYTES-HOOKED_Int_Bytes", "params": []}, "args": [{"node": "KVariable", "name": "CD", "sort": {"node": "KSort", "name": "Bytes"}}], "arity": 1, "variable": false}, {"node": "KToken", "token": "1250000000", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "#notPrecompileAddress(_)_LEMMAS-MCD-SYNTAX_Bool_Int", "params": []}, "args": [{"node": "KVariable", "name": "Owner", "sort": {"node": "KSort", "name": "Int"}}], "arity": 1, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_=/=Int_", "params": []}, "args": [{"node": "KVariable", "name": "ABI_src", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ABI_dst", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_=/=Int_", "params": []}, "args": [{"node": "KVariable", "name": "ABI_src", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "CALLER_ID", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Junk_0", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Junk_0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Junk_1", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Junk_1", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Junk_2", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Junk_2", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "_-Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_s", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ABI_wad", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_-Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_s", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ABI_wad", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KApply", "label": {"node": "KLabel", "name": "_+Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_d", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ABI_wad", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_+Int_", "params": []}, "args": [{"node": "KVariable", "name": "Gem_d", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "ABI_wad", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639936", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_orBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_==Int_", "params": []}, "args": [{"node": "KVariable", "name": "Allowance", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "115792089237316195423570985008687907853269984665640564039457584007913129639935", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KVariable", "name": "ABI_wad", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Allowance", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_==Int_", "params": []}, "args": [{"node": "KVariable", "name": "VCallValue", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_==Int_", "params": []}, "args": [{"node": "KVariable", "name": "Stopped", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_andBool_", "params": []}, "args": [{"node": "KApply", "label": {"node": "KLabel", "name": "_<=Int_", "params": []}, "args": [{"node": "KToken", "token": "0", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KVariable", "name": "Nonce_DSToken", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}, {"node": "KApply", "label": {"node": "KLabel", "name": "_<Int_", "params": []}, "args": [{"node": "KVariable", "name": "Nonce_DSToken", "sort": {"node": "KSort", "name": "Int"}}, {"node": "KToken", "token": "18446744073709551615", "sort": {"node": "KSort", "name": "Int"}}], "arity": 2, "variable": false}], "arity": 2, "variable": false}], "arity": 2, "variable": false}, "ensures": {"node": "KToken", "token": "true", "sort": {"node": "KSort", "name": "Bool"}}, "att": {"node": "KAtt", "att": {"org.kframework.definition.Production": {"node": "KProduction", "klabel": {"node": "KLabel", "name": "#ruleRequires", "params": []}, "productionItems": [{"node": "KNonTerminal", "sort": {"node": "KSort", "name": "#RuleBody"}}, {"node": "KTerminal", "value": "requires"}, {"node": "KNonTerminal", "sort": {"node": "KSort", "name": "Bool"}}], "params": [], "sort": {"node": "KSort", "name": "#RuleContent"}, "att": {"node": "KAtt", "att": {"symbol": "#ruleRequires", "org.kframework.attributes.Location": [346, 27, 346, 94], "org.kframework.attributes.Source": "/nix/store/b9ydnz6rpq5gmya15cacdzhlsskadqsw-k-7.1.244-9922ec2536765c1370fd83914a006961d9149326/include/kframework/builtin/kast.md"}}}, "UNIQUE_ID": "0868a17bb9b1186f21ec9c07799c624cf834f4fe0cbdbee6bfa78b61b1a5ec85", "label": "FLAPPER-YANK-PASS-ROUGH-SPEC.DSToken.move.pass", "trusted": "", "org.kframework.attributes.Source": "/home/anvacaru/dev/evm-semantics/eip-7691/tests/specs/mcd-structured/flapper-yank-pass-rough-spec.k", "org.kframework.attributes.Location": [171, 7, 306, 42]}}}], "imports": [{"node": "KImport", "name": "VERIFICATION", "isPublic": true}], "att": {"node": "KAtt", "att": {"org.kframework.attributes.Location": [3, 1, 310, 10], "org.kframework.attributes.Source": "/home/anvacaru/dev/evm-semantics/eip-7691/tests/specs/mcd-structured/flapper-yank-pass-rough-spec.k", "digest": "b2OnZXcrfj45bCWGgCiCaVdThfYDi+CHdHzIAepJk58="}}}]}, "digest": "1fa9654d472b1c67253b8b56f9812d044d91659da10823b96d32003bc05bcea2"}
\ No newline at end of file
diff --git a/tests/specs/mcd-structured/verification.k b/tests/specs/mcd-structured/verification.k
index aaec5beecb..d7ce5f1c2b 100644
--- a/tests/specs/mcd-structured/verification.k
+++ b/tests/specs/mcd-structured/verification.k
@@ -404,8 +404,9 @@ module LEMMAS-MCD [symbolic]
   // #buf simplification comparing to null-bytes: compare as Int
   rule #buf(N, X:Int) ==K NULLBYTES => X ==Int 0
     requires 0 <=Int X
-     andBool X <=Int 2 ^Int ( 8 *Int N)
+     andBool X <Int 2 ^Int ( 8 *Int N)
      andBool #asInteger(NULLBYTES) ==Int 0
-    [simplification, concrete(NULLBYTES)]
+     andBool lengthBytes(NULLBYTES) ==Int N
+    [simplification, concrete(NULLBYTES), preserves-definedness]
 
 endmodule