docs: document checkSummaries

morpho-org · Mar 22, 2024 · 4f186ca · 4f186ca
1 parent deda832
commit 4f186ca
Showing 1 changed file with 2 additions and 0 deletions.
diff --git a/certora/specs/MarketInteractions.spec b/certora/specs/MarketInteractions.spec
@@ -54,5 +54,7 @@ function summaryWithdraw(MetaMorphoHarness.MarketParams marketParams, uint256 as
     return (_, _);
 }
 
+// Check assertions in the summaries.
+// This requires to turn off sanity checks for this invariant that appears vacuous.
 invariant checkSummaries()
     true;