summaryrefslogtreecommitdiff
path: root/Chalice/tests/regressions/workitem-10195.output.txt
blob: 6e8b355684ef594ec508465ce2244e1ae64da54f (plain)
1
2
3
4
5
6
7
8
9
10
11
12
Verification of workitem-10195.chalice using parameters="" 

  4.14: Range minimum might not be smaller or equal to range maximum.
  10.14: Range minimum might not be smaller or equal to range maximum.

The program did not fully verify; the smoke warnings might be misleading if contradictions are introduced by failing proof attempts of the verification.
  2.5: The end of method fails is unreachable.
  8.5: The end of method succeeds1 is unreachable.
  19.9: Precondition of method succeeds2 is equivalent to false.
  27.9: Precondition of method fails2 is equivalent to false.

Boogie program verifier finished with 2 errors and 4 smoke test warnings