team-worthwhile / worthwhile

PSE am KIT 2011/12: Programmverifikation (Team 2)
BSD 3-Clause "New" or "Revised" License
5 stars 3 forks source link

Prover fails to incorporate condition of quantified expression into proof #68

Closed jspam closed 12 years ago

jspam commented 12 years ago

Test program for this is test-qexpr-condition.ww, tested in CheckProgramTest::testTestProgramValidity[9]:

// EXPECTED:VALID
function Integer test(Integer i)
    _requires i ≥ 0
    _ensures _return = 42
{
    return 42
}

_assert ∀ Integer j, j ≥ 0 : test(j) = 42

Generated formula and model output here

I expect the program to be valid, instead the "counterexample" j = -1 is provided. This should not happen since I only tried to prove the formula for j >= 0.

When I remove the precondition i >= 0, the program verifies correctly.