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

Jump to bottom

New unsoundness bug in z3str3 after recent pushes #2994

Closed
numairmansur opened this issue Feb 13, 2020 · 1 comment · Fixed by #2997
Closed

New unsoundness bug in z3str3 after recent pushes #2994

numairmansur opened this issue Feb 13, 2020 · 1 comment · Fixed by #2997
Assignees
@mtrberzi
Labels
string z3str3

Comments

@numairmansur
Copy link

Hi @mtrberzi
I have an example where z3str3 gives an unsound result. The following file is satisfiable but z3str3 gives unsat.

9.smt2

I think this bug was introduced after the recent changes in z3str3. It does not exist in commit 321bad2 .

The bug was found on the following commit:

commit 0146259
Author: Murphy Berzish murphy.berzish@gmail.com
Date: Wed Feb 12 13:46:27 2020 -0500
@mtrberzi mtrberzi self-assigned this Feb 13, 2020
@mtrberzi mtrberzi mentioned this issue Feb 13, 2020
Merged
@mtrberzi
Copy link
Collaborator

This was an interesting one. The bug ended up being exposed as a result of the commit you identified, but had been around for a while previous to that commit. Thanks for the report!

Opened #2997

# for free to join this conversation on GitHub. Already have an account? # to comment
Assignees

@mtrberzi mtrberzi

Labels
string z3str3
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

z3str3: assert precondition for regex length linearity axiom mtrberzi/z3
2 participants
@mtrberzi @numairmansur