E0010 — Contract violation

A requires or ensures clause evaluated to false at runtime.

---

What triggers it

requires is checked before the function body runs; ensures is checked after with result bound to the return value. When the clause evaluates to false, the runtime aborts with E0010 and names the clause that failed. Programs run through resilient verify can lift these to compile-time Z3 checks instead.

Minimal example

fn halve(int n) -> int
    requires n >= 0
{
    return n / 2;
}
fn main() {
    return halve(-4);
}

Output:

scratch.rs:2:18: error[E0010]: contract violation in fn halve: requires n >= 0 failed
    requires n >= 0
             ^^^^^^

Fix

Either meet the contract at the call site, or weaken the clause if the contract was too strict. If you suspect a bug in how the clause is written, the Z3 verifier tutorial walks through how to prove clauses ahead of time so violations become impossible, not just reported.

fn halve(int n) -> int
    requires n >= 0
{
    return n / 2;
}
fn main() {
    return halve(4);
}

Source

Emitted from apply_function in resilient/src/main.rs (both requires and ensures arms).