Avoid unused mutable match rebinding in AntiAliasing

[Copilot]

AntiAliasing was rebinding mutable pattern variables even when the binder was never referenced, which introduced unnecessary asInstanceOf casts and triggered downstream type encoding in simple matches. This change keeps the existing alias-tracking behavior for used mutable binders while leaving unused ones untouched.

• Normalizer change

  • Restrict mutable pattern rebinding in AntiAliasing to binders that are actually referenced in the case guard or RHS.
  • Preserve the existing rewrite path for mutable binders that do participate in target computation.

• Effect on extracted trees

  • Stop generating synthetic bindings like val n = l.asInstanceOf[Cons].next for cases where n is unused.
  • Reduce unnecessary instanceOf/type-encoding noise in debug output and later phases.

• Regression coverage

  • Add a focused test for the reported SwapInstanceOf pattern-match case.
  • Assert that AntiAliasing output no longer contains the unused asInstanceOf[Cons].next rebinding.

Example of the case covered by the change:

import stainless.annotation.*
object SwapInstanceOf:

  case class Cell[@mutable T](var v: T)

  sealed trait List
  case class Cons(next: Cell[List]) extends List
  case class Nil() extends List

  def change(l: List): Unit =
    l match
      case Nil() => ()
      case Cons(n) => ()

Before, AntiAliasing rewrote the Cons branch to introduce an unused binding derived from l.asInstanceOf[Cons].next. With this change, that rebinding is only introduced when the mutable binder is actually used.

[CLAassistant]

Thank you for your submission! We really appreciate it. Like many open source projects, we ask that you sign our Contributor License Agreement before we can accept your contribution.
_{You have signed the CLA already but the status is still pending? Let us recheck it.}

[vkuncak]

What if I have in change function a more general line

case Cons(n) => change(n.v)

There is again no need for any casts as far as I can tell.