5 Rejections
When a refinement claim fails, Liquid Shplait reports this and presents a counter-example:
`h`, call to `safe_div`, argument 2: the claim `(a + 1) != 0` is violated when a = -1 |
Only the values the failing claim depends on are shown. When every argument is a literal, there is nothing to show, and the message ends with “is violated”: the claim is false for the call as written.
Sometimes a claim may mathematically be true, but the prover is not able to
discharge it. In such cases, Liquid Shplait will halt with an error. This is an
inherent weakness of using refinement types—
The checker in Liquid Shplait cannot handle all the constructs of Shplait in their generality [Limitations]. When it cannot analyze a construct, it reprts a compile-time error:
`f`, return: cannot check: an anonymous `fun` cannot be used as a |
value here |