[B6 (ENTRY)] Succs (1): B5 [B1] 1: x 2: [B1.1] (ImplicitCastExpr, LValueToRValue, int) 3: return [B1.2]; Preds (1): B2 Succs (1): B0 [B2] 1: x 2: [B2.1] (ImplicitCastExpr, LValueToRValue, int) 3: 10 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: x 2: [B4.1] (ImplicitCastExpr, LValueToRValue, int) 3: 1 4: [B4.2] + [B4.3] 5: x 6: [B4.5] = [B4.4] Preds (1): B2 Succs (1): B3 [B5] 1: 1 2: int x = 1; Preds (1): B6 Succs (1): B2 [B0 (EXIT)] Preds (1): B1 0-6-pre = max(-inf, inf) 1-6-pre = max(-inf, inf) 0-5-pre = max(-inf, 0-6-pre) 1-5-pre = max(-inf, 1-6-pre) 0-5-0 = max(-inf, add(1, MCF<[0,0],[2:1,1:2]>(0-5-pre, 1-5-pre))) 1-5-0 = max(-inf, add(-1, MCF<[0,0],[2:1,1:2]>(0-5-pre, 1-5-pre))) 0-2-pre = max(-inf, 0-5-0, 0-3-pre) 1-2-pre = max(-inf, 1-5-0, 1-3-pre) 0-4-pre = max(-inf, min(10, 0-2-pre)) 1-4-pre = max(-inf, 1-2-pre) 0-1-pre = max(-inf, 0-2-pre) 1-1-pre = max(-inf, min(-11, 1-2-pre)) 0-4-0 = max(-inf, add(1, MCF<[-1,1],[2:1,1:2]>(0-4-pre, 1-4-pre))) 1-4-0 = max(-inf, add(-1, MCF<[1,-1],[2:1,1:2]>(0-4-pre, 1-4-pre))) 0-3-pre = max(-inf, 0-4-0) 1-3-pre = max(-inf, 1-4-0) 0-0-pre = max(-inf, 0-1-pre) 1-0-pre = max(-inf, 1-1-pre) Block 0: x <= 11 -x <= -11 Block 1: x <= 11 -x <= -11 Block 2: x <= 11 -x <= -1 Block 3: x <= 11 -x <= -2 Block 4: x <= 10 -x <= -1 Block 5: x <= inf -x <= inf Block 6: x <= inf -x <= inf