diff options
Diffstat (limited to 'Test/VSI-Benchmarks/b3.dfy')
| -rw-r--r-- | Test/VSI-Benchmarks/b3.dfy | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/Test/VSI-Benchmarks/b3.dfy b/Test/VSI-Benchmarks/b3.dfy index 4f44612d..ed121ba0 100644 --- a/Test/VSI-Benchmarks/b3.dfy +++ b/Test/VSI-Benchmarks/b3.dfy @@ -100,7 +100,7 @@ class Benchmark3 { call r.Enqueue(m);
pperm:= pperm[k+1..|p|+1] + pperm[..k] + pperm[|p|+1..] +[pperm[k]];
}
- assert (forall i:int :: 0<=i && i < |perm| ==> perm[i] == pperm[i]); //needed to trigger axiom
+ assert (forall i:int :: 0<=i && i < |perm| ==> perm[i] == pperm[i]); //lemma needed to trigger axiom
}
|