janhaag/PSE2011 — Issue #83: Division in quantifier range is translated wrong
Author: ratefuchs
Created: 2012-03-03 20:16:23+00:00
State: open
Labels: Parser

When executing the following program:

main(){int z=2;}ensure exists z(0,1/z) true;

the ensure fails. Debugging shows that the parser pushes the "division by zero prevention" into the expression that is quantified (i.e. makes it to "ensure exists z(1,1/z) ((z != 0) & true)"). But that moves the expression into an inner scope and the inner z is taken to evaluate z != 0. But it has to be the outer z.