NO Initial ITS Start location: l9 Program variables: __const_10^0 __const_12^0 __const_30^0 __const_5^0 a4^0 a^0 answer^0 b5^0 b^0 ret_complex6^0 0: l0 -> l1 : __const_10^0'=__const_10^post1, __const_12^0'=__const_12^post1, __const_30^0'=__const_30^post1, __const_5^0'=__const_5^post1, a4^0'=a4^post1, a^0'=a^post1, answer^0'=answer^post1, b5^0'=b5^post1, b^0'=b^post1, ret_complex6^0'=ret_complex6^post1, (answer^post1-ret_complex6^post1 == 0 /\ -__const_5^post1+__const_5^0 == 0 /\ __const_30^0-__const_30^post1 == 0 /\ __const_30^0-a4^0 <= 0 /\ b^0-b^post1 == 0 /\ __const_12^0-__const_12^post1 == 0 /\ a^0-a^post1 == 0 /\ -a4^post1+a4^0 == 0 /\ -__const_10^post1+__const_10^0 == 0 /\ -1+ret_complex6^post1 == 0 /\ -b5^post1+b5^0 == 0), cost: 1 1: l0 -> l2 : __const_10^0'=__const_10^post2, __const_12^0'=__const_12^post2, __const_30^0'=__const_30^post2, __const_5^0'=__const_5^post2, a4^0'=a4^post2, a^0'=a^post2, answer^0'=answer^post2, b5^0'=b5^post2, b^0'=b^post2, ret_complex6^0'=ret_complex6^post2, (-a4^post2+a4^0 == 0 /\ -ret_complex6^post2+ret_complex6^0 == 0 /\ __const_12^0-__const_12^post2 == 0 /\ 1-__const_30^0+a4^0 <= 0 /\ __const_30^0-__const_30^post2 == 0 /\ -__const_5^post2+__const_5^0 == 0 /\ b^0-b^post2 == 0 /\ a^0-a^post2 == 0 /\ -__const_10^post2+__const_10^0 == 0 /\ -b5^post2+b5^0 == 0 /\ -answer^post2+answer^0 == 0), cost: 1 3: l2 -> l4 : __const_10^0'=__const_10^post4, __const_12^0'=__const_12^post4, __const_30^0'=__const_30^post4, __const_5^0'=__const_5^post4, a4^0'=a4^post4, a^0'=a^post4, answer^0'=answer^post4, b5^0'=b5^post4, b^0'=b^post4, ret_complex6^0'=ret_complex6^post4, (a^0-a^post4 == 0 /\ -b^post4+b^0 == 0 /\ -ret_complex6^post4+ret_complex6^0 == 0 /\ __const_5^0-__const_5^post4 == 0 /\ -b5^post4+b5^0 == 0 /\ __const_12^0-__const_12^post4 == 0 /\ answer^0-answer^post4 == 0 /\ -a4^post4+a4^0 == 0 /\ -__const_30^post4+__const_30^0 == 0 /\ -__const_10^post4+__const_10^0 == 0), cost: 1 2: l3 -> l0 : __const_10^0'=__const_10^post3, __const_12^0'=__const_12^post3, __const_30^0'=__const_30^post3, __const_5^0'=__const_5^post3, a4^0'=a4^post3, a^0'=a^post3, answer^0'=answer^post3, b5^0'=b5^post3, b^0'=b^post3, ret_complex6^0'=ret_complex6^post3, (-a4^post3+a4^0 == 0 /\ __const_30^0-__const_30^post3 == 0 /\ -b5^post3+b5^0 == 0 /\ __const_12^0-__const_12^post3 == 0 /\ -ret_complex6^post3+ret_complex6^0 == 0 /\ -__const_10^post3+__const_10^0 == 0 /\ -answer^post3+answer^0 == 0 /\ b^0-b^post3 == 0 /\ a^0-a^post3 == 0 /\ -__const_5^post3+__const_5^0 == 0), cost: 1 10: l4 -> l3 : __const_10^0'=__const_10^post11, __const_12^0'=__const_12^post11, __const_30^0'=__const_30^post11, __const_5^0'=__const_5^post11, a4^0'=a4^post11, a^0'=a^post11, answer^0'=answer^post11, b5^0'=b5^post11, b^0'=b^post11, ret_complex6^0'=ret_complex6^post11, (b5^post11-b5^0+__const_10^0 == 0 /\ -b5^0+a4^0 <= 0 /\ -2+a4^post11-a4^0 == 0 /\ -__const_30^post11+__const_30^0 == 0 /\ ret_complex6^0-ret_complex6^post11 == 0 /\ -__const_10^post11+__const_10^0 == 0 /\ answer^0-answer^post11 == 0 /\ __const_12^0-__const_12^post11 == 0 /\ __const_5^0-__const_5^post11 == 0 /\ a^0-a^post11 == 0 /\ b^0-b^post11 == 0), cost: 1 11: l4 -> l7 : __const_10^0'=__const_10^post12, __const_12^0'=__const_12^post12, __const_30^0'=__const_30^post12, __const_5^0'=__const_5^post12, a4^0'=a4^post12, a^0'=a^post12, answer^0'=answer^post12, b5^0'=b5^post12, b^0'=b^post12, ret_complex6^0'=ret_complex6^post12, (b^0-b^post12 == 0 /\ a^0-a^post12 == 0 /\ -__const_12^post12+__const_12^0 == 0 /\ __const_5^0-__const_5^post12 == 0 /\ ret_complex6^0-ret_complex6^post12 == 0 /\ 1+b5^0-a4^0 <= 0 /\ -b5^post12+b5^0 == 0 /\ answer^0-answer^post12 == 0 /\ -a4^post12+a4^0 == 0 /\ -__const_30^post12+__const_30^0 == 0 /\ -__const_10^post12+__const_10^0 == 0), cost: 1 4: l5 -> l2 : __const_10^0'=__const_10^post5, __const_12^0'=__const_12^post5, __const_30^0'=__const_30^post5, __const_5^0'=__const_5^post5, a4^0'=a4^post5, a^0'=a^post5, answer^0'=answer^post5, b5^0'=b5^post5, b^0'=b^post5, ret_complex6^0'=ret_complex6^post5, (1+__const_12^0-b5^0 <= 0 /\ -__const_30^post5+__const_30^0 == 0 /\ a^0-a^post5 == 0 /\ __const_10^0-__const_10^post5 == 0 /\ -__const_12^post5+__const_12^0 == 0 /\ __const_5^0-__const_5^post5 == 0 /\ ret_complex6^0-ret_complex6^post5 == 0 /\ -1+a4^post5-a4^0 == 0 /\ answer^0-answer^post5 == 0 /\ -b5^post5+b5^0 == 0 /\ b^0-b^post5 == 0), cost: 1 5: l5 -> l2 : __const_10^0'=__const_10^post6, __const_12^0'=__const_12^post6, __const_30^0'=__const_30^post6, __const_5^0'=__const_5^post6, a4^0'=a4^post6, a^0'=a^post6, answer^0'=answer^post6, b5^0'=b5^post6, b^0'=b^post6, ret_complex6^0'=ret_complex6^post6, (-b5^post6+b5^0 == 0 /\ a4^post6-__const_10^0-a4^0 == 0 /\ a^0-a^post6 == 0 /\ ret_complex6^0-ret_complex6^post6 == 0 /\ b^0-b^post6 == 0 /\ -__const_12^0+b5^0 <= 0 /\ __const_5^0-__const_5^post6 == 0 /\ -__const_12^post6+__const_12^0 == 0 /\ -answer^post6+answer^0 == 0 /\ __const_30^0-__const_30^post6 == 0 /\ -__const_10^post6+__const_10^0 == 0), cost: 1 6: l6 -> l2 : __const_10^0'=__const_10^post7, __const_12^0'=__const_12^post7, __const_30^0'=__const_30^post7, __const_5^0'=__const_5^post7, a4^0'=a4^post7, a^0'=a^post7, answer^0'=answer^post7, b5^0'=b5^post7, b^0'=b^post7, ret_complex6^0'=ret_complex6^post7, (__const_30^0-__const_30^post7 == 0 /\ -ret_complex6^post7+ret_complex6^0 == 0 /\ 1+b5^0-__const_10^0 <= 0 /\ __const_12^0-__const_12^post7 == 0 /\ -__const_5^post7+__const_5^0 == 0 /\ b^0-b^post7 == 0 /\ a^0-a^post7 == 0 /\ -1+a4^post7-a4^0 == 0 /\ -b5^post7+b5^0 == 0 /\ -answer^post7+answer^0 == 0 /\ -__const_10^post7+__const_10^0 == 0), cost: 1 7: l6 -> l5 : __const_10^0'=__const_10^post8, __const_12^0'=__const_12^post8, __const_30^0'=__const_30^post8, __const_5^0'=__const_5^post8, a4^0'=a4^post8, a^0'=a^post8, answer^0'=answer^post8, b5^0'=b5^post8, b^0'=b^post8, ret_complex6^0'=ret_complex6^post8, (-b5^0+__const_10^0 <= 0 /\ __const_12^0-__const_12^post8 == 0 /\ -a4^post8+a4^0 == 0 /\ b^0-b^post8 == 0 /\ -__const_5^post8+__const_5^0 == 0 /\ -ret_complex6^post8+ret_complex6^0 == 0 /\ __const_30^0-__const_30^post8 == 0 /\ -__const_10^post8+__const_10^0 == 0 /\ a^0-a^post8 == 0 /\ -answer^post8+answer^0 == 0 /\ -b5^post8+b5^0 == 0), cost: 1 8: l7 -> l6 : __const_10^0'=__const_10^post9, __const_12^0'=__const_12^post9, __const_30^0'=__const_30^post9, __const_5^0'=__const_5^post9, a4^0'=a4^post9, a^0'=a^post9, answer^0'=answer^post9, b5^0'=b5^post9, b^0'=b^post9, ret_complex6^0'=ret_complex6^post9, (-answer^post9+answer^0 == 0 /\ __const_30^0-__const_30^post9 == 0 /\ __const_12^0-__const_12^post9 == 0 /\ -ret_complex6^post9+ret_complex6^0 == 0 /\ a^0-a^post9 == 0 /\ -a4^post9+a4^0 == 0 /\ -__const_5^0+b5^0 <= 0 /\ -__const_10^post9+__const_10^0 == 0 /\ -2+b5^post9-b5^0 == 0 /\ -__const_5^post9+__const_5^0 == 0 /\ b^0-b^post9 == 0), cost: 1 9: l7 -> l6 : __const_10^0'=__const_10^post10, __const_12^0'=__const_12^post10, __const_30^0'=__const_30^post10, __const_5^0'=__const_5^post10, a4^0'=a4^post10, a^0'=a^post10, answer^0'=answer^post10, b5^0'=b5^post10, b^0'=b^post10, ret_complex6^0'=ret_complex6^post10, (0 == 0 /\ a^0-a^post10 == 0 /\ -b^post10+b^0 == 0 /\ __const_5^0-__const_5^post10 == 0 /\ -ret_complex6^post10+ret_complex6^0 == 0 /\ -a4^post10+a4^0 == 0 /\ answer^0-answer^post10 == 0 /\ 1+__const_5^0-b5^0 <= 0 /\ __const_12^0-__const_12^post10 == 0 /\ -__const_30^post10+__const_30^0 == 0 /\ -__const_10^post10+__const_10^0 == 0), cost: 1 12: l8 -> l3 : __const_10^0'=__const_10^post13, __const_12^0'=__const_12^post13, __const_30^0'=__const_30^post13, __const_5^0'=__const_5^post13, a4^0'=a4^post13, a^0'=a^post13, answer^0'=answer^post13, b5^0'=b5^post13, b^0'=b^post13, ret_complex6^0'=ret_complex6^post13, (-__const_10^post13+__const_10^0 == 0 /\ answer^post13 == 0 /\ a4^post13-a^post13 == 0 /\ __const_12^0-__const_12^post13 == 0 /\ -1+b^post13 == 0 /\ -__const_5^post13+__const_5^0 == 0 /\ -ret_complex6^post13+ret_complex6^0 == 0 /\ __const_30^0-__const_30^post13 == 0 /\ -1+a^post13 == 0 /\ b5^post13-b^post13 == 0), cost: 1 13: l9 -> l8 : __const_10^0'=__const_10^post14, __const_12^0'=__const_12^post14, __const_30^0'=__const_30^post14, __const_5^0'=__const_5^post14, a4^0'=a4^post14, a^0'=a^post14, answer^0'=answer^post14, b5^0'=b5^post14, b^0'=b^post14, ret_complex6^0'=ret_complex6^post14, (__const_30^0-__const_30^post14 == 0 /\ __const_12^0-__const_12^post14 == 0 /\ b^0-b^post14 == 0 /\ -ret_complex6^post14+ret_complex6^0 == 0 /\ -a4^post14+a4^0 == 0 /\ -__const_10^post14+__const_10^0 == 0 /\ -answer^post14+answer^0 == 0 /\ -__const_5^post14+__const_5^0 == 0 /\ -b5^post14+b5^0 == 0 /\ a^0-a^post14 == 0), cost: 1 Chained Linear Paths Start location: l9 Program variables: __const_10^0 __const_12^0 __const_30^0 __const_5^0 a4^0 a^0 answer^0 b5^0 b^0 ret_complex6^0 0: l0 -> l1 : __const_10^0'=__const_10^post1, __const_12^0'=__const_12^post1, __const_30^0'=__const_30^post1, __const_5^0'=__const_5^post1, a4^0'=a4^post1, a^0'=a^post1, answer^0'=answer^post1, b5^0'=b5^post1, b^0'=b^post1, ret_complex6^0'=ret_complex6^post1, (answer^post1-ret_complex6^post1 == 0 /\ -__const_5^post1+__const_5^0 == 0 /\ __const_30^0-__const_30^post1 == 0 /\ __const_30^0-a4^0 <= 0 /\ b^0-b^post1 == 0 /\ __const_12^0-__const_12^post1 == 0 /\ a^0-a^post1 == 0 /\ -a4^post1+a4^0 == 0 /\ -__const_10^post1+__const_10^0 == 0 /\ -1+ret_complex6^post1 == 0 /\ -b5^post1+b5^0 == 0), cost: 1 1: l0 -> l2 : __const_10^0'=__const_10^post2, __const_12^0'=__const_12^post2, __const_30^0'=__const_30^post2, __const_5^0'=__const_5^post2, a4^0'=a4^post2, a^0'=a^post2, answer^0'=answer^post2, b5^0'=b5^post2, b^0'=b^post2, ret_complex6^0'=ret_complex6^post2, (-a4^post2+a4^0 == 0 /\ -ret_complex6^post2+ret_complex6^0 == 0 /\ __const_12^0-__const_12^post2 == 0 /\ 1-__const_30^0+a4^0 <= 0 /\ __const_30^0-__const_30^post2 == 0 /\ -__const_5^post2+__const_5^0 == 0 /\ b^0-b^post2 == 0 /\ a^0-a^post2 == 0 /\ -__const_10^post2+__const_10^0 == 0 /\ -b5^post2+b5^0 == 0 /\ -answer^post2+answer^0 == 0), cost: 1 3: l2 -> l4 : __const_10^0'=__const_10^post4, __const_12^0'=__const_12^post4, __const_30^0'=__const_30^post4, __const_5^0'=__const_5^post4, a4^0'=a4^post4, a^0'=a^post4, answer^0'=answer^post4, b5^0'=b5^post4, b^0'=b^post4, ret_complex6^0'=ret_complex6^post4, (a^0-a^post4 == 0 /\ -b^post4+b^0 == 0 /\ -ret_complex6^post4+ret_complex6^0 == 0 /\ __const_5^0-__const_5^post4 == 0 /\ -b5^post4+b5^0 == 0 /\ __const_12^0-__const_12^post4 == 0 /\ answer^0-answer^post4 == 0 /\ -a4^post4+a4^0 == 0 /\ -__const_30^post4+__const_30^0 == 0 /\ -__const_10^post4+__const_10^0 == 0), cost: 1 2: l3 -> l0 : __const_10^0'=__const_10^post3, __const_12^0'=__const_12^post3, __const_30^0'=__const_30^post3, __const_5^0'=__const_5^post3, a4^0'=a4^post3, a^0'=a^post3, answer^0'=answer^post3, b5^0'=b5^post3, b^0'=b^post3, ret_complex6^0'=ret_complex6^post3, (-a4^post3+a4^0 == 0 /\ __const_30^0-__const_30^post3 == 0 /\ -b5^post3+b5^0 == 0 /\ __const_12^0-__const_12^post3 == 0 /\ -ret_complex6^post3+ret_complex6^0 == 0 /\ -__const_10^post3+__const_10^0 == 0 /\ -answer^post3+answer^0 == 0 /\ b^0-b^post3 == 0 /\ a^0-a^post3 == 0 /\ -__const_5^post3+__const_5^0 == 0), cost: 1 10: l4 -> l3 : __const_10^0'=__const_10^post11, __const_12^0'=__const_12^post11, __const_30^0'=__const_30^post11, __const_5^0'=__const_5^post11, a4^0'=a4^post11, a^0'=a^post11, answer^0'=answer^post11, b5^0'=b5^post11, b^0'=b^post11, ret_complex6^0'=ret_complex6^post11, (b5^post11-b5^0+__const_10^0 == 0 /\ -b5^0+a4^0 <= 0 /\ -2+a4^post11-a4^0 == 0 /\ -__const_30^post11+__const_30^0 == 0 /\ ret_complex6^0-ret_complex6^post11 == 0 /\ -__const_10^post11+__const_10^0 == 0 /\ answer^0-answer^post11 == 0 /\ __const_12^0-__const_12^post11 == 0 /\ __const_5^0-__const_5^post11 == 0 /\ a^0-a^post11 == 0 /\ b^0-b^post11 == 0), cost: 1 11: l4 -> l7 : __const_10^0'=__const_10^post12, __const_12^0'=__const_12^post12, __const_30^0'=__const_30^post12, __const_5^0'=__const_5^post12, a4^0'=a4^post12, a^0'=a^post12, answer^0'=answer^post12, b5^0'=b5^post12, b^0'=b^post12, ret_complex6^0'=ret_complex6^post12, (b^0-b^post12 == 0 /\ a^0-a^post12 == 0 /\ -__const_12^post12+__const_12^0 == 0 /\ __const_5^0-__const_5^post12 == 0 /\ ret_complex6^0-ret_complex6^post12 == 0 /\ 1+b5^0-a4^0 <= 0 /\ -b5^post12+b5^0 == 0 /\ answer^0-answer^post12 == 0 /\ -a4^post12+a4^0 == 0 /\ -__const_30^post12+__const_30^0 == 0 /\ -__const_10^post12+__const_10^0 == 0), cost: 1 4: l5 -> l2 : __const_10^0'=__const_10^post5, __const_12^0'=__const_12^post5, __const_30^0'=__const_30^post5, __const_5^0'=__const_5^post5, a4^0'=a4^post5, a^0'=a^post5, answer^0'=answer^post5, b5^0'=b5^post5, b^0'=b^post5, ret_complex6^0'=ret_complex6^post5, (1+__const_12^0-b5^0 <= 0 /\ -__const_30^post5+__const_30^0 == 0 /\ a^0-a^post5 == 0 /\ __const_10^0-__const_10^post5 == 0 /\ -__const_12^post5+__const_12^0 == 0 /\ __const_5^0-__const_5^post5 == 0 /\ ret_complex6^0-ret_complex6^post5 == 0 /\ -1+a4^post5-a4^0 == 0 /\ answer^0-answer^post5 == 0 /\ -b5^post5+b5^0 == 0 /\ b^0-b^post5 == 0), cost: 1 5: l5 -> l2 : __const_10^0'=__const_10^post6, __const_12^0'=__const_12^post6, __const_30^0'=__const_30^post6, __const_5^0'=__const_5^post6, a4^0'=a4^post6, a^0'=a^post6, answer^0'=answer^post6, b5^0'=b5^post6, b^0'=b^post6, ret_complex6^0'=ret_complex6^post6, (-b5^post6+b5^0 == 0 /\ a4^post6-__const_10^0-a4^0 == 0 /\ a^0-a^post6 == 0 /\ ret_complex6^0-ret_complex6^post6 == 0 /\ b^0-b^post6 == 0 /\ -__const_12^0+b5^0 <= 0 /\ __const_5^0-__const_5^post6 == 0 /\ -__const_12^post6+__const_12^0 == 0 /\ -answer^post6+answer^0 == 0 /\ __const_30^0-__const_30^post6 == 0 /\ -__const_10^post6+__const_10^0 == 0), cost: 1 6: l6 -> l2 : __const_10^0'=__const_10^post7, __const_12^0'=__const_12^post7, __const_30^0'=__const_30^post7, __const_5^0'=__const_5^post7, a4^0'=a4^post7, a^0'=a^post7, answer^0'=answer^post7, b5^0'=b5^post7, b^0'=b^post7, ret_complex6^0'=ret_complex6^post7, (__const_30^0-__const_30^post7 == 0 /\ -ret_complex6^post7+ret_complex6^0 == 0 /\ 1+b5^0-__const_10^0 <= 0 /\ __const_12^0-__const_12^post7 == 0 /\ -__const_5^post7+__const_5^0 == 0 /\ b^0-b^post7 == 0 /\ a^0-a^post7 == 0 /\ -1+a4^post7-a4^0 == 0 /\ -b5^post7+b5^0 == 0 /\ -answer^post7+answer^0 == 0 /\ -__const_10^post7+__const_10^0 == 0), cost: 1 7: l6 -> l5 : __const_10^0'=__const_10^post8, __const_12^0'=__const_12^post8, __const_30^0'=__const_30^post8, __const_5^0'=__const_5^post8, a4^0'=a4^post8, a^0'=a^post8, answer^0'=answer^post8, b5^0'=b5^post8, b^0'=b^post8, ret_complex6^0'=ret_complex6^post8, (-b5^0+__const_10^0 <= 0 /\ __const_12^0-__const_12^post8 == 0 /\ -a4^post8+a4^0 == 0 /\ b^0-b^post8 == 0 /\ -__const_5^post8+__const_5^0 == 0 /\ -ret_complex6^post8+ret_complex6^0 == 0 /\ __const_30^0-__const_30^post8 == 0 /\ -__const_10^post8+__const_10^0 == 0 /\ a^0-a^post8 == 0 /\ -answer^post8+answer^0 == 0 /\ -b5^post8+b5^0 == 0), cost: 1 8: l7 -> l6 : __const_10^0'=__const_10^post9, __const_12^0'=__const_12^post9, __const_30^0'=__const_30^post9, __const_5^0'=__const_5^post9, a4^0'=a4^post9, a^0'=a^post9, answer^0'=answer^post9, b5^0'=b5^post9, b^0'=b^post9, ret_complex6^0'=ret_complex6^post9, (-answer^post9+answer^0 == 0 /\ __const_30^0-__const_30^post9 == 0 /\ __const_12^0-__const_12^post9 == 0 /\ -ret_complex6^post9+ret_complex6^0 == 0 /\ a^0-a^post9 == 0 /\ -a4^post9+a4^0 == 0 /\ -__const_5^0+b5^0 <= 0 /\ -__const_10^post9+__const_10^0 == 0 /\ -2+b5^post9-b5^0 == 0 /\ -__const_5^post9+__const_5^0 == 0 /\ b^0-b^post9 == 0), cost: 1 9: l7 -> l6 : __const_10^0'=__const_10^post10, __const_12^0'=__const_12^post10, __const_30^0'=__const_30^post10, __const_5^0'=__const_5^post10, a4^0'=a4^post10, a^0'=a^post10, answer^0'=answer^post10, b5^0'=b5^post10, b^0'=b^post10, ret_complex6^0'=ret_complex6^post10, (0 == 0 /\ a^0-a^post10 == 0 /\ -b^post10+b^0 == 0 /\ __const_5^0-__const_5^post10 == 0 /\ -ret_complex6^post10+ret_complex6^0 == 0 /\ -a4^post10+a4^0 == 0 /\ answer^0-answer^post10 == 0 /\ 1+__const_5^0-b5^0 <= 0 /\ __const_12^0-__const_12^post10 == 0 /\ -__const_30^post10+__const_30^0 == 0 /\ -__const_10^post10+__const_10^0 == 0), cost: 1 14: l9 -> l3 : __const_10^0'=__const_10^post13, __const_12^0'=__const_12^post13, __const_30^0'=__const_30^post13, __const_5^0'=__const_5^post13, a4^0'=a4^post13, a^0'=a^post13, answer^0'=answer^post13, b5^0'=b5^post13, b^0'=b^post13, ret_complex6^0'=ret_complex6^post13, (-__const_5^post13+__const_5^post14 == 0 /\ answer^post13 == 0 /\ a4^post13-a^post13 == 0 /\ __const_30^0-__const_30^post14 == 0 /\ __const_12^0-__const_12^post14 == 0 /\ -__const_12^post13+__const_12^post14 == 0 /\ -1+b^post13 == 0 /\ b^0-b^post14 == 0 /\ ret_complex6^post14-ret_complex6^post13 == 0 /\ -ret_complex6^post14+ret_complex6^0 == 0 /\ -__const_10^post13+__const_10^post14 == 0 /\ -a4^post14+a4^0 == 0 /\ -1+a^post13 == 0 /\ b5^post13-b^post13 == 0 /\ -__const_10^post14+__const_10^0 == 0 /\ -__const_30^post13+__const_30^post14 == 0 /\ -answer^post14+answer^0 == 0 /\ -__const_5^post14+__const_5^0 == 0 /\ -b5^post14+b5^0 == 0 /\ a^0-a^post14 == 0), cost: 1 Eliminating location l8 by chaining: Applied chaining First rule: l9 -> l8 : __const_10^0'=__const_10^post14, __const_12^0'=__const_12^post14, __const_30^0'=__const_30^post14, __const_5^0'=__const_5^post14, a4^0'=a4^post14, a^0'=a^post14, answer^0'=answer^post14, b5^0'=b5^post14, b^0'=b^post14, ret_complex6^0'=ret_complex6^post14, (__const_30^0-__const_30^post14 == 0 /\ __const_12^0-__const_12^post14 == 0 /\ b^0-b^post14 == 0 /\ -ret_complex6^post14+ret_complex6^0 == 0 /\ -a4^post14+a4^0 == 0 /\ -__const_10^post14+__const_10^0 == 0 /\ -answer^post14+answer^0 == 0 /\ -__const_5^post14+__const_5^0 == 0 /\ -b5^post14+b5^0 == 0 /\ a^0-a^post14 == 0), cost: 1 Second rule: l8 -> l3 : __const_10^0'=__const_10^post13, __const_12^0'=__const_12^post13, __const_30^0'=__const_30^post13, __const_5^0'=__const_5^post13, a4^0'=a4^post13, a^0'=a^post13, answer^0'=answer^post13, b5^0'=b5^post13, b^0'=b^post13, ret_complex6^0'=ret_complex6^post13, (-__const_10^post13+__const_10^0 == 0 /\ answer^post13 == 0 /\ a4^post13-a^post13 == 0 /\ __const_12^0-__const_12^post13 == 0 /\ -1+b^post13 == 0 /\ -__const_5^post13+__const_5^0 == 0 /\ -ret_complex6^post13+ret_complex6^0 == 0 /\ __const_30^0-__const_30^post13 == 0 /\ -1+a^post13 == 0 /\ b5^post13-b^post13 == 0), cost: 1 New rule: l9 -> l3 : __const_10^0'=__const_10^post13, __const_12^0'=__const_12^post13, __const_30^0'=__const_30^post13, __const_5^0'=__const_5^post13, a4^0'=a4^post13, a^0'=a^post13, answer^0'=answer^post13, b5^0'=b5^post13, b^0'=b^post13, ret_complex6^0'=ret_complex6^post13, (-__const_5^post13+__const_5^post14 == 0 /\ answer^post13 == 0 /\ a4^post13-a^post13 == 0 /\ __const_30^0-__const_30^post14 == 0 /\ __const_12^0-__const_12^post14 == 0 /\ -__const_12^post13+__const_12^post14 == 0 /\ -1+b^post13 == 0 /\ b^0-b^post14 == 0 /\ ret_complex6^post14-ret_complex6^post13 == 0 /\ -ret_complex6^post14+ret_complex6^0 == 0 /\ -__const_10^post13+__const_10^post14 == 0 /\ -a4^post14+a4^0 == 0 /\ -1+a^post13 == 0 /\ b5^post13-b^post13 == 0 /\ -__const_10^post14+__const_10^0 == 0 /\ -__const_30^post13+__const_30^post14 == 0 /\ -answer^post14+answer^0 == 0 /\ -__const_5^post14+__const_5^0 == 0 /\ -b5^post14+b5^0 == 0 /\ a^0-a^post14 == 0), cost: 1 Applied deletion Removed the following rules: 12 13 Simplified Transitions Start location: l9 Program variables: __const_10^0 __const_12^0 __const_30^0 __const_5^0 a4^0 a^0 answer^0 b5^0 b^0 ret_complex6^0 15: l0 -> l1 : answer^0'=1, ret_complex6^0'=1, __const_30^0-a4^0 <= 0, cost: 1 16: l0 -> l2 : 1-__const_30^0+a4^0 <= 0, cost: 1 18: l2 -> l4 : T, cost: 1 17: l3 -> l0 : T, cost: 1 25: l4 -> l3 : a4^0'=2+a4^0, b5^0'=b5^0-__const_10^0, -b5^0+a4^0 <= 0, cost: 1 26: l4 -> l7 : 1+b5^0-a4^0 <= 0, cost: 1 19: l5 -> l2 : a4^0'=1+a4^0, 1+__const_12^0-b5^0 <= 0, cost: 1 20: l5 -> l2 : a4^0'=__const_10^0+a4^0, -__const_12^0+b5^0 <= 0, cost: 1 21: l6 -> l2 : a4^0'=1+a4^0, 1+b5^0-__const_10^0 <= 0, cost: 1 22: l6 -> l5 : -b5^0+__const_10^0 <= 0, cost: 1 23: l7 -> l6 : b5^0'=2+b5^0, -__const_5^0+b5^0 <= 0, cost: 1 24: l7 -> l6 : b5^0'=b5^post10, 1+__const_5^0-b5^0 <= 0, cost: 1 27: l9 -> l3 : a4^0'=1, a^0'=1, answer^0'=0, b5^0'=1, b^0'=1, T, cost: 1 Propagated Equalities Original rule: l0 -> l1 : __const_10^0'=__const_10^post1, __const_12^0'=__const_12^post1, __const_30^0'=__const_30^post1, __const_5^0'=__const_5^post1, a4^0'=a4^post1, a^0'=a^post1, answer^0'=answer^post1, b5^0'=b5^post1, b^0'=b^post1, ret_complex6^0'=ret_complex6^post1, (answer^post1-ret_complex6^post1 == 0 /\ -__const_5^post1+__const_5^0 == 0 /\ __const_30^0-__const_30^post1 == 0 /\ __const_30^0-a4^0 <= 0 /\ b^0-b^post1 == 0 /\ __const_12^0-__const_12^post1 == 0 /\ a^0-a^post1 == 0 /\ -a4^post1+a4^0 == 0 /\ -__const_10^post1+__const_10^0 == 0 /\ -1+ret_complex6^post1 == 0 /\ -b5^post1+b5^0 == 0), cost: 1 New rule: l0 -> l1 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=1, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=1, (0 == 0 /\ __const_30^0-a4^0 <= 0), cost: 1 propagated equality answer^post1 = ret_complex6^post1 propagated equality __const_5^post1 = __const_5^0 propagated equality __const_30^post1 = __const_30^0 propagated equality b^post1 = b^0 propagated equality __const_12^post1 = __const_12^0 propagated equality a^post1 = a^0 propagated equality a4^post1 = a4^0 propagated equality __const_10^post1 = __const_10^0 propagated equality ret_complex6^post1 = 1 propagated equality b5^post1 = b5^0 Simplified Guard Original rule: l0 -> l1 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=1, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=1, (0 == 0 /\ __const_30^0-a4^0 <= 0), cost: 1 New rule: l0 -> l1 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=1, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=1, __const_30^0-a4^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=1, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=1, __const_30^0-a4^0 <= 0, cost: 1 New rule: l0 -> l1 : answer^0'=1, ret_complex6^0'=1, __const_30^0-a4^0 <= 0, cost: 1 Propagated Equalities Original rule: l0 -> l2 : __const_10^0'=__const_10^post2, __const_12^0'=__const_12^post2, __const_30^0'=__const_30^post2, __const_5^0'=__const_5^post2, a4^0'=a4^post2, a^0'=a^post2, answer^0'=answer^post2, b5^0'=b5^post2, b^0'=b^post2, ret_complex6^0'=ret_complex6^post2, (-a4^post2+a4^0 == 0 /\ -ret_complex6^post2+ret_complex6^0 == 0 /\ __const_12^0-__const_12^post2 == 0 /\ 1-__const_30^0+a4^0 <= 0 /\ __const_30^0-__const_30^post2 == 0 /\ -__const_5^post2+__const_5^0 == 0 /\ b^0-b^post2 == 0 /\ a^0-a^post2 == 0 /\ -__const_10^post2+__const_10^0 == 0 /\ -b5^post2+b5^0 == 0 /\ -answer^post2+answer^0 == 0), cost: 1 New rule: l0 -> l2 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, (0 == 0 /\ 1-__const_30^0+a4^0 <= 0), cost: 1 propagated equality a4^post2 = a4^0 propagated equality ret_complex6^post2 = ret_complex6^0 propagated equality __const_12^post2 = __const_12^0 propagated equality __const_30^post2 = __const_30^0 propagated equality __const_5^post2 = __const_5^0 propagated equality b^post2 = b^0 propagated equality a^post2 = a^0 propagated equality __const_10^post2 = __const_10^0 propagated equality b5^post2 = b5^0 propagated equality answer^post2 = answer^0 Simplified Guard Original rule: l0 -> l2 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, (0 == 0 /\ 1-__const_30^0+a4^0 <= 0), cost: 1 New rule: l0 -> l2 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, 1-__const_30^0+a4^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l0 -> l2 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, 1-__const_30^0+a4^0 <= 0, cost: 1 New rule: l0 -> l2 : 1-__const_30^0+a4^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l0 : __const_10^0'=__const_10^post3, __const_12^0'=__const_12^post3, __const_30^0'=__const_30^post3, __const_5^0'=__const_5^post3, a4^0'=a4^post3, a^0'=a^post3, answer^0'=answer^post3, b5^0'=b5^post3, b^0'=b^post3, ret_complex6^0'=ret_complex6^post3, (-a4^post3+a4^0 == 0 /\ __const_30^0-__const_30^post3 == 0 /\ -b5^post3+b5^0 == 0 /\ __const_12^0-__const_12^post3 == 0 /\ -ret_complex6^post3+ret_complex6^0 == 0 /\ -__const_10^post3+__const_10^0 == 0 /\ -answer^post3+answer^0 == 0 /\ b^0-b^post3 == 0 /\ a^0-a^post3 == 0 /\ -__const_5^post3+__const_5^0 == 0), cost: 1 New rule: l3 -> l0 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, 0 == 0, cost: 1 propagated equality a4^post3 = a4^0 propagated equality __const_30^post3 = __const_30^0 propagated equality b5^post3 = b5^0 propagated equality __const_12^post3 = __const_12^0 propagated equality ret_complex6^post3 = ret_complex6^0 propagated equality __const_10^post3 = __const_10^0 propagated equality answer^post3 = answer^0 propagated equality b^post3 = b^0 propagated equality a^post3 = a^0 propagated equality __const_5^post3 = __const_5^0 Simplified Guard Original rule: l3 -> l0 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, 0 == 0, cost: 1 New rule: l3 -> l0 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, T, cost: 1 Removed Trivial Updates Original rule: l3 -> l0 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, T, cost: 1 New rule: l3 -> l0 : T, cost: 1 Propagated Equalities Original rule: l2 -> l4 : __const_10^0'=__const_10^post4, __const_12^0'=__const_12^post4, __const_30^0'=__const_30^post4, __const_5^0'=__const_5^post4, a4^0'=a4^post4, a^0'=a^post4, answer^0'=answer^post4, b5^0'=b5^post4, b^0'=b^post4, ret_complex6^0'=ret_complex6^post4, (a^0-a^post4 == 0 /\ -b^post4+b^0 == 0 /\ -ret_complex6^post4+ret_complex6^0 == 0 /\ __const_5^0-__const_5^post4 == 0 /\ -b5^post4+b5^0 == 0 /\ __const_12^0-__const_12^post4 == 0 /\ answer^0-answer^post4 == 0 /\ -a4^post4+a4^0 == 0 /\ -__const_30^post4+__const_30^0 == 0 /\ -__const_10^post4+__const_10^0 == 0), cost: 1 New rule: l2 -> l4 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, 0 == 0, cost: 1 propagated equality a^post4 = a^0 propagated equality b^post4 = b^0 propagated equality ret_complex6^post4 = ret_complex6^0 propagated equality __const_5^post4 = __const_5^0 propagated equality b5^post4 = b5^0 propagated equality __const_12^post4 = __const_12^0 propagated equality answer^post4 = answer^0 propagated equality a4^post4 = a4^0 propagated equality __const_30^post4 = __const_30^0 propagated equality __const_10^post4 = __const_10^0 Simplified Guard Original rule: l2 -> l4 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, 0 == 0, cost: 1 New rule: l2 -> l4 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, T, cost: 1 Removed Trivial Updates Original rule: l2 -> l4 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, T, cost: 1 New rule: l2 -> l4 : T, cost: 1 Propagated Equalities Original rule: l5 -> l2 : __const_10^0'=__const_10^post5, __const_12^0'=__const_12^post5, __const_30^0'=__const_30^post5, __const_5^0'=__const_5^post5, a4^0'=a4^post5, a^0'=a^post5, answer^0'=answer^post5, b5^0'=b5^post5, b^0'=b^post5, ret_complex6^0'=ret_complex6^post5, (1+__const_12^0-b5^0 <= 0 /\ -__const_30^post5+__const_30^0 == 0 /\ a^0-a^post5 == 0 /\ __const_10^0-__const_10^post5 == 0 /\ -__const_12^post5+__const_12^0 == 0 /\ __const_5^0-__const_5^post5 == 0 /\ ret_complex6^0-ret_complex6^post5 == 0 /\ -1+a4^post5-a4^0 == 0 /\ answer^0-answer^post5 == 0 /\ -b5^post5+b5^0 == 0 /\ b^0-b^post5 == 0), cost: 1 New rule: l5 -> l2 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=1+a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, (0 == 0 /\ 1+__const_12^0-b5^0 <= 0), cost: 1 propagated equality __const_30^post5 = __const_30^0 propagated equality a^post5 = a^0 propagated equality __const_10^post5 = __const_10^0 propagated equality __const_12^post5 = __const_12^0 propagated equality __const_5^post5 = __const_5^0 propagated equality ret_complex6^post5 = ret_complex6^0 propagated equality a4^post5 = 1+a4^0 propagated equality answer^post5 = answer^0 propagated equality b5^post5 = b5^0 propagated equality b^post5 = b^0 Simplified Guard Original rule: l5 -> l2 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=1+a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, (0 == 0 /\ 1+__const_12^0-b5^0 <= 0), cost: 1 New rule: l5 -> l2 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=1+a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, 1+__const_12^0-b5^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l2 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=1+a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, 1+__const_12^0-b5^0 <= 0, cost: 1 New rule: l5 -> l2 : a4^0'=1+a4^0, 1+__const_12^0-b5^0 <= 0, cost: 1 Propagated Equalities Original rule: l5 -> l2 : __const_10^0'=__const_10^post6, __const_12^0'=__const_12^post6, __const_30^0'=__const_30^post6, __const_5^0'=__const_5^post6, a4^0'=a4^post6, a^0'=a^post6, answer^0'=answer^post6, b5^0'=b5^post6, b^0'=b^post6, ret_complex6^0'=ret_complex6^post6, (-b5^post6+b5^0 == 0 /\ a4^post6-__const_10^0-a4^0 == 0 /\ a^0-a^post6 == 0 /\ ret_complex6^0-ret_complex6^post6 == 0 /\ b^0-b^post6 == 0 /\ -__const_12^0+b5^0 <= 0 /\ __const_5^0-__const_5^post6 == 0 /\ -__const_12^post6+__const_12^0 == 0 /\ -answer^post6+answer^0 == 0 /\ __const_30^0-__const_30^post6 == 0 /\ -__const_10^post6+__const_10^0 == 0), cost: 1 New rule: l5 -> l2 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=__const_10^0+a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, (0 == 0 /\ -__const_12^0+b5^0 <= 0), cost: 1 propagated equality b5^post6 = b5^0 propagated equality a4^post6 = __const_10^0+a4^0 propagated equality a^post6 = a^0 propagated equality ret_complex6^post6 = ret_complex6^0 propagated equality b^post6 = b^0 propagated equality __const_5^post6 = __const_5^0 propagated equality __const_12^post6 = __const_12^0 propagated equality answer^post6 = answer^0 propagated equality __const_30^post6 = __const_30^0 propagated equality __const_10^post6 = __const_10^0 Simplified Guard Original rule: l5 -> l2 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=__const_10^0+a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, (0 == 0 /\ -__const_12^0+b5^0 <= 0), cost: 1 New rule: l5 -> l2 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=__const_10^0+a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, -__const_12^0+b5^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l5 -> l2 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=__const_10^0+a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, -__const_12^0+b5^0 <= 0, cost: 1 New rule: l5 -> l2 : a4^0'=__const_10^0+a4^0, -__const_12^0+b5^0 <= 0, cost: 1 Propagated Equalities Original rule: l6 -> l2 : __const_10^0'=__const_10^post7, __const_12^0'=__const_12^post7, __const_30^0'=__const_30^post7, __const_5^0'=__const_5^post7, a4^0'=a4^post7, a^0'=a^post7, answer^0'=answer^post7, b5^0'=b5^post7, b^0'=b^post7, ret_complex6^0'=ret_complex6^post7, (__const_30^0-__const_30^post7 == 0 /\ -ret_complex6^post7+ret_complex6^0 == 0 /\ 1+b5^0-__const_10^0 <= 0 /\ __const_12^0-__const_12^post7 == 0 /\ -__const_5^post7+__const_5^0 == 0 /\ b^0-b^post7 == 0 /\ a^0-a^post7 == 0 /\ -1+a4^post7-a4^0 == 0 /\ -b5^post7+b5^0 == 0 /\ -answer^post7+answer^0 == 0 /\ -__const_10^post7+__const_10^0 == 0), cost: 1 New rule: l6 -> l2 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=1+a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, (0 == 0 /\ 1+b5^0-__const_10^0 <= 0), cost: 1 propagated equality __const_30^post7 = __const_30^0 propagated equality ret_complex6^post7 = ret_complex6^0 propagated equality __const_12^post7 = __const_12^0 propagated equality __const_5^post7 = __const_5^0 propagated equality b^post7 = b^0 propagated equality a^post7 = a^0 propagated equality a4^post7 = 1+a4^0 propagated equality b5^post7 = b5^0 propagated equality answer^post7 = answer^0 propagated equality __const_10^post7 = __const_10^0 Simplified Guard Original rule: l6 -> l2 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=1+a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, (0 == 0 /\ 1+b5^0-__const_10^0 <= 0), cost: 1 New rule: l6 -> l2 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=1+a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, 1+b5^0-__const_10^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l6 -> l2 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=1+a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, 1+b5^0-__const_10^0 <= 0, cost: 1 New rule: l6 -> l2 : a4^0'=1+a4^0, 1+b5^0-__const_10^0 <= 0, cost: 1 Propagated Equalities Original rule: l6 -> l5 : __const_10^0'=__const_10^post8, __const_12^0'=__const_12^post8, __const_30^0'=__const_30^post8, __const_5^0'=__const_5^post8, a4^0'=a4^post8, a^0'=a^post8, answer^0'=answer^post8, b5^0'=b5^post8, b^0'=b^post8, ret_complex6^0'=ret_complex6^post8, (-b5^0+__const_10^0 <= 0 /\ __const_12^0-__const_12^post8 == 0 /\ -a4^post8+a4^0 == 0 /\ b^0-b^post8 == 0 /\ -__const_5^post8+__const_5^0 == 0 /\ -ret_complex6^post8+ret_complex6^0 == 0 /\ __const_30^0-__const_30^post8 == 0 /\ -__const_10^post8+__const_10^0 == 0 /\ a^0-a^post8 == 0 /\ -answer^post8+answer^0 == 0 /\ -b5^post8+b5^0 == 0), cost: 1 New rule: l6 -> l5 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, (0 == 0 /\ -b5^0+__const_10^0 <= 0), cost: 1 propagated equality __const_12^post8 = __const_12^0 propagated equality a4^post8 = a4^0 propagated equality b^post8 = b^0 propagated equality __const_5^post8 = __const_5^0 propagated equality ret_complex6^post8 = ret_complex6^0 propagated equality __const_30^post8 = __const_30^0 propagated equality __const_10^post8 = __const_10^0 propagated equality a^post8 = a^0 propagated equality answer^post8 = answer^0 propagated equality b5^post8 = b5^0 Simplified Guard Original rule: l6 -> l5 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, (0 == 0 /\ -b5^0+__const_10^0 <= 0), cost: 1 New rule: l6 -> l5 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, -b5^0+__const_10^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l6 -> l5 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, -b5^0+__const_10^0 <= 0, cost: 1 New rule: l6 -> l5 : -b5^0+__const_10^0 <= 0, cost: 1 Propagated Equalities Original rule: l7 -> l6 : __const_10^0'=__const_10^post9, __const_12^0'=__const_12^post9, __const_30^0'=__const_30^post9, __const_5^0'=__const_5^post9, a4^0'=a4^post9, a^0'=a^post9, answer^0'=answer^post9, b5^0'=b5^post9, b^0'=b^post9, ret_complex6^0'=ret_complex6^post9, (-answer^post9+answer^0 == 0 /\ __const_30^0-__const_30^post9 == 0 /\ __const_12^0-__const_12^post9 == 0 /\ -ret_complex6^post9+ret_complex6^0 == 0 /\ a^0-a^post9 == 0 /\ -a4^post9+a4^0 == 0 /\ -__const_5^0+b5^0 <= 0 /\ -__const_10^post9+__const_10^0 == 0 /\ -2+b5^post9-b5^0 == 0 /\ -__const_5^post9+__const_5^0 == 0 /\ b^0-b^post9 == 0), cost: 1 New rule: l7 -> l6 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=2+b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, (0 == 0 /\ -__const_5^0+b5^0 <= 0), cost: 1 propagated equality answer^post9 = answer^0 propagated equality __const_30^post9 = __const_30^0 propagated equality __const_12^post9 = __const_12^0 propagated equality ret_complex6^post9 = ret_complex6^0 propagated equality a^post9 = a^0 propagated equality a4^post9 = a4^0 propagated equality __const_10^post9 = __const_10^0 propagated equality b5^post9 = 2+b5^0 propagated equality __const_5^post9 = __const_5^0 propagated equality b^post9 = b^0 Simplified Guard Original rule: l7 -> l6 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=2+b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, (0 == 0 /\ -__const_5^0+b5^0 <= 0), cost: 1 New rule: l7 -> l6 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=2+b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, -__const_5^0+b5^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l7 -> l6 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=2+b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, -__const_5^0+b5^0 <= 0, cost: 1 New rule: l7 -> l6 : b5^0'=2+b5^0, -__const_5^0+b5^0 <= 0, cost: 1 Propagated Equalities Original rule: l7 -> l6 : __const_10^0'=__const_10^post10, __const_12^0'=__const_12^post10, __const_30^0'=__const_30^post10, __const_5^0'=__const_5^post10, a4^0'=a4^post10, a^0'=a^post10, answer^0'=answer^post10, b5^0'=b5^post10, b^0'=b^post10, ret_complex6^0'=ret_complex6^post10, (0 == 0 /\ a^0-a^post10 == 0 /\ -b^post10+b^0 == 0 /\ __const_5^0-__const_5^post10 == 0 /\ -ret_complex6^post10+ret_complex6^0 == 0 /\ -a4^post10+a4^0 == 0 /\ answer^0-answer^post10 == 0 /\ 1+__const_5^0-b5^0 <= 0 /\ __const_12^0-__const_12^post10 == 0 /\ -__const_30^post10+__const_30^0 == 0 /\ -__const_10^post10+__const_10^0 == 0), cost: 1 New rule: l7 -> l6 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^post10, b^0'=b^0, ret_complex6^0'=ret_complex6^0, (0 == 0 /\ 1+__const_5^0-b5^0 <= 0), cost: 1 propagated equality a^post10 = a^0 propagated equality b^post10 = b^0 propagated equality __const_5^post10 = __const_5^0 propagated equality ret_complex6^post10 = ret_complex6^0 propagated equality a4^post10 = a4^0 propagated equality answer^post10 = answer^0 propagated equality __const_12^post10 = __const_12^0 propagated equality __const_30^post10 = __const_30^0 propagated equality __const_10^post10 = __const_10^0 Simplified Guard Original rule: l7 -> l6 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^post10, b^0'=b^0, ret_complex6^0'=ret_complex6^0, (0 == 0 /\ 1+__const_5^0-b5^0 <= 0), cost: 1 New rule: l7 -> l6 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^post10, b^0'=b^0, ret_complex6^0'=ret_complex6^0, 1+__const_5^0-b5^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l7 -> l6 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^post10, b^0'=b^0, ret_complex6^0'=ret_complex6^0, 1+__const_5^0-b5^0 <= 0, cost: 1 New rule: l7 -> l6 : b5^0'=b5^post10, 1+__const_5^0-b5^0 <= 0, cost: 1 Propagated Equalities Original rule: l4 -> l3 : __const_10^0'=__const_10^post11, __const_12^0'=__const_12^post11, __const_30^0'=__const_30^post11, __const_5^0'=__const_5^post11, a4^0'=a4^post11, a^0'=a^post11, answer^0'=answer^post11, b5^0'=b5^post11, b^0'=b^post11, ret_complex6^0'=ret_complex6^post11, (b5^post11-b5^0+__const_10^0 == 0 /\ -b5^0+a4^0 <= 0 /\ -2+a4^post11-a4^0 == 0 /\ -__const_30^post11+__const_30^0 == 0 /\ ret_complex6^0-ret_complex6^post11 == 0 /\ -__const_10^post11+__const_10^0 == 0 /\ answer^0-answer^post11 == 0 /\ __const_12^0-__const_12^post11 == 0 /\ __const_5^0-__const_5^post11 == 0 /\ a^0-a^post11 == 0 /\ b^0-b^post11 == 0), cost: 1 New rule: l4 -> l3 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=2+a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0-__const_10^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, (0 == 0 /\ -b5^0+a4^0 <= 0), cost: 1 propagated equality b5^post11 = b5^0-__const_10^0 propagated equality a4^post11 = 2+a4^0 propagated equality __const_30^post11 = __const_30^0 propagated equality ret_complex6^post11 = ret_complex6^0 propagated equality __const_10^post11 = __const_10^0 propagated equality answer^post11 = answer^0 propagated equality __const_12^post11 = __const_12^0 propagated equality __const_5^post11 = __const_5^0 propagated equality a^post11 = a^0 propagated equality b^post11 = b^0 Simplified Guard Original rule: l4 -> l3 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=2+a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0-__const_10^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, (0 == 0 /\ -b5^0+a4^0 <= 0), cost: 1 New rule: l4 -> l3 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=2+a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0-__const_10^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, -b5^0+a4^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l4 -> l3 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=2+a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0-__const_10^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, -b5^0+a4^0 <= 0, cost: 1 New rule: l4 -> l3 : a4^0'=2+a4^0, b5^0'=b5^0-__const_10^0, -b5^0+a4^0 <= 0, cost: 1 Propagated Equalities Original rule: l4 -> l7 : __const_10^0'=__const_10^post12, __const_12^0'=__const_12^post12, __const_30^0'=__const_30^post12, __const_5^0'=__const_5^post12, a4^0'=a4^post12, a^0'=a^post12, answer^0'=answer^post12, b5^0'=b5^post12, b^0'=b^post12, ret_complex6^0'=ret_complex6^post12, (b^0-b^post12 == 0 /\ a^0-a^post12 == 0 /\ -__const_12^post12+__const_12^0 == 0 /\ __const_5^0-__const_5^post12 == 0 /\ ret_complex6^0-ret_complex6^post12 == 0 /\ 1+b5^0-a4^0 <= 0 /\ -b5^post12+b5^0 == 0 /\ answer^0-answer^post12 == 0 /\ -a4^post12+a4^0 == 0 /\ -__const_30^post12+__const_30^0 == 0 /\ -__const_10^post12+__const_10^0 == 0), cost: 1 New rule: l4 -> l7 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, (0 == 0 /\ 1+b5^0-a4^0 <= 0), cost: 1 propagated equality b^post12 = b^0 propagated equality a^post12 = a^0 propagated equality __const_12^post12 = __const_12^0 propagated equality __const_5^post12 = __const_5^0 propagated equality ret_complex6^post12 = ret_complex6^0 propagated equality b5^post12 = b5^0 propagated equality answer^post12 = answer^0 propagated equality a4^post12 = a4^0 propagated equality __const_30^post12 = __const_30^0 propagated equality __const_10^post12 = __const_10^0 Simplified Guard Original rule: l4 -> l7 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, (0 == 0 /\ 1+b5^0-a4^0 <= 0), cost: 1 New rule: l4 -> l7 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, 1+b5^0-a4^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l4 -> l7 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=a4^0, a^0'=a^0, answer^0'=answer^0, b5^0'=b5^0, b^0'=b^0, ret_complex6^0'=ret_complex6^0, 1+b5^0-a4^0 <= 0, cost: 1 New rule: l4 -> l7 : 1+b5^0-a4^0 <= 0, cost: 1 Propagated Equalities Original rule: l9 -> l3 : __const_10^0'=__const_10^post13, __const_12^0'=__const_12^post13, __const_30^0'=__const_30^post13, __const_5^0'=__const_5^post13, a4^0'=a4^post13, a^0'=a^post13, answer^0'=answer^post13, b5^0'=b5^post13, b^0'=b^post13, ret_complex6^0'=ret_complex6^post13, (-__const_5^post13+__const_5^post14 == 0 /\ answer^post13 == 0 /\ a4^post13-a^post13 == 0 /\ __const_30^0-__const_30^post14 == 0 /\ __const_12^0-__const_12^post14 == 0 /\ -__const_12^post13+__const_12^post14 == 0 /\ -1+b^post13 == 0 /\ b^0-b^post14 == 0 /\ ret_complex6^post14-ret_complex6^post13 == 0 /\ -ret_complex6^post14+ret_complex6^0 == 0 /\ -__const_10^post13+__const_10^post14 == 0 /\ -a4^post14+a4^0 == 0 /\ -1+a^post13 == 0 /\ b5^post13-b^post13 == 0 /\ -__const_10^post14+__const_10^0 == 0 /\ -__const_30^post13+__const_30^post14 == 0 /\ -answer^post14+answer^0 == 0 /\ -__const_5^post14+__const_5^0 == 0 /\ -b5^post14+b5^0 == 0 /\ a^0-a^post14 == 0), cost: 1 New rule: l9 -> l3 : __const_10^0'=__const_10^post14, __const_12^0'=__const_12^post14, __const_30^0'=__const_30^post14, __const_5^0'=__const_5^post14, a4^0'=1, a^0'=1, answer^0'=0, b5^0'=1, b^0'=1, ret_complex6^0'=ret_complex6^post14, (0 == 0 /\ __const_30^0-__const_30^post14 == 0 /\ __const_12^0-__const_12^post14 == 0 /\ b^0-b^post14 == 0 /\ -ret_complex6^post14+ret_complex6^0 == 0 /\ -a4^post14+a4^0 == 0 /\ -__const_10^post14+__const_10^0 == 0 /\ -answer^post14+answer^0 == 0 /\ -__const_5^post14+__const_5^0 == 0 /\ -b5^post14+b5^0 == 0 /\ a^0-a^post14 == 0), cost: 1 propagated equality __const_5^post13 = __const_5^post14 propagated equality answer^post13 = 0 propagated equality a4^post13 = a^post13 propagated equality __const_12^post13 = __const_12^post14 propagated equality b^post13 = 1 propagated equality ret_complex6^post13 = ret_complex6^post14 propagated equality __const_10^post13 = __const_10^post14 propagated equality a^post13 = 1 propagated equality b5^post13 = 1 propagated equality __const_30^post13 = __const_30^post14 Propagated Equalities Original rule: l9 -> l3 : __const_10^0'=__const_10^post14, __const_12^0'=__const_12^post14, __const_30^0'=__const_30^post14, __const_5^0'=__const_5^post14, a4^0'=1, a^0'=1, answer^0'=0, b5^0'=1, b^0'=1, ret_complex6^0'=ret_complex6^post14, (0 == 0 /\ __const_30^0-__const_30^post14 == 0 /\ __const_12^0-__const_12^post14 == 0 /\ b^0-b^post14 == 0 /\ -ret_complex6^post14+ret_complex6^0 == 0 /\ -a4^post14+a4^0 == 0 /\ -__const_10^post14+__const_10^0 == 0 /\ -answer^post14+answer^0 == 0 /\ -__const_5^post14+__const_5^0 == 0 /\ -b5^post14+b5^0 == 0 /\ a^0-a^post14 == 0), cost: 1 New rule: l9 -> l3 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=1, a^0'=1, answer^0'=0, b5^0'=1, b^0'=1, ret_complex6^0'=ret_complex6^0, 0 == 0, cost: 1 propagated equality __const_30^post14 = __const_30^0 propagated equality __const_12^post14 = __const_12^0 propagated equality b^post14 = b^0 propagated equality ret_complex6^post14 = ret_complex6^0 propagated equality a4^post14 = a4^0 propagated equality __const_10^post14 = __const_10^0 propagated equality answer^post14 = answer^0 propagated equality __const_5^post14 = __const_5^0 propagated equality b5^post14 = b5^0 propagated equality a^post14 = a^0 Simplified Guard Original rule: l9 -> l3 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=1, a^0'=1, answer^0'=0, b5^0'=1, b^0'=1, ret_complex6^0'=ret_complex6^0, 0 == 0, cost: 1 New rule: l9 -> l3 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=1, a^0'=1, answer^0'=0, b5^0'=1, b^0'=1, ret_complex6^0'=ret_complex6^0, T, cost: 1 Removed Trivial Updates Original rule: l9 -> l3 : __const_10^0'=__const_10^0, __const_12^0'=__const_12^0, __const_30^0'=__const_30^0, __const_5^0'=__const_5^0, a4^0'=1, a^0'=1, answer^0'=0, b5^0'=1, b^0'=1, ret_complex6^0'=ret_complex6^0, T, cost: 1 New rule: l9 -> l3 : a4^0'=1, a^0'=1, answer^0'=0, b5^0'=1, b^0'=1, T, cost: 1 Step with 27 Trace 27[T] Blocked [{}, {}] Step with 17 Trace 27[T], 17[T] Blocked [{}, {}, {}] Step with 15 Trace 27[T], 17[T], 15[(__const_30^0-a4^0 <= 0)] Blocked [{}, {}, {}, {}] Backtrack Trace 27[T], 17[T] Blocked [{}, {}, {15[T]}] Step with 16 Trace 27[T], 17[T], 16[(1-__const_30^0+a4^0 <= 0)] Blocked [{}, {}, {15[T]}, {}] Step with 18 Trace 27[T], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 18[T] Blocked [{}, {}, {15[T]}, {}, {}] Step with 25 Trace 27[T], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 18[T], 25[(-b5^0+a4^0 <= 0)] Blocked [{}, {}, {15[T]}, {}, {}, {}] Accelerate Start location: l9 Program variables: __const_10^0 __const_12^0 __const_30^0 __const_5^0 a4^0 a^0 answer^0 b5^0 b^0 ret_complex6^0 15: l0 -> l1 : answer^0'=1, ret_complex6^0'=1, __const_30^0-a4^0 <= 0, cost: 1 16: l0 -> l2 : 1-__const_30^0+a4^0 <= 0, cost: 1 18: l2 -> l4 : T, cost: 1 17: l3 -> l0 : T, cost: 1 28: l3 -> l3 : a4^0'=2*n+a4^0, b5^0'=b5^0-__const_10^0*n, (b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0), cost: 1 25: l4 -> l3 : a4^0'=2+a4^0, b5^0'=b5^0-__const_10^0, -b5^0+a4^0 <= 0, cost: 1 26: l4 -> l7 : 1+b5^0-a4^0 <= 0, cost: 1 19: l5 -> l2 : a4^0'=1+a4^0, 1+__const_12^0-b5^0 <= 0, cost: 1 20: l5 -> l2 : a4^0'=__const_10^0+a4^0, -__const_12^0+b5^0 <= 0, cost: 1 21: l6 -> l2 : a4^0'=1+a4^0, 1+b5^0-__const_10^0 <= 0, cost: 1 22: l6 -> l5 : -b5^0+__const_10^0 <= 0, cost: 1 23: l7 -> l6 : b5^0'=2+b5^0, -__const_5^0+b5^0 <= 0, cost: 1 24: l7 -> l6 : b5^0'=b5^post10, 1+__const_5^0-b5^0 <= 0, cost: 1 27: l9 -> l3 : a4^0'=1, a^0'=1, answer^0'=0, b5^0'=1, b^0'=1, T, cost: 1 Loop Acceleration Original rule: l3 -> l3 : a4^0'=2+a4^0, b5^0'=b5^0-__const_10^0, (-b5^0+a4^0 <= 0 /\ 1-__const_30^0+a4^0 <= 0), cost: 1 New rule: l3 -> l3 : a4^0'=2*n+a4^0, b5^0'=b5^0-__const_10^0*n, (b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0), cost: 1 b5^0-a4^0 >= 0 [0]: eventual decrease yields (b5^0-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0) b5^0-a4^0 >= 0 [1]: eventual increase yields (2+__const_10^0 <= 0 /\ b5^0-a4^0 >= 0) -1+__const_30^0-a4^0 >= 0 [0]: montonic decrease yields 1+__const_30^0-2*n-a4^0 >= 0 -1+__const_30^0-a4^0 >= 0 [1]: eventual increase yields (2 <= 0 /\ -1+__const_30^0-a4^0 >= 0) Replacement map: {b5^0-a4^0 >= 0 -> (b5^0-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0), -1+__const_30^0-a4^0 >= 0 -> 1+__const_30^0-2*n-a4^0 >= 0} Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)] Blocked [{}, {}, {28[T]}] Step with 17 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T] Blocked [{}, {}, {28[T]}, {}] Step with 16 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}] Step with 18 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 18[T] Blocked [{}, {}, {28[T]}, {}, {}, {}] Step with 25 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 18[T], 25[(-b5^0+a4^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {}, {}] Covered Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 18[T] Blocked [{}, {}, {28[T]}, {}, {}, {25[T]}] Step with 26 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {25[T]}, {}] Step with 23 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)], 23[(-__const_5^0+b5^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {25[T]}, {}, {}] Step with 21 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)], 23[(-__const_5^0+b5^0 <= 0)], 21[(1+b5^0-__const_10^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {25[T]}, {}, {}, {}] Accelerate Start location: l9 Program variables: __const_10^0 __const_12^0 __const_30^0 __const_5^0 a4^0 a^0 answer^0 b5^0 b^0 ret_complex6^0 15: l0 -> l1 : answer^0'=1, ret_complex6^0'=1, __const_30^0-a4^0 <= 0, cost: 1 16: l0 -> l2 : 1-__const_30^0+a4^0 <= 0, cost: 1 18: l2 -> l4 : T, cost: 1 29: l2 -> l2 : a4^0'=n2+a4^0, b5^0'=2*n2+b5^0, (-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0), cost: 1 17: l3 -> l0 : T, cost: 1 28: l3 -> l3 : a4^0'=2*n+a4^0, b5^0'=b5^0-__const_10^0*n, (b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0), cost: 1 25: l4 -> l3 : a4^0'=2+a4^0, b5^0'=b5^0-__const_10^0, -b5^0+a4^0 <= 0, cost: 1 26: l4 -> l7 : 1+b5^0-a4^0 <= 0, cost: 1 19: l5 -> l2 : a4^0'=1+a4^0, 1+__const_12^0-b5^0 <= 0, cost: 1 20: l5 -> l2 : a4^0'=__const_10^0+a4^0, -__const_12^0+b5^0 <= 0, cost: 1 21: l6 -> l2 : a4^0'=1+a4^0, 1+b5^0-__const_10^0 <= 0, cost: 1 22: l6 -> l5 : -b5^0+__const_10^0 <= 0, cost: 1 23: l7 -> l6 : b5^0'=2+b5^0, -__const_5^0+b5^0 <= 0, cost: 1 24: l7 -> l6 : b5^0'=b5^post10, 1+__const_5^0-b5^0 <= 0, cost: 1 27: l9 -> l3 : a4^0'=1, a^0'=1, answer^0'=0, b5^0'=1, b^0'=1, T, cost: 1 Loop Acceleration Original rule: l2 -> l2 : a4^0'=1+a4^0, b5^0'=2+b5^0, (3+b5^0-__const_10^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -__const_5^0+b5^0 <= 0), cost: 1 New rule: l2 -> l2 : a4^0'=n2+a4^0, b5^0'=2*n2+b5^0, (-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0), cost: 1 -3-b5^0+__const_10^0 >= 0 [0]: montonic decrease yields -1-2*n2-b5^0+__const_10^0 >= 0 -3-b5^0+__const_10^0 >= 0 [1]: eventual increase yields (-3-b5^0+__const_10^0 >= 0 /\ 2 <= 0) __const_5^0-b5^0 >= 0 [0]: montonic decrease yields 2-2*n2+__const_5^0-b5^0 >= 0 __const_5^0-b5^0 >= 0 [1]: eventual increase yields (2 <= 0 /\ __const_5^0-b5^0 >= 0) -1-b5^0+a4^0 >= 0 [0]: montonic decrease yields -n2-b5^0+a4^0 >= 0 -1-b5^0+a4^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1-b5^0+a4^0 >= 0) Replacement map: {-3-b5^0+__const_10^0 >= 0 -> -1-2*n2-b5^0+__const_10^0 >= 0, __const_5^0-b5^0 >= 0 -> 2-2*n2+__const_5^0-b5^0 >= 0, -1-b5^0+a4^0 >= 0 -> -n2-b5^0+a4^0 >= 0} Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}] Step with 18 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 18[T] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {}] Step with 26 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {}, {}] Step with 23 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)], 23[(-__const_5^0+b5^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {}, {}, {}] Step with 21 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)], 23[(-__const_5^0+b5^0 <= 0)], 21[(1+b5^0-__const_10^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {}, {}, {}, {}] Covered Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)], 23[(-__const_5^0+b5^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {}, {}, {21[T]}] Step with 22 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)], 23[(-__const_5^0+b5^0 <= 0)], 22[(-b5^0+__const_10^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {}, {}, {21[T]}, {}] Step with 19 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)], 23[(-__const_5^0+b5^0 <= 0)], 22[(-b5^0+__const_10^0 <= 0)], 19[(1+__const_12^0-b5^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {}, {}, {21[T]}, {}, {}] Accelerate Start location: l9 Program variables: __const_10^0 __const_12^0 __const_30^0 __const_5^0 a4^0 a^0 answer^0 b5^0 b^0 ret_complex6^0 15: l0 -> l1 : answer^0'=1, ret_complex6^0'=1, __const_30^0-a4^0 <= 0, cost: 1 16: l0 -> l2 : 1-__const_30^0+a4^0 <= 0, cost: 1 18: l2 -> l4 : T, cost: 1 29: l2 -> l2 : a4^0'=n2+a4^0, b5^0'=2*n2+b5^0, (-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0), cost: 1 30: l2 -> l2 : a4^0'=n3+a4^0, b5^0'=2*n3+b5^0, (2+b5^0-__const_10^0 >= 0 /\ 1-__const_12^0+b5^0 >= 0 /\ -1+n3 >= 0 /\ 2-2*n3+__const_5^0-b5^0 >= 0 /\ -n3-b5^0+a4^0 >= 0), cost: 1 17: l3 -> l0 : T, cost: 1 28: l3 -> l3 : a4^0'=2*n+a4^0, b5^0'=b5^0-__const_10^0*n, (b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0), cost: 1 25: l4 -> l3 : a4^0'=2+a4^0, b5^0'=b5^0-__const_10^0, -b5^0+a4^0 <= 0, cost: 1 26: l4 -> l7 : 1+b5^0-a4^0 <= 0, cost: 1 19: l5 -> l2 : a4^0'=1+a4^0, 1+__const_12^0-b5^0 <= 0, cost: 1 20: l5 -> l2 : a4^0'=__const_10^0+a4^0, -__const_12^0+b5^0 <= 0, cost: 1 21: l6 -> l2 : a4^0'=1+a4^0, 1+b5^0-__const_10^0 <= 0, cost: 1 22: l6 -> l5 : -b5^0+__const_10^0 <= 0, cost: 1 23: l7 -> l6 : b5^0'=2+b5^0, -__const_5^0+b5^0 <= 0, cost: 1 24: l7 -> l6 : b5^0'=b5^post10, 1+__const_5^0-b5^0 <= 0, cost: 1 27: l9 -> l3 : a4^0'=1, a^0'=1, answer^0'=0, b5^0'=1, b^0'=1, T, cost: 1 Loop Acceleration Original rule: l2 -> l2 : a4^0'=1+a4^0, b5^0'=2+b5^0, (-2-b5^0+__const_10^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -__const_5^0+b5^0 <= 0 /\ -1+__const_12^0-b5^0 <= 0), cost: 1 New rule: l2 -> l2 : a4^0'=n3+a4^0, b5^0'=2*n3+b5^0, (2+b5^0-__const_10^0 >= 0 /\ 1-__const_12^0+b5^0 >= 0 /\ -1+n3 >= 0 /\ 2-2*n3+__const_5^0-b5^0 >= 0 /\ -n3-b5^0+a4^0 >= 0), cost: 1 2+b5^0-__const_10^0 >= 0 [0]: monotonic increase yields 2+b5^0-__const_10^0 >= 0 1-__const_12^0+b5^0 >= 0 [0]: monotonic increase yields 1-__const_12^0+b5^0 >= 0 __const_5^0-b5^0 >= 0 [0]: montonic decrease yields 2-2*n3+__const_5^0-b5^0 >= 0 __const_5^0-b5^0 >= 0 [1]: eventual increase yields (2 <= 0 /\ __const_5^0-b5^0 >= 0) -1-b5^0+a4^0 >= 0 [0]: montonic decrease yields -n3-b5^0+a4^0 >= 0 -1-b5^0+a4^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1-b5^0+a4^0 >= 0) Replacement map: {2+b5^0-__const_10^0 >= 0 -> 2+b5^0-__const_10^0 >= 0, 1-__const_12^0+b5^0 >= 0 -> 1-__const_12^0+b5^0 >= 0, __const_5^0-b5^0 >= 0 -> 2-2*n3+__const_5^0-b5^0 >= 0, -1-b5^0+a4^0 >= 0 -> -n3-b5^0+a4^0 >= 0} Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 30[(2+b5^0-__const_10^0 >= 0 /\ 1-__const_12^0+b5^0 >= 0 /\ -1+n3 >= 0 /\ 2-2*n3+__const_5^0-b5^0 >= 0 /\ -n3-b5^0+a4^0 >= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {30[T]}] Acceleration Failed marked recursive suffix as redundant Step with 18 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 30[(2+b5^0-__const_10^0 >= 0 /\ 1-__const_12^0+b5^0 >= 0 /\ -1+n3 >= 0 /\ 2-2*n3+__const_5^0-b5^0 >= 0 /\ -n3-b5^0+a4^0 >= 0)], 18[T] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {30[T]}, {}] Step with 26 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 30[(2+b5^0-__const_10^0 >= 0 /\ 1-__const_12^0+b5^0 >= 0 /\ -1+n3 >= 0 /\ 2-2*n3+__const_5^0-b5^0 >= 0 /\ -n3-b5^0+a4^0 >= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {30[T]}, {}, {}] Step with 23 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 30[(2+b5^0-__const_10^0 >= 0 /\ 1-__const_12^0+b5^0 >= 0 /\ -1+n3 >= 0 /\ 2-2*n3+__const_5^0-b5^0 >= 0 /\ -n3-b5^0+a4^0 >= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)], 23[(-__const_5^0+b5^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {30[T]}, {}, {}, {}] Step with 22 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 30[(2+b5^0-__const_10^0 >= 0 /\ 1-__const_12^0+b5^0 >= 0 /\ -1+n3 >= 0 /\ 2-2*n3+__const_5^0-b5^0 >= 0 /\ -n3-b5^0+a4^0 >= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)], 23[(-__const_5^0+b5^0 <= 0)], 22[(-b5^0+__const_10^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {30[T]}, {}, {}, {}, {}] Step with 19 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 30[(2+b5^0-__const_10^0 >= 0 /\ 1-__const_12^0+b5^0 >= 0 /\ -1+n3 >= 0 /\ 2-2*n3+__const_5^0-b5^0 >= 0 /\ -n3-b5^0+a4^0 >= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)], 23[(-__const_5^0+b5^0 <= 0)], 22[(-b5^0+__const_10^0 <= 0)], 19[(1+__const_12^0-b5^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {30[T]}, {}, {}, {}, {}, {}] Covered Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 30[(2+b5^0-__const_10^0 >= 0 /\ 1-__const_12^0+b5^0 >= 0 /\ -1+n3 >= 0 /\ 2-2*n3+__const_5^0-b5^0 >= 0 /\ -n3-b5^0+a4^0 >= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)], 23[(-__const_5^0+b5^0 <= 0)], 22[(-b5^0+__const_10^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {30[T]}, {}, {}, {}, {19[T]}] Backtrack Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 30[(2+b5^0-__const_10^0 >= 0 /\ 1-__const_12^0+b5^0 >= 0 /\ -1+n3 >= 0 /\ 2-2*n3+__const_5^0-b5^0 >= 0 /\ -n3-b5^0+a4^0 >= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)], 23[(-__const_5^0+b5^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {30[T]}, {}, {}, {22[T]}] Backtrack Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 30[(2+b5^0-__const_10^0 >= 0 /\ 1-__const_12^0+b5^0 >= 0 /\ -1+n3 >= 0 /\ 2-2*n3+__const_5^0-b5^0 >= 0 /\ -n3-b5^0+a4^0 >= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {30[T]}, {}, {23[T]}] Step with 24 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 30[(2+b5^0-__const_10^0 >= 0 /\ 1-__const_12^0+b5^0 >= 0 /\ -1+n3 >= 0 /\ 2-2*n3+__const_5^0-b5^0 >= 0 /\ -n3-b5^0+a4^0 >= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)], 24[(1+__const_5^0-b5^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {30[T]}, {}, {23[T]}, {}] Step with 22 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 30[(2+b5^0-__const_10^0 >= 0 /\ 1-__const_12^0+b5^0 >= 0 /\ -1+n3 >= 0 /\ 2-2*n3+__const_5^0-b5^0 >= 0 /\ -n3-b5^0+a4^0 >= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)], 24[(1+__const_5^0-b5^0 <= 0)], 22[(-b5^0+__const_10^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {30[T]}, {}, {23[T]}, {}, {}] Step with 19 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 30[(2+b5^0-__const_10^0 >= 0 /\ 1-__const_12^0+b5^0 >= 0 /\ -1+n3 >= 0 /\ 2-2*n3+__const_5^0-b5^0 >= 0 /\ -n3-b5^0+a4^0 >= 0)], 18[T], 26[(1+b5^0-a4^0 <= 0)], 24[(1+__const_5^0-b5^0 <= 0)], 22[(-b5^0+__const_10^0 <= 0)], 19[(1+__const_12^0-b5^0 <= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {30[T]}, {}, {23[T]}, {}, {}, {}] Nonterm Start location: l9 Program variables: __const_10^0 __const_12^0 __const_30^0 __const_5^0 a4^0 a^0 answer^0 b5^0 b^0 ret_complex6^0 15: l0 -> l1 : answer^0'=1, ret_complex6^0'=1, __const_30^0-a4^0 <= 0, cost: 1 16: l0 -> l2 : 1-__const_30^0+a4^0 <= 0, cost: 1 18: l2 -> l4 : T, cost: 1 29: l2 -> l2 : a4^0'=n2+a4^0, b5^0'=2*n2+b5^0, (-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0), cost: 1 30: l2 -> l2 : a4^0'=n3+a4^0, b5^0'=2*n3+b5^0, (2+b5^0-__const_10^0 >= 0 /\ 1-__const_12^0+b5^0 >= 0 /\ -1+n3 >= 0 /\ 2-2*n3+__const_5^0-b5^0 >= 0 /\ -n3-b5^0+a4^0 >= 0), cost: 1 31: l2 -> LoAT_sink : (-b5^post101+b5^0 <= 0 /\ -1-__const_5^0+b5^0 >= 0 /\ -1+b5^post101-b5^0 <= 0 /\ b5^post101-__const_10^0 >= 0 /\ -1+b5^post101-__const_12^0 >= 0 /\ -1-b5^0+a4^0 >= 0), cost: NONTERM 32: l2 -> l2 : a4^0'=n4+a4^0, b5^0'=b5^post101, (-1+b5^post101-__const_5^0 >= 0 /\ -1-__const_5^0+b5^0 >= 0 /\ -1+n4 >= 0 /\ -1+b5^post101-b5^0 <= 0 /\ b5^post101-__const_10^0 >= 0 /\ -1+b5^post101-__const_12^0 >= 0 /\ -1-b5^0+a4^0 >= 0), cost: 1 17: l3 -> l0 : T, cost: 1 28: l3 -> l3 : a4^0'=2*n+a4^0, b5^0'=b5^0-__const_10^0*n, (b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0), cost: 1 25: l4 -> l3 : a4^0'=2+a4^0, b5^0'=b5^0-__const_10^0, -b5^0+a4^0 <= 0, cost: 1 26: l4 -> l7 : 1+b5^0-a4^0 <= 0, cost: 1 19: l5 -> l2 : a4^0'=1+a4^0, 1+__const_12^0-b5^0 <= 0, cost: 1 20: l5 -> l2 : a4^0'=__const_10^0+a4^0, -__const_12^0+b5^0 <= 0, cost: 1 21: l6 -> l2 : a4^0'=1+a4^0, 1+b5^0-__const_10^0 <= 0, cost: 1 22: l6 -> l5 : -b5^0+__const_10^0 <= 0, cost: 1 23: l7 -> l6 : b5^0'=2+b5^0, -__const_5^0+b5^0 <= 0, cost: 1 24: l7 -> l6 : b5^0'=b5^post10, 1+__const_5^0-b5^0 <= 0, cost: 1 27: l9 -> l3 : a4^0'=1, a^0'=1, answer^0'=0, b5^0'=1, b^0'=1, T, cost: 1 Certificate of Non-Termination Original rule: l2 -> l2 : a4^0'=1+a4^0, b5^0'=b5^post101, (1-b5^post101+__const_12^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -b5^post101+__const_10^0 <= 0 /\ 1+__const_5^0-b5^0 <= 0), cost: 1 New rule: l2 -> LoAT_sink : (-b5^post101+b5^0 <= 0 /\ -1-__const_5^0+b5^0 >= 0 /\ -1+b5^post101-b5^0 <= 0 /\ b5^post101-__const_10^0 >= 0 /\ -1+b5^post101-__const_12^0 >= 0 /\ -1-b5^0+a4^0 >= 0), cost: NONTERM -1-__const_5^0+b5^0 >= 0 [0]: eventual decrease yields (-1+b5^post101-__const_5^0 >= 0 /\ -1-__const_5^0+b5^0 >= 0) -1-__const_5^0+b5^0 >= 0 [1]: eventual increase yields (-b5^post101+b5^0 <= 0 /\ -1-__const_5^0+b5^0 >= 0) b5^post101-__const_10^0 >= 0 [0]: monotonic increase yields b5^post101-__const_10^0 >= 0 -1+b5^post101-__const_12^0 >= 0 [0]: monotonic increase yields -1+b5^post101-__const_12^0 >= 0 -1-b5^0+a4^0 >= 0 [0]: eventual increase yields (-1+b5^post101-b5^0 <= 0 /\ -1-b5^0+a4^0 >= 0) Replacement map: {-1-__const_5^0+b5^0 >= 0 -> (-b5^post101+b5^0 <= 0 /\ -1-__const_5^0+b5^0 >= 0), b5^post101-__const_10^0 >= 0 -> b5^post101-__const_10^0 >= 0, -1+b5^post101-__const_12^0 >= 0 -> -1+b5^post101-__const_12^0 >= 0, -1-b5^0+a4^0 >= 0 -> (-1+b5^post101-b5^0 <= 0 /\ -1-b5^0+a4^0 >= 0)} Loop Acceleration Original rule: l2 -> l2 : a4^0'=1+a4^0, b5^0'=b5^post101, (1-b5^post101+__const_12^0 <= 0 /\ 1+b5^0-a4^0 <= 0 /\ -b5^post101+__const_10^0 <= 0 /\ 1+__const_5^0-b5^0 <= 0), cost: 1 New rule: l2 -> l2 : a4^0'=n4+a4^0, b5^0'=b5^post101, (-1+b5^post101-__const_5^0 >= 0 /\ -1-__const_5^0+b5^0 >= 0 /\ -1+n4 >= 0 /\ -1+b5^post101-b5^0 <= 0 /\ b5^post101-__const_10^0 >= 0 /\ -1+b5^post101-__const_12^0 >= 0 /\ -1-b5^0+a4^0 >= 0), cost: 1 -1-__const_5^0+b5^0 >= 0 [0]: eventual decrease yields (-1+b5^post101-__const_5^0 >= 0 /\ -1-__const_5^0+b5^0 >= 0) -1-__const_5^0+b5^0 >= 0 [1]: eventual increase yields (-b5^post101+b5^0 <= 0 /\ -1-__const_5^0+b5^0 >= 0) b5^post101-__const_10^0 >= 0 [0]: monotonic increase yields b5^post101-__const_10^0 >= 0 -1+b5^post101-__const_12^0 >= 0 [0]: monotonic increase yields -1+b5^post101-__const_12^0 >= 0 -1-b5^0+a4^0 >= 0 [0]: eventual increase yields (-1+b5^post101-b5^0 <= 0 /\ -1-b5^0+a4^0 >= 0) Replacement map: {-1-__const_5^0+b5^0 >= 0 -> (-1+b5^post101-__const_5^0 >= 0 /\ -1-__const_5^0+b5^0 >= 0), b5^post101-__const_10^0 >= 0 -> b5^post101-__const_10^0 >= 0, -1+b5^post101-__const_12^0 >= 0 -> -1+b5^post101-__const_12^0 >= 0, -1-b5^0+a4^0 >= 0 -> (-1+b5^post101-b5^0 <= 0 /\ -1-b5^0+a4^0 >= 0)} Step with 31 Trace 27[T], 28[(b5^0-a4^0 >= 0 /\ 1+__const_30^0-2*n-a4^0 >= 0 /\ 2+b5^0-__const_10^0*(-1+n)-2*n-a4^0 >= 0 /\ -1+n >= 0)], 17[T], 16[(1-__const_30^0+a4^0 <= 0)], 29[(-1+n2 >= 0 /\ -1-2*n2-b5^0+__const_10^0 >= 0 /\ -n2-b5^0+a4^0 >= 0 /\ 2-2*n2+__const_5^0-b5^0 >= 0)], 30[(2+b5^0-__const_10^0 >= 0 /\ 1-__const_12^0+b5^0 >= 0 /\ -1+n3 >= 0 /\ 2-2*n3+__const_5^0-b5^0 >= 0 /\ -n3-b5^0+a4^0 >= 0)], 31[(-b5^post101+b5^0 <= 0 /\ -1-__const_5^0+b5^0 >= 0 /\ -1+b5^post101-b5^0 <= 0 /\ b5^post101-__const_10^0 >= 0 /\ -1+b5^post101-__const_12^0 >= 0 /\ -1-b5^0+a4^0 >= 0)] Blocked [{}, {}, {28[T]}, {}, {}, {29[T]}, {30[T]}, {31[T]}] Refute Counterexample [ __const_10^0=2 __const_12^0=1 __const_30^0=4 __const_5^0=4 a4^0=1 a^0=1 answer^0=0 b5^0=1 b^0=1 ret_complex6^0=0 ] 27 [ __const_10^0=2 __const_12^0=1 __const_30^0=4 __const_5^0=4 a4^0=3 a^0=1 answer^0=0 b5^0=-1 b^0=1 ret_complex6^0=0 ] 28 [ __const_10^0=2 __const_12^0=1 __const_30^0=4 __const_5^0=4 a4^0=3 a^0=1 answer^0=0 b5^0=-1 b^0=1 ret_complex6^0=0 ] 17 [ __const_10^0=2 __const_12^0=1 __const_30^0=4 __const_5^0=4 a4^0=3 a^0=1 answer^0=0 b5^0=-1 b^0=1 ret_complex6^0=0 ] 16 [ __const_10^0=2 __const_12^0=1 __const_30^0=4 __const_5^0=4 a4^0=4 a^0=1 answer^0=0 b5^0=1 b^0=1 ret_complex6^0=0 ] 29 [ __const_10^0=2 __const_12^0=1 __const_30^0=4 __const_5^0=4 a4^0=6 a^0=1 answer^0=0 b5^0=5 b^0=1 ret_complex6^0=0 ] 30 [ __const_10^0=2 __const_12^0=1 __const_30^0=4 __const_5^0=4 a4^0=a4^0 a^0=a^0 answer^0=answer^0 b5^0=b5^0 b^0=b^0 ret_complex6^0=0 ] 31 NO Build SHA: a05f16bf13df659c382799650051f91bf6828c7b