Demo.scala

import stainless.annotation._

object Demo {

  def f(x: BigInt, y: BigInt): BigInt = {
    require(x >= 0 && y >= 1)
    x * y
  }.ensuring(res =>
    res >= x
  )

  def g(z: BigInt): Unit = {
    require(z >= 10)

    val r1 = f(z, z)
    val r2 = f(10, 5)
    val r3 = f(z, 3)

    assert(r3 >= 3)
    assert(r2 == 50)
  }

  @extern
  def main(args: Array[String]): Unit = {
    println(f(100, 20))
  }

}