diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py index a9169b5a1..5f5e346cd 100644 --- a/src/kontrol/prove.py +++ b/src/kontrol/prove.py @@ -1064,6 +1064,7 @@ def _init_cterm( 'ACCESSEDSTORAGE_CELL': map_empty(), 'INTERIMSTATES_CELL': list_empty(), 'TOUCHEDACCOUNTS_CELL': set_empty(), + 'CREATEDACCOUNTS_CELL': set_empty(), 'STATIC_CELL': FALSE, 'ACCOUNTS_CELL': KEVM.accounts(init_account_list), } diff --git a/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected b/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected index 2b167bd20..30ef0fb59 100644 --- a/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected +++ b/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected @@ -107,6 +107,9 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0 .Map + + .Set + ... diff --git a/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected b/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected index fa455752b..3509a9af7 100644 --- a/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected +++ b/src/tests/integration/test-data/show/AddrTest.test_addr_true().trace.expected @@ -108,6 +108,9 @@ module SUMMARY-TEST%ADDRTEST.TEST-ADDR-TRUE():0 .Map + + .Set + ... diff --git a/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected index 02d97d7ed..0f4005130 100644 --- a/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected +++ b/src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected @@ -141,6 +141,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 .Map + + .Set + ... @@ -380,6 +383,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 .Map + + .Set + ... @@ -618,6 +624,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 .Map + + .Set + ... @@ -858,6 +867,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 .Map + + .Set + ... @@ -1098,6 +1110,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0 .Map + + .Set + ... diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected b/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected index bb12fb751..cad3904ce 100644 --- a/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected +++ b/src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected @@ -141,6 +141,9 @@ Node 10: .Map + + .Set + ... @@ -384,6 +387,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 .Map + + .Set + ... @@ -623,6 +629,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 .Map + + .Set + ... @@ -861,6 +870,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 .Map + + .Set + ... @@ -1101,6 +1113,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 .Map + + .Set + ... @@ -1341,6 +1356,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0 .Map + + .Set + ... diff --git a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected index 72e75126d..c059452a2 100644 --- a/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected +++ b/src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected @@ -227,6 +227,9 @@ Node 20: .Map + + .Set + ... @@ -475,6 +478,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + ... @@ -714,6 +720,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + ... @@ -952,6 +961,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + ... @@ -1192,6 +1204,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + ... @@ -1435,6 +1450,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + ... @@ -1682,6 +1700,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + ... @@ -1970,6 +1991,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + } ) ) @@ -2024,6 +2048,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + ORIGIN_ID:Int @@ -2309,6 +2336,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + } ) @@ -2363,6 +2393,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + ORIGIN_ID:Int @@ -2649,6 +2682,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + } ) @@ -2703,6 +2739,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + ORIGIN_ID:Int @@ -2992,6 +3031,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + } ) @@ -3046,6 +3088,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + ORIGIN_ID:Int @@ -3335,6 +3380,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + } ) @@ -3389,6 +3437,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + ORIGIN_ID:Int @@ -3681,6 +3732,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + } ) @@ -3735,6 +3789,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + ORIGIN_ID:Int @@ -4027,6 +4084,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + } ) => .List ) @@ -4081,6 +4141,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + ORIGIN_ID:Int @@ -4325,6 +4388,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + ... @@ -4570,6 +4636,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0 .Map + + .Set + ... diff --git a/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected b/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected index c98a79a22..e1d963a32 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected +++ b/src/tests/integration/test-data/show/AssertTest.test_assert_false().expected @@ -138,6 +138,9 @@ Node 10: .Map + + .Set + ... @@ -381,6 +384,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 .Map + + .Set + ... @@ -620,6 +626,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 .Map + + .Set + ... @@ -858,6 +867,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 .Map + + .Set + ... @@ -1098,6 +1110,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 .Map + + .Set + ... @@ -1338,6 +1353,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0 .Map + + .Set + ... diff --git a/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected b/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected index 984ed7556..60c34dd20 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected +++ b/src/tests/integration/test-data/show/AssertTest.test_assert_true().expected @@ -144,6 +144,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 .Map + + .Set + ... @@ -383,6 +386,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 .Map + + .Set + ... @@ -621,6 +627,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 .Map + + .Set + ... @@ -861,6 +870,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 .Map + + .Set + ... @@ -1101,6 +1113,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0 .Map + + .Set + ... diff --git a/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected b/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected index 9fe428d32..91b8973a1 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected +++ b/src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected @@ -201,6 +201,9 @@ Node 16: .Map + + .Set + ... @@ -447,6 +450,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 .Map + + .Set + ... @@ -686,6 +692,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 .Map + + .Set + ... @@ -927,6 +936,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 .Map + + .Set + ... @@ -1167,6 +1179,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 .Map + + .Set + ... @@ -1408,6 +1423,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 .Map + + .Set + ... @@ -1651,6 +1669,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 .Map + + .Set + ... @@ -1894,6 +1915,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 .Map + + .Set + ... @@ -2137,6 +2161,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 .Map + + .Set + ... @@ -2380,6 +2407,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0 .Map + + .Set + ... diff --git a/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected b/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected index 3ce2a1231..6b41bfd24 100644 --- a/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected @@ -199,6 +199,9 @@ Node 16: .Map + + .Set + ... @@ -447,6 +450,9 @@ Node 15: .Map + + .Set + ... @@ -695,6 +701,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 .Map + + .Set + ... @@ -934,6 +943,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 .Map + + .Set + ... @@ -1177,6 +1189,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 .Map + + .Set + ... @@ -1419,6 +1434,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 .Map + + .Set + ... @@ -1662,6 +1680,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 .Map + + .Set + ... @@ -1907,6 +1928,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 .Map + + .Set + ... @@ -2152,6 +2176,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 .Map + + .Set + ... @@ -2397,6 +2424,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 .Map + + .Set + ... @@ -2642,6 +2672,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0 .Map + + .Set + ... diff --git a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected index 83101bf70..4e7c3f7ae 100644 --- a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_false(uint256,uint256).expected @@ -139,6 +139,9 @@ Node 7: .Map + + .Set + ... @@ -385,6 +388,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 .Map + + .Set + ... @@ -630,6 +636,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 .Map + + .Set + ... @@ -876,6 +885,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 .Map + + .Set + ... @@ -1122,6 +1134,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 .Map + + .Set + ... @@ -1366,6 +1381,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0 .Map + + .Set + ... diff --git a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected index 261403030..fd3dfa906 100644 --- a/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.testFail_assume_true(uint256,uint256).expected @@ -165,6 +165,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 .Map + + .Set + ... @@ -410,6 +413,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 .Map + + .Set + ... @@ -655,6 +661,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 .Map + + .Set + ... @@ -898,6 +907,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 .Map + + .Set + ... @@ -1144,6 +1156,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 .Map + + .Set + ... @@ -1391,6 +1406,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 .Map + + .Set + ... @@ -1637,6 +1655,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 .Map + + .Set + ... @@ -1883,6 +1904,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0 .Map + + .Set + ... diff --git a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected index 4821c1e32..0f428cc54 100644 --- a/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected +++ b/src/tests/integration/test-data/show/AssumeTest.test_assume_false(uint256,uint256).expected @@ -163,6 +163,9 @@ Node 10: .Map + + .Set + ... @@ -411,6 +414,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 .Map + + .Set + ... @@ -656,6 +662,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 .Map + + .Set + ... @@ -901,6 +910,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 .Map + + .Set + ... @@ -1144,6 +1156,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 .Map + + .Set + ... @@ -1390,6 +1405,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 .Map + + .Set + ... @@ -1637,6 +1655,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 .Map + + .Set + ... @@ -1883,6 +1904,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 .Map + + .Set + ... @@ -2129,6 +2153,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0 .Map + + .Set + ... diff --git a/src/tests/integration/test-data/show/BMCBoundTest.testBound().expected b/src/tests/integration/test-data/show/BMCBoundTest.testBound().expected index 116a0d6a5..70a3077f3 100644 --- a/src/tests/integration/test-data/show/BMCBoundTest.testBound().expected +++ b/src/tests/integration/test-data/show/BMCBoundTest.testBound().expected @@ -311,6 +311,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 .Map + + .Set + ... @@ -555,6 +558,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 .Map + + .Set + ... @@ -799,6 +805,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 .Map + + .Set + ... @@ -1044,6 +1053,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 .Map + + .Set + ... @@ -1290,6 +1302,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 .Map + + .Set + ... @@ -1534,6 +1549,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 .Map + + .Set + ... @@ -1779,6 +1797,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 .Map + + .Set + ... @@ -2021,6 +2042,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 .Map + + .Set + ... @@ -2264,6 +2288,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 .Map + + .Set + ... @@ -2508,6 +2535,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 .Map + + .Set + ... @@ -2753,6 +2783,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 .Map + + .Set + ... @@ -2994,6 +3027,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 .Map + + .Set + ... @@ -3236,6 +3272,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 .Map + + .Set + ... @@ -3479,6 +3518,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0 .Map + + .Set + ... diff --git a/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected b/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected index e4f34636b..cb918e8fe 100644 --- a/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected +++ b/src/tests/integration/test-data/show/BlockParamsTest.testWarp(uint256).trace.expected @@ -108,6 +108,9 @@ module SUMMARY-TEST%BLOCKPARAMSTEST.TESTWARP(UINT256):0 .Map + + .Set + ... diff --git a/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected b/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected index 0691827b9..74e0c344d 100644 --- a/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected +++ b/src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected @@ -144,6 +144,9 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 .Map + + ( .Set => SetItem ( 491460923342184218035706888008750043977755113263 ) ) + ... @@ -424,6 +427,9 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 .Map + + ( SetItem ( 491460923342184218035706888008750043977755113263 ) => .Set ) + ... @@ -683,6 +689,9 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 .Map + + .Set + ... @@ -944,6 +953,9 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 .Map + + .Set + ... @@ -1205,6 +1217,9 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0 .Map + + .Set + ... diff --git a/src/tests/integration/test-data/show/gas-abstraction.expected b/src/tests/integration/test-data/show/gas-abstraction.expected index aea903c74..1822c744d 100644 --- a/src/tests/integration/test-data/show/gas-abstraction.expected +++ b/src/tests/integration/test-data/show/gas-abstraction.expected @@ -139,6 +139,9 @@ Node 6: .Map + + .Set + GASPRICE_CELL:Int @@ -483,6 +486,9 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 .Map + + .Set + ... @@ -718,6 +724,9 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 .Map + + .Set + ... @@ -953,6 +962,9 @@ module SUMMARY-TEST%GASTEST.TESTINFINITEGAS():0 .Map + + .Set + ... diff --git a/src/tests/integration/test-data/show/merge-loop-heads.expected b/src/tests/integration/test-data/show/merge-loop-heads.expected index b2cb61ed6..295cb4771 100644 --- a/src/tests/integration/test-data/show/merge-loop-heads.expected +++ b/src/tests/integration/test-data/show/merge-loop-heads.expected @@ -281,6 +281,9 @@ Node 21: .Map + + .Set + ... @@ -530,6 +533,9 @@ Node 22: .Map + + .Set + ... @@ -779,6 +785,9 @@ Node 23: .Map + + .Set + ... @@ -1025,6 +1034,9 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 .Map + + .Set + ... @@ -1265,6 +1277,9 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 .Map + + .Set + ... @@ -1506,6 +1521,9 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 .Map + + .Set + ... @@ -1748,6 +1766,9 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 .Map + + .Set + ... @@ -1992,6 +2013,9 @@ module SUMMARY-TEST%BMCLOOPSTEST.TEST-BMC(UINT256):0 .Map + + .Set + ... diff --git a/src/tests/integration/test-data/show/node-refutation.expected b/src/tests/integration/test-data/show/node-refutation.expected index 2afbd476a..5e67920d3 100644 --- a/src/tests/integration/test-data/show/node-refutation.expected +++ b/src/tests/integration/test-data/show/node-refutation.expected @@ -159,6 +159,9 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 .Map + + .Set + ... @@ -400,6 +403,9 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 .Map + + .Set + ... @@ -644,6 +650,9 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 .Map + + .Set + ... @@ -888,6 +897,9 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0 .Map + + .Set + ... diff --git a/src/tests/integration/test-data/show/split-node.expected b/src/tests/integration/test-data/show/split-node.expected index e7d7ea278..2623e4990 100644 --- a/src/tests/integration/test-data/show/split-node.expected +++ b/src/tests/integration/test-data/show/split-node.expected @@ -734,6 +734,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + ( .Set => SetItem ( 491460923342184218035706888008750043977755113263 ) ) + ... @@ -1014,6 +1017,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + ( SetItem ( 491460923342184218035706888008750043977755113263 ) => .Set ) + ... @@ -1276,6 +1282,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -1539,6 +1548,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -1804,6 +1816,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -2070,6 +2085,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -2350,6 +2368,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -2630,6 +2651,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -2911,6 +2935,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -3235,6 +3262,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -3515,6 +3545,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -3795,6 +3828,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -4075,6 +4111,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -4441,6 +4480,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) ) @@ -4495,6 +4537,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -4836,6 +4881,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) ) @@ -4890,6 +4938,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -5231,6 +5282,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) ) @@ -5285,6 +5339,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -5647,6 +5704,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) ) @@ -5701,6 +5761,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -6064,6 +6127,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -6118,6 +6184,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -6457,6 +6526,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -6511,6 +6583,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -6850,6 +6925,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -6904,6 +6982,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -7264,6 +7345,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -7318,6 +7402,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -7682,6 +7769,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -7736,6 +7826,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -8076,6 +8169,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -8130,6 +8226,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -8470,6 +8569,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -8524,6 +8626,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -8885,6 +8990,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -8939,6 +9047,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -9306,6 +9417,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -9360,6 +9474,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -9703,6 +9820,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -9757,6 +9877,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -10100,6 +10223,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -10154,6 +10280,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -10518,6 +10647,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -10572,6 +10704,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -10939,6 +11074,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -10993,6 +11131,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -11336,6 +11477,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -11390,6 +11534,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -11733,6 +11880,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -11787,6 +11937,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -12151,6 +12304,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -12205,6 +12361,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -12575,6 +12734,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -12629,6 +12791,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -12975,6 +13140,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -13029,6 +13197,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -13375,6 +13546,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -13429,6 +13603,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -13796,6 +13973,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) @@ -13850,6 +14030,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -14220,6 +14403,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) => .List ) @@ -14274,6 +14460,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -14620,6 +14809,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) => .List ) @@ -14674,6 +14866,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -15020,6 +15215,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) => .List ) @@ -15074,6 +15272,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -15441,6 +15642,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + } ) => .List ) @@ -15495,6 +15699,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ORIGIN_ID:Int @@ -15801,6 +16008,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -16083,6 +16293,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -16365,6 +16578,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -16647,6 +16863,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -16955,6 +17174,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -17238,6 +17460,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -17521,6 +17746,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -17804,6 +18032,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -18108,6 +18339,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -18387,6 +18621,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -18666,6 +18903,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -18945,6 +19185,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -19249,6 +19492,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -19528,6 +19774,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -19807,6 +20056,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ... @@ -20086,6 +20338,9 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0 .Map + + .Set + ...