janhaag/PSE2011 — Issue #100: Equal Bounds in forall does not work in SMTLibTranslator
Author: headri
Created: 2012-03-06 00:54:53+00:00
State: open
Labels: Verifier/SMTLib

The following program:
main(){}ensure forall x(1,1) x == 1;
has two problems:
1. Verifier says false but it should be true.
2. The following exception is thrown: line 3:21 required (...)+ loop did not match anything at input ')'