Type encoding erases error[Nothing] to ()

[gsps]

In the following example

import stainless.lang._

object Error {
  def foo(x: Int): Unit = {
    if (x == 0) {
      error[Nothing]("Panic")
    } else {
      ()
    }
  }
}

type encoding is triggered, because we instantiated error at Nothing. After type encoding, that tree has been replaced by just (), so we miss the counterexample x == 0.

This presumably has something to do with the Unit type, in particular, as I couldn't recreate the same problematic behavior using any other primitive type. The problem also doesn't occur when we explicitly instantiate at the right type (error[Unit]).

[gsps]

It seems that when "unwrapping" an encoded expression e to Unit, we simply drop the expression and replace it by () at the moment (https://github.com/epfl-lara/stainless/blob/master/core/src/main/scala/stainless/extraction/oo/TypeEncoding.scala#L147). I suppose we should instead emit { e; () }, @samarion ?

[samarion]

Indeed, sounds like a reasonable fix.

You'll have to use a let-binding for e though, we don't have blocks at that point anymore.