Fatal error: Variable tmp is not defined in context

[andreagilot-da]

When running the following snippet of code with both stainless-scalac and dotty, Stainless outputs the following error message.

case class A() {
  def f(w: Unit): Unit = ()
  def g: Unit = ()
}

def foo(a: A): Unit = ()

def bug(a: A): Unit = {
  if (true) {
    foo(a)
    def w = a.g
    unfold(a.f(w))
  }
  if (true) {
    def w = a.g
    unfold(a.f(w))
  }
}

[ Fatal  ] Bug.scala:14:7: Variable tmp 0 is not defined in context:
[ Fatal  ] Kind: argument types (call w(a, tmp))
[ Fatal  ] Check SAT: false
[ Fatal  ] Emit VCs: true
[ Fatal  ] Functions: f, g, w, foo
[ Fatal  ] ADTs: A
[ Fatal  ] Type Variables: 
[ Fatal  ] Term Variables:
[ Fatal  ]   a: A
[ Fatal  ]   targetBound: Boolean
[ Fatal  ]   targetBound == true
[ Fatal  ]   t: Unit
[ Fatal  ]   t == (if (targetBound) {
[ Fatal  ]   val tmp: Unit = foo(a)
[ Fatal  ]   assume(f(a, w(a)) == (()): @DropVCs )
[ Fatal  ]   ()
[ Fatal  ] } else {
[ Fatal  ]   ()
[ Fatal  ] })
[ Fatal  ]   res: Unit
[ Fatal  ]   res == t
[ Fatal  ]   tmp: Unit
[ Fatal  ]   tmp == res
[ Fatal  ]   targetBound: Boolean
[ Fatal  ]   targetBound == true
[ Fatal  ]   targetBound
[ Fatal  ]   thiss: A
[ Fatal  ]   thiss == a
[ Fatal  ]   a: A
[ Fatal  ]   a == a
[ Fatal  ] 
                 def w = a.g
                 ^^^^^^^^^^^

Any change to the minimized example removes the error.

[andreagilot-da]

Other minimal example but this time without unfold(...) or variables defined twice with the same name:

case class A() {
    def f(w: Unit): Boolean = true
  }

  def foo(a: A): Unit = ()

  def bug(a: A, w: Unit): Unit = {
    if (true) {
      foo(a)
      assert(a.f(w))
      def w2: Unit = w
      assert(a.f(w2))
    }
    def w3: Unit = w
    val variable = a.f(w3)
  }