janhaag/PSE2011 — Issue #97: Quantifier with same variable don't work properly
Author: ratefuchs
Created: 2012-03-05 21:21:17+00:00
State: open
Labels: Verifier/SMTLib

In programs similar to the following program:

main(){assert exists x() x==2; assert exists x() x==1;}

the quantifiers have the same name (even with same scope information).
I don't know how to produce an actual failure, but chances are high that such a failure can be constructed.