diff options
Diffstat (limited to 'Chalice/tests/examples/prog4.output.txt')
| -rw-r--r-- | Chalice/tests/examples/prog4.output.txt | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/Chalice/tests/examples/prog4.output.txt b/Chalice/tests/examples/prog4.output.txt index db9af8c2..9415df7c 100644 --- a/Chalice/tests/examples/prog4.output.txt +++ b/Chalice/tests/examples/prog4.output.txt @@ -8,6 +8,7 @@ Verification of prog4.chalice using parameters="" 34.5: The target of the release statement might not be locked by the current thread. 34.5: Release might fail because the current thread might hold the read lock. +The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification. 2.3: The end of method M is unreachable. Boogie program verifier finished with 7 errors and 1 smoke test warnings.
|