{:inline 0} is inconsistent

[petemud]

Under /inline:assume, which is default

procedure {:inline 0} inline0() {}

procedure inconsistent() {
    call inline0();
    assert true == false;
}

becomes

procedure inconsistent() {
    assume false;
    assert true == false;
}

Boogie program verifier finished with 1 verified, 0 errors

---

The bug got introduced in 08e368784c1ae629d870db6b09edadbef306e1d6

[shazqadeer]

This is not a bug. Rather it is intended behavior. Boogie provides ways to customize what happens when the inline limit for a procedure is reached. See the documentation here.

[petemud]

Why is proving true==false ever an intended behavior? If it is intended under an option, at least this option shouldn't be the default

[shazqadeer]

What default would you prefer?

[petemud]

You choose. The consistent and sound options if inline depth reaches 0 are:

1. put a call (inline requires and ensures)
2. only inline requires as assert or - only if there are no requires - drop a call completely
3. instead of inlining requires put assert false

Putting assume false ever is plainly inconsistent. As for dropping call when there are requires - it is unsound, because this way you can prove more, not less