diff --git a/client/src/types/diagnostics.ts b/client/src/types/diagnostics.ts
index 36ab1c4..84172e0 100644
--- a/client/src/types/diagnostics.ts
+++ b/client/src/types/diagnostics.ts
@@ -27,6 +27,9 @@ export type LJWarning = CustomWarning | ExternalClassNotFoundWarning | ExternalM
 export type LJHintKind = 'general' | 'deciding-argument' | 'call-sequence' | 'available-calls' | 'unreachable-state'
     | 'path-dependent-state' | 'final-state' | 'reaching-calls';
 
+// the kind of mistake an error shows, as the verifier names it, e.g. 'unknown' when nothing known could prove what was expected
+export type LJErrorCategory = 'out-of-order' | 'out-of-domain' | 'argument-picks-the-state' | 'path-dependent-state' | 'unknown';
+
 export type LJHint = {
     kind: LJHintKind;
     message: string;
@@ -68,6 +71,8 @@ export type RefinementError = BaseDiagnostic & {
     category: 'error';
     type: 'refinement-error';
     translationTable: TranslationTable;
+    // absent when the verifier gives none, as lsp4j leaves out null fields
+    errorCategory?: LJErrorCategory;
     expected: string;
     found: VCSimplificationResult;
     customMessage: string;
@@ -95,6 +100,8 @@ export type StateRefinementError = BaseDiagnostic & {
     category: 'error';
     type: 'state-refinement-error';
     translationTable: TranslationTable;
+    // absent when the verifier gives none, as lsp4j leaves out null fields
+    errorCategory?: LJErrorCategory;
     expected: string;
     found: VCSimplificationResult;
     customMessage: string;
diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts
index e682ed1..74c5748 100644
--- a/client/src/webview/styles.ts
+++ b/client/src/webview/styles.ts
@@ -569,6 +569,23 @@ export function getStyles(): string {
         .vc-binder {
             color: var(--vscode-descriptionForeground);
         }
+        .vc-nothing-known {
+            margin: 0;
+            padding: 0.0625rem 0.25rem;
+            color: var(--vscode-descriptionForeground);
+            font-family: var(--vscode-font-family);
+        }
+        .vc-step-title {
+            display: inline-flex;
+            align-items: center;
+            gap: 0.25rem;
+            min-width: 0;
+        }
+        .vc-step-info {
+            display: inline-flex;
+            color: var(--vscode-descriptionForeground);
+            cursor: help;
+        }
         .vc-step-controls {
             display: inline-flex;
             align-items: center;
diff --git a/client/src/webview/views/diagnostics/vc-changes.spec.ts b/client/src/webview/views/diagnostics/vc-changes.spec.ts
index 06527fb..ece89c8 100644
--- a/client/src/webview/views/diagnostics/vc-changes.spec.ts
+++ b/client/src/webview/views/diagnostics/vc-changes.spec.ts
@@ -37,4 +37,16 @@ describe('verification implications', () => {
         expect(document.querySelector('.vc-predicate-cell')?.textContent?.trim()).toBe('x == 1');
         expect(document.querySelector('.vc-arrow')).toBeNull();
     });
+    it('puts each conjunct outside parentheses and strings on its own line', () => {
+        document.body.innerHTML = renderImplication({ ...conclusion, predicate: 'a > 0 && (b || c && d) && s == "x&&y"' });
+
+        expect(Array.from(document.querySelectorAll('.vc-predicate-cell'), cell => cell.textContent?.trim()))
+            .toEqual(['a > 0 &&', '(b || c && d) &&', 's == "x&&y"']);
+    });
+
+    it.each(['a || b && c', 'a && b --> c', 'a && b ? c : d'])('keeps %s on one line', predicate => {
+        document.body.innerHTML = renderImplication({ ...conclusion, predicate });
+
+        expect(document.querySelectorAll('.vc-predicate-cell')).toHaveLength(1);
+    });
 });
diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts
index a5c0d37..d5a97ec 100644
--- a/client/src/webview/views/diagnostics/vc-changes.ts
+++ b/client/src/webview/views/diagnostics/vc-changes.ts
@@ -11,27 +11,65 @@ const MIN_LINE_SIMILARITY = 0.3;
 const TOKEN_PATTERN = /\s+|-->|&&|\|\||==|!=|<=|>=|[a-zA-Z_#][a-zA-Z0-9_#⁰¹²³⁴⁵⁶⁷⁸⁹]*|\d+(?:\.\d+)?|[^\s]/gu;
 const WHITESPACE_PATTERN = /^\s+$/u;
 const VC_LINE_SEPARATOR = "\t";
+const WEAKER_THAN_AND = ["||", "-->", "?"];
 
 function hasBinder(node: VCImplication): boolean {
     return typeof node.name === "string" && node.name.length > 0;
 }
 
-function formatImplicationLine(node: VCImplication): string {
+// one line per conjunct of a node's predicate; the lines after the first keep its binder to tell nodes apart, but do not show it
+function formatImplicationLines(node: VCImplication): string[] {
     const binder = hasBinder(node) ? `∀${node.name}` : "";
     const type = typeof node.type === "string" ? node.type : "";
-    return [binder, type, node.predicate, node.next ? "next" : ""].join(VC_LINE_SEPARATOR);
+    const conjuncts = splitConjuncts(node.predicate);
+    return conjuncts.map((conjunct, index) => {
+        const isLast = index === conjuncts.length - 1;
+        const predicate = isLast ? conjunct : `${conjunct} &&`;
+        return [binder, type, predicate, isLast && node.next ? "next" : "", index > 0 ? "continued" : ""]
+            .join(VC_LINE_SEPARATOR);
+    });
+}
+
+function parseImplicationLine(line: string): {
+    binder: string; type: string; predicate: string; hasNext: boolean; isContinued: boolean;
+} {
+    const [binder = "", type = "", predicate = "", next = "", continued = ""] = line.split(VC_LINE_SEPARATOR);
+    return { binder, type, predicate, hasNext: next === "next", isContinued: continued === "continued" };
 }
 
-function parseImplicationLine(line: string): { binder: string; type: string; predicate: string; hasNext: boolean } {
-    const [binder = "", type = "", predicate = "", next = ""] = line.split(VC_LINE_SEPARATOR);
-    return { binder, type, predicate, hasNext: next === "next" };
+// splits a predicate on the && outside parentheses and string literals, unless a weaker operator outside them
+// (||, -->, ?:) would make its parts look like conjuncts of the whole predicate
+function splitConjuncts(predicate: string): string[] {
+    const conjuncts: string[] = [];
+    let depth = 0;
+    let start = 0;
+    let inString = false;
+    for (let i = 0; i < predicate.length; i++) {
+        if (inString) {
+            if (predicate[i] === "\\") i++;
+            else if (predicate[i] === '"') inString = false;
+        }
+        else if (predicate[i] === '"') inString = true;
+        else if (predicate[i] === "(") depth++;
+        else if (predicate[i] === ")") depth--;
+        else if (depth > 0) continue;
+        else if (WEAKER_THAN_AND.some(operator => predicate.startsWith(operator, i))) return [predicate];
+        else if (predicate.startsWith("&&", i)) {
+            conjuncts.push(predicate.slice(start, i).trim());
+            start = i + 2;
+        }
+    }
+    return [...conjuncts, predicate.slice(start).trim()];
 }
 
-function getImplicationLines(node: VCImplication): string[] {
+/**
+ * The lines of a VC chain: one per conjunct of each node with a binder, and of the conclusion
+ */
+export function getImplicationLines(node: VCImplication): string[] {
     const lines: string[] = [];
     for (let current: VCImplication | null = node; current; current = current.next) {
         if (current.next && !hasBinder(current)) continue;
-        lines.push(formatImplicationLine(current));
+        lines.push(...formatImplicationLines(current));
     }
     return lines;
 }
@@ -55,10 +93,11 @@ export function renderVCLine(
     predicateContent?: string,
     translationTable?: TranslationTable,
 ): string {
-    const { binder, type, predicate, hasNext } = parseImplicationLine(line);
+    const { binder, type, predicate, hasNext, isContinued } = parseImplicationLine(line);
+    const binderCell = isContinued ? "" : renderBinder(binder, type, translationTable);
     return /*html*/`
         <div class="vc-line ${className}">
-            ${binder ? /*html*/`<div class="vc-binder-cell">${renderBinder(binder, type, translationTable)}</div>` : ""}
+            ${binder ? /*html*/`<div class="vc-binder-cell">${binderCell}</div>` : ""}
             <div class="vc-predicate-cell"><span class="vc-node">${predicateContent ?? renderHighlightedInlineExpression(predicate)}</span>${hasNext ? ' <span class="vc-arrow">→</span>' : ""}</div>
         </div>
     `;
diff --git a/client/src/webview/views/diagnostics/vc-implications.spec.ts b/client/src/webview/views/diagnostics/vc-implications.spec.ts
new file mode 100644
index 0000000..2f25914
--- /dev/null
+++ b/client/src/webview/views/diagnostics/vc-implications.spec.ts
@@ -0,0 +1,96 @@
+import { afterEach, describe, expect, it } from 'vitest';
+import type { LJErrorCategory, RefinementError } from '../../../types/diagnostics';
+import type { VCImplication, VCSimplificationResult } from '../../../types/vc-implications';
+import { handleVCImplicationStepClick, renderVCImplication } from './vc-implications';
+
+// a VC chain from its rows, each a binder and its predicate
+function chain(...rows: ReadonlyArray<readonly [string, string]>): VCImplication {
+    return rows.reduceRight<VCImplication | null>(
+        (next, [name, predicate]) => ({ name, type: 'int', predicate, next }), null,
+    ) as VCImplication;
+}
+
+// a derivation from its steps, oldest first, each the pass that produced it and its chain
+function derivation(...steps: Array<[string | null, VCImplication]>): VCSimplificationResult {
+    return steps.reduce<VCSimplificationResult | null>(
+        (origin, [simplification, implication]) => ({ implication, origin, simplification }), null,
+    ) as VCSimplificationResult;
+}
+
+function render(found: VCSimplificationResult, message = 'found ... but expected ...', errorCategory?: LJErrorCategory): void {
+    const error = {
+        file: 'A.java', position: null, title: 'Refinement Error', message, errorCategory,
+    } as unknown as RefinementError;
+    document.body.innerHTML = renderVCImplication(error, found);
+}
+
+function shown() {
+    return {
+        label: document.querySelector('.vc-step-name')?.textContent,
+        info: document.querySelector('.vc-step-info')?.getAttribute('title'),
+        position: document.querySelector('.vc-step-position')?.textContent?.trim(),
+        lines: Array.from(document.querySelectorAll('.vc-line')).map(line => line.textContent?.replace(/\s+/gu, ' ').trim()),
+    };
+}
+
+function previous(): void {
+    handleVCImplicationStepClick(document.querySelector('.vc-step-previous-btn')!);
+}
+
+afterEach(() => { document.body.innerHTML = ''; });
+
+describe('Found', () => {
+    it('keeps the binders and implications, with a line per conjunct', () => {
+        const size = 'failures.size() == size(this.failures) && failures.size() >= 0';
+        render(derivation(
+            [null, chain(['this.failures', 'true'], ['failures', 'failures == this.failures'],
+                ['failures.size()', 'failures.size() == size(failures) && failures.size() >= 0'])],
+            ['Substitution', chain(['this.failures', 'true'], ['failures.size()', size])],
+        ));
+
+        expect(shown()).toEqual({
+            label: 'Simplified', info: 'Replaced variables with the values they are equal to.', position: '2/2',
+            lines: ['∀this.failures true →', '∀failures.size() failures.size() == size(this.failures) &&', 'failures.size() >= 0'],
+        });
+        // a conjunct after the first sits under its binder, which is shown once
+        expect(Array.from(document.querySelectorAll('.vc-binder'), binder => binder.textContent))
+            .toEqual(['∀this.failures', '∀failures.size()']);
+        previous();
+        expect(shown()).toMatchObject({ label: 'Original', position: '1/2' });
+        expect(shown().lines).toContain('∀failures failures == this.failures →');
+    });
+
+    it('shows a display step by name and skips steps with generated names or the same pass', () => {
+        const states = 'tiling(p) == tilingNotExplicit && compression(p) == compressionNotExplicit';
+        render(derivation(
+            [null, chain(['#if_condition', '#if_condition'], ['x', 'x > 0'], ['p', states])],
+            ['Binder', chain(['x', 'x > 0'], ['p', states])],
+            ['Binder', chain(['p', states])],
+            ['Relevant to Expected', chain(['p', 'compression(p) == compressionNotExplicit'])],
+        ), 'found compression(p) == compressionNotExplicit but expected ...');
+
+        expect(shown()).toEqual({
+            label: 'Relevant to Expected', info: 'Kept only the facts that share a term with Expected.',
+            position: '2/2', lines: ['∀p compression(p) == compressionNotExplicit'],
+        });
+        previous();
+        expect(shown()).toMatchObject({
+            label: 'Simplified', position: '1/2',
+            lines: ['∀p tiling(p) == tilingNotExplicit &&', 'compression(p) == compressionNotExplicit'],
+        });
+    });
+
+    it.each([
+        ['its category is unknown', [['undoManager', 'undoManager == undoManager@12']], 'unknown'],
+        ['found states nothing', [['timeout', 'true']], undefined],
+    ] as const)('says that nothing known proves Expected when %s, with the steps a step back', (label, rows, errorCategory) => {
+        render(derivation([null, chain(...rows)]), `found ${label}`, errorCategory);
+
+        expect(shown()).toMatchObject({ label: 'Summary', info: 'Go back to see what is known here.', position: '2/2', lines: [] });
+        expect(document.querySelector('.vc-nothing-known')?.textContent)
+            .toBe('Nothing is known here that could prove Expected.');
+        previous();
+        expect(document.querySelector('.vc-nothing-known')).toBeNull();
+        expect(shown()).toMatchObject({ label: 'Original', position: '1/2', lines: [`∀${rows[0][0]} ${rows[0][1]}`] });
+    });
+});
diff --git a/client/src/webview/views/diagnostics/vc-implications.ts b/client/src/webview/views/diagnostics/vc-implications.ts
index f433e2b..bd2140e 100644
--- a/client/src/webview/views/diagnostics/vc-implications.ts
+++ b/client/src/webview/views/diagnostics/vc-implications.ts
@@ -1,38 +1,76 @@
 import type { RefinementMismatchError, TranslationTable } from "../../../types/diagnostics";
-import type { VCSimplificationResult } from "../../../types/vc-implications";
+import type { VCImplication, VCSimplificationResult } from "../../../types/vc-implications";
 import { renderHighlightedExpression } from "../../highlighting";
 import { renderCodicon } from "../../icons";
 import { escapeHtml } from "../../utils";
-import { renderImplication, renderImplicationChange } from "./vc-changes";
+import { getImplicationLines, renderImplication, renderImplicationChange } from "./vc-changes";
+
+// A step of Found as it is shown: its chain, the lines it is shown in, and the passes that changed them since the step before
+type VCStep = {
+    implication: VCImplication;
+    lines: string[];
+    passes: string[];
+    // a step before the newest that says nothing known proves Expected, instead of showing the chain
+    nothingKnown?: boolean;
+};
 
 // state to preserve across re-renders
 type VCState = {
-    steps: VCSimplificationResult[];
+    steps: VCStep[];
     translationTable: TranslationTable;
     stepIndex: number;
 };
 
 const vcStates = new Map<string, VCState>(); // errorId => VCState
 
+// What each simplification pass of the verifier does, in the words of the step's tooltip; any other step, such as
+// "Relevant to Expected", is a display step and is shown by its name
+const PASS_DESCRIPTIONS: Record<string, string> = {
+    "Substitution": "Replaced variables with the values they are equal to.",
+    "Function Substitution": "Replaced calls with the values they are equal to.",
+    "Binder": "Removed facts that say nothing, and conditions that Expected does not depend on.",
+    "Known Enum Values": "Decided comparisons of variables whose enum value is known.",
+    "Folding": "Computed constant expressions.",
+    "Arithmetic": "Simplified arithmetic.",
+    "Logical": "Simplified logical operators.",
+    "Constraint": "Removed facts that other facts already imply.",
+};
+const DISPLAY_STEP_DESCRIPTIONS: Record<string, string> = {
+    "Relevant to Expected": "Kept only the facts that share a term with Expected.",
+};
+const ORIGINAL_DESCRIPTION = "What is known here, before simplifying.";
+const NOTHING_KNOWN = "Nothing is known here that could prove Expected.";
+const NOTHING_KNOWN_DESCRIPTION = "Go back to see what is known here.";
+// names the verifier makes up (#if_condition) or numbers (x#1), which do not appear in the code
+const GENERATED_NAME = /#\w/u;
+
 function renderStepButton(errorId: string, step: "previous" | "next", disabled: boolean): string {
     const label = `${step === "previous" ? "Previous" : "Next"} simplification`;
     const icon = step === "previous" ? "arrow-small-left" : "arrow-small-right";
     return `<button class="vc-step-btn vc-step-${step}-btn" data-error-id="${errorId}" data-vc-step="${step}" title="${label}" aria-label="${label}" ${disabled ? "disabled" : ""} type="button">${renderCodicon(icon)}</button>`;
 }
 
-function renderStepHeader(
-    errorId: string,
-    current: VCSimplificationResult,
-    index: number,
-    stepCount: number,
-): string {
+function getStepLabel(step: VCStep): { label: string; description: string } {
+    if (step.nothingKnown) return { label: "Summary", description: NOTHING_KNOWN_DESCRIPTION };
+    if (step.passes.length === 0) return { label: "Original", description: ORIGINAL_DESCRIPTION };
+    const displayStep = step.passes.find(pass => !(pass in PASS_DESCRIPTIONS));
+    const description = step.passes
+        .map(pass => PASS_DESCRIPTIONS[pass] ?? DISPLAY_STEP_DESCRIPTIONS[pass])
+        .filter(Boolean)
+        .join(" ");
+    return { label: displayStep ?? "Simplified", description };
+}
+
+function renderStepHeader(errorId: string, step: VCStep, index: number, stepCount: number): string {
     const currStep = stepCount - index;
-    const simplification = current.simplification?.trim();
-    const label = escapeHtml(index === 0 ? "Simplified" : simplification || "Original");
+    const { label, description } = getStepLabel(step);
 
     return /*html*/`
         <div class="vc-step-header">
-            <span class="vc-step-name" title="${label}">${label}</span>
+            <span class="vc-step-title">
+                <span class="vc-step-name" title="${escapeHtml(label)}">${escapeHtml(label)}</span>
+                ${description ? /*html*/`<span class="vc-step-info" title="${escapeHtml(description)}" aria-label="${escapeHtml(description)}">${renderCodicon("info")}</span>` : ""}
+            </span>
             <div class="vc-step-navigation">
                 <span class="vc-step-position" aria-label="Simplification step ${currStep} of ${stepCount}">
                     ${currStep}/${stepCount}
@@ -46,6 +84,54 @@ function renderStepHeader(
     `;
 }
 
+/**
+ * The steps of a derivation worth showing, newest first. The newest is always shown; an older one only when its lines
+ * use no generated name, and not when it looks like the step after it or only continues the same pass. Each step keeps
+ * the passes that changed the lines since the step before it
+ */
+function getVCSteps(result: VCSimplificationResult): VCStep[] {
+    const derivation: VCSimplificationResult[] = [];
+    for (let current: VCSimplificationResult | null = result; current; current = current.origin) {
+        derivation.unshift(current);
+    }
+    const lines = derivation.map(current => getImplicationLines(current.implication));
+
+    const shown: number[] = [];
+    lines.forEach((stepLines, index) => {
+        const isNewest = index === derivation.length - 1;
+        if (!isNewest && stepLines.some(line => GENERATED_NAME.test(line))) return;
+        const last: number | undefined = shown[shown.length - 1];
+        if (last !== undefined && (sameLines(lines[last], stepLines)
+            || (last > 0 && derivation[last].simplification === derivation[index].simplification))) {
+            shown.pop();
+        }
+        shown.push(index);
+    });
+
+    let previous = 0;
+    return shown.map(index => {
+        const passes = new Set<string>();
+        for (let i = previous + 1; i <= index; i++) {
+            const pass = derivation[i].simplification;
+            if (pass && !sameLines(lines[i - 1], lines[i])) passes.add(pass);
+        }
+        previous = index;
+        return { implication: derivation[index].implication, lines: lines[index], passes: [...passes] };
+    }).reverse();
+}
+
+function sameLines(a: string[], b: string[]): boolean {
+    return a.length === b.length && a.every((line, i) => line === b[i]);
+}
+
+// a chain states nothing when every predicate in it is true
+function statesNothing(node: VCImplication): boolean {
+    for (let current: VCImplication | null = node; current; current = current.next) {
+        if (current.predicate.trim() !== "true") return false;
+    }
+    return true;
+}
+
 function getTargetStepIndex(state: VCState, step: string | null): number | undefined {
     const targetIndex = step === "previous"
         ? state.stepIndex + 1
@@ -62,10 +148,13 @@ function renderSelectedStep(errorId: string, previousIndex?: number): string {
 
     const { steps, translationTable, stepIndex } = state;
     const current = steps[stepIndex];
-    const previous = previousIndex === undefined ? undefined : steps[previousIndex];
-    const implication = previous
-        ? `<div class="vc-chain">${renderImplicationChange(previous.implication, current.implication, translationTable)}</div>`
-        : `<div class="vc-chain">${renderImplication(current.implication, translationTable)}</div>`;
+    // a change is shown from a step whose chain was shown
+    const previous = previousIndex === undefined || steps[previousIndex].nothingKnown ? undefined : steps[previousIndex];
+    const implication = current.nothingKnown
+        ? `<p class="vc-nothing-known">${NOTHING_KNOWN}</p>`
+        : previous
+            ? `<div class="vc-chain">${renderImplicationChange(previous.implication, current.implication, translationTable)}</div>`
+            : `<div class="vc-chain">${renderImplication(current.implication, translationTable)}</div>`;
 
     return /*html*/`
         ${steps.length > 1 ? renderStepHeader(errorId, current, stepIndex, steps.length) : ""}
@@ -97,6 +186,12 @@ export function renderVCImplication(
     result: VCSimplificationResult
 ): string {
     if (!result?.implication) return renderHighlightedExpression(String(result));
+    const derivedSteps = getVCSteps(result);
+    // also when found states nothing, which a state error the verifier leaves uncategorized can have;
+    // the steps stay a step back
+    const steps = error.errorCategory === "unknown" || statesNothing(derivedSteps[0].implication)
+        ? [{ ...derivedSteps[0], passes: [], nothingKnown: true }, ...derivedSteps]
+        : derivedSteps;
 
     const errorId = encodeURIComponent(JSON.stringify([
         error.file,
@@ -104,10 +199,6 @@ export function renderVCImplication(
         error.title,
         error.message
     ]));
-    const steps: VCSimplificationResult[] = [];
-    for (let current: VCSimplificationResult | null = result; current; current = current.origin) {
-        steps.push(current);
-    }
     const stepIndex = Math.min(vcStates.get(errorId)?.stepIndex ?? 0, steps.length - 1);
     vcStates.set(errorId, { steps, translationTable: error.translationTable, stepIndex });
 
diff --git a/server/src/main/java/dtos/errors/LJErrorDTO.java b/server/src/main/java/dtos/errors/LJErrorDTO.java
index 9293491..02f0c5e 100644
--- a/server/src/main/java/dtos/errors/LJErrorDTO.java
+++ b/server/src/main/java/dtos/errors/LJErrorDTO.java
@@ -1,6 +1,7 @@
 package dtos.errors;
 
 import java.util.List;
+import java.util.Locale;
 
 import dtos.diagnostics.HintDTO;
 import dtos.diagnostics.LJDiagnosticDTO;
@@ -14,21 +15,25 @@
 public class LJErrorDTO extends LJDiagnosticDTO {
 
     public final TranslationTableDTO translationTable;
+    /** The kind of mistake, e.g. {@code unknown} when nothing known could prove what was expected, or null */
+    public final String errorCategory;
 
     public LJErrorDTO(String type, LJError error) {
-        super("error", type, error);
-        this.translationTable = TranslationTableDTO.from(error.getTranslationTable());
+        this("error", type, error);
     }
 
     protected LJErrorDTO(String category, String type, LJError error) {
         super(category, type, error);
         this.translationTable = TranslationTableDTO.from(error.getTranslationTable());
+        this.errorCategory = error.getCategory()
+                .map(kind -> kind.name().toLowerCase(Locale.ROOT).replace('_', '-')).orElse(null);
     }
 
     public LJErrorDTO(String category, String type, String title, String message, List<HintDTO> hints, String file,
             SourcePositionDTO position, TranslationTableDTO translationTable) {
         super(category, type, title, message, hints, file, position);
         this.translationTable = translationTable;
+        this.errorCategory = null;
     }
 
     public static LJErrorDTO from(LJError error) {
diff --git a/server/src/test/java/utils/DiagnosticConverterTest.java b/server/src/test/java/utils/DiagnosticConverterTest.java
index 1e24658..6776562 100644
--- a/server/src/test/java/utils/DiagnosticConverterTest.java
+++ b/server/src/test/java/utils/DiagnosticConverterTest.java
@@ -165,6 +165,7 @@ void preservesRefinementDetailsAndSimplificationHistory() {
         assertNull(dto.found.origin().origin());
         assertNull(dto.found.origin().simplification());
         assertTrue(dto.counterexample.assignments().isEmpty());
+        assertEquals("unknown", dto.errorCategory);
     }
 
     @Test
@@ -180,6 +181,7 @@ void preservesStateRefinementDetailsWithoutDeclarationFile() {
         assertEquals("expected closed", dto.customMessage);
         assertNull(dto.declarationPosition);
         assertEquals(List.of(), dto.stateMachines);
+        assertNull(dto.errorCategory);
     }
 
     @Test