E0019 — Z3 could not prove a contract clause

The static (Z3) verifier could not prove a requires or ensures clause ahead of time.

---

What triggers it

Building with --features z3 and running rz verify (or rz --audit) lifts contract clauses to SMT queries. When Z3 returns unsat/unknown for the clause’s negation, verification fails at compile time — distinct from E0010, which is the same clause failing at runtime on a build without static verification.

Minimal example

fn halve(int n) -> int
    ensures result * 2 == n
{
    return n / 2 + 1;
}

Output:

scratch.rz:2:14: error[E0019]: Z3 could not prove ensures clause in fn halve
    ensures result * 2 == n
            ^^^^^^^^^^^^^^^

Fix

Fix the clause or the implementation so the postcondition actually holds, or weaken the clause to what the implementation guarantees.

fn halve(int n) -> int
    ensures result * 2 <= n
{
    return n / 2;
}

Source

Emitted from the Z3 bridge in resilient/src/z3_bridge.rs (gated on feature = "z3").