diff --git a/deps/kevm_release b/deps/kevm_release
index 554b4d0ac..37e27ac56 100644
--- a/deps/kevm_release
+++ b/deps/kevm_release
@@ -1 +1 @@
-1.0.858
+1.0.860
diff --git a/flake.lock b/flake.lock
index 74c2abf5a..8886f8b71 100644
--- a/flake.lock
+++ b/flake.lock
@@ -477,16 +477,16 @@
"uv2nix": "uv2nix_2"
},
"locked": {
- "lastModified": 1754040884,
- "narHash": "sha256-sZnzANvHc2XosqWoedVePKieq3B2V1B8UQ5JlzvCblU=",
+ "lastModified": 1755685688,
+ "narHash": "sha256-F3PVfZvXboPO+exmc/mgTdg13fRkxYv4soVu4gQ1WNU=",
"owner": "runtimeverification",
"repo": "evm-semantics",
- "rev": "426e623182ef5f30f7e474b7b1ea794d27369fc5",
+ "rev": "4829d259e7fced7a5142df6ebe70643ea5a47757",
"type": "github"
},
"original": {
"owner": "runtimeverification",
- "ref": "v1.0.858",
+ "ref": "v1.0.860",
"repo": "evm-semantics",
"type": "github"
}
diff --git a/flake.nix b/flake.nix
index f056f4d9e..023cbbad9 100644
--- a/flake.nix
+++ b/flake.nix
@@ -5,7 +5,7 @@
rv-nix-tools.url = "github:runtimeverification/rv-nix-tools/854d4f05ea78547d46e807b414faad64cea10ae4";
nixpkgs.follows = "rv-nix-tools/nixpkgs";
- kevm.url = "github:runtimeverification/evm-semantics/v1.0.858";
+ kevm.url = "github:runtimeverification/evm-semantics/v1.0.860";
kevm.inputs.nixpkgs.follows = "nixpkgs";
k-framework.follows = "kevm/k-framework";
diff --git a/pyproject.toml b/pyproject.toml
index 1187d951b..d21aec99d 100644
--- a/pyproject.toml
+++ b/pyproject.toml
@@ -8,7 +8,7 @@ version = "1.0.0"
description = "Foundry integration for KEVM"
requires-python = "~=3.10"
dependencies = [
- "kevm-pyk@git+https://github.com/runtimeverification/evm-semantics.git@v1.0.858#subdirectory=kevm-pyk",
+ "kevm-pyk@git+https://github.com/runtimeverification/evm-semantics.git@v1.0.860#subdirectory=kevm-pyk",
"eth-utils>=5,<6",
"pycryptodome>=3.20.0,<4",
"pyevmasm>=0.2.3,<0.3",
diff --git a/src/kontrol/prove.py b/src/kontrol/prove.py
index 8ba7bf07b..3f0f7bf52 100644
--- a/src/kontrol/prove.py
+++ b/src/kontrol/prove.py
@@ -965,6 +965,7 @@ def _init_cterm(
trace_options = TraceOptions({})
jumpdests = bytesToken(_process_jumpdests(bytecode=program))
+ id_cell = KVariable(Foundry.symbolic_contract_id(contract_name), sort=KSort('Int'))
init_subst = {
'MODE_CELL': KApply(evm_chain_options.mode),
'USEGAS_CELL': boolToken(evm_chain_options.usegas),
@@ -974,7 +975,8 @@ def _init_cterm(
'STATUSCODE_CELL': KVariable('STATUSCODE'),
'PROGRAM_CELL': bytesToken(program),
'JUMPDESTS_CELL': jumpdests,
- 'ID_CELL': KVariable(Foundry.symbolic_contract_id(contract_name), sort=KSort('Int')),
+ 'ID_CELL': id_cell,
+ 'CODEADDR_CELL': id_cell,
'ORIGIN_CELL': KVariable('ORIGIN_ID', sort=KSort('Int')),
'CALLER_CELL': KVariable('CALLER_ID', sort=KSort('Int')),
'LOCALMEM_CELL': bytesToken(b''),
@@ -1016,6 +1018,7 @@ def _init_cterm(
'CALLSTACK_CELL': list_empty(),
'CALLDEPTH_CELL': intToken(0),
'ID_CELL': Foundry.address_TEST_CONTRACT(),
+ 'CODEADDR_CELL': Foundry.address_TEST_CONTRACT(),
'ORIGIN_CELL': origin_id,
'CALLER_CELL': caller_id,
'LOG_CELL': list_empty(),
@@ -1397,6 +1400,7 @@ def _final_term(
account_list.append(KVariable('ACCOUNTS_FINAL'))
final_subst_test = {
'ID_CELL': Foundry.address_TEST_CONTRACT(),
+ 'CODEADDR_CELL': Foundry.address_TEST_CONTRACT(),
'ACCOUNTS_CELL': KEVM.accounts(account_list),
}
final_subst.update(final_subst_test)
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 a840dc0a8..0482d4c09 100644
--- a/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected
+++ b/src/tests/integration/test-data/show/AccountParamsTest.testDealConcrete().trace.expected
@@ -92,6 +92,9 @@ module SUMMARY-TEST%ACCOUNTPARAMSTEST.TESTDEALCONCRETE():0
0
+
+ #address ( FoundryTest )
+
...
diff --git a/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected b/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected
index aecfbf2f2..0a2b9ed35 100644
--- a/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected
+++ b/src/tests/integration/test-data/show/AddConst.applyOp(uint256).cse.expected
@@ -126,6 +126,9 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
0
+
+ C_ADDCONST_ID:Int
+
...
@@ -250,9 +253,15 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
andBool ( ( notBool
C_ADDCONST_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ADDCONST_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
0
+
+ C_ADDCONST_ID:Int
+
...
@@ -429,9 +441,15 @@ module SUMMARY-SRC%CSE%ADDCONST.APPLYOP(UINT256):0
andBool ( ( notBool
C_ADDCONST_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ADDCONST_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
0
+
+ #address ( FoundryTest )
+
...
diff --git a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected
index 3ec10017b..e4e81cd9a 100644
--- a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected
+++ b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add(uint256,uint256).cse.expected
@@ -175,6 +175,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
) => .List )
@@ -300,6 +303,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
( 1 => 0 )
+
+ ( 491460923342184218035706888008750043977755113263 => #address ( FoundryTest ) )
+
...
@@ -555,6 +561,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
) )
@@ -680,6 +689,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
( 0 => 1 )
+
+ ( #address ( FoundryTest ) => 491460923342184218035706888008750043977755113263 )
+
...
@@ -959,6 +971,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
) => .List )
@@ -1084,6 +1099,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
( 1 => 0 )
+
+ ( 491460923342184218035706888008750043977755113263 => #address ( FoundryTest ) )
+
...
@@ -1344,6 +1362,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
) => .List )
@@ -1469,6 +1490,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
( 1 => 0 )
+
+ ( 491460923342184218035706888008750043977755113263 => #address ( FoundryTest ) )
+
...
@@ -1730,6 +1754,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
) => .List )
@@ -1855,6 +1882,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD(UINT256,UINT256):0
( 1 => 0 )
+
+ ( 491460923342184218035706888008750043977755113263 => #address ( FoundryTest ) )
+
...
diff --git a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected
index e4d8a2ee7..68e8af5a0 100644
--- a/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected
+++ b/src/tests/integration/test-data/show/ArithmeticCallTest.test_double_add_double_sub(uint256,uint256).cse.expected
@@ -224,6 +224,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
0
+
+ #address ( FoundryTest )
+
...
) => .List )
@@ -349,6 +352,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
( 1 => 0 )
+
+ ( 491460923342184218035706888008750043977755113263 => #address ( FoundryTest ) )
+
...
@@ -604,6 +610,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
0
+
+ #address ( FoundryTest )
+
...
) )
@@ -729,6 +738,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
( 0 => 1 )
+
+ ( #address ( FoundryTest ) => 491460923342184218035706888008750043977755113263 )
+
...
@@ -1008,6 +1020,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
0
+
+ #address ( FoundryTest )
+
...
) => .List )
@@ -1133,6 +1148,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
( 1 => 0 )
+
+ ( 491460923342184218035706888008750043977755113263 => #address ( FoundryTest ) )
+
...
@@ -1393,6 +1411,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
0
+
+ #address ( FoundryTest )
+
...
) => .List )
@@ -1518,6 +1539,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
( 1 => 0 )
+
+ ( 491460923342184218035706888008750043977755113263 => #address ( FoundryTest ) )
+
...
@@ -1779,6 +1803,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
0
+
+ #address ( FoundryTest )
+
...
) => .List )
@@ -1904,6 +1931,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
( 1 => 0 )
+
+ ( 491460923342184218035706888008750043977755113263 => #address ( FoundryTest ) )
+
...
@@ -2105,10 +2135,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
andBool ( KV0_x:Int <=Int ( maxUInt256 -Int KV1_y:Int )
andBool ( ( KV0_x:Int +Int KV1_y:Int ) <=Int ( maxUInt256 -Int KV1_y:Int )
))))))))))))
- ensures ( 0 <=Int ( KV0_x:Int -Int KV1_y:Int )
- andBool ( ( KV0_x:Int +Int KV1_y:Int )
@@ -2169,6 +2198,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
0
+
+ #address ( FoundryTest )
+
...
) => .List )
@@ -2294,6 +2326,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
( 1 => 0 )
+
+ ( 491460923342184218035706888008750043977755113263 => #address ( FoundryTest ) )
+
...
@@ -2496,11 +2531,10 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
andBool ( ( KV0_x:Int +Int KV1_y:Int ) <=Int ( maxUInt256 -Int KV1_y:Int )
andBool ( ( ( ( KV0_x:Int +Int KV1_y:Int ) +Int KV1_y:Int ) -Int ( ( KV0_x:Int -Int KV1_y:Int ) -Int KV1_y:Int ) ) =/=Int 0
)))))))))))))
- ensures ( 0 <=Int ( KV0_x:Int -Int KV1_y:Int )
- andBool ( ( KV0_x:Int +Int KV1_y:Int )
@@ -2561,6 +2595,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
0
+
+ #address ( FoundryTest )
+
...
) => .List )
@@ -2686,6 +2723,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
( 1 => 0 )
+
+ ( 491460923342184218035706888008750043977755113263 => #address ( FoundryTest ) )
+
...
@@ -2888,10 +2928,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-DOUBLE-SUB(UINT256,UINT25
andBool ( ( KV0_x:Int +Int KV1_y:Int ) <=Int ( maxUInt256 -Int KV1_y:Int )
andBool ( 0 ==Int ( ( ( KV0_x:Int +Int KV1_y:Int ) +Int KV1_y:Int ) -Int ( ( KV0_x:Int -Int KV1_y:Int ) -Int KV1_y:Int ) )
)))))))))))))
- ensures ( 0 <=Int ( KV0_x:Int -Int KV1_y:Int )
- andBool ( ( KV0_x:Int +Int KV1_y:Int )
1
+
+ 491460923342184218035706888008750043977755113263
+
...
) ListItem (
@@ -255,6 +258,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
0
+
+ #address ( FoundryTest )
+
...
) )
@@ -465,6 +471,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
( 0 => 2 )
+
+ ( #address ( FoundryTest ) => 491460923342184218035706888008750043977755113263 )
+
...
@@ -751,6 +760,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
1
+
+ 491460923342184218035706888008750043977755113263
+
...
) ListItem (
@@ -783,6 +795,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
0
+
+ #address ( FoundryTest )
+
...
) => .List )
@@ -993,6 +1008,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
( 2 => 0 )
+
+ ( 491460923342184218035706888008750043977755113263 => #address ( FoundryTest ) )
+
...
@@ -1258,6 +1276,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
1
+
+ 491460923342184218035706888008750043977755113263
+
...
) ListItem (
@@ -1290,6 +1311,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
0
+
+ #address ( FoundryTest )
+
...
) => .List )
@@ -1500,6 +1524,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
( 2 => 0 )
+
+ ( 491460923342184218035706888008750043977755113263 => #address ( FoundryTest ) )
+
...
@@ -1766,6 +1793,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
1
+
+ 491460923342184218035706888008750043977755113263
+
...
) ListItem (
@@ -1798,6 +1828,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
0
+
+ #address ( FoundryTest )
+
...
) => .List )
@@ -2008,6 +2041,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
( 2 => 0 )
+
+ ( 491460923342184218035706888008750043977755113263 => #address ( FoundryTest ) )
+
...
@@ -2210,9 +2246,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
andBool ( KV0_x:Int <=Int ( maxUInt256 -Int KV1_y:Int )
andBool ( ( maxUInt256 -Int KV1_y:Int )
@@ -2278,6 +2312,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
1
+
+ 491460923342184218035706888008750043977755113263
+
...
) ListItem (
@@ -2310,6 +2347,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
0
+
+ #address ( FoundryTest )
+
...
) => .List )
@@ -2520,6 +2560,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
( 2 => 0 )
+
+ ( 491460923342184218035706888008750043977755113263 => #address ( FoundryTest ) )
+
...
@@ -2723,9 +2766,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
andBool ( ( ( ( KV0_x:Int +Int KV1_y:Int ) -Int KV2_z:Int ) +Int KV1_y:Int )
@@ -2791,6 +2832,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
1
+
+ 491460923342184218035706888008750043977755113263
+
...
) ListItem (
@@ -2823,6 +2867,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
0
+
+ #address ( FoundryTest )
+
...
) => .List )
@@ -3033,6 +3080,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
( 2 => 0 )
+
+ ( 491460923342184218035706888008750043977755113263 => #address ( FoundryTest ) )
+
...
@@ -3237,9 +3287,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
andBool ( ( ( KV0_x:Int +Int KV1_y:Int ) -Int KV2_z:Int ) <=Int ( maxUInt256 -Int KV1_y:Int )
andBool ( KV0_x:Int
@@ -3305,6 +3353,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
1
+
+ 491460923342184218035706888008750043977755113263
+
...
) ListItem (
@@ -3337,6 +3388,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
0
+
+ #address ( FoundryTest )
+
...
) => .List )
@@ -3547,6 +3601,9 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
( 2 => 0 )
+
+ ( 491460923342184218035706888008750043977755113263 => #address ( FoundryTest ) )
+
...
@@ -3751,9 +3808,7 @@ module SUMMARY-TEST%ARITHMETICCALLTEST.TEST-DOUBLE-ADD-SUB-EXTERNAL(UINT256,UINT
andBool ( ( ( KV0_x:Int +Int KV1_y:Int ) -Int KV2_z:Int ) <=Int ( maxUInt256 -Int KV1_y:Int )
andBool ( ( ( ( ( KV0_x:Int +Int KV1_y:Int ) -Int KV2_z:Int ) +Int KV1_y:Int ) -Int KV2_z:Int ) <=Int KV0_x:Int
)))))))))))))))
- ensures ( 0 <=Int ( ( KV0_x:Int +Int KV1_y:Int ) -Int KV2_z:Int )
- andBool ( ( ( KV0_x:Int +Int KV1_y:Int ) -Int KV2_z:Int )
0
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -250,9 +253,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD(UINT256,UINT256):0
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
andBool ( KV0_x:Int <=Int ( maxUInt256 -Int KV1_y:Int )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
0
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -428,9 +440,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD(UINT256,UINT256):0
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
andBool ( ( maxUInt256 -Int KV1_y:Int )
0
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -1467,9 +1470,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
CALLDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -1667,9 +1679,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -1876,9 +1897,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10 .K =/=K C_ARITHMETICCONTRACT_ID:Int ~> .K
[priority(20), label(BASIC-BLOCK-7-TO-13)]
@@ -1933,6 +1960,9 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -2084,9 +2114,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10 .K =/=K C_ARITHMETICCONTRACT_ID:Int ~> .K
[priority(20), label(BASIC-BLOCK-14-TO-25)]
@@ -2141,6 +2177,9 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -2292,9 +2331,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10 .K =/=K C_ARITHMETICCONTRACT_ID:Int ~> .K
[priority(20), label(BASIC-BLOCK-26-TO-44)]
@@ -2349,6 +2394,9 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -2500,9 +2548,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10 .K =/=K C_ARITHMETICCONTRACT_ID:Int ~> .K
[priority(20), label(BASIC-BLOCK-45-TO-75)]
@@ -2555,6 +2609,9 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
DEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -2712,9 +2769,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -2927,9 +2993,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -3140,9 +3215,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -3352,9 +3436,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -3564,9 +3657,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -3771,9 +3873,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10 .K =/=K C_ARITHMETICCONTRACT_ID:Int ~> .K
[priority(20), label(BASIC-BLOCK-76-TO-123)]
@@ -3826,6 +3934,9 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
DEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -3986,9 +4097,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
DEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -4197,9 +4317,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
CALLDEPTH_CELL:Int
+
+ #address ( FoundryConsole )
+
...
@@ -4403,8 +4532,12 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
#address ( FoundryConsole )
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
CALLDEPTH_CELL:Int
+
+ #address ( FoundryConsole )
+
...
@@ -4608,9 +4744,13 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
#address ( FoundryConsole )
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -4827,9 +4970,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -5040,9 +5192,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -5256,9 +5417,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -5468,9 +5638,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -5684,9 +5863,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -5896,9 +6084,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
DEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -6109,9 +6306,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
DEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -6319,9 +6525,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -6536,9 +6751,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -6748,9 +6972,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -6964,9 +7197,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -7176,9 +7418,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
DEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -7388,9 +7639,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
DEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -7597,9 +7857,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
DEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -7810,9 +8079,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
DEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -8019,9 +8297,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
DEPTH_CELL:Int
+
+ ( C_ARITHMETICCONTRACT_ID:Int => #address ( FoundryConsole ) )
+
...
@@ -8234,9 +8521,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
DEPTH_CELL:Int
+
+ ( C_ARITHMETICCONTRACT_ID:Int => #address ( FoundryConsole ) )
+
...
@@ -8450,9 +8746,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
DEPTH_CELL:Int
+
+ ( C_ARITHMETICCONTRACT_ID:Int => #address ( FoundryConsole ) )
+
...
@@ -8667,9 +8972,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
DEPTH_CELL:Int
+
+ ( C_ARITHMETICCONTRACT_ID:Int => #address ( FoundryConsole ) )
+
...
@@ -8884,9 +9198,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
DEPTH_CELL:Int
+
+ ( C_ARITHMETICCONTRACT_ID:Int => #address ( FoundryConsole ) )
+
...
@@ -9102,9 +9425,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
CALLDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
) CALLSTACK_CELL:List )
@@ -9249,6 +9581,9 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
( CALLDEPTH_CELL:Int => ( CALLDEPTH_CELL:Int +Int 1 ) )
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -9419,9 +9754,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
#address ( FoundryConsole )
@@ -9486,6 +9827,9 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
CALLDEPTH_CELL:Int
+
+ C_ARITHMETICCONTRACT_ID:Int
+
...
@@ -9636,9 +9980,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
#address ( FoundryConsole )
@@ -9700,6 +10050,9 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
EXPECTEDDEPTH_CELL:Int
+
+ ( C_ARITHMETICCONTRACT_ID:Int => #address ( FoundryConsole ) )
+
...
@@ -9860,9 +10213,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ ( C_ARITHMETICCONTRACT_ID:Int => #address ( FoundryConsole ) )
+
...
@@ -10080,9 +10442,15 @@ module SUMMARY-SRC%ARITHMETICCONTRACT.ADD-SUB-EXTERNAL(UINT256,UINT256,UINT256):
andBool ( ( notBool
C_ARITHMETICCONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ARITHMETICCONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
0
+
+ #address ( FoundryTest )
+
...
@@ -359,6 +362,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
0
+
+ #address ( FoundryTest )
+
...
@@ -591,6 +597,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
0
+
+ #address ( FoundryTest )
+
...
@@ -826,6 +835,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
0
+
+ #address ( FoundryTest )
+
...
@@ -1061,6 +1073,9 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
0
+
+ #address ( FoundryTest )
+
...
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 2fee819ab..0368f5787 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
@@ -126,6 +126,9 @@ Node 10:
0
+
+ #address ( FoundryTest )
+
...
@@ -364,6 +367,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0
0
+
+ #address ( FoundryTest )
+
...
@@ -597,6 +603,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0
0
+
+ #address ( FoundryTest )
+
...
@@ -829,6 +838,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0
0
+
+ #address ( FoundryTest )
+
...
@@ -1064,6 +1076,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0
0
+
+ #address ( FoundryTest )
+
...
@@ -1299,6 +1314,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0
0
+
+ #address ( FoundryTest )
+
...
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 5e7d9d060..a4187602d 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
@@ -212,6 +212,9 @@ Node 20:
0
+
+ #address ( FoundryTest )
+
...
@@ -455,6 +458,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
0
+
+ #address ( FoundryTest )
+
...
@@ -688,6 +694,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
0
+
+ #address ( FoundryTest )
+
...
@@ -920,6 +929,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
0
+
+ #address ( FoundryTest )
+
...
@@ -1155,6 +1167,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
0
+
+ #address ( FoundryTest )
+
...
@@ -1393,6 +1408,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
0
+
+ #address ( FoundryTest )
+
...
@@ -1635,6 +1653,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
0
+
+ #address ( FoundryTest )
+
...
@@ -1870,6 +1891,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
0
+
+ #address ( FoundryTest )
+
...
) )
@@ -1972,6 +1996,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
( 0 => 1 )
+
+ #address ( FoundryTest )
+
...
@@ -2207,6 +2234,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
0
+
+ #address ( FoundryTest )
+
...
)
@@ -2309,6 +2339,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
1
+
+ #address ( FoundryTest )
+
...
@@ -2545,6 +2578,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
0
+
+ #address ( FoundryTest )
+
...
)
@@ -2647,6 +2683,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
1
+
+ #address ( FoundryTest )
+
...
@@ -2886,6 +2925,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
0
+
+ #address ( FoundryTest )
+
...
)
@@ -2988,6 +3030,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
1
+
+ #address ( FoundryTest )
+
...
@@ -3227,6 +3272,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
0
+
+ #address ( FoundryTest )
+
...
)
@@ -3329,6 +3377,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
1
+
+ #address ( FoundryTest )
+
...
@@ -3571,6 +3622,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
0
+
+ #address ( FoundryTest )
+
...
)
@@ -3673,6 +3727,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
1
+
+ #address ( FoundryTest )
+
...
@@ -3915,6 +3972,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
0
+
+ #address ( FoundryTest )
+
...
) => .List )
@@ -4017,6 +4077,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
( 1 => 0 )
+
+ #address ( FoundryTest )
+
...
@@ -4259,6 +4322,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
0
+
+ #address ( FoundryTest )
+
...
@@ -4499,6 +4565,9 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
0
+
+ #address ( FoundryTest )
+
...
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 3c631916e..c1289e798 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
@@ -123,6 +123,9 @@ Node 10:
0
+
+ #address ( FoundryTest )
+
...
@@ -361,6 +364,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0
0
+
+ #address ( FoundryTest )
+
...
@@ -594,6 +600,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0
0
+
+ #address ( FoundryTest )
+
...
@@ -826,6 +835,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0
0
+
+ #address ( FoundryTest )
+
...
@@ -1061,6 +1073,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0
0
+
+ #address ( FoundryTest )
+
...
@@ -1296,6 +1311,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0
0
+
+ #address ( FoundryTest )
+
...
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 727ec7615..29daf0708 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
@@ -129,6 +129,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0
0
+
+ #address ( FoundryTest )
+
...
@@ -362,6 +365,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0
0
+
+ #address ( FoundryTest )
+
...
@@ -594,6 +600,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0
0
+
+ #address ( FoundryTest )
+
...
@@ -829,6 +838,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0
0
+
+ #address ( FoundryTest )
+
...
@@ -1064,6 +1076,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0
0
+
+ #address ( FoundryTest )
+
...
diff --git a/src/tests/integration/test-data/show/AssertTest.test_assert_true().trace.expected b/src/tests/integration/test-data/show/AssertTest.test_assert_true().trace.expected
index d9ad87484..e3d51a2a3 100644
--- a/src/tests/integration/test-data/show/AssertTest.test_assert_true().trace.expected
+++ b/src/tests/integration/test-data/show/AssertTest.test_assert_true().trace.expected
@@ -103,6 +103,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0
0
+
+ #address ( FoundryTest )
+
...
@@ -327,6 +330,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0
0
+
+ #address ( FoundryTest )
+
...
@@ -551,6 +557,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0
0
+
+ #address ( FoundryTest )
+
...
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 5af202300..593ceec7d 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
@@ -186,6 +186,9 @@ Node 16:
0
+
+ #address ( FoundryTest )
+
...
@@ -427,6 +430,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -660,6 +666,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -895,6 +904,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -1130,6 +1142,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -1366,6 +1381,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -1604,6 +1622,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -1842,6 +1863,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -2080,6 +2104,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -2318,6 +2345,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0
0
+
+ #address ( FoundryTest )
+
...
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 5ca49201d..dcbc18e0c 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
@@ -184,6 +184,9 @@ Node 16:
0
+
+ #address ( FoundryTest )
+
...
@@ -427,6 +430,9 @@ Node 15:
0
+
+ #address ( FoundryTest )
+
...
@@ -670,6 +676,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -903,6 +912,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -1140,6 +1152,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -1377,6 +1392,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -1615,6 +1633,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -1855,6 +1876,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -2095,6 +2119,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -2335,6 +2362,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -2575,6 +2605,9 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
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 b99f9fc43..e80db4903 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
@@ -124,6 +124,9 @@ Node 7:
0
+
+ #address ( FoundryTest )
+
...
@@ -364,6 +367,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -603,6 +609,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -843,6 +852,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -1083,6 +1095,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -1321,6 +1336,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-FALSE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
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 2a6ad87be..17a4be6b2 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
@@ -150,6 +150,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -389,6 +392,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -628,6 +634,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -865,6 +874,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -1105,6 +1117,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -1346,6 +1361,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -1586,6 +1604,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -1826,6 +1847,9 @@ module SUMMARY-TEST%ASSUMETEST.TESTFAIL-ASSUME-TRUE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
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 98c61f96d..3ec6d54b0 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
@@ -148,6 +148,9 @@ Node 10:
0
+
+ #address ( FoundryTest )
+
...
@@ -390,6 +393,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -629,6 +635,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -868,6 +877,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -1105,6 +1117,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -1345,6 +1360,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -1586,6 +1604,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -1826,6 +1847,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -2066,6 +2090,9 @@ module SUMMARY-TEST%ASSUMETEST.TEST-ASSUME-FALSE(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
diff --git a/src/tests/integration/test-data/show/BMCBoundTest.testBound().expected b/src/tests/integration/test-data/show/BMCBoundTest.testBound().expected
index 1f0c19f70..c3ff87b70 100644
--- a/src/tests/integration/test-data/show/BMCBoundTest.testBound().expected
+++ b/src/tests/integration/test-data/show/BMCBoundTest.testBound().expected
@@ -296,6 +296,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
0
+
+ #address ( FoundryTest )
+
...
@@ -534,6 +537,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
0
+
+ #address ( FoundryTest )
+
...
@@ -772,6 +778,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
0
+
+ #address ( FoundryTest )
+
...
@@ -1011,6 +1020,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
0
+
+ #address ( FoundryTest )
+
...
@@ -1251,6 +1263,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
0
+
+ #address ( FoundryTest )
+
...
@@ -1489,6 +1504,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
0
+
+ #address ( FoundryTest )
+
...
@@ -1728,6 +1746,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
0
+
+ #address ( FoundryTest )
+
...
@@ -1964,6 +1985,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
0
+
+ #address ( FoundryTest )
+
...
@@ -2201,6 +2225,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
0
+
+ #address ( FoundryTest )
+
...
@@ -2364,8 +2391,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
- requires ( 0
@@ -2439,6 +2465,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
0
+
+ #address ( FoundryTest )
+
...
@@ -2602,8 +2631,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
- requires ( 0
@@ -2678,6 +2706,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
0
+
+ #address ( FoundryTest )
+
...
@@ -2914,6 +2945,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
0
+
+ #address ( FoundryTest )
+
...
@@ -3151,6 +3185,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
0
+
+ #address ( FoundryTest )
+
...
@@ -3314,8 +3351,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
- requires ( 0
@@ -3389,6 +3425,9 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
0
+
+ #address ( FoundryTest )
+
...
@@ -3552,8 +3591,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
- requires ( 0
0
+
+ #address ( FoundryTest )
+
...
diff --git a/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected
index fccabc78e..227440c57 100644
--- a/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected
+++ b/src/tests/integration/test-data/show/CSETest.test_add_const(uint256,uint256).cse.expected
@@ -137,6 +137,9 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -444,6 +447,9 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -751,6 +757,9 @@ module SUMMARY-TEST%CSETEST.TEST-ADD-CONST(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
diff --git a/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected b/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected
index c952eb69b..9a252e69a 100644
--- a/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected
+++ b/src/tests/integration/test-data/show/CSETest.test_identity(uint256,uint256).cse.expected
@@ -133,6 +133,9 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -440,6 +443,9 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
@@ -745,6 +751,9 @@ module SUMMARY-TEST%CSETEST.TEST-IDENTITY(UINT256,UINT256):0
0
+
+ #address ( FoundryTest )
+
...
diff --git a/src/tests/integration/test-data/show/CallableStorageContract.str().cse.expected b/src/tests/integration/test-data/show/CallableStorageContract.str().cse.expected
index c21e4c1be..74d34e083 100644
--- a/src/tests/integration/test-data/show/CallableStorageContract.str().cse.expected
+++ b/src/tests/integration/test-data/show/CallableStorageContract.str().cse.expected
@@ -128,6 +128,9 @@ module SUMMARY-TEST%CALLABLESTORAGECONTRACT.STR():0
0
+
+ C_CALLABLESTORAGECONTRACT_ID:Int
+
...
@@ -256,9 +259,15 @@ module SUMMARY-TEST%CALLABLESTORAGECONTRACT.STR():0
andBool ( ( notBool
C_CALLABLESTORAGECONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_CALLABLESTORAGECONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
0
+
+ C_CALLABLESTORAGECONTRACT_ID:Int
+
...
@@ -438,9 +450,15 @@ module SUMMARY-TEST%CALLABLESTORAGECONTRACT.STR():0
andBool ( ( notBool
C_CALLABLESTORAGECONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_CALLABLESTORAGECONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
0
+
+ #address ( FoundryTest )
+
...
diff --git a/src/tests/integration/test-data/show/ConstructorTest.init.cse.expected b/src/tests/integration/test-data/show/ConstructorTest.init.cse.expected
index 37576c63f..ac2f8f703 100644
--- a/src/tests/integration/test-data/show/ConstructorTest.init.cse.expected
+++ b/src/tests/integration/test-data/show/ConstructorTest.init.cse.expected
@@ -91,6 +91,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.INIT:0
0
+
+ #address ( FoundryTest )
+
...
diff --git a/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected b/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected
index 508a01339..b7f4e41ba 100644
--- a/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected
+++ b/src/tests/integration/test-data/show/ConstructorTest.test_contract_call().cse.expected
@@ -93,6 +93,9 @@ module SUMMARY-TEST%CONSTRUCTORTEST.TEST-CONTRACT-CALL():0
0
+
+ #address ( FoundryTest )
+
...
diff --git a/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected b/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected
index 15438381b..66a058f34 100644
--- a/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected
+++ b/src/tests/integration/test-data/show/ContractFieldTest.testEscrowToken().cse.expected
@@ -93,6 +93,9 @@ module SUMMARY-TEST%CONTRACTFIELDTEST.TESTESCROWTOKEN():0
0
+
+ #address ( FoundryTest )
+
...
diff --git a/src/tests/integration/test-data/show/Enum.enum_argument_range(uint8).cse.expected b/src/tests/integration/test-data/show/Enum.enum_argument_range(uint8).cse.expected
index d1829a09e..1631d428a 100644
--- a/src/tests/integration/test-data/show/Enum.enum_argument_range(uint8).cse.expected
+++ b/src/tests/integration/test-data/show/Enum.enum_argument_range(uint8).cse.expected
@@ -86,6 +86,9 @@ module SUMMARY-TEST%ENUM.ENUM-ARGUMENT-RANGE(UINT8):0
0
+
+ C_ENUM_ID:Int
+
...
@@ -240,10 +243,18 @@ module SUMMARY-TEST%ENUM.ENUM-ARGUMENT-RANGE(UINT8):0
C_ENUM_MEMBER_CONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
andBool ( #lookup ( C_ENUM_MEMBER_CONTRACT_STORAGE:Map , 1 )
0
+
+ C_ENUM_ID:Int
+
...
@@ -1531,10 +1534,18 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0
C_ENUM_MEMBER_CONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
andBool ( #lookup ( C_ENUM_MEMBER_CONTRACT_STORAGE:Map , 1 )
CALLDEPTH_CELL:Int
+
+ C_ENUM_ID:Int
+
...
@@ -1758,10 +1772,18 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0
andBool ( ( notBool
C_ENUM_MEMBER_CONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ENUM_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ENUM_MEMBER_CONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ C_ENUM_ID:Int
+
...
@@ -1994,10 +2019,18 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0
andBool ( ( notBool
C_ENUM_MEMBER_CONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ENUM_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ENUM_MEMBER_CONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10 .K =/=K C_ENUM_ID:Int ~> .K
[priority(20), label(BASIC-BLOCK-7-TO-13)]
@@ -2052,6 +2085,9 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0
EXPECTEDDEPTH_CELL:Int
+
+ C_ENUM_ID:Int
+
...
@@ -2229,10 +2265,18 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0
andBool ( ( notBool
C_ENUM_MEMBER_CONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ENUM_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ENUM_MEMBER_CONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10 .K =/=K C_ENUM_ID:Int ~> .K
[priority(20), label(BASIC-BLOCK-14-TO-25)]
@@ -2287,6 +2331,9 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0
EXPECTEDDEPTH_CELL:Int
+
+ C_ENUM_ID:Int
+
...
@@ -2464,10 +2511,18 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0
andBool ( ( notBool
C_ENUM_MEMBER_CONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ENUM_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ENUM_MEMBER_CONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10 .K =/=K C_ENUM_ID:Int ~> .K
[priority(20), label(BASIC-BLOCK-26-TO-44)]
@@ -2522,6 +2577,9 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0
EXPECTEDDEPTH_CELL:Int
+
+ C_ENUM_ID:Int
+
...
@@ -2699,10 +2757,18 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0
andBool ( ( notBool
C_ENUM_MEMBER_CONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ENUM_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ENUM_MEMBER_CONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10 .K =/=K C_ENUM_ID:Int ~> .K
[priority(20), label(BASIC-BLOCK-45-TO-75)]
@@ -2755,6 +2821,9 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0
DEPTH_CELL:Int
+
+ C_ENUM_ID:Int
+
...
@@ -2938,10 +3007,18 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0
andBool ( ( notBool
C_ENUM_MEMBER_CONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ENUM_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ENUM_MEMBER_CONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+
+ C_ENUM_ID:Int
+
...
@@ -3180,10 +3260,18 @@ module SUMMARY-TEST%ENUM.ENUM-STORAGE-RANGE():0
andBool ( ( notBool
C_ENUM_MEMBER_CONTRACT_ID:Int
in_keys ( ACCOUNTS_REST:AccountCellMap ) )
- andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ENUM_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 10 ) )
- andBool ( ( notBool #range ( 0 < C_ENUM_MEMBER_CONTRACT_ID:Int <= 10 ) )
+ andBool ( ( CALLER_ID:Int <=Int 0
+ orBool ( 10
EXPECTEDDEPTH_CELL:Int
+