diff --git a/client/src/types/context.ts b/client/src/types/context.ts
index 90ec9d7..174fcd2 100644
--- a/client/src/types/context.ts
+++ b/client/src/types/context.ts
@@ -1,4 +1,4 @@
-import { SourcePosition } from "./diagnostics";
+import { SourcePosition, TranslationTable } from "./diagnostics";
 
 // Type definitions used for LiquidJava context information
 
@@ -54,6 +54,7 @@ export type LJContext = {
   visibleVars: LJVariable[]; // variables visible in the current selection
   allVars: LJVariable[]; // instance vars + global vars + vars in scope
   fileScopes: Record<string, Range[]>; // file -> scopes
+  generatedPlaces: TranslationTable; // where each value the verifier introduces, such as #if_condition, comes from
 }
 
 export type Range = {
diff --git a/client/src/webview/generated-names.ts b/client/src/webview/generated-names.ts
new file mode 100644
index 0000000..890d3ed
--- /dev/null
+++ b/client/src/webview/generated-names.ts
@@ -0,0 +1,73 @@
+import type { PlacementInCode, SourcePosition } from "../types/diagnostics";
+import { escapeHtml } from "./utils";
+
+// what a value the verifier names stands for, given where it is (" at line 12", or empty when unknown)
+type Description = (at: string) => string;
+
+const NAMED_VALUES = new Map<string, Description>(Object.entries({
+    if_condition: at => `the condition of the if${at}`,
+    loop_condition: at => `the condition of the loop${at}`,
+    ternary_condition: at => `the condition of the ? :${at}`,
+    switch_selector: at => `the value the switch${at} checks`,
+    case_condition: at => `whether the case${at} matches`,
+    try_branch: at => `whether the try block${at} runs to its end, rather than a catch block`,
+    catch_branch: at => `whether this catch block of the try${at} runs, rather than a later one`,
+    array_length: at => `the length of the array created${at}`,
+    operation_result: at => `the result of the operation${at}`,
+    expression_value: at => `the value of the expression${at}`,
+} satisfies Record<string, Description>));
+
+// values named after the code they come from: a call, a new object or a field read
+const VALUES_OF_CODE: [RegExp, (code: string) => Description][] = [
+    [/^new_(\w+)$/, type => at => `the new ${type} object created${at}`],
+    [/^(\w+)_result$/, method => at => `the value returned by the call to ${method}()${at}`],
+    [/^(\w+)_value$/, field => at => `the value of the field ${field} read${at}`],
+];
+
+function describe(name: string): Description | undefined {
+    const kind = name.slice(1);
+    if (!name.startsWith("#") || !kind) return undefined;
+    const named = NAMED_VALUES.get(kind);
+    if (named) return named;
+    for (const [pattern, describeCode] of VALUES_OF_CODE) {
+        const code = pattern.exec(kind)?.[1];
+        if (code) return describeCode(code);
+    }
+    return undefined;
+}
+
+/** Whether a name, written without its line tag, is one the verifier gives a value of the code, such as #if_condition */
+export function isGeneratedName(name: string): boolean {
+    return describe(name) !== undefined;
+}
+
+// says in plain words what a value the verifier names stands for, such as "The condition of the if at line 12"
+function explain(name: string, line?: number): string {
+    const description = describe(name)?.(line === undefined ? "" : ` at line ${line}`) ?? "";
+    return `${description.charAt(0).toUpperCase()}${description.slice(1)}. LiquidJava gives it the name ${name}.`;
+}
+
+/**
+ * The hover text of a name the verifier gives a value of the code: what the value is, and where when it is known
+ * @param name the name without its line tag
+ * @param position where the value comes from, if known; it is a link when it has a file
+ * @param tagLine the line of the name's line tag, used when the position is not known
+ */
+export function generatedNameTitle(name: string, position?: SourcePosition | null, tagLine?: number): string {
+    const explanation = explain(name, position ? position.lineStart + 1 : tagLine);
+    return position?.file ? `${explanation} Click to go to it.` : explanation;
+}
+
+/**
+ * Renders a name the verifier gives a value of the code, explained on hover and, when its place is known, a link to it
+ * @param name the name without its line tag
+ * @param content the name as rendered, with its line tag
+ * @param tagLine the line of its line tag, if it has one
+ * @param place where the value comes from, if known
+ */
+export function renderGeneratedName(name: string, content: string, tagLine?: number, place?: PlacementInCode): string {
+    const position = place?.position;
+    const title = escapeHtml(generatedNameTitle(name, position, tagLine));
+    if (!position?.file) return `<span class="lj-generated-name" title="${title}">${content}</span>`;
+    return /*html*/`<span class="lj-generated-name location-link" title="${title}" data-file="${escapeHtml(position.file)}" data-line="${position.lineStart}" data-column="${position.colStart}">${content}</span>`;
+}
diff --git a/client/src/webview/highlighting.ts b/client/src/webview/highlighting.ts
index 4c46924..c89bfd4 100644
--- a/client/src/webview/highlighting.ts
+++ b/client/src/webview/highlighting.ts
@@ -1,4 +1,6 @@
 import * as liquidJavaGrammar from "../../syntaxes/liquidjava.json";
+import type { TranslationTable } from "../types/diagnostics";
+import { isGeneratedName, renderGeneratedName } from "./generated-names";
 import { escapeHtml } from "./utils";
 
 type GrammarPattern = {
@@ -22,6 +24,8 @@ type ScopeColorRule = {
 // numbered when values share a line or have none, x@12#2 and x#2
 export const LINE_TAG = "@\\d+(?:#\\d+)?\\b|(?<=[\\w)])#\\d+\\b";
 const LINE_TAG_SCOPE = "line-tag";
+const VARIABLE_SCOPE = "variable.other.liquidjava";
+const LINE_TAG_AT_INDEX = new RegExp(LINE_TAG, "y");
 // string and character literals, whose text is shown as it is even where it looks like a line tag
 export const LITERAL = `"(?:\\\\.|[^"\\\\])*"|'(?:\\\\.|[^'\\\\])*'`;
 const LINE_TAGS_OUTSIDE_LITERALS = new RegExp(`${LITERAL}|${LINE_TAG}`, "g");
@@ -44,7 +48,7 @@ const expressionPatterns: GrammarPattern[] = [
     { match: "\\bnull\\b", name: "constant.language.null.liquidjava.webview" },
     ...patterns("literals"),
     { match: "[(){}.,;\\[\\]]", name: "punctuation.separator.liquidjava" },
-    { match: "#*[a-zA-Z_](?:[a-zA-Z0-9_]|#(?!\\d))*", name: "variable.other.liquidjava" }
+    { match: "#*[a-zA-Z_](?:[a-zA-Z0-9_]|#(?!\\d))*", name: VARIABLE_SCOPE }
 ];
 
 const highlightRules: HighlightRule[] = expressionPatterns
@@ -117,12 +121,38 @@ export function renderLineTags(text: string): string {
     return html + escapeHtml(text.slice(index));
 }
 
+/** The line of the line tag a name ends with, x@12 or x@12#2, if it has one */
+export function lineOfTag(name: string): number | undefined {
+    const line = /@(\d+)(?:#\d+)?$/.exec(name)?.[1];
+    return line === undefined ? undefined : Number(line);
+}
+
 /** The name of a variable without its line tag, as it is written in code */
 export function withoutLineTag(name: string): string {
     return name.replace(new RegExp(`(?:${LINE_TAG})$`), "");
 }
 
-function renderHighlightedContent(expression: string): string {
+function renderToken(content: string, scope: string): string {
+    return `<span style="color:${colorForScope(scope)}">${escapeHtml(content)}</span>`;
+}
+
+/**
+ * Renders a name the verifier gives a value of the code, with the line tag after it if any
+ * @returns the html and the length of the text it renders
+ */
+function renderGeneratedNameAt(expression: string, index: number, name: string, places?: TranslationTable): [string, number] {
+    LINE_TAG_AT_INDEX.lastIndex = index + name.length;
+    const tag = LINE_TAG_AT_INDEX.exec(expression)?.[0] ?? "";
+    const content = renderToken(name, VARIABLE_SCOPE) + (tag ? renderLineTag(tag, name) : "");
+    const html = renderGeneratedName(name, content, lineOfTag(tag), places?.[name + tag]);
+    return [html, name.length + tag.length];
+}
+
+/**
+ * Renders an expression with its tokens colored
+ * @param places where the variables of the expression come from, by name, such as the translation table of an error
+ */
+function renderHighlightedContent(expression: string, places?: TranslationTable): string {
     let html = "";
     let index = 0;
 
@@ -140,25 +170,31 @@ function renderHighlightedContent(expression: string): string {
         const match = matchingRule.regex.exec(expression);
         const content = match?.[0] || expression[index] || "";
 
+        if (matchingRule.scope === VARIABLE_SCOPE && isGeneratedName(content)) {
+            const [generated, length] = renderGeneratedNameAt(expression, index, content, places);
+            html += generated;
+            index += length;
+            continue;
+        }
         html += matchingRule.scope === LINE_TAG_SCOPE
             ? renderLineTag(content, variableBefore(expression, index))
-            : `<span style="color:${colorForScope(matchingRule.scope)}">${escapeHtml(content)}</span>`;
+            : renderToken(content, matchingRule.scope);
         index += content.length;
     }
     return html;
 }
 
-function renderExpression(expression: string, wrap: boolean): string {
+function renderExpression(expression: string, wrap: boolean, places?: TranslationTable): string {
     if (!expression) return "";
 
-    const content = renderHighlightedContent(expression);
+    const content = renderHighlightedContent(expression, places);
     return wrap
         ? `<pre class="lj-expression-block"><code class="lj-expression-code">${content}</code></pre>`
         : content;
 }
 
-export function renderHighlightedExpression(expression: string): string {
-    return renderExpression(expression, true);
+export function renderHighlightedExpression(expression: string, places?: TranslationTable): string {
+    return renderExpression(expression, true, places);
 }
 
 const WEAKER_THAN_AND = ["||", "-->", "?"];
@@ -239,7 +275,7 @@ export function getExpressionLines(expression: string): ExpressionLine[] {
  */
 export function renderExpressionLines(
     lines: ExpressionLine[],
-    renderText: (text: string, index: number) => string = renderHighlightedContent,
+    renderText: (text: string, index: number) => string = text => renderHighlightedContent(text),
     trailing = "",
 ): string {
     return lines.map((line, index) => {
@@ -250,14 +286,19 @@ export function renderExpressionLines(
 
 /**
  * Renders an expression on the lines of getExpressionLines, in an expression block as renderHighlightedExpression does
+ * @param places where the variables of the expression come from, by name
  */
-export function renderHighlightedLines(expression: string): string {
+export function renderHighlightedLines(expression: string, places?: TranslationTable): string {
     if (!expression) return "";
 
-    const html = renderExpressionLines(getExpressionLines(expression));
+    const html = renderExpressionLines(getExpressionLines(expression), text => renderHighlightedContent(text, places));
     return `<pre class="lj-expression-block"><code class="lj-expression-code">${html}</code></pre>`;
 }
 
-export function renderHighlightedInlineExpression(expression: string): string {
-    return renderExpression(expression, false);
+/**
+ * Renders an expression inline, with its tokens colored
+ * @param places where the variables of the expression come from, by name
+ */
+export function renderHighlightedInlineExpression(expression: string, places?: TranslationTable): string {
+    return renderExpression(expression, false, places);
 }
diff --git a/client/src/webview/script.spec.ts b/client/src/webview/script.spec.ts
index 97ba956..247ee76 100644
--- a/client/src/webview/script.spec.ts
+++ b/client/src/webview/script.spec.ts
@@ -47,6 +47,7 @@ function context(file = currentFile): LJContext {
         visibleVars: [variable],
         allVars: [variable],
         fileScopes: {},
+        generatedPlaces: {},
     };
 }
 
diff --git a/client/src/webview/styles.ts b/client/src/webview/styles.ts
index 5c1e47d..88ddb27 100644
--- a/client/src/webview/styles.ts
+++ b/client/src/webview/styles.ts
@@ -399,6 +399,18 @@ export function getStyles(): string {
             color: var(--vscode-descriptionForeground);
             cursor: help;
         }
+        /* a name LiquidJava gives a value of the code, explained on hover */
+        .lj-generated-name {
+            text-decoration: underline dotted var(--vscode-descriptionForeground);
+            text-underline-offset: 2px;
+            cursor: help;
+        }
+        .lj-generated-name.location-link {
+            cursor: pointer;
+        }
+        .lj-generated-name.location-link:hover {
+            text-decoration-style: solid;
+        }
         .lj-expression,
         .lj-expression-code {
             font-family: var(--vscode-editor-font-family);
diff --git a/client/src/webview/views/context/context.spec.ts b/client/src/webview/views/context/context.spec.ts
index a0546bb..56def08 100644
--- a/client/src/webview/views/context/context.spec.ts
+++ b/client/src/webview/views/context/context.spec.ts
@@ -15,7 +15,7 @@ function ghost(name: string, file = currentFile, stateSet: string | null = null)
 function context(overrides: Partial<LJContext> = {}): LJContext {
     return {
         localVars: [], globalVars: [], ghosts: [], aliases: [], methods: [],
-        visibleVars: [], allVars: [], fileScopes: {}, ...overrides,
+        visibleVars: [], allVars: [], fileScopes: {}, generatedPlaces: {}, ...overrides,
     };
 }
 
@@ -50,6 +50,21 @@ describe('context view', () => {
         expect(document.querySelectorAll('.context-section-content.collapsed')).toHaveLength(0);
     });
 
+    it('links the names LiquidJava gives values of the code in refinements to their lines', () => {
+        document.body.innerHTML = renderContextView(context({
+            allVars: [{
+                name: 'a', displayName: 'a', internalName: 'a', type: 'int', refinement: 'a == #pos_result',
+                mainRefinement: '', position: null, annotationPosition: null,
+            }],
+            generatedPlaces: { '#pos_result': { text: 'pos(x)', position: { file: '/w/A.java', lineStart: 6, colStart: 16, lineEnd: 6, colEnd: 22 } } },
+        }), currentFile, sectionState);
+
+        const name = document.querySelector('#context-vars .lj-generated-name.location-link');
+        expect(name?.getAttribute('title')).toBe(
+            'The value returned by the call to pos() at line 7. LiquidJava gives it the name #pos_result. Click to go to it.');
+        expect([name?.getAttribute('data-file'), name?.getAttribute('data-line')]).toEqual(['/w/A.java', '6']);
+    });
+
     it('honors each section collapse state independently', () => {
         document.body.innerHTML = renderContextView(context({ ghosts: [ghost('size')] }), currentFile, {
             aliases: false, ghosts: true, vars: false,
diff --git a/client/src/webview/views/context/context.ts b/client/src/webview/views/context/context.ts
index 421de3b..4696f91 100644
--- a/client/src/webview/views/context/context.ts
+++ b/client/src/webview/views/context/context.ts
@@ -23,7 +23,7 @@ export function renderContextView(context: LJContext | undefined, currentFile: s
                 ? 'No context information available at the cursor position'
                 : `${renderContextAliases(aliases, sectionState.aliases)}
                    ${renderContextGhosts(ghosts, sectionState.ghosts)}
-                   ${renderContextVariables(allVars, sectionState.vars, errorAtCursor)}
+                   ${renderContextVariables(allVars, sectionState.vars, errorAtCursor, context?.generatedPlaces)}
             `}
         </div>
     `;
diff --git a/client/src/webview/views/context/variables.ts b/client/src/webview/views/context/variables.ts
index 75d4817..353d36b 100644
--- a/client/src/webview/views/context/variables.ts
+++ b/client/src/webview/views/context/variables.ts
@@ -1,10 +1,13 @@
 import { LJVariable } from "../../../types/context";
-import { RefinementMismatchError } from "../../../types/diagnostics";
+import { RefinementMismatchError, TranslationTable } from "../../../types/diagnostics";
 import { renderHighlightedInlineExpression, withoutLineTag } from "../../highlighting";
 import { escapeHtml, getSimpleName } from "../../utils";
 import { renderToggleSection, renderVariableHighlightButton, renderDiagnosticRevealButton } from "../sections";
 
-export function renderContextVariables(variables: LJVariable[], isExpanded: boolean, errorAtCursor?: RefinementMismatchError): string {
+/**
+ * @param generatedPlaces where each value the verifier introduces comes from, by name
+ */
+export function renderContextVariables(variables: LJVariable[], isExpanded: boolean, errorAtCursor?: RefinementMismatchError, generatedPlaces?: TranslationTable): string {
     const relevantNames = new Set(Object.keys(errorAtCursor?.translationTable || {}).map(withoutLineTag));
     return /*html*/`
         <div class="context-section">
@@ -28,7 +31,7 @@ export function renderContextVariables(variables: LJVariable[], isExpanded: bool
                                 return /*html*/`
                                 <tr class="${isRelevant ? 'context-variable-relevant' : ''}">
                                     <td>${renderVariableHighlightButton(variable)}</td>
-                                    <td><code>${renderHighlightedInlineExpression(variable.refinement)}</code></td>
+                                    <td><code>${renderHighlightedInlineExpression(variable.refinement, generatedPlaces)}</code></td>
                                 </tr>
                             `;}).join('')}
                             ${errorAtCursor ? renderFailingRefinement(errorAtCursor) : ''}
diff --git a/client/src/webview/views/diagnostics/counterexample.ts b/client/src/webview/views/diagnostics/counterexample.ts
index 904d14f..3e3e2a7 100644
--- a/client/src/webview/views/diagnostics/counterexample.ts
+++ b/client/src/webview/views/diagnostics/counterexample.ts
@@ -1,7 +1,7 @@
-import type { Counterexample } from "../../../types/diagnostics";
+import type { Counterexample, TranslationTable } from "../../../types/diagnostics";
 import { renderHighlightedInlineExpression } from "../../highlighting";
 
-export function renderCounterexample(counterexample: Counterexample): string {
+export function renderCounterexample(counterexample: Counterexample, translationTable?: TranslationTable): string {
     if (counterexample.assignments.length === 0) return "";
 
     return /*html*/`
@@ -10,7 +10,7 @@ export function renderCounterexample(counterexample: Counterexample): string {
                 ${counterexample.assignments.map(assignment => /*html*/`
                     <div class="counterexample-line">
                         <span class="vc-node">${renderHighlightedInlineExpression(
-                            `${assignment.variable} == ${assignment.value}`
+                            `${assignment.variable} == ${assignment.value}`, translationTable
                         )}</span>
                     </div>
                 `).join("")}
diff --git a/client/src/webview/views/diagnostics/errors.ts b/client/src/webview/views/diagnostics/errors.ts
index 2e423f6..93a1a1f 100644
--- a/client/src/webview/views/diagnostics/errors.ts
+++ b/client/src/webview/views/diagnostics/errors.ts
@@ -39,14 +39,14 @@ type ErrorRendererMap = { [E in LJError as E['type']]: (error: E) => string };
 
 const errorContentRenderers: ErrorRendererMap = {
     'refinement-error': (e: RefinementError) => /*html*/ `
-        ${renderCustomSection('Expected', renderHighlightedLines(e.expected))}
+        ${renderCustomSection('Expected', renderHighlightedLines(e.expected, e.translationTable))}
         ${renderCustomSection('Found', renderVCImplication(e, e.found))}
         ${e.counterexample.assignments.length > 0
-            ? renderCustomSection('Counterexample', renderCounterexample(e.counterexample))
+            ? renderCustomSection('Counterexample', renderCounterexample(e.counterexample, e.translationTable))
             : ''}
     `,
     'state-refinement-error': (e: StateRefinementError) => /*html*/ `
-        ${renderCustomSection('Expected', renderHighlightedLines(e.expected))}
+        ${renderCustomSection('Expected', renderHighlightedLines(e.expected, e.translationTable))}
         ${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 14a2d0c..da1769f 100644
--- a/client/src/webview/views/diagnostics/vc-changes.spec.ts
+++ b/client/src/webview/views/diagnostics/vc-changes.spec.ts
@@ -69,6 +69,34 @@ describe('verification implications', () => {
         expect(Array.from(document.querySelectorAll('.vc-change-fragment')).map(fragment => fragment.innerHTML))
             .toEqual([expect.stringMatching(/^<span [^>]*>x<\/span><sub [^>]*>l13<\/sub>$/)]);
     });
+    it('explains the names LiquidJava gives values of the code, linking each to its line when it is known', () => {
+        const at = (lineStart: number) => ({ text: '', position: { file: '/w/A.java', lineStart, colStart: 4, lineEnd: lineStart, colEnd: 9 } });
+        const table = { '#if_condition': at(9), '#size_result': at(14) };
+        const chain: VCImplication = {
+            name: '#if_condition', type: 'boolean', predicate: 'x > 0',
+            next: { ...conclusion, predicate: 'a == #size_result + #new_File + #case_condition@20#1 + #ret' },
+        };
+        const names = () => Array.from(document.querySelectorAll('.lj-generated-name'), name =>
+            [name.textContent, name.getAttribute('title'), name.getAttribute('data-line')]);
+
+        document.body.innerHTML = renderImplication(chain, table);
+        expect(document.querySelector('.vc-binder')?.getAttribute('title')).toBe(
+            'The condition of the if at line 10. LiquidJava gives it the name #if_condition. Click to go to it.');
+        expect(names()).toEqual([
+            ['#size_result', 'The value returned by the call to size() at line 15. LiquidJava gives it the name #size_result. Click to go to it.', '14'],
+            ['#new_File', 'The new File object created. LiquidJava gives it the name #new_File.', null],
+            ['#case_conditionl20#1', 'Whether the case at line 20 matches. LiquidJava gives it the name #case_condition.', null],
+        ]);
+
+        document.body.innerHTML = renderImplication({ ...chain, name: '#case_condition@74' });
+        expect(document.querySelector('.vc-binder')?.getAttribute('title')).toBe(
+            'Whether the case at line 74 matches. LiquidJava gives it the name #case_condition.');
+
+        document.body.innerHTML = renderImplicationChange(
+            { ...conclusion, predicate: 'a == x + y + z' }, { ...conclusion, predicate: 'a == x + y + #size_result' }, table,
+        );
+        expect(document.querySelector('.vc-change-fragment .lj-generated-name')?.getAttribute('data-line')).toBe('14');
+    });
     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 a3ec82e..c710958 100644
--- a/client/src/webview/views/diagnostics/vc-changes.ts
+++ b/client/src/webview/views/diagnostics/vc-changes.ts
@@ -2,9 +2,11 @@ import type { VCImplication } from "../../../types/vc-implications";
 import type { TranslationTable } from "../../../types/diagnostics";
 import {
     getExpressionLines, LINE_TAG, LITERAL, renderExpressionLines, renderHighlightedInlineExpression, renderLineTags,
+    lineOfTag, withoutLineTag,
 } from "../../highlighting";
 import { escapeHtml } from "../../utils";
 import { renderSourceHighlightButton } from "../sections";
+import { generatedNameTitle, isGeneratedName } from "../../generated-names";
 
 type ChangeKind = "unchanged" | "removed" | "added";
 type DiffOperation<T> = { kind: ChangeKind; value: T };
@@ -41,13 +43,16 @@ function getImplicationLines(node: VCImplication): string[] {
 
 function renderBinder(binder: string, type: string, translationTable?: TranslationTable): string {
     const placement = translationTable?.[binder.slice(1)];
-    if (!placement?.position?.file) {
-        return `<span class="vc-node vc-binder" title="${escapeHtml(type)}">${renderLineTags(binder)}</span>`;
+    const position = placement?.position;
+    const name = withoutLineTag(binder.slice(1));
+    const explanation = isGeneratedName(name) ? generatedNameTitle(name, position, lineOfTag(binder)) : "";
+    if (!position?.file) {
+        return `<span class="vc-node vc-binder" title="${escapeHtml(explanation || type)}">${renderLineTags(binder)}</span>`;
     }
     return renderSourceHighlightButton(
         renderLineTags(binder),
-        type ? `Go to source (${type})` : "Go to source",
-        placement.position,
+        explanation || (type ? `Go to source (${type})` : "Go to source"),
+        position,
         "vc-node vc-binder clickable",
     );
 }
@@ -63,11 +68,12 @@ export function renderVCLine(
     translationTable?: TranslationTable,
 ): string {
     const { binder, type, predicate, hasNext } = parseImplicationLine(line);
+    const renderPredicateLine = renderText ?? (text => renderHighlightedInlineExpression(text, translationTable));
     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">${renderExpressionLines(getExpressionLines(predicate), renderText, arrow)}</span></div>
+            <div class="vc-predicate-cell"><span class="vc-node">${renderExpressionLines(getExpressionLines(predicate), renderPredicateLine, arrow)}</span></div>
         </div>
     `;
 }
@@ -112,11 +118,15 @@ function tokenizeExpression(expression: string): string[] {
     return expression.match(TOKEN_PATTERN) || [];
 }
 
-function renderChangedFragment(content: string): string {
-    return `<span class="vc-change-fragment">${renderHighlightedInlineExpression(content)}</span>`;
+function renderChangedFragment(content: string, translationTable?: TranslationTable): string {
+    return `<span class="vc-change-fragment">${renderHighlightedInlineExpression(content, translationTable)}</span>`;
 }
 
-function renderDestinationTokenDiff(before: string, after: string): { content: string; hasAddedContent: boolean } {
+function renderDestinationTokenDiff(
+    before: string,
+    after: string,
+    translationTable?: TranslationTable,
+): { content: string; hasAddedContent: boolean } {
     const operations = diffSequence(tokenizeExpression(before), tokenizeExpression(after));
     let html = "";
     let changedContent = "";
@@ -126,7 +136,7 @@ function renderDestinationTokenDiff(before: string, after: string): { content: s
         if (!changedContent) return;
         const trailingWhitespace = changedContent.match(/\s+$/u)?.[0] ?? "";
         const content = changedContent.slice(0, changedContent.length - trailingWhitespace.length);
-        if (content) html += renderChangedFragment(content);
+        if (content) html += renderChangedFragment(content, translationTable);
         html += trailingWhitespace;
         changedContent = "";
     };
@@ -143,7 +153,7 @@ function renderDestinationTokenDiff(before: string, after: string): { content: s
                 return;
             }
             flushChangedContent();
-            html += renderHighlightedInlineExpression(operation.value);
+            html += renderHighlightedInlineExpression(operation.value, translationTable);
         }
     });
     flushChangedContent();
@@ -197,14 +207,14 @@ function alignChangedLines(removed: string[], added: string[]): Array<[string |
 }
 
 // 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[] {
+function renderChangedPredicateLines(before: string, after: string, translationTable?: TranslationTable): 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];
+                ? renderChangedFragment(afterLine, translationTable)
+                : renderDestinationTokenDiff(beforeLine, afterLine, translationTable).content];
         });
 }
 
@@ -222,7 +232,7 @@ function renderChangedDestinationLines(
             const beforePredicate = parseImplicationLine(before).predicate;
             const afterPredicate = parseImplicationLine(after).predicate;
             const change = renderDestinationTokenDiff(beforePredicate, afterPredicate);
-            const lines = renderChangedPredicateLines(beforePredicate, afterPredicate);
+            const lines = renderChangedPredicateLines(beforePredicate, afterPredicate, translationTable);
             return renderVCLine(
                 after,
                 change.hasAddedContent ? "" : "vc-change-line",
diff --git a/server/src/main/java/dtos/context/ContextHistoryDTO.java b/server/src/main/java/dtos/context/ContextHistoryDTO.java
index 19debbd..3327b7a 100644
--- a/server/src/main/java/dtos/context/ContextHistoryDTO.java
+++ b/server/src/main/java/dtos/context/ContextHistoryDTO.java
@@ -3,6 +3,7 @@
 import java.util.List;
 import java.util.Map;
 
+import dtos.diagnostics.PlacementInCodeDTO;
 import dtos.diagnostics.SourcePositionDTO;
 import spoon.reflect.reference.CtTypeReference;
 
@@ -15,7 +16,9 @@ public record ContextHistoryDTO(
     List<GhostDTO> ghosts,
     List<AliasDTO> aliases,
     List<MethodDTO> methods,
-    Map<String, List<SourcePositionDTO>> fileScopes
+    Map<String, List<SourcePositionDTO>> fileScopes,
+    // where each value the verifier introduces, such as #if_condition, comes from, by the name the context shows it with
+    Map<String, PlacementInCodeDTO> generatedPlaces
 ) {
     public static String stringifyType(CtTypeReference<?> typeReference) {
         if (typeReference == null)
diff --git a/server/src/main/java/utils/ContextHistoryConverter.java b/server/src/main/java/utils/ContextHistoryConverter.java
index 1685aba..e65ad19 100644
--- a/server/src/main/java/utils/ContextHistoryConverter.java
+++ b/server/src/main/java/utils/ContextHistoryConverter.java
@@ -6,6 +6,7 @@
 import java.util.Map;
 import java.util.Set;
 import java.util.stream.Collectors;
+import java.util.stream.Stream;
 
 import dtos.context.AliasDTO;
 import dtos.context.ContextDisplay;
@@ -13,6 +14,7 @@
 import dtos.context.MethodDTO;
 import dtos.context.GhostDTO;
 import dtos.context.VariableDTO;
+import dtos.diagnostics.PlacementInCodeDTO;
 import dtos.diagnostics.SourcePositionDTO;
 import liquidjava.processor.context.ContextHistory;
 import liquidjava.processor.context.GhostFunction;
@@ -47,7 +49,8 @@ public static ContextHistoryDTO convertToDTO(ContextHistory contextHistory) {
             contextHistory.getGhosts().stream().sorted(GHOST_ORDER).map(GhostDTO::from).collect(Collectors.toList()),
             contextHistory.getAliases().stream().map(AliasDTO::from).collect(Collectors.toList()),
             contextHistory.getMethods().stream().map(MethodDTO::from).filter(f -> f != null).collect(Collectors.toList()),
-            parseFileScopes(contextHistory.getFileScopes())
+            parseFileScopes(contextHistory.getFileScopes()),
+            convertGeneratedPlaces(contextHistory, display)
         );
     }
 
@@ -72,6 +75,15 @@ private static List<VariableDTO> convertVariables(Set<RefinedVariable> variables
             .collect(Collectors.toList());
     }
 
+    // where each value the verifier introduces comes from, by the name the context shows it with
+    private static Map<String, PlacementInCodeDTO> convertGeneratedPlaces(ContextHistory history, ContextDisplay display) {
+        Map<String, PlacementInCodeDTO> places = new HashMap<>();
+        Stream.concat(history.getLocalVars().stream(), history.getGlobalVars().stream())
+            .filter(v -> GeneratedNames.isGenerated(v.getName()) && v.getPlacementInCode() != null)
+            .forEach(v -> places.put(display.name(v.getName()), PlacementInCodeDTO.from(v.getPlacementInCode())));
+        return places;
+    }
+
     private static Map<String, List<SourcePositionDTO>> parseFileScopes(Map<String, Set<String>> fileScopes) {
         return fileScopes.entrySet().stream().collect(Collectors.toMap(
             Map.Entry::getKey,
diff --git a/server/src/test/java/utils/ContextHistoryConverterTest.java b/server/src/test/java/utils/ContextHistoryConverterTest.java
index b44d55b..f5bf9a6 100644
--- a/server/src/test/java/utils/ContextHistoryConverterTest.java
+++ b/server/src/test/java/utils/ContextHistoryConverterTest.java
@@ -15,6 +15,7 @@
 import dtos.context.ContextHistoryDTO;
 import dtos.context.GhostDTO;
 import dtos.context.VariableDTO;
+import dtos.diagnostics.PlacementInCodeDTO;
 import dtos.diagnostics.SourcePositionDTO;
 import liquidjava.api.CommandLineLauncher;
 import liquidjava.processor.context.ContextHistory;
@@ -88,6 +89,13 @@ void showsVariablesAsErrorMessagesDo() {
         assertTrue(variables.stream().noneMatch(v -> v.displayName().startsWith("#")), refinements.toString());
     }
 
+    @Test
+    void sendsWhereTheValuesTheVerifierIntroducesComeFrom() {
+        PlacementInCodeDTO length = verify(DOOR).generatedPlaces().get("#array_length");
+        assertEquals("2", length.text());
+        assertEquals(13, length.position().lineStart()); // new int[2], from line zero
+    }
+
     @Test
     void showsTheStatesOfANamedSetAsValuesOfTheSet() {
         List<GhostDTO> ghosts = verify(DOOR).ghosts();