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
z3str3 assertion violation #2692
Comments
There is a propagate() inside theory_str::init_search_eh. Note however, that init_search_eh is called inside smt::context in a place where it is setting up various variables. |
Are you able to provide a stack trace? |
|
Reproduced on the latest commit. The context seems to become inconsistent immediately after |
I am testing a potential fix for this bug and will PR soon. |
Opened #2769 |
Hi,
z3 with z3str3 crashes on the following formula using smt.string_solver=z3str3
OS: Ubuntu 18.04
Revision: dd827ca
The text was updated successfully, but these errors were encountered: