From 1de4fbcbb5bfd95a91844432684169fd3b551a1d Mon Sep 17 00:00:00 2001
From: Catarina Gamboa <catarina.vg@hotmail.com>
Date: Tue, 10 Nov 2026 15:23:29 +0000
Subject: [PATCH 1/3] Wrap the Verification panel at spaces and operators, one
 conjunct per line

Expected and every Found line now show one top-level conjunct per line, and a
conditional's condition and branches each on a line of their own, with a
hanging indent for wrapped lines. The VC cells no longer break anywhere, so a
name is split only when it alone is wider than the line. A narrow panel puts
each binder above its predicate, with tighter padding and line height.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 client/src/webview/highlighting.ts            | 85 +++++++++++++++++++
 client/src/webview/styles.spec.ts             |  8 ++
 client/src/webview/styles.ts                  | 29 ++++++-
 .../src/webview/views/diagnostics/errors.ts   |  5 +-
 .../views/diagnostics/vc-changes.spec.ts      | 16 +++-
 .../webview/views/diagnostics/vc-changes.ts   |  7 +-
 6 files changed, 143 insertions(+), 7 deletions(-)

diff --git a/client/src/webview/highlighting.ts b/client/src/webview/highlighting.ts
index 03102879..fe6d3eca 100644
--- a/client/src/webview/highlighting.ts
+++ b/client/src/webview/highlighting.ts
@@ -98,6 +98,91 @@ export function renderHighlightedExpression(expression: string): string {
     return renderExpression(expression, true);
 }
 
+const WEAKER_THAN_AND = ["||", "-->", "?"];
+
+// the positions of the characters outside parentheses and string literals
+function topLevelIndices(expression: string): number[] {
+    const indices: number[] = [];
+    let depth = 0;
+    let inString = false;
+    for (let i = 0; i < expression.length; i++) {
+        if (inString) {
+            if (expression[i] === "\\") i++;
+            else if (expression[i] === '"') inString = false;
+        }
+        else if (expression[i] === '"') inString = true;
+        else if (expression[i] === "(") depth++;
+        else if (expression[i] === ")") depth--;
+        else if (depth === 0) indices.push(i);
+    }
+    return indices;
+}
+
+/**
+ * Splits an expression at its top-level &&, keeping the && at the end of each conjunct but the last. An && inside
+ * parentheses or a string literal stays in its conjunct, and nothing is split when a weaker operator (||, -->, ?:)
+ * outside them would make the parts look like conjuncts of the whole expression
+ */
+function splitConjuncts(expression: string): string[] {
+    const indices = topLevelIndices(expression);
+    if (indices.some(i => WEAKER_THAN_AND.some(operator => expression.startsWith(operator, i)))) return [expression.trim()];
+
+    const conjuncts: string[] = [];
+    let start = 0;
+    for (const i of indices) {
+        if (i < start || !expression.startsWith("&&", i)) continue;
+        conjuncts.push(expression.slice(start, i + 2).trim());
+        start = i + 2;
+    }
+    const last = expression.slice(start).trim();
+    return last ? [...conjuncts, last] : conjuncts;
+}
+
+// the condition and the two branches of an expression that is a conditional outside parentheses, or null
+function splitConditional(expression: string): [string, string, string] | null {
+    const indices = topLevelIndices(expression);
+    const question = indices.find(i => expression[i] === "?");
+    if (question === undefined) return null;
+
+    let nested = 0;
+    for (const i of indices.filter(i => i > question)) {
+        if (expression[i] === "?") nested++;
+        else if (expression[i] === ":" && nested-- === 0)
+            return [expression.slice(0, question), expression.slice(question + 1, i), expression.slice(i + 1)]
+                .map(part => part.trim()) as [string, string, string];
+    }
+    return null;
+}
+
+/**
+ * The lines an expression is shown on: one per top-level conjunct, and a conditional's condition with each branch
+ * on a line of its own, indented
+ */
+function getExpressionLines(expression: string): { text: string; branch: boolean }[] {
+    return splitConjuncts(expression).flatMap(conjunct => {
+        const conditional = splitConditional(conjunct);
+        if (!conditional) return [{ text: conjunct, branch: false }];
+        const [condition, then, otherwise] = conditional;
+        return [{ text: condition, branch: false }, { text: `? ${then}`, branch: true }, { text: `: ${otherwise}`, branch: true }];
+    });
+}
+
+/**
+ * Renders an expression on the lines of getExpressionLines, each of which wraps with a hanging indent
+ * @param wrap whether to wrap the lines in an expression block, as renderHighlightedExpression does
+ * @param trailing html shown at the end of the last line
+ */
+export function renderHighlightedLines(expression: string, wrap = true, trailing = ""): string {
+    if (!expression) return "";
+
+    const lines = getExpressionLines(expression);
+    const html = lines.map((line, index) => {
+        const end = index === lines.length - 1 ? trailing : "";
+        return `<span class="lj-line${line.branch ? " lj-line-branch" : ""}">${renderHighlightedContent(line.text)}${end}</span>`;
+    }).join("");
+    return wrap ? `<pre class="lj-expression-block"><code class="lj-expression-code">${html}</code></pre>` : html;
+}
+
 export function renderHighlightedInlineExpression(expression: string): string {
     return renderExpression(expression, false);
 }
diff --git a/client/src/webview/styles.spec.ts b/client/src/webview/styles.spec.ts
index 722e3d0b..70408c91 100644
--- a/client/src/webview/styles.spec.ts
+++ b/client/src/webview/styles.spec.ts
@@ -105,6 +105,14 @@ describe('state error styles', () => {
         }
     });
 
+    it('breaks a Found line inside a name only when the name alone is wider than the line', () => {
+        render('');
+        document.body.insertAdjacentHTML('beforeend', '<div class="vc-binder-cell"></div><div class="vc-predicate-cell"></div>');
+
+        expect(style('.vc-binder-cell').overflowWrap).toBe('break-word');
+        expect(style('.vc-predicate-cell').overflowWrap).toBe('break-word');
+    });
+
     it('keeps other states with the default outline', () => {
         render(state(''));
 
diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts
index e682ed1c..2bed3abc 100644
--- a/client/src/webview/styles.ts
+++ b/client/src/webview/styles.ts
@@ -392,6 +392,14 @@ export function getStyles(): string {
             background: transparent !important;
             background-color: transparent !important;
         }
+        .lj-line {
+            display: block;
+            padding-left: 2ch;
+            text-indent: -2ch;
+        }
+        .lj-line-branch {
+            padding-left: 4ch;
+        }
         .lj-token-keyword {
             color: var(--lj-token-keyword);
         }
@@ -479,7 +487,7 @@ export function getStyles(): string {
             gap: 0.25rem;
         }
         .counterexample-line {
-            overflow-wrap: anywhere;
+            overflow-wrap: break-word;
         }
         .vc-line {
             display: contents;
@@ -488,7 +496,7 @@ export function getStyles(): string {
         .vc-predicate-cell {
             min-width: 0;
             padding: 0.0625rem 0.25rem;
-            overflow-wrap: anywhere;
+            overflow-wrap: break-word;
         }
         .vc-binder-cell {
             min-height: 1.2em;
@@ -499,6 +507,23 @@ export function getStyles(): string {
         .vc-predicate-cell {
             color: var(--vscode-editor-foreground);
         }
+        /* a narrow panel puts each binder above its predicate, so that the predicate gets the whole width */
+        @media (max-width: 420px) {
+            .diagnostic-item {
+                padding-inline: 0.5rem;
+            }
+            .vc-container {
+                padding-inline: 0.25rem;
+            }
+            .vc-chain {
+                grid-template-columns: minmax(0, 1fr);
+                line-height: 1.4;
+            }
+            .vc-binder-cell,
+            .vc-predicate-cell {
+                padding-inline: 0;
+            }
+        }
         .vc-arrow {
             font-size: 1.5em;
             line-height: 0;
diff --git a/client/src/webview/views/diagnostics/errors.ts b/client/src/webview/views/diagnostics/errors.ts
index 0e58ed46..72c4875a 100644
--- a/client/src/webview/views/diagnostics/errors.ts
+++ b/client/src/webview/views/diagnostics/errors.ts
@@ -1,5 +1,6 @@
 import { renderDiagnosticDataAttributes, renderExpressionSection, renderDiagnosticHeader, renderCustomSection, renderLocation, renderDiagnosticContextButton, renderDiagnosticStateMachineButton, renderHints } from "../sections";
 import { renderCounterexample } from "./counterexample";
+import { renderHighlightedLines } from "../../highlighting";
 import { renderVCImplication } from "./vc-implications";
 import type {
     ArgumentMismatchError,
@@ -38,14 +39,14 @@ type ErrorRendererMap = { [E in LJError as E['type']]: (error: E) => string };
 
 const errorContentRenderers: ErrorRendererMap = {
     'refinement-error': (e: RefinementError) => /*html*/ `
-        ${renderExpressionSection('Expected', e.expected)}
+        ${renderCustomSection('Expected', renderHighlightedLines(e.expected))}
         ${renderCustomSection('Found', renderVCImplication(e, e.found))}
         ${e.counterexample.assignments.length > 0
             ? renderCustomSection('Counterexample', renderCounterexample(e.counterexample))
             : ''}
     `,
     'state-refinement-error': (e: StateRefinementError) => /*html*/ `
-        ${renderExpressionSection('Expected', e.expected)}
+        ${renderCustomSection('Expected', renderHighlightedLines(e.expected))}
         ${renderCustomSection('Found', renderVCImplication(e, e.found))}
     `,
     'invalid-refinement-error': (e: InvalidRefinementError) => /*html*/ `
diff --git a/client/src/webview/views/diagnostics/vc-changes.spec.ts b/client/src/webview/views/diagnostics/vc-changes.spec.ts
index 06527fb1..33b658a4 100644
--- a/client/src/webview/views/diagnostics/vc-changes.spec.ts
+++ b/client/src/webview/views/diagnostics/vc-changes.spec.ts
@@ -25,7 +25,21 @@ describe('verification implications', () => {
         expect(document.querySelector('.vc-line:last-child')?.textContent?.trim()).toBe('x > 0');
         expect(Array.from(document.querySelectorAll('.vc-predicate-cell')).map(cell => cell.textContent?.trim()))
             .toEqual(['x == 1 →', 'y == 2 →', 'x > 0']);
-        expect(document.querySelectorAll('.vc-predicate-cell > .vc-arrow')).toHaveLength(2);
+        expect(document.querySelectorAll('.vc-predicate-cell .vc-arrow')).toHaveLength(2);
+    });
+    it('puts each top-level conjunct and each branch of a conditional on a line of its own', () => {
+        document.body.innerHTML = renderImplication({
+            name: 'h', type: 'Frame', predicate: 'a > 0 && (b || c) && s == "x && y"',
+            next: { ...conclusion, predicate: 'p && q ? d(h) == on : (p ? d(h) == off : d(h) == on)' },
+        });
+
+        const lines = (cell: Element) => Array.from(cell.querySelectorAll('.lj-line'))
+            .map(line => [line.textContent, line.classList.contains('lj-line-branch')]);
+        const [fact, conditional] = document.querySelectorAll('.vc-predicate-cell');
+        expect(lines(fact)).toEqual([['a > 0 &&', false], ['(b || c) &&', false], ['s == "x && y" →', false]]);
+        expect(lines(conditional)).toEqual([
+            ['p && q', false], ['? d(h) == on', true], [': (p ? d(h) == off : d(h) == on)', true],
+        ]);
     });
     it.each([
         ['initial rendering', () => renderImplication({ ...implication, next: null })],
diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts
index a5c0d37b..f15fd899 100644
--- a/client/src/webview/views/diagnostics/vc-changes.ts
+++ b/client/src/webview/views/diagnostics/vc-changes.ts
@@ -1,6 +1,6 @@
 import type { VCImplication } from "../../../types/vc-implications";
 import type { TranslationTable } from "../../../types/diagnostics";
-import { renderHighlightedInlineExpression } from "../../highlighting";
+import { renderHighlightedInlineExpression, renderHighlightedLines } from "../../highlighting";
 import { escapeHtml } from "../../utils";
 import { renderSourceHighlightButton } from "../sections";
 
@@ -56,10 +56,13 @@ export function renderVCLine(
     translationTable?: TranslationTable,
 ): string {
     const { binder, type, predicate, hasNext } = parseImplicationLine(line);
+    const arrow = hasNext ? ' <span class="vc-arrow">→</span>' : "";
     return /*html*/`
         <div class="vc-line ${className}">
             ${binder ? /*html*/`<div class="vc-binder-cell">${renderBinder(binder, type, translationTable)}</div>` : ""}
-            <div class="vc-predicate-cell"><span class="vc-node">${predicateContent ?? renderHighlightedInlineExpression(predicate)}</span>${hasNext ? ' <span class="vc-arrow">→</span>' : ""}</div>
+            <div class="vc-predicate-cell">${predicateContent === undefined
+                ? `<span class="vc-node">${renderHighlightedLines(predicate, false, arrow)}</span>`
+                : `<span class="vc-node">${predicateContent}</span>${arrow}`}</div>
         </div>
     `;
 }

From 56287c186f06631432f38f6fbfe5131733211048 Mon Sep 17 00:00:00 2001
From: Catarina Gamboa <catarina.vg@hotmail.com>
Date: Tue, 10 Nov 2026 19:05:02 +0000
Subject: [PATCH 2/3] Split changed Found predicates into lines too, and skip
 character literals

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 client/src/webview/highlighting.ts            | 44 ++++++++++++-------
 .../views/diagnostics/vc-changes.spec.ts      | 13 +++++-
 .../webview/views/diagnostics/vc-changes.ts   | 20 ++++-----
 3 files changed, 49 insertions(+), 28 deletions(-)

diff --git a/client/src/webview/highlighting.ts b/client/src/webview/highlighting.ts
index fe6d3eca..0210aae2 100644
--- a/client/src/webview/highlighting.ts
+++ b/client/src/webview/highlighting.ts
@@ -100,17 +100,17 @@ export function renderHighlightedExpression(expression: string): string {
 
 const WEAKER_THAN_AND = ["||", "-->", "?"];
 
-// the positions of the characters outside parentheses and string literals
+// the positions of the characters outside parentheses and string or character literals
 function topLevelIndices(expression: string): number[] {
     const indices: number[] = [];
     let depth = 0;
-    let inString = false;
+    let quote: string | null = null;
     for (let i = 0; i < expression.length; i++) {
-        if (inString) {
+        if (quote) {
             if (expression[i] === "\\") i++;
-            else if (expression[i] === '"') inString = false;
+            else if (expression[i] === quote) quote = null;
         }
-        else if (expression[i] === '"') inString = true;
+        else if (expression[i] === '"' || expression[i] === "'") quote = expression[i];
         else if (expression[i] === "(") depth++;
         else if (expression[i] === ")") depth--;
         else if (depth === 0) indices.push(i);
@@ -120,7 +120,7 @@ function topLevelIndices(expression: string): number[] {
 
 /**
  * Splits an expression at its top-level &&, keeping the && at the end of each conjunct but the last. An && inside
- * parentheses or a string literal stays in its conjunct, and nothing is split when a weaker operator (||, -->, ?:)
+ * parentheses or a literal stays in its conjunct, and nothing is split when a weaker operator (||, -->, ?:)
  * outside them would make the parts look like conjuncts of the whole expression
  */
 function splitConjuncts(expression: string): string[] {
@@ -154,11 +154,13 @@ function splitConditional(expression: string): [string, string, string] | null {
     return null;
 }
 
+export type ExpressionLine = { text: string; branch: boolean };
+
 /**
  * The lines an expression is shown on: one per top-level conjunct, and a conditional's condition with each branch
  * on a line of its own, indented
  */
-function getExpressionLines(expression: string): { text: string; branch: boolean }[] {
+export function getExpressionLines(expression: string): ExpressionLine[] {
     return splitConjuncts(expression).flatMap(conjunct => {
         const conditional = splitConditional(conjunct);
         if (!conditional) return [{ text: conjunct, branch: false }];
@@ -168,19 +170,29 @@ function getExpressionLines(expression: string): { text: string; branch: boolean
 }
 
 /**
- * Renders an expression on the lines of getExpressionLines, each of which wraps with a hanging indent
- * @param wrap whether to wrap the lines in an expression block, as renderHighlightedExpression does
+ * Renders the lines of an expression, each of which wraps with a hanging indent
+ * @param renderText renders the text of a line, highlighted by default
  * @param trailing html shown at the end of the last line
  */
-export function renderHighlightedLines(expression: string, wrap = true, trailing = ""): string {
-    if (!expression) return "";
-
-    const lines = getExpressionLines(expression);
-    const html = lines.map((line, index) => {
+export function renderExpressionLines(
+    lines: ExpressionLine[],
+    renderText: (text: string) => string = renderHighlightedContent,
+    trailing = "",
+): string {
+    return lines.map((line, index) => {
         const end = index === lines.length - 1 ? trailing : "";
-        return `<span class="lj-line${line.branch ? " lj-line-branch" : ""}">${renderHighlightedContent(line.text)}${end}</span>`;
+        return `<span class="lj-line${line.branch ? " lj-line-branch" : ""}">${renderText(line.text)}${end}</span>`;
     }).join("");
-    return wrap ? `<pre class="lj-expression-block"><code class="lj-expression-code">${html}</code></pre>` : html;
+}
+
+/**
+ * Renders an expression on the lines of getExpressionLines, in an expression block as renderHighlightedExpression does
+ */
+export function renderHighlightedLines(expression: string): string {
+    if (!expression) return "";
+
+    const html = renderExpressionLines(getExpressionLines(expression));
+    return `<pre class="lj-expression-block"><code class="lj-expression-code">${html}</code></pre>`;
 }
 
 export function renderHighlightedInlineExpression(expression: string): string {
diff --git a/client/src/webview/views/diagnostics/vc-changes.spec.ts b/client/src/webview/views/diagnostics/vc-changes.spec.ts
index 33b658a4..d90c4679 100644
--- a/client/src/webview/views/diagnostics/vc-changes.spec.ts
+++ b/client/src/webview/views/diagnostics/vc-changes.spec.ts
@@ -30,7 +30,7 @@ describe('verification implications', () => {
     it('puts each top-level conjunct and each branch of a conditional on a line of its own', () => {
         document.body.innerHTML = renderImplication({
             name: 'h', type: 'Frame', predicate: 'a > 0 && (b || c) && s == "x && y"',
-            next: { ...conclusion, predicate: 'p && q ? d(h) == on : (p ? d(h) == off : d(h) == on)' },
+            next: { ...conclusion, predicate: "p && q ? d(h) == on : (c == ':' ? d(h) == off : d(h) == on)" },
         });
 
         const lines = (cell: Element) => Array.from(cell.querySelectorAll('.lj-line'))
@@ -38,9 +38,18 @@ describe('verification implications', () => {
         const [fact, conditional] = document.querySelectorAll('.vc-predicate-cell');
         expect(lines(fact)).toEqual([['a > 0 &&', false], ['(b || c) &&', false], ['s == "x && y" →', false]]);
         expect(lines(conditional)).toEqual([
-            ['p && q', false], ['? d(h) == on', true], [': (p ? d(h) == off : d(h) == on)', true],
+            ['p && q', false], ['? d(h) == on', true], [": (c == ':' ? d(h) == off : d(h) == on)", true],
         ]);
     });
+    it('keeps a conjunct per line in a predicate that a simplification changed', () => {
+        document.body.innerHTML = renderImplicationChange(
+            { ...conclusion, predicate: 'x > 0 && y > 0' }, { ...conclusion, predicate: 'x > 0 && y == 1' },
+        );
+
+        expect(Array.from(document.querySelectorAll('.lj-line')).map(line => line.textContent))
+            .toEqual(['x > 0 &&', 'y == 1']);
+        expect(document.querySelector('.lj-line:last-child .vc-change-fragment')?.textContent).toBe('==');
+    });
     it.each([
         ['initial rendering', () => renderImplication({ ...implication, next: null })],
         ['simplification change', () => renderImplicationChange(implication, { ...implication, next: null })],
diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts
index f15fd899..56ee3653 100644
--- a/client/src/webview/views/diagnostics/vc-changes.ts
+++ b/client/src/webview/views/diagnostics/vc-changes.ts
@@ -1,6 +1,6 @@
 import type { VCImplication } from "../../../types/vc-implications";
 import type { TranslationTable } from "../../../types/diagnostics";
-import { renderHighlightedInlineExpression, renderHighlightedLines } from "../../highlighting";
+import { getExpressionLines, renderExpressionLines, renderHighlightedInlineExpression } from "../../highlighting";
 import { escapeHtml } from "../../utils";
 import { renderSourceHighlightButton } from "../sections";
 
@@ -49,10 +49,14 @@ function renderBinder(binder: string, type: string, translationTable?: Translati
     );
 }
 
+/**
+ * Renders a line of a VC chain, its predicate on the lines of getExpressionLines
+ * @param renderText renders the text of each of those lines, highlighted by default
+ */
 export function renderVCLine(
     line: string,
     className = "",
-    predicateContent?: string,
+    renderText?: (text: string) => string,
     translationTable?: TranslationTable,
 ): string {
     const { binder, type, predicate, hasNext } = parseImplicationLine(line);
@@ -60,9 +64,7 @@ export function renderVCLine(
     return /*html*/`
         <div class="vc-line ${className}">
             ${binder ? /*html*/`<div class="vc-binder-cell">${renderBinder(binder, type, translationTable)}</div>` : ""}
-            <div class="vc-predicate-cell">${predicateContent === undefined
-                ? `<span class="vc-node">${renderHighlightedLines(predicate, false, arrow)}</span>`
-                : `<span class="vc-node">${predicateContent}</span>${arrow}`}</div>
+            <div class="vc-predicate-cell"><span class="vc-node">${renderExpressionLines(getExpressionLines(predicate), renderText, arrow)}</span></div>
         </div>
     `;
 }
@@ -202,14 +204,12 @@ function renderChangedDestinationLines(
         .map(([before, after]) => {
             if (after === undefined) return "";
             if (before === undefined) return renderVCLine(after, "vc-change-line", undefined, translationTable);
-            const change = renderDestinationTokenDiff(
-                parseImplicationLine(before).predicate,
-                parseImplicationLine(after).predicate,
-            );
+            const beforePredicate = parseImplicationLine(before).predicate;
+            const change = renderDestinationTokenDiff(beforePredicate, parseImplicationLine(after).predicate);
             return renderVCLine(
                 after,
                 change.hasAddedContent ? "" : "vc-change-line",
-                change.content,
+                text => renderDestinationTokenDiff(beforePredicate, text).content,
                 translationTable,
             );
         })

From 600f884068cd8f13e5bd5833edc919ec3eaaf268 Mon Sep 17 00:00:00 2001
From: Catarina Gamboa <catarina.vg@hotmail.com>
Date: Tue, 10 Nov 2026 19:08:02 +0000
Subject: [PATCH 3/3] Diff each line of a changed Found predicate against the
 line it replaces

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
---
 client/src/webview/highlighting.ts            |  6 ++---
 .../views/diagnostics/vc-changes.spec.ts      | 10 ++++-----
 .../webview/views/diagnostics/vc-changes.ts   | 22 +++++++++++++++----
 3 files changed, 26 insertions(+), 12 deletions(-)

diff --git a/client/src/webview/highlighting.ts b/client/src/webview/highlighting.ts
index 0210aae2..3b50bf1f 100644
--- a/client/src/webview/highlighting.ts
+++ b/client/src/webview/highlighting.ts
@@ -171,17 +171,17 @@ export function getExpressionLines(expression: string): ExpressionLine[] {
 
 /**
  * Renders the lines of an expression, each of which wraps with a hanging indent
- * @param renderText renders the text of a line, highlighted by default
+ * @param renderText renders the text of the line at an index, highlighted by default
  * @param trailing html shown at the end of the last line
  */
 export function renderExpressionLines(
     lines: ExpressionLine[],
-    renderText: (text: string) => string = renderHighlightedContent,
+    renderText: (text: string, index: number) => string = renderHighlightedContent,
     trailing = "",
 ): string {
     return lines.map((line, index) => {
         const end = index === lines.length - 1 ? trailing : "";
-        return `<span class="lj-line${line.branch ? " lj-line-branch" : ""}">${renderText(line.text)}${end}</span>`;
+        return `<span class="lj-line${line.branch ? " lj-line-branch" : ""}">${renderText(line.text, index)}${end}</span>`;
     }).join("");
 }
 
diff --git a/client/src/webview/views/diagnostics/vc-changes.spec.ts b/client/src/webview/views/diagnostics/vc-changes.spec.ts
index d90c4679..20287274 100644
--- a/client/src/webview/views/diagnostics/vc-changes.spec.ts
+++ b/client/src/webview/views/diagnostics/vc-changes.spec.ts
@@ -41,14 +41,14 @@ describe('verification implications', () => {
             ['p && q', false], ['? d(h) == on', true], [": (c == ':' ? d(h) == off : d(h) == on)", true],
         ]);
     });
-    it('keeps a conjunct per line in a predicate that a simplification changed', () => {
+    it('keeps a conjunct per line in a predicate that a simplification changed, marking a repeated conjunct it adds', () => {
         document.body.innerHTML = renderImplicationChange(
-            { ...conclusion, predicate: 'x > 0 && y > 0' }, { ...conclusion, predicate: 'x > 0 && y == 1' },
+            { ...conclusion, predicate: 'x > 0' }, { ...conclusion, predicate: 'x > 0 && x > 0' },
         );
 
-        expect(Array.from(document.querySelectorAll('.lj-line')).map(line => line.textContent))
-            .toEqual(['x > 0 &&', 'y == 1']);
-        expect(document.querySelector('.lj-line:last-child .vc-change-fragment')?.textContent).toBe('==');
+        expect(Array.from(document.querySelectorAll('.lj-line')).map(line => line.textContent)).toEqual(['x > 0 &&', 'x > 0']);
+        expect(Array.from(document.querySelectorAll('.vc-change-fragment')).map(fragment => fragment.textContent))
+            .toEqual(['x > 0 &&']);
     });
     it.each([
         ['initial rendering', () => renderImplication({ ...implication, next: null })],
diff --git a/client/src/webview/views/diagnostics/vc-changes.ts b/client/src/webview/views/diagnostics/vc-changes.ts
index 56ee3653..24f2e742 100644
--- a/client/src/webview/views/diagnostics/vc-changes.ts
+++ b/client/src/webview/views/diagnostics/vc-changes.ts
@@ -51,12 +51,12 @@ function renderBinder(binder: string, type: string, translationTable?: Translati
 
 /**
  * Renders a line of a VC chain, its predicate on the lines of getExpressionLines
- * @param renderText renders the text of each of those lines, highlighted by default
+ * @param renderText renders the text of the line at an index, highlighted by default
  */
 export function renderVCLine(
     line: string,
     className = "",
-    renderText?: (text: string) => string,
+    renderText?: (text: string, index: number) => string,
     translationTable?: TranslationTable,
 ): string {
     const { binder, type, predicate, hasNext } = parseImplicationLine(line);
@@ -193,6 +193,18 @@ function alignChangedLines(removed: string[], added: string[]): Array<[string |
     return lines;
 }
 
+// each line of a changed predicate, diffed against the line of the old predicate it replaces, or all marked if none
+function renderChangedPredicateLines(before: string, after: string): string[] {
+    const lines = (predicate: string) => getExpressionLines(predicate).map(line => line.text);
+    return alignChangedLines(lines(before), lines(after))
+        .flatMap(([beforeLine, afterLine]) => {
+            if (afterLine === undefined) return [];
+            return [beforeLine === undefined
+                ? renderChangedFragment(afterLine)
+                : renderDestinationTokenDiff(beforeLine, afterLine).content];
+        });
+}
+
 function renderChangedDestinationLines(
     removed: string[],
     added: string[],
@@ -205,11 +217,13 @@ function renderChangedDestinationLines(
             if (after === undefined) return "";
             if (before === undefined) return renderVCLine(after, "vc-change-line", undefined, translationTable);
             const beforePredicate = parseImplicationLine(before).predicate;
-            const change = renderDestinationTokenDiff(beforePredicate, parseImplicationLine(after).predicate);
+            const afterPredicate = parseImplicationLine(after).predicate;
+            const change = renderDestinationTokenDiff(beforePredicate, afterPredicate);
+            const lines = renderChangedPredicateLines(beforePredicate, afterPredicate);
             return renderVCLine(
                 after,
                 change.hasAddedContent ? "" : "vc-change-line",
-                text => renderDestinationTokenDiff(beforePredicate, text).content,
+                (_text, index) => lines[index],
                 translationTable,
             );
         })