summaryrefslogtreecommitdiff
path: root/Test/test2/False.bpl
blob: 3fe148654b71f92b5aefde8375a1f37e911bd93c (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
procedure Test1()
{
   entry:
      assert !true == false;
      return;
}

procedure Test2()
{
   var b: bool;

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