Change Request #3547
Check/fix identifier names generation in Z3
This is related to #3364 (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.