NO Solver Timeout: 4 Global Timeout: 300 No parsing errors! Init Location: 0 Transitions: undef3, oldX1^0 -> undef8, oldX2^0 -> undef9, oldX3^0 -> undef10, oldX4^0 -> undef11, oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef14, oldX8^0 -> undef15, x0^0 -> (0 + undef3), x1^0 -> (0 + undef8), x2^0 -> (0 + undef9), x3^0 -> (0 + undef10), x4^0 -> (0 + undef11), x5^0 -> (0 + undef14), x6^0 -> (0 + undef15)}> undef26, oldX1^0 -> undef31, oldX2^0 -> undef32, oldX3^0 -> undef33, oldX4^0 -> undef34, oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef37, oldX8^0 -> undef38, x0^0 -> (0 + undef26), x1^0 -> (0 + undef31), x2^0 -> (0 + undef32), x3^0 -> (0 + undef33), x4^0 -> (0 + undef34), x5^0 -> (0 + undef37), x6^0 -> (0 + undef38)}> undef49, oldX1^0 -> undef54, oldX2^0 -> undef55, oldX3^0 -> undef56, oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef60, oldX8^0 -> undef61, oldX9^0 -> undef62, x0^0 -> (0 + undef49), x1^0 -> (0 + undef54), x2^0 -> (0 + undef55), x3^0 -> ((0 + (~(1) * __const_32^0)) + undef56), x4^0 -> (0 + undef60), x5^0 -> (0 + undef61), x6^0 -> (0 + undef62)}> undef72, oldX1^0 -> undef77, oldX2^0 -> undef78, oldX3^0 -> undef79, oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef83, oldX8^0 -> undef84, x0^0 -> (0 + undef72), x1^0 -> (0 + undef77), x2^0 -> (0 + undef78), x3^0 -> (0 + undef79), x4^0 -> (0 + undef79), x5^0 -> (0 + undef83), x6^0 -> (0 + undef84)}> undef95, oldX1^0 -> undef100, oldX2^0 -> undef101, oldX3^0 -> undef102, oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef106, oldX8^0 -> undef107, oldX9^0 -> undef108, x0^0 -> (0 + undef95), x1^0 -> (0 + undef100), x2^0 -> (0 + undef101), x3^0 -> (0 + undef102), x4^0 -> (0 + undef106), x5^0 -> (0 + undef107), x6^0 -> (0 + undef108)}> undef118, oldX10^0 -> undef119, oldX1^0 -> undef123, oldX2^0 -> undef124, oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef129, oldX8^0 -> undef130, oldX9^0 -> undef131, x0^0 -> (0 + undef118), x1^0 -> (0 + undef123), x2^0 -> (~(1) + undef124), x3^0 -> (0 + undef129), x4^0 -> (0 + undef130), x5^0 -> (0 + undef131), x6^0 -> (0 + undef119)}> undef141, oldX10^0 -> undef142, oldX11^0 -> undef143, oldX1^0 -> undef146, oldX2^0 -> undef147, oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef152, oldX8^0 -> undef153, oldX9^0 -> undef154, x0^0 -> (0 + undef141), x1^0 -> (0 + undef146), x2^0 -> (0 + undef147), x3^0 -> (0 + undef152), x4^0 -> (0 + undef153), x5^0 -> (0 + undef154), x6^0 -> (0 + undef142)}> undef164, oldX10^0 -> undef165, oldX11^0 -> undef166, oldX1^0 -> undef169, oldX2^0 -> undef170, oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef175, oldX8^0 -> undef176, oldX9^0 -> undef177, x0^0 -> (0 + undef164), x1^0 -> (0 + undef169), x2^0 -> (0 + undef170), x3^0 -> (0 + undef175), x4^0 -> (0 + undef176), x5^0 -> (0 + undef177), x6^0 -> (0 + undef165)}> undef187, oldX10^0 -> undef188, oldX11^0 -> undef189, oldX1^0 -> undef192, oldX2^0 -> undef193, oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef198, oldX8^0 -> undef199, oldX9^0 -> undef200, x0^0 -> (0 + undef187), x1^0 -> (0 + undef192), x2^0 -> (0 + undef193), x3^0 -> (0 + undef198), x4^0 -> (0 + undef199), x5^0 -> (0 + undef200), x6^0 -> (0 + undef188)}> undef210, oldX1^0 -> undef215, oldX2^0 -> undef216, oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef221, oldX8^0 -> undef222, oldX9^0 -> undef223, x0^0 -> (0 + undef210), x1^0 -> (0 + undef215), x2^0 -> (0 + undef216), x3^0 -> (0 + undef216), x4^0 -> (0 + undef221), x5^0 -> (0 + undef222), x6^0 -> (0 + undef223)}> undef233, oldX10^0 -> undef234, oldX1^0 -> undef238, oldX2^0 -> undef239, oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef244, oldX8^0 -> undef245, oldX9^0 -> undef246, x0^0 -> (0 + undef233), x1^0 -> (0 + undef238), x2^0 -> (0 + undef239), x3^0 -> (0 + undef244), x4^0 -> (0 + undef245), x5^0 -> (0 + undef246), x6^0 -> (0 + undef234)}> undef256, oldX10^0 -> undef257, oldX1^0 -> undef261, oldX2^0 -> undef262, oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef267, oldX8^0 -> undef268, oldX9^0 -> undef269, x0^0 -> (0 + undef256), x1^0 -> (0 + undef261), x2^0 -> (0 + undef262), x3^0 -> (0 + undef267), x4^0 -> (0 + undef268), x5^0 -> (0 + undef269), x6^0 -> (0 + undef257)}> (0 + x0^0), oldX10^0 -> undef280, oldX11^0 -> undef281, oldX12^0 -> undef282, oldX13^0 -> undef283, oldX1^0 -> (0 + x1^0), oldX2^0 -> (0 + x2^0), oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef290, oldX8^0 -> undef291, oldX9^0 -> undef292, x0^0 -> (0 + undef290), x1^0 -> (0 + undef291), x2^0 -> (0 + undef292), x3^0 -> (0 + undef280), x4^0 -> (0 + undef281), x5^0 -> (0 + undef282), x6^0 -> (0 + undef283)}> undef302, oldX1^0 -> undef307, oldX2^0 -> undef308, oldX3^0 -> undef309, oldX4^0 -> undef310, oldX5^0 -> undef311, oldX6^0 -> undef312, x0^0 -> (0 + undef302), x1^0 -> (0 + undef307), x2^0 -> (0 + undef308), x3^0 -> (0 + undef309), x4^0 -> (0 + undef310), x5^0 -> (0 + undef311), x6^0 -> (0 + undef312)}> undef325, oldX1^0 -> undef330, oldX2^0 -> undef331, oldX3^0 -> undef332, oldX4^0 -> undef333, oldX5^0 -> undef334, oldX6^0 -> undef335, x0^0 -> (0 + undef325), x1^0 -> (0 + undef330), x2^0 -> (0 + undef331), x3^0 -> (0 + undef332), x4^0 -> (0 + undef333), x5^0 -> (0 + undef334), x6^0 -> (~(1) + undef335)}> undef371, oldX1^0 -> undef376, oldX2^0 -> undef377, oldX3^0 -> undef378, oldX4^0 -> undef379, oldX5^0 -> undef380, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef382, x0^0 -> (0 + undef371), x1^0 -> (0 + undef376), x2^0 -> (0 + undef377), x3^0 -> (0 + undef378), x4^0 -> (0 + undef379), x5^0 -> (0 + undef380), x6^0 -> (0 + undef382)}> undef394, oldX1^0 -> undef399, oldX2^0 -> undef400, oldX3^0 -> undef401, oldX4^0 -> undef402, oldX5^0 -> undef403, oldX6^0 -> (0 + x6^0), x0^0 -> (0 + undef394), x1^0 -> (0 + undef399), x2^0 -> (0 + undef400), x3^0 -> (0 + undef401), x4^0 -> (0 + undef402), x5^0 -> (0 + undef403), x6^0 -> (0 + undef403)}> undef417, oldX1^0 -> undef422, oldX2^0 -> undef423, oldX3^0 -> undef424, oldX4^0 -> undef425, oldX5^0 -> undef426, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef428, x0^0 -> (0 + undef417), x1^0 -> (0 + undef422), x2^0 -> (0 + undef423), x3^0 -> (0 + undef424), x4^0 -> (0 + undef425), x5^0 -> (~(4) + undef426), x6^0 -> (0 + undef428)}> undef440, oldX1^0 -> undef445, oldX2^0 -> undef446, oldX3^0 -> undef447, oldX4^0 -> undef448, oldX5^0 -> undef449, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef451, x0^0 -> (0 + undef440), x1^0 -> (0 + undef445), x2^0 -> (0 + undef446), x3^0 -> (0 + undef447), x4^0 -> (0 + undef448), x5^0 -> (0 + undef449), x6^0 -> (0 + undef451)}> undef463, oldX1^0 -> undef468, oldX2^0 -> undef469, oldX3^0 -> undef470, oldX4^0 -> undef471, oldX5^0 -> undef472, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef474, x0^0 -> (0 + undef463), x1^0 -> (0 + undef468), x2^0 -> (0 + undef469), x3^0 -> (0 + undef470), x4^0 -> (0 + undef471), x5^0 -> (0 + undef472), x6^0 -> (0 + undef474)}> undef486, oldX1^0 -> undef491, oldX2^0 -> undef492, oldX3^0 -> undef493, oldX4^0 -> undef494, oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef497, oldX8^0 -> undef498, x0^0 -> (0 + undef486), x1^0 -> (0 + undef491), x2^0 -> (0 + undef492), x3^0 -> (0 + undef493), x4^0 -> ((0 + (~(1) * __const_32^0)) + undef494), x5^0 -> (0 + undef497), x6^0 -> (0 + undef498)}> undef509, oldX1^0 -> undef514, oldX2^0 -> undef515, oldX3^0 -> undef516, oldX4^0 -> undef517, oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef520, x0^0 -> (0 + undef509), x1^0 -> (0 + undef514), x2^0 -> (0 + undef515), x3^0 -> (0 + undef516), x4^0 -> (0 + undef517), x5^0 -> (0 + undef517), x6^0 -> (0 + undef520)}> undef532, oldX1^0 -> undef537, oldX2^0 -> undef538, oldX3^0 -> undef539, oldX4^0 -> undef540, oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef543, oldX8^0 -> undef544, x0^0 -> (0 + undef532), x1^0 -> (0 + undef537), x2^0 -> (0 + undef538), x3^0 -> (0 + undef539), x4^0 -> (0 + undef540), x5^0 -> (0 + undef543), x6^0 -> (0 + undef544)}> undef555, oldX10^0 -> undef556, oldX1^0 -> undef560, oldX2^0 -> (0 + x2^0), oldX3^0 -> undef562, oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef566, oldX8^0 -> undef567, oldX9^0 -> undef568, x0^0 -> (0 + undef555), x1^0 -> (0 + undef560), x2^0 -> (0 + undef566), x3^0 -> (~(1) + undef562), x4^0 -> (0 + undef567), x5^0 -> (0 + undef568), x6^0 -> (0 + undef556)}> undef578, oldX10^0 -> undef579, oldX1^0 -> undef583, oldX2^0 -> (0 + x2^0), oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef589, oldX8^0 -> undef590, oldX9^0 -> undef591, x0^0 -> (0 + undef578), x1^0 -> (0 + undef583), x2^0 -> (0 + undef583), x3^0 -> (0 + undef589), x4^0 -> (0 + undef590), x5^0 -> (0 + undef591), x6^0 -> (0 + undef579)}> undef601, oldX10^0 -> undef602, oldX1^0 -> undef606, oldX2^0 -> undef607, oldX3^0 -> undef608, oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef612, oldX8^0 -> undef613, oldX9^0 -> undef614, x0^0 -> (0 + undef601), x1^0 -> (0 + undef606), x2^0 -> (0 + undef607), x3^0 -> (0 + undef608), x4^0 -> (0 + undef612), x5^0 -> (0 + undef613), x6^0 -> (0 + undef614)}> undef624, oldX10^0 -> undef625, oldX1^0 -> undef629, oldX2^0 -> undef630, oldX3^0 -> undef631, oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef635, oldX8^0 -> undef636, oldX9^0 -> undef637, x0^0 -> (0 + undef624), x1^0 -> (0 + undef629), x2^0 -> (0 + undef630), x3^0 -> (0 + undef631), x4^0 -> (0 + undef635), x5^0 -> (0 + undef636), x6^0 -> (0 + undef637)}> undef647, oldX10^0 -> undef648, oldX1^0 -> undef652, oldX2^0 -> undef653, oldX3^0 -> undef654, oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef658, oldX8^0 -> undef659, oldX9^0 -> undef660, x0^0 -> (0 + undef647), x1^0 -> (0 + undef652), x2^0 -> (0 + undef653), x3^0 -> (0 + undef654), x4^0 -> (0 + undef658), x5^0 -> (0 + undef659), x6^0 -> (0 + undef660)}> undef670, oldX1^0 -> undef675, oldX2^0 -> undef676, oldX3^0 -> undef677, oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef681, oldX8^0 -> undef682, x0^0 -> (0 + undef670), x1^0 -> (0 + undef675), x2^0 -> (0 + undef676), x3^0 -> (0 + undef677), x4^0 -> (0 + undef677), x5^0 -> (0 + undef681), x6^0 -> (0 + undef682)}> undef693, oldX1^0 -> undef698, oldX2^0 -> undef699, oldX3^0 -> undef700, oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef704, oldX8^0 -> undef705, oldX9^0 -> undef706, x0^0 -> (0 + undef693), x1^0 -> (0 + undef698), x2^0 -> (0 + undef699), x3^0 -> (0 + undef700), x4^0 -> (0 + undef704), x5^0 -> (0 + undef705), x6^0 -> (0 + undef706)}> undef716, oldX1^0 -> undef721, oldX2^0 -> undef722, oldX3^0 -> undef723, oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef727, oldX8^0 -> undef728, oldX9^0 -> undef729, x0^0 -> (0 + undef716), x1^0 -> (0 + undef721), x2^0 -> (0 + undef722), x3^0 -> (0 + undef723), x4^0 -> (0 + undef727), x5^0 -> (0 + undef728), x6^0 -> (0 + undef729)}> undef739, oldX10^0 -> undef740, oldX11^0 -> undef741, oldX12^0 -> undef742, oldX13^0 -> undef743, oldX1^0 -> undef744, oldX2^0 -> (0 + x2^0), oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef750, oldX8^0 -> undef751, oldX9^0 -> undef752, x0^0 -> (0 + undef739), x1^0 -> (0 + undef744), x2^0 -> ((((~(1) + (~(1) * undef740)) + (~(1) * undef750)) + (~(1) * undef751)) + (~(1) * undef752)), x3^0 -> (0 + undef744), x4^0 -> (0 + undef741), x5^0 -> (0 + undef742), x6^0 -> (0 + undef743)}> (0 + x0^0), oldX10^0 -> undef763, oldX11^0 -> undef764, oldX12^0 -> undef765, oldX13^0 -> undef766, oldX1^0 -> (0 + x1^0), oldX2^0 -> (0 + x2^0), oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef773, oldX8^0 -> undef774, oldX9^0 -> undef775, x0^0 -> (0 + undef773), x1^0 -> (0 + undef774), x2^0 -> (0 + undef775), x3^0 -> (0 + undef763), x4^0 -> (0 + undef764), x5^0 -> (0 + undef765), x6^0 -> (0 + undef766)}> undef785, oldX1^0 -> undef790, oldX2^0 -> undef791, oldX3^0 -> undef792, oldX4^0 -> undef793, oldX5^0 -> undef794, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef796, x0^0 -> (0 + undef785), x1^0 -> (0 + undef790), x2^0 -> (0 + undef791), x3^0 -> (0 + undef792), x4^0 -> (0 + undef793), x5^0 -> (0 + undef794), x6^0 -> (0 + undef796)}> undef808, oldX1^0 -> undef813, oldX2^0 -> undef814, oldX3^0 -> undef815, oldX4^0 -> undef816, oldX5^0 -> undef817, oldX6^0 -> (0 + x6^0), oldX7^0 -> undef819, x0^0 -> (0 + undef808), x1^0 -> (0 + undef813), x2^0 -> (0 + undef814), x3^0 -> (0 + undef815), x4^0 -> (0 + undef816), x5^0 -> (~(1) + undef817), x6^0 -> (0 + undef819)}> undef854, oldX1^0 -> undef859, oldX2^0 -> undef860, oldX3^0 -> undef861, oldX4^0 -> undef862, oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef865, oldX8^0 -> undef866, x0^0 -> (0 + undef854), x1^0 -> (0 + undef859), x2^0 -> (0 + undef860), x3^0 -> (0 + undef861), x4^0 -> (0 + undef862), x5^0 -> (0 + undef865), x6^0 -> (0 + undef866)}> undef877, oldX1^0 -> undef882, oldX2^0 -> undef883, oldX3^0 -> undef884, oldX4^0 -> undef885, oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef888, x0^0 -> (0 + undef877), x1^0 -> (0 + undef882), x2^0 -> (0 + undef883), x3^0 -> (0 + undef884), x4^0 -> (0 + undef885), x5^0 -> (0 + undef885), x6^0 -> (0 + undef888)}> undef900, oldX1^0 -> undef905, oldX2^0 -> undef906, oldX3^0 -> undef907, oldX4^0 -> undef908, oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef911, oldX8^0 -> undef912, x0^0 -> (0 + undef900), x1^0 -> (0 + undef905), x2^0 -> (0 + undef906), x3^0 -> (0 + undef907), x4^0 -> (~(4) + undef908), x5^0 -> (0 + undef911), x6^0 -> (0 + undef912)}> (0 + x0^0), oldX10^0 -> undef924, oldX11^0 -> undef925, oldX12^0 -> undef926, oldX13^0 -> undef927, oldX1^0 -> (0 + x1^0), oldX2^0 -> (0 + x2^0), oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef934, oldX8^0 -> undef935, oldX9^0 -> undef936, x0^0 -> (0 + undef934), x1^0 -> (0 + undef935), x2^0 -> (0 + undef936), x3^0 -> (0 + undef924), x4^0 -> (0 + undef925), x5^0 -> (0 + undef926), x6^0 -> (0 + undef927)}> undef946, oldX10^0 -> undef947, oldX11^0 -> undef948, oldX1^0 -> undef951, oldX2^0 -> (0 + x2^0), oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef957, oldX8^0 -> undef958, oldX9^0 -> undef959, x0^0 -> (0 + undef946), x1^0 -> (0 + undef951), x2^0 -> (0 + undef957), x3^0 -> (0 + undef958), x4^0 -> (0 + undef959), x5^0 -> (0 + undef947), x6^0 -> (0 + undef948)}> undef969, oldX10^0 -> undef970, oldX11^0 -> undef971, oldX1^0 -> undef974, oldX2^0 -> (0 + x2^0), oldX3^0 -> (0 + x3^0), oldX4^0 -> (0 + x4^0), oldX5^0 -> (0 + x5^0), oldX6^0 -> (0 + x6^0), oldX7^0 -> undef980, oldX8^0 -> undef981, oldX9^0 -> undef982, x0^0 -> (0 + undef969), x1^0 -> (0 + undef974), x2^0 -> (0 + undef980), x3^0 -> (0 + undef981), x4^0 -> (0 + undef982), x5^0 -> (0 + undef970), x6^0 -> (0 + undef971)}> Fresh variables: undef3, undef8, undef9, undef10, undef11, undef14, undef15, undef26, undef31, undef32, undef33, undef34, undef37, undef38, undef49, undef54, undef55, undef56, undef60, undef61, undef62, undef72, undef77, undef78, undef79, undef83, undef84, undef95, undef100, undef101, undef102, undef106, undef107, undef108, undef118, undef119, undef123, undef124, undef129, undef130, undef131, undef141, undef142, undef143, undef146, undef147, undef152, undef153, undef154, undef164, undef165, undef166, undef169, undef170, undef175, undef176, undef177, undef187, undef188, undef189, undef192, undef193, undef198, undef199, undef200, undef210, undef215, undef216, undef221, undef222, undef223, undef233, undef234, undef238, undef239, undef244, undef245, undef246, undef256, undef257, undef261, undef262, undef267, undef268, undef269, undef280, undef281, undef282, undef283, undef290, undef291, undef292, undef302, undef307, undef308, undef309, undef310, undef311, undef312, undef325, undef330, undef331, undef332, undef333, undef334, undef335, undef371, undef376, undef377, undef378, undef379, undef380, undef382, undef394, undef399, undef400, undef401, undef402, undef403, undef417, undef422, undef423, undef424, undef425, undef426, undef428, undef440, undef445, undef446, undef447, undef448, undef449, undef451, undef463, undef468, undef469, undef470, undef471, undef472, undef474, undef486, undef491, undef492, undef493, undef494, undef497, undef498, undef509, undef514, undef515, undef516, undef517, undef520, undef532, undef537, undef538, undef539, undef540, undef543, undef544, undef555, undef556, undef560, undef562, undef566, undef567, undef568, undef578, undef579, undef583, undef589, undef590, undef591, undef601, undef602, undef606, undef607, undef608, undef612, undef613, undef614, undef624, undef625, undef629, undef630, undef631, undef635, undef636, undef637, undef647, undef648, undef652, undef653, undef654, undef658, undef659, undef660, undef670, undef675, undef676, undef677, undef681, undef682, undef693, undef698, undef699, undef700, undef704, undef705, undef706, undef716, undef721, undef722, undef723, undef727, undef728, undef729, undef739, undef740, undef741, undef742, undef743, undef744, undef750, undef751, undef752, undef763, undef764, undef765, undef766, undef773, undef774, undef775, undef785, undef790, undef791, undef792, undef793, undef794, undef796, undef808, undef813, undef814, undef815, undef816, undef817, undef819, undef854, undef859, undef860, undef861, undef862, undef865, undef866, undef877, undef882, undef883, undef884, undef885, undef888, undef900, undef905, undef906, undef907, undef908, undef911, undef912, undef924, undef925, undef926, undef927, undef934, undef935, undef936, undef946, undef947, undef948, undef951, undef957, undef958, undef959, undef969, undef970, undef971, undef974, undef980, undef981, undef982, Undef variables: undef3, undef8, undef9, undef10, undef11, undef14, undef15, undef26, undef31, undef32, undef33, undef34, undef37, undef38, undef49, undef54, undef55, undef56, undef60, undef61, undef62, undef72, undef77, undef78, undef79, undef83, undef84, undef95, undef100, undef101, undef102, undef106, undef107, undef108, undef118, undef119, undef123, undef124, undef129, undef130, undef131, undef141, undef142, undef143, undef146, undef147, undef152, undef153, undef154, undef164, undef165, undef166, undef169, undef170, undef175, undef176, undef177, undef187, undef188, undef189, undef192, undef193, undef198, undef199, undef200, undef210, undef215, undef216, undef221, undef222, undef223, undef233, undef234, undef238, undef239, undef244, undef245, undef246, undef256, undef257, undef261, undef262, undef267, undef268, undef269, undef280, undef281, undef282, undef283, undef290, undef291, undef292, undef302, undef307, undef308, undef309, undef310, undef311, undef312, undef325, undef330, undef331, undef332, undef333, undef334, undef335, undef371, undef376, undef377, undef378, undef379, undef380, undef382, undef394, undef399, undef400, undef401, undef402, undef403, undef417, undef422, undef423, undef424, undef425, undef426, undef428, undef440, undef445, undef446, undef447, undef448, undef449, undef451, undef463, undef468, undef469, undef470, undef471, undef472, undef474, undef486, undef491, undef492, undef493, undef494, undef497, undef498, undef509, undef514, undef515, undef516, undef517, undef520, undef532, undef537, undef538, undef539, undef540, undef543, undef544, undef555, undef556, undef560, undef562, undef566, undef567, undef568, undef578, undef579, undef583, undef589, undef590, undef591, undef601, undef602, undef606, undef607, undef608, undef612, undef613, undef614, undef624, undef625, undef629, undef630, undef631, undef635, undef636, undef637, undef647, undef648, undef652, undef653, undef654, undef658, undef659, undef660, undef670, undef675, undef676, undef677, undef681, undef682, undef693, undef698, undef699, undef700, undef704, undef705, undef706, undef716, undef721, undef722, undef723, undef727, undef728, undef729, undef739, undef740, undef741, undef742, undef743, undef744, undef750, undef751, undef752, undef763, undef764, undef765, undef766, undef773, undef774, undef775, undef785, undef790, undef791, undef792, undef793, undef794, undef796, undef808, undef813, undef814, undef815, undef816, undef817, undef819, undef854, undef859, undef860, undef861, undef862, undef865, undef866, undef877, undef882, undef883, undef884, undef885, undef888, undef900, undef905, undef906, undef907, undef908, undef911, undef912, undef924, undef925, undef926, undef927, undef934, undef935, undef936, undef946, undef947, undef948, undef951, undef957, undef958, undef959, undef969, undef970, undef971, undef974, undef980, undef981, undef982, Abstraction variables: Exit nodes: Accepting locations: Asserts: Preprocessed LLVMGraph Init Location: 0 Transitions: (0 + undef934), x1^0 -> (0 + undef935), x2^0 -> (0 + undef936), x3^0 -> (0 + undef924), x4^0 -> (0 + undef925), x5^0 -> (0 + undef926), x6^0 -> (0 + undef927)}> (0 + undef739), x1^0 -> (0 + undef744), x2^0 -> ((((~(1) + (~(1) * undef740)) + (~(1) * undef750)) + (~(1) * undef751)) + (~(1) * undef752)), x3^0 -> (0 + undef744), x4^0 -> (0 + undef741), x5^0 -> (0 + undef742), x6^0 -> (0 + undef743)}> (0 + undef578), x1^0 -> (0 + undef583), x2^0 -> (0 + undef583), x3^0 -> (0 + undef589), x4^0 -> (0 + undef590), x5^0 -> (0 + undef591), x6^0 -> (0 + undef579)}> (0 + undef210), x1^0 -> (0 + undef215), x2^0 -> (0 + undef216), x3^0 -> (0 + undef216), x4^0 -> (0 + undef221), x5^0 -> (0 + undef222), x6^0 -> (0 + undef223)}> (0 + undef290), x1^0 -> (0 + undef291), x2^0 -> (0 + undef292), x3^0 -> (0 + undef280), x4^0 -> (0 + undef281), x5^0 -> (0 + undef282), x6^0 -> (0 + undef283)}> (0 + undef578), x1^0 -> (0 + undef583), x2^0 -> (0 + undef583), x3^0 -> (0 + undef589), x4^0 -> (0 + undef590), x5^0 -> (0 + undef591), x6^0 -> (0 + undef579)}> (0 + undef670), x1^0 -> (0 + undef675), x2^0 -> (0 + undef676), x3^0 -> (0 + undef677), x4^0 -> (0 + undef677), x5^0 -> (0 + undef681), x6^0 -> (0 + undef682)}> (0 + undef739), x1^0 -> (0 + undef744), x2^0 -> ((((~(1) + (~(1) * undef740)) + (~(1) * undef750)) + (~(1) * undef751)) + (~(1) * undef752)), x3^0 -> (0 + undef744), x4^0 -> (0 + undef741), x5^0 -> (0 + undef742), x6^0 -> (0 + undef743)}> (0 + undef773), x1^0 -> (0 + undef774), x2^0 -> (0 + undef775), x3^0 -> (0 + undef763), x4^0 -> (0 + undef764), x5^0 -> (0 + undef765), x6^0 -> (0 + undef766)}> (0 + undef900), x1^0 -> (0 + undef905), x2^0 -> (0 + undef906), x3^0 -> (0 + undef907), x4^0 -> (~(4) + undef908), x5^0 -> (0 + undef911), x6^0 -> (0 + undef912)}> (0 + undef3), x1^0 -> (0 + undef8), x2^0 -> (0 + undef9), x3^0 -> (0 + undef10), x4^0 -> (0 + undef11), x5^0 -> (0 + undef14), x6^0 -> (0 + undef15)}> (0 + undef900), x1^0 -> (0 + undef905), x2^0 -> (0 + undef906), x3^0 -> (0 + undef907), x4^0 -> (~(4) + undef908), x5^0 -> (0 + undef911), x6^0 -> (0 + undef912)}> (0 + undef773), x1^0 -> (0 + undef774), x2^0 -> (0 + undef775), x3^0 -> (0 + undef763), x4^0 -> (0 + undef764), x5^0 -> (0 + undef765), x6^0 -> (0 + undef766)}> (0 + undef877), x1^0 -> (0 + undef882), x2^0 -> (0 + undef883), x3^0 -> (0 + undef884), x4^0 -> (0 + undef885), x5^0 -> (0 + undef885), x6^0 -> (0 + undef888)}> (0 + undef49), x1^0 -> (0 + undef54), x2^0 -> (0 + undef55), x3^0 -> ((0 + (~(1) * __const_32^0)) + undef56), x4^0 -> (0 + undef60), x5^0 -> (0 + undef61), x6^0 -> (0 + undef62)}> (0 + undef72), x1^0 -> (0 + undef77), x2^0 -> (0 + undef78), x3^0 -> (0 + undef79), x4^0 -> (0 + undef79), x5^0 -> (0 + undef83), x6^0 -> (0 + undef84)}> (0 + undef95), x1^0 -> (0 + undef100), x2^0 -> (0 + undef101), x3^0 -> (0 + undef102), x4^0 -> (0 + undef106), x5^0 -> (0 + undef107), x6^0 -> (0 + undef108)}> (0 + undef118), x1^0 -> (0 + undef123), x2^0 -> (~(1) + undef124), x3^0 -> (0 + undef129), x4^0 -> (0 + undef130), x5^0 -> (0 + undef131), x6^0 -> (0 + undef119)}> (0 + undef233), x1^0 -> (0 + undef238), x2^0 -> (0 + undef239), x3^0 -> (0 + undef244), x4^0 -> (0 + undef245), x5^0 -> (0 + undef246), x6^0 -> (0 + undef234)}> (0 + undef210), x1^0 -> (0 + undef215), x2^0 -> (0 + undef216), x3^0 -> (0 + undef216), x4^0 -> (0 + undef221), x5^0 -> (0 + undef222), x6^0 -> (0 + undef223)}> (0 + undef210), x1^0 -> (0 + undef215), x2^0 -> (0 + undef216), x3^0 -> (0 + undef216), x4^0 -> (0 + undef221), x5^0 -> (0 + undef222), x6^0 -> (0 + undef223)}> (0 + undef164), x1^0 -> (0 + undef169), x2^0 -> (0 + undef170), x3^0 -> (0 + undef175), x4^0 -> (0 + undef176), x5^0 -> (0 + undef177), x6^0 -> (0 + undef165)}> (0 + undef187), x1^0 -> (0 + undef192), x2^0 -> (0 + undef193), x3^0 -> (0 + undef198), x4^0 -> (0 + undef199), x5^0 -> (0 + undef200), x6^0 -> (0 + undef188)}> (0 + undef290), x1^0 -> (0 + undef291), x2^0 -> (0 + undef292), x3^0 -> (0 + undef280), x4^0 -> (0 + undef281), x5^0 -> (0 + undef282), x6^0 -> (0 + undef283)}> (0 + undef325), x1^0 -> (0 + undef330), x2^0 -> (0 + undef331), x3^0 -> (0 + undef332), x4^0 -> (0 + undef333), x5^0 -> (0 + undef334), x6^0 -> (~(1) + undef335)}> (0 + undef290), x1^0 -> (0 + undef291), x2^0 -> (0 + undef292), x3^0 -> (0 + undef280), x4^0 -> (0 + undef281), x5^0 -> (0 + undef282), x6^0 -> (0 + undef283)}> (0 + undef394), x1^0 -> (0 + undef399), x2^0 -> (0 + undef400), x3^0 -> (0 + undef401), x4^0 -> (0 + undef402), x5^0 -> (0 + undef403), x6^0 -> (0 + undef403)}> (0 + undef417), x1^0 -> (0 + undef422), x2^0 -> (0 + undef423), x3^0 -> (0 + undef424), x4^0 -> (0 + undef425), x5^0 -> (~(4) + undef426), x6^0 -> (0 + undef428)}> (0 + undef440), x1^0 -> (0 + undef445), x2^0 -> (0 + undef446), x3^0 -> (0 + undef447), x4^0 -> (0 + undef448), x5^0 -> (0 + undef449), x6^0 -> (0 + undef451)}> (0 + undef463), x1^0 -> (0 + undef468), x2^0 -> (0 + undef469), x3^0 -> (0 + undef470), x4^0 -> (0 + undef471), x5^0 -> (0 + undef472), x6^0 -> (0 + undef474)}> (0 + undef486), x1^0 -> (0 + undef491), x2^0 -> (0 + undef492), x3^0 -> (0 + undef493), x4^0 -> ((0 + (~(1) * __const_32^0)) + undef494), x5^0 -> (0 + undef497), x6^0 -> (0 + undef498)}> (0 + undef509), x1^0 -> (0 + undef514), x2^0 -> (0 + undef515), x3^0 -> (0 + undef516), x4^0 -> (0 + undef517), x5^0 -> (0 + undef517), x6^0 -> (0 + undef520)}> (0 + undef532), x1^0 -> (0 + undef537), x2^0 -> (0 + undef538), x3^0 -> (0 + undef539), x4^0 -> (0 + undef540), x5^0 -> (0 + undef543), x6^0 -> (0 + undef544)}> (0 + undef555), x1^0 -> (0 + undef560), x2^0 -> (0 + undef566), x3^0 -> (~(1) + undef562), x4^0 -> (0 + undef567), x5^0 -> (0 + undef568), x6^0 -> (0 + undef556)}> (0 + undef693), x1^0 -> (0 + undef698), x2^0 -> (0 + undef699), x3^0 -> (0 + undef700), x4^0 -> (0 + undef704), x5^0 -> (0 + undef705), x6^0 -> (0 + undef706)}> (0 + undef670), x1^0 -> (0 + undef675), x2^0 -> (0 + undef676), x3^0 -> (0 + undef677), x4^0 -> (0 + undef677), x5^0 -> (0 + undef681), x6^0 -> (0 + undef682)}> (0 + undef670), x1^0 -> (0 + undef675), x2^0 -> (0 + undef676), x3^0 -> (0 + undef677), x4^0 -> (0 + undef677), x5^0 -> (0 + undef681), x6^0 -> (0 + undef682)}> (0 + undef624), x1^0 -> (0 + undef629), x2^0 -> (0 + undef630), x3^0 -> (0 + undef631), x4^0 -> (0 + undef635), x5^0 -> (0 + undef636), x6^0 -> (0 + undef637)}> (0 + undef647), x1^0 -> (0 + undef652), x2^0 -> (0 + undef653), x3^0 -> (0 + undef654), x4^0 -> (0 + undef658), x5^0 -> (0 + undef659), x6^0 -> (0 + undef660)}> (0 + undef773), x1^0 -> (0 + undef774), x2^0 -> (0 + undef775), x3^0 -> (0 + undef763), x4^0 -> (0 + undef764), x5^0 -> (0 + undef765), x6^0 -> (0 + undef766)}> (0 + undef808), x1^0 -> (0 + undef813), x2^0 -> (0 + undef814), x3^0 -> (0 + undef815), x4^0 -> (0 + undef816), x5^0 -> (~(1) + undef817), x6^0 -> (0 + undef819)}> Fresh variables: undef3, undef8, undef9, undef10, undef11, undef14, undef15, undef26, undef31, undef32, undef33, undef34, undef37, undef38, undef49, undef54, undef55, undef56, undef60, undef61, undef62, undef72, undef77, undef78, undef79, undef83, undef84, undef95, undef100, undef101, undef102, undef106, undef107, undef108, undef118, undef119, undef123, undef124, undef129, undef130, undef131, undef141, undef142, undef143, undef146, undef147, undef152, undef153, undef154, undef164, undef165, undef166, undef169, undef170, undef175, undef176, undef177, undef187, undef188, undef189, undef192, undef193, undef198, undef199, undef200, undef210, undef215, undef216, undef221, undef222, undef223, undef233, undef234, undef238, undef239, undef244, undef245, undef246, undef256, undef257, undef261, undef262, undef267, undef268, undef269, undef280, undef281, undef282, undef283, undef290, undef291, undef292, undef302, undef307, undef308, undef309, undef310, undef311, undef312, undef325, undef330, undef331, undef332, undef333, undef334, undef335, undef371, undef376, undef377, undef378, undef379, undef380, undef382, undef394, undef399, undef400, undef401, undef402, undef403, undef417, undef422, undef423, undef424, undef425, undef426, undef428, undef440, undef445, undef446, undef447, undef448, undef449, undef451, undef463, undef468, undef469, undef470, undef471, undef472, undef474, undef486, undef491, undef492, undef493, undef494, undef497, undef498, undef509, undef514, undef515, undef516, undef517, undef520, undef532, undef537, undef538, undef539, undef540, undef543, undef544, undef555, undef556, undef560, undef562, undef566, undef567, undef568, undef578, undef579, undef583, undef589, undef590, undef591, undef601, undef602, undef606, undef607, undef608, undef612, undef613, undef614, undef624, undef625, undef629, undef630, undef631, undef635, undef636, undef637, undef647, undef648, undef652, undef653, undef654, undef658, undef659, undef660, undef670, undef675, undef676, undef677, undef681, undef682, undef693, undef698, undef699, undef700, undef704, undef705, undef706, undef716, undef721, undef722, undef723, undef727, undef728, undef729, undef739, undef740, undef741, undef742, undef743, undef744, undef750, undef751, undef752, undef763, undef764, undef765, undef766, undef773, undef774, undef775, undef785, undef790, undef791, undef792, undef793, undef794, undef796, undef808, undef813, undef814, undef815, undef816, undef817, undef819, undef854, undef859, undef860, undef861, undef862, undef865, undef866, undef877, undef882, undef883, undef884, undef885, undef888, undef900, undef905, undef906, undef907, undef908, undef911, undef912, undef924, undef925, undef926, undef927, undef934, undef935, undef936, undef946, undef947, undef948, undef951, undef957, undef958, undef959, undef969, undef970, undef971, undef974, undef980, undef981, undef982, Undef variables: undef3, undef8, undef9, undef10, undef11, undef14, undef15, undef26, undef31, undef32, undef33, undef34, undef37, undef38, undef49, undef54, undef55, undef56, undef60, undef61, undef62, undef72, undef77, undef78, undef79, undef83, undef84, undef95, undef100, undef101, undef102, undef106, undef107, undef108, undef118, undef119, undef123, undef124, undef129, undef130, undef131, undef141, undef142, undef143, undef146, undef147, undef152, undef153, undef154, undef164, undef165, undef166, undef169, undef170, undef175, undef176, undef177, undef187, undef188, undef189, undef192, undef193, undef198, undef199, undef200, undef210, undef215, undef216, undef221, undef222, undef223, undef233, undef234, undef238, undef239, undef244, undef245, undef246, undef256, undef257, undef261, undef262, undef267, undef268, undef269, undef280, undef281, undef282, undef283, undef290, undef291, undef292, undef302, undef307, undef308, undef309, undef310, undef311, undef312, undef325, undef330, undef331, undef332, undef333, undef334, undef335, undef371, undef376, undef377, undef378, undef379, undef380, undef382, undef394, undef399, undef400, undef401, undef402, undef403, undef417, undef422, undef423, undef424, undef425, undef426, undef428, undef440, undef445, undef446, undef447, undef448, undef449, undef451, undef463, undef468, undef469, undef470, undef471, undef472, undef474, undef486, undef491, undef492, undef493, undef494, undef497, undef498, undef509, undef514, undef515, undef516, undef517, undef520, undef532, undef537, undef538, undef539, undef540, undef543, undef544, undef555, undef556, undef560, undef562, undef566, undef567, undef568, undef578, undef579, undef583, undef589, undef590, undef591, undef601, undef602, undef606, undef607, undef608, undef612, undef613, undef614, undef624, undef625, undef629, undef630, undef631, undef635, undef636, undef637, undef647, undef648, undef652, undef653, undef654, undef658, undef659, undef660, undef670, undef675, undef676, undef677, undef681, undef682, undef693, undef698, undef699, undef700, undef704, undef705, undef706, undef716, undef721, undef722, undef723, undef727, undef728, undef729, undef739, undef740, undef741, undef742, undef743, undef744, undef750, undef751, undef752, undef763, undef764, undef765, undef766, undef773, undef774, undef775, undef785, undef790, undef791, undef792, undef793, undef794, undef796, undef808, undef813, undef814, undef815, undef816, undef817, undef819, undef854, undef859, undef860, undef861, undef862, undef865, undef866, undef877, undef882, undef883, undef884, undef885, undef888, undef900, undef905, undef906, undef907, undef908, undef911, undef912, undef924, undef925, undef926, undef927, undef934, undef935, undef936, undef946, undef947, undef948, undef951, undef957, undef958, undef959, undef969, undef970, undef971, undef974, undef980, undef981, undef982, Abstraction variables: Exit nodes: Accepting locations: Asserts: ************************************************************* ******************************************************************************************* *********************** WORKING TRANSITION SYSTEM (DAG) *********************** ******************************************************************************************* Init Location: 0 Graph 0: Transitions: Variables: Graph 1: Transitions: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> Variables: x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0 Graph 2: Transitions: undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> Variables: __const_32^0, x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0, __const_31^0 Graph 3: Transitions: undef900, x1^0 -> undef905, x2^0 -> undef906, x3^0 -> undef907, x4^0 -> -4 + undef908, x5^0 -> undef911, x6^0 -> undef912, rest remain the same}> Variables: x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0 Graph 4: Transitions: Variables: Graph 5: Transitions: undef808, x1^0 -> undef813, x2^0 -> undef814, x3^0 -> undef815, x4^0 -> undef816, x5^0 -> -1 + undef817, x6^0 -> undef819, rest remain the same}> Variables: x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0 Graph 6: Transitions: Variables: Graph 7: Transitions: undef555, x1^0 -> undef560, x2^0 -> undef566, x3^0 -> -1 + undef562, x4^0 -> undef567, x5^0 -> undef568, x6^0 -> undef556, rest remain the same}> undef693, x1^0 -> undef698, x2^0 -> undef699, x3^0 -> undef700, x4^0 -> undef704, x5^0 -> undef705, x6^0 -> undef706, rest remain the same}> undef624, x1^0 -> undef629, x2^0 -> undef630, x3^0 -> undef631, x4^0 -> undef635, x5^0 -> undef636, x6^0 -> undef637, rest remain the same}> undef647, x1^0 -> undef652, x2^0 -> undef653, x3^0 -> undef654, x4^0 -> undef658, x5^0 -> undef659, x6^0 -> undef660, rest remain the same}> Variables: x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0 Graph 8: Transitions: undef486, x1^0 -> undef491, x2^0 -> undef492, x3^0 -> undef493, x4^0 -> -__const_32^0 + undef494, x5^0 -> undef497, x6^0 -> undef498, rest remain the same}> undef532, x1^0 -> undef537, x2^0 -> undef538, x3^0 -> undef539, x4^0 -> undef540, x5^0 -> undef543, x6^0 -> undef544, rest remain the same}> Variables: __const_32^0, x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0, __const_31^0 Graph 9: Transitions: undef417, x1^0 -> undef422, x2^0 -> undef423, x3^0 -> undef424, x4^0 -> undef425, x5^0 -> -4 + undef426, x6^0 -> undef428, rest remain the same}> undef463, x1^0 -> undef468, x2^0 -> undef469, x3^0 -> undef470, x4^0 -> undef471, x5^0 -> undef472, x6^0 -> undef474, rest remain the same}> Variables: x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0 Graph 10: Transitions: Variables: Graph 11: Transitions: undef325, x1^0 -> undef330, x2^0 -> undef331, x3^0 -> undef332, x4^0 -> undef333, x5^0 -> undef334, x6^0 -> -1 + undef335, rest remain the same}> Variables: x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0 Graph 12: Transitions: Variables: Graph 13: Transitions: Variables: Precedence: Graph 0 Graph 1 undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> Graph 2 undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> Graph 3 undef900, x1^0 -> undef905, x2^0 -> undef906, x3^0 -> undef907, x4^0 -> -4 + undef908, x5^0 -> undef911, x6^0 -> undef912, rest remain the same}> undef72, x1^0 -> undef77, x2^0 -> undef78, x3^0 -> undef79, x4^0 -> undef79, x5^0 -> undef83, x6^0 -> undef84, rest remain the same}> Graph 4 undef3, x1^0 -> undef8, x2^0 -> undef9, x3^0 -> undef10, x4^0 -> undef11, x5^0 -> undef14, x6^0 -> undef15, rest remain the same}> Graph 5 undef877, x1^0 -> undef882, x2^0 -> undef883, x3^0 -> undef884, x4^0 -> undef885, x5^0 -> undef885, x6^0 -> undef888, rest remain the same}> Graph 6 undef773, x1^0 -> undef774, x2^0 -> undef775, x3^0 -> undef763, x4^0 -> undef764, x5^0 -> undef765, x6^0 -> undef766, rest remain the same}> undef773, x1^0 -> undef774, x2^0 -> undef775, x3^0 -> undef763, x4^0 -> undef764, x5^0 -> undef765, x6^0 -> undef766, rest remain the same}> undef773, x1^0 -> undef774, x2^0 -> undef775, x3^0 -> undef763, x4^0 -> undef764, x5^0 -> undef765, x6^0 -> undef766, rest remain the same}> Graph 7 undef739, x1^0 -> undef744, x2^0 -> -1 - undef740 - undef750 - undef751 - undef752, x3^0 -> undef744, x4^0 -> undef741, x5^0 -> undef742, x6^0 -> undef743, rest remain the same}> undef739, x1^0 -> undef744, x2^0 -> -1 - undef740 - undef750 - undef751 - undef752, x3^0 -> undef744, x4^0 -> undef741, x5^0 -> undef742, x6^0 -> undef743, rest remain the same}> Graph 8 undef670, x1^0 -> undef675, x2^0 -> undef676, x3^0 -> undef677, x4^0 -> undef677, x5^0 -> undef681, x6^0 -> undef682, rest remain the same}> undef670, x1^0 -> undef675, x2^0 -> undef676, x3^0 -> undef677, x4^0 -> undef677, x5^0 -> undef681, x6^0 -> undef682, rest remain the same}> undef670, x1^0 -> undef675, x2^0 -> undef676, x3^0 -> undef677, x4^0 -> undef677, x5^0 -> undef681, x6^0 -> undef682, rest remain the same}> Graph 9 undef509, x1^0 -> undef514, x2^0 -> undef515, x3^0 -> undef516, x4^0 -> undef517, x5^0 -> undef517, x6^0 -> undef520, rest remain the same}> Graph 10 undef440, x1^0 -> undef445, x2^0 -> undef446, x3^0 -> undef447, x4^0 -> undef448, x5^0 -> undef449, x6^0 -> undef451, rest remain the same}> Graph 11 undef394, x1^0 -> undef399, x2^0 -> undef400, x3^0 -> undef401, x4^0 -> undef402, x5^0 -> undef403, x6^0 -> undef403, rest remain the same}> Graph 12 undef290, x1^0 -> undef291, x2^0 -> undef292, x3^0 -> undef280, x4^0 -> undef281, x5^0 -> undef282, x6^0 -> undef283, rest remain the same}> undef290, x1^0 -> undef291, x2^0 -> undef292, x3^0 -> undef280, x4^0 -> undef281, x5^0 -> undef282, x6^0 -> undef283, rest remain the same}> undef290, x1^0 -> undef291, x2^0 -> undef292, x3^0 -> undef280, x4^0 -> undef281, x5^0 -> undef282, x6^0 -> undef283, rest remain the same}> Graph 13 undef934, x1^0 -> undef935, x2^0 -> undef936, x3^0 -> undef924, x4^0 -> undef925, x5^0 -> undef926, x6^0 -> undef927, rest remain the same}> Map Locations to Subgraph: ( 0 , 0 ) ( 1 , 3 ) ( 2 , 4 ) ( 4 , 2 ) ( 5 , 2 ) ( 6 , 1 ) ( 7 , 1 ) ( 8 , 1 ) ( 11 , 12 ) ( 12 , 11 ) ( 14 , 10 ) ( 15 , 9 ) ( 16 , 9 ) ( 17 , 8 ) ( 18 , 8 ) ( 19 , 7 ) ( 20 , 7 ) ( 22 , 7 ) ( 26 , 6 ) ( 27 , 5 ) ( 30 , 13 ) ******************************************************************************************* ******************************** CHECKING ASSERTIONS ******************************** ******************************************************************************************* Proving termination of subgraph 0 Proving termination of subgraph 1 Checking unfeasibility... Time used: 0.010173 Checking conditional termination of SCC {l6, l7, l8}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001946s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006716s Trying to remove transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.017697s Time used: 0.017012 Trying to remove transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013965s Time used: 0.011596 Trying to remove transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014469s Time used: 0.012206 Trying to remove transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014178s Time used: 0.011837 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.056310s Time used: 0.053699 Improving Solution with cost 2 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.155443s Time used: 0.15544 LOG: SAT solveNonLinear - Elapsed time: 0.211753s Cost: 2; Total time: 0.209139 Failed at location 6: 0 <= x2^0 Failed at location 8: 0 <= x2^0 Before Improving: Quasi-invariant at l6: 0 <= x2^0 Quasi-invariant at l8: 0 <= x2^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.016235s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004238s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003914s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003871s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003871s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003849s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003878s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003851s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003844s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003889s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003893s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003886s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003880s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003902s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003900s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003880s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003868s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003903s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003907s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003918s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003894s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003911s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003923s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003945s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003934s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003955s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003934s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003922s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003942s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003937s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003921s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003936s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003954s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003939s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003924s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003961s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003967s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003937s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003947s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003972s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003982s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003984s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003974s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003990s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003973s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003976s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003972s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003972s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003963s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003959s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004004s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003988s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003959s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004023s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003977s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004006s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003981s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003993s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003980s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003965s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003981s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003966s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003960s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003970s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003972s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003967s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003989s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004015s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004006s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004020s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003991s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004019s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004026s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004013s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004003s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003984s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003985s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004023s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003984s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003972s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003997s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004061s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004004s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004021s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004008s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004050s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004000s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004034s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004020s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004089s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004009s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003995s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004022s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004012s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004034s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004006s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004005s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004072s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004012s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004019s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004035s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004026s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004026s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004068s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004034s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004031s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004032s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004032s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004012s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004028s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004034s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004069s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004003s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004019s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004019s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004085s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004007s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004062s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004026s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004029s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004048s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004037s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004039s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004031s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004017s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004030s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004022s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004052s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004080s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004062s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004022s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004066s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004048s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004032s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004023s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004031s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004137s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004081s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004041s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004048s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004079s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004110s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004072s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004097s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004072s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004066s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004066s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004071s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004044s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004092s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004078s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004056s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004100s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004147s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004097s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004099s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004057s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004083s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004062s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004093s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004075s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004098s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004063s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004111s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004097s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004110s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004065s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004102s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004092s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004091s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004070s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004115s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004089s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004091s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004078s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004083s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004082s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004106s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004085s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004082s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004104s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004124s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004134s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004129s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004094s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004107s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004098s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004092s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004110s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004095s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004095s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004137s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004109s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004129s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004099s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004097s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004093s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004176s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004106s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004119s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004130s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004110s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004088s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004124s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004141s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004134s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004104s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004140s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004105s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004119s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004144s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004096s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004126s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004111s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004148s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004149s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004132s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004122s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004149s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004117s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004128s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004158s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004116s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004155s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004148s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004108s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004135s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004164s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004134s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004172s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004156s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004169s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004194s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004132s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004193s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004138s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004138s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004148s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004168s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004154s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004125s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004164s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004133s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004148s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004123s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004146s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004150s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004150s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004161s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004173s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004173s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004147s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004144s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004166s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004165s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004245s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004182s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004144s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004167s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004157s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004147s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004154s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004183s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004155s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004170s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004195s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004179s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004174s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004171s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004182s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004197s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004265s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004198s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004195s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004144s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004160s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004201s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004268s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004160s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004209s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002924s Remaining time after improvement: -0.001757 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l6: 0 <= 280 + x2^0 Quasi-invariant at l8: 0 <= 280 + x2^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> Ranking function: 280 + x2^0 New Graphs: Calling Safety with literal 0 <= 280 + x2^0 and entry LOG: CALL check - Post:0 <= 280 + x2^0 - Process 1 * Exit transition: * Postcondition : 0 <= 280 + x2^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000703s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000733s Calling Safety with literal 0 <= 280 + x2^0 and entry LOG: CALL check - Post:0 <= 280 + x2^0 - Process 2 * Exit transition: * Postcondition : 0 <= 280 + x2^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000695s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000719s INVARIANTS: 6: 8: Quasi-INVARIANTS to narrow Graph: 6: 0 <= 280 + x2^0 , 8: 0 <= 280 + x2^0 , Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 It's unfeasible. Removing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> Variables: x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0 Proving termination of subgraph 2 Checking unfeasibility... Time used: 0.00571 Checking conditional termination of SCC {l4, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001599s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004398s Trying to remove transition: undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.008976s Time used: 0.00848 Trying to remove transition: undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.009394s Time used: 0.00813 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.029247s Time used: 0.027826 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.041195s Time used: 0.041192 LOG: SAT solveNonLinear - Elapsed time: 0.070442s Cost: 5; Total time: 0.069018 Failed at location 4: 1 <= 0 Failed at location 5: x3^0 <= __const_31^0 Failed at location 5: x3^0 <= __const_31^0 Failed at location 5: x3^0 <= __const_31^0 Failed at location 5: x3^0 <= __const_31^0 Before Improving: Quasi-invariant at l4: 1 <= 0 Quasi-invariant at l5: x3^0 <= __const_31^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007109s Remaining time after improvement: 0.997877 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: 1 <= 0 Quasi-invariant at l5: x3^0 <= __const_31^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: undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... > It's unfeasible. Removing transition: undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> New Graphs: Calling Safety with literal 1 <= 0 and entry LOG: CALL check - Post:1 <= 0 - Process 3 * Exit transition: * Postcondition : 1 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001139s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001160s Calling Safety with literal x3^0 <= __const_31^0 and entry LOG: CALL check - Post:x3^0 <= __const_31^0 - Process 4 * Exit transition: * Postcondition : x3^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001172s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001199s Calling Safety with literal x3^0 <= __const_31^0 and entry undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> LOG: CALL check - Post:x3^0 <= __const_31^0 - Process 5 * Exit transition: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> * Postcondition : x3^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000826s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000877s Calling Safety with literal x3^0 <= __const_31^0 and entry undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> LOG: CALL check - Post:x3^0 <= __const_31^0 - Process 6 * Exit transition: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> * Postcondition : x3^0 <= __const_31^0 Postcodition moved up: undef216 <= __const_31^0 LOG: Try proving POST Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 7 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000977s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001050s Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 8 * Exit transition: * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000851s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000896s Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 9 * Exit transition: * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000839s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000882s Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 10 * Exit transition: * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000836s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000879s Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 11 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000915s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000977s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> END ENTRIES: GRAPH: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> END GRAPH: EXIT: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> POST: x3^0 <= __const_31^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.040516s Time used: 0.040221 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.030270s Time used: 0.030267 LOG: SAT solveNonLinear - Elapsed time: 0.070786s Cost: 5; Total time: 0.070488 Failed at location 6: x2^0 <= __const_31^0 Failed at location 7: 1 + x2^0 <= __const_31^0 Failed at location 7: 1 + x2^0 <= __const_31^0 Failed at location 7: 1 + x2^0 <= __const_31^0 Failed at location 8: 1 <= __const_31^0 Before Improving: Quasi-invariant at l6: x2^0 <= __const_31^0 Quasi-invariant at l7: 1 + x2^0 <= __const_31^0 Quasi-invariant at l8: 1 <= __const_31^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007610s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002682s Remaining time after improvement: 0.993856 Postcondition implied by a set of quasi-invariant(s): Quasi-invariant at l6: x2^0 <= 1 + __const_31^0 Quasi-invariant at l7: x2^0 <= __const_31^0 Quasi-invariant at l8: 1 <= __const_31^0 Postcondition: x2^0 <= __const_31^0 LOG: CALL check - Post:x2^0 <= __const_31^0 - Process 12 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001313s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001393s Postcondition: x2^0 <= 1 + __const_31^0 LOG: CALL check - Post:x2^0 <= 1 + __const_31^0 - Process 13 * Exit transition: * Postcondition : x2^0 <= 1 + __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000941s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000991s Postcondition: 1 <= __const_31^0 LOG: CALL check - Post:1 <= __const_31^0 - Process 14 * Exit transition: * Postcondition : 1 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000892s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000938s Postcondition: x2^0 <= __const_31^0 LOG: CALL check - Post:x2^0 <= __const_31^0 - Process 15 * Exit transition: * Postcondition : x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000899s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000947s Postcondition: x2^0 <= __const_31^0 LOG: CALL check - Post:x2^0 <= __const_31^0 - Process 16 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000985s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001052s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 INVARIANTS: 6: 7: 8: Quasi-INVARIANTS to narrow Graph: 6: x2^0 <= 1 + __const_31^0 , 7: x2^0 <= __const_31^0 , 8: 1 <= __const_31^0 , Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> END ENTRIES: GRAPH: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> END GRAPH: EXIT: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> POST: x3^0 <= __const_31^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.043971s Time used: 0.043677 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.034372s Time used: 0.034369 LOG: SAT solveNonLinear - Elapsed time: 0.078343s Cost: 5; Total time: 0.078046 Failed at location 6: x2^0 <= 1 + __const_31^0 Failed at location 7: 1 + x2^0 <= __const_31^0 Failed at location 7: 1 + x2^0 <= __const_31^0 Failed at location 7: 1 + x2^0 <= __const_31^0 Failed at location 8: x2^0 <= 1 + __const_31^0 Before Improving: Quasi-invariant at l6: x2^0 <= 1 + __const_31^0 Quasi-invariant at l7: 1 + x2^0 <= __const_31^0 Quasi-invariant at l8: x2^0 <= 1 + __const_31^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009177s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.003956s Remaining time after improvement: 0.991547 Postcondition implied by a set of quasi-invariant(s): Quasi-invariant at l6: x2^0 <= 1 + __const_31^0 Quasi-invariant at l7: x2^0 <= __const_31^0 Quasi-invariant at l8: x2^0 <= 1 + __const_31^0 Postcondition: x2^0 <= __const_31^0 LOG: CALL check - Post:x2^0 <= __const_31^0 - Process 17 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001509s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001598s Postcondition: x2^0 <= 1 + __const_31^0 LOG: CALL check - Post:x2^0 <= 1 + __const_31^0 - Process 18 * Exit transition: * Postcondition : x2^0 <= 1 + __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000984s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001039s Postcondition: x2^0 <= 1 + __const_31^0 LOG: CALL check - Post:x2^0 <= 1 + __const_31^0 - Process 19 * Exit transition: * Postcondition : x2^0 <= 1 + __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000963s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001017s Postcondition: x2^0 <= __const_31^0 LOG: CALL check - Post:x2^0 <= __const_31^0 - Process 20 * Exit transition: * Postcondition : x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000928s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.000980s Postcondition: x2^0 <= __const_31^0 LOG: CALL check - Post:x2^0 <= __const_31^0 - Process 21 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.000997s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001068s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 INVARIANTS: 6: 7: 8: Quasi-INVARIANTS to narrow Graph: 6: x2^0 <= 1 + __const_31^0 , 7: x2^0 <= __const_31^0 , 8: x2^0 <= 1 + __const_31^0 , Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> END ENTRIES: GRAPH: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> END GRAPH: EXIT: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> POST: x3^0 <= __const_31^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.001101s Time used: 4.00101 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.004711s Time used: 4.00002 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.023889s Time used: 1.00002 LOG: Postcondition is not implied - no solution > Postcondition is not implied! LOG: RETURN check - Elapsed time: 9.294922s Calling Safety with literal x3^0 <= __const_31^0 and entry undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> LOG: CALL check - Post:x3^0 <= __const_31^0 - Process 22 * Exit transition: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> * Postcondition : x3^0 <= __const_31^0 Postcodition moved up: undef216 <= __const_31^0 LOG: Try proving POST Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 23 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001247s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001325s Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 24 * Exit transition: * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001142s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001188s Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 25 * Exit transition: * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001073s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001117s Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 26 * Exit transition: * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001114s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001159s Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 27 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001185s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001248s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> END ENTRIES: GRAPH: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> END GRAPH: EXIT: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> POST: x3^0 <= __const_31^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.030473s Time used: 0.030151 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.024107s Time used: 0.024104 LOG: SAT solveNonLinear - Elapsed time: 0.054580s Cost: 5; Total time: 0.054255 Failed at location 6: x2^0 <= 1 + __const_31^0 Failed at location 7: x2^0 <= __const_31^0 Failed at location 7: x2^0 <= __const_31^0 Failed at location 7: x2^0 <= __const_31^0 Failed at location 8: x2^0 <= __const_31^0 Before Improving: Quasi-invariant at l6: x2^0 <= 1 + __const_31^0 Quasi-invariant at l7: x2^0 <= __const_31^0 Quasi-invariant at l8: x2^0 <= __const_31^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006535s Remaining time after improvement: 0.997371 Postcondition implied by a set of quasi-invariant(s): Quasi-invariant at l6: x2^0 <= 1 + __const_31^0 Quasi-invariant at l7: x2^0 <= __const_31^0 Quasi-invariant at l8: x2^0 <= __const_31^0 Postcondition: x2^0 <= __const_31^0 LOG: CALL check - Post:x2^0 <= __const_31^0 - Process 28 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001834s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001917s Postcondition: x2^0 <= 1 + __const_31^0 LOG: CALL check - Post:x2^0 <= 1 + __const_31^0 - Process 29 * Exit transition: * Postcondition : x2^0 <= 1 + __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001724s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001776s Postcondition: x2^0 <= __const_31^0 LOG: CALL check - Post:x2^0 <= __const_31^0 - Process 30 * Exit transition: * Postcondition : x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001128s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001177s Postcondition: x2^0 <= __const_31^0 LOG: CALL check - Post:x2^0 <= __const_31^0 - Process 31 * Exit transition: * Postcondition : x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001116s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001173s Postcondition: x2^0 <= __const_31^0 LOG: CALL check - Post:x2^0 <= __const_31^0 - Process 32 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001202s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001270s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 INVARIANTS: 6: 7: 8: Quasi-INVARIANTS to narrow Graph: 6: x2^0 <= 1 + __const_31^0 , 7: x2^0 <= __const_31^0 , 8: x2^0 <= __const_31^0 , Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> END ENTRIES: GRAPH: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> END GRAPH: EXIT: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> POST: x3^0 <= __const_31^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.035993s Time used: 0.035691 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.037781s Time used: 0.037777 LOG: SAT solveNonLinear - Elapsed time: 0.073774s Cost: 5; Total time: 0.073468 Failed at location 6: 1 <= 0 Failed at location 7: x2^0 <= 0 Failed at location 7: x2^0 <= 0 Failed at location 7: x2^0 <= 0 Failed at location 8: 1 <= 0 Before Improving: Quasi-invariant at l6: 1 <= 0 Quasi-invariant at l7: x2^0 <= 0 Quasi-invariant at l8: 1 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007593s Remaining time after improvement: 0.996467 Postcondition implied by a set of quasi-invariant(s): Quasi-invariant at l6: 1 <= 0 Quasi-invariant at l7: x2^0 <= 0 Quasi-invariant at l8: 1 <= 0 Postcondition: x2^0 <= 0 LOG: CALL check - Post:x2^0 <= 0 - Process 33 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001917s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.002001s Postcondition: 1 <= 0 LOG: CALL check - Post:1 <= 0 - Process 34 * Exit transition: * Postcondition : 1 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001381s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001431s Postcondition: 1 <= 0 LOG: CALL check - Post:1 <= 0 - Process 35 * Exit transition: * Postcondition : 1 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001170s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001227s Postcondition: x2^0 <= 0 LOG: CALL check - Post:x2^0 <= 0 - Process 36 * Exit transition: * Postcondition : x2^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001150s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001203s Postcondition: x2^0 <= 0 LOG: CALL check - Post:x2^0 <= 0 - Process 37 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001238s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001307s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 INVARIANTS: 6: 7: 8: Quasi-INVARIANTS to narrow Graph: 6: 1 <= 0 , 7: x2^0 <= 0 , 8: 1 <= 0 , Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> END ENTRIES: GRAPH: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> END GRAPH: EXIT: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> POST: x3^0 <= __const_31^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.036320s Time used: 0.036012 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.051243s Time used: 0.051241 LOG: SAT solveNonLinear - Elapsed time: 0.087564s Cost: 5; Total time: 0.087253 Failed at location 6: x2^0 <= 0 Failed at location 7: x2^0 <= 0 Failed at location 7: x2^0 <= 0 Failed at location 7: x2^0 <= 0 Failed at location 8: 1 <= 0 Before Improving: Quasi-invariant at l6: x2^0 <= 0 Quasi-invariant at l7: x2^0 <= 0 Quasi-invariant at l8: 1 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009709s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004572s Remaining time after improvement: 0.990607 Postcondition implied by a set of quasi-invariant(s): Quasi-invariant at l6: x2^0 <= 1 Quasi-invariant at l7: x2^0 <= 0 Quasi-invariant at l8: 1 <= 0 Postcondition: x2^0 <= 0 LOG: CALL check - Post:x2^0 <= 0 - Process 38 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001834s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001929s Postcondition: x2^0 <= 1 LOG: CALL check - Post:x2^0 <= 1 - Process 39 * Exit transition: * Postcondition : x2^0 <= 1 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001255s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001311s Postcondition: 1 <= 0 LOG: CALL check - Post:1 <= 0 - Process 40 * Exit transition: * Postcondition : 1 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001159s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001210s Postcondition: x2^0 <= 0 LOG: CALL check - Post:x2^0 <= 0 - Process 41 * Exit transition: * Postcondition : x2^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001144s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001198s Postcondition: x2^0 <= 0 LOG: CALL check - Post:x2^0 <= 0 - Process 42 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001193s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001266s > Postcondition is not implied (too many tries)! LOG: RETURN check - Elapsed time: 0.354014s INVARIANTS: 4: 5: Quasi-INVARIANTS to narrow Graph: 4: 1 <= 0 , 5: x3^0 <= __const_31^0 , Narrowing transition: undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> Variables: __const_32^0, x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0, __const_31^0 Checking conditional termination of SCC {l4, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001277s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.005278s Trying to remove transition: undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.010837s Time used: 0.010138 Trying to remove transition: undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.011311s Time used: 0.009653 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.043996s Time used: 0.042152 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.053395s Time used: 0.053392 LOG: SAT solveNonLinear - Elapsed time: 0.097391s Cost: 5; Total time: 0.095544 Failed at location 4: 1 + x3^0 <= __const_31^0 + __const_32^0 Failed at location 5: x3^0 <= __const_31^0 Failed at location 5: x3^0 <= __const_31^0 Failed at location 5: x3^0 <= __const_31^0 Failed at location 5: x3^0 <= __const_31^0 Before Improving: Quasi-invariant at l4: 1 + x3^0 <= __const_31^0 + __const_32^0 Quasi-invariant at l5: x3^0 <= __const_31^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009531s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002793s Remaining time after improvement: 0.993282 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: x3^0 <= __const_31^0 + __const_32^0 Quasi-invariant at l5: x3^0 <= __const_31^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility It's unfeasible. Removing transition: undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> New Graphs: Calling Safety with literal x3^0 <= __const_31^0 + __const_32^0 and entry LOG: CALL check - Post:x3^0 <= __const_31^0 + __const_32^0 - Process 43 * Exit transition: * Postcondition : x3^0 <= __const_31^0 + __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001063s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001107s Calling Safety with literal x3^0 <= __const_31^0 and entry LOG: CALL check - Post:x3^0 <= __const_31^0 - Process 44 * Exit transition: * Postcondition : x3^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001008s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001039s Calling Safety with literal x3^0 <= __const_31^0 and entry undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> LOG: CALL check - Post:x3^0 <= __const_31^0 - Process 45 * Exit transition: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> * Postcondition : x3^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001185s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001239s Calling Safety with literal x3^0 <= __const_31^0 and entry undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> LOG: CALL check - Post:x3^0 <= __const_31^0 - Process 46 * Exit transition: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> * Postcondition : x3^0 <= __const_31^0 Postcodition moved up: undef216 <= __const_31^0 LOG: Try proving POST Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 47 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001347s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001426s Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 48 * Exit transition: * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001233s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001283s Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 49 * Exit transition: * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001205s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001254s Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 50 * Exit transition: * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001142s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001191s Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 51 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001234s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001302s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> END ENTRIES: GRAPH: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> END GRAPH: EXIT: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> POST: x3^0 <= __const_31^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.036697s Time used: 0.036409 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.031914s Time used: 0.031911 LOG: SAT solveNonLinear - Elapsed time: 0.068611s Cost: 5; Total time: 0.06832 Failed at location 6: 1 <= 0 Failed at location 7: 1 + x2^0 <= __const_31^0 Failed at location 7: 1 + x2^0 <= __const_31^0 Failed at location 7: 1 + x2^0 <= __const_31^0 Failed at location 8: 1 <= __const_31^0 Before Improving: Quasi-invariant at l6: 1 <= 0 Quasi-invariant at l7: 1 + x2^0 <= __const_31^0 Quasi-invariant at l8: 1 <= __const_31^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006727s Remaining time after improvement: 0.997229 Postcondition implied by a set of quasi-invariant(s): Quasi-invariant at l6: 1 <= 0 Quasi-invariant at l7: 1 + x2^0 <= __const_31^0 Quasi-invariant at l8: 1 <= __const_31^0 Postcondition: 1 + x2^0 <= __const_31^0 LOG: CALL check - Post:1 + x2^0 <= __const_31^0 - Process 52 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : 1 + x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001916s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001999s Postcondition: 1 <= 0 LOG: CALL check - Post:1 <= 0 - Process 53 * Exit transition: * Postcondition : 1 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001424s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001473s Postcondition: 1 <= __const_31^0 LOG: CALL check - Post:1 <= __const_31^0 - Process 54 * Exit transition: * Postcondition : 1 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001207s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001254s Postcondition: 1 + x2^0 <= __const_31^0 LOG: CALL check - Post:1 + x2^0 <= __const_31^0 - Process 55 * Exit transition: * Postcondition : 1 + x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001220s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001276s Postcondition: 1 + x2^0 <= __const_31^0 LOG: CALL check - Post:1 + x2^0 <= __const_31^0 - Process 56 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : 1 + x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001314s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001384s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 INVARIANTS: 6: 7: 8: Quasi-INVARIANTS to narrow Graph: 6: 1 <= 0 , 7: 1 + x2^0 <= __const_31^0 , 8: 1 <= __const_31^0 , Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> END ENTRIES: GRAPH: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> END GRAPH: EXIT: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> POST: x3^0 <= __const_31^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.033828s Time used: 0.033521 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.033459s Time used: 0.033457 LOG: SAT solveNonLinear - Elapsed time: 0.067287s Cost: 5; Total time: 0.066978 Failed at location 6: x2^0 <= __const_31^0 Failed at location 7: 1 + x2^0 <= __const_31^0 Failed at location 7: 1 + x2^0 <= __const_31^0 Failed at location 7: 1 + x2^0 <= __const_31^0 Failed at location 8: 1 <= 0 Before Improving: Quasi-invariant at l6: x2^0 <= __const_31^0 Quasi-invariant at l7: 1 + x2^0 <= __const_31^0 Quasi-invariant at l8: 1 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.008048s Remaining time after improvement: 0.996046 Postcondition implied by a set of quasi-invariant(s): Quasi-invariant at l6: x2^0 <= __const_31^0 Quasi-invariant at l7: 1 + x2^0 <= __const_31^0 Quasi-invariant at l8: 1 <= 0 Postcondition: 1 + x2^0 <= __const_31^0 LOG: CALL check - Post:1 + x2^0 <= __const_31^0 - Process 57 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : 1 + x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002013s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.002102s Postcondition: x2^0 <= __const_31^0 LOG: CALL check - Post:x2^0 <= __const_31^0 - Process 58 * Exit transition: * Postcondition : x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001463s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001530s Postcondition: 1 <= 0 LOG: CALL check - Post:1 <= 0 - Process 59 * Exit transition: * Postcondition : 1 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001254s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001304s Postcondition: 1 + x2^0 <= __const_31^0 LOG: CALL check - Post:1 + x2^0 <= __const_31^0 - Process 60 * Exit transition: * Postcondition : 1 + x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001242s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001298s Postcondition: 1 + x2^0 <= __const_31^0 LOG: CALL check - Post:1 + x2^0 <= __const_31^0 - Process 61 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : 1 + x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001313s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001387s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 INVARIANTS: 6: 7: 8: Quasi-INVARIANTS to narrow Graph: 6: x2^0 <= __const_31^0 , 7: 1 + x2^0 <= __const_31^0 , 8: 1 <= 0 , Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> END ENTRIES: GRAPH: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> END GRAPH: EXIT: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> POST: x3^0 <= __const_31^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.042200s Time used: 0.041872 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.035419s Time used: 0.035416 LOG: SAT solveNonLinear - Elapsed time: 0.077619s Cost: 5; Total time: 0.077288 Failed at location 6: 1 + x2^0 <= __const_31^0 Failed at location 7: x2^0 <= __const_31^0 Failed at location 7: x2^0 <= __const_31^0 Failed at location 7: x2^0 <= __const_31^0 Failed at location 8: 1 <= 0 Before Improving: Quasi-invariant at l6: 1 + x2^0 <= __const_31^0 Quasi-invariant at l7: x2^0 <= __const_31^0 Quasi-invariant at l8: 1 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009696s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006278s Remaining time after improvement: 0.989045 Postcondition implied by a set of quasi-invariant(s): Quasi-invariant at l6: x2^0 <= 1 + __const_31^0 Quasi-invariant at l7: x2^0 <= __const_31^0 Quasi-invariant at l8: 1 <= 0 Postcondition: x2^0 <= __const_31^0 LOG: CALL check - Post:x2^0 <= __const_31^0 - Process 62 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001885s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001982s Postcondition: x2^0 <= 1 + __const_31^0 LOG: CALL check - Post:x2^0 <= 1 + __const_31^0 - Process 63 * Exit transition: * Postcondition : x2^0 <= 1 + __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001354s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001416s Postcondition: 1 <= 0 LOG: CALL check - Post:1 <= 0 - Process 64 * Exit transition: * Postcondition : 1 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001263s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001314s Postcondition: x2^0 <= __const_31^0 LOG: CALL check - Post:x2^0 <= __const_31^0 - Process 65 * Exit transition: * Postcondition : x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001248s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001301s Postcondition: x2^0 <= __const_31^0 LOG: CALL check - Post:x2^0 <= __const_31^0 - Process 66 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001331s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001406s > Postcondition is not implied (too many tries)! LOG: RETURN check - Elapsed time: 0.357160s Calling Safety with literal x3^0 <= __const_31^0 and entry undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> LOG: CALL check - Post:x3^0 <= __const_31^0 - Process 67 * Exit transition: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> * Postcondition : x3^0 <= __const_31^0 Postcodition moved up: undef216 <= __const_31^0 LOG: Try proving POST Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 68 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001372s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001455s Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 69 * Exit transition: * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001224s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001273s Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 70 * Exit transition: * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001234s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001282s Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 71 * Exit transition: * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001221s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001269s Postcondition: undef216 <= __const_31^0 LOG: CALL check - Post:undef216 <= __const_31^0 - Process 72 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : undef216 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001330s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001397s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> END ENTRIES: GRAPH: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> END GRAPH: EXIT: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> POST: x3^0 <= __const_31^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.040202s Time used: 0.039912 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.029431s Time used: 0.029427 LOG: SAT solveNonLinear - Elapsed time: 0.069633s Cost: 5; Total time: 0.069339 Failed at location 6: x2^0 <= 1 Failed at location 7: x2^0 <= 0 Failed at location 7: x2^0 <= 0 Failed at location 7: x2^0 <= 0 Failed at location 8: 1 <= 0 Before Improving: Quasi-invariant at l6: x2^0 <= 1 Quasi-invariant at l7: x2^0 <= 0 Quasi-invariant at l8: 1 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007211s Remaining time after improvement: 0.996708 Postcondition implied by a set of quasi-invariant(s): Quasi-invariant at l6: x2^0 <= 1 Quasi-invariant at l7: x2^0 <= 0 Quasi-invariant at l8: 1 <= 0 Postcondition: x2^0 <= 0 LOG: CALL check - Post:x2^0 <= 0 - Process 73 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001927s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.002015s Postcondition: x2^0 <= 1 LOG: CALL check - Post:x2^0 <= 1 - Process 74 * Exit transition: * Postcondition : x2^0 <= 1 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001471s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001521s Postcondition: 1 <= 0 LOG: CALL check - Post:1 <= 0 - Process 75 * Exit transition: * Postcondition : 1 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001234s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001279s Postcondition: x2^0 <= 0 LOG: CALL check - Post:x2^0 <= 0 - Process 76 * Exit transition: * Postcondition : x2^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001211s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001257s Postcondition: x2^0 <= 0 LOG: CALL check - Post:x2^0 <= 0 - Process 77 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001309s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001374s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 INVARIANTS: 6: 7: 8: Quasi-INVARIANTS to narrow Graph: 6: x2^0 <= 1 , 7: x2^0 <= 0 , 8: 1 <= 0 , Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> END ENTRIES: GRAPH: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> END GRAPH: EXIT: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> POST: x3^0 <= __const_31^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.045659s Time used: 0.045321 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.041059s Time used: 0.041056 LOG: SAT solveNonLinear - Elapsed time: 0.086718s Cost: 5; Total time: 0.086377 Failed at location 6: x2^0 <= __const_31^0 Failed at location 7: x2^0 <= __const_31^0 Failed at location 7: x2^0 <= __const_31^0 Failed at location 7: x2^0 <= __const_31^0 Failed at location 8: x2^0 <= __const_31^0 Before Improving: Quasi-invariant at l6: x2^0 <= __const_31^0 Quasi-invariant at l7: x2^0 <= __const_31^0 Quasi-invariant at l8: x2^0 <= __const_31^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010400s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.005689s Remaining time after improvement: 0.988792 Postcondition implied by a set of quasi-invariant(s): Quasi-invariant at l6: x2^0 <= 1 + __const_31^0 Quasi-invariant at l7: x2^0 <= __const_31^0 Quasi-invariant at l8: x2^0 <= __const_31^0 Postcondition: x2^0 <= __const_31^0 LOG: CALL check - Post:x2^0 <= __const_31^0 - Process 78 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001890s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001985s Postcondition: x2^0 <= 1 + __const_31^0 LOG: CALL check - Post:x2^0 <= 1 + __const_31^0 - Process 79 * Exit transition: * Postcondition : x2^0 <= 1 + __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001350s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001407s Postcondition: x2^0 <= __const_31^0 LOG: CALL check - Post:x2^0 <= __const_31^0 - Process 80 * Exit transition: * Postcondition : x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001258s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001314s Postcondition: x2^0 <= __const_31^0 LOG: CALL check - Post:x2^0 <= __const_31^0 - Process 81 * Exit transition: * Postcondition : x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001245s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001301s Postcondition: x2^0 <= __const_31^0 LOG: CALL check - Post:x2^0 <= __const_31^0 - Process 82 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001337s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001411s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 INVARIANTS: 6: 7: 8: Quasi-INVARIANTS to narrow Graph: 6: x2^0 <= 1 + __const_31^0 , 7: x2^0 <= __const_31^0 , 8: x2^0 <= __const_31^0 , Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> END ENTRIES: GRAPH: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> END GRAPH: EXIT: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> POST: x3^0 <= __const_31^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.058410s Time used: 0.058346 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.002418s Time used: 4.00004 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.010354s Time used: 1.00012 LOG: Postcondition is not implied - no solution > Postcondition is not implied! LOG: RETURN check - Elapsed time: 5.371211s INVARIANTS: 4: 5: Quasi-INVARIANTS to narrow Graph: 4: x3^0 <= __const_31^0 + __const_32^0 , 5: x3^0 <= __const_31^0 , Narrowing transition: undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> Variables: __const_32^0, x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0, __const_31^0 Checking conditional termination of SCC {l4, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001494s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.005982s Trying to remove transition: undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.012564s Time used: 0.011746 Trying to remove transition: undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013434s Time used: 0.011814 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.074838s Time used: 0.072783 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.046158s Time used: 0.046155 LOG: SAT solveNonLinear - Elapsed time: 0.120997s Cost: 5; Total time: 0.118938 Failed at location 4: 1 <= __const_32^0 Failed at location 5: 1 <= __const_32^0 Failed at location 5: 1 <= __const_32^0 Failed at location 5: 1 <= __const_32^0 Failed at location 5: 1 <= __const_32^0 Before Improving: Quasi-invariant at l4: 1 <= __const_32^0 Quasi-invariant at l5: 1 <= __const_32^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.008589s Remaining time after improvement: 0.996872 Termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: 1 <= __const_32^0 Quasi-invariant at l5: 1 <= __const_32^0 [ Invariant Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> [ Termination Graph ] Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> Ranking function: -__const_31^0 - __const_32^0 + x3^0 New Graphs: Calling Safety with literal 1 <= __const_32^0 and entry LOG: CALL check - Post:1 <= __const_32^0 - Process 83 * Exit transition: * Postcondition : 1 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001250s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001285s Calling Safety with literal 1 <= __const_32^0 and entry LOG: CALL check - Post:1 <= __const_32^0 - Process 84 * Exit transition: * Postcondition : 1 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001233s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001261s Calling Safety with literal 1 <= __const_32^0 and entry undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> LOG: CALL check - Post:1 <= __const_32^0 - Process 85 * Exit transition: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> * Postcondition : 1 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001346s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001397s Calling Safety with literal 1 <= __const_32^0 and entry undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> LOG: CALL check - Post:1 <= __const_32^0 - Process 86 * Exit transition: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> * Postcondition : 1 <= __const_32^0 Postcodition moved up: 1 <= __const_32^0 LOG: Try proving POST Postcondition: 1 <= __const_32^0 LOG: CALL check - Post:1 <= __const_32^0 - Process 87 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : 1 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001521s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001598s Postcondition: 1 <= __const_32^0 LOG: CALL check - Post:1 <= __const_32^0 - Process 88 * Exit transition: * Postcondition : 1 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001360s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001407s Postcondition: 1 <= __const_32^0 LOG: CALL check - Post:1 <= __const_32^0 - Process 89 * Exit transition: * Postcondition : 1 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001400s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001446s Postcondition: 1 <= __const_32^0 LOG: CALL check - Post:1 <= __const_32^0 - Process 90 * Exit transition: * Postcondition : 1 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001376s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001422s Postcondition: 1 <= __const_32^0 LOG: CALL check - Post:1 <= __const_32^0 - Process 91 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : 1 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001501s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001567s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> END ENTRIES: GRAPH: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> END GRAPH: EXIT: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> POST: 1 <= __const_32^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.042736s Time used: 0.042387 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.040178s Time used: 0.040176 LOG: SAT solveNonLinear - Elapsed time: 0.082914s Cost: 5; Total time: 0.082563 Failed at location 6: 1 <= 0 Failed at location 7: 1 + x2^0 <= __const_31^0 Failed at location 7: 1 + x2^0 <= __const_31^0 Failed at location 7: 1 + x2^0 <= __const_31^0 Failed at location 8: 1 <= 0 Before Improving: Quasi-invariant at l6: 1 <= 0 Quasi-invariant at l7: 1 + x2^0 <= __const_31^0 Quasi-invariant at l8: 1 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007217s Remaining time after improvement: 0.997312 Postcondition implied by a set of quasi-invariant(s): Quasi-invariant at l6: 1 <= 0 Quasi-invariant at l7: 1 + x2^0 <= __const_31^0 Quasi-invariant at l8: 1 <= 0 Postcondition: 1 + x2^0 <= __const_31^0 LOG: CALL check - Post:1 + x2^0 <= __const_31^0 - Process 92 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : 1 + x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002053s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.002138s Postcondition: 1 <= 0 LOG: CALL check - Post:1 <= 0 - Process 93 * Exit transition: * Postcondition : 1 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001563s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001614s Postcondition: 1 <= 0 LOG: CALL check - Post:1 <= 0 - Process 94 * Exit transition: * Postcondition : 1 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001384s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001431s Postcondition: 1 + x2^0 <= __const_31^0 LOG: CALL check - Post:1 + x2^0 <= __const_31^0 - Process 95 * Exit transition: * Postcondition : 1 + x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001378s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001431s Postcondition: 1 + x2^0 <= __const_31^0 LOG: CALL check - Post:1 + x2^0 <= __const_31^0 - Process 96 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : 1 + x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001466s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001539s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 INVARIANTS: 6: 7: 8: Quasi-INVARIANTS to narrow Graph: 6: 1 <= 0 , 7: 1 + x2^0 <= __const_31^0 , 8: 1 <= 0 , Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> END ENTRIES: GRAPH: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> END GRAPH: EXIT: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> POST: 1 <= __const_32^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.043445s Time used: 0.043062 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.038025s Time used: 0.038022 LOG: SAT solveNonLinear - Elapsed time: 0.081470s Cost: 5; Total time: 0.081084 Failed at location 6: 1 <= __const_31^0 Failed at location 7: x2^0 <= __const_31^0 + __const_32^0 Failed at location 7: x2^0 <= __const_31^0 + __const_32^0 Failed at location 7: x2^0 <= __const_31^0 + __const_32^0 Failed at location 8: 1 <= __const_31^0 Before Improving: Quasi-invariant at l6: 1 <= __const_31^0 Quasi-invariant at l7: x2^0 <= __const_31^0 + __const_32^0 Quasi-invariant at l8: 1 <= __const_31^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009252s Remaining time after improvement: 0.995389 Postcondition implied by a set of quasi-invariant(s): Quasi-invariant at l6: 1 <= __const_31^0 Quasi-invariant at l7: x2^0 <= __const_31^0 + __const_32^0 Quasi-invariant at l8: 1 <= __const_31^0 Postcondition: x2^0 <= __const_31^0 + __const_32^0 LOG: CALL check - Post:x2^0 <= __const_31^0 + __const_32^0 - Process 97 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= __const_31^0 + __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002259s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.002355s Postcondition: 1 <= __const_31^0 LOG: CALL check - Post:1 <= __const_31^0 - Process 98 * Exit transition: * Postcondition : 1 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001645s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001702s Postcondition: 1 <= __const_31^0 LOG: CALL check - Post:1 <= __const_31^0 - Process 99 * Exit transition: * Postcondition : 1 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001406s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001461s Postcondition: x2^0 <= __const_31^0 + __const_32^0 LOG: CALL check - Post:x2^0 <= __const_31^0 + __const_32^0 - Process 100 * Exit transition: * Postcondition : x2^0 <= __const_31^0 + __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001415s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001477s Postcondition: x2^0 <= __const_31^0 + __const_32^0 LOG: CALL check - Post:x2^0 <= __const_31^0 + __const_32^0 - Process 101 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= __const_31^0 + __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001535s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001622s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 INVARIANTS: 6: 7: 8: Quasi-INVARIANTS to narrow Graph: 6: 1 <= __const_31^0 , 7: x2^0 <= __const_31^0 + __const_32^0 , 8: 1 <= __const_31^0 , Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> END ENTRIES: GRAPH: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> END GRAPH: EXIT: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> POST: 1 <= __const_32^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.043813s Time used: 0.043388 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.036124s Time used: 0.036121 LOG: SAT solveNonLinear - Elapsed time: 0.079937s Cost: 5; Total time: 0.079509 Failed at location 6: x2^0 <= __const_31^0 + __const_32^0 Failed at location 7: 1 + x2^0 <= __const_31^0 + __const_32^0 Failed at location 7: 1 + x2^0 <= __const_31^0 + __const_32^0 Failed at location 7: 1 + x2^0 <= __const_31^0 + __const_32^0 Failed at location 8: 1 + x2^0 <= __const_31^0 + __const_32^0 Before Improving: Quasi-invariant at l6: x2^0 <= __const_31^0 + __const_32^0 Quasi-invariant at l7: 1 + x2^0 <= __const_31^0 + __const_32^0 Quasi-invariant at l8: 1 + x2^0 <= __const_31^0 + __const_32^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.011101s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.007227s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006978s Remaining time after improvement: 0.98117 Postcondition implied by a set of quasi-invariant(s): Quasi-invariant at l6: x2^0 <= 1 + __const_31^0 + __const_32^0 Quasi-invariant at l7: x2^0 <= __const_31^0 + __const_32^0 Quasi-invariant at l8: x2^0 <= 1 + __const_31^0 + __const_32^0 Postcondition: x2^0 <= __const_31^0 + __const_32^0 LOG: CALL check - Post:x2^0 <= __const_31^0 + __const_32^0 - Process 102 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= __const_31^0 + __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001992s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.002102s Postcondition: x2^0 <= 1 + __const_31^0 + __const_32^0 LOG: CALL check - Post:x2^0 <= 1 + __const_31^0 + __const_32^0 - Process 103 * Exit transition: * Postcondition : x2^0 <= 1 + __const_31^0 + __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001553s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001622s Postcondition: x2^0 <= 1 + __const_31^0 + __const_32^0 LOG: CALL check - Post:x2^0 <= 1 + __const_31^0 + __const_32^0 - Process 104 * Exit transition: * Postcondition : x2^0 <= 1 + __const_31^0 + __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001453s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001518s Postcondition: x2^0 <= __const_31^0 + __const_32^0 LOG: CALL check - Post:x2^0 <= __const_31^0 + __const_32^0 - Process 105 * Exit transition: * Postcondition : x2^0 <= __const_31^0 + __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001391s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001457s Postcondition: x2^0 <= __const_31^0 + __const_32^0 LOG: CALL check - Post:x2^0 <= __const_31^0 + __const_32^0 - Process 106 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= __const_31^0 + __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001400s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001485s > Postcondition is not implied (too many tries)! LOG: RETURN check - Elapsed time: 0.413717s Calling Safety with literal 1 <= __const_32^0 and entry undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> LOG: CALL check - Post:1 <= __const_32^0 - Process 107 * Exit transition: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> * Postcondition : 1 <= __const_32^0 Postcodition moved up: 1 <= __const_32^0 LOG: Try proving POST Postcondition: 1 <= __const_32^0 LOG: CALL check - Post:1 <= __const_32^0 - Process 108 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : 1 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001542s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001624s Postcondition: 1 <= __const_32^0 LOG: CALL check - Post:1 <= __const_32^0 - Process 109 * Exit transition: * Postcondition : 1 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001409s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001455s Postcondition: 1 <= __const_32^0 LOG: CALL check - Post:1 <= __const_32^0 - Process 110 * Exit transition: * Postcondition : 1 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001381s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001427s Postcondition: 1 <= __const_32^0 LOG: CALL check - Post:1 <= __const_32^0 - Process 111 * Exit transition: * Postcondition : 1 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001412s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001458s Postcondition: 1 <= __const_32^0 LOG: CALL check - Post:1 <= __const_32^0 - Process 112 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : 1 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001503s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001567s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> END ENTRIES: GRAPH: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> END GRAPH: EXIT: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> POST: 1 <= __const_32^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.051047s Time used: 0.050699 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.037851s Time used: 0.037847 LOG: SAT solveNonLinear - Elapsed time: 0.088898s Cost: 5; Total time: 0.088546 Failed at location 6: 1 <= __const_32^0 Failed at location 7: 1 + x2^0 <= __const_32^0 Failed at location 7: 1 + x2^0 <= __const_32^0 Failed at location 7: 1 + x2^0 <= __const_32^0 Failed at location 8: 1 <= __const_32^0 Before Improving: Quasi-invariant at l6: 1 <= __const_32^0 Quasi-invariant at l7: 1 + x2^0 <= __const_32^0 Quasi-invariant at l8: 1 <= __const_32^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.009540s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004104s Remaining time after improvement: 0.991511 Postcondition implied by a set of quasi-invariant(s): Quasi-invariant at l6: 1 <= __const_32^0 Quasi-invariant at l7: x2^0 <= __const_32^0 Quasi-invariant at l8: 1 <= __const_32^0 Postcondition: x2^0 <= __const_32^0 LOG: CALL check - Post:x2^0 <= __const_32^0 - Process 113 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001978s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.002070s Postcondition: 1 <= __const_32^0 LOG: CALL check - Post:1 <= __const_32^0 - Process 114 * Exit transition: * Postcondition : 1 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001540s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001593s Postcondition: 1 <= __const_32^0 LOG: CALL check - Post:1 <= __const_32^0 - Process 115 * Exit transition: * Postcondition : 1 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001445s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001496s Postcondition: x2^0 <= __const_32^0 LOG: CALL check - Post:x2^0 <= __const_32^0 - Process 116 * Exit transition: * Postcondition : x2^0 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001456s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001510s Postcondition: x2^0 <= __const_32^0 LOG: CALL check - Post:x2^0 <= __const_32^0 - Process 117 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : x2^0 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001526s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001598s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 INVARIANTS: 6: 7: 8: Quasi-INVARIANTS to narrow Graph: 6: 1 <= __const_32^0 , 7: x2^0 <= __const_32^0 , 8: 1 <= __const_32^0 , Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> END ENTRIES: GRAPH: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> END GRAPH: EXIT: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> POST: 1 <= __const_32^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.045441s Time used: 0.045077 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.039314s Time used: 0.039312 LOG: SAT solveNonLinear - Elapsed time: 0.084756s Cost: 5; Total time: 0.084389 Failed at location 6: 1 + x2^0 <= __const_32^0 Failed at location 7: 1 + x2^0 <= 0 Failed at location 7: 1 + x2^0 <= 0 Failed at location 7: 1 + x2^0 <= 0 Failed at location 8: 1 <= __const_32^0 Before Improving: Quasi-invariant at l6: 1 + x2^0 <= __const_32^0 Quasi-invariant at l7: 1 + x2^0 <= 0 Quasi-invariant at l8: 1 <= __const_32^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010528s Quasi-invariant improved LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.005469s Remaining time after improvement: 0.989489 Postcondition implied by a set of quasi-invariant(s): Quasi-invariant at l6: x2^0 <= __const_32^0 Quasi-invariant at l7: 1 + x2^0 <= 0 Quasi-invariant at l8: 1 <= __const_32^0 Postcondition: 1 + x2^0 <= 0 LOG: CALL check - Post:1 + x2^0 <= 0 - Process 118 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : 1 + x2^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.002089s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.002176s Postcondition: x2^0 <= __const_32^0 LOG: CALL check - Post:x2^0 <= __const_32^0 - Process 119 * Exit transition: * Postcondition : x2^0 <= __const_32^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001552s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001608s Postcondition: 1 <= __const_32^0 LOG: Postcondition is not implied - Post: 1 <= __const_32^0 - Already checked Already checked with failure Postcondition: 1 + x2^0 <= 0 LOG: CALL check - Post:1 + x2^0 <= 0 - Process 120 * Exit transition: * Postcondition : 1 + x2^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001469s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001524s Postcondition: 1 + x2^0 <= 0 LOG: CALL check - Post:1 + x2^0 <= 0 - Process 121 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : 1 + x2^0 <= 0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001518s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001592s LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 LOG: NarrowEntry size 1 INVARIANTS: 6: 7: 8: Quasi-INVARIANTS to narrow Graph: 6: x2^0 <= __const_32^0 , 7: 1 + x2^0 <= 0 , 8: 1 <= __const_32^0 , Narrowing transition: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> LOG: Narrow transition size 1 ENTRIES: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> END ENTRIES: GRAPH: undef118, x1^0 -> undef123, x2^0 -> -1 + undef124, x3^0 -> undef129, x4^0 -> undef130, x5^0 -> undef131, x6^0 -> undef119, rest remain the same}> undef233, x1^0 -> undef238, x2^0 -> undef239, x3^0 -> undef244, x4^0 -> undef245, x5^0 -> undef246, x6^0 -> undef234, rest remain the same}> undef164, x1^0 -> undef169, x2^0 -> undef170, x3^0 -> undef175, x4^0 -> undef176, x5^0 -> undef177, x6^0 -> undef165, rest remain the same}> undef187, x1^0 -> undef192, x2^0 -> undef193, x3^0 -> undef198, x4^0 -> undef199, x5^0 -> undef200, x6^0 -> undef188, rest remain the same}> END GRAPH: EXIT: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> POST: 1 <= __const_32^0 LOG: Try proving POST Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.056546s Time used: 0.056171 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.042150s Time used: 0.042146 LOG: SAT solveNonLinear - Elapsed time: 0.098695s Cost: 5; Total time: 0.098317 Failed at location 6: 1 + x2^0 <= __const_31^0 Failed at location 7: 1 + x2^0 <= __const_31^0 Failed at location 7: 1 + x2^0 <= __const_31^0 Failed at location 7: 1 + x2^0 <= __const_31^0 Failed at location 8: 1 + x2^0 <= __const_31^0 Before Improving: Quasi-invariant at l6: 1 + x2^0 <= __const_31^0 Quasi-invariant at l7: 1 + x2^0 <= __const_31^0 Quasi-invariant at l8: 1 + x2^0 <= __const_31^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 1.004948s Remaining time after improvement: -8.9e-05 Postcondition implied by a set of quasi-invariant(s): Quasi-invariant at l6: 1 + x2^0 <= __const_31^0 Quasi-invariant at l7: 1 + x2^0 <= __const_31^0 Quasi-invariant at l8: 1 + x2^0 <= __const_31^0 Postcondition: 1 + x2^0 <= __const_31^0 LOG: CALL check - Post:1 + x2^0 <= __const_31^0 - Process 122 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : 1 + x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004726s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.004833s Postcondition: 1 + x2^0 <= __const_31^0 LOG: CALL check - Post:1 + x2^0 <= __const_31^0 - Process 123 * Exit transition: * Postcondition : 1 + x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001788s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001850s Postcondition: 1 + x2^0 <= __const_31^0 LOG: CALL check - Post:1 + x2^0 <= __const_31^0 - Process 124 * Exit transition: * Postcondition : 1 + x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001466s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001520s Postcondition: 1 + x2^0 <= __const_31^0 LOG: CALL check - Post:1 + x2^0 <= __const_31^0 - Process 125 * Exit transition: * Postcondition : 1 + x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001475s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001538s Postcondition: 1 + x2^0 <= __const_31^0 LOG: CALL check - Post:1 + x2^0 <= __const_31^0 - Process 126 * Exit transition: undef578, x1^0 -> undef583, x2^0 -> undef583, x3^0 -> undef589, x4^0 -> undef590, x5^0 -> undef591, x6^0 -> undef579, rest remain the same}> * Postcondition : 1 + x2^0 <= __const_31^0 LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001588s > Postcondition is not implied! LOG: RETURN check - Elapsed time: 0.001679s > Postcondition is not implied (too many tries)! LOG: RETURN check - Elapsed time: 1.439247s INVARIANTS: 4: 5: Quasi-INVARIANTS to narrow Graph: 4: 1 <= __const_32^0 , 5: 1 <= __const_32^0 , Narrowing transition: undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> LOG: Narrow transition size 1 Narrowing transition: undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> LOG: Narrow transition size 1 invGraph after Narrowing: Transitions: undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> Variables: __const_32^0, x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0, __const_31^0 Checking conditional termination of SCC {l4, l5}... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.001551s LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.006469s Trying to remove transition: undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.013187s Time used: 0.012319 Trying to remove transition: undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.014368s Time used: 0.012264 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.081457s Time used: 0.079542 Solving with 2 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 4.003260s Time used: 4.00003 Solving with 3 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 1.013207s Time used: 1.00016 Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.023722s Time used: 0.020299 Proving non-termination of subgraph 2 Transitions: undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> Variables: __const_32^0, x0^0, x1^0, x2^0, x3^0, x4^0, x5^0, x6^0, __const_31^0 Checking that every undef value has an assignment... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.004873s Checking conditional non-termination of SCC {l4, l5}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.247001s Time used: 0.245859 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.412147s Time used: 0.412142 LOG: SAT solveNonLinear - Elapsed time: 0.659149s Cost: 5; Total time: 0.658001 Failed at location 4: __const_32^0 <= 0 Before Improving: Quasi-invariant at l4: __const_32^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.011334s Remaining time after improvement: 0.993796 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.012971s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: __const_32^0 <= 0 Strengthening and disabling EXIT transitions... Closed exits from l4: 1 Strengthening exit transition (result): Strengthening exit transition (result): Strengthening exit transition (result): Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> Checking conditional non-termination of SCC {l4, l5}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.321333s Time used: 0.320343 Improving Solution with cost 4 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.073099s Time used: 0.073095 LOG: SAT solveNonLinear - Elapsed time: 0.394431s Cost: 4; Total time: 0.393438 Failed at location 4: 1 + __const_31^0 <= x3^0 Before Improving: Quasi-invariant at l4: 1 + __const_31^0 <= x3^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010776s Remaining time after improvement: 0.993835 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.012810s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l4: 1 + __const_31^0 <= x3^0 Strengthening and disabling EXIT transitions... Closed exits from l4: 1 Strengthening exit transition (result): Strengthening exit transition (result): Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> Checking conditional non-termination of SCC {l4, l5}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.215127s Time used: 0.214164 Improving Solution with cost 5 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.138649s Time used: 0.138644 LOG: SAT solveNonLinear - Elapsed time: 0.353776s Cost: 5; Total time: 0.352808 Failed at location 5: __const_32^0 <= 0 Failed at location 5: __const_32^0 <= 0 Failed at location 5: __const_32^0 <= 0 Failed at location 5: __const_32^0 <= 0 Before Improving: Quasi-invariant at l5: __const_32^0 <= 0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.011345s Remaining time after improvement: 0.993787 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.013047s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l5: __const_32^0 <= 0 Strengthening and disabling EXIT transitions... Closed exits from l5: 1 Strengthening exit transition (result): Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> Checking conditional non-termination of SCC {l4, l5}... EXIT TRANSITIONS: Solving with 1 template(s). LOG: CALL solveNonLinearGetFirstSolution LOG: RETURN solveNonLinearGetFirstSolution - Elapsed time: 0.121970s Time used: 0.120988 Improving Solution with cost 4 ... LOG: CALL solveNonLinearGetNextSolution LOG: RETURN solveNonLinearGetNextSolution - Elapsed time: 0.070884s Time used: 0.07088 LOG: SAT solveNonLinear - Elapsed time: 0.192854s Cost: 4; Total time: 0.191868 Failed at location 5: 1 + __const_31^0 <= x3^0 Failed at location 5: 1 + __const_31^0 <= x3^0 Failed at location 5: 1 + __const_31^0 <= x3^0 Failed at location 5: 1 + __const_31^0 <= x3^0 Before Improving: Quasi-invariant at l5: 1 + __const_31^0 <= x3^0 Optimizing invariants... LOG: CALL solveLinear LOG: RETURN solveLinear - Elapsed time: 0.010708s Remaining time after improvement: 0.993844 Minimizing number of undef constraints... LOG: CALL solveNonLinear LOG: RETURN solveNonLinear - Elapsed time: 0.012487s Number of undef constraints reduced! Non-termination implied by a set of quasi-invariant(s): Quasi-invariant at l5: 1 + __const_31^0 <= x3^0 Strengthening and disabling EXIT transitions... Closed exits from l5: 1 Strengthening and disabling transitions... LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef49, x1^0 -> undef54, x2^0 -> undef55, x3^0 -> -__const_32^0 + undef56, x4^0 -> undef60, x5^0 -> undef61, x6^0 -> undef62, rest remain the same}> LOG: CALL solverLinear in Graph for feasibility LOG: RETURN solveLinear in Graph for feasibility Strengthening transition (result): undef95, x1^0 -> undef100, x2^0 -> undef101, x3^0 -> undef102, x4^0 -> undef106, x5^0 -> undef107, x6^0 -> undef108, rest remain the same}> Calling reachability with... Transition: Conditions: __const_32^0 <= 0, 1 + __const_31^0 <= x3^0, Transition: Conditions: __const_32^0 <= 0, 1 + __const_31^0 <= x3^0, Transition: Conditions: __const_32^0 <= 0, 1 + __const_31^0 <= x3^0, Transition: Conditions: __const_32^0 <= 0, 1 + __const_31^0 <= x3^0, Transition: Conditions: __const_32^0 <= 0, 1 + __const_31^0 <= x3^0, OPEN EXITS: (condsUp: __const_32^0 <= 0) (condsUp: __const_32^0 <= 0) (condsUp: __const_32^0 <= 0) (condsUp: __const_32^0 <= 0) (condsUp: __const_32^0 <= 0) --- Reachability graph --- > Graph without transitions. Calling reachability with... Transition: Conditions: 1 + __const_31^0 <= x3^0, __const_32^0 <= 0, Transition: Conditions: 1 + __const_31^0 <= x3^0, __const_32^0 <= 0, Transition: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> Conditions: 1 + __const_31^0 <= x3^0, __const_32^0 <= 0, Transition: Conditions: 1 + __const_31^0 <= x3^0, __const_32^0 <= 0, Transition: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> Conditions: 1 + __const_31^0 <= x3^0, __const_32^0 <= 0, Transition: Conditions: 1 + __const_31^0 <= x3^0, __const_32^0 <= 0, Transition: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> Conditions: 1 + __const_31^0 <= x3^0, __const_32^0 <= 0, Transition: Conditions: 1 + __const_31^0 <= x3^0, __const_32^0 <= 0, Transition: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> Conditions: 1 + __const_31^0 <= x3^0, __const_32^0 <= 0, OPEN EXITS: undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> undef210, x1^0 -> undef215, x2^0 -> undef216, x3^0 -> undef216, x4^0 -> undef221, x5^0 -> undef222, x6^0 -> undef223, rest remain the same}> > Conditions are reachable! Program does NOT terminate