Skip to content

Commit

Permalink
other expected outputs
Browse files Browse the repository at this point in the history
  • Loading branch information
@PetarMax
PetarMax committed Sep 19, 2024
1 parent 4d73753 commit 82cde52
Show file tree
Hide file tree
Showing 3 changed files with 21 additions and 21 deletions.
6 changes: 3 additions & 3 deletions src/tests/integration/test-data/show/merge-loop-heads.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -30,7 +30,7 @@
┃ │ method: test%BMCLoopsTest.test_bmc(uint256)
┃ │
┃ ┊ constraint:
┃ ┊ ( ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( 0 <=In...
┃ ┊ ( ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( 0 <=Int VV0_n_114b9705:Int andBool ( VV0_n_114b9705:Int <=Int 0 andBool ( pow24 <Int NUMBER_CELL:Int andBool ( NUMBER_CELL:Int <Int pow32 andBool ( 1073741824 <Int TIMESTAMP_CELL:Int andBool ( TIMESTAMP_CELL:Int <Int 34359738368 andBool ( CALLER_ID:Int <Int pow160 andBool ( ORIGIN_ID:Int <Int pow160 andBool ( VV0_n_114b9705:Int <Int pow256 andBool ( ( notBool CALLER_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) andBool ( ( notBool ORIGIN_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) andBool ( ( notBool C_BMCLOOPSTEST_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) impliesBool ( ( 0 ==K V_45741f39:Int andBool ( ( V_45741f39 ==K 0 andBool VV0_n_114b9705:Int <=Int 0 ) orBool ( V_45741f39 ==K 1 andBool #range ( 0 < VV0_n_114b9705:Int <= 1 ) ) ) ) orBool ( 0 ==K 2 andBool ( 0 <Int VV0_n_114b9705:Int andBool ( 1 <Int VV0_n_114b9705:Int andBool ( VV0_n_114b9705:Int <=Int 2 andBool ( notBool C_BMCLOOPSTEST_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) ) ) ) ) ) )
┃ ┊ subst: ...
┃ ├─ 20
┃ │ k: JUMPI 1478 bool2Word ( VV0_n_114b9705:Int <=Int V_8ae8c0f0:Int ) ~> #pc [ JUMPI ...
Expand Down Expand Up @@ -84,7 +84,7 @@
┃ │ method: test%BMCLoopsTest.test_bmc(uint256)
┃ │
┃ ┊ constraint:
┃ ┊ ( ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( 0 <Int...
┃ ┊ ( ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( 0 <Int VV0_n_114b9705:Int andBool ( 0 <=Int VV0_n_114b9705:Int andBool ( VV0_n_114b9705:Int <=Int 1 andBool ( pow24 <Int NUMBER_CELL:Int andBool ( NUMBER_CELL:Int <Int pow32 andBool ( 1073741824 <Int TIMESTAMP_CELL:Int andBool ( TIMESTAMP_CELL:Int <Int 34359738368 andBool ( CALLER_ID:Int <Int pow160 andBool ( ORIGIN_ID:Int <Int pow160 andBool ( VV0_n_114b9705:Int <Int pow256 andBool ( ( notBool CALLER_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) andBool ( ( notBool ORIGIN_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) andBool ( ( notBool C_BMCLOOPSTEST_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) impliesBool ( ( 1 ==K V_45741f39:Int andBool ( ( V_45741f39 ==K 0 andBool VV0_n_114b9705:Int <=Int 0 ) orBool ( V_45741f39 ==K 1 andBool #range ( 0 < VV0_n_114b9705:Int <= 1 ) ) ) ) orBool ( 1 ==K 2 andBool ( 0 <Int VV0_n_114b9705:Int andBool ( 1 <Int VV0_n_114b9705:Int andBool ( VV0_n_114b9705:Int <=Int 2 andBool ( notBool C_BMCLOOPSTEST_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) ) ) ) ) ) )
┃ ┊ subst: ...
┃ └─ 20
┃ k: JUMPI 1478 bool2Word ( VV0_n_114b9705:Int <=Int V_8ae8c0f0:Int ) ~> #pc [ JUMPI ...
Expand Down Expand Up @@ -130,7 +130,7 @@
┃ │ method: test%BMCLoopsTest.test_bmc(uint256)
┃ │
┃ ┊ constraint:
┃ ┊ ( ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( 0 <Int...
┃ ┊ ( ( 0 <=Int CALLER_ID:Int andBool ( 0 <=Int ORIGIN_ID:Int andBool ( 0 <Int VV0_n_114b9705:Int andBool ( 1 <Int VV0_n_114b9705:Int andBool ( 0 <=Int VV0_n_114b9705:Int andBool ( VV0_n_114b9705:Int <=Int 2 andBool ( pow24 <Int NUMBER_CELL:Int andBool ( NUMBER_CELL:Int <Int pow32 andBool ( 1073741824 <Int TIMESTAMP_CELL:Int andBool ( TIMESTAMP_CELL:Int <Int 34359738368 andBool ( CALLER_ID:Int <Int pow160 andBool ( ORIGIN_ID:Int <Int pow160 andBool ( VV0_n_114b9705:Int <Int pow256 andBool ( ( notBool CALLER_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) andBool ( ( notBool ORIGIN_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) andBool ( ( notBool C_BMCLOOPSTEST_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) ) andBool ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) ) impliesBool ( ( 2 ==K V_45741f39:Int andBool ( ( V_45741f39 ==K 0 andBool VV0_n_114b9705:Int <=Int 0 ) orBool ( V_45741f39 ==K 1 andBool #range ( 0 < VV0_n_114b9705:Int <= 1 ) ) ) ) orBool ( 2 ==K 2 andBool ( 0 <Int VV0_n_114b9705:Int andBool ( 1 <Int VV0_n_114b9705:Int andBool ( VV0_n_114b9705:Int <=Int 2 andBool ( notBool C_BMCLOOPSTEST_ID:Int ==Int 645326474426547203313410069153905908525362434349 ) ) ) ) ) ) )
┃ ┊ subst: ...
┃ └─ 20
┃ k: JUMPI 1478 bool2Word ( VV0_n_114b9705:Int <=Int V_8ae8c0f0:Int ) ~> #pc [ JUMPI ...
Expand Down
18 changes: 9 additions & 9 deletions src/tests/integration/test-data/show/node-refutation.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -42,7 +42,7 @@
│ method: test%MergeTest.test_branch_merge(uint256)
│
│ (90 steps)
├─ 12
├─ 10
│ k: #end EVMC_SUCCESS ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
│ pc: 235
│ callDepth: 0
Expand All @@ -51,7 +51,7 @@
│ method: test%MergeTest.test_branch_merge(uint256)
│
│ (1 step)
├─ 13
├─ 11
│ k: #halt ~> #pc [ STOP ] ~> #execute ~> CONTINUATION:K
│ pc: 235
│ callDepth: 0
Expand All @@ -60,7 +60,7 @@
│ method: test%MergeTest.test_branch_merge(uint256)
│
│ (2 steps)
├─ 14 (terminal)
├─ 12 (terminal)
│ k: #halt ~> CONTINUATION:K
│ pc: 235
│ callDepth: 0
Expand Down Expand Up @@ -319,7 +319,7 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0
)))))))))))))))
[priority(20), label(BASIC-BLOCK-1-TO-3)]

rule [BASIC-BLOCK-5-TO-12]: <foundry>
rule [BASIC-BLOCK-5-TO-10]: <foundry>
<kevm>
<k>
( JUMPI 535 bool2Word ( 10 <=Int VV0_x_114b9705:Int )
Expand Down Expand Up @@ -556,9 +556,9 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))))))))))))))))
[priority(20), label(BASIC-BLOCK-5-TO-12)]
[priority(20), label(BASIC-BLOCK-5-TO-10)]

rule [BASIC-BLOCK-12-TO-13]: <foundry>
rule [BASIC-BLOCK-10-TO-11]: <foundry>
<kevm>
<k>
( #end EVMC_SUCCESS => #halt )
Expand Down Expand Up @@ -797,9 +797,9 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))))))))))))))))
[priority(20), label(BASIC-BLOCK-12-TO-13)]
[priority(20), label(BASIC-BLOCK-10-TO-11)]

rule [BASIC-BLOCK-13-TO-14]: <foundry>
rule [BASIC-BLOCK-11-TO-12]: <foundry>
<kevm>
<k>
#halt
Expand Down Expand Up @@ -1038,7 +1038,7 @@ module SUMMARY-TEST%MERGETEST.TEST-BRANCH-MERGE(UINT256):0
andBool ( ( notBool #range ( 0 < CALLER_ID:Int <= 9 ) )
andBool ( ( notBool #range ( 0 < ORIGIN_ID:Int <= 9 ) )
))))))))))))))))
[priority(20), label(BASIC-BLOCK-13-TO-14)]
[priority(20), label(BASIC-BLOCK-11-TO-12)]

endmodule
0 Failure nodes. (0 pending and 0 failing)
Expand Down
18 changes: 9 additions & 9 deletions src/tests/integration/test-data/show/split-node.expected
View file
Original file line number Diff line number Diff line change
Expand Up @@ -44,7 +44,7 @@
┃ (branch)
┣━━┓ subst: .Subst
┃ ┃ constraint:
┃ ┃ VV0_addr_114b9705:Int ==Int 4914609233421842180357068880087500439777551132...
┃ ┃ VV0_addr_114b9705:Int ==Int 491460923342184218035706888008750043977755113263
┃ │
┃ └─ 70 (leaf, refuted)
┃ k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
Expand All @@ -55,7 +55,7 @@
┃
┗━━┓ subst: .Subst
┃ constraint:
┃ ( notBool VV0_addr_114b9705:Int ==Int 491460923342184218035706888008750043...
┃ ( notBool VV0_addr_114b9705:Int ==Int 491460923342184218035706888008750043977755113263 )
│
├─ 71 (split)
│ k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
Expand All @@ -67,7 +67,7 @@
┃ (branch)
┣━━┓ subst: .Subst
┃ ┃ constraint:
┃ ┃ VV0_addr_114b9705:Int ==Int 6453264744265472033134100691539059085253624343...
┃ ┃ VV0_addr_114b9705:Int ==Int 645326474426547203313410069153905908525362434349
┃ │
┃ └─ 72 (leaf, refuted)
┃ k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
Expand All @@ -78,7 +78,7 @@
┃
┗━━┓ subst: .Subst
┃ constraint:
┃ ( notBool VV0_addr_114b9705:Int ==Int 645326474426547203313410069153905908...
┃ ( notBool VV0_addr_114b9705:Int ==Int 645326474426547203313410069153905908525362434349 )
│
├─ 73 (split)
│ k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
Expand All @@ -90,7 +90,7 @@
┃ (branch)
┣━━┓ subst: .Subst
┃ ┃ constraint:
┃ ┃ VV0_addr_114b9705:Int ==Int 7288155633859770404529437778790614277562773065...
┃ ┃ VV0_addr_114b9705:Int ==Int 728815563385977040452943777879061427756277306518
┃ │
┃ └─ 74 (leaf, refuted)
┃ k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
Expand All @@ -101,7 +101,7 @@
┃
┗━━┓ subst: .Subst
┃ constraint:
┃ ( notBool VV0_addr_114b9705:Int ==Int 728815563385977040452943777879061427...
┃ ( notBool VV0_addr_114b9705:Int ==Int 728815563385977040452943777879061427756277306518 )
│
├─ 75
│ k: #accessAccounts 645326474426547203313410069153905908525362434349 ~> #checkCall 7 ...
Expand Down Expand Up @@ -226,9 +226,9 @@
│ method: test%PrankTest.testSymbolicStartPrank(address)
│
┊ constraint:
┊ ( notBool VV0_addr_114b9705:Int ==Int 491460923342184218035706888008750043...
┊ ( notBool VV0_addr_114b9705:Int ==Int 645326474426547203313410069153905908...
┊ ( notBool VV0_addr_114b9705:Int ==Int 728815563385977040452943777879061427...
┊ ( notBool VV0_addr_114b9705:Int ==Int 491460923342184218035706888008750043977755113263 )
┊ ( notBool VV0_addr_114b9705:Int ==Int 645326474426547203313410069153905908525362434349 )
┊ ( notBool VV0_addr_114b9705:Int ==Int 728815563385977040452943777879061427756277306518 )
┊ subst: ...
└─ 10 (leaf, target, terminal)
k: #halt ~> CONTINUATION:K
Expand Down

0 comments on commit 82cde52

Please sign in to comment.