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

Update dependency: deps/z3 #2675

Conversation

rv-jenkins
Copy link
Contributor

No description provided.

@PetarMax
Copy link
Contributor

PetarMax commented Jan 9, 2025

This is very unfortunate, I have no idea why that proof is failing. Are there any dependencies that need to be synchronised somewhere else? Much more complex SMT queries are passing in real-world engagements, and I'm pretty sure in other tests here as well.

@palinatolmach
Copy link
Contributor

Are there any dependencies that need to be synchronised somewhere else?

@PetarMax I don't think so, but I'll ask @jberthold once he's back on Monday! I planned to push a commit increasing the timeout to see if it helps, you've said that it only passes on your machine with retries and the timeout of 300, right?

@palinatolmach palinatolmach force-pushed the _update-deps/runtimeverification/z3-images branch from bdc5c93 to ab5b7ec Compare January 9, 2025 14:13
@palinatolmach
Copy link
Contributor

I doubled the SMT timeout and retry limit for test_prove_rules[examples/sum-to-n-spec.k] (to 600 and 20, respectively) to see if it helps.

@PetarMax
Copy link
Contributor

There's a slightly deeper problem, likely inside z3. I've pushed a temp fix.

@palinatolmach palinatolmach self-requested a review January 13, 2025 12:23
@automergerpr-permission-manager automergerpr-permission-manager bot merged commit f28dcd9 into master Jan 13, 2025
12 checks passed
@automergerpr-permission-manager automergerpr-permission-manager bot deleted the _update-deps/runtimeverification/z3-images branch January 13, 2025 13:42
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Projects
None yet
Development

Successfully merging this pull request may close these issues.

4 participants