Function not equal to its body when using extern annotations

[andreagilot-da]

The following snippet does not verify although it is only asserting that foo is equal to its body:

  case class A(useless: BigInt) {
    @extern
    def map(f: (Unit) => (Unit, Unit)): A = this
  }

  def get(key: Unit): Option[Unit] = None[Unit]()

  def foo(m: A): A = {
    m.map {
      key =>
        val value = get(key) match {
          case None() => ()
          case Some(_) => ()
        }
        () -> value
    }
  }

  def fooEqualsItsBody(m: A): Unit = {
    assert(foo(m) == m.map {
      key =>
        val value = get(key) match {
          case None() => ()
          case Some(_) => ()
        }
        () -> value
    })
  }

The followings make the verification succeed:

• Inlining value
• Removing the @externannotation on map
• Changing get so that it takes no argument instead of one
• Making map return only one value instead of a pair
• Removing the useless argument from A
• Changing value by () or by get(key)

[mario-bucev]

May be another instance of epfl-lara/inox#139