Skip to content

Update to Z3 4.7.1 #128

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
Closed
PhilippWendler opened this issue May 25, 2018 · 4 comments
Closed

Update to Z3 4.7.1 #128

PhilippWendler opened this issue May 25, 2018 · 4 comments
Labels
Z3

Comments

@PhilippWendler
Copy link
Member

PhilippWendler commented May 25, 2018 •
edited
Loading

Z3 4.7.1 is released, but upgrading JavaSMT to it produces a failing test: VariableNamesTest.testBoolVariableEscaping (cf. branch z3-4.7.1 and the Travis build for it).

This is related to the escaping of variable names and probably requires that we come to a conclusion for #26 first. If we forbid all variable names with | in them, this test would not be a problem (it checks what happens if we create a variable with |). However, if we decide otherwise, I do not know what to do to fix this.
@PhilippWendler PhilippWendler mentioned this issue May 25, 2018
Open
@PhilippWendler
Copy link
Member Author

It seems that the tests go through after 0dc6a4b. Is there anything left to do before merging z3-4.7.1?

@PhilippWendler
Copy link
Member Author

Ping?

@kfriedberger
Copy link
Member

Variable names should work now. I assume we can merge/reintegrate the branch.

@kfriedberger kfriedberger mentioned this issue Oct 8, 2018
Merged
@kfriedberger
Copy link
Member

Rebased, merged, done.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
Z3
Milestone
No milestone
Development

No branches or pull requests
2 participants
@PhilippWendler @kfriedberger