Merge branch 'josef/resetQuint' of github.com:informalsystems/malachi…

…te into josef/resetQuint
informalsystems · Apr 17, 2024 · 9fa2d74 · 9fa2d74
2 parents 767b795 + 0e867ed
commit 9fa2d74
Showing 1 changed file with 2 additions and 1 deletion.
diff --git a/specs/quint/specs/reset.qnt b/specs/quint/specs/reset.qnt
@@ -86,7 +86,8 @@ pure def L1Epoch(b: L1Block) : int =
     b.height / L1EpochSize
 
 pure def staleRegs (b: L1Block) : Set[Registration] =
-    b.pendingRegistrations.filter(r => r.eth_epoch + 1 < b.height / L1EpochSize)
+    b.pendingRegistrations.filter(r => r.eth_epoch + 2 <= b.height / L1EpochSize)
+
 
 pure def existsStale (b: L1Block) : bool =
     staleRegs(b).size() > 0