Test/test21/Orderings2.bpl


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


const b:int;
const a:int extends b complete;

const c:int extends a;
const d:int extends a;

procedure P() returns () {
  var x:int;

  assert c <: b && d <: a;

  assume x <: a && !(x <: c) && x != a;
  assert x <: d;

  assert b <: x;            // should not be provable
}