Java Modeling Language (JML) / Feature Requests / #145 jmlc doesn't handle quantifiers in in-line assertions

#145 jmlc doesn't handle quantifiers in in-line assertions

Status: open

Module:

Priority: 5

Updated: 2013-10-27

Created: 2008-03-10

Private: No

Gabriela Montoya produced the following test,
which doesn't work in the new RAC semantics, although it worked under JML 5.4.

The problem seems to be that quantifiers don't work with in-line assertions, although the RAC appropriately warns that it won't be executed.