unknown Initial ITS Start location: __init Program variables: arg1 arg2 arg3 0: f1_0_main_Load -> f127_0_times_NE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (1+arg1p1 > 0 /\ 1+arg2p1 > 0 /\ arg1 > 0 /\ -1+arg2 > 0), cost: 1 1: f127_0_times_NE -> f127_0_times_NE : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, (-1-arg2p2+arg2 == 0 /\ arg1-arg1p2 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 2: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, (-arg2p3 == 0 /\ 1-arg1p3 == 0 /\ -arg3p3+arg1 == 0 /\ 1-arg2 == 0), cost: 1 3: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, (-arg2p4 == 0 /\ -arg1p4+arg2 == 0 /\ -arg1 == 0 /\ -arg3p4 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 4: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, (-arg3p5+arg1 == 0 /\ -arg1p5+arg2 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 5: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, (-arg1 == 0 /\ -arg3p6 == 0 /\ -arg1p6+arg2 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 7: f469_0_times_InvokeMethod -> f484_0_plus_LE : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, (-arg1p8+arg2 == 0 /\ arg1 > 0 /\ arg3-arg2p8 == 0), cost: 1 6: f218_0_times_Return -> f469_0_times_InvokeMethod : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, (arg3-arg2p7 == 0 /\ -arg1p7+arg1 == 0 /\ -arg3p7+arg2 == 0), cost: 1 8: f484_0_plus_LE -> f484_0_plus_LE : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, (-arg1p9+arg1 == 0 /\ -1-arg2p9+arg2 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 9: f484_0_plus_LE -> f484_0_plus_LE : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, (-arg2p10+arg2 == 0 /\ -1-arg1p10+arg1 == 0 /\ arg1 > 0 /\ -1 < 0 /\ -1+arg2 < 0), cost: 1 10: __init -> f1_0_main_Load : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, T, cost: 1 Chained Linear Paths Start location: __init Program variables: arg1 arg2 arg3 1: f127_0_times_NE -> f127_0_times_NE : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, (-1-arg2p2+arg2 == 0 /\ arg1-arg1p2 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 2: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, (-arg2p3 == 0 /\ 1-arg1p3 == 0 /\ -arg3p3+arg1 == 0 /\ 1-arg2 == 0), cost: 1 3: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, (-arg2p4 == 0 /\ -arg1p4+arg2 == 0 /\ -arg1 == 0 /\ -arg3p4 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 4: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, (-arg3p5+arg1 == 0 /\ -arg1p5+arg2 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 5: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, (-arg1 == 0 /\ -arg3p6 == 0 /\ -arg1p6+arg2 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 7: f469_0_times_InvokeMethod -> f484_0_plus_LE : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, (-arg1p8+arg2 == 0 /\ arg1 > 0 /\ arg3-arg2p8 == 0), cost: 1 6: f218_0_times_Return -> f469_0_times_InvokeMethod : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, (arg3-arg2p7 == 0 /\ -arg1p7+arg1 == 0 /\ -arg3p7+arg2 == 0), cost: 1 8: f484_0_plus_LE -> f484_0_plus_LE : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, (-arg1p9+arg1 == 0 /\ -1-arg2p9+arg2 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 9: f484_0_plus_LE -> f484_0_plus_LE : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, (-arg2p10+arg2 == 0 /\ -1-arg1p10+arg1 == 0 /\ arg1 > 0 /\ -1 < 0 /\ -1+arg2 < 0), cost: 1 11: __init -> f127_0_times_NE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (arg1p11 > 0 /\ 1+arg1p1 > 0 /\ 1+arg2p1 > 0 /\ -1+arg2p11 > 0), cost: 1 Eliminating location f1_0_main_Load by chaining: Applied chaining First rule: __init -> f1_0_main_Load : arg1'=arg1p11, arg2'=arg2p11, arg3'=arg3p11, T, cost: 1 Second rule: f1_0_main_Load -> f127_0_times_NE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (1+arg1p1 > 0 /\ 1+arg2p1 > 0 /\ arg1 > 0 /\ -1+arg2 > 0), cost: 1 New rule: __init -> f127_0_times_NE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (arg1p11 > 0 /\ 1+arg1p1 > 0 /\ 1+arg2p1 > 0 /\ -1+arg2p11 > 0), cost: 1 Applied deletion Removed the following rules: 0 10 Simplified Transitions Start location: __init Program variables: arg1 arg2 arg3 12: f127_0_times_NE -> f127_0_times_NE : arg2'=-1+arg2, arg3'=arg3p2, arg2 > 0, cost: 1 13: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg1, 1-arg2 == 0, cost: 1 14: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=0, arg3'=0, (-arg1 == 0 /\ arg2 > 0), cost: 1 15: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=arg2p5, arg3'=arg1, arg2 > 0, cost: 1 16: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=arg2p6, arg3'=0, (-arg1 == 0 /\ arg2 > 0), cost: 1 18: f469_0_times_InvokeMethod -> f484_0_plus_LE : arg1'=arg2, arg2'=arg3, arg3'=arg3p8, arg1 > 0, cost: 1 17: f218_0_times_Return -> f469_0_times_InvokeMethod : arg2'=arg3, arg3'=arg2, T, cost: 1 19: f484_0_plus_LE -> f484_0_plus_LE : arg2'=-1+arg2, arg3'=arg3p9, arg2 > 0, cost: 1 20: f484_0_plus_LE -> f484_0_plus_LE : arg1'=-1+arg1, arg3'=arg3p10, (arg1 > 0 /\ -1+arg2 < 0), cost: 1 21: __init -> f127_0_times_NE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (1+arg1p1 > 0 /\ 1+arg2p1 > 0), cost: 1 Propagated Equalities Original rule: f127_0_times_NE -> f127_0_times_NE : arg1'=arg1p2, arg2'=arg2p2, arg3'=arg3p2, (-1-arg2p2+arg2 == 0 /\ arg1-arg1p2 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 New rule: f127_0_times_NE -> f127_0_times_NE : arg1'=arg1, arg2'=-1+arg2, arg3'=arg3p2, (0 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 propagated equality arg2p2 = -1+arg2 propagated equality arg1p2 = arg1 Simplified Guard Original rule: f127_0_times_NE -> f127_0_times_NE : arg1'=arg1, arg2'=-1+arg2, arg3'=arg3p2, (0 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 New rule: f127_0_times_NE -> f127_0_times_NE : arg1'=arg1, arg2'=-1+arg2, arg3'=arg3p2, arg2 > 0, cost: 1 Removed Trivial Updates Original rule: f127_0_times_NE -> f127_0_times_NE : arg1'=arg1, arg2'=-1+arg2, arg3'=arg3p2, arg2 > 0, cost: 1 New rule: f127_0_times_NE -> f127_0_times_NE : arg2'=-1+arg2, arg3'=arg3p2, arg2 > 0, cost: 1 Propagated Equalities Original rule: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg1p3, arg2'=arg2p3, arg3'=arg3p3, (-arg2p3 == 0 /\ 1-arg1p3 == 0 /\ -arg3p3+arg1 == 0 /\ 1-arg2 == 0), cost: 1 New rule: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg1, (0 == 0 /\ 1-arg2 == 0), cost: 1 propagated equality arg2p3 = 0 propagated equality arg1p3 = 1 propagated equality arg3p3 = arg1 Simplified Guard Original rule: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg1, (0 == 0 /\ 1-arg2 == 0), cost: 1 New rule: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg1, 1-arg2 == 0, cost: 1 Propagated Equalities Original rule: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg1p4, arg2'=arg2p4, arg3'=arg3p4, (-arg2p4 == 0 /\ -arg1p4+arg2 == 0 /\ -arg1 == 0 /\ -arg3p4 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 New rule: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=0, arg3'=0, (0 == 0 /\ -arg1 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 propagated equality arg2p4 = 0 propagated equality arg1p4 = arg2 propagated equality arg3p4 = 0 Simplified Guard Original rule: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=0, arg3'=0, (0 == 0 /\ -arg1 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 New rule: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=0, arg3'=0, (-arg1 == 0 /\ arg2 > 0), cost: 1 Propagated Equalities Original rule: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg1p5, arg2'=arg2p5, arg3'=arg3p5, (-arg3p5+arg1 == 0 /\ -arg1p5+arg2 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 New rule: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=arg2p5, arg3'=arg1, (0 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 propagated equality arg3p5 = arg1 propagated equality arg1p5 = arg2 Simplified Guard Original rule: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=arg2p5, arg3'=arg1, (0 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 New rule: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=arg2p5, arg3'=arg1, arg2 > 0, cost: 1 Propagated Equalities Original rule: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg1p6, arg2'=arg2p6, arg3'=arg3p6, (-arg1 == 0 /\ -arg3p6 == 0 /\ -arg1p6+arg2 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 New rule: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=arg2p6, arg3'=0, (0 == 0 /\ -arg1 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 propagated equality arg3p6 = 0 propagated equality arg1p6 = arg2 Simplified Guard Original rule: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=arg2p6, arg3'=0, (0 == 0 /\ -arg1 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 New rule: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=arg2p6, arg3'=0, (-arg1 == 0 /\ arg2 > 0), cost: 1 Propagated Equalities Original rule: f218_0_times_Return -> f469_0_times_InvokeMethod : arg1'=arg1p7, arg2'=arg2p7, arg3'=arg3p7, (arg3-arg2p7 == 0 /\ -arg1p7+arg1 == 0 /\ -arg3p7+arg2 == 0), cost: 1 New rule: f218_0_times_Return -> f469_0_times_InvokeMethod : arg1'=arg1, arg2'=arg3, arg3'=arg2, 0 == 0, cost: 1 propagated equality arg2p7 = arg3 propagated equality arg1p7 = arg1 propagated equality arg3p7 = arg2 Simplified Guard Original rule: f218_0_times_Return -> f469_0_times_InvokeMethod : arg1'=arg1, arg2'=arg3, arg3'=arg2, 0 == 0, cost: 1 New rule: f218_0_times_Return -> f469_0_times_InvokeMethod : arg1'=arg1, arg2'=arg3, arg3'=arg2, T, cost: 1 Removed Trivial Updates Original rule: f218_0_times_Return -> f469_0_times_InvokeMethod : arg1'=arg1, arg2'=arg3, arg3'=arg2, T, cost: 1 New rule: f218_0_times_Return -> f469_0_times_InvokeMethod : arg2'=arg3, arg3'=arg2, T, cost: 1 Propagated Equalities Original rule: f469_0_times_InvokeMethod -> f484_0_plus_LE : arg1'=arg1p8, arg2'=arg2p8, arg3'=arg3p8, (-arg1p8+arg2 == 0 /\ arg1 > 0 /\ arg3-arg2p8 == 0), cost: 1 New rule: f469_0_times_InvokeMethod -> f484_0_plus_LE : arg1'=arg2, arg2'=arg3, arg3'=arg3p8, (0 == 0 /\ arg1 > 0), cost: 1 propagated equality arg1p8 = arg2 propagated equality arg2p8 = arg3 Simplified Guard Original rule: f469_0_times_InvokeMethod -> f484_0_plus_LE : arg1'=arg2, arg2'=arg3, arg3'=arg3p8, (0 == 0 /\ arg1 > 0), cost: 1 New rule: f469_0_times_InvokeMethod -> f484_0_plus_LE : arg1'=arg2, arg2'=arg3, arg3'=arg3p8, arg1 > 0, cost: 1 Propagated Equalities Original rule: f484_0_plus_LE -> f484_0_plus_LE : arg1'=arg1p9, arg2'=arg2p9, arg3'=arg3p9, (-arg1p9+arg1 == 0 /\ -1-arg2p9+arg2 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 New rule: f484_0_plus_LE -> f484_0_plus_LE : arg1'=arg1, arg2'=-1+arg2, arg3'=arg3p9, (0 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 propagated equality arg1p9 = arg1 propagated equality arg2p9 = -1+arg2 Simplified Guard Original rule: f484_0_plus_LE -> f484_0_plus_LE : arg1'=arg1, arg2'=-1+arg2, arg3'=arg3p9, (0 == 0 /\ -1 < 0 /\ arg2 > 0), cost: 1 New rule: f484_0_plus_LE -> f484_0_plus_LE : arg1'=arg1, arg2'=-1+arg2, arg3'=arg3p9, arg2 > 0, cost: 1 Removed Trivial Updates Original rule: f484_0_plus_LE -> f484_0_plus_LE : arg1'=arg1, arg2'=-1+arg2, arg3'=arg3p9, arg2 > 0, cost: 1 New rule: f484_0_plus_LE -> f484_0_plus_LE : arg2'=-1+arg2, arg3'=arg3p9, arg2 > 0, cost: 1 Propagated Equalities Original rule: f484_0_plus_LE -> f484_0_plus_LE : arg1'=arg1p10, arg2'=arg2p10, arg3'=arg3p10, (-arg2p10+arg2 == 0 /\ -1-arg1p10+arg1 == 0 /\ arg1 > 0 /\ -1 < 0 /\ -1+arg2 < 0), cost: 1 New rule: f484_0_plus_LE -> f484_0_plus_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p10, (0 == 0 /\ arg1 > 0 /\ -1 < 0 /\ -1+arg2 < 0), cost: 1 propagated equality arg2p10 = arg2 propagated equality arg1p10 = -1+arg1 Simplified Guard Original rule: f484_0_plus_LE -> f484_0_plus_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p10, (0 == 0 /\ arg1 > 0 /\ -1 < 0 /\ -1+arg2 < 0), cost: 1 New rule: f484_0_plus_LE -> f484_0_plus_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p10, (arg1 > 0 /\ -1+arg2 < 0), cost: 1 Removed Trivial Updates Original rule: f484_0_plus_LE -> f484_0_plus_LE : arg1'=-1+arg1, arg2'=arg2, arg3'=arg3p10, (arg1 > 0 /\ -1+arg2 < 0), cost: 1 New rule: f484_0_plus_LE -> f484_0_plus_LE : arg1'=-1+arg1, arg3'=arg3p10, (arg1 > 0 /\ -1+arg2 < 0), cost: 1 Eliminated Temporary Variables via Transitive Closure Original rule: __init -> f127_0_times_NE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (arg1p11 > 0 /\ 1+arg1p1 > 0 /\ 1+arg2p1 > 0 /\ -1+arg2p11 > 0), cost: 1 New rule: __init -> f127_0_times_NE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (1+arg1p1 > 0 /\ 1+arg2p1 > 0), cost: 1 Step with 21 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)] Blocked [{}, {}] Step with 13 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(1-arg2 == 0)] Blocked [{}, {}, {}] Step with 18 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(1-arg2 == 0)], 18[(arg1 > 0)] Blocked [{}, {}, {}, {}] Step with 19 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(1-arg2 == 0)], 18[(arg1 > 0)], 19[(arg2 > 0)] Blocked [{}, {}, {}, {}, {}] Accelerate Start location: __init Program variables: arg1 arg2 arg3 12: f127_0_times_NE -> f127_0_times_NE : arg2'=-1+arg2, arg3'=arg3p2, arg2 > 0, cost: 1 13: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg1, 1-arg2 == 0, cost: 1 14: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=0, arg3'=0, (-arg1 == 0 /\ arg2 > 0), cost: 1 15: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=arg2p5, arg3'=arg1, arg2 > 0, cost: 1 16: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=arg2p6, arg3'=0, (-arg1 == 0 /\ arg2 > 0), cost: 1 18: f469_0_times_InvokeMethod -> f484_0_plus_LE : arg1'=arg2, arg2'=arg3, arg3'=arg3p8, arg1 > 0, cost: 1 17: f218_0_times_Return -> f469_0_times_InvokeMethod : arg2'=arg3, arg3'=arg2, T, cost: 1 19: f484_0_plus_LE -> f484_0_plus_LE : arg2'=-1+arg2, arg3'=arg3p9, arg2 > 0, cost: 1 20: f484_0_plus_LE -> f484_0_plus_LE : arg1'=-1+arg1, arg3'=arg3p10, (arg1 > 0 /\ -1+arg2 < 0), cost: 1 22: f484_0_plus_LE -> f484_0_plus_LE : arg2'=-n+arg2, arg3'=arg3p9, (1-n+arg2 > 0 /\ -1+n >= 0), cost: 1 21: __init -> f127_0_times_NE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (1+arg1p1 > 0 /\ 1+arg2p1 > 0), cost: 1 Loop Acceleration Original rule: f484_0_plus_LE -> f484_0_plus_LE : arg2'=-1+arg2, arg3'=arg3p9, (arg2 > 0), cost: 1 New rule: f484_0_plus_LE -> f484_0_plus_LE : arg2'=-n+arg2, arg3'=arg3p9, (1-n+arg2 > 0 /\ -1+n >= 0), cost: 1 arg2 > 0 [0]: montonic decrease yields 1-n+arg2 > 0 arg2 > 0 [1]: eventual increase yields (1 <= 0 /\ arg2 > 0) Replacement map: {arg2 > 0 -> 1-n+arg2 > 0} Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(1-arg2 == 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)] Blocked [{}, {}, {}, {}, {19[T], 22[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(1-arg2 == 0)], 18[(arg1 > 0)] Blocked [{}, {}, {}, {22[T]}] Step with 19 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(1-arg2 == 0)], 18[(arg1 > 0)], 19[(arg2 > 0)] Blocked [{}, {}, {}, {22[T]}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(1-arg2 == 0)], 18[(arg1 > 0)] Blocked [{}, {}, {}, {19[T], 22[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 13[(1-arg2 == 0)] Blocked [{}, {}, {18[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)] Blocked [{}, {13[T]}] Step with 14 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(-arg1 == 0 /\ arg2 > 0)] Blocked [{}, {13[T]}, {}] Step with 18 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(-arg1 == 0 /\ arg2 > 0)], 18[(arg1 > 0)] Blocked [{}, {13[T]}, {}, {}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 14[(-arg1 == 0 /\ arg2 > 0)] Blocked [{}, {13[T]}, {18[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)] Blocked [{}, {13[T], 14[T]}] Step with 15 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)] Blocked [{}, {13[T], 14[T]}, {}] Step with 18 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T]}, {}, {}] Step with 19 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 19[(arg2 > 0)] Blocked [{}, {13[T], 14[T]}, {}, {}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T]}, {}, {19[T]}] Step with 20 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 20[(arg1 > 0 /\ -1+arg2 < 0)] Blocked [{}, {13[T], 14[T]}, {}, {19[T]}, {}] Accelerate Start location: __init Program variables: arg1 arg2 arg3 12: f127_0_times_NE -> f127_0_times_NE : arg2'=-1+arg2, arg3'=arg3p2, arg2 > 0, cost: 1 13: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg1, 1-arg2 == 0, cost: 1 14: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=0, arg3'=0, (-arg1 == 0 /\ arg2 > 0), cost: 1 15: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=arg2p5, arg3'=arg1, arg2 > 0, cost: 1 16: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=arg2p6, arg3'=0, (-arg1 == 0 /\ arg2 > 0), cost: 1 18: f469_0_times_InvokeMethod -> f484_0_plus_LE : arg1'=arg2, arg2'=arg3, arg3'=arg3p8, arg1 > 0, cost: 1 17: f218_0_times_Return -> f469_0_times_InvokeMethod : arg2'=arg3, arg3'=arg2, T, cost: 1 19: f484_0_plus_LE -> f484_0_plus_LE : arg2'=-1+arg2, arg3'=arg3p9, arg2 > 0, cost: 1 20: f484_0_plus_LE -> f484_0_plus_LE : arg1'=-1+arg1, arg3'=arg3p10, (arg1 > 0 /\ -1+arg2 < 0), cost: 1 22: f484_0_plus_LE -> f484_0_plus_LE : arg2'=-n+arg2, arg3'=arg3p9, (1-n+arg2 > 0 /\ -1+n >= 0), cost: 1 23: f484_0_plus_LE -> f484_0_plus_LE : arg1'=-n2+arg1, arg3'=arg3p10, (-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0), cost: 1 21: __init -> f127_0_times_NE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (1+arg1p1 > 0 /\ 1+arg2p1 > 0), cost: 1 Loop Acceleration Original rule: f484_0_plus_LE -> f484_0_plus_LE : arg1'=-1+arg1, arg3'=arg3p10, (arg1 > 0 /\ -1+arg2 < 0), cost: 1 New rule: f484_0_plus_LE -> f484_0_plus_LE : arg1'=-n2+arg1, arg3'=arg3p10, (-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0), cost: 1 arg1 > 0 [0]: montonic decrease yields 1-n2+arg1 > 0 arg1 > 0 [1]: eventual increase yields (1 <= 0 /\ arg1 > 0) 1-arg2 > 0 [0]: monotonic increase yields 1-arg2 > 0 Replacement map: {arg1 > 0 -> 1-n2+arg1 > 0, 1-arg2 > 0 -> 1-arg2 > 0} Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 23[(-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0)] Blocked [{}, {13[T], 14[T]}, {}, {19[T]}, {20[T], 23[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T]}, {}, {19[T], 23[T]}] Step with 20 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 20[(arg1 > 0 /\ -1+arg2 < 0)] Blocked [{}, {13[T], 14[T]}, {}, {19[T], 23[T]}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T]}, {}, {19[T], 20[T], 23[T]}] Step with 22 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 14[T]}, {}, {19[T], 20[T], 23[T]}, {22[T]}] Step with 23 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)], 23[(-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0)] Blocked [{}, {13[T], 14[T]}, {}, {19[T], 20[T], 23[T]}, {22[T]}, {23[T]}] Acceleration Failed marked recursive suffix as redundant Step with 20 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)], 23[(-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0)], 20[(arg1 > 0 /\ -1+arg2 < 0)] Blocked [{}, {13[T], 14[T]}, {}, {19[T], 20[T], 23[T]}, {22[T]}, {19[T], 23[T]}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)], 23[(-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0)] Blocked [{}, {13[T], 14[T]}, {}, {19[T], 20[T], 23[T]}, {22[T]}, {19[T], 20[T], 23[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 14[T]}, {}, {19[T], 20[T], 23[T]}, {22[T], 23[T]}] Step with 20 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)], 20[(arg1 > 0 /\ -1+arg2 < 0)] Blocked [{}, {13[T], 14[T]}, {}, {19[T], 20[T], 23[T]}, {22[T], 23[T]}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 14[T]}, {}, {19[T], 20[T], 23[T]}, {20[T], 22[T], 23[T]}] Step with 19 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)], 19[(arg2 > 0)] Blocked [{}, {13[T], 14[T]}, {}, {19[T], 20[T], 23[T]}, {20[T], 22[T], 23[T]}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 14[T]}, {}, {19[T], 20[T], 23[T]}, {19[T], 20[T], 22[T], 23[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T]}, {}, {19[T], 20[T], 22[T], 23[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 15[(arg2 > 0)] Blocked [{}, {13[T], 14[T]}, {18[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)] Blocked [{}, {13[T], 14[T], 15[T]}] Step with 16 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 16[(-arg1 == 0 /\ arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T]}, {}] Step with 18 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 16[(-arg1 == 0 /\ arg2 > 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T], 15[T]}, {}, {}] Step with 20 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 16[(-arg1 == 0 /\ arg2 > 0)], 18[(arg1 > 0)], 20[(arg1 > 0 /\ -1+arg2 < 0)] Blocked [{}, {13[T], 14[T], 15[T]}, {}, {19[T]}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 16[(-arg1 == 0 /\ arg2 > 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T], 15[T]}, {}, {19[T], 20[T]}] Step with 23 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 16[(-arg1 == 0 /\ arg2 > 0)], 18[(arg1 > 0)], 23[(-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T]}, {}, {19[T], 20[T], 22[T]}, {23[T]}] Step with 20 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 16[(-arg1 == 0 /\ arg2 > 0)], 18[(arg1 > 0)], 23[(-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0)], 20[(arg1 > 0 /\ -1+arg2 < 0)] Blocked [{}, {13[T], 14[T], 15[T]}, {}, {19[T], 20[T], 22[T]}, {19[T], 23[T]}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 16[(-arg1 == 0 /\ arg2 > 0)], 18[(arg1 > 0)], 23[(-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T]}, {}, {19[T], 20[T], 22[T]}, {19[T], 20[T], 23[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 16[(-arg1 == 0 /\ arg2 > 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T], 15[T]}, {}, {19[T], 20[T], 22[T], 23[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 16[(-arg1 == 0 /\ arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T]}, {18[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}] Step with 12 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {}] Accelerate Start location: __init Program variables: arg1 arg2 arg3 12: f127_0_times_NE -> f127_0_times_NE : arg2'=-1+arg2, arg3'=arg3p2, arg2 > 0, cost: 1 13: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=1, arg2'=0, arg3'=arg1, 1-arg2 == 0, cost: 1 14: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=0, arg3'=0, (-arg1 == 0 /\ arg2 > 0), cost: 1 15: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=arg2p5, arg3'=arg1, arg2 > 0, cost: 1 16: f127_0_times_NE -> f469_0_times_InvokeMethod : arg1'=arg2, arg2'=arg2p6, arg3'=0, (-arg1 == 0 /\ arg2 > 0), cost: 1 24: f127_0_times_NE -> f127_0_times_NE : arg2'=-n4+arg2, arg3'=arg3p2, (-1+n4 >= 0 /\ 1-n4+arg2 > 0), cost: 1 18: f469_0_times_InvokeMethod -> f484_0_plus_LE : arg1'=arg2, arg2'=arg3, arg3'=arg3p8, arg1 > 0, cost: 1 17: f218_0_times_Return -> f469_0_times_InvokeMethod : arg2'=arg3, arg3'=arg2, T, cost: 1 19: f484_0_plus_LE -> f484_0_plus_LE : arg2'=-1+arg2, arg3'=arg3p9, arg2 > 0, cost: 1 20: f484_0_plus_LE -> f484_0_plus_LE : arg1'=-1+arg1, arg3'=arg3p10, (arg1 > 0 /\ -1+arg2 < 0), cost: 1 22: f484_0_plus_LE -> f484_0_plus_LE : arg2'=-n+arg2, arg3'=arg3p9, (1-n+arg2 > 0 /\ -1+n >= 0), cost: 1 23: f484_0_plus_LE -> f484_0_plus_LE : arg1'=-n2+arg1, arg3'=arg3p10, (-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0), cost: 1 21: __init -> f127_0_times_NE : arg1'=arg1p1, arg2'=arg2p1, arg3'=arg3p1, (1+arg1p1 > 0 /\ 1+arg2p1 > 0), cost: 1 Loop Acceleration Original rule: f127_0_times_NE -> f127_0_times_NE : arg2'=-1+arg2, arg3'=arg3p2, (arg2 > 0), cost: 1 New rule: f127_0_times_NE -> f127_0_times_NE : arg2'=-n4+arg2, arg3'=arg3p2, (-1+n4 >= 0 /\ 1-n4+arg2 > 0), cost: 1 arg2 > 0 [0]: montonic decrease yields 1-n4+arg2 > 0 arg2 > 0 [1]: eventual increase yields (1 <= 0 /\ arg2 > 0) Replacement map: {arg2 > 0 -> 1-n4+arg2 > 0} Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 24[T]}] Step with 13 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 13[(1-arg2 == 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 24[T]}, {}] Step with 18 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 13[(1-arg2 == 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 24[T]}, {}, {}] Step with 22 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 13[(1-arg2 == 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 24[T]}, {}, {20[T]}, {22[T]}] Step with 19 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 13[(1-arg2 == 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)], 19[(arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 24[T]}, {}, {20[T]}, {22[T], 23[T]}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 13[(1-arg2 == 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 24[T]}, {}, {20[T]}, {19[T], 22[T], 23[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 13[(1-arg2 == 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 24[T]}, {}, {20[T], 22[T]}] Step with 19 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 13[(1-arg2 == 0)], 18[(arg1 > 0)], 19[(arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 24[T]}, {}, {20[T], 22[T]}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 13[(1-arg2 == 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 24[T]}, {}, {19[T], 20[T], 22[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 13[(1-arg2 == 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 24[T]}, {18[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 24[T]}] Step with 14 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 14[(-arg1 == 0 /\ arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 24[T]}, {}] Step with 18 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 14[(-arg1 == 0 /\ arg2 > 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 24[T]}, {}, {}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 14[(-arg1 == 0 /\ arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 24[T]}, {18[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}] Step with 15 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}] Step with 18 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {}] Step with 19 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 19[(arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {19[T]}] Step with 20 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 20[(arg1 > 0 /\ -1+arg2 < 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {19[T]}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {19[T], 20[T]}] Step with 22 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {19[T], 20[T]}, {22[T]}] Step with 23 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)], 23[(-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {19[T], 20[T]}, {22[T]}, {23[T]}] Step with 20 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)], 23[(-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0)], 20[(arg1 > 0 /\ -1+arg2 < 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {19[T], 20[T]}, {22[T]}, {19[T], 23[T]}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)], 23[(-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {19[T], 20[T]}, {22[T]}, {19[T], 20[T], 23[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {19[T], 20[T]}, {22[T], 23[T]}] Step with 20 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)], 20[(arg1 > 0 /\ -1+arg2 < 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {19[T], 20[T]}, {22[T], 23[T]}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {19[T], 20[T]}, {20[T], 22[T], 23[T]}] Step with 19 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)], 19[(arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {19[T], 20[T]}, {20[T], 22[T], 23[T]}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 22[(1-n+arg2 > 0 /\ -1+n >= 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {19[T], 20[T]}, {19[T], 20[T], 22[T], 23[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {19[T], 20[T], 22[T]}] Step with 23 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 23[(-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {19[T], 20[T], 22[T]}, {23[T]}] Step with 20 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 23[(-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0)], 20[(arg1 > 0 /\ -1+arg2 < 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {19[T], 20[T], 22[T]}, {19[T], 23[T]}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)], 23[(-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {19[T], 20[T], 22[T]}, {19[T], 20[T], 23[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {}, {19[T], 20[T], 22[T], 23[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 15[(arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 24[T]}, {18[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 15[T], 24[T]}] Step with 16 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 16[(-arg1 == 0 /\ arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 15[T], 24[T]}, {}] Step with 18 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 16[(-arg1 == 0 /\ arg2 > 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 15[T], 24[T]}, {}, {}] Step with 20 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 16[(-arg1 == 0 /\ arg2 > 0)], 18[(arg1 > 0)], 20[(arg1 > 0 /\ -1+arg2 < 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 15[T], 24[T]}, {}, {}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 16[(-arg1 == 0 /\ arg2 > 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 15[T], 24[T]}, {}, {20[T]}] Step with 23 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 16[(-arg1 == 0 /\ arg2 > 0)], 18[(arg1 > 0)], 23[(-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 15[T], 24[T]}, {}, {20[T], 22[T]}, {23[T]}] Step with 20 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 16[(-arg1 == 0 /\ arg2 > 0)], 18[(arg1 > 0)], 23[(-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0)], 20[(arg1 > 0 /\ -1+arg2 < 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 15[T], 24[T]}, {}, {20[T], 22[T]}, {19[T], 23[T]}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 16[(-arg1 == 0 /\ arg2 > 0)], 18[(arg1 > 0)], 23[(-1+n2 >= 0 /\ 1-n2+arg1 > 0 /\ 1-arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 15[T], 24[T]}, {}, {20[T], 22[T]}, {19[T], 20[T], 23[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 16[(-arg1 == 0 /\ arg2 > 0)], 18[(arg1 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 15[T], 24[T]}, {}, {20[T], 22[T], 23[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)], 16[(-arg1 == 0 /\ arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 15[T], 24[T]}, {18[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 24[(-1+n4 >= 0 /\ 1-n4+arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T]}, {12[T], 13[T], 14[T], 15[T], 16[T], 24[T]}] Backtrack Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T], 24[T]}] Step with 12 Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)], 12[(arg2 > 0)] Blocked [{}, {13[T], 14[T], 15[T], 16[T], 24[T]}, {}] Covered Trace 21[(1+arg1p1 > 0 /\ 1+arg2p1 > 0)] Blocked [{}, {12[T], 13[T], 14[T], 15[T], 16[T], 24[T]}] Backtrack Trace Blocked [{21[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b