import leon.lang._
import leon.annotation._
import leon._

object Operators {

  def foo(a: Int): Int = {
    require(a > 0)

    {
      val b = a
      assert(b > 0, "Hey now")
      b + bar(1)
    } ensuring { _ < 2 }

  } ensuring {
    _ > a
  }

  def bar(a: Int): Int = {
    require(a > 0)

    {
      val b = a
      assert(b > 0, "Hey now")
      b + 2
    } ensuring { _ > 2 }

  } ensuring {
    _ > a
  }
}

import leon.lang._
import leon.annotation._
import leon._

object Operators {

  def foo(a: Int): Int = {
    require(a > 0)
    val b = a
    assert(b > 0, "Hey now")
    b + bar(1)
  } ensuring { res =>
    res > a && res < 2
  }

  def bar(a: Int): Int = {
    require(a > 0)
    val b = a
    assert(b > 0, "Hey now")
    b + 2
  } ensuring { res =>
    res > a && res > 2
  }
}

Rename Passes to Gives, and further integration
Rename Passes to Gives, and further integration
