[B6 (ENTRY)] Succs (1): B5 [B1] 1: fib 2: [B1.1] (ImplicitCastExpr, LValueToRValue, int) 3: return [B1.2]; Preds (1): B2 Succs (1): B0 [B2] 1: i 2: [B2.1] (ImplicitCastExpr, LValueToRValue, int) 3: 20 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: fib 2: [B4.1] (ImplicitCastExpr, LValueToRValue, int) 3: int temp_fib = fib; 4: fib 5: [B4.4] (ImplicitCastExpr, LValueToRValue, int) 6: fib_last 7: [B4.6] (ImplicitCastExpr, LValueToRValue, int) 8: [B4.5] + [B4.7] 9: fib 10: [B4.9] = [B4.8] 11: temp_fib 12: [B4.11] (ImplicitCastExpr, LValueToRValue, int) 13: fib_last 14: [B4.13] = [B4.12] 15: i 16: [B4.15] (ImplicitCastExpr, LValueToRValue, int) 17: 1 18: [B4.16] + [B4.17] 19: i 20: [B4.19] = [B4.18] Preds (1): B2 Succs (1): B3 [B5] 1: 0 2: int fib_last = 0; 3: 1 4: int fib = 1; 5: 0 6: int i = 0; 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) 6-6-pre = max(-inf, inf) 7-6-pre = max(-inf, inf) 8-6-pre = max(-inf, inf) 9-6-pre = max(-inf, inf) 10-6-pre = max(-inf, inf) 11-6-pre = max(-inf, inf) 12-6-pre = max(-inf, inf) 13-6-pre = max(-inf, inf) 14-6-pre = max(-inf, inf) 15-6-pre = max(-inf, inf) 16-6-pre = max(-inf, inf) 17-6-pre = max(-inf, inf) 18-6-pre = max(-inf, inf) 19-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) 6-5-pre = max(-inf, 6-6-pre) 7-5-pre = max(-inf, 7-6-pre) 8-5-pre = max(-inf, 8-6-pre) 9-5-pre = max(-inf, 9-6-pre) 10-5-pre = max(-inf, 10-6-pre) 11-5-pre = max(-inf, 11-6-pre) 12-5-pre = max(-inf, 12-6-pre) 13-5-pre = max(-inf, 13-6-pre) 14-5-pre = max(-inf, 14-6-pre) 15-5-pre = max(-inf, 15-6-pre) 16-5-pre = max(-inf, 16-6-pre) 17-5-pre = max(-inf, 17-6-pre) 18-5-pre = max(-inf, 18-6-pre) 19-5-pre = max(-inf, 19-6-pre) 0-5-0 = max(-inf, add(1, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))) 1-5-0 = max(-inf, add(-1, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))) 2-5-0 = max(-inf, add(1, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))) 3-5-0 = max(-inf, add(1, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))) 4-5-0 = max(-inf, add(1, MCF<[1,0,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))) 5-5-0 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) 6-5-0 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) 7-5-0 = max(-inf, add(-1, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))) 8-5-0 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) 9-5-0 = max(-inf, MCF<[1,0,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) 10-5-0 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) 11-5-0 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) 12-5-0 = max(-inf, add(-1, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))) 13-5-0 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) 14-5-0 = max(-inf, MCF<[1,0,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) 15-5-0 = max(-inf, MCF<[-1,0,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) 16-5-0 = max(-inf, MCF<[1,0,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) 17-5-0 = max(-inf, add(-1, MCF<[-1,0,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre))) 18-5-0 = max(-inf, MCF<[-1,0,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-5-pre)) 19-5-0 = max(-inf, MCF<[-1,0,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-5-pre, 1-5-pre, 2-5-pre, 3-5-pre, 4-5-pre, 5-5-pre, 6-5-pre, 7-5-pre, 8-5-pre, 9-5-pre, 10-5-pre, 11-5-pre, 12-5-pre, 13-5-pre, 14-5-pre, 15-5-pre, 16-5-pre, 17-5-pre, 18-5-pre, 19-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) 6-2-pre = max(-inf, 6-5-0, 6-3-pre) 7-2-pre = max(-inf, 7-5-0, 7-3-pre) 8-2-pre = max(-inf, 8-5-0, 8-3-pre) 9-2-pre = max(-inf, 9-5-0, 9-3-pre) 10-2-pre = max(-inf, 10-5-0, 10-3-pre) 11-2-pre = max(-inf, 11-5-0, 11-3-pre) 12-2-pre = max(-inf, 12-5-0, 12-3-pre) 13-2-pre = max(-inf, 13-5-0, 13-3-pre) 14-2-pre = max(-inf, 14-5-0, 14-3-pre) 15-2-pre = max(-inf, 15-5-0, 15-3-pre) 16-2-pre = max(-inf, 16-5-0, 16-3-pre) 17-2-pre = max(-inf, 17-5-0, 17-3-pre) 18-2-pre = max(-inf, 18-5-0, 18-3-pre) 19-2-pre = max(-inf, 19-5-0, 19-3-pre) 0-4-pre = max(-inf, 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) 6-4-pre = max(-inf, 6-2-pre) 7-4-pre = max(-inf, 7-2-pre) 8-4-pre = max(-inf, 8-2-pre) 9-4-pre = max(-inf, 9-2-pre) 10-4-pre = max(-inf, min(19, 10-2-pre)) 11-4-pre = max(-inf, 11-2-pre) 12-4-pre = max(-inf, 12-2-pre) 13-4-pre = max(-inf, 13-2-pre) 14-4-pre = max(-inf, 14-2-pre) 15-4-pre = max(-inf, 15-2-pre) 16-4-pre = max(-inf, 16-2-pre) 17-4-pre = max(-inf, 17-2-pre) 18-4-pre = max(-inf, 18-2-pre) 19-4-pre = max(-inf, 19-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) 3-1-pre = max(-inf, 3-2-pre) 4-1-pre = max(-inf, 4-2-pre) 5-1-pre = max(-inf, 5-2-pre) 6-1-pre = max(-inf, 6-2-pre) 7-1-pre = max(-inf, 7-2-pre) 8-1-pre = max(-inf, 8-2-pre) 9-1-pre = max(-inf, 9-2-pre) 10-1-pre = max(-inf, 10-2-pre) 11-1-pre = max(-inf, min(-20, 11-2-pre)) 12-1-pre = max(-inf, 12-2-pre) 13-1-pre = max(-inf, 13-2-pre) 14-1-pre = max(-inf, 14-2-pre) 15-1-pre = max(-inf, 15-2-pre) 16-1-pre = max(-inf, 16-2-pre) 17-1-pre = max(-inf, 17-2-pre) 18-1-pre = max(-inf, 18-2-pre) 19-1-pre = max(-inf, 19-2-pre) 0-4-0 = max(-inf, MCF<[-2,1,1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 1-4-0 = max(-inf, MCF<[2,-1,-1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 2-4-0 = max(-inf, MCF<[-1,1,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 3-4-0 = max(-inf, MCF<[-1,1,1,-1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 4-4-0 = max(-inf, MCF<[-1,0,1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 5-4-0 = max(-inf, MCF<[-1,0,1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 6-4-0 = max(-inf, MCF<[1,0,-1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 7-4-0 = max(-inf, MCF<[1,-1,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 8-4-0 = max(-inf, MCF<[0,0,1,-1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 9-4-0 = max(-inf, MCF<[0,-1,1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 10-4-0 = max(-inf, MCF<[-1,0,0,1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 11-4-0 = max(-inf, MCF<[1,0,0,-1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 12-4-0 = max(-inf, MCF<[1,-1,-1,1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 13-4-0 = max(-inf, MCF<[0,0,-1,1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 14-4-0 = max(-inf, MCF<[0,-1,0,1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 15-4-0 = max(-inf, MCF<[-1,1,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 16-4-0 = max(-inf, MCF<[1,-1,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 17-4-0 = max(-inf, MCF<[1,0,-1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 18-4-0 = max(-inf, MCF<[0,1,-1,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 19-4-0 = max(-inf, MCF<[0,1,0,-1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-pre, 1-4-pre, 2-4-pre, 3-4-pre, 4-4-pre, 5-4-pre, 6-4-pre, 7-4-pre, 8-4-pre, 9-4-pre, 10-4-pre, 11-4-pre, 12-4-pre, 13-4-pre, 14-4-pre, 15-4-pre, 16-4-pre, 17-4-pre, 18-4-pre, 19-4-pre)) 0-4-1 = max(-inf, MCF<[-1,1,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) 1-4-1 = max(-inf, MCF<[1,-1,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) 2-4-1 = max(-inf, MCF<[0,1,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) 3-4-1 = max(-inf, add(-1, MCF<[0,1,0,-1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))) 4-4-1 = max(-inf, MCF<[0,1,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) 5-4-1 = max(-inf, MCF<[-1,0,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) 6-4-1 = max(-inf, MCF<[1,0,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) 7-4-1 = max(-inf, MCF<[0,-1,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) 8-4-1 = max(-inf, add(-1, MCF<[0,0,0,-1,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))) 9-4-1 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) 10-4-1 = max(-inf, add(1, MCF<[-1,0,0,1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))) 11-4-1 = max(-inf, add(-1, MCF<[1,0,0,-1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))) 12-4-1 = max(-inf, add(1, MCF<[0,-1,0,1,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))) 13-4-1 = max(-inf, add(1, MCF<[0,0,0,1,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))) 14-4-1 = max(-inf, add(1, MCF<[0,0,0,1,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))) 15-4-1 = max(-inf, MCF<[-1,0,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) 16-4-1 = max(-inf, MCF<[1,0,0,0,-1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) 17-4-1 = max(-inf, MCF<[0,-1,0,0,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) 18-4-1 = max(-inf, MCF<[0,0,0,0,0],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0)) 19-4-1 = max(-inf, add(-1, MCF<[0,0,0,-1,1],[2:1,1:2,2:3,2:4,2:5,3:1,1:3,3:2,3:4,3:5,4:1,1:4,4:2,4:3,4:5,5:1,1:5,5:2,5:3,5:4]>(0-4-0, 1-4-0, 2-4-0, 3-4-0, 4-4-0, 5-4-0, 6-4-0, 7-4-0, 8-4-0, 9-4-0, 10-4-0, 11-4-0, 12-4-0, 13-4-0, 14-4-0, 15-4-0, 16-4-0, 17-4-0, 18-4-0, 19-4-0))) 0-3-pre = max(-inf, 0-4-1) 1-3-pre = max(-inf, 1-4-1) 2-3-pre = max(-inf, 2-4-1) 3-3-pre = max(-inf, 3-4-1) 4-3-pre = max(-inf, 4-4-1) 5-3-pre = max(-inf, 5-4-1) 6-3-pre = max(-inf, 6-4-1) 7-3-pre = max(-inf, 7-4-1) 8-3-pre = max(-inf, 8-4-1) 9-3-pre = max(-inf, 9-4-1) 10-3-pre = max(-inf, 10-4-1) 11-3-pre = max(-inf, 11-4-1) 12-3-pre = max(-inf, 12-4-1) 13-3-pre = max(-inf, 13-4-1) 14-3-pre = max(-inf, 14-4-1) 15-3-pre = max(-inf, 15-4-1) 16-3-pre = max(-inf, 16-4-1) 17-3-pre = max(-inf, 17-4-1) 18-3-pre = max(-inf, 18-4-1) 19-3-pre = max(-inf, 19-4-1) 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) 6-0-pre = max(-inf, 6-1-pre) 7-0-pre = max(-inf, 7-1-pre) 8-0-pre = max(-inf, 8-1-pre) 9-0-pre = max(-inf, 9-1-pre) 10-0-pre = max(-inf, 10-1-pre) 11-0-pre = max(-inf, 11-1-pre) 12-0-pre = max(-inf, 12-1-pre) 13-0-pre = max(-inf, 13-1-pre) 14-0-pre = max(-inf, 14-1-pre) 15-0-pre = max(-inf, 15-1-pre) 16-0-pre = max(-inf, 16-1-pre) 17-0-pre = max(-inf, 17-1-pre) 18-0-pre = max(-inf, 18-1-pre) 19-0-pre = max(-inf, 19-1-pre) Block 0: fib <= 1 -fib <= -1 fib - fib_last <= 1 fib - i <= 1 fib - temp_fib <= inf fib_last <= 1 -fib_last <= 0 fib_last - fib <= 0 fib_last - i <= 0 fib_last - temp_fib <= inf i <= 20 -i <= -20 i - fib <= 19 i - fib_last <= 19 i - temp_fib <= inf temp_fib <= inf -temp_fib <= inf temp_fib - fib <= inf temp_fib - fib_last <= inf temp_fib - i <= inf Block 1: fib <= 1 -fib <= -1 fib - fib_last <= 1 fib - i <= 1 fib - temp_fib <= inf fib_last <= 1 -fib_last <= 0 fib_last - fib <= 0 fib_last - i <= 0 fib_last - temp_fib <= inf i <= 20 -i <= -20 i - fib <= 19 i - fib_last <= 19 i - temp_fib <= inf temp_fib <= inf -temp_fib <= inf temp_fib - fib <= inf temp_fib - fib_last <= inf temp_fib - i <= inf Block 2: fib <= 39 -fib <= -1 fib - fib_last <= 19 fib - i <= 37 fib - temp_fib <= inf fib_last <= 38 -fib_last <= 0 fib_last - fib <= 0 fib_last - i <= inf fib_last - temp_fib <= inf i <= 20 -i <= 0 i - fib <= 19 i - fib_last <= 19 i - temp_fib <= inf temp_fib <= inf -temp_fib <= inf temp_fib - fib <= inf temp_fib - fib_last <= inf temp_fib - i <= inf Block 3: fib <= inf -fib <= -1 fib - fib_last <= inf fib - i <= inf fib - temp_fib <= inf fib_last <= inf -fib_last <= -1 fib_last - fib <= 0 fib_last - i <= inf fib_last - temp_fib <= 0 i <= 20 -i <= -1 i - fib <= 19 i - fib_last <= 19 i - temp_fib <= 19 temp_fib <= inf -temp_fib <= -1 temp_fib - fib <= 0 temp_fib - fib_last <= 0 temp_fib - i <= inf Block 4: fib <= inf -fib <= -1 fib - fib_last <= inf fib - i <= inf fib - temp_fib <= inf fib_last <= inf -fib_last <= 0 fib_last - fib <= 0 fib_last - i <= inf fib_last - temp_fib <= inf i <= 19 -i <= 0 i - fib <= 19 i - fib_last <= 19 i - temp_fib <= inf temp_fib <= inf -temp_fib <= inf temp_fib - fib <= inf temp_fib - fib_last <= inf temp_fib - i <= inf Block 5: fib <= inf -fib <= inf fib - fib_last <= inf fib - i <= inf fib - temp_fib <= inf fib_last <= inf -fib_last <= inf fib_last - fib <= inf fib_last - i <= inf fib_last - temp_fib <= inf i <= inf -i <= inf i - fib <= inf i - fib_last <= inf i - temp_fib <= inf temp_fib <= inf -temp_fib <= inf temp_fib - fib <= inf temp_fib - fib_last <= inf temp_fib - i <= inf Block 6: fib <= inf -fib <= inf fib - fib_last <= inf fib - i <= inf fib - temp_fib <= inf fib_last <= inf -fib_last <= inf fib_last - fib <= inf fib_last - i <= inf fib_last - temp_fib <= inf i <= inf -i <= inf i - fib <= inf i - fib_last <= inf i - temp_fib <= inf temp_fib <= inf -temp_fib <= inf temp_fib - fib <= inf temp_fib - fib_last <= inf temp_fib - i <= inf