Test/og/houd1.bpl


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24

// RUN: %boogie -noinfer -typeEncoding:m -useArrayTheory "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// XFAIL: *
const {:existential true} b0: bool;
const {:existential true} b1: bool;
const {:existential true} b2: bool;

var x:int;

procedure A()
{
  x := x + 1;
  yield;
}

procedure B()
{
  x := 5;
  yield;
  assert b0 ==> (x == 5);
  assert b1 ==> (x >= 5);
  assert b2 ==> (x >= 6);
}