unknown Initial ITS Start location: l3 Program variables: id^0 m^0 x^0 0: l0 -> l1 : id^0'=id^post1, m^0'=m^post1, x^0'=x^post1, (-1+x^post1-x^0 == 0 /\ x^0-m^0 <= 0 /\ -m^post1+m^0 == 0 /\ -1+x^post1-m^0 <= 0 /\ id^0-id^post1 == 0 /\ -x^post1 <= 0), cost: 1 1: l0 -> l1 : id^0'=id^post2, m^0'=m^post2, x^0'=x^post2, (1-x^0 <= 0 /\ x^post2 == 0 /\ 1-x^0+m^0 <= 0 /\ id^0-id^post2 == 0 /\ -m^post2+m^0 == 0 /\ -1+x^post2-m^0 <= 0 /\ -x^post2 <= 0), cost: 1 2: l1 -> l0 : id^0'=id^post3, m^0'=m^post3, x^0'=x^post3, (1+id^0-x^0 <= 0 /\ id^0-id^post3 == 0 /\ -m^post3+m^0 == 0 /\ -x^post3+x^0 == 0), cost: 1 3: l1 -> l0 : id^0'=id^post4, m^0'=m^post4, x^0'=x^post4, (1-id^0+x^0 <= 0 /\ -x^post4+x^0 == 0 /\ id^0-id^post4 == 0 /\ -m^post4+m^0 == 0), cost: 1 4: l2 -> l1 : id^0'=id^post5, m^0'=m^post5, x^0'=x^post5, (-m^post5+m^0 == 0 /\ 1-id^0 <= 0 /\ id^0-id^post5 == 0 /\ -1+x^post5-m^0 <= 0 /\ -x^post5 <= 0 /\ -1+x^post5-id^0 == 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0), cost: 1 5: l3 -> l2 : id^0'=id^post6, m^0'=m^post6, x^0'=x^post6, (-id^post6+id^0 == 0 /\ -m^post6+m^0 == 0 /\ -x^post6+x^0 == 0), cost: 1 Chained Linear Paths Start location: l3 Program variables: id^0 m^0 x^0 0: l0 -> l1 : id^0'=id^post1, m^0'=m^post1, x^0'=x^post1, (-1+x^post1-x^0 == 0 /\ x^0-m^0 <= 0 /\ -m^post1+m^0 == 0 /\ -1+x^post1-m^0 <= 0 /\ id^0-id^post1 == 0 /\ -x^post1 <= 0), cost: 1 1: l0 -> l1 : id^0'=id^post2, m^0'=m^post2, x^0'=x^post2, (1-x^0 <= 0 /\ x^post2 == 0 /\ 1-x^0+m^0 <= 0 /\ id^0-id^post2 == 0 /\ -m^post2+m^0 == 0 /\ -1+x^post2-m^0 <= 0 /\ -x^post2 <= 0), cost: 1 2: l1 -> l0 : id^0'=id^post3, m^0'=m^post3, x^0'=x^post3, (1+id^0-x^0 <= 0 /\ id^0-id^post3 == 0 /\ -m^post3+m^0 == 0 /\ -x^post3+x^0 == 0), cost: 1 3: l1 -> l0 : id^0'=id^post4, m^0'=m^post4, x^0'=x^post4, (1-id^0+x^0 <= 0 /\ -x^post4+x^0 == 0 /\ id^0-id^post4 == 0 /\ -m^post4+m^0 == 0), cost: 1 6: l3 -> l1 : id^0'=id^post5, m^0'=m^post5, x^0'=x^post5, (m^post6-m^post5 == 0 /\ 1-id^post6 <= 0 /\ -id^post6+id^0 == 0 /\ -m^post6+m^0 == 0 /\ -1+x^post5-m^post6 <= 0 /\ id^post6-id^post5 == 0 /\ -x^post5 <= 0 /\ -1+x^post5-id^post6 == 0 /\ -x^post6+x^0 == 0 /\ 1-m^post6 <= 0 /\ id^post6-m^post6 <= 0), cost: 1 Eliminating location l2 by chaining: Applied chaining First rule: l3 -> l2 : id^0'=id^post6, m^0'=m^post6, x^0'=x^post6, (-id^post6+id^0 == 0 /\ -m^post6+m^0 == 0 /\ -x^post6+x^0 == 0), cost: 1 Second rule: l2 -> l1 : id^0'=id^post5, m^0'=m^post5, x^0'=x^post5, (-m^post5+m^0 == 0 /\ 1-id^0 <= 0 /\ id^0-id^post5 == 0 /\ -1+x^post5-m^0 <= 0 /\ -x^post5 <= 0 /\ -1+x^post5-id^0 == 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0), cost: 1 New rule: l3 -> l1 : id^0'=id^post5, m^0'=m^post5, x^0'=x^post5, (m^post6-m^post5 == 0 /\ 1-id^post6 <= 0 /\ -id^post6+id^0 == 0 /\ -m^post6+m^0 == 0 /\ -1+x^post5-m^post6 <= 0 /\ id^post6-id^post5 == 0 /\ -x^post5 <= 0 /\ -1+x^post5-id^post6 == 0 /\ -x^post6+x^0 == 0 /\ 1-m^post6 <= 0 /\ id^post6-m^post6 <= 0), cost: 1 Applied deletion Removed the following rules: 4 5 Simplified Transitions Start location: l3 Program variables: id^0 m^0 x^0 7: l0 -> l1 : x^0'=1+x^0, (x^0-m^0 <= 0 /\ -1-x^0 <= 0), cost: 1 8: l0 -> l1 : x^0'=0, (-1-m^0 <= 0 /\ 1-x^0 <= 0 /\ 1-x^0+m^0 <= 0), cost: 1 9: l1 -> l0 : 1+id^0-x^0 <= 0, cost: 1 10: l1 -> l0 : 1-id^0+x^0 <= 0, cost: 1 11: l3 -> l1 : x^0'=1+id^0, (1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0), cost: 1 Propagated Equalities Original rule: l0 -> l1 : id^0'=id^post1, m^0'=m^post1, x^0'=x^post1, (-1+x^post1-x^0 == 0 /\ x^0-m^0 <= 0 /\ -m^post1+m^0 == 0 /\ -1+x^post1-m^0 <= 0 /\ id^0-id^post1 == 0 /\ -x^post1 <= 0), cost: 1 New rule: l0 -> l1 : id^0'=id^0, m^0'=m^0, x^0'=1+x^0, (0 == 0 /\ x^0-m^0 <= 0 /\ -1-x^0 <= 0), cost: 1 propagated equality x^post1 = 1+x^0 propagated equality m^post1 = m^0 propagated equality id^post1 = id^0 Simplified Guard Original rule: l0 -> l1 : id^0'=id^0, m^0'=m^0, x^0'=1+x^0, (0 == 0 /\ x^0-m^0 <= 0 /\ -1-x^0 <= 0), cost: 1 New rule: l0 -> l1 : id^0'=id^0, m^0'=m^0, x^0'=1+x^0, (x^0-m^0 <= 0 /\ -1-x^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : id^0'=id^0, m^0'=m^0, x^0'=1+x^0, (x^0-m^0 <= 0 /\ -1-x^0 <= 0), cost: 1 New rule: l0 -> l1 : x^0'=1+x^0, (x^0-m^0 <= 0 /\ -1-x^0 <= 0), cost: 1 Propagated Equalities Original rule: l0 -> l1 : id^0'=id^post2, m^0'=m^post2, x^0'=x^post2, (1-x^0 <= 0 /\ x^post2 == 0 /\ 1-x^0+m^0 <= 0 /\ id^0-id^post2 == 0 /\ -m^post2+m^0 == 0 /\ -1+x^post2-m^0 <= 0 /\ -x^post2 <= 0), cost: 1 New rule: l0 -> l1 : id^0'=id^0, m^0'=m^0, x^0'=0, (0 <= 0 /\ 0 == 0 /\ -1-m^0 <= 0 /\ 1-x^0 <= 0 /\ 1-x^0+m^0 <= 0), cost: 1 propagated equality x^post2 = 0 propagated equality id^post2 = id^0 propagated equality m^post2 = m^0 Simplified Guard Original rule: l0 -> l1 : id^0'=id^0, m^0'=m^0, x^0'=0, (0 <= 0 /\ 0 == 0 /\ -1-m^0 <= 0 /\ 1-x^0 <= 0 /\ 1-x^0+m^0 <= 0), cost: 1 New rule: l0 -> l1 : id^0'=id^0, m^0'=m^0, x^0'=0, (-1-m^0 <= 0 /\ 1-x^0 <= 0 /\ 1-x^0+m^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l0 -> l1 : id^0'=id^0, m^0'=m^0, x^0'=0, (-1-m^0 <= 0 /\ 1-x^0 <= 0 /\ 1-x^0+m^0 <= 0), cost: 1 New rule: l0 -> l1 : x^0'=0, (-1-m^0 <= 0 /\ 1-x^0 <= 0 /\ 1-x^0+m^0 <= 0), cost: 1 Propagated Equalities Original rule: l1 -> l0 : id^0'=id^post3, m^0'=m^post3, x^0'=x^post3, (1+id^0-x^0 <= 0 /\ id^0-id^post3 == 0 /\ -m^post3+m^0 == 0 /\ -x^post3+x^0 == 0), cost: 1 New rule: l1 -> l0 : id^0'=id^0, m^0'=m^0, x^0'=x^0, (0 == 0 /\ 1+id^0-x^0 <= 0), cost: 1 propagated equality id^post3 = id^0 propagated equality m^post3 = m^0 propagated equality x^post3 = x^0 Simplified Guard Original rule: l1 -> l0 : id^0'=id^0, m^0'=m^0, x^0'=x^0, (0 == 0 /\ 1+id^0-x^0 <= 0), cost: 1 New rule: l1 -> l0 : id^0'=id^0, m^0'=m^0, x^0'=x^0, 1+id^0-x^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l0 : id^0'=id^0, m^0'=m^0, x^0'=x^0, 1+id^0-x^0 <= 0, cost: 1 New rule: l1 -> l0 : 1+id^0-x^0 <= 0, cost: 1 Propagated Equalities Original rule: l1 -> l0 : id^0'=id^post4, m^0'=m^post4, x^0'=x^post4, (1-id^0+x^0 <= 0 /\ -x^post4+x^0 == 0 /\ id^0-id^post4 == 0 /\ -m^post4+m^0 == 0), cost: 1 New rule: l1 -> l0 : id^0'=id^0, m^0'=m^0, x^0'=x^0, (0 == 0 /\ 1-id^0+x^0 <= 0), cost: 1 propagated equality x^post4 = x^0 propagated equality id^post4 = id^0 propagated equality m^post4 = m^0 Simplified Guard Original rule: l1 -> l0 : id^0'=id^0, m^0'=m^0, x^0'=x^0, (0 == 0 /\ 1-id^0+x^0 <= 0), cost: 1 New rule: l1 -> l0 : id^0'=id^0, m^0'=m^0, x^0'=x^0, 1-id^0+x^0 <= 0, cost: 1 Removed Trivial Updates Original rule: l1 -> l0 : id^0'=id^0, m^0'=m^0, x^0'=x^0, 1-id^0+x^0 <= 0, cost: 1 New rule: l1 -> l0 : 1-id^0+x^0 <= 0, cost: 1 Propagated Equalities Original rule: l3 -> l1 : id^0'=id^post5, m^0'=m^post5, x^0'=x^post5, (m^post6-m^post5 == 0 /\ 1-id^post6 <= 0 /\ -id^post6+id^0 == 0 /\ -m^post6+m^0 == 0 /\ -1+x^post5-m^post6 <= 0 /\ id^post6-id^post5 == 0 /\ -x^post5 <= 0 /\ -1+x^post5-id^post6 == 0 /\ -x^post6+x^0 == 0 /\ 1-m^post6 <= 0 /\ id^post6-m^post6 <= 0), cost: 1 New rule: l3 -> l1 : id^0'=id^post6, m^0'=m^post6, x^0'=1+id^post6, (0 == 0 /\ 1-id^post6 <= 0 /\ -id^post6+id^0 == 0 /\ -m^post6+m^0 == 0 /\ -x^post6+x^0 == 0 /\ 1-m^post6 <= 0 /\ -1-id^post6 <= 0 /\ id^post6-m^post6 <= 0), cost: 1 propagated equality m^post5 = m^post6 propagated equality id^post5 = id^post6 propagated equality x^post5 = 1+id^post6 Propagated Equalities Original rule: l3 -> l1 : id^0'=id^post6, m^0'=m^post6, x^0'=1+id^post6, (0 == 0 /\ 1-id^post6 <= 0 /\ -id^post6+id^0 == 0 /\ -m^post6+m^0 == 0 /\ -x^post6+x^0 == 0 /\ 1-m^post6 <= 0 /\ -1-id^post6 <= 0 /\ id^post6-m^post6 <= 0), cost: 1 New rule: l3 -> l1 : id^0'=id^0, m^0'=m^0, x^0'=1+id^0, (0 == 0 /\ 1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0), cost: 1 propagated equality id^post6 = id^0 propagated equality m^post6 = m^0 propagated equality x^post6 = x^0 Simplified Guard Original rule: l3 -> l1 : id^0'=id^0, m^0'=m^0, x^0'=1+id^0, (0 == 0 /\ 1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0), cost: 1 New rule: l3 -> l1 : id^0'=id^0, m^0'=m^0, x^0'=1+id^0, (1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0), cost: 1 Removed Trivial Updates Original rule: l3 -> l1 : id^0'=id^0, m^0'=m^0, x^0'=1+id^0, (1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0), cost: 1 New rule: l3 -> l1 : x^0'=1+id^0, (1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0), cost: 1 Step with 11 Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)] Blocked [{}, {}] Step with 9 Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)], 9[(1+id^0-x^0 <= 0)] Blocked [{}, {}, {}] Step with 7 Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)], 9[(1+id^0-x^0 <= 0)], 7[(x^0-m^0 <= 0 /\ -1-x^0 <= 0)] Blocked [{}, {}, {}, {}] Accelerate Start location: l3 Program variables: id^0 m^0 x^0 7: l0 -> l1 : x^0'=1+x^0, (x^0-m^0 <= 0 /\ -1-x^0 <= 0), cost: 1 8: l0 -> l1 : x^0'=0, (-1-m^0 <= 0 /\ 1-x^0 <= 0 /\ 1-x^0+m^0 <= 0), cost: 1 9: l1 -> l0 : 1+id^0-x^0 <= 0, cost: 1 10: l1 -> l0 : 1-id^0+x^0 <= 0, cost: 1 12: l1 -> l1 : x^0'=n+x^0, (-1+n >= 0 /\ 1+x^0 >= 0 /\ 1-n-x^0+m^0 >= 0 /\ -1-id^0+x^0 >= 0), cost: 1 11: l3 -> l1 : x^0'=1+id^0, (1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0), cost: 1 Loop Acceleration Original rule: l1 -> l1 : x^0'=1+x^0, (x^0-m^0 <= 0 /\ 1+id^0-x^0 <= 0 /\ -1-x^0 <= 0), cost: 1 New rule: l1 -> l1 : x^0'=n+x^0, (-1+n >= 0 /\ 1+x^0 >= 0 /\ 1-n-x^0+m^0 >= 0 /\ -1-id^0+x^0 >= 0), cost: 1 -x^0+m^0 >= 0 [0]: montonic decrease yields 1-n-x^0+m^0 >= 0 -x^0+m^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -x^0+m^0 >= 0) 1+x^0 >= 0 [0]: monotonic increase yields 1+x^0 >= 0 -1-id^0+x^0 >= 0 [0]: monotonic increase yields -1-id^0+x^0 >= 0 Replacement map: {-x^0+m^0 >= 0 -> 1-n-x^0+m^0 >= 0, 1+x^0 >= 0 -> 1+x^0 >= 0, -1-id^0+x^0 >= 0 -> -1-id^0+x^0 >= 0} Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)], 12[(-1+n >= 0 /\ 1+x^0 >= 0 /\ 1-n-x^0+m^0 >= 0 /\ -1-id^0+x^0 >= 0)] Blocked [{}, {}, {12[T]}] Step with 9 Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)], 12[(-1+n >= 0 /\ 1+x^0 >= 0 /\ 1-n-x^0+m^0 >= 0 /\ -1-id^0+x^0 >= 0)], 9[(1+id^0-x^0 <= 0)] Blocked [{}, {}, {12[T]}, {}] Step with 7 Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)], 12[(-1+n >= 0 /\ 1+x^0 >= 0 /\ 1-n-x^0+m^0 >= 0 /\ -1-id^0+x^0 >= 0)], 9[(1+id^0-x^0 <= 0)], 7[(x^0-m^0 <= 0 /\ -1-x^0 <= 0)] Blocked [{}, {}, {12[T]}, {}, {}] Covered Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)], 12[(-1+n >= 0 /\ 1+x^0 >= 0 /\ 1-n-x^0+m^0 >= 0 /\ -1-id^0+x^0 >= 0)], 9[(1+id^0-x^0 <= 0)] Blocked [{}, {}, {12[T]}, {7[T]}] Step with 8 Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)], 12[(-1+n >= 0 /\ 1+x^0 >= 0 /\ 1-n-x^0+m^0 >= 0 /\ -1-id^0+x^0 >= 0)], 9[(1+id^0-x^0 <= 0)], 8[(-1-m^0 <= 0 /\ 1-x^0 <= 0 /\ 1-x^0+m^0 <= 0)] Blocked [{}, {}, {12[T]}, {7[T]}, {}] Acceleration Failed marked recursive suffix as redundant Accelerate and Drop Start location: l3 Program variables: id^0 m^0 x^0 7: l0 -> l1 : x^0'=1+x^0, (x^0-m^0 <= 0 /\ -1-x^0 <= 0), cost: 1 8: l0 -> l1 : x^0'=0, (-1-m^0 <= 0 /\ 1-x^0 <= 0 /\ 1-x^0+m^0 <= 0), cost: 1 9: l1 -> l0 : 1+id^0-x^0 <= 0, cost: 1 10: l1 -> l0 : 1-id^0+x^0 <= 0, cost: 1 12: l1 -> l1 : x^0'=n+x^0, (-1+n >= 0 /\ 1+x^0 >= 0 /\ 1-n-x^0+m^0 >= 0 /\ -1-id^0+x^0 >= 0), cost: 1 13: l1 -> LoAT_sink : (1+m^0 >= 0 /\ -x^0 <= 0 /\ -x^0+m^0 >= 0 /\ 1+x^0 >= 0 /\ x^0 <= 0 /\ -id^0+m^0 >= 0 /\ -1-id^0+x^0 >= 0 /\ m^0 >= 0), cost: NONTERM 11: l3 -> l1 : x^0'=1+id^0, (1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0), cost: 1 Certificate of Non-Termination Original rule: l1 -> l1 : x^0'=0, (-1-m^0 <= 0 /\ -x^0+m^0 >= 0 /\ 1+x^0 >= 0 /\ -1-id^0+x^0 >= 0 /\ id^0-m^0 <= 0 /\ -m^0 <= 0), cost: 1 New rule: l1 -> LoAT_sink : (1+m^0 >= 0 /\ -x^0 <= 0 /\ -x^0+m^0 >= 0 /\ 1+x^0 >= 0 /\ x^0 <= 0 /\ -id^0+m^0 >= 0 /\ -1-id^0+x^0 >= 0 /\ m^0 >= 0), cost: NONTERM 1+m^0 >= 0 [0]: monotonic increase yields 1+m^0 >= 0 -x^0+m^0 >= 0 [0]: eventual decrease yields (-x^0+m^0 >= 0 /\ m^0 >= 0) -x^0+m^0 >= 0 [1]: eventual increase yields (-x^0 <= 0 /\ -x^0+m^0 >= 0) 1+x^0 >= 0 [0]: monotonic increase yields 1+x^0 >= 0 -id^0+m^0 >= 0 [0]: monotonic increase yields -id^0+m^0 >= 0 -1-id^0+x^0 >= 0 [0]: eventual decrease yields (-1-id^0+x^0 >= 0 /\ -1-id^0 >= 0) -1-id^0+x^0 >= 0 [1]: eventual increase yields (x^0 <= 0 /\ -1-id^0+x^0 >= 0) m^0 >= 0 [0]: monotonic increase yields m^0 >= 0 Replacement map: {1+m^0 >= 0 -> 1+m^0 >= 0, -x^0+m^0 >= 0 -> (-x^0 <= 0 /\ -x^0+m^0 >= 0), 1+x^0 >= 0 -> 1+x^0 >= 0, -id^0+m^0 >= 0 -> -id^0+m^0 >= 0, -1-id^0+x^0 >= 0 -> (x^0 <= 0 /\ -1-id^0+x^0 >= 0), m^0 >= 0 -> m^0 >= 0} Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)] Blocked [{}, {12[T]}] Step with 9 Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)], 9[(1+id^0-x^0 <= 0)] Blocked [{}, {12[T]}, {}] Step with 8 Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)], 9[(1+id^0-x^0 <= 0)], 8[(-1-m^0 <= 0 /\ 1-x^0 <= 0 /\ 1-x^0+m^0 <= 0)] Blocked [{}, {12[T]}, {}, {}] Step with 10 Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)], 9[(1+id^0-x^0 <= 0)], 8[(-1-m^0 <= 0 /\ 1-x^0 <= 0 /\ 1-x^0+m^0 <= 0)], 10[(1-id^0+x^0 <= 0)] Blocked [{}, {12[T]}, {}, {9[T], 13[T]}, {}] Acceleration Failed marked recursive suffix as redundant Step with 7 Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)], 9[(1+id^0-x^0 <= 0)], 8[(-1-m^0 <= 0 /\ 1-x^0 <= 0 /\ 1-x^0+m^0 <= 0)], 10[(1-id^0+x^0 <= 0)], 7[(x^0-m^0 <= 0 /\ -1-x^0 <= 0)] Blocked [{}, {12[T]}, {}, {9[T], 13[T]}, {8[T]}, {}] Accelerate Start location: l3 Program variables: id^0 m^0 x^0 7: l0 -> l1 : x^0'=1+x^0, (x^0-m^0 <= 0 /\ -1-x^0 <= 0), cost: 1 8: l0 -> l1 : x^0'=0, (-1-m^0 <= 0 /\ 1-x^0 <= 0 /\ 1-x^0+m^0 <= 0), cost: 1 9: l1 -> l0 : 1+id^0-x^0 <= 0, cost: 1 10: l1 -> l0 : 1-id^0+x^0 <= 0, cost: 1 12: l1 -> l1 : x^0'=n+x^0, (-1+n >= 0 /\ 1+x^0 >= 0 /\ 1-n-x^0+m^0 >= 0 /\ -1-id^0+x^0 >= 0), cost: 1 13: l1 -> LoAT_sink : (1+m^0 >= 0 /\ -x^0 <= 0 /\ -x^0+m^0 >= 0 /\ 1+x^0 >= 0 /\ x^0 <= 0 /\ -id^0+m^0 >= 0 /\ -1-id^0+x^0 >= 0 /\ m^0 >= 0), cost: NONTERM 14: l1 -> l1 : x^0'=x^0+n3, (1+x^0 >= 0 /\ id^0-x^0-n3 >= 0 /\ 1-x^0-n3+m^0 >= 0 /\ -1+n3 >= 0), cost: 1 11: l3 -> l1 : x^0'=1+id^0, (1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0), cost: 1 Loop Acceleration Original rule: l1 -> l1 : x^0'=1+x^0, (1-id^0+x^0 <= 0 /\ x^0-m^0 <= 0 /\ -1-x^0 <= 0), cost: 1 New rule: l1 -> l1 : x^0'=x^0+n3, (1+x^0 >= 0 /\ id^0-x^0-n3 >= 0 /\ 1-x^0-n3+m^0 >= 0 /\ -1+n3 >= 0), cost: 1 -x^0+m^0 >= 0 [0]: montonic decrease yields 1-x^0-n3+m^0 >= 0 -x^0+m^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -x^0+m^0 >= 0) -1+id^0-x^0 >= 0 [0]: montonic decrease yields id^0-x^0-n3 >= 0 -1+id^0-x^0 >= 0 [1]: eventual increase yields (1 <= 0 /\ -1+id^0-x^0 >= 0) 1+x^0 >= 0 [0]: monotonic increase yields 1+x^0 >= 0 Replacement map: {-x^0+m^0 >= 0 -> 1-x^0-n3+m^0 >= 0, -1+id^0-x^0 >= 0 -> id^0-x^0-n3 >= 0, 1+x^0 >= 0 -> 1+x^0 >= 0} Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)], 9[(1+id^0-x^0 <= 0)], 8[(-1-m^0 <= 0 /\ 1-x^0 <= 0 /\ 1-x^0+m^0 <= 0)], 14[(1+x^0 >= 0 /\ id^0-x^0-n3 >= 0 /\ 1-x^0-n3+m^0 >= 0 /\ -1+n3 >= 0)] Blocked [{}, {12[T]}, {}, {9[T], 13[T]}, {14[T]}] Acceleration Failed marked recursive suffix as redundant Step with 10 Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)], 9[(1+id^0-x^0 <= 0)], 8[(-1-m^0 <= 0 /\ 1-x^0 <= 0 /\ 1-x^0+m^0 <= 0)], 14[(1+x^0 >= 0 /\ id^0-x^0-n3 >= 0 /\ 1-x^0-n3+m^0 >= 0 /\ -1+n3 >= 0)], 10[(1-id^0+x^0 <= 0)] Blocked [{}, {12[T]}, {}, {9[T], 13[T]}, {9[T], 13[T], 14[T]}, {}] Accelerate and Drop Start location: l3 Program variables: id^0 m^0 x^0 7: l0 -> l1 : x^0'=1+x^0, (x^0-m^0 <= 0 /\ -1-x^0 <= 0), cost: 1 8: l0 -> l1 : x^0'=0, (-1-m^0 <= 0 /\ 1-x^0 <= 0 /\ 1-x^0+m^0 <= 0), cost: 1 15: l0 -> LoAT_sink : (1+m^0 >= 0 /\ -1+n31 >= 0 /\ -1+x^0 >= 0 /\ 1-n31+m^0 >= 0 /\ -1-n31+id^0 >= 0 /\ -n31+id^0 >= 0 /\ -n31+x^0 <= 0 /\ -1+x^0-m^0 >= 0), cost: NONTERM 16: l0 -> l0 : x^0'=1+m^0, (-1+id^0-m^0 >= 0 /\ 1+m^0 >= 0 /\ -2+id^0-m^0 >= 0 /\ -1+x^0-m^0 >= 0 /\ m^0 >= 0), cost: 1 9: l1 -> l0 : 1+id^0-x^0 <= 0, cost: 1 10: l1 -> l0 : 1-id^0+x^0 <= 0, cost: 1 12: l1 -> l1 : x^0'=n+x^0, (-1+n >= 0 /\ 1+x^0 >= 0 /\ 1-n-x^0+m^0 >= 0 /\ -1-id^0+x^0 >= 0), cost: 1 13: l1 -> LoAT_sink : (1+m^0 >= 0 /\ -x^0 <= 0 /\ -x^0+m^0 >= 0 /\ 1+x^0 >= 0 /\ x^0 <= 0 /\ -id^0+m^0 >= 0 /\ -1-id^0+x^0 >= 0 /\ m^0 >= 0), cost: NONTERM 14: l1 -> l1 : x^0'=x^0+n3, (1+x^0 >= 0 /\ id^0-x^0-n3 >= 0 /\ 1-x^0-n3+m^0 >= 0 /\ -1+n3 >= 0), cost: 1 11: l3 -> l1 : x^0'=1+id^0, (1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0), cost: 1 Certificate of Non-Termination Original rule: l0 -> l0 : x^0'=n31, (-1-m^0 <= 0 /\ -1+n31 >= 0 /\ 1-x^0 <= 0 /\ 1-x^0+m^0 <= 0 /\ 1-n31+m^0 >= 0 /\ -n31+id^0 >= 0 /\ 1+n31-id^0 <= 0), cost: 1 New rule: l0 -> LoAT_sink : (1+m^0 >= 0 /\ -1+n31 >= 0 /\ -1+x^0 >= 0 /\ 1-n31+m^0 >= 0 /\ -1-n31+id^0 >= 0 /\ -n31+id^0 >= 0 /\ -n31+x^0 <= 0 /\ -1+x^0-m^0 >= 0), cost: NONTERM 1+m^0 >= 0 [0]: monotonic increase yields 1+m^0 >= 0 -1+n31 >= 0 [0]: monotonic increase yields -1+n31 >= 0 -1+x^0 >= 0 [0]: montonic decrease yields -1+n31 >= 0, dependencies: 1-n31+m^0 >= 0 -1+x^0-m^0 >= 0 -1+x^0 >= 0 [1]: eventual decrease yields (-1+n31 >= 0 /\ -1+x^0 >= 0) -1+x^0 >= 0 [2]: eventual increase yields (-1+x^0 >= 0 /\ -n31+x^0 <= 0) 1-n31+m^0 >= 0 [0]: monotonic increase yields 1-n31+m^0 >= 0 -1-n31+id^0 >= 0 [0]: monotonic increase yields -1-n31+id^0 >= 0 -n31+id^0 >= 0 [0]: monotonic increase yields -n31+id^0 >= 0, dependencies: -1-n31+id^0 >= 0 -1+x^0-m^0 >= 0 [0]: eventual decrease yields (-1+x^0-m^0 >= 0 /\ -1+n31-m^0 >= 0) -1+x^0-m^0 >= 0 [1]: eventual increase yields (-n31+x^0 <= 0 /\ -1+x^0-m^0 >= 0) Replacement map: {1+m^0 >= 0 -> 1+m^0 >= 0, -1+n31 >= 0 -> -1+n31 >= 0, -1+x^0 >= 0 -> (-1+x^0 >= 0 /\ -n31+x^0 <= 0), 1-n31+m^0 >= 0 -> 1-n31+m^0 >= 0, -1-n31+id^0 >= 0 -> -1-n31+id^0 >= 0, -n31+id^0 >= 0 -> -n31+id^0 >= 0, -1+x^0-m^0 >= 0 -> (-n31+x^0 <= 0 /\ -1+x^0-m^0 >= 0)} Loop Acceleration Original rule: l0 -> l0 : x^0'=n31, (-1-m^0 <= 0 /\ -1+n31 >= 0 /\ 1-x^0 <= 0 /\ 1-x^0+m^0 <= 0 /\ 1-n31+m^0 >= 0 /\ -n31+id^0 >= 0 /\ 1+n31-id^0 <= 0), cost: 1 New rule: l0 -> l0 : x^0'=n31, (1+m^0 >= 0 /\ -1+n31 >= 0 /\ 1-n31+m^0 >= 0 /\ -1-n31+id^0 >= 0 /\ -n31+id^0 >= 0 /\ -1+n4 >= 0 /\ -1+x^0-m^0 >= 0 /\ -1+n31-m^0 >= 0), cost: 1 1+m^0 >= 0 [0]: monotonic increase yields 1+m^0 >= 0 -1+n31 >= 0 [0]: monotonic increase yields -1+n31 >= 0 -1+x^0 >= 0 [0]: montonic decrease yields -1+n31 >= 0, dependencies: 1-n31+m^0 >= 0 -1+x^0-m^0 >= 0 -1+x^0 >= 0 [1]: eventual decrease yields (-1+n31 >= 0 /\ -1+x^0 >= 0) -1+x^0 >= 0 [2]: eventual increase yields (-1+x^0 >= 0 /\ -n31+x^0 <= 0) 1-n31+m^0 >= 0 [0]: monotonic increase yields 1-n31+m^0 >= 0 -1-n31+id^0 >= 0 [0]: monotonic increase yields -1-n31+id^0 >= 0 -n31+id^0 >= 0 [0]: monotonic increase yields -n31+id^0 >= 0, dependencies: -1-n31+id^0 >= 0 -1+x^0-m^0 >= 0 [0]: eventual decrease yields (-1+x^0-m^0 >= 0 /\ -1+n31-m^0 >= 0) -1+x^0-m^0 >= 0 [1]: eventual increase yields (-n31+x^0 <= 0 /\ -1+x^0-m^0 >= 0) Replacement map: {1+m^0 >= 0 -> 1+m^0 >= 0, -1+n31 >= 0 -> -1+n31 >= 0, -1+x^0 >= 0 -> -1+n31 >= 0, 1-n31+m^0 >= 0 -> 1-n31+m^0 >= 0, -1-n31+id^0 >= 0 -> -1-n31+id^0 >= 0, -n31+id^0 >= 0 -> -n31+id^0 >= 0, -1+x^0-m^0 >= 0 -> (-1+x^0-m^0 >= 0 /\ -1+n31-m^0 >= 0)} made implied equalities explicit Original rule: l0 -> l0 : x^0'=n31, (1+m^0 >= 0 /\ -1+n31 >= 0 /\ 1-n31+m^0 >= 0 /\ -1-n31+id^0 >= 0 /\ -n31+id^0 >= 0 /\ -1+n4 >= 0 /\ -1+x^0-m^0 >= 0 /\ -1+n31-m^0 >= 0), cost: 1 New rule: l0 -> l0 : x^0'=n31, (1+m^0 >= 0 /\ -1+n31 >= 0 /\ 1-n31+m^0 >= 0 /\ -1-n31+id^0 >= 0 /\ -n31+id^0 >= 0 /\ -1+n4 >= 0 /\ -1+x^0-m^0 >= 0 /\ -1+n31-m^0 >= 0 /\ -1+n31-m^0 == 0), cost: 1 Propagated Equalities Original rule: l0 -> l0 : x^0'=n31, (1+m^0 >= 0 /\ -1+n31 >= 0 /\ 1-n31+m^0 >= 0 /\ -1-n31+id^0 >= 0 /\ -n31+id^0 >= 0 /\ -1+n4 >= 0 /\ -1+x^0-m^0 >= 0 /\ -1+n31-m^0 >= 0 /\ -1+n31-m^0 == 0), cost: 1 New rule: l0 -> l0 : x^0'=1+m^0, (0 >= 0 /\ 0 == 0 /\ -1+id^0-m^0 >= 0 /\ 1+m^0 >= 0 /\ -1+n4 >= 0 /\ -2+id^0-m^0 >= 0 /\ -1+x^0-m^0 >= 0 /\ m^0 >= 0), cost: 1 propagated equality n31 = 1+m^0 Simplified Guard Original rule: l0 -> l0 : x^0'=1+m^0, (0 >= 0 /\ 0 == 0 /\ -1+id^0-m^0 >= 0 /\ 1+m^0 >= 0 /\ -1+n4 >= 0 /\ -2+id^0-m^0 >= 0 /\ -1+x^0-m^0 >= 0 /\ m^0 >= 0), cost: 1 New rule: l0 -> l0 : x^0'=1+m^0, (-1+id^0-m^0 >= 0 /\ 1+m^0 >= 0 /\ -1+n4 >= 0 /\ -2+id^0-m^0 >= 0 /\ -1+x^0-m^0 >= 0 /\ m^0 >= 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: l0 -> l0 : x^0'=1+m^0, (-1+id^0-m^0 >= 0 /\ 1+m^0 >= 0 /\ -1+n4 >= 0 /\ -2+id^0-m^0 >= 0 /\ -1+x^0-m^0 >= 0 /\ m^0 >= 0), cost: 1 New rule: l0 -> l0 : x^0'=1+m^0, (-1+id^0-m^0 >= 0 /\ 1+m^0 >= 0 /\ -2+id^0-m^0 >= 0 /\ -1+x^0-m^0 >= 0 /\ m^0 >= 0), cost: 1 Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)], 9[(1+id^0-x^0 <= 0)] Blocked [{}, {12[T]}, {8[T]}] Step with 7 Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)], 9[(1+id^0-x^0 <= 0)], 7[(x^0-m^0 <= 0 /\ -1-x^0 <= 0)] Blocked [{}, {12[T]}, {8[T]}, {}] Covered Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)], 9[(1+id^0-x^0 <= 0)] Blocked [{}, {12[T]}, {7[T], 8[T]}] Backtrack Trace 11[(1-id^0 <= 0 /\ id^0-m^0 <= 0 /\ 1-m^0 <= 0 /\ -1-id^0 <= 0)] Blocked [{}, {9[T], 12[T]}] Backtrack Trace Blocked [{11[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b