W7002 vacuous_obligation
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:
fn f(x: Int) -> Int
requires x > 0 && x < 0
ensures result > 100
{ x }Fixed:
fn f(x: Int) -> Int
requires x > 0
ensures result > 0
{ x }Wrong program
No fixture in compiler/tests/ui reports this code yet.
Fixed program
No fixed program yet; the explanation above describes the repair.