import stainless._
import stainless.lang._

object IndexMutation {

  case class Box(var value: Int)

  def f(arr: Array[Box], i: Int): Unit = {
    require(0 <= i && i < 2000)
    require(arr.length >= 3000)

    var ii = i
    ii += 1

    val aliasedElem = arr(ii)
    arr(ii).value = 123

    assert(aliasedElem.value == 123) // Ok

    ii += 1
    arr(ii).value = 456
    // Unaffected, but does not pass
    assert(aliasedElem.value == 123)
  }
}

// Symbols before AntiAliasing
def f(arr: Array[Box], (i: Int) @pure): Unit = {
  require(0 <= i && i < 2000)
  require(arr.length >= 3000)
  var (ii: Int) @var = i
  ii = (ii + 1)
  val aliasedElem: Box = arr(ii)
  arr(ii).value = 123
  assert(aliasedElem.value == 123)
  ii = (ii + 1)
  arr(ii).value = 456
  assert(aliasedElem.value == 123)
  ()
}

// Symbols after AntiAliasing
def f(arr: Array[Box], (i: Int) @pure): (Unit, Array[Box]) = {
  require(0 <= i && i < 2000)
  require(arr.length >= 3000)
  var arr: Array[Box] = arr
  ({
    var (ii: Int) @var = i
    ii = (ii + 1)
    var aliasedElem: Box = arr(ii)
    arr = arr.updated(ii, Box(123))
    // All occurrences of aliasedElem are replaced by arr(ii) 
    assert(arr(ii).value == 123)
    ii = (ii + 1)
    arr = arr.updated(ii, Box(456))
    assert(arr(ii).value == 123)
    ()
  }, arr)
}