Open Halbaroth opened 4 months ago
Note: it is easy for Dolmen to change that behavior and for instance treat as errors a problem that would try to redefine/shadow a builtin type (that is already being done for the smtlib). It all depends on the rules for the native ae language, which the alt-ergo team can choose.
I think we should forbid such redefinitions but we can do it after the next release.
IIRC it was used on function and value names, not on theory symbols, AFAIK the shadowing of theory symbols is not allowed in the SMT-LIB standard.
Dolmen accepts to shadow some builtin types. For instance, the input file:
produces the error:
The legacy frontend of Alt-Ergo accepts this input file because it uses the names of types as identifiers.
Notice this file is refused by both legacy and Dolmen frontend:
because
int
is a reserved token, which isn't the case offarray
.It seems shadowing is used in the SMT-LIB as noticed in the issue #712.