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

Liquid Fixpoint hangs on constraint #726

Open
vrindisbacher opened this issue Dec 16, 2024 · 3 comments
Open

Liquid Fixpoint hangs on constraint #726

vrindisbacher opened this issue Dec 16, 2024 · 3 comments

Comments

@vrindisbacher
Copy link
Contributor

@ranjitjhala here is the .smt2 file from earlier. Let me know if you need more info.

l.smt2.txt
@ranjitjhala
Copy link
Member

NVM. Ignore the above!

@vrindisbacher
Copy link
Contributor Author

@ranjitjhala, as mentioned in slack, seems like fixpoint run with cvc5 crushes this constraint no problem. I'm guessing it's more bitvectory things slowing down z3...

@ranjitjhala
Copy link
Member

Have posted an issue here Z3Prover/z3#7484

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@ranjitjhala @vrindisbacher