From 5c65b06ea668af750eb84e4cfec5f69a0d258fb9 Mon Sep 17 00:00:00 2001
From: PJ <ipriyanshujain@gmail.com>
Date: Wed, 12 Aug 2026 16:46:26 +0530
Subject: [PATCH] fix(ltl): reduce a thrown-predicate residual instead of
 panicking

The verifier substitutes an ErrorFormula for the residual of a property whose
predicate threw, and that residual is fed back in on the next step. reduce had
no case for it, so the run crashed. It re-reports the same failure now.

Claude-Session: https://claude.ai/code/session_01Fj4wJUikdABuMQEETwW55J
---
 internal/ltl/evaluator.go     |  6 ++++++
 internal/ltl/finalize_test.go | 20 ++++++++++++++++++++
 2 files changed, 26 insertions(+)

diff --git a/internal/ltl/evaluator.go b/internal/ltl/evaluator.go
index f0b6c2b..2d07194 100644
--- a/internal/ltl/evaluator.go
+++ b/internal/ltl/evaluator.go
@@ -336,6 +336,12 @@ func reduce(formula Formula, now time.Time) reduceResult {
 		}
 		return violatedWith(concrete, "pure false")
 
+	case ErrorFormula:
+		// A thrown predicate substituted into a residual at the trace
+		// boundary. Reducing it re-reports the same failure rather than
+		// crashing the run.
+		return violatedByError(concrete, concrete.Message)
+
 	case ThunkFormula:
 		result, err := concrete.predicate()
 		if err != nil {
diff --git a/internal/ltl/finalize_test.go b/internal/ltl/finalize_test.go
index 54a6953..4ae5456 100644
--- a/internal/ltl/finalize_test.go
+++ b/internal/ltl/finalize_test.go
@@ -262,3 +262,23 @@ func TestCollapse_UnnamedPredicatesDoNotMerge(t *testing.T) {
 		t.Errorf("origin = %d, want 2", witness.Step)
 	}
 }
+
+// TestReduce_ErrorFormulaViolates: the verifier substitutes an ErrorFormula for
+// the residual of a property whose predicate threw, and that residual is fed
+// back into the evaluator on the next step. Reducing one used to panic.
+func TestReduce_ErrorFormulaViolates(t *testing.T) {
+	evaluator := NewEvaluator(Always(ErrorFormula{Message: "boom"}))
+	if got := evaluator.Observe(); got != VerdictViolated {
+		t.Fatalf("got %v, want violated", got)
+	}
+	witness := evaluator.Violation()
+	if witness == nil {
+		t.Fatal("Violation = nil, want non-nil")
+	}
+	if witness.Reason != "boom" {
+		t.Errorf("Reason = %q, want %q", witness.Reason, "boom")
+	}
+	if !witness.IsError {
+		t.Error("IsError = false, want true")
+	}
+}