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.

Sign up for GitHub

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

Jump to bottom

Spacer (global guidance): assertion failed #6543

Closed
corwin-of-amber opened this issue Jan 18, 2023 · 3 comments
Closed

Spacer (global guidance): assertion failed #6543

corwin-of-amber opened this issue Jan 18, 2023 · 3 comments
Assignees
@agurfinkel @hgvk94
Labels
Horn

Comments

@corwin-of-amber
Copy link

I stumbled upon this situation:

ASSERTION VIOLATION
File: /Users/corwin/var/ext/z3/master/src/muz/spacer/spacer_global_generalizer.cpp
Line: 331
UNEXPECTED CODE WAS REACHED.
4.12.0.0 ca6fed8b25331cd6a472d3296b4b28b73c0c993b z3-4.8.4-7099-gca6fed8b2
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new

This is the file that caused it.
assertion_failed_in_globalgen.smt2.txt

z3 fp.spacer.global=true assertion_failed_in_globalgen.smt2
@NikolajBjorner
Copy link
Contributor

What should be done about the bug reported by the second son of Oberon and father of Merlin?

@hgvk94
Copy link
Contributor

hgvk94 commented Feb 22, 2023

Thanks for reporting it. I am looking into it.
Sorry, it's been a month. I was in paper deadline mode and didn't notice the time.

agurfinkel added a commit that referenced this issue Feb 24, 2023
@agurfinkel
Merge pull request #6608 from hgvk94/bugfix
358caa8 
fix #6543. don't assume order on bindings
@corwin-of-amber
Copy link
Author

Hurray go Hari 🎉

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

@agurfinkel agurfinkel

@hgvk94 hgvk94

Labels
Horn
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
4 participants
@corwin-of-amber @NikolajBjorner @agurfinkel @hgvk94