-
Notifications
You must be signed in to change notification settings - Fork 1.5k
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.
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
Unsoundness issue with smt.string_solver=z3str3 #6159
Comments
There is currently a stream of bugs reported to z3str3 but at this point no reaction on when or whether they are going to be addressed. If there is no response, it will be more practical to lump these bugs into a larger issue. In the past we ended up with a large fraction of open issues against z3 being for z3str3. |
Ok, then I will add more issue to this thread if I find more regarding z3str3 |
Adding a few cases (there seem to be quite many):
|
|
|
|
|
|
|
|
This bug has been fixed in #6312 |
Hi,
for the following formula z3 incorrectly reports
sat
instead ofunsat
.OS: Ubuntu 20.04
The text was updated successfully, but these errors were encountered: