Test/test2/LoopInvAssume.bpl


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

// RUN: %boogie -noinfer "%s" > "%t"
// RUN: %diff "%s.expect" "%t"
// Check that assumes in loop invariants are handled correctly

var x : int;

procedure Test()
  modifies x;
{
   entry:
      goto loophead, exit;

   loophead:
      assume x >= 0;
      x := 0;
      goto loophead, exit; 

   exit:
      assume x < 0;
      assert false;
      return;
}