diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
index 6f1070c7ddea..aea10c4911f8 100644
--- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
+++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala
@@ -461,10 +461,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser:
    */
   def consumeError(ref: Capability, loc: (SrcPos, TypeRole), pos: SrcPos)(using Context): Unit =
     val (locPos, role) = loc
-    report.error(
-      em"""Separation failure: Illegal access to $ref, which was ${role.howConsumed}
-          |on line ${locPos.line + 1} and therefore is no longer available.""",
-      pos)
+    report.error(reporting.UseAfterConsume(ref, locPos.sourcePos, pos.sourcePos, role.howConsumed), pos)
 
   /** Report a failure where a capability is consumed in a loop.
    *  @param ref     the capability
diff --git a/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala b/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala
index a4c30b4658e9..807185106d01 100644
--- a/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/Diagnostic.scala
@@ -117,6 +117,6 @@ class Diagnostic(
     msg.message.replaceAll("\u001B\\[[;\\d]*m", "")
   override def diagnosticRelatedInformation: JList[interfaces.DiagnosticRelatedInformation] =
     Collections.emptyList()
-
   override def toString: String = s"$getClass at $pos L${pos.line+1}: $message"
 end Diagnostic
+
diff --git a/compiler/src/dotty/tools/dotc/reporting/Message.scala b/compiler/src/dotty/tools/dotc/reporting/Message.scala
index 1c71b7468c0b..1a542ca0dbdd 100644
--- a/compiler/src/dotty/tools/dotc/reporting/Message.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/Message.scala
@@ -300,6 +300,13 @@ object Message:
       super.toText(sym)
   end Printer
 
+  /** A part of a multi-span message, associating text with a source position.
+   *  @param text       the message text for this part
+   *  @param srcPos     the source position where this part applies
+   *  @param isPrimary  whether this is the primary message (true) or a secondary note (false)
+   */
+  case class MessagePart(text: String, srcPos: util.SourcePosition, isPrimary: Boolean)
+
 end Message
 
 /** A `Message` contains all semantic information necessary to easily
@@ -370,6 +377,17 @@ abstract class Message(val errorId: ErrorMessageID)(using Context) { self =>
     */
   protected def explain(using Context): String
 
+  /** Optional leading text to be displayed before the source snippet.
+    * If present along with parts, triggers multi-span rendering.
+    */
+  def leading(using Context): Option[String] = None
+
+  /** Optional list of message parts for multi-span error messages.
+    * Each part associates text with a source position and indicates
+    * whether it's a primary message or a secondary note.
+    */
+  def parts(using Context): List[MessagePart] = Nil
+
   /** What gets printed after the message proper */
   protected def msgPostscript(using Context): String =
     if ctx eq NoContext then ""
diff --git a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
index 9366050a5a17..42a8659c852e 100644
--- a/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/MessageRendering.scala
@@ -12,7 +12,7 @@ import io.AbstractFile
 import printing.Highlighting.{Blue, Red, Yellow}
 import printing.SyntaxHighlighting
 import Diagnostic.*
-import util.{SourcePosition, NoSourcePosition}
+import util.{SourceFile, SourcePosition, NoSourcePosition}
 import util.Chars.{ LF, CR, FF, SU }
 import scala.annotation.switch
 
@@ -77,24 +77,32 @@ trait MessageRendering {
    *  -- Error: source.scala ---------------------
    *  ```
    */
-  private def boxTitle(title: String)(using Context, Level, Offset): String =
+  private def boxTitle(title: String, isSubtitle: Boolean = false)(using Context, Level, Offset): String =
     val pageWidth = ctx.settings.pageWidth.value
     val line = "-" * (pageWidth - title.length - 4)
-    hl(s"-- $title $line")
+    val starter = if isSubtitle then ".." else "--"
+    hl(s"$starter $title $line")
 
   /** The position markers aligned under the error
    *
    *  ```
    *    |         ^^^^^
    *  ```
+   *  or for sub-diagnostics:
+   *  ```
+   *    |         -----
+   *  ```
+   *
+   *  @param pos the source position to mark
+   *  @param markerChar the character to use for marking ('^' for primary errors, '-' for notes)
    */
-  private def positionMarker(pos: SourcePosition)(using Context, Level, Offset): String = {
+  private def positionMarker(pos: SourcePosition, markerChar: Char = '^')(using Context, Level, Offset): String = {
     val padding = pos.startColumnPadding
-    val carets =
+    val markers =
       if (pos.startLine == pos.endLine)
-        "^" * math.max(1, pos.endColumn - pos.startColumn)
-      else "^"
-    hl(s"$offsetBox$padding$carets")
+        markerChar.toString * math.max(1, pos.endColumn - pos.startColumn)
+      else markerChar.toString
+    hl(s"$offsetBox$padding$markers")
   }
 
   /** The horizontal line with the given offset
@@ -169,7 +177,8 @@ trait MessageRendering {
   private def posStr(
     pos: SourcePosition,
     message: Message,
-    diagnosticString: String
+    diagnosticString: String,
+    isSubdiag: Boolean = false
   )(using Context, Level, Offset): String =
     assert(
       message.errorId.isActive,
@@ -191,7 +200,7 @@ trait MessageRendering {
         val title =
           if fileAndPos.isEmpty then s"$errId$kind:" // this happens in dotty.tools.repl.ScriptedTests // TODO add name of source or remove `:` (and update test files)
           else s"$errId$kind: $fileAndPos"
-        boxTitle(title)
+        boxTitle(title, isSubtitle = isSubdiag)
       })
     else ""
   end posStr
@@ -232,6 +241,201 @@ trait MessageRendering {
     if origin.nonEmpty then
       addHelp("origin=")(origin)
 
+  // adjust a pos at EOF if preceded by newline
+  private def adjust(pos: SourcePosition): SourcePosition =
+    if pos.span.isSynthetic
+    && pos.span.isZeroExtent
+    && pos.span.exists
+    && pos.span.start == pos.source.length
+    && pos.source(pos.span.start - 1) == '\n'
+    then
+    pos.withSpan(pos.span.shift(-1))
+    else
+    pos
+
+  /** Render parts for a single source file.
+   *  @param parts the message parts to render (all must be from the same source)
+   *  @param sb the StringBuilder to append to
+   */
+  private def renderPartsForFile(
+    parts: List[Message.MessagePart],
+    sb: StringBuilder
+  )(using Context, Level, Offset): Unit =
+    if parts.isEmpty then return
+
+    val source = parts.head.srcPos.source
+
+    // Find the line range covering all positions
+    val minLine = parts.map(_.srcPos.startLine).min
+    val maxLine = parts.map(_.srcPos.endLine).max
+
+    // Render the unified code snippet
+    val startOffset = source.lineToOffset(minLine)
+    val endOffset = source.nextLine(source.lineToOffset(maxLine))
+    val content = source.content.slice(startOffset, endOffset)
+    val syntax =
+      if (summon[Context].settings.color.value != "never" && !summon[Context].isJava)
+        SyntaxHighlighting.highlight(new String(content)).toCharArray
+      else content
+
+    // Split syntax-highlighted content into lines
+    def linesFrom(arr: Array[Char]): List[String] = {
+      def pred(c: Char) = (c: @switch) match {
+        case LF | CR | FF | SU => true
+        case _ => false
+      }
+      val (line, rest0) = arr.span(!pred(_))
+      // Only consume one line terminator (CRLF counts as one)
+      val rest =
+        if rest0.isEmpty then rest0
+        else if rest0(0) == CR && rest0.length > 1 && rest0(1) == LF then rest0.drop(2)
+        else rest0.drop(1)
+      new String(line) :: { if rest.isEmpty then Nil else linesFrom(rest) }
+    }
+
+    val lines = linesFrom(syntax)
+    val maxLineNumber = maxLine + 1
+    val lineNumberWidth = maxLineNumber.toString.length
+
+    // Render each line with its markers and messages
+    for (lineNum <- minLine to maxLine) do
+      val lineIdx = lineNum - minLine
+      if lineIdx < lines.length then
+        val lineContent = lines(lineIdx)
+        val lineNbr = (lineNum + 1).toString
+        val linePrefix = String.format(s"%${lineNumberWidth}s |", lineNbr)
+        val lnum = hl(" " * math.max(0, offset - linePrefix.length - 1) + linePrefix)
+        sb.append(lnum).append(lineContent.stripLineEnd).append(EOL)
+
+        // Find all positions that should show markers after this line
+        val partsOnLine = parts.filter(_.srcPos.startLine == lineNum)
+          .sortBy(p => (p.srcPos.startColumn, !p.isPrimary))
+
+        if partsOnLine.size == 1 then
+          // Single marker on this line
+          val part = partsOnLine.head
+          val markerChar = if part.isPrimary then '^' else '-'
+          val marker = positionMarker(part.srcPos, markerChar)
+          val err = errorMsg(part.srcPos, part.text)
+          sb.append(marker).append(EOL)
+          sb.append(err).append(EOL)
+        else if partsOnLine.size > 1 then
+          // Multiple markers on same line
+          val markerLine = StringBuilder()
+          markerLine.append(offsetBox)
+
+          var currentCol = 0
+          for part <- partsOnLine do
+            val markerChar = if part.isPrimary then '^' else '-'
+            val targetCol = part.srcPos.startColumn
+            val padding = " " * (targetCol - currentCol)
+            markerLine.append(padding).append(markerChar)
+            currentCol = targetCol + 1
+
+          sb.append(markerLine).append(EOL)
+
+          // Render messages from right to left with connector bars
+          val sortedByColumn = partsOnLine.reverse // rightmost first
+          for (part, idx) <- sortedByColumn.zipWithIndex do
+            val remainingParts = sortedByColumn.drop(idx + 1) // parts still waiting for messages
+
+            // Build connector line with vertical bars for remaining parts
+            val connectorLine = StringBuilder()
+            connectorLine.append(offsetBox)
+
+            var col = 0
+            // First, add vertical bars for all remaining (not-yet-shown) parts
+            for p <- partsOnLine do
+              if remainingParts.contains(p) then
+                val targetCol = p.srcPos.startColumn
+                val padding = " " * (targetCol - col)
+                connectorLine.append(padding).append("|")
+                col = targetCol + 1
+
+            // Then add the message for the current part, aligned to its column
+            val msgText = part.text
+            val msgCol = part.srcPos.startColumn
+            // If we've added bars, col is position after last bar; if not, col is 0
+            // We want the message to start at msgCol, with at least one space separation
+            val msgPadding = if col == 0 then " " * msgCol else " " * Math.max(1, msgCol - col)
+            connectorLine.append(msgPadding).append(msgText)
+
+            sb.append(connectorLine).append(EOL)
+  end renderPartsForFile
+
+  /** Group consecutive parts by their source file. */
+  private def groupPartsByFile(parts: List[Message.MessagePart]): List[(SourceFile, List[Message.MessagePart])] =
+    if parts.isEmpty then Nil
+    else
+      val head = parts.head
+      val source = head.srcPos.source
+      val (sameSrc, rest) = parts.span(_.srcPos.source == source)
+      (source, sameSrc) :: groupPartsByFile(rest)
+
+  /** Render a message using multi-span information from Message.parts. */
+  def messageAndPosFromParts(dia: Diagnostic)(using Context): String =
+    val msg = dia.msg
+    val pos = dia.pos
+    val pos1 = adjust(pos.nonInlined)
+    val msgParts = msg.parts
+
+    if msgParts.isEmpty then
+      return msg.leading.getOrElse("") + (if msg.leading.isDefined then "\n" else "") + msg.message
+
+    // Collect all positions from message parts
+    val validParts = msgParts.filter(p => p.srcPos.exists && p.srcPos.source.file.exists)
+
+    if validParts.isEmpty then
+      return msg.leading.map(_ + "\n").getOrElse("") + msg.message
+
+    // Group parts by consecutive source files
+    val groupedParts = groupPartsByFile(validParts)
+
+    // Calculate the maximum line number across all files for consistent offset
+    val maxLineNumber = validParts.map(_.srcPos.endLine).max + 1
+
+    given Level = Level(dia.level)
+    given Offset = Offset(maxLineNumber.toString.length + 2)
+
+    val sb = StringBuilder()
+
+    // Title using the primary position
+    val posString = posStr(pos1, msg, diagnosticLevel(dia))
+    if posString.nonEmpty then sb.append(posString).append(EOL)
+
+    // Display leading text if present
+    msg.leading.foreach { leadingText =>
+      sb.append(leadingText)
+      if !leadingText.endsWith(EOL) then sb.append(EOL)
+    }
+
+    // Track the current file
+    // When starting, we set it to the file of the diagnostic
+    var currentFile: SourceFile = pos1.source
+
+    // Render each group of parts
+    for (source, parts) <- groupedParts do
+      // Add a file indicator line when switching to a different file
+      if source != currentFile then
+        sb.append("... ").append(renderPath(source.file)).append(EOL)
+        currentFile = source
+      renderPartsForFile(parts, sb)
+
+    // Add explanation if needed
+    if Diagnostic.shouldExplain(dia) then
+      sb.append(newBox())
+      sb.append(EOL).append(offsetBox).append(" Explanation (enabled by `-explain`)")
+      sb.append(EOL).append(newBox(soft = true))
+      dia.msg.explanation.split(raw"\R").foreach: line =>
+        sb.append(EOL).append(offsetBox).append(if line.isEmpty then "" else " ").append(line)
+      sb.append(EOL).append(endBox)
+    else if dia.msg.canExplain then
+      sb.append(offsetBox)
+      sb.append(EOL).append(offsetBox).append(" longer explanation available when compiling with `-explain`")
+
+    sb.toString
+  end messageAndPosFromParts
+
   /** The whole message rendered from `dia.msg`.
    *
    *  For a position in an inline expansion, choose `pos1`
@@ -252,65 +456,59 @@ trait MessageRendering {
    *
    */
   def messageAndPos(dia: Diagnostic)(using Context): String =
-    // adjust a pos at EOF if preceded by newline
-    def adjust(pos: SourcePosition): SourcePosition =
-      if pos.span.isSynthetic
-      && pos.span.isZeroExtent
-      && pos.span.exists
-      && pos.span.start == pos.source.length
-      && pos.source(pos.span.start - 1) == '\n'
-      then
-        pos.withSpan(pos.span.shift(-1))
-      else
-        pos
     val msg = dia.msg
-    val pos = dia.pos
-    val pos1 = adjust(pos.nonInlined) // innermost pos contained by call.pos
-    val outermost = pos.outermost // call.pos
-    val inlineStack = pos.inlinePosStack.filterNot(outermost.contains(_))
-    given Level = Level(dia.level)
-    given Offset =
-      val maxLineNumber =
-        if pos.exists then (pos1 :: inlineStack).map(_.endLine).max + 1
-        else 0
-      Offset(maxLineNumber.toString.length + 2)
-    val sb = StringBuilder()
-    val posString = posStr(pos1, msg, diagnosticLevel(dia))
-    if posString.nonEmpty then sb.append(posString).append(EOL)
-    if pos.exists && pos1.exists && pos1.source.file.exists then
-      val (srcBefore, srcAfter, offset) = sourceLines(pos1)
-      val marker = positionMarker(pos1)
-      val err = errorMsg(pos1, msg.message)
-      sb.append((srcBefore ::: marker :: err :: srcAfter).mkString(EOL))
-
-      if inlineStack.nonEmpty then
+    // Check if message provides its own multi-span structure
+    if msg.leading.isDefined || msg.parts.nonEmpty then
+      messageAndPosFromParts(dia)
+    else
+      val pos = dia.pos
+      val pos1 = adjust(pos.nonInlined) // innermost pos contained by call.pos
+      val outermost = pos.outermost // call.pos
+      val inlineStack = pos.inlinePosStack.filterNot(outermost.contains(_))
+      given Level = Level(dia.level)
+      given Offset =
+        val maxLineNumber =
+          if pos.exists then (pos1 :: inlineStack).map(_.endLine).max + 1
+          else 0
+        Offset(maxLineNumber.toString.length + 2)
+      val sb = StringBuilder()
+      val posString = posStr(pos1, msg, diagnosticLevel(dia))
+      if posString.nonEmpty then sb.append(posString).append(EOL)
+      if pos.exists && pos1.exists && pos1.source.file.exists then
+        val (srcBefore, srcAfter, offset) = sourceLines(pos1)
+        val marker = positionMarker(pos1)
+        val err = errorMsg(pos1, msg.message)
+        sb.append((srcBefore ::: marker :: err :: srcAfter).mkString(EOL))
+
+        if inlineStack.nonEmpty then
+          sb.append(EOL).append(newBox())
+          sb.append(EOL).append(offsetBox).append(i"Inline stack trace")
+          for inlinedPos <- inlineStack do
+            sb.append(EOL).append(newBox(soft = true))
+            sb.append(EOL).append(offsetBox).append(i"This location contains code that was inlined from $pos")
+            if inlinedPos.source.file.exists then
+              val (srcBefore, srcAfter, _) = sourceLines(inlinedPos)
+              val marker = positionMarker(inlinedPos)
+              sb.append(EOL).append((srcBefore ::: marker :: srcAfter).mkString(EOL))
+          sb.append(EOL).append(endBox)
+        end if
+      else sb.append(msg.message)
+
+      if dia.isVerbose then
+        appendFilterHelp(dia, sb)
+
+      if Diagnostic.shouldExplain(dia) then
         sb.append(EOL).append(newBox())
-        sb.append(EOL).append(offsetBox).append(i"Inline stack trace")
-        for inlinedPos <- inlineStack do
-          sb.append(EOL).append(newBox(soft = true))
-          sb.append(EOL).append(offsetBox).append(i"This location contains code that was inlined from $pos")
-          if inlinedPos.source.file.exists then
-            val (srcBefore, srcAfter, _) = sourceLines(inlinedPos)
-            val marker = positionMarker(inlinedPos)
-            sb.append(EOL).append((srcBefore ::: marker :: srcAfter).mkString(EOL))
+        sb.append(EOL).append(offsetBox).append(" Explanation (enabled by `-explain`)")
+        sb.append(EOL).append(newBox(soft = true))
+        dia.msg.explanation.split(raw"\R").foreach: line =>
+          sb.append(EOL).append(offsetBox).append(if line.isEmpty then "" else " ").append(line)
         sb.append(EOL).append(endBox)
-      end if
-    else sb.append(msg.message)
-    if dia.isVerbose then
-      appendFilterHelp(dia, sb)
+      else if dia.msg.canExplain then
+        sb.append(EOL).append(offsetBox)
+        sb.append(EOL).append(offsetBox).append(" longer explanation available when compiling with `-explain`")
 
-    if Diagnostic.shouldExplain(dia) then
-      sb.append(EOL).append(newBox())
-      sb.append(EOL).append(offsetBox).append(" Explanation (enabled by `-explain`)")
-      sb.append(EOL).append(newBox(soft = true))
-      dia.msg.explanation.split(raw"\R").foreach: line =>
-        sb.append(EOL).append(offsetBox).append(if line.isEmpty then "" else " ").append(line)
-      sb.append(EOL).append(endBox)
-    else if dia.msg.canExplain then
-      sb.append(EOL).append(offsetBox)
-      sb.append(EOL).append(offsetBox).append(" longer explanation available when compiling with `-explain`")
-
-    sb.toString
+      sb.toString
   end messageAndPos
 
   private def hl(str: String)(using Context, Level): String =
diff --git a/compiler/src/dotty/tools/dotc/reporting/messages.scala b/compiler/src/dotty/tools/dotc/reporting/messages.scala
index 159b3c9a905e..86ce1dda58ab 100644
--- a/compiler/src/dotty/tools/dotc/reporting/messages.scala
+++ b/compiler/src/dotty/tools/dotc/reporting/messages.scala
@@ -1212,6 +1212,30 @@ extends DeclarationMsg(OverrideErrorID), NoDisambiguation:
   def explain(using Context) =
     if canExplain then err.whyNoMatchStr(memberTp, otherTp) else ""
 
+  /** Whether the overridden symbol has a valid source position */
+  private def otherHasValidPos(using Context): Boolean =
+    val otherPos = other.sourcePos
+    otherPos.exists && otherPos.source.file.exists
+
+  override def leading(using Context): Option[String] =
+    if otherHasValidPos then Some(message) else None
+
+  override def parts(using Context): List[Message.MessagePart] =
+    if otherHasValidPos then
+      List(
+        Message.MessagePart(
+          i"the overridden ${other.showKind} is here",
+          other.sourcePos,
+          isPrimary = false
+        ),
+        Message.MessagePart(
+          i"the overriding ${member.showKind} $core",
+          member.sourcePos,
+          isPrimary = true
+        )
+      )
+    else Nil
+
 class ForwardReferenceExtendsOverDefinition(value: Symbol, definition: Symbol)(using Context)
 extends ReferenceMsg(ForwardReferenceExtendsOverDefinitionID) {
   extension (sym: Symbol) def srcLine = sym.line + 1
@@ -3749,3 +3773,27 @@ final class EncodedPackageName(name: Name)(using Context) extends SyntaxMsg(Enco
        |or `myfile-test.scala` can produce encoded names for the generated package objects.
        |
        |In this case, the name `$name` is encoded as `${name.encode}`."""
+
+class UseAfterConsume(ref: cc.Capabilities.Capability, consumedLoc: SourcePosition, useLoc: SourcePosition, howConsumed: => String)(using Context) extends Message(NoExplanationID):
+  def kind = MessageKind.NoKind
+
+  protected def msg(using Context): String =
+    i"""Separation failure: Illegal access to $ref, which was $howConsumed
+       |and therefore is no longer available."""
+
+  protected def explain(using Context): String = ""
+
+  override def leading(using Context): Option[String] = Some(message)
+
+  override def parts(using Context): List[Message.MessagePart] = List(
+    Message.MessagePart(
+      "The capability was consumed here.",
+      consumedLoc,
+      isPrimary = false
+    ),
+    Message.MessagePart(
+      "Then, it was used here",
+      useLoc,
+      isPrimary = true
+    )
+  )
diff --git a/tests/neg-custom-args/captures/consume-in-constructor.check b/tests/neg-custom-args/captures/consume-in-constructor.check
index 4937bf7fc6e4..4fb2a49a8e87 100644
--- a/tests/neg-custom-args/captures/consume-in-constructor.check
+++ b/tests/neg-custom-args/captures/consume-in-constructor.check
@@ -1,19 +1,32 @@
 -- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:20:10 --------------------------------------------
+Separation failure: Illegal access to (b : B^), which was passed as a consume parameter to constructor of class A2
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of value b
+18 |  val a2 = A2(b)
+   |              -
+   |              The capability was consumed here.
+19 |  val _: A2^{cap, b} = a2
 20 |  println(b) // error
    |          ^
-   |Separation failure: Illegal access to (b : B^), which was passed as a consume parameter to constructor of class A2
-   |on line 18 and therefore is no longer available.
-   |
-   |where:    ^ refers to a fresh root capability in the type of value b
+   |          Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:21:10 --------------------------------------------
+Separation failure: Illegal access to (a1 : A1{val b: B^{b²}}^{cap, b²}), which was passed as a consume parameter to constructor of class A2
+and therefore is no longer available.
+
+where:    b   is a value in class A1
+          b²  is a value in method Test
+          cap is a fresh root capability in the type of value a1
+18 |  val a2 = A2(b)
+   |              -
+   |              The capability was consumed here.
+19 |  val _: A2^{cap, b} = a2
+20 |  println(b) // error
 21 |  println(a1) // error, since `b` was consumed before
    |          ^^
-   |Separation failure: Illegal access to (a1 : A1{val b: B^{b²}}^{cap, b²}), which was passed as a consume parameter to constructor of class A2
-   |on line 18 and therefore is no longer available.
-   |
-   |where:    b   is a value in class A1
-   |          b²  is a value in method Test
-   |          cap is a fresh root capability in the type of value a1
+   |          Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/consume-in-constructor.scala:27:10 --------------------------------------------
 27 |  println(b) // error, b is hidden in the type of a1
    |          ^
diff --git a/tests/neg-custom-args/captures/consume-twice-same-line.check b/tests/neg-custom-args/captures/consume-twice-same-line.check
new file mode 100644
index 000000000000..2617e42d538a
--- /dev/null
+++ b/tests/neg-custom-args/captures/consume-twice-same-line.check
@@ -0,0 +1,30 @@
+-- Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:5:16 --------------------------------------------
+Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of parameter x
+5 |  send(x); send(x)  // error
+  |       -        ^
+  |       |        Then, it was used here
+  |       The capability was consumed here.
+
+-- Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:8:16 --------------------------------------------
+Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of parameter x
+8 |  send(x); send(x); send(x)  // error // error
+  |       -        ^
+  |       |        Then, it was used here
+  |       The capability was consumed here.
+
+-- Error: tests/neg-custom-args/captures/consume-twice-same-line.scala:8:25 --------------------------------------------
+Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of parameter x
+8 |  send(x); send(x); send(x)  // error // error
+  |       -                 ^
+  |       |                 Then, it was used here
+  |       The capability was consumed here.
+
diff --git a/tests/neg-custom-args/captures/consume-twice-same-line.scala b/tests/neg-custom-args/captures/consume-twice-same-line.scala
new file mode 100644
index 000000000000..858786419e16
--- /dev/null
+++ b/tests/neg-custom-args/captures/consume-twice-same-line.scala
@@ -0,0 +1,8 @@
+import language.experimental.captureChecking
+import language.experimental.separationChecking
+def send(consume x: Object^): Unit = ()
+def consumeTwice(consume x: Object^): Unit =
+  send(x); send(x)  // error
+
+def consumeThrice(consume x: Object^): Unit =
+  send(x); send(x); send(x)  // error // error
diff --git a/tests/neg-custom-args/captures/consume-twice.check b/tests/neg-custom-args/captures/consume-twice.check
new file mode 100644
index 000000000000..1fd11b4f6c83
--- /dev/null
+++ b/tests/neg-custom-args/captures/consume-twice.check
@@ -0,0 +1,12 @@
+-- Error: tests/neg-custom-args/captures/consume-twice.scala:6:7 -------------------------------------------------------
+Separation failure: Illegal access to (x : Object^), which was passed as a consume parameter to method send
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of parameter x
+5 |  send(x)
+  |       -
+  |       The capability was consumed here.
+6 |  send(x)  // error
+  |       ^
+  |       Then, it was used here
+
diff --git a/tests/neg-custom-args/captures/consume-twice.scala b/tests/neg-custom-args/captures/consume-twice.scala
new file mode 100644
index 000000000000..b0f955e9dbf7
--- /dev/null
+++ b/tests/neg-custom-args/captures/consume-twice.scala
@@ -0,0 +1,6 @@
+import language.experimental.captureChecking
+import language.experimental.separationChecking
+def send(consume x: Object^): Unit = ()
+def consumeTwice(consume x: Object^): Unit =
+  send(x)
+  send(x)  // error
diff --git a/tests/neg-custom-args/captures/i24373.check b/tests/neg-custom-args/captures/i24373.check
index 08e196fc1dc9..497749b42b24 100644
--- a/tests/neg-custom-args/captures/i24373.check
+++ b/tests/neg-custom-args/captures/i24373.check
@@ -1,21 +1,36 @@
 -- Error: tests/neg-custom-args/captures/i24373.scala:28:2 -------------------------------------------------------------
+Separation failure: Illegal access to (x1 : Foo^), which was used as a prefix to consume method sink1
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of value x1
+27 |  x1.sink1
+   |  --
+   |  The capability was consumed here.
 28 |  x1.sink1 // error
    |  ^^
-   |  Separation failure: Illegal access to (x1 : Foo^), which was used as a prefix to consume method sink1
-   |  on line 27 and therefore is no longer available.
-   |
-   |  where:    ^ refers to a fresh root capability in the type of value x1
+   |  Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/i24373.scala:32:2 -------------------------------------------------------------
+Separation failure: Illegal access to (x2 : Bar^), which was used as a prefix to consume method sink2
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of value x2
+31 |  x2.sink2
+   |  --
+   |  The capability was consumed here.
 32 |  x2.sink2 // error
    |  ^^
-   |  Separation failure: Illegal access to (x2 : Bar^), which was used as a prefix to consume method sink2
-   |  on line 31 and therefore is no longer available.
-   |
-   |  where:    ^ refers to a fresh root capability in the type of value x2
+   |  Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/i24373.scala:49:8 -------------------------------------------------------------
+Separation failure: Illegal access to (x6 : Bar^), which was passed as a consume parameter to method sink6
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of value x6
+48 |  sink6(x6)
+   |        --
+   |        The capability was consumed here.
 49 |  sink6(x6) // error
    |        ^^
-   |      Separation failure: Illegal access to (x6 : Bar^), which was passed as a consume parameter to method sink6
-   |      on line 48 and therefore is no longer available.
-   |
-   |      where:    ^ refers to a fresh root capability in the type of value x6
+   |        Then, it was used here
+
diff --git a/tests/neg-custom-args/captures/i24373a.check b/tests/neg-custom-args/captures/i24373a.check
index 61198e8cc676..91a287772378 100644
--- a/tests/neg-custom-args/captures/i24373a.check
+++ b/tests/neg-custom-args/captures/i24373a.check
@@ -1,38 +1,72 @@
 -- Error: tests/neg-custom-args/captures/i24373a.scala:15:8 ------------------------------------------------------------
+Separation failure: Illegal access to (x1 : Bar^), which was passed as a consume parameter to method sink1
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of value x1
+13 |  sink1(x1)
+   |        --
+   |        The capability was consumed here.
+14 |  sink1(x1)  // ok, rd/rd
 15 |  sink2(x1)  // error
    |        ^^
-   |      Separation failure: Illegal access to (x1 : Bar^), which was passed as a consume parameter to method sink1
-   |      on line 13 and therefore is no longer available.
-   |
-   |      where:    ^ refers to a fresh root capability in the type of value x1
+   |        Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/i24373a.scala:19:8 ------------------------------------------------------------
+Separation failure: Illegal access to x2.rd, which was passed as a consume parameter to method sink2
+and therefore is no longer available.
+18 |  sink2(x2)
+   |        --
+   |        The capability was consumed here.
 19 |  sink1(x2)  // error
    |        ^^
-   |        Separation failure: Illegal access to x2.rd, which was passed as a consume parameter to method sink2
-   |        on line 18 and therefore is no longer available.
+   |        Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/i24373a.scala:20:8 ------------------------------------------------------------
+Separation failure: Illegal access to (x2 : Bar^), which was passed as a consume parameter to method sink2
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of value x2
+18 |  sink2(x2)
+   |        --
+   |        The capability was consumed here.
+19 |  sink1(x2)  // error
 20 |  sink2(x2)  // error
    |        ^^
-   |      Separation failure: Illegal access to (x2 : Bar^), which was passed as a consume parameter to method sink2
-   |      on line 18 and therefore is no longer available.
-   |
-   |      where:    ^ refers to a fresh root capability in the type of value x2
+   |        Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/i24373a.scala:25:8 ------------------------------------------------------------
+Separation failure: Illegal access to (x3 : Bar^), which was passed as a consume parameter to method sink3
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of value x3
+23 |  sink3(x3)
+   |        --
+   |        The capability was consumed here.
+24 |  sink3(x3)  // ok, rd/rd
 25 |  sink2(x3)  // error
    |        ^^
-   |      Separation failure: Illegal access to (x3 : Bar^), which was passed as a consume parameter to method sink3
-   |      on line 23 and therefore is no longer available.
-   |
-   |      where:    ^ refers to a fresh root capability in the type of value x3
+   |        Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/i24373a.scala:29:8 ------------------------------------------------------------
+Separation failure: Illegal access to x4.rd, which was passed as a consume parameter to method sink2
+and therefore is no longer available.
+28 |  sink2(x4)
+   |        --
+   |        The capability was consumed here.
 29 |  sink3(x4)  // error
    |        ^^
-   |        Separation failure: Illegal access to x4.rd, which was passed as a consume parameter to method sink2
-   |        on line 28 and therefore is no longer available.
+   |        Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/i24373a.scala:30:8 ------------------------------------------------------------
+Separation failure: Illegal access to (x4 : Bar^), which was passed as a consume parameter to method sink2
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of value x4
+28 |  sink2(x4)
+   |        --
+   |        The capability was consumed here.
+29 |  sink3(x4)  // error
 30 |  sink2(x4)  // error
    |        ^^
-   |      Separation failure: Illegal access to (x4 : Bar^), which was passed as a consume parameter to method sink2
-   |      on line 28 and therefore is no longer available.
-   |
-   |      where:    ^ refers to a fresh root capability in the type of value x4
+   |        Then, it was used here
+
diff --git a/tests/neg-custom-args/captures/lazyListState.check b/tests/neg-custom-args/captures/lazyListState.check
index bb84f3d7f006..85a9a92a4c2c 100644
--- a/tests/neg-custom-args/captures/lazyListState.check
+++ b/tests/neg-custom-args/captures/lazyListState.check
@@ -1,10 +1,20 @@
 -- [E164] Declaration Error: tests/neg-custom-args/captures/lazyListState.scala:12:39 ----------------------------------
+error overriding method tail in trait State of type -> LazyListIterable[A]^{cap};
+  value tail of type LazyListIterable[A]^ has incompatible type
+
+where:    ^   refers to a fresh root capability in the type of value tail
+          cap is a root capability associated with the result type of -> LazyListIterable[A²]^²
+ 5 |  def tail: LazyListIterable[A]^
+   |      -
+   |      the overridden method is here
+ 6 |
+ 7 |private object State:
+ 8 |  object Empty extends State[Nothing]:
+ 9 |    def head: Nothing = throw new NoSuchElementException("head of empty lazy list")
+10 |    def tail: LazyListIterable[Nothing] = throw new UnsupportedOperationException("tail of empty lazy list")
+11 |
 12 |  final class Cons[A](val head: A, val tail: LazyListIterable[A]^) extends State[A] // error
    |                                       ^
-   |                 error overriding method tail in trait State of type -> LazyListIterable[A]^{cap};
-   |                   value tail of type LazyListIterable[A]^ has incompatible type
-   |
-   |                 where:    ^   refers to a fresh root capability in the type of value tail
-   |                           cap is a root capability associated with the result type of -> LazyListIterable[A²]^²
+   |                                       the overriding value has incompatible type
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/lazylist.check b/tests/neg-custom-args/captures/lazylist.check
index 7dc69e879466..d3aa91bfda97 100644
--- a/tests/neg-custom-args/captures/lazylist.check
+++ b/tests/neg-custom-args/captures/lazylist.check
@@ -44,11 +44,28 @@
    |
    | longer explanation available when compiling with `-explain`
 -- [E164] Declaration Error: tests/neg-custom-args/captures/lazylist.scala:22:6 ----------------------------------------
+error overriding method tail in class LazyList of type -> lazylists.LazyList[Nothing];
+  method tail of type -> lazylists.LazyList[Nothing]^{cap} has incompatible type
+
+where:    cap is a root capability associated with the result type of -> lazylists.LazyList[Nothing]^
+ 8 |  def tail: LazyList[T]
+   |      -
+   |      the overridden method is here
+ 9 |
+10 |  def map[U](f: T => U): LazyList[U]^{f, this} =
+11 |    if isEmpty then LazyNil
+12 |    else LazyCons(f(head), () => tail.map(f))
+13 |
+14 |class LazyCons[+T](val x: T, val xs: () => LazyList[T]^) extends LazyList[T]:
+15 |  def isEmpty = false
+16 |  def head = x
+17 |  def tail = xs() // error
+18 |
+19 |object LazyNil extends LazyList[Nothing]:
+20 |  def isEmpty = true
+21 |  def head = ???
 22 |  def tail: LazyList[Nothing]^ = ???  // error overriding
    |      ^
-   |      error overriding method tail in class LazyList of type -> lazylists.LazyList[Nothing];
-   |        method tail of type -> lazylists.LazyList[Nothing]^{cap} has incompatible type
-   |
-   |      where:    cap is a root capability associated with the result type of -> lazylists.LazyList[Nothing]^
+   |      the overriding method has incompatible type
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/linear-buffer-2.check b/tests/neg-custom-args/captures/linear-buffer-2.check
index 6a3853770f4e..1e997ba87366 100644
--- a/tests/neg-custom-args/captures/linear-buffer-2.check
+++ b/tests/neg-custom-args/captures/linear-buffer-2.check
@@ -1,31 +1,59 @@
 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:13:13 ---------------------------------------------------
+Separation failure: Illegal access to (buf : Buffer[Int]^), which was used as a prefix to consume method append
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability classified as Unscoped in the type of parameter buf
+11 |  val buf1: Buffer[Int]^ = buf.append(1)
+   |                           ---
+   |                           The capability was consumed here.
+12 |  val buf2 = buf1.append(2) // OK
 13 |  val buf3 = buf.append(3) // error
    |             ^^^
-   | Separation failure: Illegal access to (buf : Buffer[Int]^), which was used as a prefix to consume method append
-   | on line 11 and therefore is no longer available.
-   |
-   | where:    ^ refers to a fresh root capability classified as Unscoped in the type of parameter buf
+   |             Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:20:13 ---------------------------------------------------
+Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability classified as Unscoped in the type of value buf1
+18 |    if ??? then buf1.append(2) // OK
+   |                ----
+   |                The capability was consumed here.
+19 |    else buf1.append(3) // OK
 20 |  val buf3 = buf1.append(4) // error
    |             ^^^^
-   |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append
-   |on line 18 and therefore is no longer available.
-   |
-   |where:    ^ refers to a fresh root capability classified as Unscoped in the type of value buf1
+   |             Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:28:13 ---------------------------------------------------
+Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability classified as Unscoped in the type of value buf1
+25 |    case 1 => buf1.append(2) // OK
+   |              ----
+   |              The capability was consumed here.
+26 |    case 2 => buf1.append(2)
+27 |    case _ => buf1.append(3)
 28 |  val buf3 = buf1.append(4) // error
    |             ^^^^
-   |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append
-   |on line 25 and therefore is no longer available.
-   |
-   |where:    ^ refers to a fresh root capability classified as Unscoped in the type of value buf1
+   |             Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:38:13 ---------------------------------------------------
+Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability classified as Unscoped in the type of value buf1
+33 |    case 1 => buf1.append(2) // OK
+   |              ----
+   |              The capability was consumed here.
+34 |    case 2 => buf1.append(2)
+35 |    case 3 => buf1.append(3)
+36 |    case 4 => buf1.append(4)
+37 |    case 5 => buf1.append(5)
 38 |  val buf3 = buf1.append(4) // error
    |             ^^^^
-   |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was used as a prefix to consume method append
-   |on line 33 and therefore is no longer available.
-   |
-   |where:    ^ refers to a fresh root capability classified as Unscoped in the type of value buf1
+   |             Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/linear-buffer-2.scala:42:4 ----------------------------------------------------
 42 |    buf.append(1)  // error
    |    ^^^
diff --git a/tests/neg-custom-args/captures/linear-buffer.check b/tests/neg-custom-args/captures/linear-buffer.check
index 225792af4189..9ec4ca0c8089 100644
--- a/tests/neg-custom-args/captures/linear-buffer.check
+++ b/tests/neg-custom-args/captures/linear-buffer.check
@@ -34,33 +34,61 @@
    |       Separation failure: method bar's result type BadBuffer[T]^ hides non-local this of class class BadBuffer.
    |       The access must be in a consume method to allow this.
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:23:17 -----------------------------------------------------
+Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed as a consume parameter to method app
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability classified as Unscoped in the type of parameter buf
+21 |  val buf1: Buffer[Int]^ = app(buf, 1)
+   |                               ---
+   |                               The capability was consumed here.
+22 |  val buf2 = app(buf1, 2) // OK
 23 |  val buf3 = app(buf, 3) // error
    |                 ^^^
-   |Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed as a consume parameter to method app
-   |on line 21 and therefore is no longer available.
-   |
-   |where:    ^ refers to a fresh root capability classified as Unscoped in the type of parameter buf
+   |                 Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:30:17 -----------------------------------------------------
+Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability classified as Unscoped in the type of value buf1
+28 |    if ??? then app(buf1, 2) // OK
+   |                    ----
+   |                    The capability was consumed here.
+29 |    else app(buf1, 3) // OK
 30 |  val buf3 = app(buf1, 4) // error
    |                 ^^^^
-   |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app
-   |on line 28 and therefore is no longer available.
-   |
-   |where:    ^ refers to a fresh root capability classified as Unscoped in the type of value buf1
+   |                 Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:38:17 -----------------------------------------------------
+Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability classified as Unscoped in the type of value buf1
+35 |    case 1 => app(buf1, 2) // OK
+   |                  ----
+   |                  The capability was consumed here.
+36 |    case 2 => app(buf1, 2)
+37 |    case _ => app(buf1, 3)
 38 |  val buf3 = app(buf1, 4) // error
    |                 ^^^^
-   |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app
-   |on line 35 and therefore is no longer available.
-   |
-   |where:    ^ refers to a fresh root capability classified as Unscoped in the type of value buf1
+   |                 Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:48:17 -----------------------------------------------------
+Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability classified as Unscoped in the type of value buf1
+43 |    case 1 => app(buf1, 2) // OK
+   |                  ----
+   |                  The capability was consumed here.
+44 |    case 2 => app(buf1, 2)
+45 |    case 3 => app(buf1, 3)
+46 |    case 4 => app(buf1, 4)
+47 |    case 5 => app(buf1, 5)
 48 |  val buf3 = app(buf1, 4) // error
    |                 ^^^^
-   |Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed as a consume parameter to method app
-   |on line 43 and therefore is no longer available.
-   |
-   |where:    ^ refers to a fresh root capability classified as Unscoped in the type of value buf1
+   |                 Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:52:8 ------------------------------------------------------
 52 |    app(buf, 1)  // error
    |        ^^^
@@ -69,7 +97,14 @@
    |
    |        where:    ^ refers to a fresh root capability classified as Unscoped in the type of parameter buf
 -- Error: tests/neg-custom-args/captures/linear-buffer.scala:62:20 -----------------------------------------------------
+Separation failure: Illegal access to buf.rd, which was passed as a consume parameter to method app
+and therefore is no longer available.
+59 |  val buf1 = app(buf, "hi") // buf unavailable from here
+   |                 ---
+   |                 The capability was consumed here.
+60 |  val c1 = contents(buf1)         // only buf.rd is consumed
+61 |  val c2 = contents(buf1)         // buf.rd can be consumed repeatedly
 62 |  val c3 = contents(buf)  // error
    |                    ^^^
-   |             Separation failure: Illegal access to buf.rd, which was passed as a consume parameter to method app
-   |             on line 59 and therefore is no longer available.
+   |                    Then, it was used here
+
diff --git a/tests/neg-custom-args/captures/mut-iterator1.check b/tests/neg-custom-args/captures/mut-iterator1.check
index 2a167a752e41..df630d89a58e 100644
--- a/tests/neg-custom-args/captures/mut-iterator1.check
+++ b/tests/neg-custom-args/captures/mut-iterator1.check
@@ -1,5 +1,13 @@
 -- [E164] Declaration Error: tests/neg-custom-args/captures/mut-iterator1.scala:9:15 -----------------------------------
+error overriding method next in trait Iterator of type (): U;
+  method next of type (): U is an update method, cannot override a read-only method
+5 |  def next(): T
+  |      -
+  |      the overridden method is here
+6 |
+7 |  def map[U](f: T => U): Iterator[U] = new Iterator:
+8 |    def hasNext = Iterator.this.hasNext
 9 |    update def next() = f(Iterator.this.next()) // error
   |               ^
-  |               error overriding method next in trait Iterator of type (): U;
-  |                 method next of type (): U is an update method, cannot override a read-only method
+  |               the overriding method is an update method, cannot override a read-only method
+
diff --git a/tests/neg-custom-args/captures/sep-consume.check b/tests/neg-custom-args/captures/sep-consume.check
index 40521e319b61..d3f1b3086694 100644
--- a/tests/neg-custom-args/captures/sep-consume.check
+++ b/tests/neg-custom-args/captures/sep-consume.check
@@ -4,19 +4,31 @@
    |                          Local reach capability p.fst* leaks into capture scope of method test4.
    |                          You could try to abstract the capabilities referred to by p.fst* in a capset variable.
 -- Error: tests/neg-custom-args/captures/sep-consume.scala:19:2 --------------------------------------------------------
+Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability classified as Unscoped in the type of parameter x
+18 |  val rx: () => Unit = bad(f)  // hides x.rd in the resulting `cap`
+   |                           -
+   |                           The capability was consumed here.
 19 |  x.put(42)  // error
    |  ^
-   |  Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad
-   |  on line 18 and therefore is no longer available.
-   |
-   |  where:    ^ refers to a fresh root capability classified as Unscoped in the type of parameter x
+   |  Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/sep-consume.scala:21:16 -------------------------------------------------------
+Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability classified as Unscoped in the type of parameter x
+18 |  val rx: () => Unit = bad(f)  // hides x.rd in the resulting `cap`
+   |                           -
+   |                           The capability was consumed here.
+19 |  x.put(42)  // error
+20 |  x.get      // ok rd/rd
 21 |  par(rx, () => x.put(42))  // error
    |                ^
-   |         Separation failure: Illegal access to (x : Ref^), which was passed as a consume parameter to method bad
-   |         on line 18 and therefore is no longer available.
-   |
-   |         where:    ^ refers to a fresh root capability classified as Unscoped in the type of parameter x
+   |                Then, it was used here
+
 -- Error: tests/neg-custom-args/captures/sep-consume.scala:26:16 -------------------------------------------------------
 26 |  def foo = bad(f) // error
    |                ^
diff --git a/tests/neg-custom-args/captures/sep-curried-par.check b/tests/neg-custom-args/captures/sep-curried-par.check
index 2172c5699fa8..9a526dbd817a 100644
--- a/tests/neg-custom-args/captures/sep-curried-par.check
+++ b/tests/neg-custom-args/captures/sep-curried-par.check
@@ -34,12 +34,15 @@
    |where:    =>  refers to a fresh root capability in the type of value p
    |          =>² refers to a fresh root capability created in method test when checking argument to parameter p1 of method par
 -- Error: tests/neg-custom-args/captures/sep-curried-par.scala:18:16 ---------------------------------------------------
+Separation failure: Illegal access to (p : () => Unit), which was passed as a consume parameter to method parCurried
+and therefore is no longer available.
+
+where:    => refers to a fresh root capability in the type of value p
 18 |  parCurried(p)(p) // error: consume failure
-   |                ^
-   |Separation failure: Illegal access to (p : () => Unit), which was passed as a consume parameter to method parCurried
-   |on line 18 and therefore is no longer available.
-   |
-   |where:    => refers to a fresh root capability in the type of value p
+   |             -  ^
+   |             |  Then, it was used here
+   |             The capability was consumed here.
+
 -- Error: tests/neg-custom-args/captures/sep-curried-par.scala:21:9 ----------------------------------------------------
 21 |  foo(c)(c) // error: separation
    |         ^
diff --git a/tests/neg-custom-args/captures/sepchecks5.check b/tests/neg-custom-args/captures/sepchecks5.check
index ab7ae86a9cef..b250185c7657 100644
--- a/tests/neg-custom-args/captures/sepchecks5.check
+++ b/tests/neg-custom-args/captures/sepchecks5.check
@@ -9,9 +9,14 @@
    |             Separation failure: argument to consume parameter with type (io : Object^) refers to parameter io.
    |             The parameter needs to be annotated with consume to allow this.
 -- Error: tests/neg-custom-args/captures/sepchecks5.scala:20:24 --------------------------------------------------------
+Separation failure: Illegal access to (io : Object^), which was passed as a consume parameter to method g
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability in the type of parameter io
+19 |  val f2 = g(io)              // error
+   |             --
+   |             The capability was consumed here.
 20 |  par(f2)(() => println(io))  // error
    |                        ^^
-   |       Separation failure: Illegal access to (io : Object^), which was passed as a consume parameter to method g
-   |       on line 19 and therefore is no longer available.
-   |
-   |       where:    ^ refers to a fresh root capability in the type of parameter io
+   |                        Then, it was used here
+
diff --git a/tests/neg-custom-args/captures/unbox-overrides.check b/tests/neg-custom-args/captures/unbox-overrides.check
index 883ab56c59a5..6e13df9bcd1d 100644
--- a/tests/neg-custom-args/captures/unbox-overrides.check
+++ b/tests/neg-custom-args/captures/unbox-overrides.check
@@ -1,30 +1,55 @@
 -- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:8:6 ----------------------------------
+error overriding method foo in trait A of type [C >: scala.caps.CapSet <: scala.caps.CapSet^]: Object^{C};
+  method foo of type [C >: scala.caps.CapSet <: scala.caps.CapSet^²]: Object^{C} has a parameter C with different @reserve status than the corresponding parameter in the overridden definition
+
+where:    ^  refers to a fresh root capability in the type of type C²
+          ^² refers to a fresh root capability in the type of type C³
+4 |  def foo[@reserve C^]: Object^{C}
+  |      -
+  |      the overridden method is here
+5 |  def bar[C^]: Object^{C}
+6 |
+7 |trait B extends A:
 8 |  def foo[C^]: Object^{C}  // error
   |      ^
-  |error overriding method foo in trait A of type [C >: scala.caps.CapSet <: scala.caps.CapSet^]: Object^{C};
-  |  method foo of type [C >: scala.caps.CapSet <: scala.caps.CapSet^²]: Object^{C} has a parameter C with different @reserve status than the corresponding parameter in the overridden definition
-  |
-  |where:    ^  refers to a fresh root capability in the type of type C²
-  |          ^² refers to a fresh root capability in the type of type C³
+  |the overriding method has a parameter C with different @reserve status than the corresponding parameter in the overridden definition
   |
   | longer explanation available when compiling with `-explain`
 -- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:9:6 ----------------------------------
+error overriding method bar in trait A of type [C >: scala.caps.CapSet <: scala.caps.CapSet^]: Object^{C};
+  method bar of type [C >: scala.caps.CapSet <: scala.caps.CapSet^²]: Object^{C} has a parameter C with different @reserve status than the corresponding parameter in the overridden definition
+
+where:    ^  refers to a fresh root capability in the type of type C²
+          ^² refers to a fresh root capability in the type of type C³
+5 |  def bar[C^]: Object^{C}
+  |      -
+  |      the overridden method is here
+6 |
+7 |trait B extends A:
+8 |  def foo[C^]: Object^{C}  // error
 9 |  def bar[@reserve C^]: Object^{C} // error
   |      ^
-  |error overriding method bar in trait A of type [C >: scala.caps.CapSet <: scala.caps.CapSet^]: Object^{C};
-  |  method bar of type [C >: scala.caps.CapSet <: scala.caps.CapSet^²]: Object^{C} has a parameter C with different @reserve status than the corresponding parameter in the overridden definition
-  |
-  |where:    ^  refers to a fresh root capability in the type of type C²
-  |          ^² refers to a fresh root capability in the type of type C³
+  |the overriding method has a parameter C with different @reserve status than the corresponding parameter in the overridden definition
   |
   | longer explanation available when compiling with `-explain`
 -- [E164] Declaration Error: tests/neg-custom-args/captures/unbox-overrides.scala:15:15 --------------------------------
-15 |abstract class C extends A, B2 // error
-   |               ^
-   |error overriding method foo in trait A of type [C >: scala.caps.CapSet <: scala.caps.CapSet^]: Object^{C};
-   |  method foo in trait B2 of type [C >: scala.caps.CapSet <: scala.caps.CapSet^²]: Object^{C} has a parameter C with different @reserve status than the corresponding parameter in the overridden definition
-   |
-   |where:    ^  refers to a fresh root capability in the type of type C²
-   |          ^² refers to a fresh root capability in the type of type C³
+error overriding method foo in trait A of type [C >: scala.caps.CapSet <: scala.caps.CapSet^]: Object^{C};
+  method foo in trait B2 of type [C >: scala.caps.CapSet <: scala.caps.CapSet^²]: Object^{C} has a parameter C with different @reserve status than the corresponding parameter in the overridden definition
+
+where:    ^  refers to a fresh root capability in the type of type C²
+          ^² refers to a fresh root capability in the type of type C³
+ 4 |  def foo[@reserve C^]: Object^{C}
+   |      -
+   |      the overridden method is here
+ 5 |  def bar[C^]: Object^{C}
+ 6 |
+ 7 |trait B extends A:
+ 8 |  def foo[C^]: Object^{C}  // error
+ 9 |  def bar[@reserve C^]: Object^{C} // error
+10 |
+11 |trait B2:
+12 |  def foo[C^]: Object^{C}
+   |      ^
+   |the overriding method has a parameter C with different @reserve status than the corresponding parameter in the overridden definition
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg-custom-args/captures/unscoped-extrude.check b/tests/neg-custom-args/captures/unscoped-extrude.check
index b59c6bc2fb48..4f6b47dabe1c 100644
--- a/tests/neg-custom-args/captures/unscoped-extrude.check
+++ b/tests/neg-custom-args/captures/unscoped-extrude.check
@@ -1,7 +1,12 @@
 -- Error: tests/neg-custom-args/captures/unscoped-extrude.scala:13:4 ---------------------------------------------------
+Separation failure: Illegal access to (r : Ref[String]^), which was consumed in an assignment to variable x
+and therefore is no longer available.
+
+where:    ^ refers to a fresh root capability classified as Unscoped in the type of value r
+12 |    x = r  // should be consumed here
+   |    -----
+   |    The capability was consumed here.
 13 |    r      // error
    |    ^
-   |    Separation failure: Illegal access to (r : Ref[String]^), which was consumed in an assignment to variable x
-   |    on line 12 and therefore is no longer available.
-   |
-   |    where:    ^ refers to a fresh root capability classified as Unscoped in the type of value r
+   |    Then, it was used here
+
diff --git a/tests/neg-custom-args/captures/unsound-reach-4.check b/tests/neg-custom-args/captures/unsound-reach-4.check
index 6e4271cf0057..3ec2529eac5d 100644
--- a/tests/neg-custom-args/captures/unsound-reach-4.check
+++ b/tests/neg-custom-args/captures/unsound-reach-4.check
@@ -19,13 +19,18 @@
    |
    | longer explanation available when compiling with `-explain`
 -- [E164] Declaration Error: tests/neg-custom-args/captures/unsound-reach-4.scala:17:6 ---------------------------------
+error overriding method use in trait Foo of type (x: File^): File^²;
+  method use of type (@consume x: File^): File^³ has incompatible type
+
+where:    ^  refers to the universal root capability
+          ^² refers to a fresh root capability created in class Bar
+          ^³ refers to a root capability associated with the result type of (@consume x: File^): File^³
+15 |  def use(x: F): X
+   |      -
+   |      the overridden method is here
+16 |class Bar extends Foo[File^]: // error
 17 |  def use(consume x: F): File^ = x // error consume override
    |      ^
-   |      error overriding method use in trait Foo of type (x: File^): File^²;
-   |        method use of type (@consume x: File^): File^³ has incompatible type
-   |
-   |      where:    ^  refers to the universal root capability
-   |                ^² refers to a fresh root capability created in class Bar
-   |                ^³ refers to a root capability associated with the result type of (@consume x: File^): File^³
+   |      the overriding method has incompatible type
    |
    | longer explanation available when compiling with `-explain`
diff --git a/tests/neg/abstract-givens.check b/tests/neg/abstract-givens.check
index 51f50db266c2..e02a980d5ad0 100644
--- a/tests/neg/abstract-givens.check
+++ b/tests/neg/abstract-givens.check
@@ -3,17 +3,34 @@
    |        ^
    |instance cannot be created, since def iterator: Iterator[A] in trait IterableOnce in package scala.collection is not defined 
 -- [E164] Declaration Error: tests/neg/abstract-givens.scala:8:8 -------------------------------------------------------
+error overriding given instance y in trait T of type (using x$1: Int): String;
+  given instance y of type (using x$1: Int): String cannot override final member given instance y in trait T
+3 |  given y(using Int): String = summon[Int].toString
+  |        -
+  |        the overridden given instance is here
+4 |  given z[T](using T): List[T]
+5 |
+6 |object Test extends T:
+7 |  given x: Int = 22
 8 |  given y(using Int): String = summon[Int].toString * 22 // error
   |        ^
-  |      error overriding given instance y in trait T of type (using x$1: Int): String;
-  |        given instance y of type (using x$1: Int): String cannot override final member given instance y in trait T
+  |        the overriding given instance cannot override final member given instance y in trait T
+
 -- [E164] Declaration Error: tests/neg/abstract-givens.scala:9:8 -------------------------------------------------------
+error overriding given instance z in trait T² of type [T](using x$1: T): List[T];
+  given instance z of type [T](using x$1: T): Seq[T] has incompatible type
+
+where:    T  is a type variable
+          T² is a trait in the empty package
+4 |  given z[T](using T): List[T]
+  |        -
+  |        the overridden given instance is here
+5 |
+6 |object Test extends T:
+7 |  given x: Int = 22
+8 |  given y(using Int): String = summon[Int].toString * 22 // error
 9 |  given z[T](using T): Seq[T] = List(summon[T]) // error
   |        ^
-  |        error overriding given instance z in trait T² of type [T](using x$1: T): List[T];
-  |          given instance z of type [T](using x$1: T): Seq[T] has incompatible type
-  |
-  |        where:    T  is a type variable
-  |                  T² is a trait in the empty package
+  |        the overriding given instance has incompatible type
   |
   | longer explanation available when compiling with `-explain`
diff --git a/tests/neg/exports2.check b/tests/neg/exports2.check
index 245538b12abb..f5c096bdd3da 100644
--- a/tests/neg/exports2.check
+++ b/tests/neg/exports2.check
@@ -1,5 +1,12 @@
 -- [E164] Declaration Error: tests/neg/exports2.scala:8:11 -------------------------------------------------------------
+error overriding method f in trait B of type => String;
+  method f of type => String cannot override since it comes from an export
+5 |  def f: String = "abc"
+  |      -
+  |      the overridden method is here
+6 |
+7 |object C extends B:
 8 |  export A._            // error
   |           ^
-  |           error overriding method f in trait B of type => String;
-  |             method f of type => String cannot override since it comes from an export
+  |           the overriding method cannot override since it comes from an export
+
diff --git a/tests/neg/harmonize.scala b/tests/neg/harmonize.scala
index 72275a8f68fc..aa60656f0278 100644
--- a/tests/neg/harmonize.scala
+++ b/tests/neg/harmonize.scala
@@ -79,9 +79,9 @@ object Test {
     val a4 = ArrayBuffer(1.0f, 1L)
     val b4: ArrayBuffer[Double] = a4 // error: no widening
     val a5 = ArrayBuffer(1.0f, 1L, f())
-    val b5: ArrayBuffer[Float | Long | Int] = a5
+    val b5: ArrayBuffer[Float | Long | Int] = a5 // error: no widening
     val a6 = ArrayBuffer(1.0f, 1234567890)
-    val b6: ArrayBuffer[Float | Int] = a6
+    val b6: ArrayBuffer[Float | Int] = a6 // error: no widening
 
   def totalDuration(results: List[Long], cond: Boolean): Long =
     results.map(r => if (cond) r else 0).sum
diff --git a/tests/neg/i14415.check b/tests/neg/i14415.check
index 596debf175dc..70cb321079c1 100644
--- a/tests/neg/i14415.check
+++ b/tests/neg/i14415.check
@@ -1,5 +1,13 @@
 -- [E164] Declaration Error: tests/neg/i14415.scala:21:6 ---------------------------------------------------------------
-21 |class X extends E with D // error
-   |      ^
-   |      error overriding method m in trait C of type (a: Int): Int;
-   |        method m in trait D of type (a: Int): Int needs `abstract override` modifiers
+error overriding method m in trait C of type (a: Int): Int;
+  method m in trait D of type (a: Int): Int needs `abstract override` modifiers
+10 |    abstract override def m(a:Int):Int = { return super.m(a); }
+   |                          -
+   |                          the overridden method is here
+11 |}
+12 |
+13 |trait D extends B with C {
+14 |    override def m(a:Int):Int = { return super.m(a); }
+   |                 ^
+   |                 the overriding method needs `abstract override` modifiers
+
diff --git a/tests/neg/i23474.check b/tests/neg/i23474.check
index 441978be6809..2612e09c808f 100644
--- a/tests/neg/i23474.check
+++ b/tests/neg/i23474.check
@@ -9,10 +9,23 @@
   |      class Z needs to be abstract, since var comment_=(x$1: String): Unit in trait Comment is not defined 
   |      (Note that an abstract var requires a setter in addition to the getter)
 -- [E164] Declaration Error: tests/neg/i23474.scala:11:15 --------------------------------------------------------------
+error overriding variable comment in trait Comment of type String;
+  method comment of type => String cannot override a mutable variable
+ 2 |  var comment: String
+   |      -
+   |      the overridden variable is here
+ 3 |}
+ 4 |
+ 5 |case class Y(val comment: String) extends Comment // error
+ 6 |
+ 7 |class Z extends Comment: // error
+ 8 |  val comment: String = ""
+ 9 |
+10 |class X extends Comment: // error
 11 |  override def comment: String = "" // error
    |               ^
-   |               error overriding variable comment in trait Comment of type String;
-   |                 method comment of type => String cannot override a mutable variable
+   |               the overriding method cannot override a mutable variable
+
 -- Error: tests/neg/i23474.scala:10:6 ----------------------------------------------------------------------------------
 10 |class X extends Comment: // error
    |      ^
diff --git a/tests/neg/override-multi-file-error.check b/tests/neg/override-multi-file-error.check
new file mode 100644
index 000000000000..37f1657ff89f
--- /dev/null
+++ b/tests/neg/override-multi-file-error.check
@@ -0,0 +1,13 @@
+-- [E164] Declaration Error: tests/neg/override-multi-file-error/B.scala:2:15 ------------------------------------------
+error overriding method foo in class A of type => Int;
+  method foo of type => String has incompatible type
+... tests/neg/override-multi-file-error/A.scala
+2 |  def foo: Int = 0
+  |      -
+  |      the overridden method is here
+... tests/neg/override-multi-file-error/B.scala
+2 |  override def foo: String = "0"   // error
+  |               ^
+  |               the overriding method has incompatible type
+  |
+  | longer explanation available when compiling with `-explain`
diff --git a/tests/neg/override-multi-file-error/A.scala b/tests/neg/override-multi-file-error/A.scala
new file mode 100644
index 000000000000..84516facb381
--- /dev/null
+++ b/tests/neg/override-multi-file-error/A.scala
@@ -0,0 +1,3 @@
+class A:
+  def foo: Int = 0
+
diff --git a/tests/neg/override-multi-file-error/B.scala b/tests/neg/override-multi-file-error/B.scala
new file mode 100644
index 000000000000..837e8ca5757e
--- /dev/null
+++ b/tests/neg/override-multi-file-error/B.scala
@@ -0,0 +1,3 @@
+class B extends A:
+  override def foo: String = "0"   // error
+
diff --git a/tests/neg/override-multi-span.check b/tests/neg/override-multi-span.check
new file mode 100644
index 000000000000..a967c1139b7d
--- /dev/null
+++ b/tests/neg/override-multi-span.check
@@ -0,0 +1,14 @@
+-- [E164] Declaration Error: tests/neg/override-multi-span.scala:6:15 --------------------------------------------------
+error overriding method foo in class A of type => Int;
+  method foo of type => String has incompatible type
+2 |  def foo: Int = 0
+  |      -
+  |      the overridden method is here
+3 |def main(): Unit =
+4 |  println("Hello")
+5 |class B extends A:
+6 |  override def foo: String = "0"  // error
+  |               ^
+  |               the overriding method has incompatible type
+  |
+  | longer explanation available when compiling with `-explain`
diff --git a/tests/neg/override-multi-span.scala b/tests/neg/override-multi-span.scala
new file mode 100644
index 000000000000..3250eb5dca49
--- /dev/null
+++ b/tests/neg/override-multi-span.scala
@@ -0,0 +1,6 @@
+class A:
+  def foo: Int = 0
+def main(): Unit =
+  println("Hello")
+class B extends A:
+  override def foo: String = "0"  // error
diff --git a/tests/neg/override-scala2-macro.check b/tests/neg/override-scala2-macro.check
index ff5e478342dd..9014bdb9ac82 100644
--- a/tests/neg/override-scala2-macro.check
+++ b/tests/neg/override-scala2-macro.check
@@ -1,5 +1,12 @@
 -- [E164] Declaration Error: tests/neg/override-scala2-macro.scala:2:22 ------------------------------------------------
-2 |  override inline def f[A >: Any](args: A*): String = ??? // error
-  |                      ^
-  |error overriding method f in class StringContext of type [A >: Any](args: Seq[A]): String;
-  |  method f of type [A >: Any](args: Seq[A]): String cannot be used here - only Scala-2 macros can override Scala-2 macros
+error overriding method f in class StringContext of type [A >: Any](args: Seq[A]): String;
+  method f of type [A >: Any](args: Seq[A]): String cannot be used here - only Scala-2 macros can override Scala-2 macros
+... library/src/scala/StringContext.scala
+197 |  def f[A >: Any](args: A*): String = macro ??? // fasttracked to scala.tools.reflect.FormatInterpolator::interpolateF
+    |      -
+    |      the overridden method is here
+... tests/neg/override-scala2-macro.scala
+ 2 |  override inline def f[A >: Any](args: A*): String = ??? // error
+    |                      ^
+    |                   the overriding method cannot be used here - only Scala-2 macros can override Scala-2 macros
+
diff --git a/tests/neg/parent-refinement-access.check b/tests/neg/parent-refinement-access.check
index 5cde9d51558f..3ecb0292f726 100644
--- a/tests/neg/parent-refinement-access.check
+++ b/tests/neg/parent-refinement-access.check
@@ -1,7 +1,13 @@
 -- [E164] Declaration Error: tests/neg/parent-refinement-access.scala:6:6 ----------------------------------------------
+error overriding value x in trait Year2 of type Int;
+  value x in trait Gen of type Any has weaker access privileges; it should be public
+(Note that value x in trait Year2 of type Int is abstract,
+and is therefore overridden by concrete value x in trait Gen of type Any)
+4 |  private[Gen] val x: Any = ()
+  |                   ^
+  |                   the overriding value has weaker access privileges; it should be public
+5 |
 6 |trait Year2(private[Year2] val value: Int) extends (Gen { val x: Int }) // error
-  |      ^
-  |      error overriding value x in trait Year2 of type Int;
-  |        value x in trait Gen of type Any has weaker access privileges; it should be public
-  |      (Note that value x in trait Year2 of type Int is abstract,
-  |      and is therefore overridden by concrete value x in trait Gen of type Any)
+  |           -
+  |           the overridden value is here
+
diff --git a/tests/neg/publicInBinaryOverride.check b/tests/neg/publicInBinaryOverride.check
index e44692c78525..e90624af18de 100644
--- a/tests/neg/publicInBinaryOverride.check
+++ b/tests/neg/publicInBinaryOverride.check
@@ -1,5 +1,13 @@
 -- [E164] Declaration Error: tests/neg/publicInBinaryOverride.scala:8:15 -----------------------------------------------
+error overriding method f in class A of type (): Unit;
+  method f of type (): Unit also needs to be declared with @publicInBinary
+4 |  @publicInBinary def f(): Unit = ()
+  |                      -
+  |                      the overridden method is here
+5 |  @publicInBinary def g(): Unit = ()
+6 |
+7 |class B extends A:
 8 |  override def f(): Unit = () // error
   |               ^
-  |               error overriding method f in class A of type (): Unit;
-  |                 method f of type (): Unit also needs to be declared with @publicInBinary
+  |               the overriding method also needs to be declared with @publicInBinary
+
diff --git a/tests/neg/targetName-override.check b/tests/neg/targetName-override.check
index 230b7fe77745..9e1b1e7542bf 100644
--- a/tests/neg/targetName-override.check
+++ b/tests/neg/targetName-override.check
@@ -1,18 +1,60 @@
 -- [E164] Declaration Error: tests/neg/targetName-override.scala:16:35 -------------------------------------------------
+error overriding method foo in class Alpha of type (): Int;
+  method foo of type (): Int should not have a @targetName annotation since the overridden member hasn't one either
+ 6 |  def foo() = 1
+   |      -
+   |      the overridden method is here
+ 7 |
+ 8 |  @targetName("foo1") def foo(x: T): T
+ 9 |
+10 |  @targetName("append") def ++ (xs: Alpha[T]): Alpha[T] = this
+11 |
+12 |}
+13 |
+14 |class Beta extends Alpha[String] {  // error: needs to be abstract
+15 |
 16 |  @targetName("foo1") override def foo() = 1    // error: should not have a target name
    |                                   ^
-   |error overriding method foo in class Alpha of type (): Int;
-   |  method foo of type (): Int should not have a @targetName annotation since the overridden member hasn't one either
+   |    the overriding method should not have a @targetName annotation since the overridden member hasn't one either
+
 -- [E164] Declaration Error: tests/neg/targetName-override.scala:18:25 -------------------------------------------------
+error overriding method foo in class Alpha of type (x: String): String;
+  method foo of type (x: String): String has a different target name annotation; it should be @targetName(foo1)
+ 8 |  @targetName("foo1") def foo(x: T): T
+   |                          -
+   |                          the overridden method is here
+ 9 |
+10 |  @targetName("append") def ++ (xs: Alpha[T]): Alpha[T] = this
+11 |
+12 |}
+13 |
+14 |class Beta extends Alpha[String] {  // error: needs to be abstract
+15 |
+16 |  @targetName("foo1") override def foo() = 1    // error: should not have a target name
+17 |
 18 |  @targetName("baz") def foo(x: String): String = x ++ x   // error: has a different target name annotation
    |                         ^
-   | error overriding method foo in class Alpha of type (x: String): String;
-   |   method foo of type (x: String): String has a different target name annotation; it should be @targetName(foo1)
+   |                    the overriding method has a different target name annotation; it should be @targetName(foo1)
+
 -- [E164] Declaration Error: tests/neg/targetName-override.scala:20:15 -------------------------------------------------
+error overriding method ++ in class Alpha of type (xs: Alpha[String]): Alpha[String];
+  method ++ of type (xs: Alpha[String]): Alpha[String] misses a target name annotation @targetName(append)
+10 |  @targetName("append") def ++ (xs: Alpha[T]): Alpha[T] = this
+   |                            -
+   |                            the overridden method is here
+11 |
+12 |}
+13 |
+14 |class Beta extends Alpha[String] {  // error: needs to be abstract
+15 |
+16 |  @targetName("foo1") override def foo() = 1    // error: should not have a target name
+17 |
+18 |  @targetName("baz") def foo(x: String): String = x ++ x   // error: has a different target name annotation
+19 |
 20 |  override def ++ (xs: Alpha[String]): Alpha[String] = this   // error: misses a targetname annotation
    |               ^
-   |      error overriding method ++ in class Alpha of type (xs: Alpha[String]): Alpha[String];
-   |        method ++ of type (xs: Alpha[String]): Alpha[String] misses a target name annotation @targetName(append)
+   |               the overriding method misses a target name annotation @targetName(append)
+
 -- Error: tests/neg/targetName-override.scala:14:6 ---------------------------------------------------------------------
 14 |class Beta extends Alpha[String] {  // error: needs to be abstract
    |      ^^^^
diff --git a/tests/warn/matchable.scala b/tests/warn/matchable.scala
index 8adcdcf1c90a..2a27ad36428c 100644
--- a/tests/warn/matchable.scala
+++ b/tests/warn/matchable.scala
@@ -13,7 +13,7 @@ def foo[T](x: T): Matchable =
   List(x) match
     case (x: Int) :: Nil =>  // warn: should not be scrutinized
       println("int")
-      x
+      x  // warn
     case List(x: String) =>  // warn: should not be scrutinized
       println("string")
       x