diff --git a/tla/consensus/SIMccfraft.cfg b/tla/consensus/SIMccfraft.cfg
index 03dade83e5e..c31aaf80f40 100644
--- a/tla/consensus/SIMccfraft.cfg
+++ b/tla/consensus/SIMccfraft.cfg
@@ -72,8 +72,9 @@ INVARIANTS
     CandidateTermNotInLogInv
     ElectionSafetyInv
     LogMatchingInv
-    QuorumLogInv
-    LeaderCompletenessInv
+    \* Disabled until retirement is modeled correctly in the spec
+    \* QuorumLogInv
+    \* LeaderCompletenessInv
     SignatureInv
 
     ReconfigurationVarsTypeInv
diff --git a/tla/consensus/ccfraft.tla b/tla/consensus/ccfraft.tla
index 8649fa2bdf9..6e032968264 100644
--- a/tla/consensus/ccfraft.tla
+++ b/tla/consensus/ccfraft.tla
@@ -455,7 +455,7 @@ PlausibleSucessorNodes(i) ==
     LET
         activeServers == Servers \ removedFromConfiguration
         highestMatchServers == {n \in activeServers : \A m \in activeServers : matchIndex[i][n] >= matchIndex[i][m]}
-    IN {n \in highestMatchServers : \A m \in highestMatchServers: HighestConfigurationWithNode(i, n) >= HighestConfigurationWithNode(i, m)}
+    IN {n \in highestMatchServers : \A m \in highestMatchServers: HighestConfigurationWithNode(i, n) >= HighestConfigurationWithNode(i, m)} \ {i}
 
 StartLog(startNode, _ignored) ==
     << [term |-> StartTerm, contentType |-> TypeReconfiguration, configuration |-> startNode],