VC timeout for Z3

[jad-hamza]

Not really a Stainless issue, but we can leave this open until this works better in Z3. This example generates a VC for the assertion, which is hard to solve for Z3 due to a mix of features. Here is a simplified version of the SMT file generated for Z3: https://github.com/Z3Prover/z3/issues/5168

This example works well with CVC4.

This is similar to https://github.com/epfl-lara/stainless/issues/979, but different in the sense that Z3 times out even in non-incremental mode.

stainless Example.scala --solvers=smt-z3 --timeout=10 --debug=verification,solver --vc-cache=false

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

case class Wrap(n: Int)

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

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

    assert(prop((if (cond) x1 else x2).n - 1))
  }

}