Test/test2/False.bpl


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

// RUN: %boogie -noinfer %s > %t
// RUN: %diff %s.expect %t
procedure Test1()
{
   entry:
      assert !true == false;
      return;
}

procedure Test2()
{
   var b: bool;

   entry:
      assume b != false;
      assert b;
      return;
}