Skip to content
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

Assertion failure in theory_seq.cpp #6178

Closed
mrkmarron opened this issue Jul 20, 2022 · 0 comments
Closed

Assertion failure in theory_seq.cpp #6178

mrkmarron opened this issue Jul 20, 2022 · 0 comments

Comments

@mrkmarron
Copy link
Contributor

I just triggered an assertion failure in theory_seq.cpp (probably with foldl use). Below is the assertion message and attached is a file that generates the failure. While investigating I also noticed that the lambda quantifiers are also not getting processed in internalize_assertions flow here either (previous issue).

ASSERTION VIOLATION
File: ..\src\smt\theory_seq.cpp
Line: 3076
UNEXPECTED CODE WAS REACHED.
Z3 4.9.2.0
``
[seq_assertion.smt2.txt](https://github.com/Z3Prover/z3/files/9154236/seq_assertion.smt2.txt)
`
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant