Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

[HACK_FIX] Term names with spaces are logged wrong #106

Closed
JonasAlaif opened this issue Jan 8, 2025 · 0 comments · Fixed by #107
Closed

[HACK_FIX] Term names with spaces are logged wrong #106

JonasAlaif opened this issue Jan 8, 2025 · 0 comments · Fixed by #107
Labels
z3-issue This can only be fixed in z3

Comments

@JonasAlaif
Copy link
Collaborator

This issue is due to a bug in z3.

Description

Unlike for :qid names which are logged correctly since Z3Prover/z3#6081 was resolved, the names of fun and const terms can have spaces and are not logged correctly. This leads to ambiguity if the names contain a term ID looking word which looks like an argument rather than the name (e.g. (declare-const |x #1| Int) looks like [mk-app] #25 x #1 in the log).

Hack fix

We forbid the ambiguous case above and while parsing a mk-app name we keep parsing words until we run into a valid term ID.
@JonasAlaif JonasAlaif added the z3-issue This can only be fixed in z3 label Jan 8, 2025
@JonasAlaif JonasAlaif mentioned this issue Jan 8, 2025
Merged
@JonasAlaif JonasAlaif changed the title Term names with spaces are logged wrong [HACK_FIX] Term names with spaces are logged wrong Jan 8, 2025
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
z3-issue This can only be fixed in z3
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Correctly parse term names with spaces viperproject/smt-scope
1 participant
@JonasAlaif