Skip to content
New issue

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

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

Already on GitHub? # to your account

New unsoundness issue in z3str3 #3031

Closed
numairmansur opened this issue Feb 17, 2020 · 1 comment
Closed

New unsoundness issue in z3str3 #3031

numairmansur opened this issue Feb 17, 2020 · 1 comment
Assignees

Comments

@numairmansur
Copy link

Hi @mtrberzi,

In the latest commit (41ab578) i get the following incorrect result on the following file:

66.zip

$ ./z3-nightly/bin/z3 smt.string_solver=z3str3 66.smt2 
sat
sat
sat
sat
unsat

Everything should be sat.

Interestingly, in commit 321bad2, i still get a wrong answer but a different one:

$ ./z3-321b/bin/z3 smt.string_solver=z3str3 66.smt2 
sat
sat
unsat
unsat
unsat

@mtrberzi
Copy link
Collaborator

This is fixed as of the latest commit (5 SAT responses and all models are valid).

# for free to join this conversation on GitHub. Already have an account? # to comment
Projects
None yet
Development

No branches or pull requests

2 participants