From 2e74f7058bb54896f703d84314326ff0298d9ae7 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Adam=20Uhl=C3=AD=C5=99?= <adam@uhlir.dev>
Date: Wed, 4 Dec 2024 17:10:48 +0100
Subject: [PATCH] test(verifier): repair state can go to filled

---
 certora/specs/Marketplace.spec | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/certora/specs/Marketplace.spec b/certora/specs/Marketplace.spec
index 59e31ee0..b5ab0fc7 100644
--- a/certora/specs/Marketplace.spec
+++ b/certora/specs/Marketplace.spec
@@ -301,7 +301,10 @@ rule functionsCausingSlotStateChanges(env e, method f) {
     assert slotStateBefore == Marketplace.SlotState.Finished && slotStateAfter == Marketplace.SlotState.Paid => canMakeSlotPaid(f);
 
     // SlotState.Free -> SlotState.Filled
-    assert slotStateBefore != Marketplace.SlotState.Filled && slotStateAfter == Marketplace.SlotState.Filled => canFillSlot(f);
+    assert slotStateBefore != Marketplace.SlotState.Free && slotStateAfter == Marketplace.SlotState.Filled => canFillSlot(f);
+
+    // SlotState.Repair -> SlotState.Filled
+    assert slotStateBefore != Marketplace.SlotState.Repair && slotStateAfter == Marketplace.SlotState.Filled => canFillSlot(f);
 }
 
 rule allowedSlotStateChanges(env e, method f) {