Variablennamen in generiertem SMTLIB-Code ändern

team-worthwhile / worthwhile

PSE am KIT 2011/12: Programmverifikation (Team 2)

BSD 3-Clause "New" or "Revised" License

5 stars 3 forks source link

Variablennamen in generiertem SMTLIB-Code ändern #9

Closed jspam closed 12 years ago

jspam commented 12 years ago

Da Worthwhile-Variablen potenziell so heißen können wie SMTLIB-Schlüsselwörter, sollten die generierten Variablen im SMTLIB-Code so heißen, dass keine Konflikte entstehen können, beispielsweise durch Anhängen von _

jspam commented 12 years ago

Offensichtlich ist Z3 so intelligent, dass hier keine Konflikte entstehen. Daher ist dieser Bug irrelevant.

Getestet mit folgenden Variablennamen: as distinct let forall exists par NUMERAL Bool