Bug in program evaluation/verification

[mantognini]

This particular piece of code will trigger a postcondition violation on evaluation and an invalid verification with an empty counter example for _main but should not.

/* Copyright 2009-2016 EPFL, Lausanne */

import leon.annotation.extern

object Aliasing4 {

  case class MutableInteger(var x: Int)

  def selector(first: Boolean, i: MutableInteger, j: MutableInteger) {
    mutate(if (first) i else j)
  }

  def mutate(m: MutableInteger) {
    m.x = 0
  }

  def _main(): Int = {
    val a = MutableInteger(42)
    val b = MutableInteger(58)

    selector(first = true, a, b)

    if (a.x == 0) {
      if (b.x == 58) 0
      else 2
    } else 1
  } ensuring { _ == 0 }

  @extern
  def main(args: Array[String]): Unit = _main()
}

Running this program on the JVM yield no errors and _main indeed returns 0.

When this is fixed, src/test/resources/regression/genc/unverified/Aliasing4.scala should be moved to src/test/resources/regression/genc/valid/Aliasing4.scala (ATM only available on topic/genc_v2 branch).