VC timeout for Z3 in incremental mode

[jad-hamza]

This is an example that seems to be solved by Z3 in non-incremental mode, but times out with incremental mode. We can add it to the test suite if we switch.

import stainless.annotation._
import stainless.lang._

object IfProp {
  @extern
  def prop(j: Int): Boolean = {
    (??? : Boolean)
  }

  def gg(cond: Boolean, x1: Int, x2: Int): Unit = {
    require(
      x1 >= 0 &&
      x2 >= 0 &&
      prop(x1 - 1) &&
      prop(x2 - 1)
    )

    val x = if (cond) x1 else x2
    assert(prop(x - 1))
  }
}