Skip to content

Commit

Permalink
Update schedule in loop invariant lemmas
Browse files Browse the repository at this point in the history
  • Loading branch information
palinatolmach committed Jan 30, 2025
1 parent 2e2617d commit 305c132
Show file tree
Hide file tree
Showing 2 changed files with 2 additions and 2 deletions.
2 changes: 1 addition & 1 deletion src/tests/integration/test-data/lemmas.k
Original file line number Diff line number Diff line change
Expand Up @@ -20,7 +20,7 @@ module SUM-TO-N-INVARIANT
NORMAL
</mode>
<schedule>
SHANGHAI
CANCUN
</schedule>
<ethereum>
<evm>
Expand Down
2 changes: 1 addition & 1 deletion src/tests/integration/test-data/pausability-lemmas.k
Original file line number Diff line number Diff line change
Expand Up @@ -124,7 +124,7 @@ module PAUSABILITY-LEMMAS [symbolic]
rule [test-copy-memory-to-memory-summary]:
<k> #execute ... </k>
<useGas> false </useGas>
<schedule> SHANGHAI </schedule>
<schedule> CANCUN </schedule>
<jumpDests> JUMPDESTS </jumpDests>
// The program and program counter are symbolic, focusing on the part we will be executing (CP)
<program> PROGRAM </program>
Expand Down

0 comments on commit 305c132

Please sign in to comment.