We read every piece of feedback, and take your input very seriously.
To see all available qualifiers, see our documentation.
There was an error while loading. Please reload this page.
1 parent a4abbed commit c8e375cCopy full SHA for c8e375c
test/golden/Server/spec-qm-5.gcl.golden
@@ -5,12 +5,12 @@ Sweep Result { POs: [ Loop Invariant at ./test/source/Server/spec-qm-5.gcl [53-7
5
⇒
6
f[n] = 0`
7
explanation not available
8
- , After Loop at ./test/source/Server/spec-qm-5.gcl [78-146] 6:1-10:3 #10b2d1130ba729f6
+ , InvBase at ./test/source/Server/spec-qm-5.gcl [78-146] 6:1-10:3 #10b2d1130ba729f6
9
`f[n] = 0 ∧¬ n ≠ N
10
11
True`
12
The loop invariant f[n] = 0 should remain true while all the guards n ≠ N become false after executing the loop
13
- , Loop Termination at ./test/source/Server/spec-qm-5.gcl [78-146] 6:1-10:3 #762377d90313a209
+ , TermBase at ./test/source/Server/spec-qm-5.gcl [78-146] 6:1-10:3 #762377d90313a209
14
`f[n] = 0 ∧n ≠ N
15
16
N - n ≥ 0`
0 commit comments