blob: b9dd1d88c5ceca3d6091d2ea90da94a3454b5d3e (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
matrix-accesses-are-triggers.dfy(8,11): Warning: Selected triggers: {m[i, j]} (loops with {m[j, i + 1]})
(!) Suppressing loops would leave this expression without triggers.
matrix-accesses-are-triggers.dfy(8,81): Error: index 0 out of range
Execution trace:
(0,0): anon0
(0,0): anon4_Then
matrix-accesses-are-triggers.dfy(8,86): Error: index 1 out of range
Execution trace:
(0,0): anon0
(0,0): anon4_Then
Dafny program verifier finished with 1 verified, 2 errors
|