Test/dafny4/Bug88.dfy


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18

// RUN: %dafny   "%s" > "%t"
// RUN: %diff "%s.expect" "%t"

lemma T(a: int) returns (b: int)
  ensures a == b
{
  calc {
    a;
  }
}

lemma A(i: int)
  ensures false
{
  if * {
  } else {
  }
}