by AProVE
f1_0_main_Load | 1 | f252_0_main_InvokeMethod: | x1 = _arg1 ∧ x2 = _arg2 ∧ x3 = _arg3 ∧ x4 = _arg4 ∧ x5 = _arg5 ∧ x6 = _arg6 ∧ x7 = _arg7 ∧ x8 = _arg8 ∧ x9 = _arg9 ∧ x1 = _arg1P ∧ x2 = _arg2P ∧ x3 = _arg3P ∧ x4 = _arg4P ∧ x5 = _arg5P ∧ x6 = _arg6P ∧ x7 = _arg7P ∧ x8 = _arg8P ∧ x9 = _arg9P ∧ 0 = _arg2P ∧ 0 ≤ _arg1P − 1 ∧ 0 ≤ _arg1 − 1 ∧ _arg1P ≤ _arg1 | |
f1_0_main_Load | 2 | f252_0_main_InvokeMethod: | x1 = _x ∧ x2 = _x1 ∧ x3 = _x2 ∧ x4 = _x3 ∧ x5 = _x4 ∧ x6 = _x5 ∧ x7 = _x6 ∧ x8 = _x7 ∧ x9 = _x8 ∧ x1 = _x9 ∧ x2 = _x10 ∧ x3 = _x11 ∧ x4 = _x12 ∧ x5 = _x13 ∧ x6 = _x14 ∧ x7 = _x15 ∧ x8 = _x16 ∧ x9 = _x17 ∧ 0 ≤ _x9 − 1 ∧ 0 ≤ _x − 1 ∧ _x9 ≤ _x | |
f61_0_createTree_Return | 3 | f252_0_main_InvokeMethod: | x1 = _x18 ∧ x2 = _x19 ∧ x3 = _x20 ∧ x4 = _x21 ∧ x5 = _x22 ∧ x6 = _x23 ∧ x7 = _x24 ∧ x8 = _x25 ∧ x9 = _x26 ∧ x1 = _x27 ∧ x2 = _x28 ∧ x3 = _x29 ∧ x4 = _x30 ∧ x5 = _x31 ∧ x6 = _x32 ∧ x7 = _x33 ∧ x8 = _x34 ∧ x9 = _x35 ∧ 0 = _x28 ∧ 0 ≤ _x27 − 1 | |
f252_0_main_InvokeMethod | 4 | f355_0_createTree_Return: | x1 = _x36 ∧ x2 = _x37 ∧ x3 = _x38 ∧ x4 = _x39 ∧ x5 = _x40 ∧ x6 = _x41 ∧ x7 = _x42 ∧ x8 = _x43 ∧ x9 = _x44 ∧ x1 = _x45 ∧ x2 = _x46 ∧ x3 = _x47 ∧ x4 = _x48 ∧ x5 = _x49 ∧ x6 = _x50 ∧ x7 = _x51 ∧ x8 = _x52 ∧ x9 = _x53 ∧ 0 ≤ _x45 − 1 ∧ 0 ≤ _x36 − 1 ∧ _x45 ≤ _x36 | |
f355_0_createTree_Return | 5 | f845_0_alternate_NONNULL: | x1 = _x54 ∧ x2 = _x55 ∧ x3 = _x56 ∧ x4 = _x57 ∧ x5 = _x58 ∧ x6 = _x59 ∧ x7 = _x60 ∧ x8 = _x61 ∧ x9 = _x62 ∧ x1 = _x63 ∧ x2 = _x64 ∧ x3 = _x65 ∧ x4 = _x66 ∧ x5 = _x67 ∧ x6 = _x68 ∧ x7 = _x69 ∧ x8 = _x70 ∧ x9 = _x71 ∧ −1 ≤ _x66 − 1 ∧ −1 ≤ _x65 − 1 ∧ −1 ≤ _x64 − 1 ∧ −1 ≤ _x63 − 1 ∧ 0 ≤ _x54 − 1 ∧ _x66 + 1 ≤ _x54 ∧ _x65 + 1 ≤ _x54 ∧ _x64 + 1 ≤ _x54 ∧ _x63 + 1 ≤ _x54 | |
f1_0_main_Load | 6 | f2521_0_main_InvokeMethod: | x1 = _x72 ∧ x2 = _x73 ∧ x3 = _x74 ∧ x4 = _x75 ∧ x5 = _x76 ∧ x6 = _x77 ∧ x7 = _x78 ∧ x8 = _x80 ∧ x9 = _x81 ∧ x1 = _x83 ∧ x2 = _x84 ∧ x3 = _x85 ∧ x4 = _x86 ∧ x5 = _x87 ∧ x6 = _x89 ∧ x7 = _x91 ∧ x8 = _x92 ∧ x9 = _x93 ∧ 0 ≤ _x84 − 1 ∧ 0 ≤ _x83 − 1 ∧ 0 ≤ _x72 − 1 ∧ _x83 ≤ _x72 | |
f701_0_createTree_Return | 7 | f2521_0_main_InvokeMethod: | x1 = _x94 ∧ x2 = _x95 ∧ x3 = _x96 ∧ x4 = _x97 ∧ x5 = _x98 ∧ x6 = _x99 ∧ x7 = _x100 ∧ x8 = _x101 ∧ x9 = _x102 ∧ x1 = _x103 ∧ x2 = _x104 ∧ x3 = _x105 ∧ x4 = _x106 ∧ x5 = _x107 ∧ x6 = _x108 ∧ x7 = _x109 ∧ x8 = _x110 ∧ x9 = _x111 ∧ _x97 = _x106 ∧ _x96 = _x105 ∧ _x97 + 2 ≤ _x95 ∧ 1 ≤ _x104 − 1 ∧ 0 ≤ _x103 − 1 ∧ 1 ≤ _x95 − 1 ∧ 0 ≤ _x94 − 1 ∧ _x104 ≤ _x95 ∧ _x103 + 1 ≤ _x95 ∧ _x103 ≤ _x94 | |
f252_0_main_InvokeMethod | 8 | f2530_0_main_InvokeMethod: | x1 = _x112 ∧ x2 = _x113 ∧ x3 = _x114 ∧ x4 = _x115 ∧ x5 = _x116 ∧ x6 = _x117 ∧ x7 = _x118 ∧ x8 = _x119 ∧ x9 = _x120 ∧ x1 = _x121 ∧ x2 = _x122 ∧ x3 = _x123 ∧ x4 = _x124 ∧ x5 = _x125 ∧ x6 = _x126 ∧ x7 = _x127 ∧ x8 = _x128 ∧ x9 = _x129 ∧ 0 ≤ _x122 − 1 ∧ 0 ≤ _x121 − 1 ∧ 0 ≤ _x112 − 1 ∧ _x121 ≤ _x112 | |
f702_0_createTree_Return | 9 | f2530_0_main_InvokeMethod: | x1 = _x130 ∧ x2 = _x131 ∧ x3 = _x132 ∧ x4 = _x133 ∧ x5 = _x134 ∧ x6 = _x135 ∧ x7 = _x136 ∧ x8 = _x137 ∧ x9 = _x138 ∧ x1 = _x139 ∧ x2 = _x140 ∧ x3 = _x141 ∧ x4 = _x142 ∧ x5 = _x143 ∧ x6 = _x144 ∧ x7 = _x145 ∧ x8 = _x146 ∧ x9 = _x147 ∧ _x132 = _x141 ∧ _x132 + 2 ≤ _x131 ∧ 1 ≤ _x140 − 1 ∧ 0 ≤ _x139 − 1 ∧ 1 ≤ _x131 − 1 ∧ 0 ≤ _x130 − 1 ∧ _x140 ≤ _x131 ∧ _x139 + 1 ≤ _x131 ∧ _x139 ≤ _x130 | |
f2530_0_main_InvokeMethod | 10 | f845_0_alternate_NONNULL: | x1 = _x148 ∧ x2 = _x149 ∧ x3 = _x150 ∧ x4 = _x151 ∧ x5 = _x152 ∧ x6 = _x153 ∧ x7 = _x154 ∧ x8 = _x155 ∧ x9 = _x156 ∧ x1 = _x157 ∧ x2 = _x158 ∧ x3 = _x159 ∧ x4 = _x160 ∧ x5 = _x161 ∧ x6 = _x162 ∧ x7 = _x163 ∧ x8 = _x164 ∧ x9 = _x165 ∧ _x150 + 2 ≤ _x149 ∧ −1 ≤ _x160 − 1 ∧ 0 ≤ _x159 − 1 ∧ −1 ≤ _x158 − 1 ∧ −1 ≤ _x157 − 1 ∧ 0 ≤ _x149 − 1 ∧ 0 ≤ _x148 − 1 ∧ _x160 + 1 ≤ _x149 ∧ _x160 + 1 ≤ _x148 ∧ _x159 ≤ _x149 ∧ _x158 + 1 ≤ _x149 ∧ _x158 + 1 ≤ _x148 ∧ _x157 + 1 ≤ _x149 ∧ _x157 + 1 ≤ _x148 | |
f2521_0_main_InvokeMethod | 11 | f2589_0_main_InvokeMethod: | x1 = _x166 ∧ x2 = _x167 ∧ x3 = _x168 ∧ x4 = _x169 ∧ x5 = _x170 ∧ x6 = _x171 ∧ x7 = _x172 ∧ x8 = _x173 ∧ x9 = _x174 ∧ x1 = _x175 ∧ x2 = _x176 ∧ x3 = _x177 ∧ x4 = _x178 ∧ x5 = _x179 ∧ x6 = _x180 ∧ x7 = _x181 ∧ x8 = _x182 ∧ x9 = _x183 ∧ _x169 = _x177 ∧ _x169 + 2 ≤ _x167 ∧ _x178 + 2 ≤ _x167 ∧ 0 ≤ _x176 − 1 ∧ 0 ≤ _x175 − 1 ∧ 0 ≤ _x167 − 1 ∧ 0 ≤ _x166 − 1 ∧ _x176 ≤ _x167 ∧ _x175 ≤ _x167 ∧ _x175 ≤ _x166 | |
f2589_0_main_InvokeMethod | 12 | f845_0_alternate_NONNULL: | x1 = _x184 ∧ x2 = _x185 ∧ x3 = _x186 ∧ x4 = _x187 ∧ x5 = _x188 ∧ x6 = _x189 ∧ x7 = _x190 ∧ x8 = _x191 ∧ x9 = _x192 ∧ x1 = _x193 ∧ x2 = _x194 ∧ x3 = _x195 ∧ x4 = _x196 ∧ x5 = _x197 ∧ x6 = _x198 ∧ x7 = _x199 ∧ x8 = _x200 ∧ x9 = _x201 ∧ _x186 + 2 ≤ _x185 ∧ _x187 + 2 ≤ _x185 ∧ 0 ≤ _x196 − 1 ∧ −1 ≤ _x195 − 1 ∧ 0 ≤ _x194 − 1 ∧ 0 ≤ _x193 − 1 ∧ 0 ≤ _x185 − 1 ∧ 0 ≤ _x184 − 1 ∧ _x196 ≤ _x185 ∧ _x195 + 1 ≤ _x185 ∧ _x195 + 1 ≤ _x184 ∧ _x194 ≤ _x185 ∧ _x193 ≤ _x185 | |
f2521_0_main_InvokeMethod | 13 | f845_0_alternate_NONNULL: | x1 = _x202 ∧ x2 = _x203 ∧ x3 = _x204 ∧ x4 = _x205 ∧ x5 = _x206 ∧ x6 = _x207 ∧ x7 = _x208 ∧ x8 = _x209 ∧ x9 = _x210 ∧ x1 = _x211 ∧ x2 = _x212 ∧ x3 = _x213 ∧ x4 = _x214 ∧ x5 = _x215 ∧ x6 = _x216 ∧ x7 = _x217 ∧ x8 = _x218 ∧ x9 = _x219 ∧ _x205 + 2 ≤ _x203 ∧ 0 ≤ _x214 − 1 ∧ 0 ≤ _x213 − 1 ∧ 0 ≤ _x212 − 1 ∧ 0 ≤ _x211 − 1 ∧ 0 ≤ _x203 − 1 ∧ 0 ≤ _x202 − 1 ∧ _x214 ≤ _x203 ∧ _x212 ≤ _x203 ∧ _x211 ≤ _x203 | |
f1_0_main_Load | 14 | f741_0_random_GT: | x1 = _x220 ∧ x2 = _x221 ∧ x3 = _x222 ∧ x4 = _x223 ∧ x5 = _x224 ∧ x6 = _x225 ∧ x7 = _x226 ∧ x8 = _x227 ∧ x9 = _x228 ∧ x1 = _x229 ∧ x2 = _x230 ∧ x3 = _x231 ∧ x4 = _x232 ∧ x5 = _x233 ∧ x6 = _x234 ∧ x7 = _x235 ∧ x8 = _x236 ∧ x9 = _x237 ∧ −1 ≤ _x221 − 1 ∧ 0 ≤ _x220 − 1 | |
f252_0_main_InvokeMethod | 15 | f741_0_random_GT: | x1 = _x238 ∧ x2 = _x239 ∧ x3 = _x240 ∧ x4 = _x241 ∧ x5 = _x242 ∧ x6 = _x243 ∧ x7 = _x244 ∧ x8 = _x245 ∧ x9 = _x246 ∧ x1 = _x247 ∧ x2 = _x248 ∧ x3 = _x249 ∧ x4 = _x250 ∧ x5 = _x251 ∧ x6 = _x252 ∧ x7 = _x253 ∧ x8 = _x254 ∧ x9 = _x255 ∧ 0 ≤ _x238 − 1 ∧ −1 ≤ _x256 − 1 | |
f2521_0_main_InvokeMethod | 16 | f741_0_random_GT: | x1 = _x257 ∧ x2 = _x258 ∧ x3 = _x259 ∧ x4 = _x260 ∧ x5 = _x261 ∧ x6 = _x262 ∧ x7 = _x263 ∧ x8 = _x264 ∧ x9 = _x265 ∧ x1 = _x266 ∧ x2 = _x267 ∧ x3 = _x268 ∧ x4 = _x269 ∧ x5 = _x270 ∧ x6 = _x271 ∧ x7 = _x272 ∧ x8 = _x273 ∧ x9 = _x274 ∧ 0 ≤ _x257 − 1 ∧ −1 ≤ _x275 − 1 ∧ 0 ≤ _x258 − 1 ∧ _x260 + 2 ≤ _x258 | |
f741_0_random_GT | 17 | f875_0_createTree_NE: | x1 = _x276 ∧ x2 = _x277 ∧ x3 = _x278 ∧ x4 = _x279 ∧ x5 = _x280 ∧ x6 = _x281 ∧ x7 = _x282 ∧ x8 = _x283 ∧ x9 = _x284 ∧ x1 = _x285 ∧ x2 = _x286 ∧ x3 = _x287 ∧ x4 = _x288 ∧ x5 = _x289 ∧ x6 = _x290 ∧ x7 = _x291 ∧ x8 = _x292 ∧ x9 = _x293 ∧ −1 ≤ _x294 − 1 ∧ _x294 ≤ _x286 − 1 ∧ 0 = _x285 ∧ _x294 + 1 = _x287 | |
f741_0_random_GT | 18 | f875_0_createTree_NE: | x1 = _x295 ∧ x2 = _x296 ∧ x3 = _x297 ∧ x4 = _x298 ∧ x5 = _x299 ∧ x6 = _x300 ∧ x7 = _x301 ∧ x8 = _x302 ∧ x9 = _x303 ∧ x1 = _x304 ∧ x2 = _x305 ∧ x3 = _x306 ∧ x4 = _x307 ∧ x5 = _x308 ∧ x6 = _x309 ∧ x7 = _x310 ∧ x8 = _x311 ∧ x9 = _x312 ∧ _x313 ≤ _x305 − 1 ∧ −1 ≤ _x304 − 1 ∧ −1 ≤ _x313 − 1 ∧ _x313 + 1 = _x306 | |
f1172_0_createNode_Return | 19 | f2504_0_createTree_LE: | x1 = _x314 ∧ x2 = _x315 ∧ x3 = _x316 ∧ x4 = _x317 ∧ x5 = _x318 ∧ x6 = _x319 ∧ x7 = _x320 ∧ x8 = _x321 ∧ x9 = _x322 ∧ x1 = _x323 ∧ x2 = _x324 ∧ x3 = _x325 ∧ x4 = _x326 ∧ x5 = _x327 ∧ x6 = _x328 ∧ x7 = _x329 ∧ x8 = _x330 ∧ x9 = _x331 ∧ _x316 = _x327 ∧ _x315 = _x326 ∧ _x314 = _x325 ∧ 1 ≤ _x323 − 1 ∧ 1 ≤ _x324 − 1 | |
f875_0_createTree_NE | 20 | f2504_0_createTree_LE: | x1 = _x332 ∧ x2 = _x333 ∧ x3 = _x334 ∧ x4 = _x335 ∧ x5 = _x336 ∧ x6 = _x337 ∧ x7 = _x338 ∧ x8 = _x339 ∧ x9 = _x340 ∧ x1 = _x341 ∧ x2 = _x342 ∧ x3 = _x343 ∧ x4 = _x344 ∧ x5 = _x345 ∧ x6 = _x346 ∧ x7 = _x347 ∧ x8 = _x348 ∧ x9 = _x349 ∧ _x334 = _x345 ∧ _x333 = _x344 ∧ _x332 = _x343 ∧ 1 ≤ _x341 − 1 ∧ 1 ≤ _x342 − 1 ∧ 0 ≤ _x334 − 1 ∧ 0 ≤ _x332 − 1 | |
f875_0_createTree_NE | 21 | f2504_0_createTree_LE: | x1 = _x350 ∧ x2 = _x351 ∧ x3 = _x352 ∧ x4 = _x353 ∧ x5 = _x354 ∧ x6 = _x355 ∧ x7 = _x356 ∧ x8 = _x357 ∧ x9 = _x358 ∧ x1 = _x359 ∧ x2 = _x360 ∧ x3 = _x361 ∧ x4 = _x362 ∧ x5 = _x363 ∧ x6 = _x364 ∧ x7 = _x365 ∧ x8 = _x366 ∧ x9 = _x367 ∧ _x351 = _x362 ∧ _x350 = _x361 ∧ 1 ≤ _x359 − 1 ∧ 1 ≤ _x360 − 1 ∧ 0 ≤ _x352 − 1 ∧ 0 ≤ _x350 − 1 | |
f2504_0_createTree_LE | 22 | f2588_0_createTree_NONNULL: | x1 = _x368 ∧ x2 = _x369 ∧ x3 = _x370 ∧ x4 = _x371 ∧ x5 = _x372 ∧ x6 = _x373 ∧ x7 = _x374 ∧ x8 = _x375 ∧ x9 = _x376 ∧ x1 = _x377 ∧ x2 = _x378 ∧ x3 = _x379 ∧ x4 = _x380 ∧ x5 = _x381 ∧ x6 = _x382 ∧ x7 = _x383 ∧ x8 = _x384 ∧ x9 = _x385 ∧ _x372 = _x382 ∧ _x371 = _x381 ∧ _x370 = _x377 ∧ _x385 + 2 ≤ _x369 ∧ _x384 + 2 ≤ _x368 ∧ _x383 + 2 ≤ _x368 ∧ −1 ≤ _x380 − 1 ∧ 0 ≤ _x379 − 1 ∧ 0 ≤ _x378 − 1 ∧ 0 ≤ _x369 − 1 ∧ 0 ≤ _x368 − 1 ∧ _x380 + 1 ≤ _x369 ∧ _x379 ≤ _x369 ∧ _x378 ≤ _x368 ∧ 0 ≤ _x370 − 1 ∧ −1 ≤ _x371 − 1 ∧ _x371 ≤ _x372 | |
f2588_0_createTree_NONNULL | 23 | f2504_0_createTree_LE: | x1 = _x386 ∧ x2 = _x387 ∧ x3 = _x388 ∧ x4 = _x389 ∧ x5 = _x390 ∧ x6 = _x391 ∧ x7 = _x392 ∧ x8 = _x393 ∧ x9 = _x394 ∧ x1 = _x395 ∧ x2 = _x396 ∧ x3 = _x397 ∧ x4 = _x398 ∧ x5 = _x399 ∧ x6 = _x400 ∧ x7 = _x401 ∧ x8 = _x402 ∧ x9 = _x403 ∧ _x391 = _x399 ∧ _x390 = _x398 ∧ _x386 − 1 = _x397 ∧ _x394 + 2 ≤ _x388 ∧ _x393 + 2 ≤ _x387 ∧ _x392 + 2 ≤ _x387 ∧ 0 ≤ _x396 − 1 ∧ 0 ≤ _x395 − 1 ∧ 0 ≤ _x389 − 1 ∧ 2 ≤ _x388 − 1 ∧ 0 ≤ _x387 − 1 ∧ _x396 ≤ _x389 ∧ _x396 + 2 ≤ _x388 ∧ _x395 ≤ _x387 | |
f2588_0_createTree_NONNULL | 24 | f2671_0_createTree_FieldAccess: | x1 = _x404 ∧ x2 = _x405 ∧ x3 = _x406 ∧ x4 = _x407 ∧ x5 = _x408 ∧ x6 = _x409 ∧ x7 = _x410 ∧ x8 = _x411 ∧ x9 = _x412 ∧ x1 = _x413 ∧ x2 = _x414 ∧ x3 = _x415 ∧ x4 = _x416 ∧ x5 = _x417 ∧ x6 = _x418 ∧ x7 = _x419 ∧ x8 = _x420 ∧ x9 = _x421 ∧ _x412 = _x419 ∧ _x411 = _x418 ∧ _x409 = _x417 ∧ _x408 = _x416 ∧ _x404 = _x413 ∧ _x412 + 2 ≤ _x406 ∧ _x411 + 2 ≤ _x405 ∧ _x410 + 2 ≤ _x405 ∧ 1 ≤ _x415 − 1 ∧ 0 ≤ _x414 − 1 ∧ −1 ≤ _x407 − 1 ∧ 1 ≤ _x406 − 1 ∧ 0 ≤ _x405 − 1 ∧ _x415 ≤ _x406 ∧ _x414 ≤ _x405 ∧ 0 ≤ _x404 − 1 ∧ _x408 ≤ _x409 | |
f2588_0_createTree_NONNULL | 25 | f2671_0_createTree_FieldAccess: | x1 = _x422 ∧ x2 = _x423 ∧ x3 = _x424 ∧ x4 = _x425 ∧ x5 = _x426 ∧ x6 = _x427 ∧ x7 = _x428 ∧ x8 = _x429 ∧ x9 = _x430 ∧ x1 = _x431 ∧ x2 = _x432 ∧ x3 = _x433 ∧ x4 = _x434 ∧ x5 = _x435 ∧ x6 = _x436 ∧ x7 = _x437 ∧ x8 = _x438 ∧ x9 = _x439 ∧ _x430 = _x437 ∧ _x429 = _x436 ∧ _x426 = _x434 ∧ _x422 = _x431 ∧ _x430 + 2 ≤ _x424 ∧ _x429 + 2 ≤ _x423 ∧ _x428 + 2 ≤ _x423 ∧ 1 ≤ _x433 − 1 ∧ 0 ≤ _x432 − 1 ∧ −1 ≤ _x425 − 1 ∧ 1 ≤ _x424 − 1 ∧ 0 ≤ _x423 − 1 ∧ _x433 ≤ _x424 ∧ _x432 ≤ _x423 ∧ 0 ≤ _x422 − 1 ∧ _x426 ≤ _x427 | |
f2504_0_createTree_LE | 26 | f2712_0_createTree_LE: | x1 = _x440 ∧ x2 = _x441 ∧ x3 = _x442 ∧ x4 = _x443 ∧ x5 = _x444 ∧ x6 = _x445 ∧ x7 = _x446 ∧ x8 = _x447 ∧ x9 = _x448 ∧ x1 = _x449 ∧ x2 = _x450 ∧ x3 = _x451 ∧ x4 = _x452 ∧ x5 = _x453 ∧ x6 = _x454 ∧ x7 = _x455 ∧ x8 = _x456 ∧ x9 = _x457 ∧ _x444 + 1 = _x454 ∧ _x443 = _x453 ∧ 0 = _x452 ∧ _x442 = _x449 ∧ _x456 + 2 ≤ _x440 ∧ _x455 + 2 ≤ _x440 ∧ 0 ≤ _x451 − 1 ∧ 0 ≤ _x450 − 1 ∧ 0 ≤ _x441 − 1 ∧ 0 ≤ _x440 − 1 ∧ _x451 ≤ _x441 ∧ _x450 ≤ _x440 ∧ −1 ≤ _x444 − 1 ∧ _x444 ≤ _x443 − 1 ∧ −1 ≤ _x443 − 1 ∧ 0 ≤ _x442 − 1 | |
f2504_0_createTree_LE | 27 | f2712_0_createTree_LE: | x1 = _x458 ∧ x2 = _x459 ∧ x3 = _x460 ∧ x4 = _x461 ∧ x5 = _x462 ∧ x6 = _x463 ∧ x7 = _x464 ∧ x8 = _x465 ∧ x9 = _x466 ∧ x1 = _x467 ∧ x2 = _x468 ∧ x3 = _x469 ∧ x4 = _x470 ∧ x5 = _x471 ∧ x6 = _x472 ∧ x7 = _x473 ∧ x8 = _x474 ∧ x9 = _x475 ∧ _x462 + 1 = _x472 ∧ _x461 = _x471 ∧ _x460 = _x467 ∧ _x474 + 2 ≤ _x458 ∧ _x473 + 2 ≤ _x458 ∧ 0 ≤ _x469 − 1 ∧ 0 ≤ _x468 − 1 ∧ 0 ≤ _x459 − 1 ∧ 0 ≤ _x458 − 1 ∧ _x469 ≤ _x459 ∧ _x468 ≤ _x458 ∧ −1 ≤ _x470 − 1 ∧ −1 ≤ _x462 − 1 ∧ _x462 ≤ _x461 − 1 ∧ −1 ≤ _x461 − 1 ∧ 0 ≤ _x460 − 1 | |
f2671_0_createTree_FieldAccess | 28 | f2504_0_createTree_LE: | x1 = _x476 ∧ x2 = _x477 ∧ x3 = _x478 ∧ x4 = _x479 ∧ x5 = _x480 ∧ x6 = _x481 ∧ x7 = _x482 ∧ x8 = _x483 ∧ x9 = _x484 ∧ x1 = _x485 ∧ x2 = _x486 ∧ x3 = _x487 ∧ x4 = _x488 ∧ x5 = _x489 ∧ x6 = _x490 ∧ x7 = _x491 ∧ x8 = _x492 ∧ x9 = _x493 ∧ _x480 = _x489 ∧ _x479 = _x488 ∧ _x476 − 1 = _x487 ∧ _x482 + 2 ≤ _x478 ∧ _x481 + 2 ≤ _x477 ∧ 0 ≤ _x486 − 1 ∧ 0 ≤ _x485 − 1 ∧ 1 ≤ _x478 − 1 ∧ 0 ≤ _x477 − 1 | |
f2671_0_createTree_FieldAccess | 29 | f2504_0_createTree_LE: | x1 = _x494 ∧ x2 = _x495 ∧ x3 = _x496 ∧ x4 = _x497 ∧ x5 = _x498 ∧ x6 = _x499 ∧ x7 = _x500 ∧ x8 = _x501 ∧ x9 = _x502 ∧ x1 = _x503 ∧ x2 = _x504 ∧ x3 = _x505 ∧ x4 = _x506 ∧ x5 = _x507 ∧ x6 = _x508 ∧ x7 = _x509 ∧ x8 = _x510 ∧ x9 = _x511 ∧ _x498 = _x507 ∧ _x497 = _x506 ∧ _x494 − 1 = _x505 ∧ _x499 = _x500 ∧ _x499 + 2 ≤ _x496 ∧ _x499 + 2 ≤ _x495 ∧ 3 ≤ _x504 − 1 ∧ 3 ≤ _x503 − 1 ∧ 1 ≤ _x496 − 1 ∧ 1 ≤ _x495 − 1 ∧ _x504 − 2 ≤ _x496 ∧ _x504 − 2 ≤ _x495 ∧ _x503 − 2 ≤ _x496 ∧ _x503 − 2 ≤ _x495 | |
f2712_0_createTree_LE | 30 | f2588_0_createTree_NONNULL: | x1 = _x512 ∧ x2 = _x513 ∧ x3 = _x514 ∧ x4 = _x515 ∧ x5 = _x516 ∧ x6 = _x517 ∧ x7 = _x518 ∧ x8 = _x519 ∧ x9 = _x520 ∧ x1 = _x521 ∧ x2 = _x522 ∧ x3 = _x523 ∧ x4 = _x524 ∧ x5 = _x525 ∧ x6 = _x526 ∧ x7 = _x527 ∧ x8 = _x528 ∧ x9 = _x529 ∧ _x519 = _x528 ∧ _x518 = _x527 ∧ _x517 = _x526 ∧ _x516 = _x525 ∧ _x512 = _x521 ∧ 0 = _x515 ∧ _x529 + 2 ≤ _x514 ∧ _x519 + 2 ≤ _x513 ∧ _x518 + 2 ≤ _x513 ∧ −1 ≤ _x524 − 1 ∧ 0 ≤ _x523 − 1 ∧ 0 ≤ _x522 − 1 ∧ 0 ≤ _x514 − 1 ∧ 0 ≤ _x513 − 1 ∧ _x524 + 1 ≤ _x514 ∧ _x523 ≤ _x514 ∧ _x522 ≤ _x513 | |
f2712_0_createTree_LE | 31 | f2504_0_createTree_LE: | x1 = _x530 ∧ x2 = _x531 ∧ x3 = _x532 ∧ x4 = _x533 ∧ x5 = _x534 ∧ x6 = _x535 ∧ x7 = _x536 ∧ x8 = _x537 ∧ x9 = _x538 ∧ x1 = _x539 ∧ x2 = _x540 ∧ x3 = _x541 ∧ x4 = _x542 ∧ x5 = _x543 ∧ x6 = _x544 ∧ x7 = _x545 ∧ x8 = _x546 ∧ x9 = _x547 ∧ _x535 = _x543 ∧ _x534 = _x542 ∧ _x530 − 1 = _x541 ∧ _x537 + 2 ≤ _x531 ∧ _x536 + 2 ≤ _x531 ∧ 0 ≤ _x540 − 1 ∧ 0 ≤ _x539 − 1 ∧ 2 ≤ _x532 − 1 ∧ 0 ≤ _x531 − 1 ∧ _x540 + 2 ≤ _x532 ∧ 0 ≤ _x533 − 1 ∧ _x539 ≤ _x531 | |
f2712_0_createTree_LE | 32 | f2777_0_createTree_FieldAccess: | x1 = _x548 ∧ x2 = _x549 ∧ x3 = _x550 ∧ x4 = _x551 ∧ x5 = _x552 ∧ x6 = _x553 ∧ x7 = _x554 ∧ x8 = _x555 ∧ x9 = _x556 ∧ x1 = _x557 ∧ x2 = _x558 ∧ x3 = _x559 ∧ x4 = _x560 ∧ x5 = _x561 ∧ x6 = _x562 ∧ x7 = _x563 ∧ x8 = _x564 ∧ x9 = _x565 ∧ _x554 = _x562 ∧ _x553 = _x561 ∧ _x552 = _x560 ∧ _x548 = _x557 ∧ _x563 + 2 ≤ _x550 ∧ _x555 + 2 ≤ _x549 ∧ _x554 + 2 ≤ _x549 ∧ 1 ≤ _x559 − 1 ∧ 0 ≤ _x558 − 1 ∧ 1 ≤ _x550 − 1 ∧ 0 ≤ _x549 − 1 ∧ _x559 ≤ _x550 ∧ _x558 ≤ _x549 ∧ 0 ≤ _x548 − 1 ∧ 0 ≤ _x553 − 1 ∧ 0 ≤ _x551 − 1 | |
f2712_0_createTree_LE | 33 | f2777_0_createTree_FieldAccess: | x1 = _x566 ∧ x2 = _x567 ∧ x3 = _x568 ∧ x4 = _x569 ∧ x5 = _x570 ∧ x6 = _x571 ∧ x7 = _x572 ∧ x8 = _x573 ∧ x9 = _x574 ∧ x1 = _x575 ∧ x2 = _x576 ∧ x3 = _x577 ∧ x4 = _x578 ∧ x5 = _x579 ∧ x6 = _x580 ∧ x7 = _x581 ∧ x8 = _x582 ∧ x9 = _x583 ∧ _x572 = _x580 ∧ _x570 = _x578 ∧ _x566 = _x575 ∧ _x581 + 2 ≤ _x568 ∧ _x573 + 2 ≤ _x567 ∧ _x572 + 2 ≤ _x567 ∧ 1 ≤ _x577 − 1 ∧ 0 ≤ _x576 − 1 ∧ 1 ≤ _x568 − 1 ∧ 0 ≤ _x567 − 1 ∧ _x577 ≤ _x568 ∧ _x576 ≤ _x567 ∧ 0 ≤ _x566 − 1 ∧ 0 ≤ _x571 − 1 ∧ 0 ≤ _x569 − 1 | |
f2777_0_createTree_FieldAccess | 34 | f2504_0_createTree_LE: | x1 = _x584 ∧ x2 = _x585 ∧ x3 = _x586 ∧ x4 = _x587 ∧ x5 = _x588 ∧ x6 = _x589 ∧ x7 = _x590 ∧ x8 = _x591 ∧ x9 = _x592 ∧ x1 = _x593 ∧ x2 = _x594 ∧ x3 = _x595 ∧ x4 = _x596 ∧ x5 = _x597 ∧ x6 = _x598 ∧ x7 = _x599 ∧ x8 = _x600 ∧ x9 = _x601 ∧ _x588 = _x597 ∧ _x587 = _x596 ∧ _x584 − 1 = _x595 ∧ _x590 + 2 ≤ _x586 ∧ _x589 + 2 ≤ _x585 ∧ 0 ≤ _x594 − 1 ∧ 0 ≤ _x593 − 1 ∧ 1 ≤ _x586 − 1 ∧ 0 ≤ _x585 − 1 | |
f2777_0_createTree_FieldAccess | 35 | f2504_0_createTree_LE: | x1 = _x602 ∧ x2 = _x603 ∧ x3 = _x604 ∧ x4 = _x605 ∧ x5 = _x606 ∧ x6 = _x607 ∧ x7 = _x608 ∧ x8 = _x609 ∧ x9 = _x610 ∧ x1 = _x611 ∧ x2 = _x612 ∧ x3 = _x613 ∧ x4 = _x614 ∧ x5 = _x615 ∧ x6 = _x616 ∧ x7 = _x617 ∧ x8 = _x618 ∧ x9 = _x619 ∧ _x606 = _x615 ∧ _x605 = _x614 ∧ _x602 − 1 = _x613 ∧ _x607 = _x608 ∧ _x607 + 2 ≤ _x604 ∧ _x607 + 2 ≤ _x603 ∧ 3 ≤ _x612 − 1 ∧ 3 ≤ _x611 − 1 ∧ 1 ≤ _x604 − 1 ∧ 1 ≤ _x603 − 1 ∧ _x612 − 2 ≤ _x604 ∧ _x612 − 2 ≤ _x603 ∧ _x611 − 2 ≤ _x604 ∧ _x611 − 2 ≤ _x603 | |
f845_0_alternate_NONNULL | 36 | f756_0_copy_NONNULL: | x1 = _x620 ∧ x2 = _x621 ∧ x3 = _x622 ∧ x4 = _x623 ∧ x5 = _x624 ∧ x6 = _x625 ∧ x7 = _x626 ∧ x8 = _x627 ∧ x9 = _x628 ∧ x1 = _x629 ∧ x2 = _x630 ∧ x3 = _x631 ∧ x4 = _x632 ∧ x5 = _x633 ∧ x6 = _x634 ∧ x7 = _x635 ∧ x8 = _x636 ∧ x9 = _x637 ∧ −1 ≤ _x629 − 1 ∧ −1 ≤ _x623 − 1 ∧ −1 ≤ _x622 − 1 ∧ −1 ≤ _x621 − 1 ∧ −1 ≤ _x620 − 1 ∧ _x629 ≤ _x622 | |
f845_0_alternate_NONNULL | 37 | f756_0_copy_NONNULL: | x1 = _x638 ∧ x2 = _x639 ∧ x3 = _x640 ∧ x4 = _x641 ∧ x5 = _x642 ∧ x6 = _x643 ∧ x7 = _x644 ∧ x8 = _x645 ∧ x9 = _x646 ∧ x1 = _x647 ∧ x2 = _x648 ∧ x3 = _x649 ∧ x4 = _x650 ∧ x5 = _x651 ∧ x6 = _x652 ∧ x7 = _x653 ∧ x8 = _x654 ∧ x9 = _x655 ∧ −1 ≤ _x647 − 1 ∧ 0 ≤ _x641 − 1 ∧ −1 ≤ _x640 − 1 ∧ 0 ≤ _x639 − 1 ∧ 0 ≤ _x638 − 1 ∧ _x647 + 1 ≤ _x641 ∧ _x647 + 1 ≤ _x639 ∧ _x647 + 1 ≤ _x638 | |
f845_0_alternate_NONNULL | 38 | f845_0_alternate_NONNULL: | x1 = _x656 ∧ x2 = _x657 ∧ x3 = _x658 ∧ x4 = _x659 ∧ x5 = _x660 ∧ x6 = _x661 ∧ x7 = _x662 ∧ x8 = _x663 ∧ x9 = _x664 ∧ x1 = _x665 ∧ x2 = _x666 ∧ x3 = _x667 ∧ x4 = _x668 ∧ x5 = _x669 ∧ x6 = _x670 ∧ x7 = _x671 ∧ x8 = _x672 ∧ x9 = _x673 ∧ −1 ≤ _x668 − 1 ∧ −1 ≤ _x667 − 1 ∧ −1 ≤ _x666 − 1 ∧ −1 ≤ _x665 − 1 ∧ 1 ≤ _x659 − 1 ∧ −1 ≤ _x658 − 1 ∧ 1 ≤ _x657 − 1 ∧ 1 ≤ _x656 − 1 ∧ _x668 ≤ _x658 ∧ _x667 + 2 ≤ _x659 ∧ _x667 + 2 ≤ _x657 ∧ _x667 + 2 ≤ _x656 ∧ _x666 ≤ _x658 ∧ _x665 ≤ _x658 | |
f845_0_alternate_NONNULL | 39 | f1242_0_alternate_InvokeMethod: | x1 = _x674 ∧ x2 = _x675 ∧ x3 = _x676 ∧ x4 = _x677 ∧ x5 = _x678 ∧ x6 = _x679 ∧ x7 = _x680 ∧ x8 = _x681 ∧ x9 = _x682 ∧ x1 = _x683 ∧ x2 = _x684 ∧ x3 = _x685 ∧ x4 = _x686 ∧ x5 = _x687 ∧ x6 = _x688 ∧ x7 = _x689 ∧ x8 = _x690 ∧ x9 = _x691 ∧ −1 ≤ _x688 − 1 ∧ −1 ≤ _x686 − 1 ∧ −1 ≤ _x685 − 1 ∧ 2 ≤ _x684 − 1 ∧ 4 ≤ _x683 − 1 ∧ 4 ≤ _x677 − 1 ∧ −1 ≤ _x676 − 1 ∧ 4 ≤ _x675 − 1 ∧ 4 ≤ _x674 − 1 ∧ _x688 + 2 ≤ _x677 ∧ _x688 + 2 ≤ _x675 ∧ _x688 + 2 ≤ _x674 ∧ _x686 + 2 ≤ _x677 ∧ _x686 + 2 ≤ _x675 ∧ _x686 + 2 ≤ _x674 ∧ _x685 ≤ _x676 ∧ _x683 ≤ _x677 ∧ _x683 ≤ _x675 ∧ _x683 ≤ _x674 | |
f845_0_alternate_NONNULL | 40 | f1242_0_alternate_InvokeMethod: | x1 = _x692 ∧ x2 = _x693 ∧ x3 = _x694 ∧ x4 = _x695 ∧ x5 = _x696 ∧ x6 = _x697 ∧ x7 = _x698 ∧ x8 = _x699 ∧ x9 = _x700 ∧ x1 = _x701 ∧ x2 = _x702 ∧ x3 = _x703 ∧ x4 = _x704 ∧ x5 = _x705 ∧ x6 = _x706 ∧ x7 = _x707 ∧ x8 = _x708 ∧ x9 = _x709 ∧ −1 ≤ _x706 − 1 ∧ −1 ≤ _x704 − 1 ∧ −1 ≤ _x703 − 1 ∧ 1 ≤ _x702 − 1 ∧ 3 ≤ _x701 − 1 ∧ 3 ≤ _x695 − 1 ∧ −1 ≤ _x694 − 1 ∧ 3 ≤ _x693 − 1 ∧ 3 ≤ _x692 − 1 ∧ _x706 + 2 ≤ _x695 ∧ _x706 + 2 ≤ _x693 ∧ _x706 + 2 ≤ _x692 ∧ _x704 + 2 ≤ _x695 ∧ _x704 + 2 ≤ _x693 ∧ _x704 + 2 ≤ _x692 ∧ _x703 ≤ _x694 ∧ _x702 + 2 ≤ _x695 ∧ _x702 − 2 ≤ _x694 ∧ _x702 + 2 ≤ _x693 ∧ _x702 + 2 ≤ _x692 ∧ _x701 ≤ _x695 ∧ _x701 ≤ _x693 ∧ _x701 ≤ _x692 | |
f1242_0_alternate_InvokeMethod | 41 | f845_0_alternate_NONNULL: | x1 = _x710 ∧ x2 = _x711 ∧ x3 = _x712 ∧ x4 = _x713 ∧ x5 = _x714 ∧ x6 = _x715 ∧ x7 = _x716 ∧ x8 = _x717 ∧ x9 = _x718 ∧ x1 = _x719 ∧ x2 = _x720 ∧ x3 = _x721 ∧ x4 = _x722 ∧ x5 = _x723 ∧ x6 = _x724 ∧ x7 = _x725 ∧ x8 = _x726 ∧ x9 = _x727 ∧ −1 ≤ _x722 − 1 ∧ −1 ≤ _x721 − 1 ∧ −1 ≤ _x720 − 1 ∧ −1 ≤ _x719 − 1 ∧ −1 ≤ _x715 − 1 ∧ −1 ≤ _x713 − 1 ∧ −1 ≤ _x712 − 1 ∧ 0 ≤ _x711 − 1 ∧ 2 ≤ _x710 − 1 ∧ _x722 ≤ _x712 ∧ _x721 ≤ _x715 ∧ _x721 ≤ _x713 ∧ _x721 + 2 ≤ _x710 ∧ _x720 ≤ _x712 ∧ _x719 ≤ _x712 | |
f756_0_copy_NONNULL | 42 | f756_0_copy_NONNULL: | x1 = _x728 ∧ x2 = _x729 ∧ x3 = _x730 ∧ x4 = _x731 ∧ x5 = _x732 ∧ x6 = _x733 ∧ x7 = _x734 ∧ x8 = _x735 ∧ x9 = _x736 ∧ x1 = _x737 ∧ x2 = _x738 ∧ x3 = _x739 ∧ x4 = _x740 ∧ x5 = _x741 ∧ x6 = _x742 ∧ x7 = _x743 ∧ x8 = _x744 ∧ x9 = _x745 ∧ −1 ≤ _x737 − 1 ∧ 0 ≤ _x728 − 1 ∧ _x737 + 1 ≤ _x728 | |
f756_0_copy_NONNULL | 43 | f756_0_copy_NONNULL: | x1 = _x746 ∧ x2 = _x747 ∧ x3 = _x748 ∧ x4 = _x749 ∧ x5 = _x750 ∧ x6 = _x751 ∧ x7 = _x752 ∧ x8 = _x753 ∧ x9 = _x754 ∧ x1 = _x755 ∧ x2 = _x756 ∧ x3 = _x757 ∧ x4 = _x758 ∧ x5 = _x759 ∧ x6 = _x760 ∧ x7 = _x761 ∧ x8 = _x762 ∧ x9 = _x763 ∧ −1 ≤ _x755 − 1 ∧ 1 ≤ _x746 − 1 ∧ _x755 + 2 ≤ _x746 | |
f756_0_copy_NONNULL | 44 | f1247_0_copy_InvokeMethod: | x1 = _x764 ∧ x2 = _x765 ∧ x3 = _x766 ∧ x4 = _x767 ∧ x5 = _x768 ∧ x6 = _x769 ∧ x7 = _x770 ∧ x8 = _x771 ∧ x9 = _x772 ∧ x1 = _x773 ∧ x2 = _x774 ∧ x3 = _x775 ∧ x4 = _x776 ∧ x5 = _x777 ∧ x6 = _x778 ∧ x7 = _x779 ∧ x8 = _x780 ∧ x9 = _x781 ∧ −1 ≤ _x775 − 1 ∧ −1 ≤ _x774 − 1 ∧ 4 ≤ _x773 − 1 ∧ 4 ≤ _x764 − 1 ∧ _x775 + 2 ≤ _x764 ∧ _x774 + 2 ≤ _x764 ∧ _x773 ≤ _x764 | |
f756_0_copy_NONNULL | 45 | f1247_0_copy_InvokeMethod: | x1 = _x782 ∧ x2 = _x783 ∧ x3 = _x784 ∧ x4 = _x785 ∧ x5 = _x786 ∧ x6 = _x787 ∧ x7 = _x788 ∧ x8 = _x789 ∧ x9 = _x790 ∧ x1 = _x791 ∧ x2 = _x792 ∧ x3 = _x793 ∧ x4 = _x794 ∧ x5 = _x795 ∧ x6 = _x796 ∧ x7 = _x797 ∧ x8 = _x798 ∧ x9 = _x799 ∧ −1 ≤ _x793 − 1 ∧ −1 ≤ _x792 − 1 ∧ 3 ≤ _x791 − 1 ∧ 3 ≤ _x782 − 1 ∧ _x793 + 2 ≤ _x782 ∧ _x792 + 2 ≤ _x782 ∧ _x791 ≤ _x782 | |
f1247_0_copy_InvokeMethod | 46 | f756_0_copy_NONNULL: | x1 = _x800 ∧ x2 = _x801 ∧ x3 = _x802 ∧ x4 = _x803 ∧ x5 = _x804 ∧ x6 = _x805 ∧ x7 = _x806 ∧ x8 = _x807 ∧ x9 = _x808 ∧ x1 = _x809 ∧ x2 = _x810 ∧ x3 = _x811 ∧ x4 = _x812 ∧ x5 = _x813 ∧ x6 = _x814 ∧ x7 = _x815 ∧ x8 = _x816 ∧ x9 = _x817 ∧ −1 ≤ _x809 − 1 ∧ −1 ≤ _x802 − 1 ∧ −1 ≤ _x801 − 1 ∧ 2 ≤ _x800 − 1 ∧ _x809 ≤ _x802 ∧ _x809 ≤ _x801 ∧ _x809 + 2 ≤ _x800 | |
f875_0_createTree_NE | 47 | f2035_0_random_GT: | x1 = _x818 ∧ x2 = _x819 ∧ x3 = _x820 ∧ x4 = _x821 ∧ x5 = _x822 ∧ x6 = _x823 ∧ x7 = _x824 ∧ x8 = _x825 ∧ x9 = _x826 ∧ x1 = _x827 ∧ x2 = _x828 ∧ x3 = _x829 ∧ x4 = _x830 ∧ x5 = _x831 ∧ x6 = _x832 ∧ x7 = _x833 ∧ x8 = _x834 ∧ x9 = _x835 ∧ _x820 = _x829 ∧ _x819 = _x828 ∧ 0 ≤ _x820 − 1 ∧ −1 ≤ _x819 − 1 ∧ 0 ≤ _x818 − 1 | |
f2588_0_createTree_NONNULL | 48 | f2035_0_random_GT: | x1 = _x836 ∧ x2 = _x837 ∧ x3 = _x838 ∧ x4 = _x839 ∧ x5 = _x840 ∧ x6 = _x841 ∧ x7 = _x842 ∧ x8 = _x843 ∧ x9 = _x844 ∧ x1 = _x845 ∧ x2 = _x846 ∧ x3 = _x847 ∧ x4 = _x848 ∧ x5 = _x849 ∧ x6 = _x850 ∧ x7 = _x851 ∧ x8 = _x852 ∧ x9 = _x853 ∧ _x841 = _x847 ∧ _x840 = _x846 ∧ _x844 + 2 ≤ _x838 ∧ _x843 + 2 ≤ _x837 ∧ _x842 + 2 ≤ _x837 ∧ −1 ≤ _x839 − 1 ∧ 1 ≤ _x838 − 1 ∧ 0 ≤ _x837 − 1 ∧ 0 ≤ _x836 − 1 ∧ _x840 ≤ _x841 ∧ −1 ≤ _x840 − 1 | |
f2712_0_createTree_LE | 49 | f2035_0_random_GT: | x1 = _x854 ∧ x2 = _x855 ∧ x3 = _x856 ∧ x4 = _x857 ∧ x5 = _x858 ∧ x6 = _x859 ∧ x7 = _x860 ∧ x8 = _x861 ∧ x9 = _x862 ∧ x1 = _x863 ∧ x2 = _x864 ∧ x3 = _x865 ∧ x4 = _x866 ∧ x5 = _x867 ∧ x6 = _x868 ∧ x7 = _x869 ∧ x8 = _x870 ∧ x9 = _x871 ∧ _x859 = _x865 ∧ _x858 = _x864 ∧ _x861 + 2 ≤ _x855 ∧ _x860 + 2 ≤ _x855 ∧ 1 ≤ _x856 − 1 ∧ 0 ≤ _x855 − 1 ∧ 0 ≤ _x857 − 1 ∧ −1 ≤ _x858 − 1 ∧ 0 ≤ _x859 − 1 ∧ 0 ≤ _x854 − 1 | |
__init | 50 | f1_0_main_Load: | x1 = _x872 ∧ x2 = _x873 ∧ x3 = _x874 ∧ x4 = _x875 ∧ x5 = _x876 ∧ x6 = _x877 ∧ x7 = _x878 ∧ x8 = _x879 ∧ x9 = _x880 ∧ x1 = _x881 ∧ x2 = _x882 ∧ x3 = _x883 ∧ x4 = _x884 ∧ x5 = _x885 ∧ x6 = _x886 ∧ x7 = _x887 ∧ x8 = _x888 ∧ x9 = _x889 ∧ 0 ≤ 0 |
f2521_0_main_InvokeMethod | f2521_0_main_InvokeMethod | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f701_0_createTree_Return | f701_0_createTree_Return | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f355_0_createTree_Return | f355_0_createTree_Return | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f845_0_alternate_NONNULL | f845_0_alternate_NONNULL | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f1242_0_alternate_InvokeMethod | f1242_0_alternate_InvokeMethod | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f2589_0_main_InvokeMethod | f2589_0_main_InvokeMethod | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f2712_0_createTree_LE | f2712_0_createTree_LE | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f702_0_createTree_Return | f702_0_createTree_Return | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f2530_0_main_InvokeMethod | f2530_0_main_InvokeMethod | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f2504_0_createTree_LE | f2504_0_createTree_LE | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f756_0_copy_NONNULL | f756_0_copy_NONNULL | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f61_0_createTree_Return | f61_0_createTree_Return | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f252_0_main_InvokeMethod | f252_0_main_InvokeMethod | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
__init | __init | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f2588_0_createTree_NONNULL | f2588_0_createTree_NONNULL | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f1172_0_createNode_Return | f1172_0_createNode_Return | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f741_0_random_GT | f741_0_random_GT | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f2671_0_createTree_FieldAccess | f2671_0_createTree_FieldAccess | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f2777_0_createTree_FieldAccess | f2777_0_createTree_FieldAccess | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f1247_0_copy_InvokeMethod | f1247_0_copy_InvokeMethod | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f875_0_createTree_NE | f875_0_createTree_NE | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
f1_0_main_Load | f1_0_main_Load | : | x1 = x1 ∧ x2 = x2 ∧ x3 = x3 ∧ x4 = x4 ∧ x5 = x5 ∧ x6 = x6 ∧ x7 = x7 ∧ x8 = x8 ∧ x9 = x9 |
We consider subproblems for each of the 3 SCC(s) of the program graph.
Here we consider the SCC {
, , , , }.We remove transitions
, , using the following ranking functions, which are bounded by 0.: | −1 + x3 + x4 |
: | −2 + x1 + x5 |
: | −2 + x1 + x5 |
: | −2 + x1 + x4 |
: | −2 + x1 + x4 |
We remove transitions
, , , , , , , , , , using the following ranking functions, which are bounded by 0.: | 2 |
: | 0 |
: | 3 |
: | 1 |
: | 1 |
There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.
Here we consider the SCC {
, }.We remove transitions
, , , using the following ranking functions, which are bounded by 0.: | x4 + x3 |
: | x4 + x3 + 1 |
There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.
Here we consider the SCC {
, }.We remove transitions
, , , , using the following ranking functions, which are bounded by 0.: | x1 |
: | −1 + x1 |
There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.