seq range fix

sakehl · Mar 27, 2024 · 5dac883 · 5dac883
1 parent 400e108
commit 5dac883
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/res/universal/res/adt/range.pvl b/res/universal/res/adt/range.pvl
@@ -4,5 +4,5 @@ pure set<int> set_range(int l, int r);
 
 ensures (\forall int i; {:i \in \result:} == (l >= i && i < r));
 ensures l <= r ? \result.size == r - l : \result.size == 0;
-ensures (\forall int i=l..r; {:\result[i]:} == l + i);
+ensures (\forall int i=0..(r-l); {:\result[i]:} == l + i);
 pure seq<int> seq_range(int l, int r);