summaryrefslogtreecommitdiff
path: root/Test/codeexpr/codeExprBug.bpl
blob: e1ae938c3c16d61a7c2736129a80c60173868f13 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
// RUN: %boogie "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
procedure p() returns ($r: int);
  ensures |{ $bb0: return ($r == 1); }|;

implementation p() returns ($x: int)
{
  $x := 1;
  return;
}

procedure q()
  ensures |{ var $b: bool; $0: $b := true; goto $1; $1: return $b; }|;
{
}