NO

Solver Timeout: 4
Global Timeout: 300
No parsing errors!
Init Location: 0
Transitions:
<l0, l25, true>
<l1, l2, (0 <= (~(1) + x_9^0)) /\ (undef44 = (0 + t_589^0)) /\ (0 <= (~(1) + undef44)), par{t_11^0 -> undef44, t_15^0 -> (0 + t_582^0), x_9^0 -> (~(1) + x_9^0)}>
<l2, l3, (undef335 = undef335) /\ (undef178 = undef178) /\ (undef179 = undef179) /\ (undef336 = (0 + undef178)) /\ (undef337 = (0 + t_605^0)) /\ (0 <= ((~(1) + undef336) + (~(1) * undef337))) /\ (undef245 = (0 + t_613^0)) /\ (undef247 = (0 + t_617^0)) /\ (0 <= ((~(1) + undef245) + (~(1) * undef247))), par{nondet_18^0 -> undef178, nondet_19^0 -> undef179, t_15^0 -> undef245, t_17^0 -> undef247}>
<l4, l3, (undef505 = undef505) /\ (undef348 = undef348) /\ (undef349 = undef349) /\ (undef506 = (0 + undef348)) /\ (undef507 = (0 + t_360^0)) /\ (0 <= ((~(1) + undef506) + (~(1) * undef507))) /\ (undef415 = (0 + t_368^0)) /\ (undef417 = (0 + t_372^0)) /\ (0 <= ((~(1) + undef415) + (~(1) * undef417))), par{nondet_18^0 -> undef348, nondet_19^0 -> undef349, t_15^0 -> undef415, t_17^0 -> undef417}>
<l5, l6, (undef675 = undef675) /\ (undef646 = undef646) /\ (undef520 = undef520) /\ (undef521 = undef521) /\ (undef676 = (0 + undef520)) /\ (undef677 = (0 + t_708^0)) /\ (0 <= ((~(1) + undef676) + (~(1) * undef677))) /\ (undef585 = (0 + t_716^0)) /\ (undef587 = (0 + t_720^0)) /\ (0 <= ((~(1) + undef585) + (~(1) * undef587))), par{nondet_20^0 -> undef520, nondet_21^0 -> undef521, t_15^0 -> undef585, t_17^0 -> undef587, t_712^0 -> undef646}>
<l7, l6, (undef845 = undef845) /\ (undef679 = ((0 + (~(1) * t_11^0)) + t_436^0)) /\ (undef680 = (0 + t_436^0)) /\ (undef690 = undef690) /\ (undef691 = undef691) /\ (undef846 = (0 + undef690)) /\ (undef847 = (0 + t_459^0)) /\ (0 <= ((~(1) + undef846) + (~(1) * undef847))) /\ (undef755 = (0 + t_467^0)) /\ (undef757 = (0 + t_471^0)) /\ (0 <= ((~(1) + undef755) + (~(1) * undef757))), par{___patmp1^0 -> undef679, ___patmp2^0 -> undef680, nondet_20^0 -> undef690, nondet_21^0 -> undef691, t_15^0 -> undef755, t_17^0 -> undef757, t_684^0 -> (0 + undef680), t_712^0 -> (0 + undef679)}>
<l8, l9, (undef897 = undef897) /\ (undef898 = undef898) /\ (undef1016 = (0 + t_1193^0)) /\ ((1 + (~(1) * undef1016)) <= 0) /\ (undef1017 = (0 + t_1238^0)) /\ (undef1018 = (~(1) + undef897)) /\ (undef891 = (0 + undef898)) /\ ((0 + undef891) <= 0) /\ (undef1015 = undef1015) /\ (undef900 = undef900) /\ (undef860 = undef860) /\ (undef861 = undef861) /\ (undef1019 = (0 + undef860)) /\ (undef1020 = (0 + t_1267^0)) /\ (0 <= ((~(1) + undef1019) + (~(1) * undef1020))) /\ (undef925 = (0 + t_1275^0)) /\ (undef927 = (0 + t_1279^0)) /\ (0 <= ((~(1) + undef925) + (~(1) * undef927))), par{nondet_20^0 -> undef860, nondet_21^0 -> undef861, t_11^0 -> undef891, t_1245^0 -> undef897, t_1252^0 -> undef898, t_1271^0 -> undef900, t_15^0 -> undef925, t_17^0 -> undef927}>
<l8, l10, (undef1065 = undef1065) /\ (undef1188 = (0 + t_1193^0)) /\ (0 <= (0 + (~(1) * undef1188))) /\ (undef1189 = (0 + t_1197^0)) /\ (undef1064 = (0 + undef1065)) /\ ((0 + undef1064) <= 0) /\ (undef1037 = undef1037) /\ (undef1038 = undef1038) /\ (undef1190 = (0 + undef1037)) /\ (undef1191 = (0 + t_1219^0)) /\ (0 <= ((~(1) + undef1190) + (~(1) * undef1191))) /\ (undef1098 = (0 + t_1227^0)) /\ (undef1100 = (0 + t_1231^0)) /\ (0 <= ((~(1) + undef1098) + (~(1) * undef1100))), par{nondet_19^0 -> (0 + nondet_30^0), nondet_29^0 -> undef1037, nondet_30^0 -> undef1038, t_11^0 -> undef1064, t_1204^0 -> undef1065, t_15^0 -> undef1098, t_17^0 -> undef1100}>
<l10, l8, true>
<l11, l12, (undef1442 = undef1442) /\ (undef1527 = (0 + t_148^0)) /\ ((1 + (~(1) * undef1527)) <= 0) /\ (undef1528 = (0 + t_193^0)) /\ (undef1529 = (~(1) + undef1442)) /\ (undef1402 = (0 + t_207^0)) /\ (0 <= (~(1) + undef1402)) /\ (undef1526 = undef1526) /\ (undef1445 = undef1445) /\ (undef1371 = undef1371) /\ (undef1372 = undef1372) /\ (undef1530 = (0 + undef1371)) /\ (undef1531 = (0 + t_222^0)) /\ (0 <= ((~(1) + undef1530) + (~(1) * undef1531))) /\ (undef1436 = (0 + t_230^0)) /\ (undef1438 = (0 + t_234^0)) /\ (0 <= ((~(1) + undef1436) + (~(1) * undef1438))), par{nondet_20^0 -> undef1371, nondet_21^0 -> undef1372, t_11^0 -> undef1402, t_15^0 -> undef1436, t_17^0 -> undef1438, t_200^0 -> undef1442, t_226^0 -> undef1445}>
<l11, l13, (undef1699 = (0 + t_148^0)) /\ (0 <= (0 + (~(1) * undef1699))) /\ (undef1700 = (0 + t_152^0)) /\ (undef1575 = (0 + t_159^0)) /\ (0 <= (~(1) + undef1575)) /\ (undef1548 = undef1548) /\ (undef1549 = undef1549) /\ (undef1701 = (0 + undef1548)) /\ (undef1702 = (0 + t_174^0)) /\ (0 <= ((~(1) + undef1701) + (~(1) * undef1702))) /\ (undef1609 = (0 + t_182^0)) /\ (undef1611 = (0 + t_186^0)) /\ (0 <= ((~(1) + undef1609) + (~(1) * undef1611))), par{nondet_19^0 -> (0 + nondet_30^0), nondet_29^0 -> undef1548, nondet_30^0 -> undef1549, t_11^0 -> undef1575, t_15^0 -> undef1609, t_17^0 -> undef1611}>
<l13, l11, true>
<l3, l5, (undef2005 = undef2005) /\ (undef2037 = (0 + t_630^0)) /\ ((1 + (~(1) * undef2037)) <= 0) /\ (undef2038 = (0 + t_677^0)) /\ (undef1913 = (0 + t_691^0)) /\ (0 <= (~(1) + undef1913)), par{t_11^0 -> undef1913, t_15^0 -> (~(1) + undef2005), t_684^0 -> undef2005}>
<l3, l14, (undef2206 = (0 + t_630^0)) /\ (0 <= (0 + (~(1) * undef2206))) /\ (undef2082 = (0 + t_641^0)) /\ (0 <= (~(1) + undef2082)), par{t_11^0 -> undef2082, t_15^0 -> (0 + t_634^0)}>
<l15, l5, (undef2374 = (0 + t_383^0)) /\ ((1 + (~(1) * undef2374)) <= 0) /\ (undef2375 = (0 + t_429^0)) /\ (undef2250 = (0 + t_443^0)) /\ (0 <= (~(1) + undef2250)), par{t_11^0 -> undef2250, t_15^0 -> (~(1) + t_436^0), t_684^0 -> (0 + t_436^0)}>
<l15, l14, (undef2543 = (0 + t_383^0)) /\ (0 <= (0 + (~(1) * undef2543))) /\ (undef2419 = (0 + t_394^0)) /\ (0 <= (~(1) + undef2419)), par{t_11^0 -> undef2419, t_15^0 -> (0 + t_387^0)}>
<l16, l1, (undef2711 = undef2711) /\ (undef2688 = undef2688) /\ (undef2558 = undef2558) /\ (undef2559 = undef2559) /\ (undef2712 = (0 + undef2558)) /\ (undef2714 = (0 + t_756^0)) /\ (0 <= ((~(1) + undef2712) + (~(1) * undef2714))) /\ (undef2713 = (0 + t_764^0)) /\ (undef2623 = (0 + t_768^0)) /\ (0 <= ((~(1) + undef2713) + (~(1) * undef2623))) /\ (0 <= (~(1) + x_9^0)) /\ (undef2621 = undef2621) /\ (0 <= ((~(1) + undef2621) + (~(1) * t_806^0))) /\ (0 <= ((~(1) + t_814^0) + (~(1) * t_818^0))), par{nondet_22^0 -> undef2558, nondet_23^0 -> undef2559, t_15^0 -> undef2621, t_17^0 -> undef2623, t_760^0 -> undef2688}>
<l14, l3, (undef2731 = undef2731) /\ (undef2732 = undef2732) /\ (undef2882 = (0 + undef2731)) /\ (undef2883 = (0 + t_658^0)) /\ (0 <= ((~(1) + undef2882) + (~(1) * undef2883))) /\ (undef2792 = (0 + t_666^0)) /\ (undef2794 = (0 + t_670^0)) /\ (0 <= ((~(1) + undef2792) + (~(1) * undef2794))), par{nondet_19^0 -> (0 + nondet_30^0), nondet_29^0 -> undef2731, nondet_30^0 -> undef2732, t_15^0 -> undef2792, t_17^0 -> undef2794}>
<l17, l1, (undef3051 = undef3051) /\ (undef3001 = undef3001) /\ (undef2898 = undef2898) /\ (undef2899 = undef2899) /\ (undef3052 = (0 + undef2898)) /\ (undef3054 = (0 + t_505^0)) /\ (0 <= ((~(1) + undef3052) + (~(1) * undef3054))) /\ (undef3053 = (0 + t_513^0)) /\ (undef2963 = (0 + t_517^0)) /\ (0 <= ((~(1) + undef3053) + (~(1) * undef2963))) /\ (0 <= (~(1) + x_9^0)) /\ (undef2961 = undef2961) /\ (0 <= ((~(1) + undef2961) + (~(1) * t_554^0))) /\ (0 <= ((~(1) + t_562^0) + (~(1) * t_566^0))), par{nondet_22^0 -> undef2898, nondet_23^0 -> undef2899, t_15^0 -> undef2961, t_17^0 -> undef2963, t_509^0 -> undef3001}>
<l18, l3, (undef3071 = undef3071) /\ (undef3072 = undef3072) /\ (undef3222 = (0 + undef3071)) /\ (undef3223 = (0 + t_410^0)) /\ (0 <= ((~(1) + undef3222) + (~(1) * undef3223))) /\ (undef3132 = (0 + t_418^0)) /\ (undef3134 = (0 + t_422^0)) /\ (0 <= ((~(1) + undef3132) + (~(1) * undef3134))), par{nondet_19^0 -> (0 + nondet_30^0), nondet_29^0 -> undef3071, nondet_30^0 -> undef3072, t_15^0 -> undef3132, t_17^0 -> undef3134}>
<l9, l1, (undef3281 = undef3281) /\ (undef3392 = (0 + t_1292^0)) /\ (undef3267 = (0 + x_9^0)) /\ (0 <= (~(1) + undef3267)) /\ (undef3391 = undef3391) /\ (undef3283 = undef3283) /\ (undef3238 = undef3238) /\ (undef3239 = undef3239) /\ (undef3393 = (0 + undef3238)) /\ (undef3395 = (0 + t_1320^0)) /\ (0 <= ((~(1) + undef3393) + (~(1) * undef3395))) /\ (undef3394 = (0 + t_1328^0)) /\ (undef3303 = (0 + t_1332^0)) /\ (0 <= ((~(1) + undef3394) + (~(1) * undef3303))) /\ (0 <= (~(1) + x_9^0)) /\ (undef3301 = undef3301) /\ (0 <= ((~(1) + (~(1) * t_1374^0)) + undef3301)) /\ (0 <= ((~(1) + t_1382^0) + (~(1) * t_1386^0))), par{nondet_22^0 -> undef3238, nondet_23^0 -> undef3239, t_11^0 -> undef3267, t_1299^0 -> undef3281, t_1324^0 -> undef3283, t_15^0 -> undef3301, t_17^0 -> undef3303}>
<l9, l19, (undef3453 = undef3453) /\ (undef3564 = (0 + t_1292^0)) /\ (undef3439 = (0 + x_9^0)) /\ ((0 + undef3439) <= 0) /\ (undef3563 = undef3563) /\ (undef3464 = undef3464) /\ (undef3410 = undef3410) /\ (undef3411 = undef3411) /\ (undef3565 = (0 + undef3410)) /\ (undef3567 = (0 + t_1412^0)) /\ (0 <= ((~(1) + undef3565) + (~(1) * undef3567))) /\ (undef3566 = (0 + t_1420^0)) /\ (undef3475 = (0 + t_1424^0)) /\ (0 <= ((~(1) + undef3566) + (~(1) * undef3475))) /\ ((0 + x_9^0) <= 0) /\ (undef3473 = undef3473) /\ (0 <= ((~(1) + (~(1) * t_1470^0)) + undef3473)) /\ (0 <= ((~(1) + t_1478^0) + (~(1) * t_1482^0))), par{nondet_22^0 -> undef3410, nondet_23^0 -> undef3411, t_11^0 -> undef3439, t_1299^0 -> undef3453, t_1416^0 -> undef3464, t_15^0 -> undef3473, t_17^0 -> undef3475}>
<l6, l16, (undef3710 = undef3710) /\ (undef3611 = (0 + x_9^0)) /\ (0 <= (~(1) + undef3611)), par{t_11^0 -> undef3611, t_15^0 -> (0 + t_732^0), t_739^0 -> undef3710}>
<l6, l19, (undef3877 = undef3877) /\ (undef3903 = (0 + t_732^0)) /\ (undef3778 = (0 + x_9^0)) /\ ((0 + undef3778) <= 0) /\ (undef3902 = undef3902) /\ (undef3886 = undef3886) /\ (undef3749 = undef3749) /\ (undef3750 = undef3750) /\ (undef3904 = (0 + undef3749)) /\ (undef3906 = (0 + t_840^0)) /\ (0 <= ((~(1) + undef3904) + (~(1) * undef3906))) /\ (undef3905 = (0 + t_848^0)) /\ (undef3814 = (0 + t_852^0)) /\ (0 <= ((~(1) + undef3905) + (~(1) * undef3814))) /\ (0 <= (~(1) + x_9^0)) /\ (undef3812 = undef3812) /\ (0 <= ((~(1) + undef3812) + (~(1) * t_894^0))) /\ (0 <= ((~(1) + t_902^0) + (~(1) * t_906^0))), par{nondet_22^0 -> undef3749, nondet_23^0 -> undef3750, t_11^0 -> undef3778, t_15^0 -> undef3812, t_17^0 -> undef3814, t_739^0 -> undef3877, t_844^0 -> undef3886}>
<l20, l16, (undef3908 = (0 + t_489^0)) /\ (undef3909 = ((0 + t_436^0) + (~(1) * x_9^0))) /\ (undef3910 = (0 + t_436^0)) /\ (undef3950 = (0 + x_9^0)) /\ (0 <= (~(1) + undef3950)), par{___patmp1^0 -> undef3908, ___patmp2^0 -> undef3909, ___patmp3^0 -> undef3910, t_11^0 -> undef3950, t_15^0 -> (0 + t_482^0), t_684^0 -> (0 + undef3910), t_712^0 -> (0 + undef3909), t_739^0 -> (0 + undef3908)}>
<l20, l19, (undef4189 = undef4189) /\ (undef4242 = (0 + t_482^0)) /\ (undef4117 = (0 + x_9^0)) /\ ((0 + undef4117) <= 0) /\ (undef4241 = undef4241) /\ (undef4234 = undef4234) /\ (undef4088 = undef4088) /\ (undef4089 = undef4089) /\ (undef4243 = (0 + undef4088)) /\ (undef4245 = (0 + t_942^0)) /\ (0 <= ((~(1) + undef4243) + (~(1) * undef4245))) /\ (undef4244 = (0 + t_950^0)) /\ (undef4153 = (0 + t_954^0)) /\ (0 <= ((~(1) + undef4244) + (~(1) * undef4153))) /\ ((0 + x_9^0) <= 0) /\ (undef4151 = undef4151) /\ (0 <= ((~(1) + undef4151) + (~(1) * t_997^0))) /\ (0 <= ((~(1) + t_1005^0) + (~(1) * t_1009^0))), par{nondet_22^0 -> undef4088, nondet_23^0 -> undef4089, t_11^0 -> undef4117, t_15^0 -> undef4151, t_17^0 -> undef4153, t_489^0 -> undef4189, t_946^0 -> undef4234}>
<l12, l16, (undef4247 = (0 + temp118_31^0)) /\ (undef4248 = ((0 + t_200^0) + (~(1) * x_9^0))) /\ (undef4249 = (0 + t_200^0)) /\ (undef4289 = (0 + x_9^0)) /\ (0 <= (~(1) + undef4289)), par{___patmp1^0 -> undef4247, ___patmp2^0 -> undef4248, ___patmp3^0 -> undef4249, t_11^0 -> undef4289, t_15^0 -> (0 + t_244^0), t_684^0 -> (0 + undef4249), t_712^0 -> (0 + undef4248), t_739^0 -> (0 + undef4247)}>
<l12, l19, (undef4503 = undef4503) /\ (undef4581 = (0 + t_244^0)) /\ (undef4456 = (0 + x_9^0)) /\ ((0 + undef4456) <= 0) /\ (undef4580 = undef4580) /\ (undef4438 = undef4438) /\ (undef4427 = undef4427) /\ (undef4428 = undef4428) /\ (undef4582 = (0 + undef4427)) /\ (undef4584 = (0 + t_1035^0)) /\ (0 <= ((~(1) + undef4582) + (~(1) * undef4584))) /\ (undef4583 = (0 + t_1043^0)) /\ (undef4492 = (0 + t_1047^0)) /\ (0 <= ((~(1) + undef4583) + (~(1) * undef4492))) /\ ((0 + x_9^0) <= 0) /\ (undef4490 = undef4490) /\ (0 <= ((~(1) + (~(1) * t_1091^0)) + undef4490)) /\ (0 <= ((~(1) + t_1099^0) + (~(1) * t_1103^0))), par{nondet_22^0 -> undef4427, nondet_23^0 -> undef4428, t_1039^0 -> undef4438, t_11^0 -> undef4456, t_15^0 -> undef4490, t_17^0 -> undef4492, t_251^0 -> undef4503}>
<l21, l11, (undef4606 = undef4606) /\ (undef4589 = undef4589) /\ (undef4591 = undef4591) /\ (undef4592 = undef4592) /\ (undef4605 = undef4605) /\ (undef4603 = undef4603) /\ (undef4750 = (0 + undef4603)) /\ (undef4763 = (0 + undef4750)) /\ (undef4604 = undef4604) /\ (0 <= (~(1) + undef4763)) /\ (undef4755 = (0 + cnt_58^0)) /\ (undef4754 = (0 + undef4604)) /\ (0 <= (~(1) + undef4754)) /\ (undef4752 = undef4752) /\ (undef4593 = undef4593) /\ (undef4594 = undef4594) /\ (undef4756 = (0 + undef4593)) /\ (undef4760 = (0 + t_84^0)) /\ (0 <= ((~(1) + undef4756) + (~(1) * undef4760))) /\ (undef4757 = (0 + t_92^0)) /\ (undef4761 = (0 + t_96^0)) /\ (0 <= ((~(1) + undef4757) + (~(1) * undef4761))) /\ (0 <= (~(1) + undef4763)) /\ (undef4758 = (0 + t_105^0)) /\ (undef4628 = (0 + t_112^0)) /\ (0 <= (~(1) + undef4628)) /\ (undef4753 = undef4753) /\ (undef4595 = undef4595) /\ (undef4596 = undef4596) /\ (undef4759 = (0 + undef4595)) /\ (undef4762 = (0 + t_127^0)) /\ (0 <= ((~(1) + undef4759) + (~(1) * undef4762))) /\ (undef4662 = (0 + t_135^0)) /\ (undef4664 = (0 + t_139^0)) /\ (0 <= ((~(1) + undef4662) + (~(1) * undef4664))), par{b_10^0 -> undef4589, e_14^0 -> undef4591, f_27^0 -> undef4592, nondet_12^0 -> undef4593, nondet_13^0 -> undef4594, nondet_18^0 -> undef4595, nondet_19^0 -> undef4596, nondet_7^0 -> undef4603, nondet_8^0 -> undef4604, olde_16^0 -> undef4605, qCns_26^0 -> undef4606, t_11^0 -> undef4628, t_15^0 -> undef4662, t_17^0 -> undef4664, temp118_31^0 -> undef4750, x_9^0 -> (~(1) + undef4763)}>
<l21, l8, (undef4933 = undef4933) /\ (undef4785 = undef4785) /\ (undef4768 = undef4768) /\ (undef4770 = undef4770) /\ (undef4771 = undef4771) /\ (undef4784 = undef4784) /\ (undef4782 = undef4782) /\ (undef4929 = (0 + undef4782)) /\ (undef4943 = (0 + undef4929)) /\ (undef4783 = undef4783) /\ (0 <= (~(1) + undef4943)) /\ (undef4935 = (0 + cnt_58^0)) /\ (undef4934 = (0 + undef4783)) /\ ((0 + undef4934) <= 0) /\ (undef4931 = undef4931) /\ (undef4772 = undef4772) /\ (undef4773 = undef4773) /\ (undef4936 = (0 + undef4772)) /\ (undef4940 = (0 + t_1122^0)) /\ (0 <= ((~(1) + undef4936) + (~(1) * undef4940))) /\ (undef4937 = (0 + t_1130^0)) /\ (undef4941 = (0 + t_1134^0)) /\ (0 <= ((~(1) + undef4937) + (~(1) * undef4941))) /\ (undef4801 = undef4801) /\ (0 <= (~(1) + undef4943)) /\ (undef4938 = (0 + t_1146^0)) /\ (undef4807 = (0 + undef4801)) /\ ((0 + undef4807) <= 0) /\ (undef4932 = undef4932) /\ (undef4774 = undef4774) /\ (undef4775 = undef4775) /\ (undef4939 = (0 + undef4774)) /\ (undef4942 = (0 + t_1166^0)) /\ (0 <= ((~(1) + undef4939) + (~(1) * undef4942))) /\ (undef4841 = (0 + t_1174^0)) /\ (undef4843 = (0 + t_1178^0)) /\ (0 <= ((~(1) + undef4841) + (~(1) * undef4843))), par{b_10^0 -> undef4768, e_14^0 -> undef4770, f_27^0 -> undef4771, nondet_12^0 -> undef4772, nondet_13^0 -> undef4773, nondet_18^0 -> undef4774, nondet_19^0 -> undef4775, nondet_7^0 -> undef4782, nondet_8^0 -> undef4783, olde_16^0 -> undef4784, qCns_26^0 -> undef4785, t_1153^0 -> undef4801, t_11^0 -> undef4807, t_15^0 -> undef4841, t_17^0 -> undef4843, temp118_31^0 -> undef4929, x_9^0 -> (~(1) + undef4943)}>
<l19, l22, (undef5110 = undef5110) /\ (undef5021 = undef5021) /\ (undef5023 = undef5023) /\ ((0 + undef5110) <= 0) /\ (undef4944 = undef4944), par{Result_6^0 -> undef4944, t_15^0 -> undef5021, t_17^0 -> undef5023, x_9^0 -> undef5110}>
<l23, l2, (0 <= (~(1) + x_9^0)) /\ (undef5154 = (0 + t_345^0)) /\ (0 <= (~(1) + undef5154)), par{t_11^0 -> undef5154, t_15^0 -> (0 + t_338^0), x_9^0 -> (~(1) + x_9^0)}>
<l24, l1, (undef5445 = undef5445) /\ (0 <= ((~(1) + undef5445) + (~(1) * t_266^0))) /\ (0 <= ((~(1) + t_274^0) + (~(1) * t_278^0))) /\ (0 <= (~(1) + x_9^0)) /\ (undef5355 = undef5355) /\ (0 <= ((~(1) + undef5355) + (~(1) * t_314^0))) /\ (0 <= ((~(1) + t_322^0) + (~(1) * t_326^0))), par{t_15^0 -> undef5355}>
<l25, l21, true>

Fresh variables:
undef44, undef178, undef179, undef245, undef247, undef335, undef336, undef337, undef348, undef349, undef415, undef417, undef505, undef506, undef507, undef520, undef521, undef585, undef587, undef646, undef675, undef676, undef677, undef679, undef680, undef690, undef691, undef755, undef757, undef845, undef846, undef847, undef860, undef861, undef891, undef897, undef898, undef900, undef925, undef927, undef1015, undef1016, undef1017, undef1018, undef1019, undef1020, undef1037, undef1038, undef1064, undef1065, undef1098, undef1100, undef1188, undef1189, undef1190, undef1191, undef1371, undef1372, undef1402, undef1436, undef1438, undef1442, undef1445, undef1526, undef1527, undef1528, undef1529, undef1530, undef1531, undef1548, undef1549, undef1575, undef1609, undef1611, undef1699, undef1700, undef1701, undef1702, undef1913, undef2005, undef2037, undef2038, undef2082, undef2206, undef2250, undef2374, undef2375, undef2419, undef2543, undef2558, undef2559, undef2621, undef2623, undef2688, undef2711, undef2712, undef2713, undef2714, undef2731, undef2732, undef2792, undef2794, undef2882, undef2883, undef2898, undef2899, undef2961, undef2963, undef3001, undef3051, undef3052, undef3053, undef3054, undef3071, undef3072, undef3132, undef3134, undef3222, undef3223, undef3238, undef3239, undef3267, undef3281, undef3283, undef3301, undef3303, undef3391, undef3392, undef3393, undef3394, undef3395, undef3410, undef3411, undef3439, undef3453, undef3464, undef3473, undef3475, undef3563, undef3564, undef3565, undef3566, undef3567, undef3611, undef3710, undef3749, undef3750, undef3778, undef3812, undef3814, undef3877, undef3886, undef3902, undef3903, undef3904, undef3905, undef3906, undef3908, undef3909, undef3910, undef3950, undef4088, undef4089, undef4117, undef4151, undef4153, undef4189, undef4234, undef4241, undef4242, undef4243, undef4244, undef4245, undef4247, undef4248, undef4249, undef4289, undef4427, undef4428, undef4438, undef4456, undef4490, undef4492, undef4503, undef4580, undef4581, undef4582, undef4583, undef4584, undef4589, undef4591, undef4592, undef4593, undef4594, undef4595, undef4596, undef4603, undef4604, undef4605, undef4606, undef4628, undef4662, undef4664, undef4750, undef4752, undef4753, undef4754, undef4755, undef4756, undef4757, undef4758, undef4759, undef4760, undef4761, undef4762, undef4763, undef4768, undef4770, undef4771, undef4772, undef4773, undef4774, undef4775, undef4782, undef4783, undef4784, undef4785, undef4801, undef4807, undef4841, undef4843, undef4929, undef4931, undef4932, undef4933, undef4934, undef4935, undef4936, undef4937, undef4938, undef4939, undef4940, undef4941, undef4942, undef4943, undef4944, undef5021, undef5023, undef5110, undef5154, undef5355, undef5445, 

Undef variables:
undef44, undef178, undef179, undef245, undef247, undef335, undef336, undef337, undef348, undef349, undef415, undef417, undef505, undef506, undef507, undef520, undef521, undef585, undef587, undef646, undef675, undef676, undef677, undef679, undef680, undef690, undef691, undef755, undef757, undef845, undef846, undef847, undef860, undef861, undef891, undef897, undef898, undef900, undef925, undef927, undef1015, undef1016, undef1017, undef1018, undef1019, undef1020, undef1037, undef1038, undef1064, undef1065, undef1098, undef1100, undef1188, undef1189, undef1190, undef1191, undef1371, undef1372, undef1402, undef1436, undef1438, undef1442, undef1445, undef1526, undef1527, undef1528, undef1529, undef1530, undef1531, undef1548, undef1549, undef1575, undef1609, undef1611, undef1699, undef1700, undef1701, undef1702, undef1913, undef2005, undef2037, undef2038, undef2082, undef2206, undef2250, undef2374, undef2375, undef2419, undef2543, undef2558, undef2559, undef2621, undef2623, undef2688, undef2711, undef2712, undef2713, undef2714, undef2731, undef2732, undef2792, undef2794, undef2882, undef2883, undef2898, undef2899, undef2961, undef2963, undef3001, undef3051, undef3052, undef3053, undef3054, undef3071, undef3072, undef3132, undef3134, undef3222, undef3223, undef3238, undef3239, undef3267, undef3281, undef3283, undef3301, undef3303, undef3391, undef3392, undef3393, undef3394, undef3395, undef3410, undef3411, undef3439, undef3453, undef3464, undef3473, undef3475, undef3563, undef3564, undef3565, undef3566, undef3567, undef3611, undef3710, undef3749, undef3750, undef3778, undef3812, undef3814, undef3877, undef3886, undef3902, undef3903, undef3904, undef3905, undef3906, undef3908, undef3909, undef3910, undef3950, undef4088, undef4089, undef4117, undef4151, undef4153, undef4189, undef4234, undef4241, undef4242, undef4243, undef4244, undef4245, undef4247, undef4248, undef4249, undef4289, undef4427, undef4428, undef4438, undef4456, undef4490, undef4492, undef4503, undef4580, undef4581, undef4582, undef4583, undef4584, undef4589, undef4591, undef4592, undef4593, undef4594, undef4595, undef4596, undef4603, undef4604, undef4605, undef4606, undef4628, undef4662, undef4664, undef4750, undef4752, undef4753, undef4754, undef4755, undef4756, undef4757, undef4758, undef4759, undef4760, undef4761, undef4762, undef4763, undef4768, undef4770, undef4771, undef4772, undef4773, undef4774, undef4775, undef4782, undef4783, undef4784, undef4785, undef4801, undef4807, undef4841, undef4843, undef4929, undef4931, undef4932, undef4933, undef4934, undef4935, undef4936, undef4937, undef4938, undef4939, undef4940, undef4941, undef4942, undef4943, undef4944, undef5021, undef5023, undef5110, undef5154, undef5355, undef5445, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

Preprocessed LLVMGraph
Init Location: 0
Transitions:
<l0, l11, (undef4606 = undef4606) /\ (undef4589 = undef4589) /\ (undef4591 = undef4591) /\ (undef4592 = undef4592) /\ (undef4605 = undef4605) /\ (undef4603 = undef4603) /\ (undef4750 = (0 + undef4603)) /\ (undef4763 = (0 + undef4750)) /\ (undef4604 = undef4604) /\ (0 <= (~(1) + undef4763)) /\ (undef4755 = (0 + cnt_58^0)) /\ (undef4754 = (0 + undef4604)) /\ (0 <= (~(1) + undef4754)) /\ (undef4752 = undef4752) /\ (undef4593 = undef4593) /\ (undef4594 = undef4594) /\ (undef4756 = (0 + undef4593)) /\ (undef4760 = (0 + t_84^0)) /\ (0 <= ((~(1) + undef4756) + (~(1) * undef4760))) /\ (undef4757 = (0 + t_92^0)) /\ (undef4761 = (0 + t_96^0)) /\ (0 <= ((~(1) + undef4757) + (~(1) * undef4761))) /\ (0 <= (~(1) + undef4763)) /\ (undef4758 = (0 + t_105^0)) /\ (undef4628 = (0 + t_112^0)) /\ (0 <= (~(1) + undef4628)) /\ (undef4753 = undef4753) /\ (undef4595 = undef4595) /\ (undef4596 = undef4596) /\ (undef4759 = (0 + undef4595)) /\ (undef4762 = (0 + t_127^0)) /\ (0 <= ((~(1) + undef4759) + (~(1) * undef4762))) /\ (undef4662 = (0 + t_135^0)) /\ (undef4664 = (0 + t_139^0)) /\ (0 <= ((~(1) + undef4662) + (~(1) * undef4664))), par{t_11^0 -> undef4628, temp118_31^0 -> undef4750, x_9^0 -> (~(1) + undef4763)}>
<l0, l8, (undef4933 = undef4933) /\ (undef4785 = undef4785) /\ (undef4768 = undef4768) /\ (undef4770 = undef4770) /\ (undef4771 = undef4771) /\ (undef4784 = undef4784) /\ (undef4782 = undef4782) /\ (undef4929 = (0 + undef4782)) /\ (undef4943 = (0 + undef4929)) /\ (undef4783 = undef4783) /\ (0 <= (~(1) + undef4943)) /\ (undef4935 = (0 + cnt_58^0)) /\ (undef4934 = (0 + undef4783)) /\ ((0 + undef4934) <= 0) /\ (undef4931 = undef4931) /\ (undef4772 = undef4772) /\ (undef4773 = undef4773) /\ (undef4936 = (0 + undef4772)) /\ (undef4940 = (0 + t_1122^0)) /\ (0 <= ((~(1) + undef4936) + (~(1) * undef4940))) /\ (undef4937 = (0 + t_1130^0)) /\ (undef4941 = (0 + t_1134^0)) /\ (0 <= ((~(1) + undef4937) + (~(1) * undef4941))) /\ (undef4801 = undef4801) /\ (0 <= (~(1) + undef4943)) /\ (undef4938 = (0 + t_1146^0)) /\ (undef4807 = (0 + undef4801)) /\ ((0 + undef4807) <= 0) /\ (undef4932 = undef4932) /\ (undef4774 = undef4774) /\ (undef4775 = undef4775) /\ (undef4939 = (0 + undef4774)) /\ (undef4942 = (0 + t_1166^0)) /\ (0 <= ((~(1) + undef4939) + (~(1) * undef4942))) /\ (undef4841 = (0 + t_1174^0)) /\ (undef4843 = (0 + t_1178^0)) /\ (0 <= ((~(1) + undef4841) + (~(1) * undef4843))), par{t_11^0 -> undef4807, temp118_31^0 -> undef4929, x_9^0 -> (~(1) + undef4943)}>
<l3, l3, (undef2005 = undef2005) /\ (undef2037 = (0 + t_630^0)) /\ ((1 + (~(1) * undef2037)) <= 0) /\ (undef2038 = (0 + t_677^0)) /\ (undef1913 = (0 + t_691^0)) /\ (0 <= (~(1) + undef1913)) /\ (undef675 = undef675) /\ (undef646 = undef646) /\ (undef520 = undef520) /\ (undef521 = undef521) /\ (undef676 = (0 + undef520)) /\ (undef677 = (0 + t_708^0)) /\ (0 <= ((~(1) + undef676) + (~(1) * undef677))) /\ (undef585 = (0 + t_716^0)) /\ (undef587 = (0 + t_720^0)) /\ (0 <= ((~(1) + undef585) + (~(1) * undef587))) /\ (undef3710 = undef3710) /\ (undef3611 = (0 + x_9^0)) /\ (0 <= (~(1) + undef3611)) /\ (undef2711 = undef2711) /\ (undef2688 = undef2688) /\ (undef2558 = undef2558) /\ (undef2559 = undef2559) /\ (undef2712 = (0 + undef2558)) /\ (undef2714 = (0 + t_756^0)) /\ (0 <= ((~(1) + undef2712) + (~(1) * undef2714))) /\ (undef2713 = (0 + t_764^0)) /\ (undef2623 = (0 + t_768^0)) /\ (0 <= ((~(1) + undef2713) + (~(1) * undef2623))) /\ (0 <= (~(1) + x_9^0)) /\ (undef2621 = undef2621) /\ (0 <= ((~(1) + undef2621) + (~(1) * t_806^0))) /\ (0 <= ((~(1) + t_814^0) + (~(1) * t_818^0))) /\ (0 <= (~(1) + x_9^0)) /\ (undef44 = (0 + t_589^0)) /\ (0 <= (~(1) + undef44)) /\ (undef335 = undef335) /\ (undef178 = undef178) /\ (undef179 = undef179) /\ (undef336 = (0 + undef178)) /\ (undef337 = (0 + t_605^0)) /\ (0 <= ((~(1) + undef336) + (~(1) * undef337))) /\ (undef245 = (0 + t_613^0)) /\ (undef247 = (0 + t_617^0)) /\ (0 <= ((~(1) + undef245) + (~(1) * undef247))), par{t_11^0 -> undef44, x_9^0 -> (~(1) + x_9^0)}>
<l3, l3, (undef2206 = (0 + t_630^0)) /\ (0 <= (0 + (~(1) * undef2206))) /\ (undef2082 = (0 + t_641^0)) /\ (0 <= (~(1) + undef2082)) /\ (undef2731 = undef2731) /\ (undef2732 = undef2732) /\ (undef2882 = (0 + undef2731)) /\ (undef2883 = (0 + t_658^0)) /\ (0 <= ((~(1) + undef2882) + (~(1) * undef2883))) /\ (undef2792 = (0 + t_666^0)) /\ (undef2794 = (0 + t_670^0)) /\ (0 <= ((~(1) + undef2792) + (~(1) * undef2794))), par{nondet_30^0 -> undef2732, t_11^0 -> undef2082}>
<l8, l3, (undef897 = undef897) /\ (undef898 = undef898) /\ (undef1016 = (0 + t_1193^0)) /\ ((1 + (~(1) * undef1016)) <= 0) /\ (undef1017 = (0 + t_1238^0)) /\ (undef1018 = (~(1) + undef897)) /\ (undef891 = (0 + undef898)) /\ ((0 + undef891) <= 0) /\ (undef1015 = undef1015) /\ (undef900 = undef900) /\ (undef860 = undef860) /\ (undef861 = undef861) /\ (undef1019 = (0 + undef860)) /\ (undef1020 = (0 + t_1267^0)) /\ (0 <= ((~(1) + undef1019) + (~(1) * undef1020))) /\ (undef925 = (0 + t_1275^0)) /\ (undef927 = (0 + t_1279^0)) /\ (0 <= ((~(1) + undef925) + (~(1) * undef927))) /\ (undef3281 = undef3281) /\ (undef3392 = (0 + t_1292^0)) /\ (undef3267 = (0 + x_9^0)) /\ (0 <= (~(1) + undef3267)) /\ (undef3391 = undef3391) /\ (undef3283 = undef3283) /\ (undef3238 = undef3238) /\ (undef3239 = undef3239) /\ (undef3393 = (0 + undef3238)) /\ (undef3395 = (0 + t_1320^0)) /\ (0 <= ((~(1) + undef3393) + (~(1) * undef3395))) /\ (undef3394 = (0 + t_1328^0)) /\ (undef3303 = (0 + t_1332^0)) /\ (0 <= ((~(1) + undef3394) + (~(1) * undef3303))) /\ (0 <= (~(1) + x_9^0)) /\ (undef3301 = undef3301) /\ (0 <= ((~(1) + (~(1) * t_1374^0)) + undef3301)) /\ (0 <= ((~(1) + t_1382^0) + (~(1) * t_1386^0))) /\ (0 <= (~(1) + x_9^0)) /\ (undef44 = (0 + t_589^0)) /\ (0 <= (~(1) + undef44)) /\ (undef335 = undef335) /\ (undef178 = undef178) /\ (undef179 = undef179) /\ (undef336 = (0 + undef178)) /\ (undef337 = (0 + t_605^0)) /\ (0 <= ((~(1) + undef336) + (~(1) * undef337))) /\ (undef245 = (0 + t_613^0)) /\ (undef247 = (0 + t_617^0)) /\ (0 <= ((~(1) + undef245) + (~(1) * undef247))), par{t_11^0 -> undef44, x_9^0 -> (~(1) + x_9^0)}>
<l8, l22, (undef897 = undef897) /\ (undef898 = undef898) /\ (undef1016 = (0 + t_1193^0)) /\ ((1 + (~(1) * undef1016)) <= 0) /\ (undef1017 = (0 + t_1238^0)) /\ (undef1018 = (~(1) + undef897)) /\ (undef891 = (0 + undef898)) /\ ((0 + undef891) <= 0) /\ (undef1015 = undef1015) /\ (undef900 = undef900) /\ (undef860 = undef860) /\ (undef861 = undef861) /\ (undef1019 = (0 + undef860)) /\ (undef1020 = (0 + t_1267^0)) /\ (0 <= ((~(1) + undef1019) + (~(1) * undef1020))) /\ (undef925 = (0 + t_1275^0)) /\ (undef927 = (0 + t_1279^0)) /\ (0 <= ((~(1) + undef925) + (~(1) * undef927))) /\ (undef3453 = undef3453) /\ (undef3564 = (0 + t_1292^0)) /\ (undef3439 = (0 + x_9^0)) /\ ((0 + undef3439) <= 0) /\ (undef3563 = undef3563) /\ (undef3464 = undef3464) /\ (undef3410 = undef3410) /\ (undef3411 = undef3411) /\ (undef3565 = (0 + undef3410)) /\ (undef3567 = (0 + t_1412^0)) /\ (0 <= ((~(1) + undef3565) + (~(1) * undef3567))) /\ (undef3566 = (0 + t_1420^0)) /\ (undef3475 = (0 + t_1424^0)) /\ (0 <= ((~(1) + undef3566) + (~(1) * undef3475))) /\ ((0 + x_9^0) <= 0) /\ (undef3473 = undef3473) /\ (0 <= ((~(1) + (~(1) * t_1470^0)) + undef3473)) /\ (0 <= ((~(1) + t_1478^0) + (~(1) * t_1482^0))) /\ (undef5110 = undef5110) /\ (undef5021 = undef5021) /\ (undef5023 = undef5023) /\ ((0 + undef5110) <= 0) /\ (undef4944 = undef4944), par{t_11^0 -> undef3439, x_9^0 -> undef5110}>
<l8, l8, (undef1065 = undef1065) /\ (undef1188 = (0 + t_1193^0)) /\ (0 <= (0 + (~(1) * undef1188))) /\ (undef1189 = (0 + t_1197^0)) /\ (undef1064 = (0 + undef1065)) /\ ((0 + undef1064) <= 0) /\ (undef1037 = undef1037) /\ (undef1038 = undef1038) /\ (undef1190 = (0 + undef1037)) /\ (undef1191 = (0 + t_1219^0)) /\ (0 <= ((~(1) + undef1190) + (~(1) * undef1191))) /\ (undef1098 = (0 + t_1227^0)) /\ (undef1100 = (0 + t_1231^0)) /\ (0 <= ((~(1) + undef1098) + (~(1) * undef1100))), par{nondet_30^0 -> undef1038, t_11^0 -> undef1064}>
<l11, l3, (undef1442 = undef1442) /\ (undef1527 = (0 + t_148^0)) /\ ((1 + (~(1) * undef1527)) <= 0) /\ (undef1528 = (0 + t_193^0)) /\ (undef1529 = (~(1) + undef1442)) /\ (undef1402 = (0 + t_207^0)) /\ (0 <= (~(1) + undef1402)) /\ (undef1526 = undef1526) /\ (undef1445 = undef1445) /\ (undef1371 = undef1371) /\ (undef1372 = undef1372) /\ (undef1530 = (0 + undef1371)) /\ (undef1531 = (0 + t_222^0)) /\ (0 <= ((~(1) + undef1530) + (~(1) * undef1531))) /\ (undef1436 = (0 + t_230^0)) /\ (undef1438 = (0 + t_234^0)) /\ (0 <= ((~(1) + undef1436) + (~(1) * undef1438))) /\ (undef4247 = (0 + temp118_31^0)) /\ (undef4248 = ((0 + undef1442) + (~(1) * x_9^0))) /\ (undef4249 = (0 + undef1442)) /\ (undef4289 = (0 + x_9^0)) /\ (0 <= (~(1) + undef4289)) /\ (undef2711 = undef2711) /\ (undef2688 = undef2688) /\ (undef2558 = undef2558) /\ (undef2559 = undef2559) /\ (undef2712 = (0 + undef2558)) /\ (undef2714 = (0 + t_756^0)) /\ (0 <= ((~(1) + undef2712) + (~(1) * undef2714))) /\ (undef2713 = (0 + t_764^0)) /\ (undef2623 = (0 + t_768^0)) /\ (0 <= ((~(1) + undef2713) + (~(1) * undef2623))) /\ (0 <= (~(1) + x_9^0)) /\ (undef2621 = undef2621) /\ (0 <= ((~(1) + undef2621) + (~(1) * t_806^0))) /\ (0 <= ((~(1) + t_814^0) + (~(1) * t_818^0))) /\ (0 <= (~(1) + x_9^0)) /\ (undef44 = (0 + t_589^0)) /\ (0 <= (~(1) + undef44)) /\ (undef335 = undef335) /\ (undef178 = undef178) /\ (undef179 = undef179) /\ (undef336 = (0 + undef178)) /\ (undef337 = (0 + t_605^0)) /\ (0 <= ((~(1) + undef336) + (~(1) * undef337))) /\ (undef245 = (0 + t_613^0)) /\ (undef247 = (0 + t_617^0)) /\ (0 <= ((~(1) + undef245) + (~(1) * undef247))), par{t_11^0 -> undef44, x_9^0 -> (~(1) + x_9^0)}>
<l11, l22, (undef1442 = undef1442) /\ (undef1527 = (0 + t_148^0)) /\ ((1 + (~(1) * undef1527)) <= 0) /\ (undef1528 = (0 + t_193^0)) /\ (undef1529 = (~(1) + undef1442)) /\ (undef1402 = (0 + t_207^0)) /\ (0 <= (~(1) + undef1402)) /\ (undef1526 = undef1526) /\ (undef1445 = undef1445) /\ (undef1371 = undef1371) /\ (undef1372 = undef1372) /\ (undef1530 = (0 + undef1371)) /\ (undef1531 = (0 + t_222^0)) /\ (0 <= ((~(1) + undef1530) + (~(1) * undef1531))) /\ (undef1436 = (0 + t_230^0)) /\ (undef1438 = (0 + t_234^0)) /\ (0 <= ((~(1) + undef1436) + (~(1) * undef1438))) /\ (undef4503 = undef4503) /\ (undef4581 = (0 + t_244^0)) /\ (undef4456 = (0 + x_9^0)) /\ ((0 + undef4456) <= 0) /\ (undef4580 = undef4580) /\ (undef4438 = undef4438) /\ (undef4427 = undef4427) /\ (undef4428 = undef4428) /\ (undef4582 = (0 + undef4427)) /\ (undef4584 = (0 + t_1035^0)) /\ (0 <= ((~(1) + undef4582) + (~(1) * undef4584))) /\ (undef4583 = (0 + t_1043^0)) /\ (undef4492 = (0 + t_1047^0)) /\ (0 <= ((~(1) + undef4583) + (~(1) * undef4492))) /\ ((0 + x_9^0) <= 0) /\ (undef4490 = undef4490) /\ (0 <= ((~(1) + (~(1) * t_1091^0)) + undef4490)) /\ (0 <= ((~(1) + t_1099^0) + (~(1) * t_1103^0))) /\ (undef5110 = undef5110) /\ (undef5021 = undef5021) /\ (undef5023 = undef5023) /\ ((0 + undef5110) <= 0) /\ (undef4944 = undef4944), par{t_11^0 -> undef4456, x_9^0 -> undef5110}>
<l11, l11, (undef1699 = (0 + t_148^0)) /\ (0 <= (0 + (~(1) * undef1699))) /\ (undef1700 = (0 + t_152^0)) /\ (undef1575 = (0 + t_159^0)) /\ (0 <= (~(1) + undef1575)) /\ (undef1548 = undef1548) /\ (undef1549 = undef1549) /\ (undef1701 = (0 + undef1548)) /\ (undef1702 = (0 + t_174^0)) /\ (0 <= ((~(1) + undef1701) + (~(1) * undef1702))) /\ (undef1609 = (0 + t_182^0)) /\ (undef1611 = (0 + t_186^0)) /\ (0 <= ((~(1) + undef1609) + (~(1) * undef1611))), par{nondet_30^0 -> undef1549, t_11^0 -> undef1575}>

Fresh variables:
undef44, undef178, undef179, undef245, undef247, undef335, undef336, undef337, undef348, undef349, undef415, undef417, undef505, undef506, undef507, undef520, undef521, undef585, undef587, undef646, undef675, undef676, undef677, undef679, undef680, undef690, undef691, undef755, undef757, undef845, undef846, undef847, undef860, undef861, undef891, undef897, undef898, undef900, undef925, undef927, undef1015, undef1016, undef1017, undef1018, undef1019, undef1020, undef1037, undef1038, undef1064, undef1065, undef1098, undef1100, undef1188, undef1189, undef1190, undef1191, undef1371, undef1372, undef1402, undef1436, undef1438, undef1442, undef1445, undef1526, undef1527, undef1528, undef1529, undef1530, undef1531, undef1548, undef1549, undef1575, undef1609, undef1611, undef1699, undef1700, undef1701, undef1702, undef1913, undef2005, undef2037, undef2038, undef2082, undef2206, undef2250, undef2374, undef2375, undef2419, undef2543, undef2558, undef2559, undef2621, undef2623, undef2688, undef2711, undef2712, undef2713, undef2714, undef2731, undef2732, undef2792, undef2794, undef2882, undef2883, undef2898, undef2899, undef2961, undef2963, undef3001, undef3051, undef3052, undef3053, undef3054, undef3071, undef3072, undef3132, undef3134, undef3222, undef3223, undef3238, undef3239, undef3267, undef3281, undef3283, undef3301, undef3303, undef3391, undef3392, undef3393, undef3394, undef3395, undef3410, undef3411, undef3439, undef3453, undef3464, undef3473, undef3475, undef3563, undef3564, undef3565, undef3566, undef3567, undef3611, undef3710, undef3749, undef3750, undef3778, undef3812, undef3814, undef3877, undef3886, undef3902, undef3903, undef3904, undef3905, undef3906, undef3908, undef3909, undef3910, undef3950, undef4088, undef4089, undef4117, undef4151, undef4153, undef4189, undef4234, undef4241, undef4242, undef4243, undef4244, undef4245, undef4247, undef4248, undef4249, undef4289, undef4427, undef4428, undef4438, undef4456, undef4490, undef4492, undef4503, undef4580, undef4581, undef4582, undef4583, undef4584, undef4589, undef4591, undef4592, undef4593, undef4594, undef4595, undef4596, undef4603, undef4604, undef4605, undef4606, undef4628, undef4662, undef4664, undef4750, undef4752, undef4753, undef4754, undef4755, undef4756, undef4757, undef4758, undef4759, undef4760, undef4761, undef4762, undef4763, undef4768, undef4770, undef4771, undef4772, undef4773, undef4774, undef4775, undef4782, undef4783, undef4784, undef4785, undef4801, undef4807, undef4841, undef4843, undef4929, undef4931, undef4932, undef4933, undef4934, undef4935, undef4936, undef4937, undef4938, undef4939, undef4940, undef4941, undef4942, undef4943, undef4944, undef5021, undef5023, undef5110, undef5154, undef5355, undef5445, 

Undef variables:
undef44, undef178, undef179, undef245, undef247, undef335, undef336, undef337, undef348, undef349, undef415, undef417, undef505, undef506, undef507, undef520, undef521, undef585, undef587, undef646, undef675, undef676, undef677, undef679, undef680, undef690, undef691, undef755, undef757, undef845, undef846, undef847, undef860, undef861, undef891, undef897, undef898, undef900, undef925, undef927, undef1015, undef1016, undef1017, undef1018, undef1019, undef1020, undef1037, undef1038, undef1064, undef1065, undef1098, undef1100, undef1188, undef1189, undef1190, undef1191, undef1371, undef1372, undef1402, undef1436, undef1438, undef1442, undef1445, undef1526, undef1527, undef1528, undef1529, undef1530, undef1531, undef1548, undef1549, undef1575, undef1609, undef1611, undef1699, undef1700, undef1701, undef1702, undef1913, undef2005, undef2037, undef2038, undef2082, undef2206, undef2250, undef2374, undef2375, undef2419, undef2543, undef2558, undef2559, undef2621, undef2623, undef2688, undef2711, undef2712, undef2713, undef2714, undef2731, undef2732, undef2792, undef2794, undef2882, undef2883, undef2898, undef2899, undef2961, undef2963, undef3001, undef3051, undef3052, undef3053, undef3054, undef3071, undef3072, undef3132, undef3134, undef3222, undef3223, undef3238, undef3239, undef3267, undef3281, undef3283, undef3301, undef3303, undef3391, undef3392, undef3393, undef3394, undef3395, undef3410, undef3411, undef3439, undef3453, undef3464, undef3473, undef3475, undef3563, undef3564, undef3565, undef3566, undef3567, undef3611, undef3710, undef3749, undef3750, undef3778, undef3812, undef3814, undef3877, undef3886, undef3902, undef3903, undef3904, undef3905, undef3906, undef3908, undef3909, undef3910, undef3950, undef4088, undef4089, undef4117, undef4151, undef4153, undef4189, undef4234, undef4241, undef4242, undef4243, undef4244, undef4245, undef4247, undef4248, undef4249, undef4289, undef4427, undef4428, undef4438, undef4456, undef4490, undef4492, undef4503, undef4580, undef4581, undef4582, undef4583, undef4584, undef4589, undef4591, undef4592, undef4593, undef4594, undef4595, undef4596, undef4603, undef4604, undef4605, undef4606, undef4628, undef4662, undef4664, undef4750, undef4752, undef4753, undef4754, undef4755, undef4756, undef4757, undef4758, undef4759, undef4760, undef4761, undef4762, undef4763, undef4768, undef4770, undef4771, undef4772, undef4773, undef4774, undef4775, undef4782, undef4783, undef4784, undef4785, undef4801, undef4807, undef4841, undef4843, undef4929, undef4931, undef4932, undef4933, undef4934, undef4935, undef4936, undef4937, undef4938, undef4939, undef4940, undef4941, undef4942, undef4943, undef4944, undef5021, undef5023, undef5110, undef5154, undef5355, undef5445, 

Abstraction variables:

Exit nodes:

Accepting locations:

Asserts:

*************************************************************
*******************************************************************************************
***********************       WORKING TRANSITION SYSTEM (DAG)       ***********************
*******************************************************************************************

Init Location: 0
Graph 0:
Transitions:
Variables:

Graph 1:
Transitions:
<l8, l8, undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>
Variables:
nondet_30^0, t_1193^0, t_1197^0, t_11^0, t_1219^0, t_1227^0, t_1231^0

Graph 2:
Transitions:
<l11, l11, undef1699 <= 0 /\ 1 <= undef1575 /\ 1 + undef1611 <= undef1609 /\ 1 + undef1702 <= undef1701 /\ t_148^0 = undef1699 /\ t_152^0 = undef1700 /\ t_159^0 = undef1575 /\ t_174^0 = undef1702 /\ t_182^0 = undef1609 /\ t_186^0 = undef1611 /\ undef1548 = undef1701, {nondet_30^0 -> undef1549, t_11^0 -> undef1575, rest remain the same}>
Variables:
nondet_30^0, t_11^0, t_148^0, t_152^0, t_159^0, t_174^0, t_182^0, t_186^0

Graph 3:
Transitions:
Variables:

Graph 4:
Transitions:
<l3, l3, 1 + t_806^0 <= undef2621 /\ 1 + t_818^0 <= t_814^0 /\ 1 <= x_9^0 /\ 1 <= undef44 /\ 1 + undef247 <= undef245 /\ 1 + undef337 <= undef336 /\ 1 + undef587 <= undef585 /\ 1 + undef677 <= undef676 /\ 1 <= undef1913 /\ 1 <= undef2037 /\ 1 + undef2623 <= undef2713 /\ 1 + undef2714 <= undef2712 /\ 1 <= undef3611 /\ t_589^0 = undef44 /\ t_605^0 = undef337 /\ t_613^0 = undef245 /\ t_617^0 = undef247 /\ t_630^0 = undef2037 /\ t_677^0 = undef2038 /\ t_691^0 = undef1913 /\ t_708^0 = undef677 /\ t_716^0 = undef585 /\ t_720^0 = undef587 /\ t_756^0 = undef2714 /\ t_764^0 = undef2713 /\ t_768^0 = undef2623 /\ x_9^0 = undef3611 /\ undef178 = undef336 /\ undef520 = undef676 /\ undef2558 = undef2712, {t_11^0 -> undef44, x_9^0 -> -1 + x_9^0, rest remain the same}>
<l3, l3, undef2206 <= 0 /\ 1 <= undef2082 /\ 1 + undef2794 <= undef2792 /\ 1 + undef2883 <= undef2882 /\ t_630^0 = undef2206 /\ t_641^0 = undef2082 /\ t_658^0 = undef2883 /\ t_666^0 = undef2792 /\ t_670^0 = undef2794 /\ undef2731 = undef2882, {nondet_30^0 -> undef2732, t_11^0 -> undef2082, rest remain the same}>
Variables:
t_11^0, t_589^0, t_605^0, t_613^0, t_617^0, t_630^0, t_677^0, t_691^0, t_708^0, t_716^0, t_720^0, t_756^0, t_764^0, t_768^0, t_806^0, t_814^0, t_818^0, x_9^0, nondet_30^0, t_641^0, t_658^0, t_666^0, t_670^0

Precedence: 
Graph 0

Graph 1
<l0, l8, undef4807 <= 0 /\ undef4934 <= 0 /\ 1 + undef4843 <= undef4841 /\ 1 + undef4940 <= undef4936 /\ 1 + undef4941 <= undef4937 /\ 1 + undef4942 <= undef4939 /\ 1 <= undef4943 /\ cnt_58^0 = undef4935 /\ t_1122^0 = undef4940 /\ t_1130^0 = undef4937 /\ t_1134^0 = undef4941 /\ t_1146^0 = undef4938 /\ t_1166^0 = undef4942 /\ t_1174^0 = undef4841 /\ t_1178^0 = undef4843 /\ undef4772 = undef4936 /\ undef4774 = undef4939 /\ undef4782 = undef4929 /\ undef4783 = undef4934 /\ undef4801 = undef4807 /\ undef4929 = undef4943, {t_11^0 -> undef4807, temp118_31^0 -> undef4929, x_9^0 -> -1 + undef4943, rest remain the same}>

Graph 2
<l0, l11, 1 <= undef4628 /\ 1 + undef4664 <= undef4662 /\ 1 <= undef4754 /\ 1 + undef4760 <= undef4756 /\ 1 + undef4761 <= undef4757 /\ 1 + undef4762 <= undef4759 /\ 1 <= undef4763 /\ cnt_58^0 = undef4755 /\ t_105^0 = undef4758 /\ t_112^0 = undef4628 /\ t_127^0 = undef4762 /\ t_135^0 = undef4662 /\ t_139^0 = undef4664 /\ t_84^0 = undef4760 /\ t_92^0 = undef4757 /\ t_96^0 = undef4761 /\ undef4593 = undef4756 /\ undef4595 = undef4759 /\ undef4603 = undef4750 /\ undef4604 = undef4754 /\ undef4750 = undef4763, {t_11^0 -> undef4628, temp118_31^0 -> undef4750, x_9^0 -> -1 + undef4763, rest remain the same}>

Graph 3
<l8, l22, x_9^0 <= 0 /\ undef891 <= 0 /\ undef3439 <= 0 /\ undef5110 <= 0 /\ 1 + t_1470^0 <= undef3473 /\ 1 + t_1482^0 <= t_1478^0 /\ 1 + undef927 <= undef925 /\ 1 <= undef1016 /\ 1 + undef1020 <= undef1019 /\ 1 + undef3475 <= undef3566 /\ 1 + undef3567 <= undef3565 /\ t_1193^0 = undef1016 /\ t_1238^0 = undef1017 /\ t_1267^0 = undef1020 /\ t_1275^0 = undef925 /\ t_1279^0 = undef927 /\ t_1292^0 = undef3564 /\ t_1412^0 = undef3567 /\ t_1420^0 = undef3566 /\ t_1424^0 = undef3475 /\ x_9^0 = undef3439 /\ undef860 = undef1019 /\ undef891 = undef898 /\ undef3410 = undef3565 /\ undef897 = 1 + undef1018, {t_11^0 -> undef3439, x_9^0 -> undef5110, rest remain the same}>
<l11, l22, x_9^0 <= 0 /\ undef4456 <= 0 /\ undef5110 <= 0 /\ 1 + t_1091^0 <= undef4490 /\ 1 + t_1103^0 <= t_1099^0 /\ 1 <= undef1402 /\ 1 + undef1438 <= undef1436 /\ 1 <= undef1527 /\ 1 + undef1531 <= undef1530 /\ 1 + undef4492 <= undef4583 /\ 1 + undef4584 <= undef4582 /\ t_1035^0 = undef4584 /\ t_1043^0 = undef4583 /\ t_1047^0 = undef4492 /\ t_148^0 = undef1527 /\ t_193^0 = undef1528 /\ t_207^0 = undef1402 /\ t_222^0 = undef1531 /\ t_230^0 = undef1436 /\ t_234^0 = undef1438 /\ t_244^0 = undef4581 /\ x_9^0 = undef4456 /\ undef1371 = undef1530 /\ undef4427 = undef4582 /\ undef1442 = 1 + undef1529, {t_11^0 -> undef4456, x_9^0 -> undef5110, rest remain the same}>

Graph 4
<l8, l3, undef891 <= 0 /\ 1 + t_1374^0 <= undef3301 /\ 1 + t_1386^0 <= t_1382^0 /\ 1 <= x_9^0 /\ 1 <= undef44 /\ 1 + undef247 <= undef245 /\ 1 + undef337 <= undef336 /\ 1 + undef927 <= undef925 /\ 1 <= undef1016 /\ 1 + undef1020 <= undef1019 /\ 1 <= undef3267 /\ 1 + undef3303 <= undef3394 /\ 1 + undef3395 <= undef3393 /\ t_1193^0 = undef1016 /\ t_1238^0 = undef1017 /\ t_1267^0 = undef1020 /\ t_1275^0 = undef925 /\ t_1279^0 = undef927 /\ t_1292^0 = undef3392 /\ t_1320^0 = undef3395 /\ t_1328^0 = undef3394 /\ t_1332^0 = undef3303 /\ t_589^0 = undef44 /\ t_605^0 = undef337 /\ t_613^0 = undef245 /\ t_617^0 = undef247 /\ x_9^0 = undef3267 /\ undef178 = undef336 /\ undef860 = undef1019 /\ undef891 = undef898 /\ undef3238 = undef3393 /\ undef897 = 1 + undef1018, {t_11^0 -> undef44, x_9^0 -> -1 + x_9^0, rest remain the same}>
<l11, l3, 1 + t_806^0 <= undef2621 /\ 1 + t_818^0 <= t_814^0 /\ 1 <= x_9^0 /\ 1 <= undef44 /\ 1 + undef247 <= undef245 /\ 1 + undef337 <= undef336 /\ 1 <= undef1402 /\ 1 + undef1438 <= undef1436 /\ 1 <= undef1527 /\ 1 + undef1531 <= undef1530 /\ 1 + undef2623 <= undef2713 /\ 1 + undef2714 <= undef2712 /\ 1 <= undef4289 /\ t_148^0 = undef1527 /\ t_193^0 = undef1528 /\ t_207^0 = undef1402 /\ t_222^0 = undef1531 /\ t_230^0 = undef1436 /\ t_234^0 = undef1438 /\ t_589^0 = undef44 /\ t_605^0 = undef337 /\ t_613^0 = undef245 /\ t_617^0 = undef247 /\ t_756^0 = undef2714 /\ t_764^0 = undef2713 /\ t_768^0 = undef2623 /\ temp118_31^0 = undef4247 /\ x_9^0 + undef4248 = undef1442 /\ x_9^0 = undef4289 /\ undef178 = undef336 /\ undef1371 = undef1530 /\ undef1442 = undef4249 /\ undef2558 = undef2712 /\ undef1442 = 1 + undef1529, {t_11^0 -> undef44, x_9^0 -> -1 + x_9^0, rest remain the same}>

Map Locations to Subgraph:
( 0 , 0 )
( 3 , 4 )
( 8 , 1 )
( 11 , 2 )
( 22 , 3 )

*******************************************************************************************
********************************    CHECKING ASSERTIONS    ********************************
*******************************************************************************************

Proving termination of subgraph 0
Proving termination of subgraph 1
Checking unfeasibility...
Time used: 0.003124

Checking conditional termination of SCC {l8}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000841s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003818s
Trying to remove transition: <l8, l8, undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007384s
Time used: 0.007028
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012785s
Time used: 0.011906
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.012613s
Time used: 0.01261

LOG: SAT solveNonLinear - Elapsed time: 0.025398s
Cost: 1; Total time: 0.024516
Failed at location 8: t_1227^0 <= t_1193^0 + t_1231^0
Before Improving: 
Quasi-invariant at l8: t_1227^0 <= t_1193^0 + t_1231^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003901s
Remaining time after improvement: 0.998215
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l8: t_1227^0 <= t_1193^0 + t_1231^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l8, l8, undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l8, l8, undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>
New Graphs: 
Calling Safety with literal t_1227^0 <= t_1193^0 + t_1231^0 and entry <l0, l8, undef4807 <= 0 /\ undef4934 <= 0 /\ 1 + undef4843 <= undef4841 /\ 1 + undef4940 <= undef4936 /\ 1 + undef4941 <= undef4937 /\ 1 + undef4942 <= undef4939 /\ 1 <= undef4943 /\ cnt_58^0 = undef4935 /\ t_1122^0 = undef4940 /\ t_1130^0 = undef4937 /\ t_1134^0 = undef4941 /\ t_1146^0 = undef4938 /\ t_1166^0 = undef4942 /\ t_1174^0 = undef4841 /\ t_1178^0 = undef4843 /\ undef4772 = undef4936 /\ undef4774 = undef4939 /\ undef4782 = undef4929 /\ undef4783 = undef4934 /\ undef4801 = undef4807 /\ undef4929 = undef4943, {t_11^0 -> undef4807, temp118_31^0 -> undef4929, x_9^0 -> -1 + undef4943, rest remain the same}>

LOG: CALL check - Post:t_1227^0 <= t_1193^0 + t_1231^0 - Process 1
* Exit transition: <l0, l8, undef4807 <= 0 /\ undef4934 <= 0 /\ 1 + undef4843 <= undef4841 /\ 1 + undef4940 <= undef4936 /\ 1 + undef4941 <= undef4937 /\ 1 + undef4942 <= undef4939 /\ 1 <= undef4943 /\ cnt_58^0 = undef4935 /\ t_1122^0 = undef4940 /\ t_1130^0 = undef4937 /\ t_1134^0 = undef4941 /\ t_1146^0 = undef4938 /\ t_1166^0 = undef4942 /\ t_1174^0 = undef4841 /\ t_1178^0 = undef4843 /\ undef4772 = undef4936 /\ undef4774 = undef4939 /\ undef4782 = undef4929 /\ undef4783 = undef4934 /\ undef4801 = undef4807 /\ undef4929 = undef4943, {t_11^0 -> undef4807, temp118_31^0 -> undef4929, x_9^0 -> -1 + undef4943, rest remain the same}>
* Postcondition  : t_1227^0 <= t_1193^0 + t_1231^0

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001947s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.002079s
INVARIANTS: 
8: 
Quasi-INVARIANTS to narrow Graph: 
8: t_1227^0 <= t_1193^0 + t_1231^0 , 
Narrowing transition: 
<l8, l8, undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l8, l8, undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>
Variables:
nondet_30^0, t_1193^0, t_1197^0, t_11^0, t_1219^0, t_1227^0, t_1231^0
Checking conditional termination of SCC {l8}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000802s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.004087s
Trying to remove transition: <l8, l8, undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.006431s
Time used: 0.006018
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012128s
Time used: 0.011315
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.013095s
Time used: 0.013093

LOG: SAT solveNonLinear - Elapsed time: 0.025223s
Cost: 1; Total time: 0.024408
Failed at location 8: t_1227^0 <= t_1231^0
Before Improving: 
Quasi-invariant at l8: t_1227^0 <= t_1231^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003817s
Remaining time after improvement: 0.998072
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l8: t_1227^0 <= t_1231^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l8, l8, undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...
> It's unfeasible. Removing transition: 
<l8, l8, undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>
New Graphs: 
Calling Safety with literal t_1227^0 <= t_1231^0 and entry <l0, l8, undef4807 <= 0 /\ undef4934 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + undef4843 <= undef4841 /\ 1 + undef4940 <= undef4936 /\ 1 + undef4941 <= undef4937 /\ 1 + undef4942 <= undef4939 /\ 1 <= undef4943 /\ cnt_58^0 = undef4935 /\ t_1122^0 = undef4940 /\ t_1130^0 = undef4937 /\ t_1134^0 = undef4941 /\ t_1146^0 = undef4938 /\ t_1166^0 = undef4942 /\ t_1174^0 = undef4841 /\ t_1178^0 = undef4843 /\ undef4772 = undef4936 /\ undef4774 = undef4939 /\ undef4782 = undef4929 /\ undef4783 = undef4934 /\ undef4801 = undef4807 /\ undef4929 = undef4943, {t_11^0 -> undef4807, temp118_31^0 -> undef4929, x_9^0 -> -1 + undef4943, rest remain the same}>

LOG: CALL check - Post:t_1227^0 <= t_1231^0 - Process 2
* Exit transition: <l0, l8, undef4807 <= 0 /\ undef4934 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + undef4843 <= undef4841 /\ 1 + undef4940 <= undef4936 /\ 1 + undef4941 <= undef4937 /\ 1 + undef4942 <= undef4939 /\ 1 <= undef4943 /\ cnt_58^0 = undef4935 /\ t_1122^0 = undef4940 /\ t_1130^0 = undef4937 /\ t_1134^0 = undef4941 /\ t_1146^0 = undef4938 /\ t_1166^0 = undef4942 /\ t_1174^0 = undef4841 /\ t_1178^0 = undef4843 /\ undef4772 = undef4936 /\ undef4774 = undef4939 /\ undef4782 = undef4929 /\ undef4783 = undef4934 /\ undef4801 = undef4807 /\ undef4929 = undef4943, {t_11^0 -> undef4807, temp118_31^0 -> undef4929, x_9^0 -> -1 + undef4943, rest remain the same}>
* Postcondition  : t_1227^0 <= t_1231^0

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001600s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.001738s
INVARIANTS: 
8: 
Quasi-INVARIANTS to narrow Graph: 
8: t_1227^0 <= t_1231^0 , 
Narrowing transition: 
<l8, l8, undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l8, l8, undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + t_1231^0 <= t_1227^0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>
Variables:
nondet_30^0, t_1193^0, t_1197^0, t_11^0, t_1219^0, t_1227^0, t_1231^0
Checking conditional termination of SCC {l8}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000854s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.004139s
Trying to remove transition: <l8, l8, undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + t_1231^0 <= t_1227^0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007085s
Time used: 0.006646
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013594s
Time used: 0.012698
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.011038s
Time used: 0.011037

LOG: SAT solveNonLinear - Elapsed time: 0.024632s
Cost: 1; Total time: 0.023735
Failed at location 8: 1 <= t_1193^0
Before Improving: 
Quasi-invariant at l8: 1 <= t_1193^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.003939s
Remaining time after improvement: 0.997965
Termination implied by a set of quasi-invariant(s):
Quasi-invariant at l8: 1 <= t_1193^0
[ Invariant Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l8, l8, undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + t_1231^0 <= t_1227^0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>
[ Termination Graph ]
Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
It's unfeasible. Removing transition: 
<l8, l8, undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + t_1231^0 <= t_1227^0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>
New Graphs: 
Calling Safety with literal 1 <= t_1193^0 and entry <l0, l8, undef4807 <= 0 /\ undef4934 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + t_1231^0 <= t_1227^0 /\ 1 + undef4843 <= undef4841 /\ 1 + undef4940 <= undef4936 /\ 1 + undef4941 <= undef4937 /\ 1 + undef4942 <= undef4939 /\ 1 <= undef4943 /\ cnt_58^0 = undef4935 /\ t_1122^0 = undef4940 /\ t_1130^0 = undef4937 /\ t_1134^0 = undef4941 /\ t_1146^0 = undef4938 /\ t_1166^0 = undef4942 /\ t_1174^0 = undef4841 /\ t_1178^0 = undef4843 /\ undef4772 = undef4936 /\ undef4774 = undef4939 /\ undef4782 = undef4929 /\ undef4783 = undef4934 /\ undef4801 = undef4807 /\ undef4929 = undef4943, {t_11^0 -> undef4807, temp118_31^0 -> undef4929, x_9^0 -> -1 + undef4943, rest remain the same}>

LOG: CALL check - Post:1 <= t_1193^0 - Process 3
* Exit transition: <l0, l8, undef4807 <= 0 /\ undef4934 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + t_1231^0 <= t_1227^0 /\ 1 + undef4843 <= undef4841 /\ 1 + undef4940 <= undef4936 /\ 1 + undef4941 <= undef4937 /\ 1 + undef4942 <= undef4939 /\ 1 <= undef4943 /\ cnt_58^0 = undef4935 /\ t_1122^0 = undef4940 /\ t_1130^0 = undef4937 /\ t_1134^0 = undef4941 /\ t_1146^0 = undef4938 /\ t_1166^0 = undef4942 /\ t_1174^0 = undef4841 /\ t_1178^0 = undef4843 /\ undef4772 = undef4936 /\ undef4774 = undef4939 /\ undef4782 = undef4929 /\ undef4783 = undef4934 /\ undef4801 = undef4807 /\ undef4929 = undef4943, {t_11^0 -> undef4807, temp118_31^0 -> undef4929, x_9^0 -> -1 + undef4943, rest remain the same}>
* Postcondition  : 1 <= t_1193^0

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.001733s
> Postcondition is not implied!

LOG: RETURN check - Elapsed time: 0.001873s
INVARIANTS: 
8: 
Quasi-INVARIANTS to narrow Graph: 
8: 1 <= t_1193^0 , 
Narrowing transition: 
<l8, l8, undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + t_1231^0 <= t_1227^0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>

LOG: Narrow transition size 1
invGraph after Narrowing: 
Transitions:
<l8, l8, t_1193^0 <= 0 /\ undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + t_1231^0 <= t_1227^0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>
Variables:
nondet_30^0, t_1193^0, t_1197^0, t_11^0, t_1219^0, t_1227^0, t_1231^0
Checking conditional termination of SCC {l8}...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.000882s

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.004158s
Trying to remove transition: <l8, l8, t_1193^0 <= 0 /\ undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + t_1231^0 <= t_1227^0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.007101s
Time used: 0.006639
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013616s
Time used: 0.012897
Solving with 2 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001235s
Time used: 4.00011
Solving with 3 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.005834s
Time used: 1.00005
Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.021116s
Time used: 0.008294

Proving non-termination of subgraph 1
Transitions:
<l8, l8, t_1193^0 <= 0 /\ undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + t_1231^0 <= t_1227^0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>
Variables:
nondet_30^0, t_1193^0, t_1197^0, t_11^0, t_1219^0, t_1227^0, t_1231^0

Checking that every undef value has an assignment...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.004967s
Checking conditional non-termination of SCC {l8}...
EXIT TRANSITIONS:
<l8, end, t_1227^0 <= t_1193^0 + t_1231^0 /\ 1 <= t_1193^0, {all remain the same}>
<l8, end, 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 <= t_1193^0 /\ 1 + t_1231^0 <= t_1227^0, {all remain the same}>
<l8, end, t_1193^0 <= 0 /\ t_1227^0 <= t_1231^0, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.107444s
Time used: 0.106547
Improving Solution with cost 3 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.182679s
Time used: 0.182675

LOG: SAT solveNonLinear - Elapsed time: 0.290122s
Cost: 3; Total time: 0.289222
Failed at location 8: t_1193^0 <= 0
Before Improving: 
Quasi-invariant at l8: t_1193^0 <= 0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009671s
Remaining time after improvement: 0.994926
Minimizing number of undef constraints...

LOG: CALL solveNonLinear

LOG: RETURN solveNonLinear - Elapsed time: 0.009816s
Number of undef constraints reduced!

Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l8: t_1193^0 <= 0

Strengthening and disabling EXIT transitions...
Closed exits from l8: 2
Strengthening exit transition (result): 
<l8, end, t_1193^0 <= 0 /\ t_1227^0 <= t_1231^0, {all remain the same}>

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, t_1193^0 <= 0 /\ undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + t_1231^0 <= t_1227^0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>

Checking conditional non-termination of SCC {l8}...
EXIT TRANSITIONS:
<l8, end, t_1193^0 <= 0 /\ t_1227^0 <= t_1231^0, {all remain the same}>

Solving with 1 template(s).

LOG: CALL solveNonLinearGetFirstSolution

LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.128754s
Time used: 0.128009
Improving Solution with cost 1 ...

LOG: CALL solveNonLinearGetNextSolution

LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.061107s
Time used: 0.061104

LOG: SAT solveNonLinear - Elapsed time: 0.189861s
Cost: 1; Total time: 0.189113
Failed at location 8: 1 + t_1231^0 <= t_1227^0
Before Improving: 
Quasi-invariant at l8: 1 + t_1231^0 <= t_1227^0
Optimizing invariants...

LOG: CALL solveLinear

LOG: RETURN solveLinear - Elapsed time: 0.009456s
Remaining time after improvement: 0.994432
Minimizing number of undef constraints...

LOG: CALL solveNonLinear

LOG: RETURN solveNonLinear - Elapsed time: 0.009618s
Number of undef constraints reduced!

Non-termination implied by a set of quasi-invariant(s):
Quasi-invariant at l8: 1 + t_1231^0 <= t_1227^0

Strengthening and disabling EXIT transitions...
Closed exits from l8: 1

Strengthening and disabling transitions...

LOG: CALL solverLinear in Graph for feasibility

LOG: RETURN solveLinear in Graph for feasibility
Strengthening transition (result): 
<l8, l8, t_1193^0 <= 0 /\ undef1064 <= 0 /\ undef1188 <= 0 /\ 1 + t_1193^0 + t_1231^0 <= t_1227^0 /\ 1 + t_1231^0 <= t_1227^0 /\ 1 + undef1100 <= undef1098 /\ 1 + undef1191 <= undef1190 /\ t_1193^0 = undef1188 /\ t_1197^0 = undef1189 /\ t_1219^0 = undef1191 /\ t_1227^0 = undef1098 /\ t_1231^0 = undef1100 /\ undef1037 = undef1190 /\ undef1064 = undef1065, {nondet_30^0 -> undef1038, t_11^0 -> undef1064, rest remain the same}>

Calling reachability with...
Transition: <l8, end, true, {all remain the same}>
Conditions: t_1193^0 <= 0, 1 + t_1231^0 <= t_1227^0, 
OPEN EXITS: 
<l8, end, true, {all remain the same}> (condsUp: t_1193^0 <= 0, 1 + t_1231^0 <= t_1227^0)

--- Reachability graph ---
> Graph without transitions.

Calling reachability with...
Transition: <l0, l8, undef4807 <= 0 /\ undef4934 <= 0 /\ 1 + undef4843 <= undef4841 /\ 1 + undef4940 <= undef4936 /\ 1 + undef4941 <= undef4937 /\ 1 + undef4942 <= undef4939 /\ 1 <= undef4943 /\ cnt_58^0 = undef4935 /\ t_1122^0 = undef4940 /\ t_1130^0 = undef4937 /\ t_1134^0 = undef4941 /\ t_1146^0 = undef4938 /\ t_1166^0 = undef4942 /\ t_1174^0 = undef4841 /\ t_1178^0 = undef4843 /\ undef4772 = undef4936 /\ undef4774 = undef4939 /\ undef4782 = undef4929 /\ undef4783 = undef4934 /\ undef4801 = undef4807 /\ undef4929 = undef4943, {t_11^0 -> undef4807, temp118_31^0 -> undef4929, x_9^0 -> -1 + undef4943, rest remain the same}>
Conditions: t_1193^0 <= 0, 1 + t_1231^0 <= t_1227^0, 
OPEN EXITS: 
<l0, l8, t_1193^0 <= 0 /\ undef4807 <= 0 /\ undef4934 <= 0 /\ 1 + t_1231^0 <= t_1227^0 /\ 1 + undef4843 <= undef4841 /\ 1 + undef4940 <= undef4936 /\ 1 + undef4941 <= undef4937 /\ 1 + undef4942 <= undef4939 /\ 1 <= undef4943 /\ cnt_58^0 = undef4935 /\ t_1122^0 = undef4940 /\ t_1130^0 = undef4937 /\ t_1134^0 = undef4941 /\ t_1146^0 = undef4938 /\ t_1166^0 = undef4942 /\ t_1174^0 = undef4841 /\ t_1178^0 = undef4843 /\ undef4772 = undef4936 /\ undef4774 = undef4939 /\ undef4782 = undef4929 /\ undef4783 = undef4934 /\ undef4801 = undef4807 /\ undef4929 = undef4943, {t_11^0 -> undef4807, temp118_31^0 -> undef4929, x_9^0 -> -1 + undef4943, rest remain the same}>

> Conditions are reachable!

Program does NOT terminate