summaryrefslogtreecommitdiff
path: root/Chalice/tests/regressions/internal-bug-2.output.txt
blob: 8724af64f05fca1ec84ef722aeb20c7d408063b5 (plain)
1
2
3
4
5
6
7
8
Verification of internal-bug-2.chalice using parameters="" 

  9.9: Location might not be writable

The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
  6.5: The end of method koko is unreachable.

Boogie program verifier finished with 1 errors and 1 smoke test warnings