From 0944ef7438111dc653bd517f2d3692f63e550254 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Tam=C3=A1s=20T=C3=B3th?=
 <tothtamas28@users.noreply.github.com>
Date: Tue, 10 Oct 2023 17:32:22 +0200
Subject: [PATCH] Update expected output

---
 .../test-data/gas-abstraction.expected        |  295 +-
 .../show/LoopsTest.sum_N(uint256).expected    | 5304 +----------------
 2 files changed, 108 insertions(+), 5491 deletions(-)

diff --git a/src/tests/integration/test-data/gas-abstraction.expected b/src/tests/integration/test-data/gas-abstraction.expected
index 176fa68ae..51bb6ea4b 100644
--- a/src/tests/integration/test-data/gas-abstraction.expected
+++ b/src/tests/integration/test-data/gas-abstraction.expected
@@ -5,67 +5,8 @@
 │   callDepth: 0
 │   statusCode: STATUSCODE
 │
-│  (582 steps)
+│  (683 steps)
 ├─ 3
-│   k: #pc [ JUMPI ] ~> #execute ~> CONTINUATION:K
-│   pc: 770
-│   callDepth: 0
-│   statusCode: STATUSCODE:StatusCode
-│
-┊  constraint: true
-┊  subst: {
-    CONTINUATION <- CONTINUATION:K
-    EXITCODE_CELL <- EXITCODE_CELL:Int
-    OUTPUT_CELL <- OUTPUT_CELL:Bytes
-    STATUSCODE <- STATUSCODE:StatusCode
-    TOUCHEDACCOUNTS_CELL <- TOUCHEDACCOUNTS_CELL:Set
-    CALLER_ID <- CALLER_ID:Int
-    VGAS <- VGAS:Int
-    VGAS_d714ddf0 <- ( VGAS:Int +Int -328 )
-    CALLGAS_CELL <- CALLGAS_CELL:Gas
-    SELFDESTRUCT_CELL <- SELFDESTRUCT_CELL:Set
-    REFUND_CELL <- REFUND_CELL:Int
-    GASPRICE_CELL <- GASPRICE_CELL:Int
-    ORIGIN_ID <- ORIGIN_ID:Int
-    BLOCKHASHES_CELL <- BLOCKHASHES_CELL:List
-    PREVIOUSHASH_CELL <- PREVIOUSHASH_CELL:Int
-    OMMERSHASH_CELL <- OMMERSHASH_CELL:Int
-    COINBASE_CELL <- COINBASE_CELL:Int
-    STATEROOT_CELL <- STATEROOT_CELL:Int
-    TRANSACTIONSROOT_CELL <- TRANSACTIONSROOT_CELL:Int
-    RECEIPTSROOT_CELL <- RECEIPTSROOT_CELL:Int
-    LOGSBLOOM_CELL <- LOGSBLOOM_CELL:Bytes
-    DIFFICULTY_CELL <- DIFFICULTY_CELL:Int
-    NUMBER_CELL <- NUMBER_CELL:Int
-    GASLIMIT_CELL <- GASLIMIT_CELL:Int
-    GASUSED_CELL <- GASUSED_CELL:Gas
-    TIMESTAMP_CELL <- TIMESTAMP_CELL:Int
-    EXTRADATA_CELL <- EXTRADATA_CELL:Bytes
-    MIXHASH_CELL <- MIXHASH_CELL:Int
-    BLOCKNONCE_CELL <- BLOCKNONCE_CELL:Int
-    BASEFEE_CELL <- BASEFEE_CELL:Int
-    WITHDRAWALSROOT_CELL <- WITHDRAWALSROOT_CELL:Int
-    OMMERBLOCKHEADERS_CELL <- OMMERBLOCKHEADERS_CELL:JSON
-    CHAINID_CELL <- CHAINID_CELL:Int
-    TXORDER_CELL <- TXORDER_CELL:List
-    TXPENDING_CELL <- TXPENDING_CELL:List
-    MESSAGES_CELL <- MESSAGES_CELL:MessageCellMap
-    DEPTH_CELL <- DEPTH_CELL:Int
-    EXPECTEDREASON_CELL <- EXPECTEDREASON_CELL:Bytes
-    EXPECTEDDEPTH_CELL <- EXPECTEDDEPTH_CELL:Int
-    CHECKEDTOPICS_CELL <- CHECKEDTOPICS_CELL:List
-    CHECKEDDATA_CELL <- CHECKEDDATA_CELL:Bool
-    EXPECTEDEVENTADDRESS_CELL <- EXPECTEDEVENTADDRESS_CELL:Account
-    GENERATEDCOUNTER_CELL <- GENERATEDCOUNTER_CELL:Int
-}
-├─ 4
-│   k: #pc [ JUMPI ] ~> #execute ~> CONTINUATION:K
-│   pc: 770
-│   callDepth: 0
-│   statusCode: STATUSCODE:StatusCode
-│
-│  (101 steps)
-├─ 5
 │   k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K
 │   pc: 2698
 │   callDepth: 0
@@ -79,7 +20,7 @@
     TOUCHEDACCOUNTS_CELL <- TOUCHEDACCOUNTS_CELL:Set
     CALLER_ID <- CALLER_ID:Int
     VGAS <- VGAS:Int
-    VGAS_74a5a1fe <- ( VGAS_d714ddf0:Int +Int -45 )
+    VGAS_4b7cee1f <- ( VGAS:Int +Int -373 )
     CALLGAS_CELL <- CALLGAS_CELL:Gas
     SELFDESTRUCT_CELL <- SELFDESTRUCT_CELL:Set
     REFUND_CELL <- REFUND_CELL:Int
@@ -116,21 +57,21 @@
     EXPECTEDEVENTADDRESS_CELL <- EXPECTEDEVENTADDRESS_CELL:Account
     GENERATEDCOUNTER_CELL <- GENERATEDCOUNTER_CELL:Int
 }
-├─ 6
+├─ 4
 │   k: #end EVMC_REVERT ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K
 │   pc: 2698
 │   callDepth: 0
 │   statusCode: STATUSCODE:StatusCode
 │
 │  (1 step)
-├─ 7
+├─ 5
 │   k: #halt ~> #pc [ REVERT ] ~> #execute ~> CONTINUATION:K
 │   pc: 2698
 │   callDepth: 0
 │   statusCode: EVMC_REVERT
 │
 │  (2 steps)
-└─ 8 (leaf, terminal)
+└─ 6 (leaf, terminal)
     k: #halt ~> CONTINUATION:K
     pc: 2698
     callDepth: 0
@@ -144,7 +85,7 @@
 │   statusCode: STATUSCODE_FINAL
 
 
-Node 8:
+Node 6:
 
 ( <generatedTop>
   <foundry>
@@ -457,7 +398,8 @@ Node 8:
            <kevm>
              <k>
                ( #execute
-               ~> CONTINUATION => #pc [ JUMPI ]
+               ~> CONTINUATION => #end EVMC_REVERT
+               ~> #pc [ REVERT ]
                ~> #execute
                ~> CONTINUATION:K )
              </k>
@@ -469,6 +411,9 @@ Node 8:
              </schedule>
              <ethereum>
                <evm>
+                 <output>
+                   ( _OUTPUT_CELL => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" )
+                 </output>
                  <callStack>
                    .List
                  </callStack>
@@ -491,10 +436,10 @@ Node 8:
                      0
                    </callValue>
                    <wordStack>
-                     ( .WordStack => ( ( VGAS:Int +Int -298 ) : ( 583 : ( 928 : ( 345 : ( ( VGAS:Int +Int -207 ) : ( 266 : ( selector ( "testInfiniteGas()" ) : .WordStack ) ) ) ) ) ) ) )
+                     ( .WordStack => ( 778 : ( ( VGAS:Int +Int -298 ) : ( 583 : ( 928 : ( 345 : ( ( VGAS:Int +Int -207 ) : ( 266 : ( selector ( "testInfiniteGas()" ) : .WordStack ) ) ) ) ) ) ) ) )
                    </wordStack>
                    <localMem>
-                     ( .Bytes => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" )
+                     ( .Bytes => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" )
                    </localMem>
                    ...
                    ...
@@ -667,212 +612,6 @@ Node 8:
       [label(BASIC-BLOCK-1-TO-3)]
     
     rule [BASIC-BLOCK-4-TO-5]: <foundry>
-           <kevm>
-             <k>
-               ( #pc [ JUMPI ] => #end EVMC_REVERT
-               ~> #pc [ REVERT ] )
-               ~> #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   ( _OUTPUT_CELL => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01" )
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"c\xfe\xc36"
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( ( VGAS:Int +Int -298 ) => 778 ) : ( ( 583 => ( VGAS:Int +Int -298 ) ) : ( ( 928 => 583 ) : ( ( 345 => 928 ) : ( ( ( VGAS:Int +Int -207 ) => 345 ) : ( ( 266 => ( VGAS:Int +Int -207 ) ) : ( ( selector ( "testInfiniteGas()" ) => 266 ) : ( .WordStack => ( selector ( "testInfiniteGas()" ) : .WordStack ) ) ) ) ) ) ) ) )
-                   </wordStack>
-                   <localMem>
-                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" => b"NH{q\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x01\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80" )
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     3
-                   </memoryUsed>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                   ...
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     .Set
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VGAS:Int <Int ( VGAS:Int +Int 91 )
-               )))))))
-      [label(BASIC-BLOCK-4-TO-5)]
-    
-    rule [BASIC-BLOCK-6-TO-7]: <foundry>
            <kevm>
              <k>
                ( #end EVMC_REVERT => #halt )
@@ -1079,9 +818,9 @@ Node 8:
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VGAS:Int <Int ( VGAS:Int +Int 91 )
                )))))))
-      [label(BASIC-BLOCK-6-TO-7)]
+      [label(BASIC-BLOCK-4-TO-5)]
     
-    rule [BASIC-BLOCK-7-TO-8]: <foundry>
+    rule [BASIC-BLOCK-5-TO-6]: <foundry>
            <kevm>
              <k>
                #halt
@@ -1288,14 +1027,14 @@ Node 8:
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VGAS:Int <Int ( VGAS:Int +Int 91 )
                )))))))
-      [label(BASIC-BLOCK-7-TO-8)]
+      [label(BASIC-BLOCK-5-TO-6)]
 
 endmodule
 1 Failure nodes. (0 pending and 1 failing)
 
 Failing nodes:
 
-  Node id: 8
+  Node id: 6
   Failure reason:
     Implication check failed, the following is the remaining implication:
     ( ( { true #Equals 0 <=Int CALLER_ID:Int }
diff --git a/src/tests/integration/test-data/show/LoopsTest.sum_N(uint256).expected b/src/tests/integration/test-data/show/LoopsTest.sum_N(uint256).expected
index b11736423..644184ede 100644
--- a/src/tests/integration/test-data/show/LoopsTest.sum_N(uint256).expected
+++ b/src/tests/integration/test-data/show/LoopsTest.sum_N(uint256).expected
@@ -86,176 +86,22 @@
    │   callDepth: 0
    │   statusCode: STATUSCODE:StatusCode
    │
-   │  (1 step)
+   │  (162 steps)
    ├─ 11
-   │   k: JUMP 2423 ~> #pc [ JUMPI ] ~> #execute ~> CONTINUATION:K
-   │   pc: 2393
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (12 steps)
-   ├─ 13
-   │   k: #access [ JUMPDEST , JUMPDEST ] ~> JUMPDEST ~> #pc [ JUMPDEST ] ~> #execute ~> C ...
-   │   pc: 2423
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (5 steps)
-   ├─ 15
-   │   k: #execute ~> CONTINUATION:K
-   │   pc: 2425
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (2 steps)
-   ├─ 16
-   │   k: #execute ~> CONTINUATION:K
-   │   pc: 2426
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (9 steps)
-   ├─ 17
-   │   k: #access [ POP , POP 0 ] ~> POP 0 ~> #pc [ POP ] ~> #execute ~> CONTINUATION:K
-   │   pc: 2426
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (12 steps)
-   ├─ 18
-   │   k: #access [ POP , POP 0 ] ~> POP 0 ~> #pc [ POP ] ~> #execute ~> CONTINUATION:K
-   │   pc: 2427
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (12 steps)
-   ├─ 19
-   │   k: #access [ JUMP , JUMP 459 ] ~> JUMP 459 ~> #pc [ JUMP ] ~> #execute ~> CONTINUAT ...
-   │   pc: 2428
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (13 steps)
-   ├─ 20
-   │   k: #access [ JUMPDEST , JUMPDEST ] ~> JUMPDEST ~> #pc [ JUMPDEST ] ~> #execute ~> C ...
-   │   pc: 459
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (5 steps)
-   ├─ 21
-   │   k: #execute ~> CONTINUATION:K
-   │   pc: 462
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (12 steps)
-   ├─ 22
-   │   k: #access [ MLOAD , MLOAD 64 ] ~> MLOAD 64 ~> #pc [ MLOAD ] ~> #execute ~> CONTINU ...
-   │   pc: 462
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (6 steps)
-   ├─ 23
-   │   k: #execute ~> CONTINUATION:K
-   │   pc: 464
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (2 steps)
-   ├─ 24
-   │   k: #execute ~> CONTINUATION:K
-   │   pc: 465
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (12 steps)
-   ├─ 25
-   │   k: #access [ MSTORE , MSTORE 128 ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int + ...
-   │   pc: 465
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (5 steps)
-   ├─ 26
-   │   k: #execute ~> CONTINUATION:K
-   │   pc: 468
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (2 steps)
-   ├─ 27
-   │   k: #execute ~> CONTINUATION:K
-   │   pc: 469
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (9 steps)
-   ├─ 28
-   │   k: #access [ JUMPDEST , JUMPDEST ] ~> JUMPDEST ~> #pc [ JUMPDEST ] ~> #execute ~> C ...
-   │   pc: 469
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (5 steps)
-   ├─ 29
-   │   k: #execute ~> CONTINUATION:K
-   │   pc: 472
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (12 steps)
-   ├─ 30
-   │   k: #access [ MLOAD , MLOAD 64 ] ~> MLOAD 64 ~> #pc [ MLOAD ] ~> #execute ~> CONTINU ...
-   │   pc: 472
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (6 steps)
-   ├─ 31
-   │   k: #execute ~> CONTINUATION:K
-   │   pc: 474
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (2 steps)
-   ├─ 32
-   │   k: #execute ~> CONTINUATION:K
-   │   pc: 475
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (2 steps)
-   ├─ 33
-   │   k: #execute ~> CONTINUATION:K
-   │   pc: 476
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (2 steps)
-   ├─ 34
-   │   k: #execute ~> CONTINUATION:K
-   │   pc: 477
-   │   callDepth: 0
-   │   statusCode: STATUSCODE:StatusCode
-   │
-   │  (14 steps)
-   ├─ 35
    │   k: #end EVMC_SUCCESS ~> #pc [ RETURN ] ~> #execute ~> CONTINUATION:K
    │   pc: 477
    │   callDepth: 0
    │   statusCode: STATUSCODE:StatusCode
    │
    │  (1 step)
-   ├─ 36
+   ├─ 13
    │   k: #halt ~> #pc [ RETURN ] ~> #execute ~> CONTINUATION:K
    │   pc: 477
    │   callDepth: 0
    │   statusCode: EVMC_SUCCESS
    │
    │  (2 steps)
-   ├─ 37 (terminal)
+   ├─ 15 (terminal)
    │   k: #halt ~> CONTINUATION:K
    │   pc: 477
    │   callDepth: 0
@@ -1553,8 +1399,9 @@
     rule [BASIC-BLOCK-9-TO-11]: <foundry>
            <kevm>
              <k>
-               ( JUMPI 2423 bool2Word ( VV0_n_114b9705:Int ==Int 0 ) => JUMP 2423 )
-               ~> #pc [ JUMPI ]
+               ( JUMPI 2423 bool2Word ( VV0_n_114b9705:Int ==Int 0 )
+               ~> #pc [ JUMPI ] => #end EVMC_SUCCESS
+               ~> #pc [ RETURN ] )
                ~> #execute
                ~> _CONTINUATION
              </k>
@@ -1567,7 +1414,7 @@
              <ethereum>
                <evm>
                  <output>
-                   b""
+                   ( b"" => #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) )
                  </output>
                  <callStack>
                    .List
@@ -1591,10 +1438,10 @@
                      0
                    </callValue>
                    <wordStack>
-                     ( ( 0 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( 0 : ( ( VV0_n_114b9705:Int => 0 ) : ( 459 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) )
+                     ( ( 0 => selector ( "sum_N(uint256)" ) ) : ( ( 0 : ( VV0_n_114b9705:Int : ( 459 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) => .WordStack ) )
                    </wordStack>
                    <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5"
+                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5" )
                    </localMem>
                    ...
                    ...
@@ -1761,10 +1608,31 @@
                ))))))))))
        ensures ( VV0_n_114b9705:Int =/=K 0
        andBool ( 0 <Int VV0_n_114b9705:Int
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772579
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772582
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772585
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772588
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772591
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772594
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772597
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772598
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772601
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
        andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
        andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
        andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               )))))
+               ))))))))))))))))))))))))))
       [label(BASIC-BLOCK-9-TO-11)]
     
     rule [BASIC-BLOCK-10-TO-12]: <foundry>
@@ -1981,10 +1849,8 @@
     rule [BASIC-BLOCK-11-TO-13]: <foundry>
            <kevm>
              <k>
-               ( JUMP 2423
-               ~> #pc [ JUMPI ] => #access [ JUMPDEST , JUMPDEST ]
-               ~> JUMPDEST
-               ~> #pc [ JUMPDEST ] )
+               ( #end EVMC_SUCCESS => #halt )
+               ~> #pc [ RETURN ]
                ~> #execute
                ~> _CONTINUATION
              </k>
@@ -1997,8 +1863,11 @@
              <ethereum>
                <evm>
                  <output>
-                   b""
+                   #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) )
                  </output>
+                 <statusCode>
+                   ( _STATUSCODE => EVMC_SUCCESS )
+                 </statusCode>
                  <callStack>
                    .List
                  </callStack>
@@ -2021,10 +1890,10 @@
                      0
                    </callValue>
                    <wordStack>
-                     ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) : ( 0 : ( 0 : ( 459 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) )
+                     ( selector ( "sum_N(uint256)" ) : .WordStack )
                    </wordStack>
                    <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5"
+                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5"
                    </localMem>
                    ...
                    ...
@@ -2188,12 +2057,32 @@
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_n_114b9705:Int <Int pow256
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772579
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772582
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772585
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772588
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772591
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772594
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772597
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772598
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772601
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
        andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
        andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
        andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
        andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               ))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
+               )))))))))))))))))))))))))))))))))))
       [label(BASIC-BLOCK-11-TO-13)]
     
     rule [BASIC-BLOCK-12-TO-14]: <foundry>
@@ -2410,10 +2299,9 @@
     rule [BASIC-BLOCK-13-TO-15]: <foundry>
            <kevm>
              <k>
-               ( #access [ JUMPDEST , JUMPDEST ]
-               ~> JUMPDEST
-               ~> #pc [ JUMPDEST ] => .K )
-               ~> #execute
+               #halt
+               ~> ( #pc [ RETURN ]
+               ~> #execute => .K )
                ~> _CONTINUATION
              </k>
              <mode>
@@ -2425,8 +2313,11 @@
              <ethereum>
                <evm>
                  <output>
-                   b""
+                   #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) )
                  </output>
+                 <statusCode>
+                   EVMC_SUCCESS
+                 </statusCode>
                  <callStack>
                    .List
                  </callStack>
@@ -2449,10 +2340,10 @@
                      0
                    </callValue>
                    <wordStack>
-                     ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => 459 ) : ( 0 : ( 0 : ( ( 459 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) )
+                     ( selector ( "sum_N(uint256)" ) : .WordStack )
                    </wordStack>
                    <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5"
+                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5"
                    </localMem>
                    ...
                    ...
@@ -2616,5046 +2507,33 @@
        andBool ( ORIGIN_ID:Int <Int pow160
        andBool ( NUMBER_CELL:Int <=Int maxSInt256
        andBool ( VV0_n_114b9705:Int <Int pow256
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772579
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772582
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772585
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772588
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772591
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772594
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772597
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772598
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772601
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
+       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
        andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
        andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
        andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
        andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
        andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               )))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
+               )))))))))))))))))))))))))))))))))))
       [label(BASIC-BLOCK-13-TO-15)]
-    
-    rule [BASIC-BLOCK-15-TO-16]: <foundry>
-           <kevm>
-             <k>
-               #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( 459 => 0 ) : ( 0 : ( ( 0 => 459 ) : ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               ))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-      [label(BASIC-BLOCK-15-TO-16)]
-    
-    rule [BASIC-BLOCK-16-TO-17]: <foundry>
-           <kevm>
-             <k>
-               ( .K => #access [ POP , POP 0 ]
-               ~> POP 0
-               ~> #pc [ POP ] )
-               ~> #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( 0 : ( ( 0 => 459 ) : ( ( 459 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(uint256)" ) : .WordStack ) => .WordStack ) ) ) ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               )))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-      [label(BASIC-BLOCK-16-TO-17)]
-    
-    rule [BASIC-BLOCK-17-TO-18]: <foundry>
-           <kevm>
-             <k>
-               #access [ POP , POP 0 ]
-               ~> POP 0
-               ~> #pc [ POP ]
-               ~> #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( 0 => 459 ) : ( ( 459 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(uint256)" ) : .WordStack ) => .WordStack ) ) ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               ))))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-      [label(BASIC-BLOCK-17-TO-18)]
-    
-    rule [BASIC-BLOCK-18-TO-19]: <foundry>
-           <kevm>
-             <k>
-               ( #access [ POP , POP 0 ]
-               ~> POP 0
-               ~> #pc [ POP ] => #access [ JUMP , JUMP 459 ]
-               ~> JUMP 459
-               ~> #pc [ JUMP ] )
-               ~> #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( 459 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(uint256)" ) : .WordStack ) => .WordStack ) ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               )))))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-      [label(BASIC-BLOCK-18-TO-19)]
-    
-    rule [BASIC-BLOCK-19-TO-20]: <foundry>
-           <kevm>
-             <k>
-               ( #access [ JUMP , JUMP 459 ]
-               ~> JUMP 459
-               ~> #pc [ JUMP ] => #access [ JUMPDEST , JUMPDEST ]
-               ~> JUMPDEST
-               ~> #pc [ JUMPDEST ] )
-               ~> #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) : ( selector ( "sum_N(uint256)" ) : .WordStack ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               ))))))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-      [label(BASIC-BLOCK-19-TO-20)]
-    
-    rule [BASIC-BLOCK-20-TO-21]: <foundry>
-           <kevm>
-             <k>
-               ( #access [ JUMPDEST , JUMPDEST ]
-               ~> JUMPDEST
-               ~> #pc [ JUMPDEST ] => .K )
-               ~> #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => 64 ) : ( ( selector ( "sum_N(uint256)" ) => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( .WordStack => ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               )))))))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-      [label(BASIC-BLOCK-20-TO-21)]
-    
-    rule [BASIC-BLOCK-21-TO-22]: <foundry>
-           <kevm>
-             <k>
-               ( .K => #access [ MLOAD , MLOAD 64 ]
-               ~> MLOAD 64
-               ~> #pc [ MLOAD ] )
-               ~> #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( 64 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(uint256)" ) : .WordStack ) => .WordStack ) ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               ))))))))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-      [label(BASIC-BLOCK-21-TO-22)]
-    
-    rule [BASIC-BLOCK-22-TO-23]: <foundry>
-           <kevm>
-             <k>
-               ( #access [ MLOAD , MLOAD 64 ]
-               ~> MLOAD 64
-               ~> #pc [ MLOAD ] => .K )
-               ~> #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) : ( ( selector ( "sum_N(uint256)" ) => 128 ) : ( .WordStack => ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               )))))))))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
-      [label(BASIC-BLOCK-22-TO-23)]
-    
-    rule [BASIC-BLOCK-23-TO-24]: <foundry>
-           <kevm>
-             <k>
-               #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => 128 ) : ( ( 128 => ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) : ( ( selector ( "sum_N(uint256)" ) => 128 ) : ( .WordStack => ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               ))))))))))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
-      [label(BASIC-BLOCK-23-TO-24)]
-    
-    rule [BASIC-BLOCK-24-TO-25]: <foundry>
-           <kevm>
-             <k>
-               ( .K => #access [ MSTORE , MSTORE 128 ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ]
-               ~> MSTORE 128 ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-               ~> #pc [ MSTORE ] )
-               ~> #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( 128 : ( ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) => selector ( "sum_N(uint256)" ) ) : ( ( 128 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) => .WordStack ) ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               )))))))))))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
-      [label(BASIC-BLOCK-24-TO-25)]
-    
-    rule [BASIC-BLOCK-25-TO-26]: <foundry>
-           <kevm>
-             <k>
-               ( #access [ MSTORE , MSTORE 128 ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ]
-               ~> MSTORE 128 ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-               ~> #pc [ MSTORE ] => .K )
-               ~> #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( 128 => 32 ) : ( ( selector ( "sum_N(uint256)" ) => 128 ) : ( .WordStack => ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) )
-                   </wordStack>
-                   <localMem>
-                     ( b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\xddQ\xfa\xa2\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x7f\xff\xff\xff\xff\xff\xf3\xd5" => b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5" )
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               ))))))))))))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772601
-      [label(BASIC-BLOCK-25-TO-26)]
-    
-    rule [BASIC-BLOCK-26-TO-27]: <foundry>
-           <kevm>
-             <k>
-               #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( 32 => 160 ) : ( ( 128 => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(uint256)" ) : .WordStack ) => .WordStack ) ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772601
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               )))))))))))))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772598
-      [label(BASIC-BLOCK-26-TO-27)]
-    
-    rule [BASIC-BLOCK-27-TO-28]: <foundry>
-           <kevm>
-             <k>
-               ( .K => #access [ JUMPDEST , JUMPDEST ]
-               ~> JUMPDEST
-               ~> #pc [ JUMPDEST ] )
-               ~> #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( 160 : ( selector ( "sum_N(uint256)" ) : .WordStack ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772598
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772601
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               ))))))))))))))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772597
-      [label(BASIC-BLOCK-27-TO-28)]
-    
-    rule [BASIC-BLOCK-28-TO-29]: <foundry>
-           <kevm>
-             <k>
-               ( #access [ JUMPDEST , JUMPDEST ]
-               ~> JUMPDEST
-               ~> #pc [ JUMPDEST ] => .K )
-               ~> #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( 160 => 64 ) : ( ( selector ( "sum_N(uint256)" ) => 160 ) : ( .WordStack => ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772597
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772598
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772601
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               )))))))))))))))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772594
-      [label(BASIC-BLOCK-28-TO-29)]
-    
-    rule [BASIC-BLOCK-29-TO-30]: <foundry>
-           <kevm>
-             <k>
-               ( .K => #access [ MLOAD , MLOAD 64 ]
-               ~> MLOAD 64
-               ~> #pc [ MLOAD ] )
-               ~> #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( 64 => 160 ) : ( ( 160 => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(uint256)" ) : .WordStack ) => .WordStack ) ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772594
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772597
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772598
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772601
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               ))))))))))))))))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772591
-      [label(BASIC-BLOCK-29-TO-30)]
-    
-    rule [BASIC-BLOCK-30-TO-31]: <foundry>
-           <kevm>
-             <k>
-               ( #access [ MLOAD , MLOAD 64 ]
-               ~> MLOAD 64
-               ~> #pc [ MLOAD ] => .K )
-               ~> #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( 160 => 128 ) : ( ( selector ( "sum_N(uint256)" ) => 128 ) : ( .WordStack => ( 160 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772591
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772594
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772597
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772598
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772601
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               )))))))))))))))))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772588
-      [label(BASIC-BLOCK-30-TO-31)]
-    
-    rule [BASIC-BLOCK-31-TO-32]: <foundry>
-           <kevm>
-             <k>
-               #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( 128 => 160 ) : ( 128 : ( ( 160 => 128 ) : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772588
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772591
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772594
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772597
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772598
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772601
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               ))))))))))))))))))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772585
-      [label(BASIC-BLOCK-31-TO-32)]
-    
-    rule [BASIC-BLOCK-32-TO-33]: <foundry>
-           <kevm>
-             <k>
-               #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( 160 => 32 ) : ( 128 : ( ( 128 => selector ( "sum_N(uint256)" ) ) : ( ( selector ( "sum_N(uint256)" ) : .WordStack ) => .WordStack ) ) ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772585
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772588
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772591
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772594
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772597
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772598
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772601
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               )))))))))))))))))))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772582
-      [label(BASIC-BLOCK-32-TO-33)]
-    
-    rule [BASIC-BLOCK-33-TO-34]: <foundry>
-           <kevm>
-             <k>
-               #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   b""
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( 32 => 128 ) : ( ( 128 => 32 ) : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772582
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772585
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772588
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772591
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772594
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772597
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772598
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772601
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               ))))))))))))))))))))))))))))))))))
-       ensures ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772579
-      [label(BASIC-BLOCK-33-TO-34)]
-    
-    rule [BASIC-BLOCK-34-TO-35]: <foundry>
-           <kevm>
-             <k>
-               ( .K => #end EVMC_SUCCESS
-               ~> #pc [ RETURN ] )
-               ~> #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   ( b"" => #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) )
-                 </output>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( ( 128 => selector ( "sum_N(uint256)" ) ) : ( ( 32 : ( selector ( "sum_N(uint256)" ) : .WordStack ) ) => .WordStack ) )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772579
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772582
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772585
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772588
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772591
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772594
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772597
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772598
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772601
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               )))))))))))))))))))))))))))))))))))
-      [label(BASIC-BLOCK-34-TO-35)]
-    
-    rule [BASIC-BLOCK-35-TO-36]: <foundry>
-           <kevm>
-             <k>
-               ( #end EVMC_SUCCESS => #halt )
-               ~> #pc [ RETURN ]
-               ~> #execute
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) )
-                 </output>
-                 <statusCode>
-                   ( _STATUSCODE => EVMC_SUCCESS )
-                 </statusCode>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( selector ( "sum_N(uint256)" ) : .WordStack )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772579
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772582
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772585
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772588
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772591
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772594
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772597
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772598
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772601
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               )))))))))))))))))))))))))))))))))))
-      [label(BASIC-BLOCK-35-TO-36)]
-    
-    rule [BASIC-BLOCK-36-TO-37]: <foundry>
-           <kevm>
-             <k>
-               #halt
-               ~> ( #pc [ RETURN ]
-               ~> #execute => .K )
-               ~> _CONTINUATION
-             </k>
-             <mode>
-               NORMAL
-             </mode>
-             <schedule>
-               SHANGHAI
-             </schedule>
-             <ethereum>
-               <evm>
-                 <output>
-                   #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) )
-                 </output>
-                 <statusCode>
-                   EVMC_SUCCESS
-                 </statusCode>
-                 <callStack>
-                   .List
-                 </callStack>
-                 <interimStates>
-                   .List
-                 </interimStates>
-                 <callState>
-                   ...
-                   ...
-                   <id>
-                     728815563385977040452943777879061427756277306518
-                   </id>
-                   <caller>
-                     CALLER_ID:Int
-                   </caller>
-                   <callData>
-                     b"~\x8e#\xd0" +Bytes #buf ( 32 , VV0_n_114b9705:Int )
-                   </callData>
-                   <callValue>
-                     0
-                   </callValue>
-                   <wordStack>
-                     ( selector ( "sum_N(uint256)" ) : .WordStack )
-                   </wordStack>
-                   <localMem>
-                     b"\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x80\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00\x00" +Bytes #buf ( 32 , ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) ) +Bytes b"\xff\xff\xf3\xd5"
-                   </localMem>
-                   ...
-                   ...
-                   <memoryUsed>
-                     6
-                   </memoryUsed>
-                   <callGas>
-                     0
-                   </callGas>
-                   <static>
-                     false
-                   </static>
-                   <callDepth>
-                     0
-                   </callDepth>
-                 </callState>
-                 <substate>
-                   <log>
-                     .List
-                   </log>
-                   <accessedAccounts>
-                     SetItem ( 645326474426547203313410069153905908525362434349 )
-                   </accessedAccounts>
-                   <accessedStorage>
-                     .Map
-                   </accessedStorage>
-                   ...
-                 </substate>
-                 <origin>
-                   ORIGIN_ID:Int
-                 </origin>
-                 <block>
-                   <number>
-                     NUMBER_CELL:Int
-                   </number>
-                   ...
-                 </block>
-                 ...
-               </evm>
-               <network>
-                 <accounts>
-                   ( <account>
-                     <acctID>
-                       645326474426547203313410069153905908525362434349
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       0
-                     </nonce>
-                   </account>
-                   <account>
-                     <acctID>
-                       728815563385977040452943777879061427756277306518
-                     </acctID>
-                     <balance>
-                       0
-                     </balance>
-                     ...
-                     <storage>
-                       .Map
-                     </storage>
-                     <origStorage>
-                       .Map
-                     </origStorage>
-                     <nonce>
-                       1
-                     </nonce>
-                   </account> )
-                 </accounts>
-                 ...
-               </network>
-             </ethereum>
-             ...
-           </kevm>
-           <cheatcodes>
-             <prank>
-               <prevCaller>
-                 .Account
-               </prevCaller>
-               <prevOrigin>
-                 .Account
-               </prevOrigin>
-               <newCaller>
-                 .Account
-               </newCaller>
-               <newOrigin>
-                 .Account
-               </newOrigin>
-               <active>
-                 false
-               </active>
-               <singleCall>
-                 false
-               </singleCall>
-               ...
-             </prank>
-             <expectedRevert>
-               <isRevertExpected>
-                 false
-               </isRevertExpected>
-               ...
-             </expectedRevert>
-             <expectedOpcode>
-               <isOpcodeExpected>
-                 false
-               </isOpcodeExpected>
-               <expectedAddress>
-                 .Account
-               </expectedAddress>
-               <expectedValue>
-                 0
-               </expectedValue>
-               <expectedData>
-                 b""
-               </expectedData>
-               <opcodeType>
-                 .OpcodeType
-               </opcodeType>
-             </expectedOpcode>
-             <expectEmit>
-               <recordEvent>
-                 false
-               </recordEvent>
-               <isEventExpected>
-                 false
-               </isEventExpected>
-               ...
-             </expectEmit>
-             <whitelist>
-               <isCallWhitelistActive>
-                 false
-               </isCallWhitelistActive>
-               <isStorageWhitelistActive>
-                 false
-               </isStorageWhitelistActive>
-               <addressSet>
-                 .Set
-               </addressSet>
-               <storageSlotSet>
-                 .Set
-               </storageSlotSet>
-             </whitelist>
-           </cheatcodes>
-         </foundry>
-      requires ( VV0_n_114b9705:Int =/=K 0
-       andBool ( 0 <=Int CALLER_ID:Int
-       andBool ( 0 <=Int ORIGIN_ID:Int
-       andBool ( 0 <=Int NUMBER_CELL:Int
-       andBool ( 0 <Int VV0_n_114b9705:Int
-       andBool ( 0 <=Int VV0_n_114b9705:Int
-       andBool ( CALLER_ID:Int <Int pow160
-       andBool ( ORIGIN_ID:Int <Int pow160
-       andBool ( NUMBER_CELL:Int <=Int maxSInt256
-       andBool ( VV0_n_114b9705:Int <Int pow256
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772579
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772582
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772585
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772588
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772591
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772594
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772597
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772598
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772601
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772604
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772607
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772610
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772613
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772616
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772619
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772620
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772628
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772630
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772632
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772635
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772638
-       andBool ( ( VV0_n_114b9705:Int *Int 178 ) <=Int 9223372036854772639
-       andBool ( VV0_n_114b9705:Int <=Int 51816696836262767 ==Bool true
-       andBool ( 0 <=Int ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 )
-       andBool ( ( ( VV0_n_114b9705:Int *Int ( VV0_n_114b9705:Int +Int 1 ) ) /Int 2 ) <Int pow256
-               )))))))))))))))))))))))))))))))))))
-      [label(BASIC-BLOCK-36-TO-37)]
 
 endmodule
 0 Failure nodes. (0 pending and 0 failing)