Conversation
Also fix the orchestrator deadlock when queued work is dropped on abort, and the spurious "all branches reverted" warning after an early abort. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
msooseth
marked this pull request as draft
September 22, 2026 10:05
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Replace the slow mulmod CLI test with deterministic solver-level tests and a verify-level test that catches the orchestrator deadlock. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
msooseth
marked this pull request as ready for review
September 22, 2026 10:57
A shell-script fixture cannot be spawned on Windows; the test binary works everywhere and is never installed. Co-Authored-By: Claude Opus 5 (1M context) <noreply@anthropic.com>
msooseth
added this pull request to stack #1097
September 22, 2026 12:53
gustavo-grieco
left a comment
gustavo-grieco
left a comment
Collaborator
There was a problem hiding this comment.
Any reason not to have this as default? Maybe we could even remove the flag and always use it?
Collaborator
Author
|
I was going to ask you if you are interested to have this as default :) Yes, I think that would be great. We can make it as default for the CLI. Not for API, I think, users can choose it? What do you think? And then we can have the |
Collaborator
|
I think making this the default makes a lot of sense, but allowing to use |
This branch has not been deployed
This file contains hidden or bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
2 participants
Add this suggestion to a batch that can be applied as a single commit.This suggestion is invalid because no changes were made to the code.Suggestions cannot be applied while the pull request is closed.Suggestions cannot be applied while viewing a subset of changes.Only one suggestion per line can be applied in a batch.Add this suggestion to a batch that can be applied as a single commit.Applying suggestions on deleted lines is not supported.You must change the existing code in this line in order to create a valid suggestion.Outdated suggestions cannot be applied.This suggestion has been applied or marked resolved.Suggestions cannot be applied from pending reviews.Suggestions cannot be applied on multi-line comments.Suggestions cannot be applied while the pull request is queued to merge.Suggestion cannot be applied right now. Please check back later.
Description
With
--early-abort, SMT solvers that are still running are now killed once a counterexample is found, instead of running to completion. Fixes #938.Also fixes a deadlock ("thread blocked indefinitely in an STM transaction") when paths are still queued at abort time, and a spurious "all branches reverted" warning after an early abort.
The tests now have a "hanging solver" fixture to be able to test early abort. This solver always hangs, so we can properly check without using hacks like a very complicated query.
Checklist