[Civl] changed axiom for ChangRoberts sample (#917)

Co-authored-by: Shaz Qadeer <shaz@meta.com>
boogie-org · Jul 22, 2024 · 599970f · 599970f
1 parent d322dc6
commit 599970f
Showing 1 changed file with 1 addition and 2 deletions.
diff --git a/Test/civl/inductive-sequentialization/ChangRoberts.bpl b/Test/civl/inductive-sequentialization/ChangRoberts.bpl
@@ -20,8 +20,7 @@ function {:inline} Below(self: int, pid: int): bool
 
 const ExpectedLeader: int;
 axiom ValidPid(ExpectedLeader);
-axiom (forall i: int:: ValidPid(i) ==> Priority(i) <= Priority(ExpectedLeader));
-axiom (forall i: int:: ValidPid(i) && Priority(i) == Priority(ExpectedLeader) ==> i <= ExpectedLeader);
+axiom (forall i: int:: ValidPid(i) ==> i == ExpectedLeader || Below(i, ExpectedLeader));
 
 // alternative coordinates for identifying processes where ExpectedLeader is at position 0
 // Pos converts from process id to its position