Edited end of function summary. Number of expected restoreEnv (closin…

…g scopes) is input dependent).
Pi-Squared-Inc · Oct 3, 2024 · df1585d · df1585d
1 parent 4dac6d7
commit df1585d
Showing 1 changed file with 2 additions and 2 deletions.
diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md
@@ -2743,8 +2743,8 @@ module SOLIDITY-UNISWAP-GETAMOUNTSOUT-SUMMARY
        </store>
        <current-function> uniswapV2LibraryGetAmountsOut </current-function> [priority(40)]
 
-  // While condition evaluated to false until return from getAmountsOut to caller
-  rule <k> if ( v ( false , bool ) ) { _:Statements } else { .Statements } ~> .Statements ~> restoreEnv ( _:Map ) ~> .Statements ~> restoreEnv ( _:Map (amounts |-> var(Ia, uint256 [])) ) ~> .Statements ~> return amounts ; ~> .K => v ( Va , uint256 [] ) ~> K </k>
+  // End of function: final environment restoration until return from getAmountsOut to caller
+  rule <k> restoreEnv ( _:Map (amounts |-> var(Ia, uint256 [])) ) ~> .Statements ~> return amounts ; ~> .K => v ( Va , uint256 [] ) ~> K </k>
        <summarize> true </summarize>
        <env> _ => E </env>
        <store> _ [ Ia <- Va ] </store>