// stainless example.scala --debug=smt --solvers=smt-cvc5 --vc-cache=false
import stainless.lang.*
import stainless.lang.StaticChecks.*
case class FirstExample(var x: BigInt, var y: BigInt):
  def increase : Unit = {
    x = x + 2     // change the value of x
    y = x + 10    // refer to changed value
  }.ensuring(_ => old(this).x > 0 ==> (x > 2 && y > 12)) // relates old and new values
