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

@@ -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 {

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")
+	}
+}