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