summaryrefslogtreecommitdiff
path: root/Test/test21/NameClash.bpl
blob: 6e1ade489f0eed776cc17a6b69e2bdb628d5426e (plain)
1
2
3
4
5
6
7
8


function f(int) returns (int);
axiom f(13) == 0;

procedure P() returns () {
  assert (exists f:int :: 0 == f(f));
}