Separate SMT error categories: encoding, timeout, crash (#1090)

## Summary

Distinguishes three error types in `VCResult` instead of a single
"Implementation Error" string:
- `VCError.encoding`: SMT encoding failure (Strata bug, exit code 3)
- `VCError.solverTimeout`: solver exceeded time limit (exit 0 — treated
as inconclusive)
- `VCError.solverCrash`: solver process failed (exit code 3)

Timeout detection checks z3's `"timeout"` on stdout and cvc5's
`"interrupted by timeout"` on stderr.

`pyAnalyzeLaurel` summary partitions timeouts separately from internal
errors. `strata verify` command uses exit code 3 for internal errors
(previously all non-success was exit 2). Solver invocation errors now
return a `VCResult` instead of throwing `DiagnosticModel`, so remaining
obligations continue processing.

### Exit code table

| Code | Meaning | When |
|------|---------|------|
| 0 | Success / Inconclusive | All assertions pass, some inconclusive,
or solver timed out |
| 1 | User error | Bad input, unsupported flag |
| 2 | Failures found | Assertion violations |
| 3 | Internal error | SMT encoding failure or solver crash |
| 4 | Known limitation | Unsupported Python construct |

---------

Co-authored-by: Claude Opus 4.6 (1M context) <noreply@anthropic.com>
Co-authored-by: Mikael Mayer <mimayere@amazon.com>

Author: 3 people

DiffTestCore.lean

@@ -108,7 +108,7 @@ def checkMatch (pyRegex testStr : String) (mode : MatchMode)
           if vc.isSuccess then return .match
           else if vc.isFailure then return .noMatch
           else return match vc.outcome with
-            | .error msg => .smtError s!"impl: {msg}"
+            | .error err => .smtError s!"impl: {err}"
             | _ => .smtError "unknown"
 
 def main (args : List String) : IO UInt32 := do

Strata/DL/Imperative/SMTUtils.lean

@@ -115,6 +115,26 @@ def runSolver (solver : String) (args : Array String) : IO IO.Process.Output :=
   --                         stdout: {repr output.stdout}"
   return output
 
+/-- Classifies the error when the solver fails to produce a valid verdict. -/
+inductive SolverError where
+  | timeout (detail : String)
+  | crash (detail : String)
+
+instance : ToString SolverError where
+  toString
+    | .timeout d => s!"Solver timeout: {d}"
+    | .crash d   => s!"Solver crash: {d}"
+
+/-- True when the word "timeout" appears as a whitespace-delimited token
+    in the solver's stdout or stderr. z3 emits "timeout" as a standalone
+    line on stdout; cvc5 prints "interrupted by timeout." on stderr.
+    Only called when verdict parsing has already failed. -/
+private def isTimeoutOutput (output : IO.Process.Output) : Bool :=
+  let hasWord (s : String) := s.splitOn "\n" |>.any fun line =>
+    line.splitOn " " |>.any fun tok =>
+      tok.trimAscii.toString == "timeout" || tok.trimAscii.toString == "timeout."
+  hasWord output.stdout || hasWord output.stderr
+
 ---------------------------------------------------------------------
 -- SMTDDM-based parsing
 ---------------------------------------------------------------------
@@ -206,7 +226,7 @@ def solverResult {P : PureExpr} [ToFormat P.Ident]
     (vars : List P.TypedIdent) (output : IO.Process.Output)
     (E : Strata.SMT.EncoderState) (smtsolver : String)
     (satisfiabilityCheck validityCheck : Bool)
-    : IO (Except Format (Result P.Ident × Result P.Ident)) := do
+    : IO (Except SolverError (Result P.Ident × Result P.Ident)) := do
   let stdout := output.stdout
 
   -- Helper to parse a single verdict and model
@@ -234,29 +254,26 @@ def solverResult {P : PureExpr} [ToFormat P.Ident]
     | "unknown" => return some (.unknown, skipToNextVerdict rest)
     | _ => return none
 
-  -- Parse results based on which checks are enabled
-  match ← (if satisfiabilityCheck then parseVerdict stdout else pure (some (.unknown, stdout))) with
-  | some (satResult, remaining) =>
-    match ← (if validityCheck then parseVerdict remaining else pure (some (.unknown, remaining))) with
-    | some (validityResult, _) => return .ok (satResult, validityResult)
-    | none =>
-      let stderr := output.stderr
-      let hasExecError := stderr.contains "could not execute external process"
-      let hasFileError := stderr.contains "No such file or directory"
-      let suggestion :=
-        if (hasExecError || hasFileError) && smtsolver == Core.defaultSolver then
-          s!" \nEnsure {Core.defaultSolver} is on your PATH or use --solver to specify another SMT solver."
-        else ""
-      return .error s!"stderr:{stderr}{suggestion}\nsolver stdout: {output.stdout}\n"
-  | none =>
+  let mkError (output : IO.Process.Output) : SolverError :=
     let stderr := output.stderr
     let hasExecError := stderr.contains "could not execute external process"
     let hasFileError := stderr.contains "No such file or directory"
     let suggestion :=
       if (hasExecError || hasFileError) && smtsolver == Core.defaultSolver then
         s!" \nEnsure {Core.defaultSolver} is on your PATH or use --solver to specify another SMT solver."
       else ""
-    return .error s!"stderr:{stderr}{suggestion}\nsolver stdout: {output.stdout}\n"
+    let detail := s!"stderr:{stderr}{suggestion}\nsolver stdout: {output.stdout}\n"
+    if isTimeoutOutput output then .timeout detail else .crash detail
+
+  -- Parse results based on which checks are enabled
+  match ← (if satisfiabilityCheck then parseVerdict stdout else pure (some (.unknown, stdout))) with
+  | some (satResult, remaining) =>
+    match ← (if validityCheck then parseVerdict remaining else pure (some (.unknown, remaining))) with
+    | some (validityResult, _) => return .ok (satResult, validityResult)
+    | none =>
+      return .error (mkError output)
+  | none =>
+    return .error (mkError output)
 
 def addLocationInfo {P : PureExpr} [BEq P.Ident]
   (md : Imperative.MetaData P) (message : String × String)
@@ -287,7 +304,7 @@ def dischargeObligation {P : PureExpr} [ToFormat P.Ident] [BEq P.Ident]
   (solver_options : Array String) (printFilename : Bool)
   (satisfiabilityCheck validityCheck : Bool)
   (skipSolver : Bool := false) :
-  IO (Except Format (Result P.Ident × Result P.Ident × Strata.SMT.EncoderState)) := do
+  IO (Except SolverError (Result P.Ident × Result P.Ident × Strata.SMT.EncoderState)) := do
   let handle ← IO.FS.Handle.mk filename IO.FS.Mode.write
   let solver ← Strata.SMT.Solver.fileWriter handle
 

Strata/Languages/Core/SarifOutput.lean

@@ -115,9 +115,9 @@ def vcResultToSarifResult (mode : VerificationMode) (files : Map Strata.Uri Lean
   let ruleId := vcr.obligation.label
   let relatedLocations := extractRelatedLocations files vcr.obligation.metadata
   match vcr.outcome with
-  | .error msg =>
+  | .error err =>
     let level := .error
-    let messageText := s!"Verification error: {msg}"
+    let messageText := s!"Verification error: {err}"
     let message : Strata.Sarif.Message := { text := messageText }
     let locations := match extractLocation files vcr.obligation.metadata with
       | some loc => #[locationToSarif loc]

Strata/Languages/Core/Verifier.lean

@@ -203,7 +203,7 @@ def dischargeObligation
   (label : String)
   (varDefinitions : List VarDefinition := [])
   (varDeclarations : List VarDeclaration := [])
-  : IO (Except Format (SMT.Result × SMT.Result × EncoderState)) := do
+  : IO (Except Imperative.SMT.SolverError (SMT.Result × SMT.Result × EncoderState)) := do
   -- CVC5 requires --incremental for multiple (check-sat) commands
   let baseFlags := getSolverFlags options
   let needsIncremental := satisfiabilityCheck && validityCheck
@@ -588,13 +588,26 @@ def LExprModel.format (model : LExprModel) : Format :=
 instance : ToFormat LExprModel where
   format := LExprModel.format
 
+/-- Classifies errors that prevent a verification condition from being resolved. -/
+inductive VCError where
+  | encoding (msg : String)
+  | solverTimeout (msg : String)
+  | solverCrash (msg : String)
+  deriving Repr, BEq
+
+instance : ToString VCError where
+  toString
+    | .encoding msg      => s!"SMT Encoding Error! {msg}"
+    | .solverTimeout msg => s!"Solver Timeout! {msg}"
+    | .solverCrash msg   => s!"SMT Solver Crash! {msg}"
+
 /--
 A collection of all information relevant to a verification condition's
 analysis.
 -/
 structure VCResult where
   obligation : Imperative.ProofObligation Expression
-  outcome : Except String VCOutcome := .error "not yet computed"
+  outcome : Except VCError VCOutcome
   estate : EncoderState := EncoderState.init
   verbose : VerboseMode := .normal
   checkLevel : CheckLevel := .minimal
@@ -625,7 +638,7 @@ instance : ToFormat VCResult where
     match r.outcome with
     | .error e =>
       let prop := r.obligation.property
-      f!"Obligation: {r.obligation.label}\nProperty: {prop}\nResult: 🚨 Implementation Error! {e}"
+      f!"Obligation: {r.obligation.label}\nProperty: {prop}\nResult: 🚨 {toString e}"
     | .ok outcome =>
       let modelFmt :=
         if r.verbose >= .models && !r.lexprModel.isEmpty then
@@ -644,7 +657,7 @@ def VCResult.formatOutcome (r : VCResult) : String :=
     let suffix := o.pathSummary prop r.checkLevel r.checkMode
     s!"{o.emoji prop r.checkLevel r.checkMode} \
        {o.label prop r.checkLevel r.checkMode}{suffix}"
-  | .error e => s!"🚨 {e}"
+  | .error e => s!"🚨 {toString e}"
 
 /-- Deductive-mode success: the assertion's validity is proven (`isPass`).
     Includes unreachable paths (vacuously true). For bug-finding mode,
@@ -668,8 +681,13 @@ def VCResult.isUnknown (vr : VCResult) : Bool :=
 
 def VCResult.isImplementationError (vr : VCResult) : Bool :=
   match vr.outcome with
-  | .error _ => true
-  | .ok _ => false
+  | .error (.encoding _) | .error (.solverCrash _) => true
+  | _ => false
+
+def VCResult.isTimeout (vr : VCResult) : Bool :=
+  match vr.outcome with
+  | .error (.solverTimeout _) => true
+  | _ => false
 
 def VCResult.isNotSuccess (vcResult : Core.VCResult) :=
   !Core.VCResult.isSuccess vcResult
@@ -946,11 +964,18 @@ def getObligationResult (assumptionTerms : List Term) (obligationTerm : Term)
           assumptionTerms obligationTerm ctx satisfiabilityCheck validityCheck
           (label := obligation.label) (varDefinitions := varDefinitions) (varDeclarations := varDeclarations))
   match ans with
-  | .error e =>
-    dbg_trace f!"\n\nObligation {obligation.label}: SMT Solver Invocation Error!\
-                 \n\nError: {e}\
-                 {if options.verbose >= .debug then prog else ""}"
-    .error <| DiagnosticModel.fromFormat e
+  | .error solverError =>
+    let vcError : VCError := match solverError with
+      | .timeout d => .solverTimeout d
+      | .crash d   => .solverCrash d
+    dbg_trace f!"\n\nObligation {obligation.label}: {vcError}\
+                 {if options.verbose >= VerboseMode.debug then prog else ""}"
+    return { obligation := obligation,
+             outcome := Except.error vcError,
+             verbose := options.verbose,
+             checkLevel := options.checkLevel,
+             checkMode := options.checkMode,
+             lexprModel := [] }
   | .ok (satResult, validityResult, estate) =>
     -- Convert unvalidated sat results to unknown when phases require validation
     let (adjSat, satPhaseLog) := satResult.adjustForPhases phases obligation
@@ -1043,7 +1068,7 @@ def verifySingleEnv (oblProgram : Program)
                                     checkLevel := options.checkLevel, checkMode := options.checkMode, lexprModel := [] }
         results := results.push result
         peResolvedCount := peResolvedCount + 1
-        if result.isFailure || result.isImplementationError then
+        if result.isFailure || result.isImplementationError || result.isTimeout then
           if options.verbose >= .debug then
             let prog := f!"\n\n[DEBUG] Evaluated program:\n{Core.formatProgram p}"
             dbg_trace f!"\n\nResult: {result}\n{prog}"
@@ -1058,9 +1083,8 @@ def verifySingleEnv (oblProgram : Program)
     smtEncodeNs := smtEncodeNs + (t3 - t2)
     match maybeTerms with
     | .error err =>
-      let err := f!"SMT Encoding Error! " ++ err
       let result := { obligation,
-                      outcome := .error (toString err),
+                      outcome := .error (.encoding (toString err)),
                       verbose := options.verbose,
                       checkLevel := options.checkLevel,
                       checkMode := options.checkMode,
@@ -1230,7 +1254,11 @@ def toDiagnosticModel (vcr : Core.VCResult)
     (phases : List Core.AbstractedPhase := []) : Option DiagnosticModel :=
   let fileRange := (Imperative.getFileRange vcr.obligation.metadata).getD default
   match vcr.outcome with
-  | .error msg => some { fileRange, message := s!"analysis error: {msg}", type := DiagnosticType.StrataBug }
+  | .error err =>
+    let diagType := match err with
+      | .solverTimeout _ => DiagnosticType.Warning
+      | _ => DiagnosticType.StrataBug
+    some { fileRange, message := s!"analysis error: {err}", type := diagType }
   | .ok outcome =>
     let message? : Option String :=
       if vcr.obligation.property == .cover then

StrataMain.lean

@@ -52,11 +52,12 @@ All `strata` subcommands use a common exit code scheme:
 | 0    | Success            | Analysis passed, inconclusive, or `--no-solve` completed.  |
 | 1    | User error         | Bad input: invalid arguments, malformed source, etc.      |
 | 2    | Failures found     | Analysis completed and found failures.                    |
-| 3    | Internal error     | Tool bug, unexpected solver result, or translation crash. |
+| 3    | Internal error     | SMT encoding failure, solver crash, or translation bug.   |
 | 4    | Known limitation   | Intentionally unsupported language construct.             |
 
 Codes 1–2 are **user-actionable** (fix the input or the code under analysis).
-Codes 3–4 are **tool-side** (report as a bug or wait for support). -/
+Codes 3–4 are **tool-side** (report as a bug or wait for support).
+Exit 0 covers success, inconclusive results, and solver timeouts. -/
 
 namespace ExitCode
   def userError        : UInt8 := 1
@@ -508,10 +509,15 @@ private def exitPyAnalyzeKnownLimitation {α} (message : String) : IO α := do
 /-- Print the final RESULT/DETAIL lines based on solver outcomes.
     Always called on successful pipeline completion (as opposed to the
     exit helpers above, which are called on early pipeline failure).
-    Classification uses successive partitioning: implementation errors are
-    removed first, then the classifier partitions the rest into
+    Classification uses successive partitioning: timeouts and implementation
+    errors are removed first, then the classifier partitions the rest into
     success / failure / inconclusive (guaranteeing disjointness).
-    Unreachable count is reported as supplementary info. -/
+    Unreachable count is reported as supplementary info.
+
+    Exit-code priority (highest wins):
+    - Internal error (exit 3): encoding failures or solver crashes
+    - Failures found (exit 2): assertion violations
+    - Inconclusive / success / solver timeout (exit 0) -/
 private def printPyAnalyzeSummary (vcResults : Array Core.VCResult)
     (checkMode : VerificationMode := .deductive) : IO Unit := do
   let classifier : ResultClassifier :=
@@ -520,27 +526,34 @@ private def printPyAnalyzeSummary (vcResults : Array Core.VCResult)
       { isSuccess := (·.isBugFindingSuccess)
         isFailure := (·.isBugFindingFailure) }
     | _ => {}
-  -- 1. Partition out implementation errors (broken results, not classifiable).
-  let (implError, classifiable) :=
+  -- 1. Partition out implementation errors and timeouts (not classifiable).
+  let (implError, rest1) :=
     vcResults.partition (fun r => r.isImplementationError || r.hasSMTError)
+  let (timeouts, classifiable) := rest1.partition (·.isTimeout)
   -- 2. Successive partitioning via the classifier: success → failure → inconclusive.
   let (success, rest)          := classifiable.partition classifier.isSuccess
   let (failure, inconclusive)  := rest.partition classifier.isFailure
   -- 3. Unreachable is informational (not a separate partition).
   let nUnreachable  := vcResults.filter (·.isUnreachable) |>.size
   let nImplError    := implError.size
+  let nTimeout      := timeouts.size
   let nSuccess      := success.size
   let nFailure      := failure.size
   let nInconclusive := inconclusive.size
   let unreachableStr := if nUnreachable > 0 then s!", {nUnreachable} unreachable" else ""
-  let implErrorStr   := if nImplError > 0   then s!", {nImplError} implementation errors" else ""
-  let counts := s!"{nSuccess} passed, {nFailure} failed, {nInconclusive} inconclusive{unreachableStr}{implErrorStr}"
+  let implErrorStr   := if nImplError > 0   then s!", {nImplError} internal errors" else ""
+  let timeoutStr     := if nTimeout > 0     then s!", {nTimeout} solver timeouts" else ""
+  let counts := s!"{nSuccess} passed, {nFailure} failed, {nInconclusive} inconclusive{unreachableStr}{timeoutStr}{implErrorStr}"
   if nImplError > 0 then
     exitPyAnalyzeInternalError s!"An unexpected result was produced. {counts}"
   else if nFailure > 0 then
     exitPyAnalyzeFailuresFound counts
   else
-    printPyAnalyzeResult (if nInconclusive > 0 then "Inconclusive" else "Analysis success") counts
+    let label :=
+      if nTimeout > 0 then "Solver timeout"
+      else if nInconclusive > 0 then "Inconclusive"
+      else "Analysis success"
+    printPyAnalyzeResult label counts
 
 private def deriveBaseName (file : String) : String :=
   let name := System.FilePath.fileName file |>.getD file
@@ -958,7 +971,7 @@ def laurelAnalyzeCommand : Command where
     | some vcResults =>
       IO.println s!"==== RESULTS ===="
       for vc in vcResults do
-        IO.println s!"{vc.obligation.label}: {match vc.outcome with | .ok o => repr o | .error e => e}"
+        IO.println s!"{vc.obligation.label}: {match vc.outcome with | .ok o => repr o | .error e => toString e}"
 
 def laurelAnalyzeToGotoCommand : Command where
   name := "laurelAnalyzeToGoto"
@@ -1307,8 +1320,15 @@ def verifyCommand : Command where
       else
         let provedGoalCount := (vcResults.filter Core.VCResult.isSuccess).size
         let failedGoalCount := (vcResults.filter Core.VCResult.isNotSuccess).size
+        -- Encoding failures, solver crashes, or per-check SMT errors (exit 3)
+        let hasImplError := vcResults.any (fun r => r.isImplementationError || r.hasSMTError)
+        -- Assertion violations that are not timeouts or internal errors (exit 2)
+        let hasFailure := vcResults.any (fun r => !r.isSuccess && !r.isTimeout && !r.isImplementationError && !r.hasSMTError)
         println! f!"Finished with {provedGoalCount} goals passed, {failedGoalCount} failed."
-        IO.Process.exit ExitCode.failuresFound
+        if hasImplError then
+          IO.Process.exit ExitCode.internalError
+        else if hasFailure then
+          IO.Process.exit ExitCode.failuresFound
 
 def pyInterpretCommand : Command where
   name := "pyInterpret"

StrataTest/Languages/Core/Examples/Regex.lean

@@ -182,14 +182,14 @@ str.in.re("a", bad_re_loop(1))
 info:
 Obligation: assert_0
 Property: assert
-Result: 🚨 Implementation Error! SMT Encoding Error! Natural numbers expected as indices for re.loop.
+Result: 🚨 SMT Encoding Error! Natural numbers expected as indices for re.loop.
 Original expression: re.loop(re.range("a", "z"), 1, bvar!0)
 -- Errors: Unsupported construct in lexprToExpr: bvar index out of bounds: 0
 Context: Global scope:
 
 Obligation: assert_1
 Property: assert
-Result: 🚨 Implementation Error! SMT Encoding Error! Natural numbers expected as indices for re.loop.
+Result: 🚨 SMT Encoding Error! Natural numbers expected as indices for re.loop.
 Original expression: re.loop(re.range("a", "z"), 1, bvar!0)
 -- Errors: Unsupported construct in lexprToExpr: bvar index out of bounds: 0
 Context: Global scope:

StrataTest/Languages/Core/Tests/LambdaHigherOrderTests.lean

@@ -139,7 +139,7 @@ spec {
 info:
 Obligation: TestLambdaApply_ensures_0
 Property: assert
-Result: 🚨 Implementation Error! SMT Encoding Error! Cannot encode function 'apply' to SMT: it has function-typed parameter(s) [f]. Higher-order functions cannot be encoded to SMT. Consider marking the function as `inline`.
+Result: 🚨 SMT Encoding Error! Cannot encode function 'apply' to SMT: it has function-typed parameter(s) [f]. Higher-order functions cannot be encoded to SMT. Consider marking the function as `inline`.
 -/
 #guard_msgs in
 #eval verify lambdaApplyNoInlinePgm (options := .quiet)
@@ -167,7 +167,7 @@ spec {
 /-- info:
 Obligation: Test_ensures_0
 Property: assert
-Result: 🚨 Implementation Error! SMT Encoding Error! Cannot encode function 'mkFn' to SMT: its body contains a lambda expression. Lambda abstractions cannot be encoded to SMT. Consider marking the function as `inline`.-/
+Result: 🚨 SMT Encoding Error! Cannot encode function 'mkFn' to SMT: its body contains a lambda expression. Lambda abstractions cannot be encoded to SMT. Consider marking the function as `inline`.-/
 #guard_msgs in
 #eval verify lambdaInBodyPgm (options := .quiet)
 
@@ -253,7 +253,7 @@ spec {
 
 /-- info: Obligation: Test_ensures_0
 Property: assert
-Result: 🚨 Implementation Error! SMT Encoding Error! Cannot encode lambda expression to SMT. Lambda abstractions must be eliminated (e.g., by beta-reduction) before SMT encoding.
+Result: 🚨 SMT Encoding Error! Cannot encode lambda expression to SMT. Lambda abstractions must be eliminated (e.g., by beta-reduction) before SMT encoding.
 Lambda: fun x : int => x + 1-/
 #guard_msgs in
 #eval verify lambdaInAssertPgm (options := .quiet)