Optimistic conditional branching results in inconsistent ? semantics.

[cliu369]

Currently, we would like gradual formulas (? && p) to justify something unsatisfiable only if p is already unsatisfiable.

The following program does not adhere to this:

method foo(b: Bool) 
    requires ? && (b ? true : false)
    ensures false
{
}

Verification of foo succeeds with a run-time check for !b. This happens because the verifier branches on the conditional in the precondition. In the path where b == true, true is produced and verification fails. But in the path where b == false, false is produced and verification succeeds. Then, the verifier will try to force dynamic execution down the successful path by adding a run-time check for b == false or !b.

However, verification of foo should not succeed, since the precondition of foo is then justifying false, even though the precise part of the precondition is satisfiable. As a result, we would like the implementation to detect this behavior and prevent it.