Test/doomed/doomdebug.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
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44

procedure badtrace(x:int, y:int, z:int)
{
  var xin : int;
  xin := x+z;

  
  if (y>5) {
	xin:=5;
  } else {
	assert xin != x;
  }
}

procedure baddiamond(x:int, y:int, z:int)
{
	var xin : int;
	var yin : int;
	var zin : int;
	xin := x;
	yin := y;
	zin := z;
	
	if (y<5) {
		xin := xin -3;		
	} else {
		zin := zin +10;
		xin := 0;
	}
	
	if (x<100) {
		yin := 3;		
	} else {
		zin := 5;
	}
	
	if (z>5) {
		yin := yin - 2;
		xin := xin + 3;
	}

	zin:=zin+yin;
	
	assert xin!=x;	
}