team-worthwhile/worthwhile — Issue #111: Interpreter does not resolve symbols in Assumptions
Author: bafain
Created: 2012-03-03 17:31:09+00:00
State: open
Labels: interpreter

Let the interpreter execute the following three Worthwhile programs, each time the assertion (wrapped in a quantified expression so that the prover is asked as the interpreter not yet takes assumptions in consideration when evaluating simple assertions) should succeed since when the `_assume`s are visited `false` is assumed.

_assume false
_assert ∀ Integer i : 1 = 0

and

if (true) {
Boolean c := false
_assume c
}
_assert ∀ Integer i : 1 = 0

and

Boolean c := false
_assume c
c := true
_assert ∀ Integer i : 1 = 0

In the last two examples this not actual behaviour because one time `c` is no more present in the environment and the other time `c` is reassigned (to true) before the assumption is evaluated. Both times the assumed expression is changed after it was executed.