NO Termination: (Ranking Functions Found) ------------ l0: < < i21_0 > > l2: < < i21_0 > > NON-Termination: ---------------- SCC: +--transitions: t122,t4 +--nodes: l3,l4 Closed walk: 2 -> t122, t4 Reachability checked! - Recurrent Set Found: { tmp___115_0 -tmp___115_post == 0, tmp___024_0 -tmp___024_post == 0, tmp___017_0 -tmp___017_post == 0, tmp___014_0 -tmp___014_post == 0, ent8_0 -tmp12_post == 0, tabort4_0 -tabort4_post == 0, seed2_0 -seed2_post == 0, ret_getbyte25_0 -ret_getbyte25_post == 0, ent8_0 -ret_getbyte18_post == 0, ratio_post == 0, rat26_0 -rat26_post == 0, r_off32_0 -r_off32_post == 0, out_count_post == 0, offset_post == 0, __const_9_0 -n_bits_post == 0, n44_0 -n44_post == 0, n40_0 -n40_post == 0, maxmaxcode_0 -maxmaxcode_post == 0, maxcode_0 -maxcode_post == 0, __const_16_0 -maxbits_post == 0, m130_0 -m130_post == 0, 1 + m122_post == 0, -1 + in_count_post == 0, i6_post == 0, i45_0 -i45_post == 0, i41_0 -i41_post == 0, i3_0 -i3_post == 0, i29_0 -i29_post == 0, __const_16_0 -i21_0 + i21_post == 0, hsize_0 -hsize_reg10_post == 0, hsize___027_0 -hsize___027_post == 0, hsize_0 -hsize___019_post == 0, hsize_0 -hsize_post == 0, hshift11_0 -hshift11_post == 0, free_ent_0 -free_ent_post == 0, fcode5_0 -fcode5_post == 0, exit_stat_0 -exit_stat_post == 0, ent8_0 -ent8_post == 0, disp9_0 -disp9_post == 0, __const_50_0 -count_post == 0, code31_0 -code31_post == 0, clear_flg_post == 0, __const_10000_0 -checkpoint_post == 0, c7_0 -c7_post == 0, -3 + bytes_out_post == 0, block_compress_0 -block_compress_post == 0, bits33_0 -bits33_post == 0, apsim_bound11113_0 -apsim_bound11113_post == 0, apsim_InCnt_0 -apsim_InCnt_post == 0, __const_9_0 -__const_9_post == 0, __const_8_0 -__const_8_post == 0, __const_8388607_0 -__const_8388607_post == 0, __const_65536_0 -__const_65536_post == 0, __const_53_0 -__const_53_post == 0, __const_50_0 -__const_50_post == 0, __const_429496_0 -__const_429496_post == 0, __const_257_0 -__const_257_post == 0, __const_256_0 -__const_256_post == 0, __const_2147483647_0 -__const_2147483647_post == 0, __const_16_0 -__const_16_post == 0, __const_10000_0 -__const_10000_post == 0, InCnt_0 -InCnt_post == 0, tmp___115_0 -X61 == 0, tmp___024_0 -X60 == 0, tmp___017_0 -X59 == 0, tmp___014_0 -X58 == 0, ent8_0 -X57 == 0, tabort4_0 -X56 == 0, seed2_0 -X55 == 0, ret_getbyte25_0 -X54 == 0, ent8_0 -X53 == 0, X52 == 0, rat26_0 -X51 == 0, r_off32_0 -X50 == 0, X49 == 0, X48 == 0, __const_9_0 -X47 == 0, n44_0 -X46 == 0, n40_0 -X45 == 0, maxmaxcode_0 -X44 == 0, maxcode_0 -X43 == 0, __const_16_0 -X42 == 0, m130_0 -X41 == 0, 1 + X40 == 0, -1 + X39 == 0, X38 == 0, i45_0 -X37 == 0, i41_0 -X36 == 0, i3_0 -X35 == 0, i29_0 -X34 == 0, __const_16_0 -i21_0 + X33 == 0, hsize_0 -X32 == 0, hsize___027_0 -X31 == 0, hsize_0 -X30 == 0, hsize_0 -X29 == 0, hshift11_0 -X28 == 0, free_ent_0 -X27 == 0, fcode5_0 -X26 == 0, exit_stat_0 -X25 == 0, ent8_0 -X24 == 0, disp9_0 -X23 == 0, __const_50_0 -X22 == 0, code31_0 -X21 == 0, X20 == 0, __const_10000_0 -X19 == 0, c7_0 -X18 == 0, -3 + X17 == 0, block_compress_0 -X16 == 0, bits33_0 -X15 == 0, apsim_bound11113_0 -X14 == 0, apsim_InCnt_0 -X13 == 0, __const_9_0 -X12 == 0, __const_8_0 -X11 == 0, __const_8388607_0 -X10 == 0, __const_65536_0 -X9 == 0, __const_53_0 -X8 == 0, __const_50_0 -X7 == 0, __const_429496_0 -X6 == 0, __const_257_0 -X5 == 0, __const_256_0 -X4 == 0, __const_2147483647_0 -X3 == 0, __const_16_0 -X2 == 0, __const_10000_0 -X1 == 0, InCnt_0 -X0 == 0, ent8_0 -tmp12_0 == 0, ent8_0 -ret_getbyte18_0 == 0, ratio_0 == 0, out_count_0 == 0, offset_0 == 0, __const_9_0 -n_bits_0 == 0, __const_16_0 -maxbits_0 == 0, 1 + m122_0 == 0, -1 + in_count_0 == 0, i6_0 == 0, hsize_0 -hsize_reg10_0 == 0, hsize_0 -hsize___019_0 == 0, __const_50_0 -count_0 == 0, clear_flg_0 == 0, __const_10000_0 -checkpoint_0 == 0, -3 + bytes_out_0 == 0, InCnt_0 -__const_50_0 + __const_53_0 -apsim_InCnt_0 >= 0, -__const_16_0 >= 0, __const_8_0 -hshift11_0 >= 0, -__const_65536_0 + fcode5_0 >= 0, -__const_53_0 + apsim_InCnt_0 + i3_0 >= 0, -__const_16_0 + i21_0 >= 0, -InCnt_0 + __const_50_0 >= 0 } Connected Subgraphs where we couldn't prove Termination: -------------------------------------------------------- SCC: +--transitions: t115,t8 +--nodes: l8,l9 SCC: +--transitions: t113,t84 +--nodes: l55,l56 SCC: +--transitions: t100,t101,t102,t103,t104,t105,t106,t107,t108,t109,t11,t110,t111,t112,t114,t116,t117,t119,t121,t20,t21,t25,t31,t37,t38,t40,t42,t43,t44,t45,t46,t47,t48,t49,t5,t51,t52,t53,t54,t55,t56,t57,t58,t59,t6,t60,t61,t62,t63,t64,t65,t66,t67,t68,t70,t71,t72,t73,t74,t75,t76,t77,t78,t79,t80,t81,t82,t85,t86,t87,t88,t89,t9,t90,t91,t92,t93,t94,t95,t96,t97,t98,t99 +--nodes: l1,l10,l11,l13,l14,l19,l20,l21,l22,l26,l27,l32,l35,l36,l37,l38,l39,l40,l41,l42,l43,l44,l45,l46,l47,l48,l49,l5,l50,l51,l52,l53,l54,l57,l58,l59,l6,l60,l61,l62,l63,l64,l65,l66,l67,l68,l69,l7,l70,l71 SCC: +--transitions: t2 +--nodes: l0,l2 method 1