Currently stopOnFirstError in verifySingleEnv uses isNotSuccess which treats any non-success (including warnings, inconclusive, timeouts) as a reason to stop. The CLI exit code logic in StrataMain.lean uses a more nuanced classification: !r.isSuccess && !r.isTimeout && !r.isImplementationError && !r.hasSMTError.
The stopOnFirstError condition should be aligned with the check-mode-aware classification (similar to outcomeToLevel in SarifOutput.lean) so that only true failures (depending on --check-mode) trigger early termination.
This affects both the sequential and parallel paths in verifySingleEnv.
Ref: PR #1046 review discussion.
Currently
stopOnFirstErrorinverifySingleEnvusesisNotSuccesswhich treats any non-success (including warnings, inconclusive, timeouts) as a reason to stop. The CLI exit code logic inStrataMain.leanuses a more nuanced classification:!r.isSuccess && !r.isTimeout && !r.isImplementationError && !r.hasSMTError.The
stopOnFirstErrorcondition should be aligned with the check-mode-aware classification (similar tooutcomeToLevelinSarifOutput.lean) so that only true failures (depending on--check-mode) trigger early termination.This affects both the sequential and parallel paths in
verifySingleEnv.Ref: PR #1046 review discussion.