method m_unproven(x:int) returns (y:int)
  ensures y == 2*x;
{
}

function f(x:int) : int
{
  2*x
}