From 66bd799f0526de5d27d2faee0ebecd7e8714f02c Mon Sep 17 00:00:00 2001 From: Andrew Noyes Date: Sun, 30 Jun 2024 21:20:05 -0700 Subject: [PATCH] Fix hasty change about `end` invariants `end` is allowed to be <= 0 at the beginning of checkMaxBetweenExclusive, but not later after checking for the first range version. --- ConflictSet.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/ConflictSet.cpp b/ConflictSet.cpp index 2cb122a..1c964f2 100644 --- a/ConflictSet.cpp +++ b/ConflictSet.cpp @@ -1967,7 +1967,7 @@ bool checkMaxBetweenExclusive(Node *n, int begin, int end, InternalVersionT readVersion) { assume(-1 <= begin); assume(begin <= 256); - assume(0 < end); + assume(-1 <= end); assume(end <= 256); assume(begin < end);