Project

General

Profile

Change Request #3547

Check/fix identifier names generation in Z3

Added by Marco Volpe almost 2 years ago. Updated about 2 months ago.

Status:
New
Priority:
Normal
Assignee:
Category:
SMT
Target version:
Start date:
10/08/2018
Due date:
% Done:

0%

Estimated time:

Description

Current status.

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.

Proposed change.
Check if the approach used is safe in all cases, and possibly unify/centralize generation of names and equality checking.

History

#1 Updated by Alexander Diewald over 1 year ago

  • Target version changed from AF3 2.15 RC1 (Feature Freeze) to AF3 2.15 RC1 (Feature Freeze)

#2 Updated by Johannes Eder over 1 year ago

  • Target version changed from AF3 2.15 RC1 (Feature Freeze) to AF3 2.16 RC1 (Feature Freeze)

#3 Updated by Marco Volpe 12 months ago

  • Target version changed from AF3 2.16 RC1 (Feature Freeze) to AF3 2.17 (Tested, Bug Free)

#4 Updated by Alexander Diewald 12 months ago

  • Category set to SMT
  • Target version changed from AF3 2.17 (Tested, Bug Free) to AF3 2.17 (Feature Freeze)

#5 Updated by Alexander Diewald 8 months ago

  • Target version changed from AF3 2.17 (Feature Freeze) to Backlog

#6 Updated by Marco Volpe about 2 months ago

  • Assignee changed from Marco Volpe to Johannes Eder

Also available in: Atom PDF