[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: 0 2: int x1 = 0; 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) 0-5-pre = max(-inf, 0-6-pre) 1-5-pre = max(-inf, 1-6-pre) 2-5-pre = max(-inf, 2-6-pre) 0-5-0 = max(-inf, MCF<[0,0,0],[2:1,3:1,3:2]>(0-5-pre, 1-5-pre, 2-5-pre)) 1-5-0 = max(-inf, add(1, MCF<[0,0,0],[2:1,3:1,3:2]>(0-5-pre, 1-5-pre, 2-5-pre))) 2-5-0 = max(-inf, add(1, MCF<[0,0,0],[2:1,3:1,3:2]>(0-5-pre, 1-5-pre, 2-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) 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) 0-1-pre = max(-inf, 0-2-pre) 1-1-pre = max(-inf, 1-2-pre) 2-1-pre = max(-inf, 2-2-pre) 0-4-0 = max(-inf, add(2, MCF<[-1,1,0],[2:1,3:1,3:2]>(0-4-pre, 1-4-pre, 2-4-pre))) 1-4-0 = max(-inf, add(2, MCF<[-1,0,1],[2:1,3:1,3:2]>(0-4-pre, 1-4-pre, 2-4-pre))) 2-4-0 = max(-inf, MCF<[0,-1,1],[2:1,3:1,3:2]>(0-4-pre, 1-4-pre, 2-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) 0-0-pre = max(-inf, 0-1-pre) 1-0-pre = max(-inf, 1-1-pre) 2-0-pre = max(-inf, 2-1-pre) Block 0: x1 <= 10 x2 <= 11 x2-x1 <= 1 Block 1: x1 <= 10 x2 <= 11 x2-x1 <= 1 Block 2: x1 <= 10 x2 <= 11 x2-x1 <= 1 Block 3: x1 <= 10 x2 <= 11 x2-x1 <= 1 Block 4: x1 <= 8 x2 <= 11 x2-x1 <= 1 Block 5: x1 <= inf x2 <= inf x2-x1 <= inf Block 6: x1 <= inf x2 <= inf x2-x1 <= inf