import stainless.lang._

object Eval {
  def foo: Int = {
    // assert(false)
    43
  } ensuring { _ + 58 == 100 }

  def goo = 1

  def bar = { "hello, stainless!" } ensuring { _ => 0 < goo }

  def foobar = { "failure in foo's PC" } ensuring { _ => 0 < foo }

  def loop = {
    var x = 0
    while (x < 10) {
      // x += 1
    }
    true
  }.holds
}