Trying to load file: main.koat Initial Control flow graph problem: Start location: f0 0: f0 -> f154 : A'=0, B'=2, C'=0, [], cost: 1 1: f154 -> f154 : A'=C+A, C'=1+C, [ 2>=C ], cost: 1 240: f154 -> f160 : C'=0, [ C>=3 ], cost: 1 2: f160 -> f160 : A'=C+A, C'=1+C, [ 3>=C ], cost: 1 239: f160 -> f166 : C'=0, [ C>=4 ], cost: 1 3: f166 -> f166 : A'=C+A, C'=1+C, [ 2>=C ], cost: 1 238: f166 -> f172 : C'=0, [ C>=3 ], cost: 1 4: f172 -> f172 : A'=C+A, C'=1+C, [ 3>=C ], cost: 1 237: f172 -> f180 : C'=1, [ C>=4 ], cost: 1 5: f180 -> f180 : A'=C+A, C'=1+C, [ 1>=C ], cost: 1 236: f180 -> f186 : C'=1, [ C>=2 ], cost: 1 6: f186 -> f186 : A'=C+A, C'=1+C, [ 2>=C ], cost: 1 235: f186 -> f192 : C'=1, [ C>=3 ], cost: 1 7: f192 -> f192 : A'=C+A, C'=1+C, [ 1>=C ], cost: 1 234: f192 -> f198 : C'=1, [ C>=2 ], cost: 1 8: f198 -> f198 : A'=C+A, C'=1+C, [ 2>=C ], cost: 1 233: f198 -> f206 : C'=-3, [ C>=3 ], cost: 1 9: f206 -> f206 : A'=C+A, C'=1+C, [ 0>=3+C ], cost: 1 232: f206 -> f212 : C'=-3, [ 2+C>=0 ], cost: 1 10: f212 -> f212 : A'=C+A, C'=1+C, [ 0>=2+C ], cost: 1 231: f212 -> f218 : C'=-3, [ 1+C>=0 ], cost: 1 11: f218 -> f218 : A'=C+A, C'=1+C, [ 0>=3+C ], cost: 1 230: f218 -> f224 : C'=-3, [ 2+C>=0 ], cost: 1 12: f224 -> f224 : A'=C+A, C'=1+C, [ 0>=2+C ], cost: 1 229: f224 -> f232 : C'=-4, [ 1+C>=0 ], cost: 1 13: f232 -> f232 : A'=C+A, C'=1+C, [ 0>=2+C ], cost: 1 228: f232 -> f238 : C'=-4, [ 1+C>=0 ], cost: 1 14: f238 -> f238 : A'=C+A, C'=1+C, [ 0>=1+C ], cost: 1 227: f238 -> f244 : C'=-4, [ C>=0 ], cost: 1 15: f244 -> f244 : A'=C+A, C'=1+C, [ 0>=2+C ], cost: 1 226: f244 -> f250 : C'=-4, [ 1+C>=0 ], cost: 1 16: f250 -> f250 : A'=C+A, C'=1+C, [ 0>=1+C ], cost: 1 225: f250 -> f258 : C'=-5, [ C>=0 ], cost: 1 17: f258 -> f258 : A'=C+A, C'=1+C, [ 0>=1+C ], cost: 1 224: f258 -> f264 : C'=-5, [ C>=0 ], cost: 1 18: f264 -> f264 : A'=C+A, C'=1+C, [ 0>=C ], cost: 1 223: f264 -> f270 : C'=-5, [ C>=1 ], cost: 1 19: f270 -> f270 : A'=C+A, C'=1+C, [ 0>=1+C ], cost: 1 222: f270 -> f276 : C'=-5, [ C>=0 ], cost: 1 20: f276 -> f276 : A'=C+A, C'=1+C, [ 0>=C ], cost: 1 221: f276 -> f284 : C'=-6, [ C>=1 ], cost: 1 21: f284 -> f284 : A'=C+A, C'=1+C, [ 3>=C ], cost: 1 220: f284 -> f290 : C'=-6, [ C>=4 ], cost: 1 22: f290 -> f290 : A'=C+A, C'=1+C, [ 4>=C ], cost: 1 219: f290 -> f296 : C'=-6, [ C>=5 ], cost: 1 23: f296 -> f296 : A'=C+A, C'=1+C, [ 3>=C ], cost: 1 218: f296 -> f302 : C'=-6, [ C>=4 ], cost: 1 24: f302 -> f302 : A'=C+A, C'=1+C, [ 4>=C ], cost: 1 217: f302 -> f310 : C'=0, [ C>=5 ], cost: 1 25: f310 -> f310 : A'=C+A, C'=B+C, [ 2>=C ], cost: 1 216: f310 -> f316 : C'=0, [ C>=3 ], cost: 1 26: f316 -> f316 : A'=C+A, C'=B+C, [ 3>=C ], cost: 1 215: f316 -> f322 : C'=0, [ C>=4 ], cost: 1 27: f322 -> f322 : A'=C+A, C'=B+C, [ 2>=C ], cost: 1 214: f322 -> f328 : C'=0, [ C>=3 ], cost: 1 28: f328 -> f328 : A'=C+A, C'=B+C, [ 3>=C ], cost: 1 213: f328 -> f336 : C'=1, [ C>=4 ], cost: 1 29: f336 -> f336 : A'=C+A, C'=B+C, [ 1>=C ], cost: 1 212: f336 -> f342 : C'=1, [ C>=2 ], cost: 1 30: f342 -> f342 : A'=C+A, C'=B+C, [ 2>=C ], cost: 1 211: f342 -> f348 : C'=1, [ C>=3 ], cost: 1 31: f348 -> f348 : A'=C+A, C'=B+C, [ 1>=C ], cost: 1 210: f348 -> f354 : C'=1, [ C>=2 ], cost: 1 32: f354 -> f354 : A'=C+A, C'=B+C, [ 2>=C ], cost: 1 209: f354 -> f362 : C'=-3, [ C>=3 ], cost: 1 33: f362 -> f362 : A'=C+A, C'=B+C, [ 0>=3+C ], cost: 1 208: f362 -> f368 : C'=-3, [ 2+C>=0 ], cost: 1 34: f368 -> f368 : A'=C+A, C'=B+C, [ 0>=2+C ], cost: 1 207: f368 -> f374 : C'=-3, [ 1+C>=0 ], cost: 1 35: f374 -> f374 : A'=C+A, C'=B+C, [ 0>=3+C ], cost: 1 206: f374 -> f380 : C'=-3, [ 2+C>=0 ], cost: 1 36: f380 -> f380 : A'=C+A, C'=B+C, [ 0>=2+C ], cost: 1 205: f380 -> f388 : C'=-4, [ 1+C>=0 ], cost: 1 37: f388 -> f388 : A'=C+A, C'=B+C, [ 0>=2+C ], cost: 1 204: f388 -> f394 : C'=-4, [ 1+C>=0 ], cost: 1 38: f394 -> f394 : A'=C+A, C'=B+C, [ 0>=1+C ], cost: 1 203: f394 -> f400 : C'=-4, [ C>=0 ], cost: 1 39: f400 -> f400 : A'=C+A, C'=B+C, [ 0>=2+C ], cost: 1 202: f400 -> f406 : C'=-4, [ 1+C>=0 ], cost: 1 40: f406 -> f406 : A'=C+A, C'=B+C, [ 0>=1+C ], cost: 1 201: f406 -> f414 : C'=-5, [ C>=0 ], cost: 1 41: f414 -> f414 : A'=C+A, C'=B+C, [ 0>=1+C ], cost: 1 200: f414 -> f420 : C'=-5, [ C>=0 ], cost: 1 42: f420 -> f420 : A'=C+A, C'=B+C, [ 0>=C ], cost: 1 199: f420 -> f426 : C'=-5, [ C>=1 ], cost: 1 43: f426 -> f426 : A'=C+A, C'=B+C, [ 0>=1+C ], cost: 1 198: f426 -> f432 : C'=-5, [ C>=0 ], cost: 1 44: f432 -> f432 : A'=C+A, C'=B+C, [ 0>=C ], cost: 1 197: f432 -> f440 : C'=-6, [ C>=1 ], cost: 1 45: f440 -> f440 : A'=C+A, C'=B+C, [ 3>=C ], cost: 1 196: f440 -> f446 : C'=-6, [ C>=4 ], cost: 1 46: f446 -> f446 : A'=C+A, C'=B+C, [ 4>=C ], cost: 1 195: f446 -> f452 : C'=-6, [ C>=5 ], cost: 1 47: f452 -> f452 : A'=C+A, C'=B+C, [ 3>=C ], cost: 1 194: f452 -> f458 : C'=-6, [ C>=4 ], cost: 1 48: f458 -> f458 : A'=C+A, C'=B+C, [ 4>=C ], cost: 1 193: f458 -> f466 : C'=5, [ C>=5 ], cost: 1 49: f466 -> f466 : A'=C+A, C'=-1+C, [ C>=3 ], cost: 1 192: f466 -> f472 : C'=5, [ 2>=C ], cost: 1 50: f472 -> f472 : A'=C+A, C'=-1+C, [ C>=2 ], cost: 1 191: f472 -> f478 : C'=5, [ 1>=C ], cost: 1 51: f478 -> f478 : A'=C+A, C'=-1+C, [ C>=3 ], cost: 1 190: f478 -> f484 : C'=5, [ 2>=C ], cost: 1 52: f484 -> f484 : A'=C+A, C'=-1+C, [ C>=2 ], cost: 1 189: f484 -> f492 : C'=6, [ 1>=C ], cost: 1 53: f492 -> f492 : A'=C+A, C'=-1+C, [ C>=2 ], cost: 1 188: f492 -> f498 : C'=6, [ 1>=C ], cost: 1 54: f498 -> f498 : A'=C+A, C'=-1+C, [ C>=1 ], cost: 1 187: f498 -> f504 : C'=6, [ 0>=C ], cost: 1 55: f504 -> f504 : A'=C+A, C'=-1+C, [ C>=2 ], cost: 1 186: f504 -> f510 : C'=6, [ 1>=C ], cost: 1 56: f510 -> f510 : A'=C+A, C'=-1+C, [ C>=1 ], cost: 1 185: f510 -> f518 : C'=7, [ 0>=C ], cost: 1 57: f518 -> f518 : A'=C+A, C'=-1+C, [ C>=1 ], cost: 1 184: f518 -> f524 : C'=7, [ 0>=C ], cost: 1 58: f524 -> f524 : A'=C+A, C'=-1+C, [ C>=0 ], cost: 1 183: f524 -> f530 : C'=7, [ 0>=1+C ], cost: 1 59: f530 -> f530 : A'=C+A, C'=-1+C, [ C>=1 ], cost: 1 182: f530 -> f536 : C'=7, [ 0>=C ], cost: 1 60: f536 -> f536 : A'=C+A, C'=-1+C, [ C>=0 ], cost: 1 181: f536 -> f544 : C'=8, [ 0>=1+C ], cost: 1 61: f544 -> f544 : A'=C+A, C'=-1+C, [ C>=0 ], cost: 1 180: f544 -> f550 : C'=8, [ 0>=1+C ], cost: 1 62: f550 -> f550 : A'=C+A, C'=-1+C, [ 1+C>=0 ], cost: 1 179: f550 -> f556 : C'=8, [ 0>=2+C ], cost: 1 63: f556 -> f556 : A'=C+A, C'=-1+C, [ C>=0 ], cost: 1 178: f556 -> f562 : C'=8, [ 0>=1+C ], cost: 1 64: f562 -> f562 : A'=C+A, C'=-1+C, [ 1+C>=0 ], cost: 1 177: f562 -> f570 : C'=9, [ 0>=2+C ], cost: 1 65: f570 -> f570 : A'=C+A, C'=-1+C, [ 1+C>=0 ], cost: 1 176: f570 -> f576 : C'=9, [ 0>=2+C ], cost: 1 66: f576 -> f576 : A'=C+A, C'=-1+C, [ 2+C>=0 ], cost: 1 175: f576 -> f582 : C'=9, [ 0>=3+C ], cost: 1 67: f582 -> f582 : A'=C+A, C'=-1+C, [ 1+C>=0 ], cost: 1 174: f582 -> f588 : C'=9, [ 0>=2+C ], cost: 1 68: f588 -> f588 : A'=C+A, C'=-1+C, [ 2+C>=0 ], cost: 1 173: f588 -> f596 : C'=0, [ 0>=3+C ], cost: 1 69: f596 -> f596 : A'=C+A, C'=-1+C, [ 2+C>=0 ], cost: 1 172: f596 -> f602 : C'=0, [ 0>=3+C ], cost: 1 70: f602 -> f602 : A'=C+A, C'=-1+C, [ 3+C>=0 ], cost: 1 171: f602 -> f608 : C'=0, [ 0>=4+C ], cost: 1 71: f608 -> f608 : A'=C+A, C'=-1+C, [ 2+C>=0 ], cost: 1 170: f608 -> f614 : C'=0, [ 0>=3+C ], cost: 1 72: f614 -> f614 : A'=C+A, C'=-1+C, [ 3+C>=0 ], cost: 1 169: f614 -> f622 : C'=-1, [ 0>=4+C ], cost: 1 73: f622 -> f622 : A'=C+A, C'=-1+C, [ 4+C>=0 ], cost: 1 168: f622 -> f628 : C'=-1, [ 0>=5+C ], cost: 1 74: f628 -> f628 : A'=C+A, C'=-1+C, [ 5+C>=0 ], cost: 1 167: f628 -> f634 : C'=-1, [ 0>=6+C ], cost: 1 75: f634 -> f634 : A'=C+A, C'=-1+C, [ 4+C>=0 ], cost: 1 166: f634 -> f640 : C'=-1, [ 0>=5+C ], cost: 1 76: f640 -> f640 : A'=C+A, C'=-1+C, [ 5+C>=0 ], cost: 1 165: f640 -> f648 : C'=-2, [ 0>=6+C ], cost: 1 77: f648 -> f648 : A'=C+A, C'=-1+C, [ 6+C>=0 ], cost: 1 164: f648 -> f654 : C'=-2, [ 0>=7+C ], cost: 1 78: f654 -> f654 : A'=C+A, C'=-1+C, [ 7+C>=0 ], cost: 1 163: f654 -> f660 : C'=-2, [ 0>=8+C ], cost: 1 79: f660 -> f660 : A'=C+A, C'=-1+C, [ 6+C>=0 ], cost: 1 162: f660 -> f666 : C'=-2, [ 0>=7+C ], cost: 1 80: f666 -> f666 : A'=C+A, C'=-1+C, [ 7+C>=0 ], cost: 1 161: f666 -> f674 : C'=16, [ 0>=8+C ], cost: 1 81: f674 -> f674 : A'=C+A, C'=-1+C, [ 7+C>=0 ], cost: 1 160: f674 -> f680 : C'=16, [ 0>=8+C ], cost: 1 82: f680 -> f680 : A'=C+A, C'=-1+C, [ 8+C>=0 ], cost: 1 159: f680 -> f686 : C'=16, [ 0>=9+C ], cost: 1 83: f686 -> f686 : A'=C+A, C'=-1+C, [ 7+C>=0 ], cost: 1 158: f686 -> f692 : C'=16, [ 0>=8+C ], cost: 1 84: f692 -> f692 : A'=C+A, C'=-1+C, [ 8+C>=0 ], cost: 1 157: f692 -> f700 : C'=5, [ 0>=9+C ], cost: 1 85: f700 -> f700 : A'=C+A, C'=-B+C, [ C>=3 ], cost: 1 156: f700 -> f706 : C'=5, [ 2>=C ], cost: 1 86: f706 -> f706 : A'=C+A, C'=-B+C, [ C>=2 ], cost: 1 155: f706 -> f712 : C'=5, [ 1>=C ], cost: 1 87: f712 -> f712 : A'=C+A, C'=-B+C, [ C>=3 ], cost: 1 154: f712 -> f718 : C'=5, [ 2>=C ], cost: 1 88: f718 -> f718 : A'=C+A, C'=-B+C, [ C>=2 ], cost: 1 153: f718 -> f726 : C'=6, [ 1>=C ], cost: 1 89: f726 -> f726 : A'=C+A, C'=-B+C, [ C>=2 ], cost: 1 152: f726 -> f732 : C'=6, [ 1>=C ], cost: 1 90: f732 -> f732 : A'=C+A, C'=-B+C, [ C>=1 ], cost: 1 151: f732 -> f738 : C'=6, [ 0>=C ], cost: 1 91: f738 -> f738 : A'=C+A, C'=-B+C, [ C>=2 ], cost: 1 150: f738 -> f744 : C'=6, [ 1>=C ], cost: 1 92: f744 -> f744 : A'=C+A, C'=-B+C, [ C>=1 ], cost: 1 149: f744 -> f752 : C'=7, [ 0>=C ], cost: 1 93: f752 -> f752 : A'=C+A, C'=-B+C, [ C>=1 ], cost: 1 148: f752 -> f758 : C'=7, [ 0>=C ], cost: 1 94: f758 -> f758 : A'=C+A, C'=-B+C, [ C>=0 ], cost: 1 147: f758 -> f764 : C'=7, [ 0>=1+C ], cost: 1 95: f764 -> f764 : A'=C+A, C'=-B+C, [ C>=1 ], cost: 1 146: f764 -> f770 : C'=7, [ 0>=C ], cost: 1 96: f770 -> f770 : A'=C+A, C'=-B+C, [ C>=0 ], cost: 1 145: f770 -> f778 : C'=8, [ 0>=1+C ], cost: 1 97: f778 -> f778 : A'=C+A, C'=-B+C, [ C>=0 ], cost: 1 144: f778 -> f784 : C'=8, [ 0>=1+C ], cost: 1 98: f784 -> f784 : A'=C+A, C'=-B+C, [ 1+C>=0 ], cost: 1 143: f784 -> f790 : C'=8, [ 0>=2+C ], cost: 1 99: f790 -> f790 : A'=C+A, C'=-B+C, [ C>=0 ], cost: 1 142: f790 -> f796 : C'=8, [ 0>=1+C ], cost: 1 100: f796 -> f796 : A'=C+A, C'=-B+C, [ 1+C>=0 ], cost: 1 141: f796 -> f804 : C'=9, [ 0>=2+C ], cost: 1 101: f804 -> f804 : A'=C+A, C'=-B+C, [ 1+C>=0 ], cost: 1 140: f804 -> f810 : C'=9, [ 0>=2+C ], cost: 1 102: f810 -> f810 : A'=C+A, C'=-B+C, [ 2+C>=0 ], cost: 1 139: f810 -> f816 : C'=9, [ 0>=3+C ], cost: 1 103: f816 -> f816 : A'=C+A, C'=-B+C, [ 1+C>=0 ], cost: 1 138: f816 -> f822 : C'=9, [ 0>=2+C ], cost: 1 104: f822 -> f822 : A'=C+A, C'=-B+C, [ 2+C>=0 ], cost: 1 137: f822 -> f830 : C'=0, [ 0>=3+C ], cost: 1 105: f830 -> f830 : A'=C+A, C'=-B+C, [ 2+C>=0 ], cost: 1 136: f830 -> f836 : C'=0, [ 0>=3+C ], cost: 1 106: f836 -> f836 : A'=C+A, C'=-B+C, [ 3+C>=0 ], cost: 1 135: f836 -> f842 : C'=0, [ 0>=4+C ], cost: 1 107: f842 -> f842 : A'=C+A, C'=-B+C, [ 2+C>=0 ], cost: 1 134: f842 -> f848 : C'=0, [ 0>=3+C ], cost: 1 108: f848 -> f848 : A'=C+A, C'=-B+C, [ 3+C>=0 ], cost: 1 133: f848 -> f856 : C'=-1, [ 0>=4+C ], cost: 1 109: f856 -> f856 : A'=C+A, C'=-B+C, [ 4+C>=0 ], cost: 1 132: f856 -> f862 : C'=-1, [ 0>=5+C ], cost: 1 110: f862 -> f862 : A'=C+A, C'=-B+C, [ 5+C>=0 ], cost: 1 131: f862 -> f868 : C'=-1, [ 0>=6+C ], cost: 1 111: f868 -> f868 : A'=C+A, C'=-B+C, [ 4+C>=0 ], cost: 1 130: f868 -> f874 : C'=-1, [ 0>=5+C ], cost: 1 112: f874 -> f874 : A'=C+A, C'=-B+C, [ 5+C>=0 ], cost: 1 129: f874 -> f882 : C'=-2, [ 0>=6+C ], cost: 1 113: f882 -> f882 : A'=C+A, C'=-B+C, [ 6+C>=0 ], cost: 1 128: f882 -> f888 : C'=-2, [ 0>=7+C ], cost: 1 114: f888 -> f888 : A'=C+A, C'=-B+C, [ 7+C>=0 ], cost: 1 127: f888 -> f894 : C'=-2, [ 0>=8+C ], cost: 1 115: f894 -> f894 : A'=C+A, C'=-B+C, [ 6+C>=0 ], cost: 1 126: f894 -> f900 : C'=-2, [ 0>=7+C ], cost: 1 116: f900 -> f900 : A'=C+A, C'=-B+C, [ 7+C>=0 ], cost: 1 125: f900 -> f908 : C'=16, [ 0>=8+C ], cost: 1 117: f908 -> f908 : A'=C+A, C'=-B+C, [ 7+C>=0 ], cost: 1 124: f908 -> f914 : C'=16, [ 0>=8+C ], cost: 1 118: f914 -> f914 : A'=C+A, C'=-B+C, [ 8+C>=0 ], cost: 1 123: f914 -> f920 : C'=16, [ 0>=9+C ], cost: 1 119: f920 -> f920 : A'=C+A, C'=-B+C, [ 7+C>=0 ], cost: 1 122: f920 -> f926 : C'=16, [ 0>=8+C ], cost: 1 120: f926 -> f926 : A'=C+A, C'=-B+C, [ 8+C>=0 ], cost: 1 121: f926 -> f934 : [ 0>=9+C ], cost: 1 Simplified the transitions: Start location: f0 0: f0 -> f154 : A'=0, B'=2, C'=0, [], cost: 1 1: f154 -> f154 : A'=C+A, C'=1+C, [ 2>=C ], cost: 1 240: f154 -> f160 : C'=0, [ C>=3 ], cost: 1 2: f160 -> f160 : A'=C+A, C'=1+C, [ 3>=C ], cost: 1 239: f160 -> f166 : C'=0, [ C>=4 ], cost: 1 3: f166 -> f166 : A'=C+A, C'=1+C, [ 2>=C ], cost: 1 238: f166 -> f172 : C'=0, [ C>=3 ], cost: 1 4: f172 -> f172 : A'=C+A, C'=1+C, [ 3>=C ], cost: 1 237: f172 -> f180 : C'=1, [ C>=4 ], cost: 1 5: f180 -> f180 : A'=C+A, C'=1+C, [ 1>=C ], cost: 1 236: f180 -> f186 : C'=1, [ C>=2 ], cost: 1 6: f186 -> f186 : A'=C+A, C'=1+C, [ 2>=C ], cost: 1 235: f186 -> f192 : C'=1, [ C>=3 ], cost: 1 7: f192 -> f192 : A'=C+A, C'=1+C, [ 1>=C ], cost: 1 234: f192 -> f198 : C'=1, [ C>=2 ], cost: 1 8: f198 -> f198 : A'=C+A, C'=1+C, [ 2>=C ], cost: 1 233: f198 -> f206 : C'=-3, [ C>=3 ], cost: 1 9: f206 -> f206 : A'=C+A, C'=1+C, [ 0>=3+C ], cost: 1 232: f206 -> f212 : C'=-3, [ 2+C>=0 ], cost: 1 10: f212 -> f212 : A'=C+A, C'=1+C, [ 0>=2+C ], cost: 1 231: f212 -> f218 : C'=-3, [ 1+C>=0 ], cost: 1 11: f218 -> f218 : A'=C+A, C'=1+C, [ 0>=3+C ], cost: 1 230: f218 -> f224 : C'=-3, [ 2+C>=0 ], cost: 1 12: f224 -> f224 : A'=C+A, C'=1+C, [ 0>=2+C ], cost: 1 229: f224 -> f232 : C'=-4, [ 1+C>=0 ], cost: 1 13: f232 -> f232 : A'=C+A, C'=1+C, [ 0>=2+C ], cost: 1 228: f232 -> f238 : C'=-4, [ 1+C>=0 ], cost: 1 14: f238 -> f238 : A'=C+A, C'=1+C, [ 0>=1+C ], cost: 1 227: f238 -> f244 : C'=-4, [ C>=0 ], cost: 1 15: f244 -> f244 : A'=C+A, C'=1+C, [ 0>=2+C ], cost: 1 226: f244 -> f250 : C'=-4, [ 1+C>=0 ], cost: 1 16: f250 -> f250 : A'=C+A, C'=1+C, [ 0>=1+C ], cost: 1 225: f250 -> f258 : C'=-5, [ C>=0 ], cost: 1 17: f258 -> f258 : A'=C+A, C'=1+C, [ 0>=1+C ], cost: 1 224: f258 -> f264 : C'=-5, [ C>=0 ], cost: 1 18: f264 -> f264 : A'=C+A, C'=1+C, [ 0>=C ], cost: 1 223: f264 -> f270 : C'=-5, [ C>=1 ], cost: 1 19: f270 -> f270 : A'=C+A, C'=1+C, [ 0>=1+C ], cost: 1 222: f270 -> f276 : C'=-5, [ C>=0 ], cost: 1 20: f276 -> f276 : A'=C+A, C'=1+C, [ 0>=C ], cost: 1 221: f276 -> f284 : C'=-6, [ C>=1 ], cost: 1 21: f284 -> f284 : A'=C+A, C'=1+C, [ 3>=C ], cost: 1 220: f284 -> f290 : C'=-6, [ C>=4 ], cost: 1 22: f290 -> f290 : A'=C+A, C'=1+C, [ 4>=C ], cost: 1 219: f290 -> f296 : C'=-6, [ C>=5 ], cost: 1 23: f296 -> f296 : A'=C+A, C'=1+C, [ 3>=C ], cost: 1 218: f296 -> f302 : C'=-6, [ C>=4 ], cost: 1 24: f302 -> f302 : A'=C+A, C'=1+C, [ 4>=C ], cost: 1 217: f302 -> f310 : C'=0, [ C>=5 ], cost: 1 25: f310 -> f310 : A'=C+A, C'=B+C, [ 2>=C ], cost: 1 216: f310 -> f316 : C'=0, [ C>=3 ], cost: 1 26: f316 -> f316 : A'=C+A, C'=B+C, [ 3>=C ], cost: 1 215: f316 -> f322 : C'=0, [ C>=4 ], cost: 1 27: f322 -> f322 : A'=C+A, C'=B+C, [ 2>=C ], cost: 1 214: f322 -> f328 : C'=0, [ C>=3 ], cost: 1 28: f328 -> f328 : A'=C+A, C'=B+C, [ 3>=C ], cost: 1 213: f328 -> f336 : C'=1, [ C>=4 ], cost: 1 29: f336 -> f336 : A'=C+A, C'=B+C, [ 1>=C ], cost: 1 212: f336 -> f342 : C'=1, [ C>=2 ], cost: 1 30: f342 -> f342 : A'=C+A, C'=B+C, [ 2>=C ], cost: 1 211: f342 -> f348 : C'=1, [ C>=3 ], cost: 1 31: f348 -> f348 : A'=C+A, C'=B+C, [ 1>=C ], cost: 1 210: f348 -> f354 : C'=1, [ C>=2 ], cost: 1 32: f354 -> f354 : A'=C+A, C'=B+C, [ 2>=C ], cost: 1 209: f354 -> f362 : C'=-3, [ C>=3 ], cost: 1 33: f362 -> f362 : A'=C+A, C'=B+C, [ 0>=3+C ], cost: 1 208: f362 -> f368 : C'=-3, [ 2+C>=0 ], cost: 1 34: f368 -> f368 : A'=C+A, C'=B+C, [ 0>=2+C ], cost: 1 207: f368 -> f374 : C'=-3, [ 1+C>=0 ], cost: 1 35: f374 -> f374 : A'=C+A, C'=B+C, [ 0>=3+C ], cost: 1 206: f374 -> f380 : C'=-3, [ 2+C>=0 ], cost: 1 36: f380 -> f380 : A'=C+A, C'=B+C, [ 0>=2+C ], cost: 1 205: f380 -> f388 : C'=-4, [ 1+C>=0 ], cost: 1 37: f388 -> f388 : A'=C+A, C'=B+C, [ 0>=2+C ], cost: 1 204: f388 -> f394 : C'=-4, [ 1+C>=0 ], cost: 1 38: f394 -> f394 : A'=C+A, C'=B+C, [ 0>=1+C ], cost: 1 203: f394 -> f400 : C'=-4, [ C>=0 ], cost: 1 39: f400 -> f400 : A'=C+A, C'=B+C, [ 0>=2+C ], cost: 1 202: f400 -> f406 : C'=-4, [ 1+C>=0 ], cost: 1 40: f406 -> f406 : A'=C+A, C'=B+C, [ 0>=1+C ], cost: 1 201: f406 -> f414 : C'=-5, [ C>=0 ], cost: 1 41: f414 -> f414 : A'=C+A, C'=B+C, [ 0>=1+C ], cost: 1 200: f414 -> f420 : C'=-5, [ C>=0 ], cost: 1 42: f420 -> f420 : A'=C+A, C'=B+C, [ 0>=C ], cost: 1 199: f420 -> f426 : C'=-5, [ C>=1 ], cost: 1 43: f426 -> f426 : A'=C+A, C'=B+C, [ 0>=1+C ], cost: 1 198: f426 -> f432 : C'=-5, [ C>=0 ], cost: 1 44: f432 -> f432 : A'=C+A, C'=B+C, [ 0>=C ], cost: 1 197: f432 -> f440 : C'=-6, [ C>=1 ], cost: 1 45: f440 -> f440 : A'=C+A, C'=B+C, [ 3>=C ], cost: 1 196: f440 -> f446 : C'=-6, [ C>=4 ], cost: 1 46: f446 -> f446 : A'=C+A, C'=B+C, [ 4>=C ], cost: 1 195: f446 -> f452 : C'=-6, [ C>=5 ], cost: 1 47: f452 -> f452 : A'=C+A, C'=B+C, [ 3>=C ], cost: 1 194: f452 -> f458 : C'=-6, [ C>=4 ], cost: 1 48: f458 -> f458 : A'=C+A, C'=B+C, [ 4>=C ], cost: 1 193: f458 -> f466 : C'=5, [ C>=5 ], cost: 1 49: f466 -> f466 : A'=C+A, C'=-1+C, [ C>=3 ], cost: 1 192: f466 -> f472 : C'=5, [ 2>=C ], cost: 1 50: f472 -> f472 : A'=C+A, C'=-1+C, [ C>=2 ], cost: 1 191: f472 -> f478 : C'=5, [ 1>=C ], cost: 1 51: f478 -> f478 : A'=C+A, C'=-1+C, [ C>=3 ], cost: 1 190: f478 -> f484 : C'=5, [ 2>=C ], cost: 1 52: f484 -> f484 : A'=C+A, C'=-1+C, [ C>=2 ], cost: 1 189: f484 -> f492 : C'=6, [ 1>=C ], cost: 1 53: f492 -> f492 : A'=C+A, C'=-1+C, [ C>=2 ], cost: 1 188: f492 -> f498 : C'=6, [ 1>=C ], cost: 1 54: f498 -> f498 : A'=C+A, C'=-1+C, [ C>=1 ], cost: 1 187: f498 -> f504 : C'=6, [ 0>=C ], cost: 1 55: f504 -> f504 : A'=C+A, C'=-1+C, [ C>=2 ], cost: 1 186: f504 -> f510 : C'=6, [ 1>=C ], cost: 1 56: f510 -> f510 : A'=C+A, C'=-1+C, [ C>=1 ], cost: 1 185: f510 -> f518 : C'=7, [ 0>=C ], cost: 1 57: f518 -> f518 : A'=C+A, C'=-1+C, [ C>=1 ], cost: 1 184: f518 -> f524 : C'=7, [ 0>=C ], cost: 1 58: f524 -> f524 : A'=C+A, C'=-1+C, [ C>=0 ], cost: 1 183: f524 -> f530 : C'=7, [ 0>=1+C ], cost: 1 59: f530 -> f530 : A'=C+A, C'=-1+C, [ C>=1 ], cost: 1 182: f530 -> f536 : C'=7, [ 0>=C ], cost: 1 60: f536 -> f536 : A'=C+A, C'=-1+C, [ C>=0 ], cost: 1 181: f536 -> f544 : C'=8, [ 0>=1+C ], cost: 1 61: f544 -> f544 : A'=C+A, C'=-1+C, [ C>=0 ], cost: 1 180: f544 -> f550 : C'=8, [ 0>=1+C ], cost: 1 62: f550 -> f550 : A'=C+A, C'=-1+C, [ 1+C>=0 ], cost: 1 179: f550 -> f556 : C'=8, [ 0>=2+C ], cost: 1 63: f556 -> f556 : A'=C+A, C'=-1+C, [ C>=0 ], cost: 1 178: f556 -> f562 : C'=8, [ 0>=1+C ], cost: 1 64: f562 -> f562 : A'=C+A, C'=-1+C, [ 1+C>=0 ], cost: 1 177: f562 -> f570 : C'=9, [ 0>=2+C ], cost: 1 65: f570 -> f570 : A'=C+A, C'=-1+C, [ 1+C>=0 ], cost: 1 176: f570 -> f576 : C'=9, [ 0>=2+C ], cost: 1 66: f576 -> f576 : A'=C+A, C'=-1+C, [ 2+C>=0 ], cost: 1 175: f576 -> f582 : C'=9, [ 0>=3+C ], cost: 1 67: f582 -> f582 : A'=C+A, C'=-1+C, [ 1+C>=0 ], cost: 1 174: f582 -> f588 : C'=9, [ 0>=2+C ], cost: 1 68: f588 -> f588 : A'=C+A, C'=-1+C, [ 2+C>=0 ], cost: 1 173: f588 -> f596 : C'=0, [ 0>=3+C ], cost: 1 69: f596 -> f596 : A'=C+A, C'=-1+C, [ 2+C>=0 ], cost: 1 172: f596 -> f602 : C'=0, [ 0>=3+C ], cost: 1 70: f602 -> f602 : A'=C+A, C'=-1+C, [ 3+C>=0 ], cost: 1 171: f602 -> f608 : C'=0, [ 0>=4+C ], cost: 1 71: f608 -> f608 : A'=C+A, C'=-1+C, [ 2+C>=0 ], cost: 1 170: f608 -> f614 : C'=0, [ 0>=3+C ], cost: 1 72: f614 -> f614 : A'=C+A, C'=-1+C, [ 3+C>=0 ], cost: 1 169: f614 -> f622 : C'=-1, [ 0>=4+C ], cost: 1 73: f622 -> f622 : A'=C+A, C'=-1+C, [ 4+C>=0 ], cost: 1 168: f622 -> f628 : C'=-1, [ 0>=5+C ], cost: 1 74: f628 -> f628 : A'=C+A, C'=-1+C, [ 5+C>=0 ], cost: 1 167: f628 -> f634 : C'=-1, [ 0>=6+C ], cost: 1 75: f634 -> f634 : A'=C+A, C'=-1+C, [ 4+C>=0 ], cost: 1 166: f634 -> f640 : C'=-1, [ 0>=5+C ], cost: 1 76: f640 -> f640 : A'=C+A, C'=-1+C, [ 5+C>=0 ], cost: 1 165: f640 -> f648 : C'=-2, [ 0>=6+C ], cost: 1 77: f648 -> f648 : A'=C+A, C'=-1+C, [ 6+C>=0 ], cost: 1 164: f648 -> f654 : C'=-2, [ 0>=7+C ], cost: 1 78: f654 -> f654 : A'=C+A, C'=-1+C, [ 7+C>=0 ], cost: 1 163: f654 -> f660 : C'=-2, [ 0>=8+C ], cost: 1 79: f660 -> f660 : A'=C+A, C'=-1+C, [ 6+C>=0 ], cost: 1 162: f660 -> f666 : C'=-2, [ 0>=7+C ], cost: 1 80: f666 -> f666 : A'=C+A, C'=-1+C, [ 7+C>=0 ], cost: 1 161: f666 -> f674 : C'=16, [ 0>=8+C ], cost: 1 81: f674 -> f674 : A'=C+A, C'=-1+C, [ 7+C>=0 ], cost: 1 160: f674 -> f680 : C'=16, [ 0>=8+C ], cost: 1 82: f680 -> f680 : A'=C+A, C'=-1+C, [ 8+C>=0 ], cost: 1 159: f680 -> f686 : C'=16, [ 0>=9+C ], cost: 1 83: f686 -> f686 : A'=C+A, C'=-1+C, [ 7+C>=0 ], cost: 1 158: f686 -> f692 : C'=16, [ 0>=8+C ], cost: 1 84: f692 -> f692 : A'=C+A, C'=-1+C, [ 8+C>=0 ], cost: 1 157: f692 -> f700 : C'=5, [ 0>=9+C ], cost: 1 85: f700 -> f700 : A'=C+A, C'=-B+C, [ C>=3 ], cost: 1 156: f700 -> f706 : C'=5, [ 2>=C ], cost: 1 86: f706 -> f706 : A'=C+A, C'=-B+C, [ C>=2 ], cost: 1 155: f706 -> f712 : C'=5, [ 1>=C ], cost: 1 87: f712 -> f712 : A'=C+A, C'=-B+C, [ C>=3 ], cost: 1 154: f712 -> f718 : C'=5, [ 2>=C ], cost: 1 88: f718 -> f718 : A'=C+A, C'=-B+C, [ C>=2 ], cost: 1 153: f718 -> f726 : C'=6, [ 1>=C ], cost: 1 89: f726 -> f726 : A'=C+A, C'=-B+C, [ C>=2 ], cost: 1 152: f726 -> f732 : C'=6, [ 1>=C ], cost: 1 90: f732 -> f732 : A'=C+A, C'=-B+C, [ C>=1 ], cost: 1 151: f732 -> f738 : C'=6, [ 0>=C ], cost: 1 91: f738 -> f738 : A'=C+A, C'=-B+C, [ C>=2 ], cost: 1 150: f738 -> f744 : C'=6, [ 1>=C ], cost: 1 92: f744 -> f744 : A'=C+A, C'=-B+C, [ C>=1 ], cost: 1 149: f744 -> f752 : C'=7, [ 0>=C ], cost: 1 93: f752 -> f752 : A'=C+A, C'=-B+C, [ C>=1 ], cost: 1 148: f752 -> f758 : C'=7, [ 0>=C ], cost: 1 94: f758 -> f758 : A'=C+A, C'=-B+C, [ C>=0 ], cost: 1 147: f758 -> f764 : C'=7, [ 0>=1+C ], cost: 1 95: f764 -> f764 : A'=C+A, C'=-B+C, [ C>=1 ], cost: 1 146: f764 -> f770 : C'=7, [ 0>=C ], cost: 1 96: f770 -> f770 : A'=C+A, C'=-B+C, [ C>=0 ], cost: 1 145: f770 -> f778 : C'=8, [ 0>=1+C ], cost: 1 97: f778 -> f778 : A'=C+A, C'=-B+C, [ C>=0 ], cost: 1 144: f778 -> f784 : C'=8, [ 0>=1+C ], cost: 1 98: f784 -> f784 : A'=C+A, C'=-B+C, [ 1+C>=0 ], cost: 1 143: f784 -> f790 : C'=8, [ 0>=2+C ], cost: 1 99: f790 -> f790 : A'=C+A, C'=-B+C, [ C>=0 ], cost: 1 142: f790 -> f796 : C'=8, [ 0>=1+C ], cost: 1 100: f796 -> f796 : A'=C+A, C'=-B+C, [ 1+C>=0 ], cost: 1 141: f796 -> f804 : C'=9, [ 0>=2+C ], cost: 1 101: f804 -> f804 : A'=C+A, C'=-B+C, [ 1+C>=0 ], cost: 1 140: f804 -> f810 : C'=9, [ 0>=2+C ], cost: 1 102: f810 -> f810 : A'=C+A, C'=-B+C, [ 2+C>=0 ], cost: 1 139: f810 -> f816 : C'=9, [ 0>=3+C ], cost: 1 103: f816 -> f816 : A'=C+A, C'=-B+C, [ 1+C>=0 ], cost: 1 138: f816 -> f822 : C'=9, [ 0>=2+C ], cost: 1 104: f822 -> f822 : A'=C+A, C'=-B+C, [ 2+C>=0 ], cost: 1 137: f822 -> f830 : C'=0, [ 0>=3+C ], cost: 1 105: f830 -> f830 : A'=C+A, C'=-B+C, [ 2+C>=0 ], cost: 1 136: f830 -> f836 : C'=0, [ 0>=3+C ], cost: 1 106: f836 -> f836 : A'=C+A, C'=-B+C, [ 3+C>=0 ], cost: 1 135: f836 -> f842 : C'=0, [ 0>=4+C ], cost: 1 107: f842 -> f842 : A'=C+A, C'=-B+C, [ 2+C>=0 ], cost: 1 134: f842 -> f848 : C'=0, [ 0>=3+C ], cost: 1 108: f848 -> f848 : A'=C+A, C'=-B+C, [ 3+C>=0 ], cost: 1 133: f848 -> f856 : C'=-1, [ 0>=4+C ], cost: 1 109: f856 -> f856 : A'=C+A, C'=-B+C, [ 4+C>=0 ], cost: 1 132: f856 -> f862 : C'=-1, [ 0>=5+C ], cost: 1 110: f862 -> f862 : A'=C+A, C'=-B+C, [ 5+C>=0 ], cost: 1 131: f862 -> f868 : C'=-1, [ 0>=6+C ], cost: 1 111: f868 -> f868 : A'=C+A, C'=-B+C, [ 4+C>=0 ], cost: 1 130: f868 -> f874 : C'=-1, [ 0>=5+C ], cost: 1 112: f874 -> f874 : A'=C+A, C'=-B+C, [ 5+C>=0 ], cost: 1 129: f874 -> f882 : C'=-2, [ 0>=6+C ], cost: 1 113: f882 -> f882 : A'=C+A, C'=-B+C, [ 6+C>=0 ], cost: 1 128: f882 -> f888 : C'=-2, [ 0>=7+C ], cost: 1 114: f888 -> f888 : A'=C+A, C'=-B+C, [ 7+C>=0 ], cost: 1 127: f888 -> f894 : C'=-2, [ 0>=8+C ], cost: 1 115: f894 -> f894 : A'=C+A, C'=-B+C, [ 6+C>=0 ], cost: 1 126: f894 -> f900 : C'=-2, [ 0>=7+C ], cost: 1 116: f900 -> f900 : A'=C+A, C'=-B+C, [ 7+C>=0 ], cost: 1 125: f900 -> f908 : C'=16, [ 0>=8+C ], cost: 1 117: f908 -> f908 : A'=C+A, C'=-B+C, [ 7+C>=0 ], cost: 1 124: f908 -> f914 : C'=16, [ 0>=8+C ], cost: 1 118: f914 -> f914 : A'=C+A, C'=-B+C, [ 8+C>=0 ], cost: 1 123: f914 -> f920 : C'=16, [ 0>=9+C ], cost: 1 119: f920 -> f920 : A'=C+A, C'=-B+C, [ 7+C>=0 ], cost: 1 122: f920 -> f926 : C'=16, [ 0>=8+C ], cost: 1 120: f926 -> f926 : A'=C+A, C'=-B+C, [ 8+C>=0 ], cost: 1 Eliminating 1 self-loops for location f154 Self-Loop 1 has the metering function: 3-C, resulting in the new transition 241. Removing the self-loops: 1. Eliminating 1 self-loops for location f160 Self-Loop 2 has the metering function: 4-C, resulting in the new transition 242. Removing the self-loops: 2. Eliminating 1 self-loops for location f166 Self-Loop 3 has the metering function: 3-C, resulting in the new transition 243. Removing the self-loops: 3. Eliminating 1 self-loops for location f172 Self-Loop 4 has the metering function: 4-C, resulting in the new transition 244. Removing the self-loops: 4. Eliminating 1 self-loops for location f180 Self-Loop 5 has the metering function: 2-C, resulting in the new transition 245. Removing the self-loops: 5. Eliminating 1 self-loops for location f186 Self-Loop 6 has the metering function: 3-C, resulting in the new transition 246. Removing the self-loops: 6. Eliminating 1 self-loops for location f192 Self-Loop 7 has the metering function: 2-C, resulting in the new transition 247. Removing the self-loops: 7. Eliminating 1 self-loops for location f198 Self-Loop 8 has the metering function: 3-C, resulting in the new transition 248. Removing the self-loops: 8. Eliminating 1 self-loops for location f206 Self-Loop 9 has the metering function: -2-C, resulting in the new transition 249. Removing the self-loops: 9. Eliminating 1 self-loops for location f212 Self-Loop 10 has the metering function: -1-C, resulting in the new transition 250. Removing the self-loops: 10. Eliminating 1 self-loops for location f218 Self-Loop 11 has the metering function: -2-C, resulting in the new transition 251. Removing the self-loops: 11. Eliminating 1 self-loops for location f224 Self-Loop 12 has the metering function: -1-C, resulting in the new transition 252. Removing the self-loops: 12. Eliminating 1 self-loops for location f232 Self-Loop 13 has the metering function: -1-C, resulting in the new transition 253. Removing the self-loops: 13. Eliminating 1 self-loops for location f238 Self-Loop 14 has the metering function: -C, resulting in the new transition 254. Removing the self-loops: 14. Eliminating 1 self-loops for location f244 Self-Loop 15 has the metering function: -1-C, resulting in the new transition 255. Removing the self-loops: 15. Eliminating 1 self-loops for location f250 Self-Loop 16 has the metering function: -C, resulting in the new transition 256. Removing the self-loops: 16. Eliminating 1 self-loops for location f258 Self-Loop 17 has the metering function: -C, resulting in the new transition 257. Removing the self-loops: 17. Eliminating 1 self-loops for location f264 Self-Loop 18 has the metering function: 1-C, resulting in the new transition 258. Removing the self-loops: 18. Eliminating 1 self-loops for location f270 Self-Loop 19 has the metering function: -C, resulting in the new transition 259. Removing the self-loops: 19. Eliminating 1 self-loops for location f276 Self-Loop 20 has the metering function: 1-C, resulting in the new transition 260. Removing the self-loops: 20. Eliminating 1 self-loops for location f284 Self-Loop 21 has the metering function: 4-C, resulting in the new transition 261. Removing the self-loops: 21. Eliminating 1 self-loops for location f290 Self-Loop 22 has the metering function: 5-C, resulting in the new transition 262. Removing the self-loops: 22. Eliminating 1 self-loops for location f296 Self-Loop 23 has the metering function: 4-C, resulting in the new transition 263. Removing the self-loops: 23. Eliminating 1 self-loops for location f302 Self-Loop 24 has the metering function: 5-C, resulting in the new transition 264. Removing the self-loops: 24. Eliminating 1 self-loops for location f310 Removing the self-loops: 25. Adding an epsilon transition (to model nonexecution of the loops): 266. Eliminating 1 self-loops for location f316 Removing the self-loops: 26. Adding an epsilon transition (to model nonexecution of the loops): 268. Eliminating 1 self-loops for location f322 Removing the self-loops: 27. Adding an epsilon transition (to model nonexecution of the loops): 270. Eliminating 1 self-loops for location f328 Removing the self-loops: 28. Adding an epsilon transition (to model nonexecution of the loops): 272. Eliminating 1 self-loops for location f336 Removing the self-loops: 29. Adding an epsilon transition (to model nonexecution of the loops): 274. Eliminating 1 self-loops for location f342 Removing the self-loops: 30. Adding an epsilon transition (to model nonexecution of the loops): 276. Eliminating 1 self-loops for location f348 Removing the self-loops: 31. Adding an epsilon transition (to model nonexecution of the loops): 278. Eliminating 1 self-loops for location f354 Removing the self-loops: 32. Adding an epsilon transition (to model nonexecution of the loops): 280. Eliminating 1 self-loops for location f362 Removing the self-loops: 33. Adding an epsilon transition (to model nonexecution of the loops): 282. Eliminating 1 self-loops for location f368 Removing the self-loops: 34. Adding an epsilon transition (to model nonexecution of the loops): 284. Eliminating 1 self-loops for location f374 Removing the self-loops: 35. Adding an epsilon transition (to model nonexecution of the loops): 286. Eliminating 1 self-loops for location f380 Removing the self-loops: 36. Adding an epsilon transition (to model nonexecution of the loops): 288. Eliminating 1 self-loops for location f388 Removing the self-loops: 37. Adding an epsilon transition (to model nonexecution of the loops): 290. Eliminating 1 self-loops for location f394 Removing the self-loops: 38. Adding an epsilon transition (to model nonexecution of the loops): 292. Eliminating 1 self-loops for location f400 Removing the self-loops: 39. Adding an epsilon transition (to model nonexecution of the loops): 294. Eliminating 1 self-loops for location f406 Removing the self-loops: 40. Adding an epsilon transition (to model nonexecution of the loops): 296. Eliminating 1 self-loops for location f414 Removing the self-loops: 41. Adding an epsilon transition (to model nonexecution of the loops): 298. Eliminating 1 self-loops for location f420 Removing the self-loops: 42. Adding an epsilon transition (to model nonexecution of the loops): 300. Eliminating 1 self-loops for location f426 Removing the self-loops: 43. Adding an epsilon transition (to model nonexecution of the loops): 302. Eliminating 1 self-loops for location f432 Removing the self-loops: 44. Adding an epsilon transition (to model nonexecution of the loops): 304. Eliminating 1 self-loops for location f440 Removing the self-loops: 45. Adding an epsilon transition (to model nonexecution of the loops): 306. Eliminating 1 self-loops for location f446 Removing the self-loops: 46. Adding an epsilon transition (to model nonexecution of the loops): 308. Eliminating 1 self-loops for location f452 Removing the self-loops: 47. Adding an epsilon transition (to model nonexecution of the loops): 310. Eliminating 1 self-loops for location f458 Removing the self-loops: 48. Adding an epsilon transition (to model nonexecution of the loops): 312. Eliminating 1 self-loops for location f466 Self-Loop 49 has the metering function: -2+C, resulting in the new transition 313. Removing the self-loops: 49. Eliminating 1 self-loops for location f472 Self-Loop 50 has the metering function: -1+C, resulting in the new transition 314. Removing the self-loops: 50. Eliminating 1 self-loops for location f478 Self-Loop 51 has the metering function: -2+C, resulting in the new transition 315. Removing the self-loops: 51. Eliminating 1 self-loops for location f484 Self-Loop 52 has the metering function: -1+C, resulting in the new transition 316. Removing the self-loops: 52. Eliminating 1 self-loops for location f492 Self-Loop 53 has the metering function: -1+C, resulting in the new transition 317. Removing the self-loops: 53. Eliminating 1 self-loops for location f498 Self-Loop 54 has the metering function: C, resulting in the new transition 318. Removing the self-loops: 54. Eliminating 1 self-loops for location f504 Self-Loop 55 has the metering function: -1+C, resulting in the new transition 319. Removing the self-loops: 55. Eliminating 1 self-loops for location f510 Self-Loop 56 has the metering function: C, resulting in the new transition 320. Removing the self-loops: 56. Eliminating 1 self-loops for location f518 Self-Loop 57 has the metering function: C, resulting in the new transition 321. Removing the self-loops: 57. Eliminating 1 self-loops for location f524 Self-Loop 58 has the metering function: 1+C, resulting in the new transition 322. Removing the self-loops: 58. Eliminating 1 self-loops for location f530 Self-Loop 59 has the metering function: C, resulting in the new transition 323. Removing the self-loops: 59. Eliminating 1 self-loops for location f536 Self-Loop 60 has the metering function: 1+C, resulting in the new transition 324. Removing the self-loops: 60. Eliminating 1 self-loops for location f544 Self-Loop 61 has the metering function: 1+C, resulting in the new transition 325. Removing the self-loops: 61. Eliminating 1 self-loops for location f550 Self-Loop 62 has the metering function: 2+C, resulting in the new transition 326. Removing the self-loops: 62. Eliminating 1 self-loops for location f556 Self-Loop 63 has the metering function: 1+C, resulting in the new transition 327. Removing the self-loops: 63. Eliminating 1 self-loops for location f562 Self-Loop 64 has the metering function: 2+C, resulting in the new transition 328. Removing the self-loops: 64. Eliminating 1 self-loops for location f570 Self-Loop 65 has the metering function: 2+C, resulting in the new transition 329. Removing the self-loops: 65. Eliminating 1 self-loops for location f576 Self-Loop 66 has the metering function: 3+C, resulting in the new transition 330. Removing the self-loops: 66. Eliminating 1 self-loops for location f582 Self-Loop 67 has the metering function: 2+C, resulting in the new transition 331. Removing the self-loops: 67. Eliminating 1 self-loops for location f588 Self-Loop 68 has the metering function: 3+C, resulting in the new transition 332. Removing the self-loops: 68. Eliminating 1 self-loops for location f596 Self-Loop 69 has the metering function: 3+C, resulting in the new transition 333. Removing the self-loops: 69. Eliminating 1 self-loops for location f602 Self-Loop 70 has the metering function: 4+C, resulting in the new transition 334. Removing the self-loops: 70. Eliminating 1 self-loops for location f608 Self-Loop 71 has the metering function: 3+C, resulting in the new transition 335. Removing the self-loops: 71. Eliminating 1 self-loops for location f614 Self-Loop 72 has the metering function: 4+C, resulting in the new transition 336. Removing the self-loops: 72. Eliminating 1 self-loops for location f622 Self-Loop 73 has the metering function: 5+C, resulting in the new transition 337. Removing the self-loops: 73. Eliminating 1 self-loops for location f628 Self-Loop 74 has the metering function: 6+C, resulting in the new transition 338. Removing the self-loops: 74. Eliminating 1 self-loops for location f634 Self-Loop 75 has the metering function: 5+C, resulting in the new transition 339. Removing the self-loops: 75. Eliminating 1 self-loops for location f640 Self-Loop 76 has the metering function: 6+C, resulting in the new transition 340. Removing the self-loops: 76. Eliminating 1 self-loops for location f648 Self-Loop 77 has the metering function: 7+C, resulting in the new transition 341. Removing the self-loops: 77. Eliminating 1 self-loops for location f654 Self-Loop 78 has the metering function: 8+C, resulting in the new transition 342. Removing the self-loops: 78. Eliminating 1 self-loops for location f660 Self-Loop 79 has the metering function: 7+C, resulting in the new transition 343. Removing the self-loops: 79. Eliminating 1 self-loops for location f666 Self-Loop 80 has the metering function: 8+C, resulting in the new transition 344. Removing the self-loops: 80. Eliminating 1 self-loops for location f674 Self-Loop 81 has the metering function: 8+C, resulting in the new transition 345. Removing the self-loops: 81. Eliminating 1 self-loops for location f680 Self-Loop 82 has the metering function: 9+C, resulting in the new transition 346. Removing the self-loops: 82. Eliminating 1 self-loops for location f686 Self-Loop 83 has the metering function: 8+C, resulting in the new transition 347. Removing the self-loops: 83. Eliminating 1 self-loops for location f692 Self-Loop 84 has the metering function: 9+C, resulting in the new transition 348. Removing the self-loops: 84. Eliminating 1 self-loops for location f700 Removing the self-loops: 85. Adding an epsilon transition (to model nonexecution of the loops): 350. Eliminating 1 self-loops for location f706 Removing the self-loops: 86. Adding an epsilon transition (to model nonexecution of the loops): 352. Eliminating 1 self-loops for location f712 Removing the self-loops: 87. Adding an epsilon transition (to model nonexecution of the loops): 354. Eliminating 1 self-loops for location f718 Removing the self-loops: 88. Adding an epsilon transition (to model nonexecution of the loops): 356. Eliminating 1 self-loops for location f726 Removing the self-loops: 89. Adding an epsilon transition (to model nonexecution of the loops): 358. Eliminating 1 self-loops for location f732 Removing the self-loops: 90. Adding an epsilon transition (to model nonexecution of the loops): 360. Eliminating 1 self-loops for location f738 Removing the self-loops: 91. Adding an epsilon transition (to model nonexecution of the loops): 362. Eliminating 1 self-loops for location f744 Removing the self-loops: 92. Adding an epsilon transition (to model nonexecution of the loops): 364. Eliminating 1 self-loops for location f752 Removing the self-loops: 93. Adding an epsilon transition (to model nonexecution of the loops): 366. Eliminating 1 self-loops for location f758 Removing the self-loops: 94. Adding an epsilon transition (to model nonexecution of the loops): 368. Eliminating 1 self-loops for location f764 Removing the self-loops: 95. Adding an epsilon transition (to model nonexecution of the loops): 370. Eliminating 1 self-loops for location f770 Removing the self-loops: 96. Adding an epsilon transition (to model nonexecution of the loops): 372. Eliminating 1 self-loops for location f778 Removing the self-loops: 97. Adding an epsilon transition (to model nonexecution of the loops): 374. Eliminating 1 self-loops for location f784 Removing the self-loops: 98. Adding an epsilon transition (to model nonexecution of the loops): 376. Eliminating 1 self-loops for location f790 Removing the self-loops: 99. Adding an epsilon transition (to model nonexecution of the loops): 378. Eliminating 1 self-loops for location f796 Removing the self-loops: 100. Adding an epsilon transition (to model nonexecution of the loops): 380. Eliminating 1 self-loops for location f804 Removing the self-loops: 101. Adding an epsilon transition (to model nonexecution of the loops): 382. Eliminating 1 self-loops for location f810 Removing the self-loops: 102. Adding an epsilon transition (to model nonexecution of the loops): 384. Eliminating 1 self-loops for location f816 Removing the self-loops: 103. Adding an epsilon transition (to model nonexecution of the loops): 386. Eliminating 1 self-loops for location f822 Removing the self-loops: 104. Adding an epsilon transition (to model nonexecution of the loops): 388. Eliminating 1 self-loops for location f830 Removing the self-loops: 105. Adding an epsilon transition (to model nonexecution of the loops): 390. Eliminating 1 self-loops for location f836 Removing the self-loops: 106. Adding an epsilon transition (to model nonexecution of the loops): 392. Eliminating 1 self-loops for location f842 Removing the self-loops: 107. Adding an epsilon transition (to model nonexecution of the loops): 394. Eliminating 1 self-loops for location f848 Removing the self-loops: 108. Adding an epsilon transition (to model nonexecution of the loops): 396. Eliminating 1 self-loops for location f856 Removing the self-loops: 109. Adding an epsilon transition (to model nonexecution of the loops): 398. Eliminating 1 self-loops for location f862 Removing the self-loops: 110. Adding an epsilon transition (to model nonexecution of the loops): 400. Eliminating 1 self-loops for location f868 Removing the self-loops: 111. Adding an epsilon transition (to model nonexecution of the loops): 402. Eliminating 1 self-loops for location f874 Removing the self-loops: 112. Adding an epsilon transition (to model nonexecution of the loops): 404. Eliminating 1 self-loops for location f882 Removing the self-loops: 113. Adding an epsilon transition (to model nonexecution of the loops): 406. Eliminating 1 self-loops for location f888 Removing the self-loops: 114. Adding an epsilon transition (to model nonexecution of the loops): 408. Eliminating 1 self-loops for location f894 Removing the self-loops: 115. Adding an epsilon transition (to model nonexecution of the loops): 410. Eliminating 1 self-loops for location f900 Removing the self-loops: 116. Adding an epsilon transition (to model nonexecution of the loops): 412. Eliminating 1 self-loops for location f908 Removing the self-loops: 117. Adding an epsilon transition (to model nonexecution of the loops): 414. Eliminating 1 self-loops for location f914 Removing the self-loops: 118. Adding an epsilon transition (to model nonexecution of the loops): 416. Eliminating 1 self-loops for location f920 Removing the self-loops: 119. Adding an epsilon transition (to model nonexecution of the loops): 418. Eliminating 1 self-loops for location f926 Removing the self-loops: 120. Adding an epsilon transition (to model nonexecution of the loops): 420. Removed all Self-loops using metering functions (where possible): Start location: f0 0: f0 -> f154 : A'=0, B'=2, C'=0, [], cost: 1 241: f154 -> [122] : A'=1/2-C*(-3+C)-1/2*C+1/2*(-3+C)^2+A, C'=3, [ 2>=C ], cost: 3-C 242: f160 -> [123] : A'=1+1/2*(-4+C)^2-1/2*C-C*(-4+C)+A, C'=4, [ 3>=C ], cost: 4-C 243: f166 -> [124] : A'=1/2-C*(-3+C)-1/2*C+1/2*(-3+C)^2+A, C'=3, [ 2>=C ], cost: 3-C 244: f172 -> [125] : A'=1+1/2*(-4+C)^2-1/2*C-C*(-4+C)+A, C'=4, [ 3>=C ], cost: 4-C 245: f180 -> [126] : A'=-C*(-2+C)-1/2*C+1/2*(-2+C)^2+A, C'=2, [ 1>=C ], cost: 2-C 246: f186 -> [127] : A'=1/2-C*(-3+C)-1/2*C+1/2*(-3+C)^2+A, C'=3, [ 2>=C ], cost: 3-C 247: f192 -> [128] : A'=-C*(-2+C)-1/2*C+1/2*(-2+C)^2+A, C'=2, [ 1>=C ], cost: 2-C 248: f198 -> [129] : A'=1/2-C*(-3+C)-1/2*C+1/2*(-3+C)^2+A, C'=3, [ 2>=C ], cost: 3-C 249: f206 -> [130] : A'=-2+1/2*(2+C)^2-1/2*C-C*(2+C)+A, C'=-2, [ 0>=3+C ], cost: -2-C 250: f212 -> [131] : A'=-3/2-(1+C)*C-1/2*C+1/2*(1+C)^2+A, C'=-1, [ 0>=2+C ], cost: -1-C 251: f218 -> [132] : A'=-2+1/2*(2+C)^2-1/2*C-C*(2+C)+A, C'=-2, [ 0>=3+C ], cost: -2-C 252: f224 -> [133] : A'=-3/2-(1+C)*C-1/2*C+1/2*(1+C)^2+A, C'=-1, [ 0>=2+C ], cost: -1-C 253: f232 -> [134] : A'=-3/2-(1+C)*C-1/2*C+1/2*(1+C)^2+A, C'=-1, [ 0>=2+C ], cost: -1-C 254: f238 -> [135] : A'=-1-1/2*C+A-1/2*C^2, C'=0, [ 0>=1+C ], cost: -C 255: f244 -> [136] : A'=-3/2-(1+C)*C-1/2*C+1/2*(1+C)^2+A, C'=-1, [ 0>=2+C ], cost: -1-C 256: f250 -> [137] : A'=-1-1/2*C+A-1/2*C^2, C'=0, [ 0>=1+C ], cost: -C 257: f258 -> [138] : A'=-1-1/2*C+A-1/2*C^2, C'=0, [ 0>=1+C ], cost: -C 258: f264 -> [139] : A'=-1/2+1/2*(-1+C)^2-(-1+C)*C-1/2*C+A, C'=1, [ 0>=C ], cost: 1-C 259: f270 -> [140] : A'=-1-1/2*C+A-1/2*C^2, C'=0, [ 0>=1+C ], cost: -C 260: f276 -> [141] : A'=-1/2+1/2*(-1+C)^2-(-1+C)*C-1/2*C+A, C'=1, [ 0>=C ], cost: 1-C 261: f284 -> [142] : A'=1+1/2*(-4+C)^2-1/2*C-C*(-4+C)+A, C'=4, [ 3>=C ], cost: 4-C 262: f290 -> [143] : A'=3/2+1/2*(-5+C)^2-1/2*C-C*(-5+C)+A, C'=5, [ 4>=C ], cost: 5-C 263: f296 -> [144] : A'=1+1/2*(-4+C)^2-1/2*C-C*(-4+C)+A, C'=4, [ 3>=C ], cost: 4-C 264: f302 -> [145] : A'=3/2+1/2*(-5+C)^2-1/2*C-C*(-5+C)+A, C'=5, [ 4>=C ], cost: 5-C 265: f310 -> [146] : A'=C+A, C'=B+C, [ 2>=C ], cost: 1 266: f310 -> [146] : [], cost: 0 267: f316 -> [147] : A'=C+A, C'=B+C, [ 3>=C ], cost: 1 268: f316 -> [147] : [], cost: 0 269: f322 -> [148] : A'=C+A, C'=B+C, [ 2>=C ], cost: 1 270: f322 -> [148] : [], cost: 0 271: f328 -> [149] : A'=C+A, C'=B+C, [ 3>=C ], cost: 1 272: f328 -> [149] : [], cost: 0 273: f336 -> [150] : A'=C+A, C'=B+C, [ 1>=C ], cost: 1 274: f336 -> [150] : [], cost: 0 275: f342 -> [151] : A'=C+A, C'=B+C, [ 2>=C ], cost: 1 276: f342 -> [151] : [], cost: 0 277: f348 -> [152] : A'=C+A, C'=B+C, [ 1>=C ], cost: 1 278: f348 -> [152] : [], cost: 0 279: f354 -> [153] : A'=C+A, C'=B+C, [ 2>=C ], cost: 1 280: f354 -> [153] : [], cost: 0 281: f362 -> [154] : A'=C+A, C'=B+C, [ 0>=3+C ], cost: 1 282: f362 -> [154] : [], cost: 0 283: f368 -> [155] : A'=C+A, C'=B+C, [ 0>=2+C ], cost: 1 284: f368 -> [155] : [], cost: 0 285: f374 -> [156] : A'=C+A, C'=B+C, [ 0>=3+C ], cost: 1 286: f374 -> [156] : [], cost: 0 287: f380 -> [157] : A'=C+A, C'=B+C, [ 0>=2+C ], cost: 1 288: f380 -> [157] : [], cost: 0 289: f388 -> [158] : A'=C+A, C'=B+C, [ 0>=2+C ], cost: 1 290: f388 -> [158] : [], cost: 0 291: f394 -> [159] : A'=C+A, C'=B+C, [ 0>=1+C ], cost: 1 292: f394 -> [159] : [], cost: 0 293: f400 -> [160] : A'=C+A, C'=B+C, [ 0>=2+C ], cost: 1 294: f400 -> [160] : [], cost: 0 295: f406 -> [161] : A'=C+A, C'=B+C, [ 0>=1+C ], cost: 1 296: f406 -> [161] : [], cost: 0 297: f414 -> [162] : A'=C+A, C'=B+C, [ 0>=1+C ], cost: 1 298: f414 -> [162] : [], cost: 0 299: f420 -> [163] : A'=C+A, C'=B+C, [ 0>=C ], cost: 1 300: f420 -> [163] : [], cost: 0 301: f426 -> [164] : A'=C+A, C'=B+C, [ 0>=1+C ], cost: 1 302: f426 -> [164] : [], cost: 0 303: f432 -> [165] : A'=C+A, C'=B+C, [ 0>=C ], cost: 1 304: f432 -> [165] : [], cost: 0 305: f440 -> [166] : A'=C+A, C'=B+C, [ 3>=C ], cost: 1 306: f440 -> [166] : [], cost: 0 307: f446 -> [167] : A'=C+A, C'=B+C, [ 4>=C ], cost: 1 308: f446 -> [167] : [], cost: 0 309: f452 -> [168] : A'=C+A, C'=B+C, [ 3>=C ], cost: 1 310: f452 -> [168] : [], cost: 0 311: f458 -> [169] : A'=C+A, C'=B+C, [ 4>=C ], cost: 1 312: f458 -> [169] : [], cost: 0 313: f466 -> [170] : A'=2+C*(-2+C)-1/2*C-1/2*(-2+C)^2+A, C'=2, [ C>=3 ], cost: -2+C 314: f472 -> [171] : A'=3/2-1/2*(-1+C)^2+(-1+C)*C-1/2*C+A, C'=1, [ C>=2 ], cost: -1+C 315: f478 -> [172] : A'=2+C*(-2+C)-1/2*C-1/2*(-2+C)^2+A, C'=2, [ C>=3 ], cost: -2+C 316: f484 -> [173] : A'=3/2-1/2*(-1+C)^2+(-1+C)*C-1/2*C+A, C'=1, [ C>=2 ], cost: -1+C 317: f492 -> [174] : A'=3/2-1/2*(-1+C)^2+(-1+C)*C-1/2*C+A, C'=1, [ C>=2 ], cost: -1+C 318: f498 -> [175] : A'=1-1/2*C+A+1/2*C^2, C'=0, [ C>=1 ], cost: C 319: f504 -> [176] : A'=3/2-1/2*(-1+C)^2+(-1+C)*C-1/2*C+A, C'=1, [ C>=2 ], cost: -1+C 320: f510 -> [177] : A'=1-1/2*C+A+1/2*C^2, C'=0, [ C>=1 ], cost: C 321: f518 -> [178] : A'=1-1/2*C+A+1/2*C^2, C'=0, [ C>=1 ], cost: C 322: f524 -> [179] : A'=1/2+(1+C)*C-1/2*C-1/2*(1+C)^2+A, C'=-1, [ C>=0 ], cost: 1+C 323: f530 -> [180] : A'=1-1/2*C+A+1/2*C^2, C'=0, [ C>=1 ], cost: C 324: f536 -> [181] : A'=1/2+(1+C)*C-1/2*C-1/2*(1+C)^2+A, C'=-1, [ C>=0 ], cost: 1+C 325: f544 -> [182] : A'=1/2+(1+C)*C-1/2*C-1/2*(1+C)^2+A, C'=-1, [ C>=0 ], cost: 1+C 326: f550 -> [183] : A'=-1/2*(2+C)^2-1/2*C+C*(2+C)+A, C'=-2, [ 1+C>=0 ], cost: 2+C 327: f556 -> [184] : A'=1/2+(1+C)*C-1/2*C-1/2*(1+C)^2+A, C'=-1, [ C>=0 ], cost: 1+C 328: f562 -> [185] : A'=-1/2*(2+C)^2-1/2*C+C*(2+C)+A, C'=-2, [ 1+C>=0 ], cost: 2+C 329: f570 -> [186] : A'=-1/2*(2+C)^2-1/2*C+C*(2+C)+A, C'=-2, [ 1+C>=0 ], cost: 2+C 330: f576 -> [187] : A'=-1/2-1/2*(3+C)^2-1/2*C+C*(3+C)+A, C'=-3, [ 2+C>=0 ], cost: 3+C 331: f582 -> [188] : A'=-1/2*(2+C)^2-1/2*C+C*(2+C)+A, C'=-2, [ 1+C>=0 ], cost: 2+C 332: f588 -> [189] : A'=-1/2-1/2*(3+C)^2-1/2*C+C*(3+C)+A, C'=-3, [ 2+C>=0 ], cost: 3+C 333: f596 -> [190] : A'=-1/2-1/2*(3+C)^2-1/2*C+C*(3+C)+A, C'=-3, [ 2+C>=0 ], cost: 3+C 334: f602 -> [191] : A'=-1-1/2*(4+C)^2-1/2*C+(4+C)*C+A, C'=-4, [ 3+C>=0 ], cost: 4+C 335: f608 -> [192] : A'=-1/2-1/2*(3+C)^2-1/2*C+C*(3+C)+A, C'=-3, [ 2+C>=0 ], cost: 3+C 336: f614 -> [193] : A'=-1-1/2*(4+C)^2-1/2*C+(4+C)*C+A, C'=-4, [ 3+C>=0 ], cost: 4+C 337: f622 -> [194] : A'=-3/2-1/2*C-1/2*(5+C)^2+(5+C)*C+A, C'=-5, [ 4+C>=0 ], cost: 5+C 338: f628 -> [195] : A'=-2+(6+C)*C-1/2*C-1/2*(6+C)^2+A, C'=-6, [ 5+C>=0 ], cost: 6+C 339: f634 -> [196] : A'=-3/2-1/2*C-1/2*(5+C)^2+(5+C)*C+A, C'=-5, [ 4+C>=0 ], cost: 5+C 340: f640 -> [197] : A'=-2+(6+C)*C-1/2*C-1/2*(6+C)^2+A, C'=-6, [ 5+C>=0 ], cost: 6+C 341: f648 -> [198] : A'=-5/2+(7+C)*C-1/2*C-1/2*(7+C)^2+A, C'=-7, [ 6+C>=0 ], cost: 7+C 342: f654 -> [199] : A'=-3+(8+C)*C-1/2*C+A-1/2*(8+C)^2, C'=-8, [ 7+C>=0 ], cost: 8+C 343: f660 -> [200] : A'=-5/2+(7+C)*C-1/2*C-1/2*(7+C)^2+A, C'=-7, [ 6+C>=0 ], cost: 7+C 344: f666 -> [201] : A'=-3+(8+C)*C-1/2*C+A-1/2*(8+C)^2, C'=-8, [ 7+C>=0 ], cost: 8+C 345: f674 -> [202] : A'=-3+(8+C)*C-1/2*C+A-1/2*(8+C)^2, C'=-8, [ 7+C>=0 ], cost: 8+C 346: f680 -> [203] : A'=-7/2-1/2*(9+C)^2-1/2*C+C*(9+C)+A, C'=-9, [ 8+C>=0 ], cost: 9+C 347: f686 -> [204] : A'=-3+(8+C)*C-1/2*C+A-1/2*(8+C)^2, C'=-8, [ 7+C>=0 ], cost: 8+C 348: f692 -> [205] : A'=-7/2-1/2*(9+C)^2-1/2*C+C*(9+C)+A, C'=-9, [ 8+C>=0 ], cost: 9+C 349: f700 -> [206] : A'=C+A, C'=-B+C, [ C>=3 ], cost: 1 350: f700 -> [206] : [], cost: 0 351: f706 -> [207] : A'=C+A, C'=-B+C, [ C>=2 ], cost: 1 352: f706 -> [207] : [], cost: 0 353: f712 -> [208] : A'=C+A, C'=-B+C, [ C>=3 ], cost: 1 354: f712 -> [208] : [], cost: 0 355: f718 -> [209] : A'=C+A, C'=-B+C, [ C>=2 ], cost: 1 356: f718 -> [209] : [], cost: 0 357: f726 -> [210] : A'=C+A, C'=-B+C, [ C>=2 ], cost: 1 358: f726 -> [210] : [], cost: 0 359: f732 -> [211] : A'=C+A, C'=-B+C, [ C>=1 ], cost: 1 360: f732 -> [211] : [], cost: 0 361: f738 -> [212] : A'=C+A, C'=-B+C, [ C>=2 ], cost: 1 362: f738 -> [212] : [], cost: 0 363: f744 -> [213] : A'=C+A, C'=-B+C, [ C>=1 ], cost: 1 364: f744 -> [213] : [], cost: 0 365: f752 -> [214] : A'=C+A, C'=-B+C, [ C>=1 ], cost: 1 366: f752 -> [214] : [], cost: 0 367: f758 -> [215] : A'=C+A, C'=-B+C, [ C>=0 ], cost: 1 368: f758 -> [215] : [], cost: 0 369: f764 -> [216] : A'=C+A, C'=-B+C, [ C>=1 ], cost: 1 370: f764 -> [216] : [], cost: 0 371: f770 -> [217] : A'=C+A, C'=-B+C, [ C>=0 ], cost: 1 372: f770 -> [217] : [], cost: 0 373: f778 -> [218] : A'=C+A, C'=-B+C, [ C>=0 ], cost: 1 374: f778 -> [218] : [], cost: 0 375: f784 -> [219] : A'=C+A, C'=-B+C, [ 1+C>=0 ], cost: 1 376: f784 -> [219] : [], cost: 0 377: f790 -> [220] : A'=C+A, C'=-B+C, [ C>=0 ], cost: 1 378: f790 -> [220] : [], cost: 0 379: f796 -> [221] : A'=C+A, C'=-B+C, [ 1+C>=0 ], cost: 1 380: f796 -> [221] : [], cost: 0 381: f804 -> [222] : A'=C+A, C'=-B+C, [ 1+C>=0 ], cost: 1 382: f804 -> [222] : [], cost: 0 383: f810 -> [223] : A'=C+A, C'=-B+C, [ 2+C>=0 ], cost: 1 384: f810 -> [223] : [], cost: 0 385: f816 -> [224] : A'=C+A, C'=-B+C, [ 1+C>=0 ], cost: 1 386: f816 -> [224] : [], cost: 0 387: f822 -> [225] : A'=C+A, C'=-B+C, [ 2+C>=0 ], cost: 1 388: f822 -> [225] : [], cost: 0 389: f830 -> [226] : A'=C+A, C'=-B+C, [ 2+C>=0 ], cost: 1 390: f830 -> [226] : [], cost: 0 391: f836 -> [227] : A'=C+A, C'=-B+C, [ 3+C>=0 ], cost: 1 392: f836 -> [227] : [], cost: 0 393: f842 -> [228] : A'=C+A, C'=-B+C, [ 2+C>=0 ], cost: 1 394: f842 -> [228] : [], cost: 0 395: f848 -> [229] : A'=C+A, C'=-B+C, [ 3+C>=0 ], cost: 1 396: f848 -> [229] : [], cost: 0 397: f856 -> [230] : A'=C+A, C'=-B+C, [ 4+C>=0 ], cost: 1 398: f856 -> [230] : [], cost: 0 399: f862 -> [231] : A'=C+A, C'=-B+C, [ 5+C>=0 ], cost: 1 400: f862 -> [231] : [], cost: 0 401: f868 -> [232] : A'=C+A, C'=-B+C, [ 4+C>=0 ], cost: 1 402: f868 -> [232] : [], cost: 0 403: f874 -> [233] : A'=C+A, C'=-B+C, [ 5+C>=0 ], cost: 1 404: f874 -> [233] : [], cost: 0 405: f882 -> [234] : A'=C+A, C'=-B+C, [ 6+C>=0 ], cost: 1 406: f882 -> [234] : [], cost: 0 407: f888 -> [235] : A'=C+A, C'=-B+C, [ 7+C>=0 ], cost: 1 408: f888 -> [235] : [], cost: 0 409: f894 -> [236] : A'=C+A, C'=-B+C, [ 6+C>=0 ], cost: 1 410: f894 -> [236] : [], cost: 0 411: f900 -> [237] : A'=C+A, C'=-B+C, [ 7+C>=0 ], cost: 1 412: f900 -> [237] : [], cost: 0 413: f908 -> [238] : A'=C+A, C'=-B+C, [ 7+C>=0 ], cost: 1 414: f908 -> [238] : [], cost: 0 415: f914 -> [239] : A'=C+A, C'=-B+C, [ 8+C>=0 ], cost: 1 416: f914 -> [239] : [], cost: 0 417: f920 -> [240] : A'=C+A, C'=-B+C, [ 7+C>=0 ], cost: 1 418: f920 -> [240] : [], cost: 0 419: f926 -> [241] : A'=C+A, C'=-B+C, [ 8+C>=0 ], cost: 1 420: f926 -> [241] : [], cost: 0 240: [122] -> f160 : C'=0, [ C>=3 ], cost: 1 239: [123] -> f166 : C'=0, [ C>=4 ], cost: 1 238: [124] -> f172 : C'=0, [ C>=3 ], cost: 1 237: [125] -> f180 : C'=1, [ C>=4 ], cost: 1 236: [126] -> f186 : C'=1, [ C>=2 ], cost: 1 235: [127] -> f192 : C'=1, [ C>=3 ], cost: 1 234: [128] -> f198 : C'=1, [ C>=2 ], cost: 1 233: [129] -> f206 : C'=-3, [ C>=3 ], cost: 1 232: [130] -> f212 : C'=-3, [ 2+C>=0 ], cost: 1 231: [131] -> f218 : C'=-3, [ 1+C>=0 ], cost: 1 230: [132] -> f224 : C'=-3, [ 2+C>=0 ], cost: 1 229: [133] -> f232 : C'=-4, [ 1+C>=0 ], cost: 1 228: [134] -> f238 : C'=-4, [ 1+C>=0 ], cost: 1 227: [135] -> f244 : C'=-4, [ C>=0 ], cost: 1 226: [136] -> f250 : C'=-4, [ 1+C>=0 ], cost: 1 225: [137] -> f258 : C'=-5, [ C>=0 ], cost: 1 224: [138] -> f264 : C'=-5, [ C>=0 ], cost: 1 223: [139] -> f270 : C'=-5, [ C>=1 ], cost: 1 222: [140] -> f276 : C'=-5, [ C>=0 ], cost: 1 221: [141] -> f284 : C'=-6, [ C>=1 ], cost: 1 220: [142] -> f290 : C'=-6, [ C>=4 ], cost: 1 219: [143] -> f296 : C'=-6, [ C>=5 ], cost: 1 218: [144] -> f302 : C'=-6, [ C>=4 ], cost: 1 217: [145] -> f310 : C'=0, [ C>=5 ], cost: 1 216: [146] -> f316 : C'=0, [ C>=3 ], cost: 1 215: [147] -> f322 : C'=0, [ C>=4 ], cost: 1 214: [148] -> f328 : C'=0, [ C>=3 ], cost: 1 213: [149] -> f336 : C'=1, [ C>=4 ], cost: 1 212: [150] -> f342 : C'=1, [ C>=2 ], cost: 1 211: [151] -> f348 : C'=1, [ C>=3 ], cost: 1 210: [152] -> f354 : C'=1, [ C>=2 ], cost: 1 209: [153] -> f362 : C'=-3, [ C>=3 ], cost: 1 208: [154] -> f368 : C'=-3, [ 2+C>=0 ], cost: 1 207: [155] -> f374 : C'=-3, [ 1+C>=0 ], cost: 1 206: [156] -> f380 : C'=-3, [ 2+C>=0 ], cost: 1 205: [157] -> f388 : C'=-4, [ 1+C>=0 ], cost: 1 204: [158] -> f394 : C'=-4, [ 1+C>=0 ], cost: 1 203: [159] -> f400 : C'=-4, [ C>=0 ], cost: 1 202: [160] -> f406 : C'=-4, [ 1+C>=0 ], cost: 1 201: [161] -> f414 : C'=-5, [ C>=0 ], cost: 1 200: [162] -> f420 : C'=-5, [ C>=0 ], cost: 1 199: [163] -> f426 : C'=-5, [ C>=1 ], cost: 1 198: [164] -> f432 : C'=-5, [ C>=0 ], cost: 1 197: [165] -> f440 : C'=-6, [ C>=1 ], cost: 1 196: [166] -> f446 : C'=-6, [ C>=4 ], cost: 1 195: [167] -> f452 : C'=-6, [ C>=5 ], cost: 1 194: [168] -> f458 : C'=-6, [ C>=4 ], cost: 1 193: [169] -> f466 : C'=5, [ C>=5 ], cost: 1 192: [170] -> f472 : C'=5, [ 2>=C ], cost: 1 191: [171] -> f478 : C'=5, [ 1>=C ], cost: 1 190: [172] -> f484 : C'=5, [ 2>=C ], cost: 1 189: [173] -> f492 : C'=6, [ 1>=C ], cost: 1 188: [174] -> f498 : C'=6, [ 1>=C ], cost: 1 187: [175] -> f504 : C'=6, [ 0>=C ], cost: 1 186: [176] -> f510 : C'=6, [ 1>=C ], cost: 1 185: [177] -> f518 : C'=7, [ 0>=C ], cost: 1 184: [178] -> f524 : C'=7, [ 0>=C ], cost: 1 183: [179] -> f530 : C'=7, [ 0>=1+C ], cost: 1 182: [180] -> f536 : C'=7, [ 0>=C ], cost: 1 181: [181] -> f544 : C'=8, [ 0>=1+C ], cost: 1 180: [182] -> f550 : C'=8, [ 0>=1+C ], cost: 1 179: [183] -> f556 : C'=8, [ 0>=2+C ], cost: 1 178: [184] -> f562 : C'=8, [ 0>=1+C ], cost: 1 177: [185] -> f570 : C'=9, [ 0>=2+C ], cost: 1 176: [186] -> f576 : C'=9, [ 0>=2+C ], cost: 1 175: [187] -> f582 : C'=9, [ 0>=3+C ], cost: 1 174: [188] -> f588 : C'=9, [ 0>=2+C ], cost: 1 173: [189] -> f596 : C'=0, [ 0>=3+C ], cost: 1 172: [190] -> f602 : C'=0, [ 0>=3+C ], cost: 1 171: [191] -> f608 : C'=0, [ 0>=4+C ], cost: 1 170: [192] -> f614 : C'=0, [ 0>=3+C ], cost: 1 169: [193] -> f622 : C'=-1, [ 0>=4+C ], cost: 1 168: [194] -> f628 : C'=-1, [ 0>=5+C ], cost: 1 167: [195] -> f634 : C'=-1, [ 0>=6+C ], cost: 1 166: [196] -> f640 : C'=-1, [ 0>=5+C ], cost: 1 165: [197] -> f648 : C'=-2, [ 0>=6+C ], cost: 1 164: [198] -> f654 : C'=-2, [ 0>=7+C ], cost: 1 163: [199] -> f660 : C'=-2, [ 0>=8+C ], cost: 1 162: [200] -> f666 : C'=-2, [ 0>=7+C ], cost: 1 161: [201] -> f674 : C'=16, [ 0>=8+C ], cost: 1 160: [202] -> f680 : C'=16, [ 0>=8+C ], cost: 1 159: [203] -> f686 : C'=16, [ 0>=9+C ], cost: 1 158: [204] -> f692 : C'=16, [ 0>=8+C ], cost: 1 157: [205] -> f700 : C'=5, [ 0>=9+C ], cost: 1 156: [206] -> f706 : C'=5, [ 2>=C ], cost: 1 155: [207] -> f712 : C'=5, [ 1>=C ], cost: 1 154: [208] -> f718 : C'=5, [ 2>=C ], cost: 1 153: [209] -> f726 : C'=6, [ 1>=C ], cost: 1 152: [210] -> f732 : C'=6, [ 1>=C ], cost: 1 151: [211] -> f738 : C'=6, [ 0>=C ], cost: 1 150: [212] -> f744 : C'=6, [ 1>=C ], cost: 1 149: [213] -> f752 : C'=7, [ 0>=C ], cost: 1 148: [214] -> f758 : C'=7, [ 0>=C ], cost: 1 147: [215] -> f764 : C'=7, [ 0>=1+C ], cost: 1 146: [216] -> f770 : C'=7, [ 0>=C ], cost: 1 145: [217] -> f778 : C'=8, [ 0>=1+C ], cost: 1 144: [218] -> f784 : C'=8, [ 0>=1+C ], cost: 1 143: [219] -> f790 : C'=8, [ 0>=2+C ], cost: 1 142: [220] -> f796 : C'=8, [ 0>=1+C ], cost: 1 141: [221] -> f804 : C'=9, [ 0>=2+C ], cost: 1 140: [222] -> f810 : C'=9, [ 0>=2+C ], cost: 1 139: [223] -> f816 : C'=9, [ 0>=3+C ], cost: 1 138: [224] -> f822 : C'=9, [ 0>=2+C ], cost: 1 137: [225] -> f830 : C'=0, [ 0>=3+C ], cost: 1 136: [226] -> f836 : C'=0, [ 0>=3+C ], cost: 1 135: [227] -> f842 : C'=0, [ 0>=4+C ], cost: 1 134: [228] -> f848 : C'=0, [ 0>=3+C ], cost: 1 133: [229] -> f856 : C'=-1, [ 0>=4+C ], cost: 1 132: [230] -> f862 : C'=-1, [ 0>=5+C ], cost: 1 131: [231] -> f868 : C'=-1, [ 0>=6+C ], cost: 1 130: [232] -> f874 : C'=-1, [ 0>=5+C ], cost: 1 129: [233] -> f882 : C'=-2, [ 0>=6+C ], cost: 1 128: [234] -> f888 : C'=-2, [ 0>=7+C ], cost: 1 127: [235] -> f894 : C'=-2, [ 0>=8+C ], cost: 1 126: [236] -> f900 : C'=-2, [ 0>=7+C ], cost: 1 125: [237] -> f908 : C'=16, [ 0>=8+C ], cost: 1 124: [238] -> f914 : C'=16, [ 0>=8+C ], cost: 1 123: [239] -> f920 : C'=16, [ 0>=9+C ], cost: 1 122: [240] -> f926 : C'=16, [ 0>=8+C ], cost: 1 Applied simple chaining: Start location: f0 0: f0 -> f310 : A'=-60, B'=2, C'=0, [ 2>=0 && 3>=3 && 3>=0 && 4>=4 && 2>=0 && 3>=3 && 3>=0 && 4>=4 && 1>=1 && 2>=2 && 2>=1 && 3>=3 && 1>=1 && 2>=2 && 2>=1 && 3>=3 && 0>=0 && 0>=0 && 0>=-1 && 0>=0 && 0>=0 && 0>=0 && 0>=-1 && 0>=0 && 0>=-2 && 0>=0 && 0>=-3 && 0>=0 && 0>=-2 && 0>=0 && 0>=-3 && 0>=0 && 0>=-4 && 0>=0 && 0>=-5 && 1>=1 && 0>=-4 && 0>=0 && 0>=-5 && 1>=1 && 3>=-6 && 4>=4 && 4>=-6 && 5>=5 && 3>=-6 && 4>=4 && 4>=-6 && 5>=5 ], cost: 129 265: f310 -> [146] : A'=C+A, C'=B+C, [ 2>=C ], cost: 1 266: f310 -> [146] : [], cost: 0 267: f316 -> [147] : A'=C+A, C'=B+C, [ 3>=C ], cost: 1 268: f316 -> [147] : [], cost: 0 269: f322 -> [148] : A'=C+A, C'=B+C, [ 2>=C ], cost: 1 270: f322 -> [148] : [], cost: 0 271: f328 -> [149] : A'=C+A, C'=B+C, [ 3>=C ], cost: 1 272: f328 -> [149] : [], cost: 0 273: f336 -> [150] : A'=C+A, C'=B+C, [ 1>=C ], cost: 1 274: f336 -> [150] : [], cost: 0 275: f342 -> [151] : A'=C+A, C'=B+C, [ 2>=C ], cost: 1 276: f342 -> [151] : [], cost: 0 277: f348 -> [152] : A'=C+A, C'=B+C, [ 1>=C ], cost: 1 278: f348 -> [152] : [], cost: 0 279: f354 -> [153] : A'=C+A, C'=B+C, [ 2>=C ], cost: 1 280: f354 -> [153] : [], cost: 0 281: f362 -> [154] : A'=C+A, C'=B+C, [ 0>=3+C ], cost: 1 282: f362 -> [154] : [], cost: 0 283: f368 -> [155] : A'=C+A, C'=B+C, [ 0>=2+C ], cost: 1 284: f368 -> [155] : [], cost: 0 285: f374 -> [156] : A'=C+A, C'=B+C, [ 0>=3+C ], cost: 1 286: f374 -> [156] : [], cost: 0 287: f380 -> [157] : A'=C+A, C'=B+C, [ 0>=2+C ], cost: 1 288: f380 -> [157] : [], cost: 0 289: f388 -> [158] : A'=C+A, C'=B+C, [ 0>=2+C ], cost: 1 290: f388 -> [158] : [], cost: 0 291: f394 -> [159] : A'=C+A, C'=B+C, [ 0>=1+C ], cost: 1 292: f394 -> [159] : [], cost: 0 293: f400 -> [160] : A'=C+A, C'=B+C, [ 0>=2+C ], cost: 1 294: f400 -> [160] : [], cost: 0 295: f406 -> [161] : A'=C+A, C'=B+C, [ 0>=1+C ], cost: 1 296: f406 -> [161] : [], cost: 0 297: f414 -> [162] : A'=C+A, C'=B+C, [ 0>=1+C ], cost: 1 298: f414 -> [162] : [], cost: 0 299: f420 -> [163] : A'=C+A, C'=B+C, [ 0>=C ], cost: 1 300: f420 -> [163] : [], cost: 0 301: f426 -> [164] : A'=C+A, C'=B+C, [ 0>=1+C ], cost: 1 302: f426 -> [164] : [], cost: 0 303: f432 -> [165] : A'=C+A, C'=B+C, [ 0>=C ], cost: 1 304: f432 -> [165] : [], cost: 0 305: f440 -> [166] : A'=C+A, C'=B+C, [ 3>=C ], cost: 1 306: f440 -> [166] : [], cost: 0 307: f446 -> [167] : A'=C+A, C'=B+C, [ 4>=C ], cost: 1 308: f446 -> [167] : [], cost: 0 309: f452 -> [168] : A'=C+A, C'=B+C, [ 3>=C ], cost: 1 310: f452 -> [168] : [], cost: 0 311: f458 -> [169] : A'=C+A, C'=B+C, [ 4>=C ], cost: 1 312: f458 -> [169] : [], cost: 0 349: f700 -> [206] : A'=C+A, C'=-B+C, [ C>=3 ], cost: 1 350: f700 -> [206] : [], cost: 0 351: f706 -> [207] : A'=C+A, C'=-B+C, [ C>=2 ], cost: 1 352: f706 -> [207] : [], cost: 0 353: f712 -> [208] : A'=C+A, C'=-B+C, [ C>=3 ], cost: 1 354: f712 -> [208] : [], cost: 0 355: f718 -> [209] : A'=C+A, C'=-B+C, [ C>=2 ], cost: 1 356: f718 -> [209] : [], cost: 0 357: f726 -> [210] : A'=C+A, C'=-B+C, [ C>=2 ], cost: 1 358: f726 -> [210] : [], cost: 0 359: f732 -> [211] : A'=C+A, C'=-B+C, [ C>=1 ], cost: 1 360: f732 -> [211] : [], cost: 0 361: f738 -> [212] : A'=C+A, C'=-B+C, [ C>=2 ], cost: 1 362: f738 -> [212] : [], cost: 0 363: f744 -> [213] : A'=C+A, C'=-B+C, [ C>=1 ], cost: 1 364: f744 -> [213] : [], cost: 0 365: f752 -> [214] : A'=C+A, C'=-B+C, [ C>=1 ], cost: 1 366: f752 -> [214] : [], cost: 0 367: f758 -> [215] : A'=C+A, C'=-B+C, [ C>=0 ], cost: 1 368: f758 -> [215] : [], cost: 0 369: f764 -> [216] : A'=C+A, C'=-B+C, [ C>=1 ], cost: 1 370: f764 -> [216] : [], cost: 0 371: f770 -> [217] : A'=C+A, C'=-B+C, [ C>=0 ], cost: 1 372: f770 -> [217] : [], cost: 0 373: f778 -> [218] : A'=C+A, C'=-B+C, [ C>=0 ], cost: 1 374: f778 -> [218] : [], cost: 0 375: f784 -> [219] : A'=C+A, C'=-B+C, [ 1+C>=0 ], cost: 1 376: f784 -> [219] : [], cost: 0 377: f790 -> [220] : A'=C+A, C'=-B+C, [ C>=0 ], cost: 1 378: f790 -> [220] : [], cost: 0 379: f796 -> [221] : A'=C+A, C'=-B+C, [ 1+C>=0 ], cost: 1 380: f796 -> [221] : [], cost: 0 381: f804 -> [222] : A'=C+A, C'=-B+C, [ 1+C>=0 ], cost: 1 382: f804 -> [222] : [], cost: 0 383: f810 -> [223] : A'=C+A, C'=-B+C, [ 2+C>=0 ], cost: 1 384: f810 -> [223] : [], cost: 0 385: f816 -> [224] : A'=C+A, C'=-B+C, [ 1+C>=0 ], cost: 1 386: f816 -> [224] : [], cost: 0 387: f822 -> [225] : A'=C+A, C'=-B+C, [ 2+C>=0 ], cost: 1 388: f822 -> [225] : [], cost: 0 389: f830 -> [226] : A'=C+A, C'=-B+C, [ 2+C>=0 ], cost: 1 390: f830 -> [226] : [], cost: 0 391: f836 -> [227] : A'=C+A, C'=-B+C, [ 3+C>=0 ], cost: 1 392: f836 -> [227] : [], cost: 0 393: f842 -> [228] : A'=C+A, C'=-B+C, [ 2+C>=0 ], cost: 1 394: f842 -> [228] : [], cost: 0 395: f848 -> [229] : A'=C+A, C'=-B+C, [ 3+C>=0 ], cost: 1 396: f848 -> [229] : [], cost: 0 397: f856 -> [230] : A'=C+A, C'=-B+C, [ 4+C>=0 ], cost: 1 398: f856 -> [230] : [], cost: 0 399: f862 -> [231] : A'=C+A, C'=-B+C, [ 5+C>=0 ], cost: 1 400: f862 -> [231] : [], cost: 0 401: f868 -> [232] : A'=C+A, C'=-B+C, [ 4+C>=0 ], cost: 1 402: f868 -> [232] : [], cost: 0 403: f874 -> [233] : A'=C+A, C'=-B+C, [ 5+C>=0 ], cost: 1 404: f874 -> [233] : [], cost: 0 405: f882 -> [234] : A'=C+A, C'=-B+C, [ 6+C>=0 ], cost: 1 406: f882 -> [234] : [], cost: 0 407: f888 -> [235] : A'=C+A, C'=-B+C, [ 7+C>=0 ], cost: 1 408: f888 -> [235] : [], cost: 0 409: f894 -> [236] : A'=C+A, C'=-B+C, [ 6+C>=0 ], cost: 1 410: f894 -> [236] : [], cost: 0 411: f900 -> [237] : A'=C+A, C'=-B+C, [ 7+C>=0 ], cost: 1 412: f900 -> [237] : [], cost: 0 413: f908 -> [238] : A'=C+A, C'=-B+C, [ 7+C>=0 ], cost: 1 414: f908 -> [238] : [], cost: 0 415: f914 -> [239] : A'=C+A, C'=-B+C, [ 8+C>=0 ], cost: 1 416: f914 -> [239] : [], cost: 0 417: f920 -> [240] : A'=C+A, C'=-B+C, [ 7+C>=0 ], cost: 1 418: f920 -> [240] : [], cost: 0 419: f926 -> [241] : A'=C+A, C'=-B+C, [ 8+C>=0 ], cost: 1 420: f926 -> [241] : [], cost: 0 216: [146] -> f316 : C'=0, [ C>=3 ], cost: 1 215: [147] -> f322 : C'=0, [ C>=4 ], cost: 1 214: [148] -> f328 : C'=0, [ C>=3 ], cost: 1 213: [149] -> f336 : C'=1, [ C>=4 ], cost: 1 212: [150] -> f342 : C'=1, [ C>=2 ], cost: 1 211: [151] -> f348 : C'=1, [ C>=3 ], cost: 1 210: [152] -> f354 : C'=1, [ C>=2 ], cost: 1 209: [153] -> f362 : C'=-3, [ C>=3 ], cost: 1 208: [154] -> f368 : C'=-3, [ 2+C>=0 ], cost: 1 207: [155] -> f374 : C'=-3, [ 1+C>=0 ], cost: 1 206: [156] -> f380 : C'=-3, [ 2+C>=0 ], cost: 1 205: [157] -> f388 : C'=-4, [ 1+C>=0 ], cost: 1 204: [158] -> f394 : C'=-4, [ 1+C>=0 ], cost: 1 203: [159] -> f400 : C'=-4, [ C>=0 ], cost: 1 202: [160] -> f406 : C'=-4, [ 1+C>=0 ], cost: 1 201: [161] -> f414 : C'=-5, [ C>=0 ], cost: 1 200: [162] -> f420 : C'=-5, [ C>=0 ], cost: 1 199: [163] -> f426 : C'=-5, [ C>=1 ], cost: 1 198: [164] -> f432 : C'=-5, [ C>=0 ], cost: 1 197: [165] -> f440 : C'=-6, [ C>=1 ], cost: 1 196: [166] -> f446 : C'=-6, [ C>=4 ], cost: 1 195: [167] -> f452 : C'=-6, [ C>=5 ], cost: 1 194: [168] -> f458 : C'=-6, [ C>=4 ], cost: 1 193: [169] -> f700 : A'=548+A, C'=5, [ C>=5 && 5>=3 && 2>=2 && 5>=2 && 1>=1 && 5>=3 && 2>=2 && 5>=2 && 1>=1 && 6>=2 && 1>=1 && 6>=1 && 0>=0 && 6>=2 && 1>=1 && 6>=1 && 0>=0 && 7>=1 && 0>=0 && 7>=0 && 0>=0 && 7>=1 && 0>=0 && 7>=0 && 0>=0 && 8>=0 && 0>=0 && 9>=0 && 0>=0 && 8>=0 && 0>=0 && 9>=0 && 0>=0 && 10>=0 && 0>=0 && 11>=0 && 0>=0 && 10>=0 && 0>=0 && 11>=0 && 0>=0 && 2>=0 && 0>=0 && 3>=0 && 0>=0 && 2>=0 && 0>=0 && 3>=0 && 0>=0 && 3>=0 && 0>=0 && 4>=0 && 0>=0 && 3>=0 && 0>=0 && 4>=0 && 0>=0 && 4>=0 && 0>=0 && 5>=0 && 0>=0 && 4>=0 && 0>=0 && 5>=0 && 0>=0 && 23>=0 && 0>=0 && 24>=0 && 0>=0 && 23>=0 && 0>=0 && 24>=0 && 0>=0 ], cost: 339 156: [206] -> f706 : C'=5, [ 2>=C ], cost: 1 155: [207] -> f712 : C'=5, [ 1>=C ], cost: 1 154: [208] -> f718 : C'=5, [ 2>=C ], cost: 1 153: [209] -> f726 : C'=6, [ 1>=C ], cost: 1 152: [210] -> f732 : C'=6, [ 1>=C ], cost: 1 151: [211] -> f738 : C'=6, [ 0>=C ], cost: 1 150: [212] -> f744 : C'=6, [ 1>=C ], cost: 1 149: [213] -> f752 : C'=7, [ 0>=C ], cost: 1 148: [214] -> f758 : C'=7, [ 0>=C ], cost: 1 147: [215] -> f764 : C'=7, [ 0>=1+C ], cost: 1 146: [216] -> f770 : C'=7, [ 0>=C ], cost: 1 145: [217] -> f778 : C'=8, [ 0>=1+C ], cost: 1 144: [218] -> f784 : C'=8, [ 0>=1+C ], cost: 1 143: [219] -> f790 : C'=8, [ 0>=2+C ], cost: 1 142: [220] -> f796 : C'=8, [ 0>=1+C ], cost: 1 141: [221] -> f804 : C'=9, [ 0>=2+C ], cost: 1 140: [222] -> f810 : C'=9, [ 0>=2+C ], cost: 1 139: [223] -> f816 : C'=9, [ 0>=3+C ], cost: 1 138: [224] -> f822 : C'=9, [ 0>=2+C ], cost: 1 137: [225] -> f830 : C'=0, [ 0>=3+C ], cost: 1 136: [226] -> f836 : C'=0, [ 0>=3+C ], cost: 1 135: [227] -> f842 : C'=0, [ 0>=4+C ], cost: 1 134: [228] -> f848 : C'=0, [ 0>=3+C ], cost: 1 133: [229] -> f856 : C'=-1, [ 0>=4+C ], cost: 1 132: [230] -> f862 : C'=-1, [ 0>=5+C ], cost: 1 131: [231] -> f868 : C'=-1, [ 0>=6+C ], cost: 1 130: [232] -> f874 : C'=-1, [ 0>=5+C ], cost: 1 129: [233] -> f882 : C'=-2, [ 0>=6+C ], cost: 1 128: [234] -> f888 : C'=-2, [ 0>=7+C ], cost: 1 127: [235] -> f894 : C'=-2, [ 0>=8+C ], cost: 1 126: [236] -> f900 : C'=-2, [ 0>=7+C ], cost: 1 125: [237] -> f908 : C'=16, [ 0>=8+C ], cost: 1 124: [238] -> f914 : C'=16, [ 0>=8+C ], cost: 1 123: [239] -> f920 : C'=16, [ 0>=9+C ], cost: 1 122: [240] -> f926 : C'=16, [ 0>=8+C ], cost: 1 Applied chaining over branches and pruning: Start location: f0 Final control flow graph problem, now checking costs for infinitely many models: Start location: f0 Computing complexity for remaining 0 transitions. The final runtime is determined by this resulting transition: Final Guard: Final Cost: 1 Obtained the following complexity w.r.t. the length of the input n: Complexity class: const Complexity value: 0 WORST_CASE(Omega(1),?)