id ( x : int | y : int ) {
    assume x > 0;
    y := x;
    assert y > 0
}