LTS Termination Proof

by AProVE

Input

• Initial Location: f4423_0_transfer_ArrayAccess, f3804_0_put_NULL, f3882_0_put_EQ, f3248_0_createMap_LE, f4328_0_transfer_GE, f517_0_createMap_Return, f1_0_main_Load, f3559_0_clear_GE, __init
• Transitions: (pre-variables and post-variables)

  f1_0_main_Load	1	f3559_0_clear_GE:		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 ≤ _arg6P − 1 ∧ 0 ≤ _arg2 − 1 ∧ −1 ≤ _x7 − 1 ∧ _arg2P ≤ _arg1 ∧ 0 ≤ _arg1 − 1 ∧ 3 ≤ _arg1P − 1 ∧ 0 ≤ _arg2P − 1 ∧ 0 = _arg3P
  f517_0_createMap_Return	2	f3559_0_clear_GE:		x1 = _x ∧ x2 = _x1 ∧ x3 = _x2 ∧ x4 = _x3 ∧ x5 = _x4 ∧ x6 = _x5 ∧ x7 = _x6 ∧ 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 ∧ 16 = _x19 ∧ 12 = _x18 ∧ _x2 = _x17 ∧ 0 = _x16 ∧ 12 = _x3 ∧ 16 = _x1 ∧ _x2 + 3 ≤ _x ∧ 0 ≤ _x15 − 1 ∧ 14 ≤ _x14 − 1 ∧ 14 ≤ _x − 1 ∧ _x15 + 14 ≤ _x ∧ _x14 ≤ _x
  f3559_0_clear_GE	3	f3559_0_clear_GE:		x1 = _x27 ∧ x2 = _x28 ∧ x3 = _x29 ∧ x4 = _x30 ∧ x5 = _x31 ∧ x6 = _x32 ∧ x7 = _x33 ∧ x8 = _x34 ∧ x9 = _x37 ∧ x10 = _x38 ∧ x11 = _x39 ∧ x12 = _x40 ∧ x13 = _x41 ∧ x1 = _x42 ∧ x2 = _x43 ∧ x3 = _x44 ∧ x4 = _x45 ∧ x5 = _x46 ∧ x6 = _x47 ∧ x7 = _x50 ∧ x8 = _x51 ∧ x9 = _x52 ∧ x10 = _x53 ∧ x11 = _x54 ∧ x12 = _x55 ∧ x13 = _x56 ∧ _x32 = _x47 ∧ _x31 = _x46 ∧ _x30 = _x45 ∧ _x29 + 1 = _x44 ∧ _x31 + 3 ≤ _x27 ∧ _x30 + 3 ≤ _x27 ∧ 0 ≤ _x43 − 1 ∧ 3 ≤ _x42 − 1 ∧ 0 ≤ _x28 − 1 ∧ 3 ≤ _x27 − 1 ∧ _x43 ≤ _x28 ∧ _x43 + 3 ≤ _x27 ∧ _x42 ≤ _x27 ∧ _x29 ≤ _x32 − 1 ∧ −1 ≤ _x32 − 1
  f1_0_main_Load	4	f3248_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 = _x79 ∧ x11 = _x80 ∧ x12 = _x81 ∧ x13 = _x82 ∧ 12 = _x76 ∧ 0 = _x75 ∧ 16 = _x74 ∧ 1 = _x73 ∧ _x58 = _x72 ∧ 14 ≤ _x70 − 1 ∧ 0 ≤ _x57 − 1 ∧ _x70 − 14 ≤ _x57 ∧ 0 ≤ _x58 − 1 ∧ −1 ≤ _x71 − 1
  f3248_0_createMap_LE	5	f3248_0_createMap_LE:		x1 = _x83 ∧ x2 = _x84 ∧ x3 = _x85 ∧ x4 = _x86 ∧ x5 = _x88 ∧ x6 = _x89 ∧ x7 = _x90 ∧ x8 = _x91 ∧ x9 = _x92 ∧ x10 = _x93 ∧ x11 = _x94 ∧ x12 = _x95 ∧ x13 = _x96 ∧ x1 = _x97 ∧ x2 = _x98 ∧ x3 = _x99 ∧ x4 = _x100 ∧ x5 = _x101 ∧ x6 = _x102 ∧ x7 = _x103 ∧ x8 = _x104 ∧ x9 = _x105 ∧ x10 = _x106 ∧ x11 = _x107 ∧ x12 = _x108 ∧ x13 = _x109 ∧ 0 ≤ _x84 − 1 ∧ _x86 + 1 ≤ _x85 − 1 ∧ −1 ≤ _x85 − 1 ∧ −1 ≤ _x86 − 1 ∧ −1 ≤ _x110 − 1 ∧ −1 ≤ _x111 − 1 ∧ 1 ≤ _x88 − 1 ∧ 3 ≤ _x83 − 1 ∧ 3 ≤ _x97 − 1 ∧ _x90 + 3 ≤ _x83 ∧ _x89 + 3 ≤ _x83 ∧ _x84 − 1 = _x98 ∧ _x85 = _x99 ∧ _x86 + 2 = _x100
  f3248_0_createMap_LE	6	f3804_0_put_NULL:		x1 = _x112 ∧ x2 = _x113 ∧ x3 = _x114 ∧ x4 = _x115 ∧ x5 = _x116 ∧ x6 = _x117 ∧ x7 = _x118 ∧ x8 = _x119 ∧ x9 = _x120 ∧ x10 = _x121 ∧ x11 = _x122 ∧ x12 = _x123 ∧ x13 = _x124 ∧ x1 = _x125 ∧ x2 = _x126 ∧ x3 = _x127 ∧ x4 = _x128 ∧ x5 = _x129 ∧ x6 = _x130 ∧ x7 = _x131 ∧ x8 = _x132 ∧ x9 = _x133 ∧ x10 = _x134 ∧ x11 = _x135 ∧ x12 = _x136 ∧ x13 = _x137 ∧ _x115 + 1 ≤ _x114 − 1 ∧ 1 ≤ _x116 − 1 ∧ 0 ≤ _x113 − 1 ∧ −1 ≤ _x114 − 1 ∧ −1 ≤ _x115 − 1 ∧ −1 ≤ _x138 − 1 ∧ −1 ≤ _x139 − 1 ∧ _x127 ≤ _x116 − 1 ∧ _x125 ≤ _x112 ∧ 3 ≤ _x112 − 1 ∧ 3 ≤ _x125 − 1 ∧ −1 ≤ _x128 − 1 ∧ _x118 + 3 ≤ _x112 ∧ _x117 + 3 ≤ _x112 ∧ _x114 = _x129 ∧ _x115 + 2 = _x130 ∧ _x116 = _x131 ∧ _x117 = _x132 ∧ _x118 = _x133
  f3804_0_put_NULL	7	f3882_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 ∧ 0 = _x156 ∧ _x142 = _x154 ∧ _x162 + 4 ≤ _x143 ∧ _x141 + 2 ≤ _x143 ∧ _x148 + 3 ≤ _x140 ∧ _x147 + 3 ≤ _x140 ∧ −1 ≤ _x161 − 1 ∧ 2 ≤ _x155 − 1 ∧ 3 ≤ _x153 − 1 ∧ 2 ≤ _x143 − 1 ∧ 3 ≤ _x140 − 1 ∧ _x161 + 2 ≤ _x143 ∧ _x155 ≤ _x143 ∧ 1 ≤ _x146 − 1 ∧ _x153 ≤ _x140
  f3804_0_put_NULL	8	f3882_0_put_EQ:		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 ∧ _x167 = _x186 ∧ _x174 = _x185 ∧ _x173 = _x184 ∧ _x172 = _x183 ∧ 1 = _x182 ∧ _x168 = _x180 ∧ _x188 + 4 ≤ _x169 ∧ _x167 + 2 ≤ _x169 ∧ _x174 + 3 ≤ _x166 ∧ _x173 + 3 ≤ _x166 ∧ −1 ≤ _x187 − 1 ∧ 2 ≤ _x181 − 1 ∧ 3 ≤ _x179 − 1 ∧ 2 ≤ _x169 − 1 ∧ 3 ≤ _x166 − 1 ∧ _x187 + 2 ≤ _x169 ∧ _x181 ≤ _x169 ∧ 1 ≤ _x172 − 1 ∧ _x179 ≤ _x166
  f3804_0_put_NULL	9	f3804_0_put_NULL:		x1 = _x192 ∧ x2 = _x193 ∧ x3 = _x194 ∧ x4 = _x195 ∧ x5 = _x196 ∧ x6 = _x197 ∧ x7 = _x198 ∧ x8 = _x199 ∧ x9 = _x200 ∧ x10 = _x201 ∧ x11 = _x202 ∧ x12 = _x203 ∧ x13 = _x204 ∧ x1 = _x205 ∧ x2 = _x206 ∧ x3 = _x207 ∧ x4 = _x208 ∧ x5 = _x209 ∧ x6 = _x210 ∧ x7 = _x211 ∧ x8 = _x212 ∧ x9 = _x213 ∧ x10 = _x214 ∧ x11 = _x215 ∧ x12 = _x216 ∧ x13 = _x217 ∧ _x205 ≤ _x192 ∧ _x218 ≤ _x193 − 1 ∧ _x208 + 1 ≤ _x195 ∧ 3 ≤ _x192 − 1 ∧ 0 ≤ _x195 − 1 ∧ 3 ≤ _x205 − 1 ∧ −1 ≤ _x208 − 1 ∧ _x199 + 3 ≤ _x192 ∧ _x200 + 3 ≤ _x192 ∧ _x193 = _x206 ∧ _x194 = _x207 ∧ _x196 = _x209 ∧ _x197 = _x210 ∧ _x198 = _x211 ∧ _x199 = _x212 ∧ _x200 = _x213
  f3804_0_put_NULL	10	f3804_0_put_NULL:		x1 = _x219 ∧ x2 = _x220 ∧ x3 = _x221 ∧ x4 = _x223 ∧ x5 = _x224 ∧ x6 = _x225 ∧ x7 = _x226 ∧ x8 = _x227 ∧ x9 = _x228 ∧ x10 = _x229 ∧ x11 = _x230 ∧ x12 = _x231 ∧ x13 = _x232 ∧ x1 = _x233 ∧ x2 = _x234 ∧ x3 = _x235 ∧ x4 = _x236 ∧ x5 = _x237 ∧ x6 = _x238 ∧ x7 = _x239 ∧ x8 = _x240 ∧ x9 = _x241 ∧ x10 = _x242 ∧ x11 = _x243 ∧ x12 = _x244 ∧ x13 = _x245 ∧ _x233 ≤ _x219 ∧ _x220 ≤ _x246 − 1 ∧ _x236 + 1 ≤ _x223 ∧ 3 ≤ _x219 − 1 ∧ 0 ≤ _x223 − 1 ∧ 3 ≤ _x233 − 1 ∧ −1 ≤ _x236 − 1 ∧ _x227 + 3 ≤ _x219 ∧ _x228 + 3 ≤ _x219 ∧ _x220 = _x234 ∧ _x221 = _x235 ∧ _x224 = _x237 ∧ _x225 = _x238 ∧ _x226 = _x239 ∧ _x227 = _x240 ∧ _x228 = _x241
  f3804_0_put_NULL	11	f3804_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 ∧ _x254 + 3 ≤ _x247 ∧ −1 ≤ _x263 − 1 ∧ 3 ≤ _x260 − 1 ∧ 1 ≤ _x250 − 1 ∧ 3 ≤ _x247 − 1 ∧ _x263 + 2 ≤ _x250 ∧ 1 ≤ _x253 − 1 ∧ _x260 ≤ _x247
  f3804_0_put_NULL	12	f3804_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 ∧ _x281 = _x294 ∧ _x280 = _x293 ∧ _x279 = _x292 ∧ _x278 = _x291 ∧ _x277 = _x290 ∧ _x275 = _x288 ∧ _x274 = _x287 ∧ _x274 + 2 ≤ _x276 ∧ _x281 + 3 ≤ _x273 ∧ _x280 + 3 ≤ _x273 ∧ −1 ≤ _x289 − 1 ∧ 3 ≤ _x286 − 1 ∧ 2 ≤ _x276 − 1 ∧ 3 ≤ _x273 − 1 ∧ _x289 + 2 ≤ _x276 ∧ 1 ≤ _x279 − 1 ∧ _x286 ≤ _x273
  f3882_0_put_EQ	13	f3804_0_put_NULL:		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 ∧ _x305 = _x320 ∧ _x304 = _x319 ∧ _x303 = _x318 ∧ _x300 = _x314 ∧ _x306 = _x313 ∧ 0 = _x302 ∧ _x308 + 4 ≤ _x301 ∧ _x306 + 2 ≤ _x301 ∧ _x305 + 3 ≤ _x299 ∧ _x304 + 3 ≤ _x299 ∧ −1 ≤ _x315 − 1 ∧ 3 ≤ _x312 − 1 ∧ −1 ≤ _x307 − 1 ∧ 2 ≤ _x301 − 1 ∧ 3 ≤ _x299 − 1 ∧ _x315 ≤ _x307 ∧ _x315 + 2 ≤ _x301 ∧ _x312 ≤ _x299
  f3804_0_put_NULL	14	f4328_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 ∧ _x331 = _x345 ∧ 2⋅_x331 = _x344 ∧ _x333 = _x343 ∧ _x332 + 1 = _x342 ∧ 0 = _x341 ∧ _x333 + 3 ≤ _x325 ∧ _x332 + 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 ∧ _x331 ≤ 1073741823 ∧ 0 ≤ 2⋅_x331 ∧ _x333 ≤ _x332 ∧ 1 ≤ _x331 − 1 ∧ _x327 ≤ _x331 − 1
  f3804_0_put_NULL	15	f4328_0_transfer_GE:		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 = _x371 ∧ 2⋅_x357 = _x370 ∧ _x359 = _x369 ∧ _x358 + 1 = _x368 ∧ 0 = _x367 ∧ _x359 + 3 ≤ _x351 ∧ _x358 + 3 ≤ _x351 ∧ 0 ≤ _x366 − 1 ∧ 0 ≤ _x365 − 1 ∧ 3 ≤ _x364 − 1 ∧ −1 ≤ _x354 − 1 ∧ 3 ≤ _x351 − 1 ∧ _x366 − 1 ≤ _x354 ∧ _x366 + 3 ≤ _x351 ∧ _x365 − 1 ≤ _x354 ∧ _x365 + 3 ≤ _x351 ∧ _x364 − 1 ≤ _x351 ∧ _x359 ≤ _x358 ∧ 0 ≤ 2⋅_x357 ∧ 1073741824 ≤ _x357 − 1 ∧ _x353 ≤ _x357 − 1
  f4328_0_transfer_GE	16	f4423_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 ∧ _x383 = _x402 ∧ _x384 = _x399 ∧ _x382 = _x398 ∧ _x381 = _x397 ∧ _x380 = _x392 ∧ _x382 + 3 ≤ _x377 ∧ _x381 + 3 ≤ _x377 ∧ 0 ≤ _x395 − 1 ∧ 0 ≤ _x394 − 1 ∧ −1 ≤ _x393 − 1 ∧ 0 ≤ _x391 − 1 ∧ 3 ≤ _x390 − 1 ∧ 0 ≤ _x379 − 1 ∧ 0 ≤ _x378 − 1 ∧ 3 ≤ _x377 − 1 ∧ _x395 ≤ _x379 ∧ _x395 ≤ _x378 ∧ _x395 + 3 ≤ _x377 ∧ _x391 ≤ _x379 ∧ _x391 ≤ _x378 ∧ _x391 + 3 ≤ _x377 ∧ _x390 ≤ _x377 ∧ _x380 ≤ _x384 − 1 ∧ 0 ≤ _x383 − 1
  f4423_0_transfer_ArrayAccess	17	f4423_0_transfer_ArrayAccess:		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 ∧ _x415 = _x428 ∧ _x412 = _x425 ∧ _x411 = _x424 ∧ _x410 = _x423 ∧ _x405 = _x418 ∧ _x414 + 2 ≤ _x407 ∧ _x427 + 4 ≤ _x407 ∧ _x426 + 4 ≤ _x407 ∧ _x413 + 2 ≤ _x407 ∧ _x427 + 2 ≤ _x406 ∧ _x426 + 2 ≤ _x406 ∧ _x411 + 3 ≤ _x403 ∧ _x410 + 3 ≤ _x403 ∧ 0 ≤ _x421 − 1 ∧ 0 ≤ _x420 − 1 ∧ −1 ≤ _x419 − 1 ∧ 0 ≤ _x417 − 1 ∧ 3 ≤ _x416 − 1 ∧ 0 ≤ _x408 − 1 ∧ 2 ≤ _x407 − 1 ∧ 0 ≤ _x406 − 1 ∧ 0 ≤ _x404 − 1 ∧ 3 ≤ _x403 − 1 ∧ _x421 ≤ _x408 ∧ _x421 + 2 ≤ _x407 ∧ _x421 ≤ _x406 ∧ _x421 ≤ _x404 ∧ _x421 + 3 ≤ _x403 ∧ _x420 + 2 ≤ _x407 ∧ _x420 ≤ _x406 ∧ _x419 + 3 ≤ _x407 ∧ _x419 + 1 ≤ _x406 ∧ _x417 ≤ _x408 ∧ _x417 + 2 ≤ _x407 ∧ _x417 ≤ _x406 ∧ _x417 ≤ _x404 ∧ _x417 + 3 ≤ _x403 ∧ _x416 ≤ _x403 ∧ 0 ≤ _x415 − 1 ∧ _x409 ≤ _x415 − 1
  f4328_0_transfer_GE	18	f4328_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 ∧ _x436 = _x449 ∧ _x435 = _x448 ∧ _x434 = _x447 ∧ _x433 = _x446 ∧ _x432 + 1 = _x445 ∧ _x434 + 3 ≤ _x429 ∧ _x433 + 3 ≤ _x429 ∧ 0 ≤ _x444 − 1 ∧ 0 ≤ _x443 − 1 ∧ 3 ≤ _x442 − 1 ∧ 0 ≤ _x431 − 1 ∧ 0 ≤ _x430 − 1 ∧ 3 ≤ _x429 − 1 ∧ _x444 ≤ _x431 ∧ _x444 ≤ _x430 ∧ _x444 + 3 ≤ _x429 ∧ _x443 ≤ _x431 ∧ _x443 ≤ _x430 ∧ _x443 + 3 ≤ _x429 ∧ _x442 ≤ _x429 ∧ _x432 ≤ _x436 − 1 ∧ −1 ≤ _x436 − 1
  f4423_0_transfer_ArrayAccess	19	f4328_0_transfer_GE:		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 ∧ _x464 = _x475 ∧ _x467 = _x474 ∧ _x463 = _x473 ∧ _x462 = _x472 ∧ _x457 + 1 = _x471 ∧ _x466 + 2 ≤ _x459 ∧ _x465 + 2 ≤ _x459 ∧ _x463 + 3 ≤ _x455 ∧ _x462 + 3 ≤ _x455 ∧ 0 ≤ _x470 − 1 ∧ 0 ≤ _x469 − 1 ∧ 3 ≤ _x468 − 1 ∧ 0 ≤ _x460 − 1 ∧ 1 ≤ _x459 − 1 ∧ −1 ≤ _x458 − 1 ∧ 0 ≤ _x456 − 1 ∧ 3 ≤ _x455 − 1 ∧ _x470 ≤ _x460 ∧ _x470 + 1 ≤ _x459 ∧ _x470 − 1 ≤ _x458 ∧ _x470 ≤ _x456 ∧ _x470 + 3 ≤ _x455 ∧ _x469 ≤ _x460 ∧ _x469 + 1 ≤ _x459 ∧ _x469 − 1 ≤ _x458 ∧ _x469 ≤ _x456 ∧ _x469 + 3 ≤ _x455 ∧ _x468 ≤ _x455 ∧ _x461 ≤ _x467 − 1 ∧ −1 ≤ _x464 − 1
  __init	20	f1_0_main_Load:		x1 = _x481 ∧ x2 = _x482 ∧ x3 = _x483 ∧ x4 = _x484 ∧ x5 = _x485 ∧ x6 = _x486 ∧ x7 = _x487 ∧ x8 = _x488 ∧ x9 = _x489 ∧ x10 = _x490 ∧ x11 = _x491 ∧ x12 = _x492 ∧ x13 = _x493 ∧ x1 = _x494 ∧ x2 = _x495 ∧ x3 = _x496 ∧ x4 = _x497 ∧ x5 = _x498 ∧ x6 = _x499 ∧ x7 = _x500 ∧ x8 = _x501 ∧ x9 = _x502 ∧ x10 = _x503 ∧ x11 = _x504 ∧ x12 = _x505 ∧ x13 = _x506 ∧ 0 ≤ 0

Proof

1 Switch to Cooperation Termination Proof

2 SCC Decomposition

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

2.1 SCC Subproblem 1/4

Here we consider the SCC { f3248_0_createMap_LE }.

2.1.1 Transition Removal

We remove transition 5 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/4

Here we consider the SCC { f3804_0_put_NULL, f3882_0_put_EQ }.

2.2.1 Transition Removal

We remove transitions 7, 9, 10, 11, 12, 13, 8 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/4

Here we consider the SCC { f4423_0_transfer_ArrayAccess, f4328_0_transfer_GE }.

2.3.1 Transition Removal

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

2.3.2 Transition Removal

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

2.3.3 Transition Removal

We remove transitions 19, 17 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.

2.4 SCC Subproblem 4/4

Here we consider the SCC { f3559_0_clear_GE }.

2.4.1 Transition Removal

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

2.4.2 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 % (16 real / 0 unknown / 0 assumptions / 16 total proof steps)