diff options
| author | Anthony Wang | 2025-05-07 15:39:34 -0400 |
|---|---|---|
| committer | Anthony Wang | 2025-05-07 15:39:34 -0400 |
| commit | 00b7d3494f1fefaa91763dfe1c57ca54610d5d99 (patch) | |
| tree | 5ca54cdd479e4848517be6aa7ef14dac5c0cfdd8 | |
| parent | b57bf03d00c24260ee05676e533657fffa965b6b (diff) | |
Fix slow verification with z3 4.13
| -rw-r--r-- | fenwick.dfy | 4 |
1 files changed, 3 insertions, 1 deletions
diff --git a/fenwick.dfy b/fenwick.dfy index 958b5b1..aeee011 100644 --- a/fenwick.dfy +++ b/fenwick.dfy @@ -216,7 +216,8 @@ class fenwick { // FT array // 1-indexed and size N + 1 for Fenwick reasons // Sorry... - var F: array<int> + // const means we can modify F, but not reassign a completely new array to F + const F: array<int> // Check if F is a valid FT over A ghost predicate valid() @@ -280,6 +281,7 @@ class fenwick { assert F[j] == F[i]; assert j - lsb(j) / 2 <= i; assert F[j] == sum(A[j - lsb(j)..i]); + assert i + lsb(i) / 2 >= i && i + lsb(i) <= N; assert i + lsb(i) / 2 >= i && i + lsb(i) <= N ==> F[i] == sum(A[j - lsb(j)..i]); // Didn't break anything, hopefully assert forall j :: 0 < j <= i && j + (lsb(j) + 1) / 2 > i && j + lsb(j) <= N ==> lsb(j) < lsb(j + lsb(j)) && F[j + lsb(j)] == sum(A[j + lsb(j) - lsb(j + lsb(j))..j]) by { |