diff --git a/certora/specs/LibSummary.spec b/certora/specs/LibSummary.spec index 1790a22f..08b7b1e0 100644 --- a/certora/specs/LibSummary.spec +++ b/certora/specs/LibSummary.spec @@ -27,5 +27,6 @@ rule checkSummaryId(MorphoHarness.MarketParams marketParams) { } rule checkSummaryMin(uint256 x, uint256 y) { - assert libMin(x, y) == x < y ? x : y; + uint256 summaryMin = x < y ? x : y; + assert libMin(x, y) == summaryMin; }