add 2 new reverts for repayments in certora

term-finance · Jun 25, 2024 · 5cce3b4 · 5cce3b4
1 parent d9ba8a5
commit 5cce3b4
Showing 1 changed file with 3 additions and 1 deletion.
diff --git a/certora/specs/termRepoServicer/repayments.spec b/certora/specs/termRepoServicer/repayments.spec
@@ -170,6 +170,8 @@ rule repaymentsRevertingConditions(env e){
     }
 
     bool payable = e.msg.value > 0;
+    bool zeroRepayment = repayment == 0;
+    bool maxRepaymentZero = maxRepayment == 0;
     bool lockerTransfersPaused = locker.transfersPaused();
     bool noLockerServicerAccess = !locker.hasRole(locker.SERVICER_ROLE(), currentContract);
     bool allowanceTooLow = token.allowance( borrower, termRepoLocker()) < repayment;
@@ -180,7 +182,7 @@ rule repaymentsRevertingConditions(env e){
     bool repaymentGreaterThanMax = repaymentAmount > maxRepayment;
     bool noServicerRoleOnCollateralManager = !repaymentCollateralManager.hasRole(repaymentCollateralManager.SERVICER_ROLE(), currentContract);
 
-    bool isExpectedToRevert = payable || lockerTransfersPaused || noLockerServicerAccess || borrowTokenBalanceTooLow || allowanceTooLow || afterRepurchaseWindow || borrowerZeroObligation || uintMaxRepayment || repaymentGreaterThanMax || noServicerRoleOnCollateralManager;
+    bool isExpectedToRevert = payable || zeroRepayment || maxRepaymentZero || lockerTransfersPaused || noLockerServicerAccess || borrowTokenBalanceTooLow || allowanceTooLow || afterRepurchaseWindow || borrowerZeroObligation || uintMaxRepayment || repaymentGreaterThanMax || noServicerRoleOnCollateralManager;
 
     submitRepurchasePayment@withrevert(e, repayment);