diff --git a/src/uniswap-summaries.md b/src/uniswap-summaries.md index d81ae13..326b677 100644 --- a/src/uniswap-summaries.md +++ b/src/uniswap-summaries.md @@ -2743,8 +2743,8 @@ module SOLIDITY-UNISWAP-GETAMOUNTSOUT-SUMMARY uniswapV2LibraryGetAmountsOut [priority(40)] - // While condition evaluated to false until return from getAmountsOut to caller - rule 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 + // End of function: final environment restoration until return from getAmountsOut to caller + rule restoreEnv ( _:Map (amounts |-> var(Ia, uint256 [])) ) ~> .Statements ~> return amounts ; ~> .K => v ( Va , uint256 [] ) ~> K true _ => E _ [ Ia <- Va ]