# W7002 vacuous_obligation

URL: /docs/errors/W7002
Markdown: /docs/errors/W7002.md

> A contract obligation was proved only because the assumptions on its path are contradictory, so the path can never run and the proof says nothing useful (design §17.98, §17.105).

A warning from the `verify` phase. `sakura explain W7002` prints this explanation offline.

A contract obligation was proved only because the assumptions on its path are contradictory, so
the path can never run and the proof says nothing useful (design §17.98, §17.105). The verifier
checks the path's feasibility first; `unsat` is reported as `proved` with `path_feasible: false`
and this warning. Usually a `requires` or a branch condition rules out every input; remove the
contradiction or the dead branch.

Warning:

```sakura
fn f(x: Int) -> Int
  requires x > 0 && x < 0
  ensures result > 100
{ x }
```

Fixed:

```sakura
fn f(x: Int) -> Int
  requires x > 0
  ensures result > 0
{ x }
```

## Wrong program [#wrong-program]

No fixture in `compiler/tests/ui` reports this code yet.

## Fixed program [#fixed-program]

No fixed program yet; the explanation above describes the repair.