Imperative code elimination, block lifting

[jad-hamza]

import stainless.lang._

object Test {
  def falseTheorem() = {
    false 
  } holds

  def test() = {
    val x = {
      falseTheorem()
      0
    }
    false 
  } holds
}

The verification condition for the post-condition of test is:

val tmp: Boolean = falseTheorem
val x: Int = 0
false

Would it be possible to just have the last two lines, without val tmp?
This would make the invocation of falseTheorem invisible to the solver for
proving the post-condition of test.
This way, we can have more control of what is visible in the path for the solvers.

I guess this comes from the ImperativeCodeElimination trait, that lifts value outside blocks?
I'll have a look

[samarion]

I don't think this is an issue anymore now that the simplifier drops such tmp values. Closing the issue.