diff --git a/Strata/DL/Imperative/CmdEval.lean b/Strata/DL/Imperative/CmdEval.lean
index 7c90771cc..29b255a5e 100644
--- a/Strata/DL/Imperative/CmdEval.lean
+++ b/Strata/DL/Imperative/CmdEval.lean
@@ -18,7 +18,7 @@ public section
 /--
 Partial evaluator for an Imperative Command.
 -/
-def Cmd.eval [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P × S :=
+def Cmd.eval [BEq P.Ident] [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P × S :=
   match EC.lookupError σ with
   | some _ => (c, σ)
   | none =>
@@ -65,16 +65,19 @@ def Cmd.eval [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P × S :=
       let e := EC.eval σ e
       let assumptions := EC.getPathConditions σ
       let c' := .assert label e md
+      let propType := match md.getPropertyType with
+        | some s => if s == MetaData.divisionByZero then .divisionByZero else .assert
+        | none => .assert
       match EC.denoteBool e with
       | some true => -- Proved via evaluation.
-        (c', EC.deferObligation σ (ProofObligation.mk label .assert assumptions e md))
+        (c', EC.deferObligation σ (ProofObligation.mk label propType assumptions e md))
       | some false =>
         if assumptions.isEmpty then
           (c', EC.updateError σ (.AssertFail label e))
         else
-          (c', EC.deferObligation σ (ProofObligation.mk label .assert assumptions e md))
+          (c', EC.deferObligation σ (ProofObligation.mk label propType assumptions e md))
       | none =>
-        (c', EC.deferObligation σ (ProofObligation.mk label .assert assumptions e md))
+        (c', EC.deferObligation σ (ProofObligation.mk label propType assumptions e md))
 
     | .assume label e md =>
       let (e, σ) := EC.preprocess σ c e
@@ -99,7 +102,7 @@ def Cmd.eval [EC : EvalContext P S] (σ : S) (c : Cmd P) : Cmd P × S :=
 /--
 Partial evaluator for Imperative's Commands.
 -/
-def Cmds.eval [EvalContext P S] (σ : S) (cs : Cmds P) : Cmds P × S :=
+def Cmds.eval [BEq P.Ident] [EvalContext P S] (σ : S) (cs : Cmds P) : Cmds P × S :=
   match cs with
   | [] => ([], σ)
   | c :: crest =>
diff --git a/Strata/DL/Imperative/EvalContext.lean b/Strata/DL/Imperative/EvalContext.lean
index a58215d35..b4fa102c5 100644
--- a/Strata/DL/Imperative/EvalContext.lean
+++ b/Strata/DL/Imperative/EvalContext.lean
@@ -72,12 +72,14 @@ def PathConditions.removeByNames (ps : PathConditions P) (names : List String) :
 inductive PropertyType where
   | cover
   | assert
+  | divisionByZero
   deriving Repr, DecidableEq
 
 instance : ToFormat PropertyType where
   format p := match p with
     | .cover => "cover"
     | .assert => "assert"
+    | .divisionByZero => "division by zero check"
 
 /--
 A proof obligation can be discharged by some backend solver or a dedicated
diff --git a/Strata/DL/Imperative/MetaData.lean b/Strata/DL/Imperative/MetaData.lean
index 1e58807e0..810edb74c 100644
--- a/Strata/DL/Imperative/MetaData.lean
+++ b/Strata/DL/Imperative/MetaData.lean
@@ -214,6 +214,20 @@ def MetaData.formatFileRangeD {P : PureExpr} [BEq P.Ident] (md : MetaData P) (fi
   | some fr => fr.format fileMap includeEnd?
   | none => f!""
 
+/-- Metadata field for property type classification (e.g., "divisionByZero"). -/
+def MetaData.propertyType : MetaDataElem.Field P := .label "propertyType"
+
+/-- Metadata value for division-by-zero property type classification. -/
+def MetaData.divisionByZero : String := "divisionByZero"
+
+/-- Read the property type classification from metadata, if present. -/
+def MetaData.getPropertyType {P : PureExpr} [BEq P.Ident] (md : MetaData P) : Option String :=
+  match md.findElem MetaData.propertyType with
+  | some elem => match elem.value with
+    | .msg s => some s
+    | _ => none
+  | none => none
+
 ---------------------------------------------------------------------
 
 end -- public section
diff --git a/Strata/Languages/Core/SarifOutput.lean b/Strata/Languages/Core/SarifOutput.lean
index 94f38d5e2..3104ec8d7 100644
--- a/Strata/Languages/Core/SarifOutput.lean
+++ b/Strata/Languages/Core/SarifOutput.lean
@@ -50,9 +50,16 @@ def extractLocation (files : Map Strata.Uri Lean.FileMap) (md : Imperative.MetaD
     pure { uri, startLine := startPos.line, startColumn := startPos.column }
   | _ => none
 
+/-- Convert PropertyType to a property classification string for SARIF output -/
+def propertyTypeToClassification : Imperative.PropertyType → String
+  | .divisionByZero => "division-by-zero"
+  | .cover => "cover"
+  | .assert => "assert"
+
 /-- Convert a VCResult to a SARIF Result -/
 def vcResultToSarifResult (files : Map Strata.Uri Lean.FileMap) (vcr : VCResult) : Strata.Sarif.Result :=
   let ruleId := vcr.obligation.label
+  let classification := propertyTypeToClassification vcr.obligation.property
   let level := outcomeToLevel vcr.result
   let messageText :=
     if vcr.isUnreachable then "Path is unreachable"
@@ -63,7 +70,7 @@ def vcResultToSarifResult (files : Map Strata.Uri Lean.FileMap) (vcr : VCResult)
     | some loc => #[locationToSarif loc]
     | none => #[]
 
-  { ruleId, level, message, locations }
+  { ruleId, level, message, locations, properties := { propertyType := classification } }
 
 /-- Convert VCResults to a SARIF document -/
 def vcResultsToSarif (files : Map Strata.Uri Lean.FileMap) (vcResults : VCResults) : Strata.Sarif.SarifDocument :=
diff --git a/Strata/Languages/Core/StatementEval.lean b/Strata/Languages/Core/StatementEval.lean
index 47cd4c53a..68bc7dfbd 100644
--- a/Strata/Languages/Core/StatementEval.lean
+++ b/Strata/Languages/Core/StatementEval.lean
@@ -341,7 +341,10 @@ private def createUnreachableAssertObligations
     Imperative.ProofObligations Expression :=
   asserts.toArray.map
     (fun (label, md) =>
-      (Imperative.ProofObligation.mk label .assert pathConditions (LExpr.true ()) md))
+      let propType := match md.getPropertyType with
+        | some s => if s == Imperative.MetaData.divisionByZero then .divisionByZero else .assert
+        | _ => .assert
+      (Imperative.ProofObligation.mk label propType pathConditions (LExpr.true ()) md))
 
 /--
 Substitute free variables in an expression with their current values from the environment,
diff --git a/Strata/Languages/Core/Verifier.lean b/Strata/Languages/Core/Verifier.lean
index 9b0c7efae..d7ca523d6 100644
--- a/Strata/Languages/Core/Verifier.lean
+++ b/Strata/Languages/Core/Verifier.lean
@@ -270,7 +270,7 @@ def preprocessObligation (obligation : ProofObligation Expression) (p : Program)
       return (obligation, some result)
     else
       return (obligation, none)
-  | .assert =>
+  | .assert | .divisionByZero =>
     if obligation.obligation.isTrue && !needsReachCheck then
       -- We don't need the SMT solver if PE (partial evaluation) is enough to
       -- reduce the consequent to true. Skip the shortcut when reachCheck is
diff --git a/Strata/Transform/PrecondElim.lean b/Strata/Transform/PrecondElim.lean
index f67c89c22..0a3520166 100644
--- a/Strata/Transform/PrecondElim.lean
+++ b/Strata/Transform/PrecondElim.lean
@@ -45,18 +45,29 @@ def wfProcName (name : String) : String := s!"{name}{wfSuffix}"
 
 /-! ## Collecting assertions from expressions -/
 
+/-- Classify a function name into a property type for SARIF reporting. -/
+private def classifyPrecondition (funcName : String) : Option String :=
+  if funcName.startsWith "Int.SafeDiv" || funcName.startsWith "Int.SafeMod" then
+    some Imperative.MetaData.divisionByZero
+  else
+    none
+
 /--
 Given a Factory and an expression, collect all partial function call
 precondition obligations and return them as `assert` statements.
-The metadata from the original statement is attached to the generated assertions.
+The metadata from the original statement is attached to the generated assertions,
+with property type classification added when applicable.
 -/
 def collectPrecondAsserts (F : @Lambda.Factory CoreLParams) (e : Expression.Expr)
 (labelPrefix : String) (md : Imperative.MetaData Expression := .empty)
 : List Statement :=
   let wfObs := Lambda.collectWFObligations F e
   wfObs.mapIdx fun idx ob =>
+    let md' := match classifyPrecondition ob.funcName with
+      | some pt => md.pushElem Imperative.MetaData.propertyType (.msg pt)
+      | none => md
     Statement.assert
-    s!"{labelPrefix}_calls_{ob.funcName}_{idx}" ob.obligation md
+    s!"{labelPrefix}_calls_{ob.funcName}_{idx}" ob.obligation md'
 
 /--
 Collect assertions for all expressions in a command.
diff --git a/Strata/Util/Sarif.lean b/Strata/Util/Sarif.lean
index 20809fb54..54271f1cc 100644
--- a/Strata/Util/Sarif.lean
+++ b/Strata/Util/Sarif.lean
@@ -83,6 +83,12 @@ instance : FromJson Level where
     | "error" => pure .error
     | _ => throw s!"Invalid SARIF level: {s}"
 
+/-- SARIF property bag for tool-specific properties -/
+structure PropertyBag where
+  /-- Strata-specific classification of the property being checked -/
+  propertyType : String := "assert"
+  deriving Repr, ToJson, FromJson, DecidableEq
+
 /-- SARIF result representing a single verification result -/
 structure Result where
   /-- Stable identifier of the rule that was evaluated to produce the result --/
@@ -90,6 +96,8 @@ structure Result where
   level : Level
   message : Message
   locations : Array SarifLocation := #[]
+  /-- Tool-specific properties (SARIF property bag) -/
+  properties : PropertyBag := {}
   deriving Repr, ToJson, FromJson, DecidableEq
 
 instance : Inhabited Result where
diff --git a/StrataTest/Languages/Core/Examples/FunctionPreconditions.lean b/StrataTest/Languages/Core/Examples/FunctionPreconditions.lean
index 60e2d935c..3dda12717 100644
--- a/StrataTest/Languages/Core/Examples/FunctionPreconditions.lean
+++ b/StrataTest/Languages/Core/Examples/FunctionPreconditions.lean
@@ -27,7 +27,7 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: safeDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 precond_safeDiv_0: !($__y1 == 0)
 Obligation:
@@ -35,7 +35,7 @@ Obligation:
 
 ---
 info: Obligation: safeDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 -/
 #guard_msgs in
@@ -159,14 +159,14 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: foo_precond_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 precond_foo_0: $__y1 > 0
 Obligation:
 !($__y1 == 0)
 
 Label: foo_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 precond_foo_0: $__y1 > 0
 precond_foo_1: $__x0 / $__y1 > 0
@@ -175,11 +175,11 @@ Obligation:
 
 ---
 info: Obligation: foo_precond_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 
 Obligation: foo_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 -/
 #guard_msgs in
@@ -205,7 +205,7 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: doubleDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 precond_doubleDiv_0: !($__y1 == 0)
 precond_doubleDiv_1: !($__z2 == 0)
@@ -213,7 +213,7 @@ Obligation:
 !($__z2 == 0)
 
 Label: doubleDiv_body_calls_Int.SafeDiv_1
-Property: assert
+Property: division by zero check
 Assumptions:
 precond_doubleDiv_0: !($__y1 == 0)
 precond_doubleDiv_1: !($__z2 == 0)
@@ -223,11 +223,11 @@ Obligation:
 ---
 info:
 Obligation: doubleDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 
 Obligation: doubleDiv_body_calls_Int.SafeDiv_1
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 -/
 #guard_msgs in
@@ -250,14 +250,14 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: badDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Obligation:
 false
 
 
 
 Result: Obligation: badDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ❌ fail
 
 
@@ -273,7 +273,7 @@ function badDiv (x : int) : int {
 ---
 info:
 Obligation: badDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ❌ fail
 -/
 #guard_msgs in
@@ -297,13 +297,13 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: init_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Obligation:
 true
 
 ---
 info: Obligation: init_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 -/
 #guard_msgs in
@@ -331,7 +331,7 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: set_z_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 <label_ite_cond_true: (~Int.Gt a #0)>: $__a0 > 0
 Obligation:
@@ -339,7 +339,7 @@ Obligation:
 
 ---
 info: Obligation: set_z_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 -/
 #guard_msgs in
@@ -368,7 +368,7 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: safeDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 precond_safeDiv_0: !($__y1 == 0)
 Obligation:
@@ -383,7 +383,7 @@ Obligation:
 
 ---
 info: Obligation: safeDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 
 Obligation: init_calls_safeDiv_0
@@ -416,7 +416,7 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: safeDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 precond_safeDiv_0: !($__y1 == 0)
 Obligation:
@@ -431,7 +431,7 @@ forall __q0 : int :: __q0 > 0 ==> !(__q0 == 0)
 
 ---
 info: Obligation: safeDiv_body_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 
 Obligation: allPositiveDiv_body_calls_safeDiv_0
@@ -512,7 +512,7 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: loop_guard_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 test_requires_0: !($__n0 == 0)
 Obligation:
@@ -539,7 +539,7 @@ $__i1 + 1 >= 0
 ---
 info:
 Obligation: loop_guard_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 
 Obligation: entry_invariant_0_0
diff --git a/StrataTest/Languages/Core/Examples/Loops.lean b/StrataTest/Languages/Core/Examples/Loops.lean
index ab11b0d6c..7893e1307 100644
--- a/StrataTest/Languages/Core/Examples/Loops.lean
+++ b/StrataTest/Languages/Core/Examples/Loops.lean
@@ -39,14 +39,14 @@ info: [Strata.Core] Type checking succeeded.
 
 VCs:
 Label: sum_post_sum_ensures_1_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 sum_requires_0: $__n0 >= 0
 Obligation:
 true
 
 Label: loop_invariant_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Assumptions:
 sum_requires_0: $__n2 >= 0
 Obligation:
@@ -132,11 +132,11 @@ if 0 < $__n2 then $__s8 else 0 == $__n2 * ($__n2 + 1) / 2
 ---
 info:
 Obligation: sum_post_sum_ensures_1_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 
 Obligation: loop_invariant_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 
 Obligation: entry_invariant_0_0
diff --git a/StrataTest/Languages/Core/Examples/NoFilterWFProc.lean b/StrataTest/Languages/Core/Examples/NoFilterWFProc.lean
index c3f14289a..765c6bacc 100644
--- a/StrataTest/Languages/Core/Examples/NoFilterWFProc.lean
+++ b/StrataTest/Languages/Core/Examples/NoFilterWFProc.lean
@@ -33,11 +33,11 @@ spec {
 /--
 info:
 Obligation: P_post_result_ok_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 
 Obligation: set_r_calls_Int.SafeDiv_0
-Property: assert
+Property: division by zero check
 Result: ✅ pass
 
 Obligation: result_ok
diff --git a/StrataTest/Languages/Core/Tests/SarifOutputTests.lean b/StrataTest/Languages/Core/Tests/SarifOutputTests.lean
index b5eb1b5eb..4f8a4d6bf 100644
--- a/StrataTest/Languages/Core/Tests/SarifOutputTests.lean
+++ b/StrataTest/Languages/Core/Tests/SarifOutputTests.lean
@@ -272,7 +272,7 @@ def makeVCResult (label : String) (outcome : Outcome)
   let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
-/-- info: "{\"runs\":[{\"results\":[{\"level\":\"none\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/pass.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification succeeded\"},\"ruleId\":\"test_pass\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
+/-- info: "{\"runs\":[{\"results\":[{\"level\":\"none\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/pass.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification succeeded\"},\"properties\":{\"propertyType\":\"assert\"},\"ruleId\":\"test_pass\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
   let md := makeMetadata "/test/pass.st" 10 5
@@ -281,7 +281,7 @@ def makeVCResult (label : String) (outcome : Outcome)
   let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
-/-- info: "{\"runs\":[{\"results\":[{\"level\":\"error\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/fail.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification failed\"},\"ruleId\":\"test_fail\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
+/-- info: "{\"runs\":[{\"results\":[{\"level\":\"error\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/fail.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification failed\"},\"properties\":{\"propertyType\":\"assert\"},\"ruleId\":\"test_fail\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
   let md := makeMetadata "/test/fail.st" 20 15
@@ -290,7 +290,7 @@ def makeVCResult (label : String) (outcome : Outcome)
   let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
-/-- info: "{\"runs\":[{\"results\":[{\"level\":\"warning\",\"locations\":[],\"message\":{\"text\":\"Verification result unknown (solver timeout or incomplete)\"},\"ruleId\":\"test_unknown\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
+/-- info: "{\"runs\":[{\"results\":[{\"level\":\"warning\",\"locations\":[],\"message\":{\"text\":\"Verification result unknown (solver timeout or incomplete)\"},\"properties\":{\"propertyType\":\"assert\"},\"ruleId\":\"test_unknown\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
   let files := makeFilesMap "/test/file.st"
@@ -298,7 +298,7 @@ def makeVCResult (label : String) (outcome : Outcome)
   let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
-/-- info: "{\"runs\":[{\"results\":[{\"level\":\"error\",\"locations\":[],\"message\":{\"text\":\"Verification error: timeout\"},\"ruleId\":\"test_error\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
+/-- info: "{\"runs\":[{\"results\":[{\"level\":\"error\",\"locations\":[],\"message\":{\"text\":\"Verification error: timeout\"},\"properties\":{\"propertyType\":\"assert\"},\"ruleId\":\"test_error\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
   let files := makeFilesMap "/test/file.st"
@@ -306,7 +306,7 @@ def makeVCResult (label : String) (outcome : Outcome)
   let sarif := vcResultsToSarif files vcResults
   Strata.Sarif.toJsonString sarif
 
-/-- info: "{\"runs\":[{\"results\":[{\"level\":\"none\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/multi.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification succeeded\"},\"ruleId\":\"obligation1\"},{\"level\":\"error\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/multi.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification failed\"},\"ruleId\":\"obligation2\"},{\"level\":\"warning\",\"locations\":[],\"message\":{\"text\":\"Verification result unknown (solver timeout or incomplete)\"},\"ruleId\":\"obligation3\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
+/-- info: "{\"runs\":[{\"results\":[{\"level\":\"none\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/multi.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification succeeded\"},\"properties\":{\"propertyType\":\"assert\"},\"ruleId\":\"obligation1\"},{\"level\":\"error\",\"locations\":[{\"physicalLocation\":{\"artifactLocation\":{\"uri\":\"/test/multi.st\"},\"region\":{\"startColumn\":0,\"startLine\":1}}}],\"message\":{\"text\":\"Verification failed\"},\"properties\":{\"propertyType\":\"assert\"},\"ruleId\":\"obligation2\"},{\"level\":\"warning\",\"locations\":[],\"message\":{\"text\":\"Verification result unknown (solver timeout or incomplete)\"},\"properties\":{\"propertyType\":\"assert\"},\"ruleId\":\"obligation3\"}],\"tool\":{\"driver\":{\"informationUri\":\"https://github.com/strata-org/Strata\",\"name\":\"Strata\",\"version\":\"0.1.0\"}}}],\"schema\":\"https://raw.githubusercontent.com/oasis-tcs/sarif-spec/master/Schemata/sarif-schema-2.1.0.json\",\"version\":\"2.1.0\"}" -/
 #guard_msgs in
 #eval
   let md1 := makeMetadata "/test/multi.st" 5 1