assertion failed: varsInScope should contain b1

[vkuncak]

This code

import stainless.annotation.pure
case class Box(var length: Int)
object Foo {
  def makeBox(): Box = Box(0)
  def mutate(b: Box): Unit = { b.length = 123; }

  // Crash in ImperativeCodeElimination and omits effect on b1/b2
  def h(b1: Box, b2: Box): Unit = {
    val x = b1.length
    val c = if (true) b1 else b2
    val d = c // Interacts with Let handling `computeExprEffects`
    // We try to assign to val c (and nothing else!)
    mutate(d)
    assert(b1.length == x)
  }
}

causes the above mentioned

assertion failed: varsInScope should contain b1

Taken from #819 .