summaryrefslogtreecommitdiff
path: root/Test/snapshots/Snapshots38.v2.bpl
blob: 5c4b69d6068ea271898db8c88ea1528c5b025dff (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
procedure {:checksum "-1"} Callee();

implementation {:id "Callee"} {:checksum "2"} Callee()
{
    var r: int;

    call r := Sum(42);
    assert r != 0;
    assert 42 <= r;
}

procedure {:checksum "3"} Sum(n: int) returns (r: int);
  requires 0 <= n;
  ensures n != 0 ==> n <= r;