janhaag/PSE2011 — Issue #67: program containing certain variables behave strange
Author: ratefuchs
Created: 2012-02-28 21:49:36+00:00
State: open
Labels: Verifier/SMTLib

When trying to prove the following program:
main(int ite){}ensure ite==1;
no result is given to gui consoles, but my IDE console shows the following error messages:

line 1:0 required (...)+ loop did not match anything at input '('
line 1:45 no viable alternative at character ','

It works fine with variables like "f", "t", or "_ite".
It also fails with "distinct".

Probably there's a conflict with SMTLib functions.