Skip to content

Commit 330f278

Browse files
PetarMaxpalinatolmachrv-auditor
authored
Simplifying nodes by need (#848)
* Simplifying nodes by need * Update expected output * flake.{nix,lock}: update Nix derivations --------- Co-authored-by: Palina <[email protected]> Co-authored-by: devops <[email protected]>
1 parent 3f97614 commit 330f278

12 files changed

+52
-55
lines changed

‎flake.lock

Lines changed: 3 additions & 3 deletions
Some generated files are not rendered by default. Learn more about customizing how changed files appear on GitHub.

‎src/kontrol/prove.py

Lines changed: 2 additions & 5 deletions
Original file line numberDiff line numberDiff line change
@@ -664,18 +664,15 @@ def _method_to_initialized_cfg(
664664
init_term = KDefinition__expand_macros(foundry.kevm.definition, init_term)
665665
init_cterm = CTerm.from_kast(init_term)
666666
_LOGGER.info(f'Computing definedness constraint for node {node_id} for test: {test.name}')
667-
init_cterm = kcfg_explore.cterm_symbolic.assume_defined(init_cterm)
667+
init_cterm, _ = kcfg_explore.cterm_symbolic.simplify(kcfg_explore.cterm_symbolic.assume_defined(init_cterm))
668668
kcfg.let_node(node_id, cterm=init_cterm)
669669

670670
_LOGGER.info(f'Expanding macros in target state for test: {test.name}')
671671
target_term = kcfg.node(target_node_id).cterm.kast
672672
target_term = KDefinition__expand_macros(foundry.kevm.definition, target_term)
673-
target_cterm = CTerm.from_kast(target_term)
673+
target_cterm, _ = kcfg_explore.cterm_symbolic.simplify(CTerm.from_kast(target_term))
674674
kcfg.let_node(target_node_id, cterm=target_cterm)
675675

676-
_LOGGER.info(f'Simplifying KCFG for test: {test.name}')
677-
kcfg_explore.simplify(kcfg, {})
678-
679676
return kcfg, init_node_id, target_node_id, bounded_node_ids
680677

681678

‎src/tests/integration/test-data/show/AssertTest.checkFail_assert_false().expected

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -525,11 +525,11 @@ module SUMMARY-TEST%ASSERTTEST.CHECKFAIL-ASSERT-FALSE():0
525525
andBool ( NUMBER_CELL:Int <Int pow32
526526
andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
527527
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
528+
andBool ( CALLER_ID:Int <Int pow160
529+
andBool ( ORIGIN_ID:Int <Int pow160
528530
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
529531
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
530532
andBool ( _C_ASSERTTEST_ID =/=Int 645326474426547203313410069153905908525362434349
531-
andBool ( CALLER_ID:Int <Int pow160
532-
andBool ( ORIGIN_ID:Int <Int pow160
533533
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
534534
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
535535
)))))))))))))

‎src/tests/integration/test-data/show/AssertTest.testFail_assert_true().expected

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -765,11 +765,11 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-ASSERT-TRUE():0
765765
andBool ( NUMBER_CELL:Int <Int pow32
766766
andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
767767
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
768+
andBool ( CALLER_ID:Int <Int pow160
769+
andBool ( ORIGIN_ID:Int <Int pow160
768770
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
769771
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
770772
andBool ( _C_ASSERTTEST_ID =/=Int 645326474426547203313410069153905908525362434349
771-
andBool ( CALLER_ID:Int <Int pow160
772-
andBool ( ORIGIN_ID:Int <Int pow160
773773
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
774774
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
775775
)))))))))))))

‎src/tests/integration/test-data/show/AssertTest.testFail_expect_revert().expected

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -856,11 +856,11 @@ module SUMMARY-TEST%ASSERTTEST.TESTFAIL-EXPECT-REVERT():0
856856
andBool ( NUMBER_CELL:Int <Int pow32
857857
andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
858858
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
859+
andBool ( CALLER_ID:Int <Int pow160
860+
andBool ( ORIGIN_ID:Int <Int pow160
859861
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
860862
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
861863
andBool ( _C_ASSERTTEST_ID =/=Int 645326474426547203313410069153905908525362434349
862-
andBool ( CALLER_ID:Int <Int pow160
863-
andBool ( ORIGIN_ID:Int <Int pow160
864864
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
865865
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
866866
)))))))))))))

‎src/tests/integration/test-data/show/AssertTest.test_assert_false().expected

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -762,11 +762,11 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-FALSE():0
762762
andBool ( NUMBER_CELL:Int <Int pow32
763763
andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
764764
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
765+
andBool ( CALLER_ID:Int <Int pow160
766+
andBool ( ORIGIN_ID:Int <Int pow160
765767
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
766768
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
767769
andBool ( _C_ASSERTTEST_ID =/=Int 645326474426547203313410069153905908525362434349
768-
andBool ( CALLER_ID:Int <Int pow160
769-
andBool ( ORIGIN_ID:Int <Int pow160
770770
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
771771
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
772772
)))))))))))))

‎src/tests/integration/test-data/show/AssertTest.test_assert_true().expected

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -528,11 +528,11 @@ module SUMMARY-TEST%ASSERTTEST.TEST-ASSERT-TRUE():0
528528
andBool ( NUMBER_CELL:Int <Int pow32
529529
andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
530530
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
531+
andBool ( CALLER_ID:Int <Int pow160
532+
andBool ( ORIGIN_ID:Int <Int pow160
531533
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
532534
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
533535
andBool ( _C_ASSERTTEST_ID =/=Int 645326474426547203313410069153905908525362434349
534-
andBool ( CALLER_ID:Int <Int pow160
535-
andBool ( ORIGIN_ID:Int <Int pow160
536536
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
537537
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
538538
)))))))))))))

‎src/tests/integration/test-data/show/AssertTest.test_failing_branch(uint256).expected

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -828,11 +828,11 @@ module SUMMARY-TEST%ASSERTTEST.TEST-FAILING-BRANCH(UINT256):0
828828
andBool ( NUMBER_CELL:Int <Int pow32
829829
andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
830830
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
831+
andBool ( CALLER_ID:Int <Int pow160
832+
andBool ( ORIGIN_ID:Int <Int pow160
831833
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
832834
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
833835
andBool ( _C_ASSERTTEST_ID =/=Int 645326474426547203313410069153905908525362434349
834-
andBool ( CALLER_ID:Int <Int pow160
835-
andBool ( ORIGIN_ID:Int <Int pow160
836836
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
837837
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
838838
)))))))))))))

‎src/tests/integration/test-data/show/AssertTest.test_revert_branch(uint256,uint256).expected

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -1073,11 +1073,11 @@ module SUMMARY-TEST%ASSERTTEST.TEST-REVERT-BRANCH(UINT256,UINT256):0
10731073
andBool ( NUMBER_CELL:Int <Int pow32
10741074
andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
10751075
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
1076+
andBool ( CALLER_ID:Int <Int pow160
1077+
andBool ( ORIGIN_ID:Int <Int pow160
10761078
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
10771079
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
10781080
andBool ( _C_ASSERTTEST_ID =/=Int 645326474426547203313410069153905908525362434349
1079-
andBool ( CALLER_ID:Int <Int pow160
1080-
andBool ( ORIGIN_ID:Int <Int pow160
10811081
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
10821082
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
10831083
)))))))))))))

‎src/tests/integration/test-data/show/BMCBoundTest.testBound().expected

Lines changed: 29 additions & 29 deletions
Original file line numberDiff line numberDiff line change
@@ -21,7 +21,7 @@
2121
┃ ┃ ?WORD:Int <=Int 0
2222
┃ │
2323
┃ ├─ 4
24-
┃ │ k: JUMPI 508 1 ~> #pc [ JUMPI ] ~> #execute ~> CONTINUATION:K
24+
┃ │ k: JUMPI 508 bool2Word ( ?WORD:Int <=Int 0 ) ~> #pc [ JUMPI ] ~> #execute ~> CONTIN ...
2525
┃ │ pc: 465
2626
┃ │ callDepth: 0
2727
┃ │ statusCode: STATUSCODE:StatusCode
@@ -475,7 +475,7 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
475475
rule [BASIC-BLOCK-4-TO-6]: <foundry>
476476
<kevm>
477477
<k>
478-
( JUMPI 508 1
478+
( JUMPI 508 bool2Word ( ?WORD:Int <=Int 0 )
479479
~> #pc [ JUMPI ]
480480
~> #execute => #halt ~> .K )
481481
~> _CONTINUATION
@@ -702,12 +702,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
702702
andBool ( NUMBER_CELL:Int <Int pow32
703703
andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
704704
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
705-
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
706-
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
707-
andBool ( _C_BMCBOUNDTEST_ID =/=Int 645326474426547203313410069153905908525362434349
708705
andBool ( CALLER_ID:Int <Int pow160
709706
andBool ( ORIGIN_ID:Int <Int pow160
710707
andBool ( ?WORD:Int <Int pow256
708+
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
709+
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
710+
andBool ( _C_BMCBOUNDTEST_ID =/=Int 645326474426547203313410069153905908525362434349
711711
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
712712
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
713713
))))))))))))))))
@@ -944,12 +944,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
944944
andBool ( NUMBER_CELL:Int <Int pow32
945945
andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
946946
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
947-
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
948-
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
949-
andBool ( _C_BMCBOUNDTEST_ID =/=Int 645326474426547203313410069153905908525362434349
950947
andBool ( CALLER_ID:Int <Int pow160
951948
andBool ( ORIGIN_ID:Int <Int pow160
952949
andBool ( ?WORD:Int <Int pow256
950+
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
951+
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
952+
andBool ( _C_BMCBOUNDTEST_ID =/=Int 645326474426547203313410069153905908525362434349
953953
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
954954
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
955955
)))))))))))))))))
@@ -1187,12 +1187,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
11871187
andBool ( NUMBER_CELL:Int <Int pow32
11881188
andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
11891189
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
1190-
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
1191-
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
1192-
andBool ( _C_BMCBOUNDTEST_ID =/=Int 645326474426547203313410069153905908525362434349
11931190
andBool ( CALLER_ID:Int <Int pow160
11941191
andBool ( ORIGIN_ID:Int <Int pow160
11951192
andBool ( ?WORD:Int <Int pow256
1193+
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
1194+
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
1195+
andBool ( _C_BMCBOUNDTEST_ID =/=Int 645326474426547203313410069153905908525362434349
11961196
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
11971197
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
11981198
))))))))))))))))))
@@ -1431,12 +1431,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
14311431
andBool ( NUMBER_CELL:Int <Int pow32
14321432
andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
14331433
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
1434-
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
1435-
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
1436-
andBool ( _C_BMCBOUNDTEST_ID =/=Int 645326474426547203313410069153905908525362434349
14371434
andBool ( CALLER_ID:Int <Int pow160
14381435
andBool ( ORIGIN_ID:Int <Int pow160
14391436
andBool ( ?WORD:Int <Int pow256
1437+
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
1438+
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
1439+
andBool ( _C_BMCBOUNDTEST_ID =/=Int 645326474426547203313410069153905908525362434349
14401440
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
14411441
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
14421442
)))))))))))))))))))
@@ -1672,12 +1672,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
16721672
andBool ( NUMBER_CELL:Int <Int pow32
16731673
andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
16741674
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
1675-
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
1676-
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
1677-
andBool ( _C_BMCBOUNDTEST_ID =/=Int 645326474426547203313410069153905908525362434349
16781675
andBool ( CALLER_ID:Int <Int pow160
16791676
andBool ( ORIGIN_ID:Int <Int pow160
16801677
andBool ( ?WORD:Int <Int pow256
1678+
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
1679+
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
1680+
andBool ( _C_BMCBOUNDTEST_ID =/=Int 645326474426547203313410069153905908525362434349
16811681
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
16821682
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
16831683
)))))))))))))))))))
@@ -1911,12 +1911,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
19111911
andBool ( NUMBER_CELL:Int <Int pow32
19121912
andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
19131913
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
1914-
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
1915-
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
1916-
andBool ( _C_BMCBOUNDTEST_ID =/=Int 645326474426547203313410069153905908525362434349
19171914
andBool ( CALLER_ID:Int <Int pow160
19181915
andBool ( ORIGIN_ID:Int <Int pow160
19191916
andBool ( ?WORD:Int <Int pow256
1917+
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
1918+
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
1919+
andBool ( _C_BMCBOUNDTEST_ID =/=Int 645326474426547203313410069153905908525362434349
19201920
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
19211921
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
19221922
))))))))))))))))
@@ -2151,12 +2151,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
21512151
andBool ( NUMBER_CELL:Int <Int pow32
21522152
andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
21532153
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
2154-
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
2155-
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
2156-
andBool ( _C_BMCBOUNDTEST_ID =/=Int 645326474426547203313410069153905908525362434349
21572154
andBool ( CALLER_ID:Int <Int pow160
21582155
andBool ( ORIGIN_ID:Int <Int pow160
21592156
andBool ( ?WORD:Int <Int pow256
2157+
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
2158+
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
2159+
andBool ( _C_BMCBOUNDTEST_ID =/=Int 645326474426547203313410069153905908525362434349
21602160
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
21612161
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
21622162
)))))))))))))))))
@@ -2392,12 +2392,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
23922392
andBool ( NUMBER_CELL:Int <Int pow32
23932393
andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
23942394
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
2395-
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
2396-
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
2397-
andBool ( _C_BMCBOUNDTEST_ID =/=Int 645326474426547203313410069153905908525362434349
23982395
andBool ( CALLER_ID:Int <Int pow160
23992396
andBool ( ORIGIN_ID:Int <Int pow160
24002397
andBool ( ?WORD:Int <Int pow256
2398+
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
2399+
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
2400+
andBool ( _C_BMCBOUNDTEST_ID =/=Int 645326474426547203313410069153905908525362434349
24012401
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
24022402
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
24032403
))))))))))))))))))
@@ -2634,12 +2634,12 @@ module SUMMARY-TEST%BMCBOUNDTEST.TESTBOUND():0
26342634
andBool ( NUMBER_CELL:Int <Int pow32
26352635
andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
26362636
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
2637-
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
2638-
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
2639-
andBool ( _C_BMCBOUNDTEST_ID =/=Int 645326474426547203313410069153905908525362434349
26402637
andBool ( CALLER_ID:Int <Int pow160
26412638
andBool ( ORIGIN_ID:Int <Int pow160
26422639
andBool ( ?WORD:Int <Int pow256
2640+
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
2641+
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
2642+
andBool ( _C_BMCBOUNDTEST_ID =/=Int 645326474426547203313410069153905908525362434349
26432643
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
26442644
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
26452645
)))))))))))))))))))

‎src/tests/integration/test-data/show/SetUpDeployTest.test_extcodesize().expected

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -590,11 +590,11 @@ module SUMMARY-TEST%SETUPDEPLOYTEST.TEST-EXTCODESIZE():0
590590
andBool ( NUMBER_CELL:Int <Int pow32
591591
andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
592592
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
593+
andBool ( CALLER_ID:Int <Int pow160
594+
andBool ( ORIGIN_ID:Int <Int pow160
593595
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
594596
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
595597
andBool ( _C_SETUPDEPLOYTEST_ID =/=Int 645326474426547203313410069153905908525362434349
596-
andBool ( CALLER_ID:Int <Int pow160
597-
andBool ( ORIGIN_ID:Int <Int pow160
598598
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
599599
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
600600
)))))))))))))

‎src/tests/integration/test-data/show/split-node.expected

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -766,11 +766,11 @@ module SUMMARY-TEST%PRANKTEST.TESTSYMBOLICSTARTPRANK(ADDRESS):0
766766
andBool ( NUMBER_CELL:Int <Int pow32
767767
andBool ( 1073741824 <Int TIMESTAMP_CELL:Int
768768
andBool ( TIMESTAMP_CELL:Int <Int 34359738368
769+
andBool ( CALLER_ID:Int <Int pow160
770+
andBool ( ORIGIN_ID:Int <Int pow160
769771
andBool ( CALLER_ID:Int =/=Int 645326474426547203313410069153905908525362434349
770772
andBool ( ORIGIN_ID:Int =/=Int 645326474426547203313410069153905908525362434349
771773
andBool ( _C_PRANKTEST_ID =/=Int 645326474426547203313410069153905908525362434349
772-
andBool ( CALLER_ID:Int <Int pow160
773-
andBool ( ORIGIN_ID:Int <Int pow160
774774
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
775775
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
776776
)))))))))))))

0 commit comments

Comments
 (0)