summaryrefslogtreecommitdiff
path: root/Chalice/tests/regressions/internal-bug-2.output.txt
blob: 3b76365910f9599e951cd2fa45310af288791a81 (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.