method ReadInt() returns (y: int)

method foo(x: int) returns (z: int)
 requires x >= 0 //  && z < 0
//  ensures z >= 10
//  ensures z == x + 10
 ensures z >= x + 10
{
    return x + 10;
}

method Main() {
    assert 1 == 1;
    print "hello world\n";
    var w := foo(10);
    // assert w == 20;
    assert w >= 10;
    assert w >= 20;

    w := foo(0);
    assert !(-1 >= 0);
    // foo(-1);

    var y := ReadInt();
    if y < 0 {
        y := 0;
    }
    // assert y >= ;
    w := foo(y);
}