Check/fix identifier names generation in Z3
This is related to #3364 (closed) (some todos in the exploration.smt package were still referencing such a closed issue).
In particular these todos refer to:
- the fact of using only the first symbol of names to generate Z3 identifiers;
- how to deal with the symbol “|”, introduced by Z3 when special symbols are encountered inside a name.
Check if the approach used is safe in all cases, and possibly unify/centralize generation of names and equality checking.
(from redmine: issue id 3547, created on 2018-10-08)