Summary

A call-site precondition (E501) is not statically checked when the call appears at or after a let-destructure statement in a function body (or in the block's final expression when the block contains any destructure). The program verifies tier1-clean even though the precondition was never discharged.

This is a verification completeness / classification gap, not a silent wrong answer: the callee's own runtime requires(...) contract check still traps if the precondition is violated, so it should be reported tier3_runtime, not tier1. Pre-existing and refinement-independent — surfaced while reviewing #746 (PR #763).

Root cause

SmtContext._translate_block (vera/smt.py) bails at the first non-LetStmt/ExprStmt statement:

else:
    # LetDestruct or unknown statement type
    return None  # pragma: no cover

A let Ctor<...> = ...; destructure hits this branch, so the block translation returns None, truncating SMT translation of everything from the destructure onward — including the block's final expression. Call-site preconditions are collected during that main SMT body translation (drain_call_violations), so any call at/after the destructure is never seen. (The # pragma: no cover shows this path was assumed unreachable; a destructure followed by a call reaches it.)

Reproduction

public fn needs_pos(@Int -> @Int)
  requires(@Int.0 > 0) ensures(true) effects(pure)
{ @Int.0 }

public fn mk(@Int -> @Tuple<Int, Int>)
  requires(true) ensures(true) effects(pure)
{ Tuple(@Int.0, 3) }

public fn f(@Int -> @Int)
  requires(true) ensures(true) effects(pure)
{
  let Tuple<@Int, @Int> = mk(@Int.0);
  needs_pos(@Int.1)            -- @Int.1 is unconstrained; requires(> 0) NOT checked
}

vera verify reports this clean at tier1 (no E501). The same body with the call before the destructure correctly fires E501, and the no-destructure baseline correctly fires E501 — confirming the destructure is what truncates the check.

Scope (verified)

• Affected: call-site preconditions (E501) — and any check done via the main SMT body translation, e.g. a postcondition on the result — for statements at/after a let-destructure, or in the block's final expression when the block contains a destructure.
• NOT affected: @Nat/refinement narrowing obligations (E503/E504/E505/E506). These are separate AST walks (_walk_for_nat_binding_obligations, _obligate_destructure_narrowings) that traverse the whole body, so a violating @Nat narrowing after a destructure is still caught.
• NOT affected: call preconditions before the destructure (the block loop processes statements in order, bailing only at the destructure).

Suggested fix

Teach _translate_block to model a LetDestruct — bind each component (via the same tuple/ADT accessor machinery the obligation walks use) into current_env and continue — rather than returning None. This also lets a refined component's value flow into subsequent precondition checks (the destructure analogue of the match-arm source-fact work in #763).

Relationship

Same user-facing class as #730 (calls in statement position are never precondition-checked, runtime-guarded only), but a distinct root cause (block-translation truncation vs. statement-position calls). Both are verification-completeness gaps where the runtime contract check is the only backstop.