diff options
Diffstat (limited to 'tex/thesis/implementation/experiments/fib-output')
| -rw-r--r-- | tex/thesis/implementation/experiments/fib-output | 409 |
1 files changed, 409 insertions, 0 deletions
diff --git a/tex/thesis/implementation/experiments/fib-output b/tex/thesis/implementation/experiments/fib-output new file mode 100644 index 0000000..900f636 --- /dev/null +++ b/tex/thesis/implementation/experiments/fib-output @@ -0,0 +1,409 @@ + + [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 |