LTS Termination Proof

by AProVE

Input

• Initial Location: f3987_0_transfer_GE, f4082_0_transfer_ArrayAccess, f463_0_createMap_Return, f2980_0_createMap_LE, f3463_0_put_NULL, f1_0_main_Load, f3541_0_put_EQ, __init
• Transitions: (pre-variables and post-variables)

  f1_0_main_Load	1	f3045_0_isEmpty_NE:		x1 = _arg1 ∧ x2 = _arg2 ∧ x3 = _arg3 ∧ x4 = _arg4 ∧ x5 = _arg5 ∧ x6 = _arg6 ∧ x7 = _arg7 ∧ x8 = _arg8 ∧ x9 = _arg9 ∧ x10 = _arg10 ∧ x11 = _arg11 ∧ x12 = _arg12 ∧ x13 = _arg13 ∧ x1 = _arg1P ∧ x2 = _arg2P ∧ x3 = _arg3P ∧ x4 = _arg4P ∧ x5 = _arg5P ∧ x6 = _arg6P ∧ x7 = _arg7P ∧ x8 = _arg8P ∧ x9 = _arg9P ∧ x10 = _arg10P ∧ x11 = _arg11P ∧ x12 = _arg12P ∧ x13 = _arg13P ∧ −1 ≤ _x5 − 1 ∧ 0 ≤ _arg2 − 1 ∧ _arg1P ≤ _arg1 ∧ 0 ≤ _arg1 − 1 ∧ 0 ≤ _arg1P − 1
  f463_0_createMap_Return	2	f3045_0_isEmpty_NE:		x1 = _x ∧ x2 = _x1 ∧ x3 = _x2 ∧ x4 = _x3 ∧ x5 = _x4 ∧ x6 = _x6 ∧ x7 = _x7 ∧ x8 = _x8 ∧ x9 = _x9 ∧ x10 = _x10 ∧ x11 = _x11 ∧ x12 = _x12 ∧ x13 = _x13 ∧ x1 = _x14 ∧ x2 = _x15 ∧ x3 = _x16 ∧ x4 = _x17 ∧ x5 = _x18 ∧ x6 = _x19 ∧ x7 = _x20 ∧ x8 = _x21 ∧ x9 = _x22 ∧ x10 = _x23 ∧ x11 = _x24 ∧ x12 = _x25 ∧ x13 = _x26 ∧ _x3 = _x15 ∧ 12 = _x6 ∧ 16 = _x4 ∧ _x3 + 3 ≤ _x1 ∧ 0 ≤ _x14 − 1 ∧ 14 ≤ _x1 − 1 ∧ 0 ≤ _x − 1 ∧ _x14 + 14 ≤ _x1 ∧ _x14 ≤ _x
  f1_0_main_Load	3	f2980_0_createMap_LE:		x1 = _x29 ∧ x2 = _x30 ∧ x3 = _x31 ∧ x4 = _x32 ∧ x5 = _x33 ∧ x6 = _x34 ∧ x7 = _x35 ∧ x8 = _x36 ∧ x9 = _x37 ∧ x10 = _x38 ∧ x11 = _x39 ∧ x12 = _x42 ∧ x13 = _x43 ∧ x1 = _x44 ∧ x2 = _x45 ∧ x3 = _x46 ∧ x4 = _x47 ∧ x5 = _x48 ∧ x6 = _x49 ∧ x7 = _x50 ∧ x8 = _x51 ∧ x9 = _x52 ∧ x10 = _x53 ∧ x11 = _x54 ∧ x12 = _x55 ∧ x13 = _x56 ∧ 12 = _x50 ∧ 16 = _x49 ∧ 0 = _x48 ∧ 1 = _x47 ∧ _x30 = _x46 ∧ 14 ≤ _x44 − 1 ∧ 0 ≤ _x29 − 1 ∧ _x44 − 14 ≤ _x29 ∧ 0 ≤ _x30 − 1 ∧ −1 ≤ _x45 − 1
  f2980_0_createMap_LE	4	f2980_0_createMap_LE:		x1 = _x57 ∧ x2 = _x58 ∧ x3 = _x59 ∧ x4 = _x60 ∧ x5 = _x61 ∧ x6 = _x62 ∧ x7 = _x63 ∧ x8 = _x64 ∧ x9 = _x65 ∧ x10 = _x66 ∧ x11 = _x67 ∧ x12 = _x68 ∧ x13 = _x69 ∧ x1 = _x70 ∧ x2 = _x71 ∧ x3 = _x72 ∧ x4 = _x73 ∧ x5 = _x74 ∧ x6 = _x75 ∧ x7 = _x76 ∧ x8 = _x77 ∧ x9 = _x78 ∧ x10 = _x80 ∧ x11 = _x81 ∧ x12 = _x82 ∧ x13 = _x83 ∧ 0 ≤ _x58 − 1 ∧ _x60 + 1 ≤ _x59 − 1 ∧ −1 ≤ _x59 − 1 ∧ −1 ≤ _x60 − 1 ∧ −1 ≤ _x84 − 1 ∧ −1 ≤ _x85 − 1 ∧ 1 ≤ _x62 − 1 ∧ 3 ≤ _x57 − 1 ∧ 3 ≤ _x70 − 1 ∧ _x61 + 3 ≤ _x57 ∧ _x63 + 3 ≤ _x57 ∧ _x58 − 1 = _x71 ∧ _x59 = _x72 ∧ _x60 + 2 = _x73
  f2980_0_createMap_LE	5	f3463_0_put_NULL:		x1 = _x86 ∧ x2 = _x87 ∧ x3 = _x88 ∧ x4 = _x89 ∧ x5 = _x90 ∧ x6 = _x91 ∧ x7 = _x92 ∧ x8 = _x93 ∧ x9 = _x94 ∧ x10 = _x95 ∧ x11 = _x96 ∧ x12 = _x97 ∧ x13 = _x98 ∧ x1 = _x99 ∧ x2 = _x100 ∧ x3 = _x101 ∧ x4 = _x102 ∧ x5 = _x103 ∧ x6 = _x104 ∧ x7 = _x105 ∧ x8 = _x106 ∧ x9 = _x107 ∧ x10 = _x108 ∧ x11 = _x109 ∧ x12 = _x110 ∧ x13 = _x111 ∧ _x89 + 1 ≤ _x88 − 1 ∧ 1 ≤ _x91 − 1 ∧ 0 ≤ _x87 − 1 ∧ −1 ≤ _x88 − 1 ∧ −1 ≤ _x89 − 1 ∧ −1 ≤ _x112 − 1 ∧ −1 ≤ _x113 − 1 ∧ _x101 ≤ _x91 − 1 ∧ _x99 ≤ _x86 ∧ 3 ≤ _x86 − 1 ∧ 3 ≤ _x99 − 1 ∧ −1 ≤ _x102 − 1 ∧ _x90 + 3 ≤ _x86 ∧ _x92 + 3 ≤ _x86 ∧ _x88 = _x103 ∧ _x89 + 2 = _x104 ∧ _x90 = _x105 ∧ _x91 = _x106 ∧ _x92 = _x107
  f3463_0_put_NULL	6	f3541_0_put_EQ:		x1 = _x114 ∧ x2 = _x115 ∧ x3 = _x116 ∧ x4 = _x117 ∧ x5 = _x118 ∧ x6 = _x119 ∧ x7 = _x120 ∧ x8 = _x121 ∧ x9 = _x122 ∧ x10 = _x123 ∧ x11 = _x124 ∧ x12 = _x125 ∧ x13 = _x126 ∧ x1 = _x127 ∧ x2 = _x128 ∧ x3 = _x129 ∧ x4 = _x130 ∧ x5 = _x131 ∧ x6 = _x132 ∧ x7 = _x133 ∧ x8 = _x134 ∧ x9 = _x135 ∧ x10 = _x136 ∧ x11 = _x137 ∧ x12 = _x138 ∧ x13 = _x139 ∧ _x115 = _x134 ∧ _x122 = _x133 ∧ _x121 = _x132 ∧ _x120 = _x131 ∧ 0 = _x130 ∧ _x116 = _x128 ∧ _x136 + 4 ≤ _x117 ∧ _x115 + 2 ≤ _x117 ∧ _x122 + 3 ≤ _x114 ∧ _x120 + 3 ≤ _x114 ∧ −1 ≤ _x135 − 1 ∧ 2 ≤ _x129 − 1 ∧ 3 ≤ _x127 − 1 ∧ 2 ≤ _x117 − 1 ∧ 3 ≤ _x114 − 1 ∧ _x135 + 2 ≤ _x117 ∧ _x129 ≤ _x117 ∧ 1 ≤ _x121 − 1 ∧ _x127 ≤ _x114
  f3463_0_put_NULL	7	f3541_0_put_EQ:		x1 = _x140 ∧ x2 = _x141 ∧ x3 = _x142 ∧ x4 = _x143 ∧ x5 = _x144 ∧ x6 = _x145 ∧ x7 = _x146 ∧ x8 = _x147 ∧ x9 = _x148 ∧ x10 = _x149 ∧ x11 = _x150 ∧ x12 = _x151 ∧ x13 = _x152 ∧ x1 = _x153 ∧ x2 = _x154 ∧ x3 = _x155 ∧ x4 = _x156 ∧ x5 = _x157 ∧ x6 = _x158 ∧ x7 = _x159 ∧ x8 = _x160 ∧ x9 = _x161 ∧ x10 = _x162 ∧ x11 = _x163 ∧ x12 = _x164 ∧ x13 = _x165 ∧ _x141 = _x160 ∧ _x148 = _x159 ∧ _x147 = _x158 ∧ _x146 = _x157 ∧ 1 = _x156 ∧ _x142 = _x154 ∧ _x162 + 4 ≤ _x143 ∧ _x141 + 2 ≤ _x143 ∧ _x148 + 3 ≤ _x140 ∧ _x146 + 3 ≤ _x140 ∧ −1 ≤ _x161 − 1 ∧ 2 ≤ _x155 − 1 ∧ 3 ≤ _x153 − 1 ∧ 2 ≤ _x143 − 1 ∧ 3 ≤ _x140 − 1 ∧ _x161 + 2 ≤ _x143 ∧ _x155 ≤ _x143 ∧ 1 ≤ _x147 − 1 ∧ _x153 ≤ _x140
  f3463_0_put_NULL	8	f3463_0_put_NULL:		x1 = _x166 ∧ x2 = _x167 ∧ x3 = _x168 ∧ x4 = _x169 ∧ x5 = _x170 ∧ x6 = _x171 ∧ x7 = _x172 ∧ x8 = _x173 ∧ x9 = _x174 ∧ x10 = _x175 ∧ x11 = _x176 ∧ x12 = _x177 ∧ x13 = _x178 ∧ x1 = _x179 ∧ x2 = _x180 ∧ x3 = _x181 ∧ x4 = _x182 ∧ x5 = _x183 ∧ x6 = _x184 ∧ x7 = _x185 ∧ x8 = _x186 ∧ x9 = _x187 ∧ x10 = _x188 ∧ x11 = _x189 ∧ x12 = _x190 ∧ x13 = _x191 ∧ _x179 ≤ _x166 ∧ _x192 ≤ _x167 − 1 ∧ _x182 + 1 ≤ _x169 ∧ 3 ≤ _x166 − 1 ∧ 0 ≤ _x169 − 1 ∧ 3 ≤ _x179 − 1 ∧ −1 ≤ _x182 − 1 ∧ _x172 + 3 ≤ _x166 ∧ _x174 + 3 ≤ _x166 ∧ _x167 = _x180 ∧ _x168 = _x181 ∧ _x170 = _x183 ∧ _x171 = _x184 ∧ _x172 = _x185 ∧ _x173 = _x186 ∧ _x174 = _x187
  f3463_0_put_NULL	9	f3463_0_put_NULL:		x1 = _x193 ∧ x2 = _x194 ∧ x3 = _x195 ∧ x4 = _x196 ∧ x5 = _x197 ∧ x6 = _x198 ∧ x7 = _x199 ∧ x8 = _x200 ∧ x9 = _x201 ∧ x10 = _x202 ∧ x11 = _x203 ∧ x12 = _x204 ∧ x13 = _x205 ∧ x1 = _x206 ∧ x2 = _x207 ∧ x3 = _x208 ∧ x4 = _x209 ∧ x5 = _x210 ∧ x6 = _x211 ∧ x7 = _x213 ∧ x8 = _x214 ∧ x9 = _x215 ∧ x10 = _x216 ∧ x11 = _x217 ∧ x12 = _x218 ∧ x13 = _x219 ∧ _x206 ≤ _x193 ∧ _x194 ≤ _x220 − 1 ∧ _x209 + 1 ≤ _x196 ∧ 3 ≤ _x193 − 1 ∧ 0 ≤ _x196 − 1 ∧ 3 ≤ _x206 − 1 ∧ −1 ≤ _x209 − 1 ∧ _x199 + 3 ≤ _x193 ∧ _x201 + 3 ≤ _x193 ∧ _x194 = _x207 ∧ _x195 = _x208 ∧ _x197 = _x210 ∧ _x198 = _x211 ∧ _x199 = _x213 ∧ _x200 = _x214 ∧ _x201 = _x215
  f3463_0_put_NULL	10	f3463_0_put_NULL:		x1 = _x221 ∧ x2 = _x222 ∧ x3 = _x223 ∧ x4 = _x224 ∧ x5 = _x225 ∧ x6 = _x226 ∧ x7 = _x227 ∧ x8 = _x228 ∧ x9 = _x229 ∧ x10 = _x230 ∧ x11 = _x231 ∧ x12 = _x232 ∧ x13 = _x233 ∧ x1 = _x234 ∧ x2 = _x235 ∧ x3 = _x236 ∧ x4 = _x237 ∧ x5 = _x238 ∧ x6 = _x239 ∧ x7 = _x240 ∧ x8 = _x241 ∧ x9 = _x242 ∧ x10 = _x243 ∧ x11 = _x244 ∧ x12 = _x245 ∧ x13 = _x246 ∧ _x229 = _x242 ∧ _x228 = _x241 ∧ _x227 = _x240 ∧ _x226 = _x239 ∧ _x225 = _x238 ∧ _x223 = _x236 ∧ _x222 = _x235 ∧ _x222 + 2 ≤ _x224 ∧ _x229 + 3 ≤ _x221 ∧ _x227 + 3 ≤ _x221 ∧ −1 ≤ _x237 − 1 ∧ 3 ≤ _x234 − 1 ∧ 1 ≤ _x224 − 1 ∧ 3 ≤ _x221 − 1 ∧ _x237 + 2 ≤ _x224 ∧ 1 ≤ _x228 − 1 ∧ _x234 ≤ _x221
  f3463_0_put_NULL	11	f3463_0_put_NULL:		x1 = _x247 ∧ x2 = _x248 ∧ x3 = _x249 ∧ x4 = _x250 ∧ x5 = _x251 ∧ x6 = _x252 ∧ x7 = _x253 ∧ x8 = _x254 ∧ x9 = _x255 ∧ x10 = _x256 ∧ x11 = _x257 ∧ x12 = _x258 ∧ x13 = _x259 ∧ x1 = _x260 ∧ x2 = _x261 ∧ x3 = _x262 ∧ x4 = _x263 ∧ x5 = _x264 ∧ x6 = _x265 ∧ x7 = _x266 ∧ x8 = _x267 ∧ x9 = _x268 ∧ x10 = _x269 ∧ x11 = _x270 ∧ x12 = _x271 ∧ x13 = _x272 ∧ _x255 = _x268 ∧ _x254 = _x267 ∧ _x253 = _x266 ∧ _x252 = _x265 ∧ _x251 = _x264 ∧ _x249 = _x262 ∧ _x248 = _x261 ∧ _x248 + 2 ≤ _x250 ∧ _x255 + 3 ≤ _x247 ∧ _x253 + 3 ≤ _x247 ∧ −1 ≤ _x263 − 1 ∧ 3 ≤ _x260 − 1 ∧ 2 ≤ _x250 − 1 ∧ 3 ≤ _x247 − 1 ∧ _x263 + 2 ≤ _x250 ∧ 1 ≤ _x254 − 1 ∧ _x260 ≤ _x247
  f3541_0_put_EQ	12	f3463_0_put_NULL:		x1 = _x273 ∧ x2 = _x274 ∧ x3 = _x275 ∧ x4 = _x276 ∧ x5 = _x277 ∧ x6 = _x278 ∧ x7 = _x279 ∧ x8 = _x280 ∧ x9 = _x281 ∧ x10 = _x282 ∧ x11 = _x283 ∧ x12 = _x284 ∧ x13 = _x285 ∧ x1 = _x286 ∧ x2 = _x287 ∧ x3 = _x288 ∧ x4 = _x289 ∧ x5 = _x290 ∧ x6 = _x291 ∧ x7 = _x292 ∧ x8 = _x293 ∧ x9 = _x294 ∧ x10 = _x295 ∧ x11 = _x296 ∧ x12 = _x297 ∧ x13 = _x298 ∧ _x279 = _x294 ∧ _x278 = _x293 ∧ _x277 = _x292 ∧ _x274 = _x288 ∧ _x280 = _x287 ∧ 0 = _x276 ∧ _x282 + 4 ≤ _x275 ∧ _x280 + 2 ≤ _x275 ∧ _x279 + 3 ≤ _x273 ∧ _x277 + 3 ≤ _x273 ∧ −1 ≤ _x289 − 1 ∧ 3 ≤ _x286 − 1 ∧ −1 ≤ _x281 − 1 ∧ 2 ≤ _x275 − 1 ∧ 3 ≤ _x273 − 1 ∧ _x289 ≤ _x281 ∧ _x289 + 2 ≤ _x275 ∧ _x286 ≤ _x273
  f3463_0_put_NULL	13	f3987_0_transfer_GE:		x1 = _x299 ∧ x2 = _x300 ∧ x3 = _x301 ∧ x4 = _x302 ∧ x5 = _x303 ∧ x6 = _x304 ∧ x7 = _x305 ∧ x8 = _x306 ∧ x9 = _x307 ∧ x10 = _x308 ∧ x11 = _x309 ∧ x12 = _x310 ∧ x13 = _x311 ∧ x1 = _x312 ∧ x2 = _x313 ∧ x3 = _x314 ∧ x4 = _x315 ∧ x5 = _x316 ∧ x6 = _x317 ∧ x7 = _x318 ∧ x8 = _x319 ∧ x9 = _x320 ∧ x10 = _x321 ∧ x11 = _x322 ∧ x12 = _x323 ∧ x13 = _x324 ∧ _x306 = _x319 ∧ 2⋅_x306 = _x318 ∧ _x307 = _x317 ∧ _x305 + 1 = _x316 ∧ 0 = _x315 ∧ _x307 + 3 ≤ _x299 ∧ _x305 + 3 ≤ _x299 ∧ 0 ≤ _x314 − 1 ∧ 0 ≤ _x313 − 1 ∧ 3 ≤ _x312 − 1 ∧ −1 ≤ _x302 − 1 ∧ 3 ≤ _x299 − 1 ∧ _x314 − 1 ≤ _x302 ∧ _x314 + 3 ≤ _x299 ∧ _x313 − 1 ≤ _x302 ∧ _x313 + 3 ≤ _x299 ∧ _x312 − 1 ≤ _x299 ∧ _x306 ≤ 1073741823 ∧ 0 ≤ 2⋅_x306 ∧ _x307 ≤ _x305 ∧ 1 ≤ _x306 − 1 ∧ _x301 ≤ _x306 − 1
  f3463_0_put_NULL	14	f3987_0_transfer_GE:		x1 = _x325 ∧ x2 = _x326 ∧ x3 = _x327 ∧ x4 = _x328 ∧ x5 = _x329 ∧ x6 = _x330 ∧ x7 = _x331 ∧ x8 = _x332 ∧ x9 = _x333 ∧ x10 = _x334 ∧ x11 = _x335 ∧ x12 = _x336 ∧ x13 = _x337 ∧ x1 = _x338 ∧ x2 = _x339 ∧ x3 = _x340 ∧ x4 = _x341 ∧ x5 = _x342 ∧ x6 = _x343 ∧ x7 = _x344 ∧ x8 = _x345 ∧ x9 = _x346 ∧ x10 = _x347 ∧ x11 = _x348 ∧ x12 = _x349 ∧ x13 = _x350 ∧ _x332 = _x345 ∧ 2⋅_x332 = _x344 ∧ _x333 = _x343 ∧ _x331 + 1 = _x342 ∧ 0 = _x341 ∧ _x333 + 3 ≤ _x325 ∧ _x331 + 3 ≤ _x325 ∧ 0 ≤ _x340 − 1 ∧ 0 ≤ _x339 − 1 ∧ 3 ≤ _x338 − 1 ∧ −1 ≤ _x328 − 1 ∧ 3 ≤ _x325 − 1 ∧ _x340 − 1 ≤ _x328 ∧ _x340 + 3 ≤ _x325 ∧ _x339 − 1 ≤ _x328 ∧ _x339 + 3 ≤ _x325 ∧ _x338 − 1 ≤ _x325 ∧ _x333 ≤ _x331 ∧ 0 ≤ 2⋅_x332 ∧ 1073741824 ≤ _x332 − 1 ∧ _x327 ≤ _x332 − 1
  f3987_0_transfer_GE	15	f4082_0_transfer_ArrayAccess:		x1 = _x351 ∧ x2 = _x352 ∧ x3 = _x353 ∧ x4 = _x354 ∧ x5 = _x355 ∧ x6 = _x356 ∧ x7 = _x357 ∧ x8 = _x358 ∧ x9 = _x359 ∧ x10 = _x360 ∧ x11 = _x361 ∧ x12 = _x362 ∧ x13 = _x363 ∧ x1 = _x364 ∧ x2 = _x365 ∧ x3 = _x366 ∧ x4 = _x367 ∧ x5 = _x368 ∧ x6 = _x369 ∧ x7 = _x370 ∧ x8 = _x371 ∧ x9 = _x372 ∧ x10 = _x373 ∧ x11 = _x374 ∧ x12 = _x375 ∧ x13 = _x376 ∧ _x357 = _x376 ∧ _x358 = _x373 ∧ _x356 = _x372 ∧ _x355 = _x371 ∧ _x354 = _x366 ∧ _x356 + 3 ≤ _x351 ∧ _x355 + 3 ≤ _x351 ∧ 0 ≤ _x369 − 1 ∧ 0 ≤ _x368 − 1 ∧ −1 ≤ _x367 − 1 ∧ 0 ≤ _x365 − 1 ∧ 3 ≤ _x364 − 1 ∧ 0 ≤ _x353 − 1 ∧ 0 ≤ _x352 − 1 ∧ 3 ≤ _x351 − 1 ∧ _x369 ≤ _x353 ∧ _x369 ≤ _x352 ∧ _x369 + 3 ≤ _x351 ∧ _x365 ≤ _x353 ∧ _x365 ≤ _x352 ∧ _x365 + 3 ≤ _x351 ∧ _x364 ≤ _x351 ∧ _x354 ≤ _x358 − 1 ∧ 0 ≤ _x357 − 1
  f4082_0_transfer_ArrayAccess	16	f4082_0_transfer_ArrayAccess:		x1 = _x377 ∧ x2 = _x378 ∧ x3 = _x379 ∧ x4 = _x380 ∧ x5 = _x381 ∧ x6 = _x382 ∧ x7 = _x383 ∧ x8 = _x384 ∧ x9 = _x385 ∧ x10 = _x386 ∧ x11 = _x387 ∧ x12 = _x388 ∧ x13 = _x389 ∧ x1 = _x390 ∧ x2 = _x391 ∧ x3 = _x392 ∧ x4 = _x393 ∧ x5 = _x394 ∧ x6 = _x395 ∧ x7 = _x396 ∧ x8 = _x397 ∧ x9 = _x398 ∧ x10 = _x399 ∧ x11 = _x400 ∧ x12 = _x401 ∧ x13 = _x402 ∧ _x389 = _x402 ∧ _x386 = _x399 ∧ _x385 = _x398 ∧ _x384 = _x397 ∧ _x379 = _x392 ∧ _x388 + 2 ≤ _x381 ∧ _x401 + 4 ≤ _x381 ∧ _x400 + 4 ≤ _x381 ∧ _x387 + 2 ≤ _x381 ∧ _x401 + 2 ≤ _x380 ∧ _x400 + 2 ≤ _x380 ∧ _x385 + 3 ≤ _x377 ∧ _x384 + 3 ≤ _x377 ∧ 0 ≤ _x395 − 1 ∧ 0 ≤ _x394 − 1 ∧ −1 ≤ _x393 − 1 ∧ 0 ≤ _x391 − 1 ∧ 3 ≤ _x390 − 1 ∧ 0 ≤ _x382 − 1 ∧ 2 ≤ _x381 − 1 ∧ 0 ≤ _x380 − 1 ∧ 0 ≤ _x378 − 1 ∧ 3 ≤ _x377 − 1 ∧ _x395 ≤ _x382 ∧ _x395 + 2 ≤ _x381 ∧ _x395 ≤ _x380 ∧ _x395 ≤ _x378 ∧ _x395 + 3 ≤ _x377 ∧ _x394 + 2 ≤ _x381 ∧ _x394 ≤ _x380 ∧ _x393 + 3 ≤ _x381 ∧ _x393 + 1 ≤ _x380 ∧ _x391 ≤ _x382 ∧ _x391 + 2 ≤ _x381 ∧ _x391 ≤ _x380 ∧ _x391 ≤ _x378 ∧ _x391 + 3 ≤ _x377 ∧ _x390 ≤ _x377 ∧ 0 ≤ _x389 − 1 ∧ _x383 ≤ _x389 − 1
  f3987_0_transfer_GE	17	f3987_0_transfer_GE:		x1 = _x403 ∧ x2 = _x404 ∧ x3 = _x405 ∧ x4 = _x406 ∧ x5 = _x407 ∧ x6 = _x408 ∧ x7 = _x409 ∧ x8 = _x410 ∧ x9 = _x411 ∧ x10 = _x412 ∧ x11 = _x413 ∧ x12 = _x414 ∧ x13 = _x415 ∧ x1 = _x416 ∧ x2 = _x417 ∧ x3 = _x418 ∧ x4 = _x419 ∧ x5 = _x420 ∧ x6 = _x421 ∧ x7 = _x422 ∧ x8 = _x423 ∧ x9 = _x424 ∧ x10 = _x425 ∧ x11 = _x426 ∧ x12 = _x427 ∧ x13 = _x428 ∧ _x410 = _x423 ∧ _x409 = _x422 ∧ _x408 = _x421 ∧ _x407 = _x420 ∧ _x406 + 1 = _x419 ∧ _x408 + 3 ≤ _x403 ∧ _x407 + 3 ≤ _x403 ∧ 0 ≤ _x418 − 1 ∧ 0 ≤ _x417 − 1 ∧ 3 ≤ _x416 − 1 ∧ 0 ≤ _x405 − 1 ∧ 0 ≤ _x404 − 1 ∧ 3 ≤ _x403 − 1 ∧ _x418 ≤ _x405 ∧ _x418 ≤ _x404 ∧ _x418 + 3 ≤ _x403 ∧ _x417 ≤ _x405 ∧ _x417 ≤ _x404 ∧ _x417 + 3 ≤ _x403 ∧ _x416 ≤ _x403 ∧ _x406 ≤ _x410 − 1 ∧ −1 ≤ _x410 − 1
  f4082_0_transfer_ArrayAccess	18	f3987_0_transfer_GE:		x1 = _x429 ∧ x2 = _x430 ∧ x3 = _x431 ∧ x4 = _x432 ∧ x5 = _x433 ∧ x6 = _x434 ∧ x7 = _x435 ∧ x8 = _x436 ∧ x9 = _x437 ∧ x10 = _x438 ∧ x11 = _x439 ∧ x12 = _x440 ∧ x13 = _x441 ∧ x1 = _x442 ∧ x2 = _x443 ∧ x3 = _x444 ∧ x4 = _x445 ∧ x5 = _x446 ∧ x6 = _x447 ∧ x7 = _x448 ∧ x8 = _x449 ∧ x9 = _x450 ∧ x10 = _x451 ∧ x11 = _x452 ∧ x12 = _x453 ∧ x13 = _x454 ∧ _x438 = _x449 ∧ _x441 = _x448 ∧ _x437 = _x447 ∧ _x436 = _x446 ∧ _x431 + 1 = _x445 ∧ _x440 + 2 ≤ _x433 ∧ _x439 + 2 ≤ _x433 ∧ _x437 + 3 ≤ _x429 ∧ _x436 + 3 ≤ _x429 ∧ 0 ≤ _x444 − 1 ∧ 0 ≤ _x443 − 1 ∧ 3 ≤ _x442 − 1 ∧ 0 ≤ _x434 − 1 ∧ 1 ≤ _x433 − 1 ∧ −1 ≤ _x432 − 1 ∧ 0 ≤ _x430 − 1 ∧ 3 ≤ _x429 − 1 ∧ _x444 ≤ _x434 ∧ _x444 + 1 ≤ _x433 ∧ _x444 − 1 ≤ _x432 ∧ _x444 ≤ _x430 ∧ _x444 + 3 ≤ _x429 ∧ _x443 ≤ _x434 ∧ _x443 + 1 ≤ _x433 ∧ _x443 − 1 ≤ _x432 ∧ _x443 ≤ _x430 ∧ _x443 + 3 ≤ _x429 ∧ _x442 ≤ _x429 ∧ _x435 ≤ _x441 − 1 ∧ −1 ≤ _x438 − 1
  __init	19	f1_0_main_Load:		x1 = _x455 ∧ x2 = _x456 ∧ x3 = _x457 ∧ x4 = _x458 ∧ x5 = _x459 ∧ x6 = _x460 ∧ x7 = _x461 ∧ x8 = _x462 ∧ x9 = _x463 ∧ x10 = _x464 ∧ x11 = _x465 ∧ x12 = _x466 ∧ x13 = _x467 ∧ x1 = _x468 ∧ x2 = _x469 ∧ x3 = _x470 ∧ x4 = _x471 ∧ x5 = _x472 ∧ x6 = _x473 ∧ x7 = _x474 ∧ x8 = _x475 ∧ x9 = _x476 ∧ x10 = _x477 ∧ x11 = _x478 ∧ x12 = _x479 ∧ x13 = _x480 ∧ 0 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

2 SCC Decomposition

We consider subproblems for each of the 3 SCC(s) of the program graph.

2.1 SCC Subproblem 1/3

Here we consider the SCC { f2980_0_createMap_LE }.

2.1.1 Transition Removal

We remove transition 4 using the following ranking functions, which are bounded by 0.

2.1.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.2 SCC Subproblem 2/3

Here we consider the SCC { f3463_0_put_NULL, f3541_0_put_EQ }.

2.2.1 Transition Removal

We remove transitions 6, 8, 9, 10, 11, 12, 7 using the following ranking functions, which are bounded by 0.

2.2.2 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

2.3 SCC Subproblem 3/3

Here we consider the SCC { f3987_0_transfer_GE, f4082_0_transfer_ArrayAccess }.

2.3.1 Transition Removal

We remove transition 17 using the following ranking functions, which are bounded by 0.

2.3.2 Transition Removal

We remove transition 15 using the following ranking functions, which are bounded by 0.

2.3.3 Transition Removal

We remove transitions 18, 16 using the following ranking functions, which are bounded by 0.

2.3.4 Trivial Cooperation Program

There are no more "sharp" transitions in the cooperation program. Hence the cooperation termination is proved.

Tool configuration

AProVE

• version: AProVE Commit ID: unknown
• strategy: Statistics for single proof: 100.00 % (13 real / 0 unknown / 0 assumptions / 13 total proof steps)