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—
A construct that Liquid Shplait cannot analyze is a compile-time error naming the construct:
fun `f`: cannot check the return obligation: call to `string_append`, |
which is neither a function defined in this module nor one of the |
builtins the checker models (`max`, `min`, ...) |