Non-determinism in ACSL

[vprevosto]

Is there a need for a non-deterministic constructor such as \any T x; P(x)?

[pbaudin]

The construct \any T x ; P(x) is similar to let x of type T such that P(x) in x.

As far as I can remember, the answer was definitely no because this construct is not part of the first order logic. We wanted to have t==t being true for any term t. That may not be the case for the equality ( \any T x; P(x)) == ( \any T x; P(x)).