Test/symdiff/foo.bpl


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

// RUN: %boogie -z3multipleErrors -errorTrace:0 %s > %t
// RUN: %diff %s.expect %t
procedure Foo(x:int) 
{
  var ok:bool;
  
  ok := true;  

  if (x == 1) {
     ok := false;
  } else if (x == 2) {
     ok := false;
  } else if (x == 3) {
     ok := false;
  }
    
  assert ok;

}