[B6 (ENTRY)]
   Succs (1): B5

 [B1]
   1: x2
   2: [B1.1] (ImplicitCastExpr, LValueToRValue, int)
   3: return [B1.2];
   Preds (1): B2
   Succs (1): B0

 [B2]
   1: x1
   2: [B2.1] (ImplicitCastExpr, LValueToRValue, int)
   3: 8
   4: [B2.2] <= [B2.3]
   T: while [B2.4]
   Preds (2): B3 B5
   Succs (2): B4 B1

 [B3]
   Preds (1): B4
   Succs (1): B2

 [B4]
   1: x1
   2: [B4.1] (ImplicitCastExpr, LValueToRValue, int)
   3: 2
   4: [B4.2] + [B4.3]
   5: x1
   6: [B4.5] = [B4.4]
   7: x2
   8: [B4.7] (ImplicitCastExpr, LValueToRValue, int)
   9: 2
  10: [B4.8] + [B4.9]
  11: x2
  12: [B4.11] = [B4.10]
   Preds (1): B2
   Succs (1): B3

 [B5]
   1: 1
   2: int x1 = 1;
   3: 1
   4: int x2 = 1;
   Preds (1): B6
   Succs (1): B2

 [B0 (EXIT)]
   Preds (1): B1

0-6-pre = max(-inf, inf)
1-6-pre = max(-inf, inf)
2-6-pre = max(-inf, inf)
3-6-pre = max(-inf, inf)
4-6-pre = max(-inf, inf)
5-6-pre = max(-inf, inf)
0-5-pre = max(-inf, 0-6-pre)
1-5-pre = max(-inf, 1-6-pre)
2-5-pre = max(-inf, 2-6-pre)
3-5-pre = max(-inf, 3-6-pre)
4-5-pre = max(-inf, 4-6-pre)
5-5-pre = max(-inf, 5-6-pre)
0-5-0 = max(-inf, add(1, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre)))
1-5-0 = max(-inf, add(-1, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre)))
2-5-0 = max(-inf, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre))
3-5-0 = max(-inf, add(1, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre)))
4-5-0 = max(-inf, add(-1, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre)))
5-5-0 = max(-inf, MCF<[0,0,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre))
0-2-pre = max(-inf, 0-5-0, 0-3-pre)
1-2-pre = max(-inf, 1-5-0, 1-3-pre)
2-2-pre = max(-inf, 2-5-0, 2-3-pre)
3-2-pre = max(-inf, 3-5-0, 3-3-pre)
4-2-pre = max(-inf, 4-5-0, 4-3-pre)
5-2-pre = max(-inf, 5-5-0, 5-3-pre)
0-4-pre = max(-inf, min(8, 0-2-pre))
1-4-pre = max(-inf, 1-2-pre)
2-4-pre = max(-inf, 2-2-pre)
3-4-pre = max(-inf, 3-2-pre)
4-4-pre = max(-inf, 4-2-pre)
5-4-pre = max(-inf, 5-2-pre)
0-1-pre = max(-inf, 0-2-pre)
1-1-pre = max(-inf, min(-9, 1-2-pre))
2-1-pre = max(-inf, 2-2-pre)
3-1-pre = max(-inf, 3-2-pre)
4-1-pre = max(-inf, 4-2-pre)
5-1-pre = max(-inf, 5-2-pre)
0-4-0 = max(-inf, add(2, MCF<[-1,1,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre)))
1-4-0 = max(-inf, add(-2, MCF<[1,-1,0],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre)))
2-4-0 = max(-inf, MCF<[0,1,-1],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre))
3-4-0 = max(-inf, add(2, MCF<[-1,0,1],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre)))
4-4-0 = max(-inf, add(-2, MCF<[1,0,-1],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre)))
5-4-0 = max(-inf, MCF<[0,-1,1],[2:1,1:2,2:3,3:1,1:3,3:2]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre))
0-3-pre = max(-inf, 0-4-0)
1-3-pre = max(-inf, 1-4-0)
2-3-pre = max(-inf, 2-4-0)
3-3-pre = max(-inf, 3-4-0)
4-3-pre = max(-inf, 4-4-0)
5-3-pre = max(-inf, 5-4-0)
0-0-pre = max(-inf, 0-1-pre)
1-0-pre = max(-inf, 1-1-pre)
2-0-pre = max(-inf, 2-1-pre)
3-0-pre = max(-inf, 3-1-pre)
4-0-pre = max(-inf, 4-1-pre)
5-0-pre = max(-inf, 5-1-pre)

Block 0: 
	x1 <= 10
	-x1 <= -9
	x1 - x2 <= 0
	x2 <= 10
	-x2 <= -1
	x2 - x1 <= 0
Block 1: 
	x1 <= 10
	-x1 <= -9
	x1 - x2 <= 0
	x2 <= 10
	-x2 <= -1
	x2 - x1 <= 0
Block 2: 
	x1 <= 10
	-x1 <= -1
	x1 - x2 <= 0
	x2 <= 10
	-x2 <= -1
	x2 - x1 <= 0
Block 3: 
	x1 <= 10
	-x1 <= -3
	x1 - x2 <= 0
	x2 <= 10
	-x2 <= -3
	x2 - x1 <= 0
Block 4: 
	x1 <= 8
	-x1 <= -1
	x1 - x2 <= 0
	x2 <= 10
	-x2 <= -1
	x2 - x1 <= 0
Block 5: 
	x1 <= inf
	-x1 <= inf
	x1 - x2 <= inf
	x2 <= inf
	-x2 <= inf
	x2 - x1 <= inf
Block 6: 
	x1 <= inf
	-x1 <= inf
	x1 - x2 <= inf
	x2 <= inf
	-x2 <= inf
	x2 - x1 <= inf