unknown Initial ITS Start location: [1] Program variables: x y z 0: [1] -> [2] : x'=nondet, T, cost: 1 1: [2] -> [3] : y'=nondet1, T, cost: 1 2: [3] -> [4] : z'=nondet2, T, cost: 1 3: [4] -> [5] : -y+x < 0, cost: 1 11: [4] -> [11] : -y+x >= 0, cost: 1 4: [5] -> [7] : -z+x < 0, cost: 1 7: [5] -> [9] : -z+x >= 0, cost: 1 10: [6] -> [4] : T, cost: 1 5: [7] -> [8] : x'=1+x, T, cost: 1 6: [8] -> [6] : T, cost: 1 8: [9] -> [10] : z'=1+z, T, cost: 1 9: [10] -> [6] : T, cost: 1 Chained Linear Paths Start location: [1] Program variables: x y z 13: [1] -> [4] : x'=nondet, y'=nondet1, z'=nondet2, T, cost: 1 3: [4] -> [5] : -y+x < 0, cost: 1 11: [4] -> [11] : -y+x >= 0, cost: 1 16: [5] -> [6] : x'=1+x, -z+x < 0, cost: 1 17: [5] -> [6] : z'=1+z, -z+x >= 0, cost: 1 10: [6] -> [4] : T, cost: 1 Eliminating location [2] by chaining: Applied chaining First rule: [1] -> [2] : x'=nondet, T, cost: 1 Second rule: [2] -> [3] : y'=nondet1, T, cost: 1 New rule: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1 Applied deletion Removed the following rules: 0 1 Eliminating location [3] by chaining: Applied chaining First rule: [1] -> [3] : x'=nondet, y'=nondet1, T, cost: 1 Second rule: [3] -> [4] : z'=nondet2, T, cost: 1 New rule: [1] -> [4] : x'=nondet, y'=nondet1, z'=nondet2, T, cost: 1 Applied deletion Removed the following rules: 2 12 Eliminating location [7] by chaining: Applied chaining First rule: [5] -> [7] : -z+x < 0, cost: 1 Second rule: [7] -> [8] : x'=1+x, T, cost: 1 New rule: [5] -> [8] : x'=1+x, -z+x < 0, cost: 1 Applied deletion Removed the following rules: 4 5 Eliminating location [9] by chaining: Applied chaining First rule: [5] -> [9] : -z+x >= 0, cost: 1 Second rule: [9] -> [10] : z'=1+z, T, cost: 1 New rule: [5] -> [10] : z'=1+z, -z+x >= 0, cost: 1 Applied deletion Removed the following rules: 7 8 Eliminating location [8] by chaining: Applied chaining First rule: [5] -> [8] : x'=1+x, -z+x < 0, cost: 1 Second rule: [8] -> [6] : T, cost: 1 New rule: [5] -> [6] : x'=1+x, -z+x < 0, cost: 1 Applied deletion Removed the following rules: 6 14 Eliminating location [10] by chaining: Applied chaining First rule: [5] -> [10] : z'=1+z, -z+x >= 0, cost: 1 Second rule: [10] -> [6] : T, cost: 1 New rule: [5] -> [6] : z'=1+z, -z+x >= 0, cost: 1 Applied deletion Removed the following rules: 9 15 Step with 13 Trace 13[T] Blocked [{}, {}] Step with 11 Trace 13[T], 11[(-y+x >= 0)] Blocked [{}, {}, {}] Backtrack Trace 13[T] Blocked [{}, {11[T]}] Step with 3 Trace 13[T], 3[(-y+x < 0)] Blocked [{}, {11[T]}, {}] Step with 16 Trace 13[T], 3[(-y+x < 0)], 16[(-z+x < 0)] Blocked [{}, {11[T]}, {}, {}] Step with 10 Trace 13[T], 3[(-y+x < 0)], 16[(-z+x < 0)], 10[T] Blocked [{}, {11[T]}, {}, {}, {}] Accelerate Start location: [1] Program variables: x y z 13: [1] -> [4] : x'=nondet, y'=nondet1, z'=nondet2, T, cost: 1 3: [4] -> [5] : -y+x < 0, cost: 1 11: [4] -> [11] : -y+x >= 0, cost: 1 18: [4] -> [4] : x'=n+x, (1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0), cost: 1 16: [5] -> [6] : x'=1+x, -z+x < 0, cost: 1 17: [5] -> [6] : z'=1+z, -z+x >= 0, cost: 1 10: [6] -> [4] : T, cost: 1 Loop Acceleration Original rule: [4] -> [4] : x'=1+x, (-y+x < 0 /\ -z+x < 0), cost: 1 New rule: [4] -> [4] : x'=n+x, (1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0), cost: 1 y-x > 0 [0]: montonic decrease yields 1-n+y-x > 0 y-x > 0 [1]: eventual increase yields (1 <= 0 /\ y-x > 0) z-x > 0 [0]: montonic decrease yields 1+z-n-x > 0 z-x > 0 [1]: eventual increase yields (1 <= 0 /\ z-x > 0) Replacement map: {y-x > 0 -> 1-n+y-x > 0, z-x > 0 -> 1+z-n-x > 0} Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)] Blocked [{}, {11[T]}, {18[T]}] Step with 11 Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 11[(-y+x >= 0)] Blocked [{}, {11[T]}, {18[T]}, {}] Backtrack Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)] Blocked [{}, {11[T]}, {11[T], 18[T]}] Step with 3 Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)] Blocked [{}, {11[T]}, {11[T], 18[T]}, {}] Step with 16 Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)], 16[(-z+x < 0)] Blocked [{}, {11[T]}, {11[T], 18[T]}, {}, {}] Step with 10 Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)], 16[(-z+x < 0)], 10[T] Blocked [{}, {11[T]}, {11[T], 18[T]}, {}, {}, {}] Covered Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)], 16[(-z+x < 0)] Blocked [{}, {11[T]}, {11[T], 18[T]}, {}, {10[T]}] Backtrack Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)] Blocked [{}, {11[T]}, {11[T], 18[T]}, {16[T]}] Step with 17 Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)], 17[(-z+x >= 0)] Blocked [{}, {11[T]}, {11[T], 18[T]}, {16[T]}, {}] Step with 10 Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)], 17[(-z+x >= 0)], 10[T] Blocked [{}, {11[T]}, {11[T], 18[T]}, {16[T]}, {}, {}] Accelerate Start location: [1] Program variables: x y z 13: [1] -> [4] : x'=nondet, y'=nondet1, z'=nondet2, T, cost: 1 3: [4] -> [5] : -y+x < 0, cost: 1 11: [4] -> [11] : -y+x >= 0, cost: 1 18: [4] -> [4] : x'=n+x, (1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0), cost: 1 19: [4] -> [4] : z'=z+n2, (y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0), cost: 1 16: [5] -> [6] : x'=1+x, -z+x < 0, cost: 1 17: [5] -> [6] : z'=1+z, -z+x >= 0, cost: 1 10: [6] -> [4] : T, cost: 1 Loop Acceleration Original rule: [4] -> [4] : z'=1+z, (-y+x < 0 /\ -z+x >= 0), cost: 1 New rule: [4] -> [4] : z'=z+n2, (y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0), cost: 1 y-x > 0 [0]: monotonic increase yields y-x > 0 -z+x >= 0 [0]: montonic decrease yields 1-z-n2+x >= 0 -z+x >= 0 [1]: eventual increase yields (1 <= 0 /\ -z+x >= 0) Replacement map: {y-x > 0 -> y-x > 0, -z+x >= 0 -> 1-z-n2+x >= 0} Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)] Blocked [{}, {11[T]}, {11[T], 18[T]}, {19[T]}] Accelerate Start location: [1] Program variables: x y z 13: [1] -> [4] : x'=nondet, y'=nondet1, z'=nondet2, T, cost: 1 3: [4] -> [5] : -y+x < 0, cost: 1 11: [4] -> [11] : -y+x >= 0, cost: 1 18: [4] -> [4] : x'=n+x, (1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0), cost: 1 19: [4] -> [4] : z'=z+n2, (y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0), cost: 1 20: [4] -> [4] : x'=n1*n3+x, z'=n3*n2+z, (1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0), cost: 1 16: [5] -> [6] : x'=1+x, -z+x < 0, cost: 1 17: [5] -> [6] : z'=1+z, -z+x >= 0, cost: 1 10: [6] -> [4] : T, cost: 1 Loop Acceleration Original rule: [4] -> [4] : x'=n1+x, z'=z+n2, (1-n1+y-x > 0 /\ -n1+y-x > 0 /\ -1+n1 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0), cost: 1 New rule: [4] -> [4] : x'=n1*n3+x, z'=n3*n2+z, (1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0), cost: 1 1-n1+y-x > 0 [0]: montonic decrease yields 1-n1+y-x-n1*(-1+n3) > 0, dependencies: -n1+y-x > 0 1-n1+y-x > 0 [1]: eventual decrease yields (1-n1+y-x-n1*(-1+n3) > 0 /\ 1-n1+y-x > 0) 1-n1+y-x > 0 [2]: eventual increase yields (1-n1+y-x > 0 /\ n1 <= 0) -n1+y-x > 0 [0]: montonic decrease yields -n1+y-x-n1*(-1+n3) > 0, dependencies: -1+n1 >= 0 -n1+y-x > 0 [1]: eventual decrease yields (-n1+y-x > 0 /\ -n1+y-x-n1*(-1+n3) > 0) -n1+y-x > 0 [2]: eventual increase yields (-n1+y-x > 0 /\ n1 <= 0) -1+n1 >= 0 [0]: monotonic increase yields -1+n1 >= 0 1-n1+z-x > 0 [0]: eventual decrease yields (1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ 1-n1+z-x > 0) 1-n1+z-x > 0 [1]: eventual increase yields (1-n1+z-x > 0 /\ n1-n2 <= 0) -1+n2 >= 0 [0]: monotonic increase yields -1+n2 >= 0 1+n1-z-n2+x >= 0 [0]: monotonic increase yields 1+n1-z-n2+x >= 0, dependencies: -1+n1 >= 0 1-n1+z-x > 0 Replacement map: {1-n1+y-x > 0 -> 1-n1+y-x-n1*(-1+n3) > 0, -n1+y-x > 0 -> -n1+y-x-n1*(-1+n3) > 0, -1+n1 >= 0 -> -1+n1 >= 0, 1-n1+z-x > 0 -> (1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ 1-n1+z-x > 0), -1+n2 >= 0 -> -1+n2 >= 0, 1+n1-z-n2+x >= 0 -> 1+n1-z-n2+x >= 0} Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)] Blocked [{}, {11[T]}, {20[T]}] Step with 3 Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)] Blocked [{}, {11[T]}, {11[T], 20[T]}, {}] Step with 16 Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)], 16[(-z+x < 0)] Blocked [{}, {11[T]}, {11[T], 20[T]}, {17[T]}, {}] Step with 10 Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)], 16[(-z+x < 0)], 10[T] Blocked [{}, {11[T]}, {11[T], 20[T]}, {17[T]}, {}, {}] Covered Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)], 16[(-z+x < 0)] Blocked [{}, {11[T]}, {11[T], 20[T]}, {17[T]}, {10[T]}] Backtrack Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)] Blocked [{}, {11[T]}, {11[T], 20[T]}, {16[T], 17[T]}] Backtrack Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)] Blocked [{}, {11[T]}, {3[T], 11[T], 20[T]}] Step with 18 Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)] Blocked [{}, {11[T]}, {3[T], 11[T], 20[T]}, {18[T]}] Acceleration Failed marked recursive suffix as redundant Step with 19 Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)] Blocked [{}, {11[T]}, {3[T], 11[T], 20[T]}, {18[T]}, {19[T]}] Covered Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)] Blocked [{}, {11[T]}, {3[T], 11[T], 20[T]}, {18[T], 19[T]}] Step with 11 Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 11[(-y+x >= 0)] Blocked [{}, {11[T]}, {3[T], 11[T], 20[T]}, {18[T], 19[T], 20[T]}, {}] Backtrack Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)] Blocked [{}, {11[T]}, {3[T], 11[T], 20[T]}, {11[T], 18[T], 19[T], 20[T]}] Step with 3 Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)] Blocked [{}, {11[T]}, {3[T], 11[T], 20[T]}, {11[T], 18[T], 19[T], 20[T]}, {}] Step with 17 Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)], 17[(-z+x >= 0)] Blocked [{}, {11[T]}, {3[T], 11[T], 20[T]}, {11[T], 18[T], 19[T], 20[T]}, {16[T]}, {}] Step with 10 Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)], 17[(-z+x >= 0)], 10[T] Blocked [{}, {11[T]}, {3[T], 11[T], 20[T]}, {11[T], 18[T], 19[T], 20[T]}, {16[T]}, {}, {}] Covered Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)], 17[(-z+x >= 0)] Blocked [{}, {11[T]}, {3[T], 11[T], 20[T]}, {11[T], 18[T], 19[T], 20[T]}, {16[T]}, {10[T]}] Backtrack Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)] Blocked [{}, {11[T]}, {3[T], 11[T], 20[T]}, {11[T], 18[T], 19[T], 20[T]}, {16[T], 17[T]}] Backtrack Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)] Blocked [{}, {11[T]}, {3[T], 11[T], 20[T]}, {3[T], 11[T], 18[T], 19[T], 20[T]}] Backtrack Trace 13[T], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)] Blocked [{}, {11[T]}, {3[T], 11[T], 18[T], 20[T]}] Backtrack Trace 13[T] Blocked [{}, {11[T], 20[T]}] Step with 3 Trace 13[T], 3[(-y+x < 0)] Blocked [{}, {11[T], 20[T]}, {}] Step with 17 Trace 13[T], 3[(-y+x < 0)], 17[(-z+x >= 0)] Blocked [{}, {11[T], 20[T]}, {}, {}] Step with 10 Trace 13[T], 3[(-y+x < 0)], 17[(-z+x >= 0)], 10[T] Blocked [{}, {11[T], 20[T]}, {}, {}, {}] Covered Trace 13[T], 3[(-y+x < 0)], 17[(-z+x >= 0)] Blocked [{}, {11[T], 20[T]}, {}, {10[T]}] Backtrack Trace 13[T], 3[(-y+x < 0)] Blocked [{}, {11[T], 20[T]}, {17[T]}] Step with 16 Trace 13[T], 3[(-y+x < 0)], 16[(-z+x < 0)] Blocked [{}, {11[T], 20[T]}, {17[T]}, {}] Step with 10 Trace 13[T], 3[(-y+x < 0)], 16[(-z+x < 0)], 10[T] Blocked [{}, {11[T], 20[T]}, {17[T]}, {}, {}] Covered Trace 13[T], 3[(-y+x < 0)], 16[(-z+x < 0)] Blocked [{}, {11[T], 20[T]}, {17[T]}, {10[T]}] Backtrack Trace 13[T], 3[(-y+x < 0)] Blocked [{}, {11[T], 20[T]}, {16[T], 17[T]}] Backtrack Trace 13[T] Blocked [{}, {3[T], 11[T], 20[T]}] Step with 18 Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)] Blocked [{}, {3[T], 11[T], 20[T]}, {18[T]}] Step with 19 Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)] Blocked [{}, {3[T], 11[T], 20[T]}, {18[T]}, {19[T]}] Covered Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)] Blocked [{}, {3[T], 11[T], 20[T]}, {18[T], 19[T]}] Step with 20 Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)] Blocked [{}, {3[T], 11[T], 20[T]}, {18[T], 19[T]}, {20[T]}] Covered Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)] Blocked [{}, {3[T], 11[T], 20[T]}, {18[T], 19[T], 20[T]}] Step with 11 Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 11[(-y+x >= 0)] Blocked [{}, {3[T], 11[T], 20[T]}, {18[T], 19[T], 20[T]}, {}] Backtrack Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)] Blocked [{}, {3[T], 11[T], 20[T]}, {11[T], 18[T], 19[T], 20[T]}] Step with 3 Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)] Blocked [{}, {3[T], 11[T], 20[T]}, {11[T], 18[T], 19[T], 20[T]}, {}] Step with 16 Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)], 16[(-z+x < 0)] Blocked [{}, {3[T], 11[T], 20[T]}, {11[T], 18[T], 19[T], 20[T]}, {}, {}] Step with 10 Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)], 16[(-z+x < 0)], 10[T] Blocked [{}, {3[T], 11[T], 20[T]}, {11[T], 18[T], 19[T], 20[T]}, {}, {}, {}] Covered Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)], 16[(-z+x < 0)] Blocked [{}, {3[T], 11[T], 20[T]}, {11[T], 18[T], 19[T], 20[T]}, {}, {10[T]}] Backtrack Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)] Blocked [{}, {3[T], 11[T], 20[T]}, {11[T], 18[T], 19[T], 20[T]}, {16[T]}] Step with 17 Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)], 17[(-z+x >= 0)] Blocked [{}, {3[T], 11[T], 20[T]}, {11[T], 18[T], 19[T], 20[T]}, {16[T]}, {}] Step with 10 Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)], 17[(-z+x >= 0)], 10[T] Blocked [{}, {3[T], 11[T], 20[T]}, {11[T], 18[T], 19[T], 20[T]}, {16[T]}, {}, {}] Covered Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)], 17[(-z+x >= 0)] Blocked [{}, {3[T], 11[T], 20[T]}, {11[T], 18[T], 19[T], 20[T]}, {16[T]}, {10[T]}] Backtrack Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)], 3[(-y+x < 0)] Blocked [{}, {3[T], 11[T], 20[T]}, {11[T], 18[T], 19[T], 20[T]}, {16[T], 17[T]}] Backtrack Trace 13[T], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)] Blocked [{}, {3[T], 11[T], 20[T]}, {3[T], 11[T], 18[T], 19[T], 20[T]}] Backtrack Trace 13[T] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}] Step with 19 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}, {19[T]}] Step with 20 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}, {19[T]}, {20[T]}] Acceleration Failed marked recursive suffix as redundant Step with 3 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}, {19[T]}, {11[T], 20[T]}, {}] Step with 16 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)], 16[(-z+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}, {19[T]}, {11[T], 20[T]}, {17[T]}, {}] Step with 10 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)], 16[(-z+x < 0)], 10[T] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}, {19[T]}, {11[T], 20[T]}, {17[T]}, {}, {}] Covered Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)], 16[(-z+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}, {19[T]}, {11[T], 20[T]}, {17[T]}, {10[T]}] Backtrack Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}, {19[T]}, {11[T], 20[T]}, {16[T], 17[T]}] Backtrack Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}, {19[T]}, {3[T], 11[T], 20[T]}] Step with 18 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}, {19[T]}, {3[T], 11[T], 20[T]}, {18[T]}] Accelerate Start location: [1] Program variables: x y z 13: [1] -> [4] : x'=nondet, y'=nondet1, z'=nondet2, T, cost: 1 3: [4] -> [5] : -y+x < 0, cost: 1 11: [4] -> [11] : -y+x >= 0, cost: 1 18: [4] -> [4] : x'=n+x, (1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0), cost: 1 19: [4] -> [4] : z'=z+n2, (y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0), cost: 1 20: [4] -> [4] : x'=n1*n3+x, z'=n3*n2+z, (1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0), cost: 1 21: [4] -> [4] : x'=n7*n+n13*n7*n33+x, z'=n7*n27*n33+n7*n26+z, (-1+n13 >= 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+n13+n13*(-1+n7)*n33+(-1+n7)*n-n27-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n26 >= 0 /\ 1-n13*(-1+n7)*n33-(-1+n7)*n-n13*n33-n+y-x > 0 /\ -n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+z+n27*n33+n26-n13*n33-n-x > 0 /\ 1-n13+z+n26-x > 0 /\ 1+n13*(-1+n7)*n33+(-1+n7)*n-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n >= 0 /\ -1+n27 >= 0 /\ 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 /\ 1-z-n26+x >= 0 /\ -n13*(-1+n7)*n33-(-1+n7)*n+y-x > 0), cost: 1 16: [5] -> [6] : x'=1+x, -z+x < 0, cost: 1 17: [5] -> [6] : z'=1+z, -z+x >= 0, cost: 1 10: [6] -> [4] : T, cost: 1 Loop Acceleration Original rule: [4] -> [4] : x'=n13*n33+n+x, z'=z+n27*n33+n26, (-1+n13 >= 0 /\ y-x > 0 /\ -1+n33 >= 0 /\ -1+n26 >= 0 /\ 1-n13*n33-n+y-x > 0 /\ 1+z+n27*n33+n26-n13*n33-n-x > 0 /\ 1-n13-n13*(-1+n33)+y-x > 0 /\ 1-n13+z+n26-x > 0 /\ -n13-n13*(-1+n33)+y-x > 0 /\ -1+n >= 0 /\ -1+n27 >= 0 /\ 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 /\ 1+n13-n27-z-n26+x >= 0 /\ 1-z-n26+x >= 0), cost: 1 New rule: [4] -> [4] : x'=n7*n+n13*n7*n33+x, z'=n7*n27*n33+n7*n26+z, (-1+n13 >= 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+n13+n13*(-1+n7)*n33+(-1+n7)*n-n27-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n26 >= 0 /\ 1-n13*(-1+n7)*n33-(-1+n7)*n-n13*n33-n+y-x > 0 /\ -n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+z+n27*n33+n26-n13*n33-n-x > 0 /\ 1-n13+z+n26-x > 0 /\ 1+n13*(-1+n7)*n33+(-1+n7)*n-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n >= 0 /\ -1+n27 >= 0 /\ 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 /\ 1-z-n26+x >= 0 /\ -n13*(-1+n7)*n33-(-1+n7)*n+y-x > 0), cost: 1 -1+n13 >= 0 [0]: monotonic increase yields -1+n13 >= 0 y-x > 0 [0]: montonic decrease yields -n13*(-1+n7)*n33-(-1+n7)*n+y-x > 0, dependencies: -1+n13 >= 0 -1+n33 >= 0 -1+n >= 0 y-x > 0 [1]: eventual decrease yields (y-x > 0 /\ -n13*(-1+n7)*n33-(-1+n7)*n+y-x > 0) y-x > 0 [2]: eventual increase yields (y-x > 0 /\ n13*n33+n <= 0) -1+n33 >= 0 [0]: monotonic increase yields -1+n33 >= 0 -1+n26 >= 0 [0]: monotonic increase yields -1+n26 >= 0 1-n13*n33-n+y-x > 0 [0]: montonic decrease yields 1-n13*(-1+n7)*n33-(-1+n7)*n-n13*n33-n+y-x > 0, dependencies: y-x > 0 1-n13*n33-n+y-x > 0 [1]: eventual increase yields (1-n13*n33-n+y-x > 0 /\ n13*n33+n <= 0) 1+z+n27*n33+n26-n13*n33-n-x > 0 [0]: monotonic increase yields 1+z+n27*n33+n26-n13*n33-n-x > 0, dependencies: -1+n26 >= 0 1-z-n26+x >= 0 1+z+n27*n33+n26-n13*n33-n-x > 0 [1]: eventual decrease yields (1-n13*(-1+n7)*n33-(-1+n7)*n+(-1+n7)*n26+z+n27*n33+n26+(-1+n7)*n27*n33-n13*n33-n-x > 0 /\ 1+z+n27*n33+n26-n13*n33-n-x > 0) 1+z+n27*n33+n26-n13*n33-n-x > 0 [2]: eventual increase yields (-n27*n33-n26+n13*n33+n <= 0 /\ 1+z+n27*n33+n26-n13*n33-n-x > 0) 1-n13-n13*(-1+n33)+y-x > 0 [0]: montonic decrease yields 1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0, dependencies: -n13-n13*(-1+n33)+y-x > 0 1-n13-n13*(-1+n33)+y-x > 0 [1]: eventual decrease yields (1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1-n13-n13*(-1+n33)+y-x > 0) 1-n13-n13*(-1+n33)+y-x > 0 [2]: eventual increase yields (n13*n33+n <= 0 /\ 1-n13-n13*(-1+n33)+y-x > 0) 1-n13+z+n26-x > 0 [0]: monotonic increase yields 1-n13+z+n26-x > 0, dependencies: -1+n26 >= 0 1+z+n27*n33+n26-n13*n33-n-x > 0 1-z-n26+x >= 0 1-n13+z+n26-x > 0 [1]: eventual decrease yields (1-n13+z+n26-x > 0 /\ 1-n13-n13*(-1+n7)*n33-(-1+n7)*n+(-1+n7)*n26+z+n26+(-1+n7)*n27*n33-x > 0) 1-n13+z+n26-x > 0 [2]: eventual increase yields (-n27*n33-n26+n13*n33+n <= 0 /\ 1-n13+z+n26-x > 0) -n13-n13*(-1+n33)+y-x > 0 [0]: montonic decrease yields -n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0, dependencies: 1-n13*n33-n+y-x > 0 -1+n >= 0 -n13-n13*(-1+n33)+y-x > 0 [1]: eventual decrease yields (-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ -n13-n13*(-1+n33)+y-x > 0) -n13-n13*(-1+n33)+y-x > 0 [2]: eventual increase yields (n13*n33+n <= 0 /\ -n13-n13*(-1+n33)+y-x > 0) -1+n >= 0 [0]: monotonic increase yields -1+n >= 0 -1+n27 >= 0 [0]: monotonic increase yields -1+n27 >= 0 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 [0]: monotonic increase yields 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0, dependencies: -1+n26 >= 0 1+z+n27*n33+n26-n13*n33-n-x > 0 1-z-n26+x >= 0 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 [1]: montonic decrease yields 1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+(-1+n33)*n27+(-1+n7)*n26+z+n26+(-1+n7)*n27*n33-x > 0, dependencies: 1+z+n27*n33+n26-n13*n33-n-x > 0 1-n13+z+n26-x > 0 -1+n >= 0 1+n13-n27-z-n26+x >= 0 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 [2]: eventual decrease yields (1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+(-1+n33)*n27+(-1+n7)*n26+z+n26+(-1+n7)*n27*n33-x > 0 /\ 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0) 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 [3]: eventual increase yields (-n27*n33-n26+n13*n33+n <= 0 /\ 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0) 1+n13-n27-z-n26+x >= 0 [0]: montonic decrease yields 1+n13+n13*(-1+n7)*n33+(-1+n7)*n-n27-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0, dependencies: -1+n26 >= 0 1+z+n27*n33+n26-n13*n33-n-x > 0 1-z-n26+x >= 0 1+n13-n27-z-n26+x >= 0 [1]: eventual decrease yields (1+n13+n13*(-1+n7)*n33+(-1+n7)*n-n27-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ 1+n13-n27-z-n26+x >= 0) 1+n13-n27-z-n26+x >= 0 [2]: eventual increase yields (n27*n33+n26-n13*n33-n <= 0 /\ 1+n13-n27-z-n26+x >= 0) 1-z-n26+x >= 0 [0]: eventual decrease yields (1+n13*(-1+n7)*n33+(-1+n7)*n-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ 1-z-n26+x >= 0) 1-z-n26+x >= 0 [1]: eventual increase yields (n27*n33+n26-n13*n33-n <= 0 /\ 1-z-n26+x >= 0) Replacement map: {-1+n13 >= 0 -> -1+n13 >= 0, y-x > 0 -> -n13*(-1+n7)*n33-(-1+n7)*n+y-x > 0, -1+n33 >= 0 -> -1+n33 >= 0, -1+n26 >= 0 -> -1+n26 >= 0, 1-n13*n33-n+y-x > 0 -> 1-n13*(-1+n7)*n33-(-1+n7)*n-n13*n33-n+y-x > 0, 1+z+n27*n33+n26-n13*n33-n-x > 0 -> 1+z+n27*n33+n26-n13*n33-n-x > 0, 1-n13-n13*(-1+n33)+y-x > 0 -> 1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0, 1-n13+z+n26-x > 0 -> 1-n13+z+n26-x > 0, -n13-n13*(-1+n33)+y-x > 0 -> -n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0, -1+n >= 0 -> -1+n >= 0, -1+n27 >= 0 -> -1+n27 >= 0, 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 -> 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0, 1+n13-n27-z-n26+x >= 0 -> 1+n13+n13*(-1+n7)*n33+(-1+n7)*n-n27-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0, 1-z-n26+x >= 0 -> (1+n13*(-1+n7)*n33+(-1+n7)*n-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ 1-z-n26+x >= 0)} Trace 13[T], 21[(-1+n13 >= 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+n13+n13*(-1+n7)*n33+(-1+n7)*n-n27-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n26 >= 0 /\ 1-n13*(-1+n7)*n33-(-1+n7)*n-n13*n33-n+y-x > 0 /\ -n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+z+n27*n33+n26-n13*n33-n-x > 0 /\ 1-n13+z+n26-x > 0 /\ 1+n13*(-1+n7)*n33+(-1+n7)*n-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n >= 0 /\ -1+n27 >= 0 /\ 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 /\ 1-z-n26+x >= 0 /\ -n13*(-1+n7)*n33-(-1+n7)*n+y-x > 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}, {21[T]}] Step with 11 Trace 13[T], 21[(-1+n13 >= 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+n13+n13*(-1+n7)*n33+(-1+n7)*n-n27-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n26 >= 0 /\ 1-n13*(-1+n7)*n33-(-1+n7)*n-n13*n33-n+y-x > 0 /\ -n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+z+n27*n33+n26-n13*n33-n-x > 0 /\ 1-n13+z+n26-x > 0 /\ 1+n13*(-1+n7)*n33+(-1+n7)*n-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n >= 0 /\ -1+n27 >= 0 /\ 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 /\ 1-z-n26+x >= 0 /\ -n13*(-1+n7)*n33-(-1+n7)*n+y-x > 0)], 11[(-y+x >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}, {21[T]}, {}] Backtrack Trace 13[T], 21[(-1+n13 >= 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+n13+n13*(-1+n7)*n33+(-1+n7)*n-n27-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n26 >= 0 /\ 1-n13*(-1+n7)*n33-(-1+n7)*n-n13*n33-n+y-x > 0 /\ -n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+z+n27*n33+n26-n13*n33-n-x > 0 /\ 1-n13+z+n26-x > 0 /\ 1+n13*(-1+n7)*n33+(-1+n7)*n-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n >= 0 /\ -1+n27 >= 0 /\ 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 /\ 1-z-n26+x >= 0 /\ -n13*(-1+n7)*n33-(-1+n7)*n+y-x > 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}, {11[T], 21[T]}] Step with 3 Trace 13[T], 21[(-1+n13 >= 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+n13+n13*(-1+n7)*n33+(-1+n7)*n-n27-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n26 >= 0 /\ 1-n13*(-1+n7)*n33-(-1+n7)*n-n13*n33-n+y-x > 0 /\ -n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+z+n27*n33+n26-n13*n33-n-x > 0 /\ 1-n13+z+n26-x > 0 /\ 1+n13*(-1+n7)*n33+(-1+n7)*n-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n >= 0 /\ -1+n27 >= 0 /\ 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 /\ 1-z-n26+x >= 0 /\ -n13*(-1+n7)*n33-(-1+n7)*n+y-x > 0)], 3[(-y+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}, {11[T], 21[T]}, {}] Step with 17 Trace 13[T], 21[(-1+n13 >= 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+n13+n13*(-1+n7)*n33+(-1+n7)*n-n27-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n26 >= 0 /\ 1-n13*(-1+n7)*n33-(-1+n7)*n-n13*n33-n+y-x > 0 /\ -n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+z+n27*n33+n26-n13*n33-n-x > 0 /\ 1-n13+z+n26-x > 0 /\ 1+n13*(-1+n7)*n33+(-1+n7)*n-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n >= 0 /\ -1+n27 >= 0 /\ 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 /\ 1-z-n26+x >= 0 /\ -n13*(-1+n7)*n33-(-1+n7)*n+y-x > 0)], 3[(-y+x < 0)], 17[(-z+x >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}, {11[T], 21[T]}, {16[T]}, {}] Step with 10 Trace 13[T], 21[(-1+n13 >= 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+n13+n13*(-1+n7)*n33+(-1+n7)*n-n27-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n26 >= 0 /\ 1-n13*(-1+n7)*n33-(-1+n7)*n-n13*n33-n+y-x > 0 /\ -n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+z+n27*n33+n26-n13*n33-n-x > 0 /\ 1-n13+z+n26-x > 0 /\ 1+n13*(-1+n7)*n33+(-1+n7)*n-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n >= 0 /\ -1+n27 >= 0 /\ 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 /\ 1-z-n26+x >= 0 /\ -n13*(-1+n7)*n33-(-1+n7)*n+y-x > 0)], 3[(-y+x < 0)], 17[(-z+x >= 0)], 10[T] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}, {11[T], 21[T]}, {16[T]}, {}, {}] Covered Trace 13[T], 21[(-1+n13 >= 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+n13+n13*(-1+n7)*n33+(-1+n7)*n-n27-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n26 >= 0 /\ 1-n13*(-1+n7)*n33-(-1+n7)*n-n13*n33-n+y-x > 0 /\ -n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+z+n27*n33+n26-n13*n33-n-x > 0 /\ 1-n13+z+n26-x > 0 /\ 1+n13*(-1+n7)*n33+(-1+n7)*n-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n >= 0 /\ -1+n27 >= 0 /\ 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 /\ 1-z-n26+x >= 0 /\ -n13*(-1+n7)*n33-(-1+n7)*n+y-x > 0)], 3[(-y+x < 0)], 17[(-z+x >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}, {11[T], 21[T]}, {16[T]}, {10[T]}] Backtrack Trace 13[T], 21[(-1+n13 >= 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+n13+n13*(-1+n7)*n33+(-1+n7)*n-n27-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n26 >= 0 /\ 1-n13*(-1+n7)*n33-(-1+n7)*n-n13*n33-n+y-x > 0 /\ -n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+z+n27*n33+n26-n13*n33-n-x > 0 /\ 1-n13+z+n26-x > 0 /\ 1+n13*(-1+n7)*n33+(-1+n7)*n-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n >= 0 /\ -1+n27 >= 0 /\ 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 /\ 1-z-n26+x >= 0 /\ -n13*(-1+n7)*n33-(-1+n7)*n+y-x > 0)], 3[(-y+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}, {11[T], 21[T]}, {16[T], 17[T]}] Backtrack Trace 13[T], 21[(-1+n13 >= 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+n13+n13*(-1+n7)*n33+(-1+n7)*n-n27-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n26 >= 0 /\ 1-n13*(-1+n7)*n33-(-1+n7)*n-n13*n33-n+y-x > 0 /\ -n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+z+n27*n33+n26-n13*n33-n-x > 0 /\ 1-n13+z+n26-x > 0 /\ 1+n13*(-1+n7)*n33+(-1+n7)*n-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n >= 0 /\ -1+n27 >= 0 /\ 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 /\ 1-z-n26+x >= 0 /\ -n13*(-1+n7)*n33-(-1+n7)*n+y-x > 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T]}, {3[T], 11[T], 21[T]}] Backtrack Trace 13[T] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}] Step with 19 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {19[T]}] Step with 20 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {19[T]}, {20[T]}] Step with 3 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {19[T]}, {11[T], 20[T], 21[T]}, {}] Step with 16 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)], 16[(-z+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {19[T]}, {11[T], 20[T], 21[T]}, {17[T]}, {}] Step with 10 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)], 16[(-z+x < 0)], 10[T] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {19[T]}, {11[T], 20[T], 21[T]}, {17[T]}, {}, {}] Covered Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)], 16[(-z+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {19[T]}, {11[T], 20[T], 21[T]}, {17[T]}, {10[T]}] Backtrack Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {19[T]}, {11[T], 20[T], 21[T]}, {16[T], 17[T]}] Backtrack Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {19[T]}, {3[T], 11[T], 20[T], 21[T]}] Step with 18 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {19[T]}, {3[T], 11[T], 20[T], 21[T]}, {18[T]}] Covered Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {19[T]}, {3[T], 11[T], 18[T], 20[T], 21[T]}] Backtrack Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {19[T], 20[T]}] Step with 18 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {19[T], 20[T]}, {18[T]}] Accelerate Start location: [1] Program variables: x y z 13: [1] -> [4] : x'=nondet, y'=nondet1, z'=nondet2, T, cost: 1 3: [4] -> [5] : -y+x < 0, cost: 1 11: [4] -> [11] : -y+x >= 0, cost: 1 18: [4] -> [4] : x'=n+x, (1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0), cost: 1 19: [4] -> [4] : z'=z+n2, (y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0), cost: 1 20: [4] -> [4] : x'=n1*n3+x, z'=n3*n2+z, (1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0), cost: 1 21: [4] -> [4] : x'=n7*n+n13*n7*n33+x, z'=n7*n27*n33+n7*n26+z, (-1+n13 >= 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+n13+n13*(-1+n7)*n33+(-1+n7)*n-n27-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n26 >= 0 /\ 1-n13*(-1+n7)*n33-(-1+n7)*n-n13*n33-n+y-x > 0 /\ -n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+z+n27*n33+n26-n13*n33-n-x > 0 /\ 1-n13+z+n26-x > 0 /\ 1+n13*(-1+n7)*n33+(-1+n7)*n-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n >= 0 /\ -1+n27 >= 0 /\ 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 /\ 1-z-n26+x >= 0 /\ -n13*(-1+n7)*n33-(-1+n7)*n+y-x > 0), cost: 1 22: [4] -> [4] : x'=n15*n+x, z'=n15*n28+z, (-(-1+n15)*n+y-x > 0 /\ y-x > 0 /\ 1-z-(-1+n15)*n28+(-1+n15)*n-n28+x >= 0 /\ 1-(-1+n15)*n-n+y-x > 0 /\ -1+n15 >= 0 /\ 1+z-n+n28-x > 0 /\ 1-z-n28+x >= 0 /\ -1+n >= 0 /\ -1+n28 >= 0), cost: 1 16: [5] -> [6] : x'=1+x, -z+x < 0, cost: 1 17: [5] -> [6] : z'=1+z, -z+x >= 0, cost: 1 10: [6] -> [4] : T, cost: 1 Loop Acceleration Original rule: [4] -> [4] : x'=n+x, z'=z+n28, (1-n+y-x > 0 /\ y-x > 0 /\ 1+z-n+n28-x > 0 /\ 1-z-n28+x >= 0 /\ -1+n >= 0 /\ -1+n28 >= 0), cost: 1 New rule: [4] -> [4] : x'=n15*n+x, z'=n15*n28+z, (-(-1+n15)*n+y-x > 0 /\ y-x > 0 /\ 1-z-(-1+n15)*n28+(-1+n15)*n-n28+x >= 0 /\ 1-(-1+n15)*n-n+y-x > 0 /\ -1+n15 >= 0 /\ 1+z-n+n28-x > 0 /\ 1-z-n28+x >= 0 /\ -1+n >= 0 /\ -1+n28 >= 0), cost: 1 1-n+y-x > 0 [0]: montonic decrease yields 1-(-1+n15)*n-n+y-x > 0, dependencies: y-x > 0 1+z-n+n28-x > 0 1-z-n28+x >= 0 1-n+y-x > 0 [1]: eventual decrease yields (1-n+y-x > 0 /\ 1-(-1+n15)*n-n+y-x > 0), dependencies: -1+n >= 0 1-n+y-x > 0 [2]: eventual increase yields (1-n+y-x > 0 /\ n <= 0), dependencies: -1+n >= 0 y-x > 0 [0]: montonic decrease yields -(-1+n15)*n+y-x > 0, dependencies: 1-n+y-x > 0 -1+n >= 0 y-x > 0 [1]: eventual decrease yields (-(-1+n15)*n+y-x > 0 /\ y-x > 0), dependencies: -1+n >= 0 y-x > 0 [2]: eventual increase yields (y-x > 0 /\ n <= 0), dependencies: -1+n >= 0 1+z-n+n28-x > 0 [0]: monotonic increase yields 1+z-n+n28-x > 0, dependencies: 1-z-n28+x >= 0 -1+n28 >= 0 1+z-n+n28-x > 0 [1]: eventual decrease yields (1+z-n+n28-x > 0 /\ 1+z+(-1+n15)*n28-(-1+n15)*n-n+n28-x > 0) 1+z-n+n28-x > 0 [2]: eventual increase yields (1+z-n+n28-x > 0 /\ n-n28 <= 0) 1-z-n28+x >= 0 [0]: eventual decrease yields (1-z-(-1+n15)*n28+(-1+n15)*n-n28+x >= 0 /\ 1-z-n28+x >= 0) 1-z-n28+x >= 0 [1]: eventual increase yields (-n+n28 <= 0 /\ 1-z-n28+x >= 0) -1+n >= 0 [0]: monotonic increase yields -1+n >= 0 -1+n28 >= 0 [0]: monotonic increase yields -1+n28 >= 0 Replacement map: {1-n+y-x > 0 -> 1-(-1+n15)*n-n+y-x > 0, y-x > 0 -> (-(-1+n15)*n+y-x > 0 /\ y-x > 0), 1+z-n+n28-x > 0 -> 1+z-n+n28-x > 0, 1-z-n28+x >= 0 -> (1-z-(-1+n15)*n28+(-1+n15)*n-n28+x >= 0 /\ 1-z-n28+x >= 0), -1+n >= 0 -> -1+n >= 0, -1+n28 >= 0 -> -1+n28 >= 0} Trace 13[T], 22[(-(-1+n15)*n+y-x > 0 /\ y-x > 0 /\ 1-z-(-1+n15)*n28+(-1+n15)*n-n28+x >= 0 /\ 1-(-1+n15)*n-n+y-x > 0 /\ -1+n15 >= 0 /\ 1+z-n+n28-x > 0 /\ 1-z-n28+x >= 0 /\ -1+n >= 0 /\ -1+n28 >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {22[T]}] Step with 11 Trace 13[T], 22[(-(-1+n15)*n+y-x > 0 /\ y-x > 0 /\ 1-z-(-1+n15)*n28+(-1+n15)*n-n28+x >= 0 /\ 1-(-1+n15)*n-n+y-x > 0 /\ -1+n15 >= 0 /\ 1+z-n+n28-x > 0 /\ 1-z-n28+x >= 0 /\ -1+n >= 0 /\ -1+n28 >= 0)], 11[(-y+x >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {22[T]}, {}] Backtrack Trace 13[T], 22[(-(-1+n15)*n+y-x > 0 /\ y-x > 0 /\ 1-z-(-1+n15)*n28+(-1+n15)*n-n28+x >= 0 /\ 1-(-1+n15)*n-n+y-x > 0 /\ -1+n15 >= 0 /\ 1+z-n+n28-x > 0 /\ 1-z-n28+x >= 0 /\ -1+n >= 0 /\ -1+n28 >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {11[T], 22[T]}] Step with 3 Trace 13[T], 22[(-(-1+n15)*n+y-x > 0 /\ y-x > 0 /\ 1-z-(-1+n15)*n28+(-1+n15)*n-n28+x >= 0 /\ 1-(-1+n15)*n-n+y-x > 0 /\ -1+n15 >= 0 /\ 1+z-n+n28-x > 0 /\ 1-z-n28+x >= 0 /\ -1+n >= 0 /\ -1+n28 >= 0)], 3[(-y+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {11[T], 22[T]}, {}] Step with 17 Trace 13[T], 22[(-(-1+n15)*n+y-x > 0 /\ y-x > 0 /\ 1-z-(-1+n15)*n28+(-1+n15)*n-n28+x >= 0 /\ 1-(-1+n15)*n-n+y-x > 0 /\ -1+n15 >= 0 /\ 1+z-n+n28-x > 0 /\ 1-z-n28+x >= 0 /\ -1+n >= 0 /\ -1+n28 >= 0)], 3[(-y+x < 0)], 17[(-z+x >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {11[T], 22[T]}, {16[T]}, {}] Step with 10 Trace 13[T], 22[(-(-1+n15)*n+y-x > 0 /\ y-x > 0 /\ 1-z-(-1+n15)*n28+(-1+n15)*n-n28+x >= 0 /\ 1-(-1+n15)*n-n+y-x > 0 /\ -1+n15 >= 0 /\ 1+z-n+n28-x > 0 /\ 1-z-n28+x >= 0 /\ -1+n >= 0 /\ -1+n28 >= 0)], 3[(-y+x < 0)], 17[(-z+x >= 0)], 10[T] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {11[T], 22[T]}, {16[T]}, {}, {}] Covered Trace 13[T], 22[(-(-1+n15)*n+y-x > 0 /\ y-x > 0 /\ 1-z-(-1+n15)*n28+(-1+n15)*n-n28+x >= 0 /\ 1-(-1+n15)*n-n+y-x > 0 /\ -1+n15 >= 0 /\ 1+z-n+n28-x > 0 /\ 1-z-n28+x >= 0 /\ -1+n >= 0 /\ -1+n28 >= 0)], 3[(-y+x < 0)], 17[(-z+x >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {11[T], 22[T]}, {16[T]}, {10[T]}] Backtrack Trace 13[T], 22[(-(-1+n15)*n+y-x > 0 /\ y-x > 0 /\ 1-z-(-1+n15)*n28+(-1+n15)*n-n28+x >= 0 /\ 1-(-1+n15)*n-n+y-x > 0 /\ -1+n15 >= 0 /\ 1+z-n+n28-x > 0 /\ 1-z-n28+x >= 0 /\ -1+n >= 0 /\ -1+n28 >= 0)], 3[(-y+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {11[T], 22[T]}, {16[T], 17[T]}] Backtrack Trace 13[T], 22[(-(-1+n15)*n+y-x > 0 /\ y-x > 0 /\ 1-z-(-1+n15)*n28+(-1+n15)*n-n28+x >= 0 /\ 1-(-1+n15)*n-n+y-x > 0 /\ -1+n15 >= 0 /\ 1+z-n+n28-x > 0 /\ 1-z-n28+x >= 0 /\ -1+n >= 0 /\ -1+n28 >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {3[T], 11[T], 22[T]}] Step with 19 Trace 13[T], 22[(-(-1+n15)*n+y-x > 0 /\ y-x > 0 /\ 1-z-(-1+n15)*n28+(-1+n15)*n-n28+x >= 0 /\ 1-(-1+n15)*n-n+y-x > 0 /\ -1+n15 >= 0 /\ 1+z-n+n28-x > 0 /\ 1-z-n28+x >= 0 /\ -1+n >= 0 /\ -1+n28 >= 0)], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {3[T], 11[T], 18[T], 22[T]}, {19[T]}] Covered Trace 13[T], 22[(-(-1+n15)*n+y-x > 0 /\ y-x > 0 /\ 1-z-(-1+n15)*n28+(-1+n15)*n-n28+x >= 0 /\ 1-(-1+n15)*n-n+y-x > 0 /\ -1+n15 >= 0 /\ 1+z-n+n28-x > 0 /\ 1-z-n28+x >= 0 /\ -1+n >= 0 /\ -1+n28 >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {3[T], 11[T], 18[T], 19[T], 22[T]}] Step with 21 Trace 13[T], 22[(-(-1+n15)*n+y-x > 0 /\ y-x > 0 /\ 1-z-(-1+n15)*n28+(-1+n15)*n-n28+x >= 0 /\ 1-(-1+n15)*n-n+y-x > 0 /\ -1+n15 >= 0 /\ 1+z-n+n28-x > 0 /\ 1-z-n28+x >= 0 /\ -1+n >= 0 /\ -1+n28 >= 0)], 21[(-1+n13 >= 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+n13+n13*(-1+n7)*n33+(-1+n7)*n-n27-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n26 >= 0 /\ 1-n13*(-1+n7)*n33-(-1+n7)*n-n13*n33-n+y-x > 0 /\ -n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+z+n27*n33+n26-n13*n33-n-x > 0 /\ 1-n13+z+n26-x > 0 /\ 1+n13*(-1+n7)*n33+(-1+n7)*n-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n >= 0 /\ -1+n27 >= 0 /\ 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 /\ 1-z-n26+x >= 0 /\ -n13*(-1+n7)*n33-(-1+n7)*n+y-x > 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {3[T], 11[T], 18[T], 19[T], 20[T], 22[T]}, {21[T]}] Covered Trace 13[T], 22[(-(-1+n15)*n+y-x > 0 /\ y-x > 0 /\ 1-z-(-1+n15)*n28+(-1+n15)*n-n28+x >= 0 /\ 1-(-1+n15)*n-n+y-x > 0 /\ -1+n15 >= 0 /\ 1+z-n+n28-x > 0 /\ 1-z-n28+x >= 0 /\ -1+n >= 0 /\ -1+n28 >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T]}, {3[T], 11[T], 18[T], 19[T], 20[T], 21[T], 22[T]}] Backtrack Trace 13[T] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}] Step with 19 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {19[T]}] Step with 20 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {19[T]}, {20[T]}] Step with 3 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {19[T]}, {11[T], 20[T], 21[T], 22[T]}, {}] Step with 16 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)], 16[(-z+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {19[T]}, {11[T], 20[T], 21[T], 22[T]}, {17[T]}, {}] Step with 10 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)], 16[(-z+x < 0)], 10[T] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {19[T]}, {11[T], 20[T], 21[T], 22[T]}, {17[T]}, {}, {}] Covered Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)], 16[(-z+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {19[T]}, {11[T], 20[T], 21[T], 22[T]}, {17[T]}, {10[T]}] Backtrack Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 3[(-y+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {19[T]}, {11[T], 20[T], 21[T], 22[T]}, {16[T], 17[T]}] Backtrack Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {19[T]}, {3[T], 11[T], 20[T], 21[T], 22[T]}] Step with 18 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {19[T]}, {3[T], 11[T], 20[T], 21[T], 22[T]}, {18[T]}] Covered Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 20[(1-n1+y-x-n1*(-1+n3) > 0 /\ -n1+y-x-n1*(-1+n3) > 0 /\ -1+n1 >= 0 /\ 1-n1+(-1+n3)*n2+z-x-n1*(-1+n3) > 0 /\ -1+n3 >= 0 /\ 1-n1+z-x > 0 /\ -1+n2 >= 0 /\ 1+n1-z-n2+x >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {19[T]}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}] Backtrack Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {19[T], 20[T]}] Step with 18 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 18[(1-n+y-x > 0 /\ -1+n >= 0 /\ 1+z-n-x > 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {19[T], 20[T]}, {18[T]}] Covered Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {18[T], 19[T], 20[T]}] Step with 21 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 21[(-1+n13 >= 0 /\ -1+n7 >= 0 /\ -1+n33 >= 0 /\ 1-n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+n13+n13*(-1+n7)*n33+(-1+n7)*n-n27-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n26 >= 0 /\ 1-n13*(-1+n7)*n33-(-1+n7)*n-n13*n33-n+y-x > 0 /\ -n13-n13*(-1+n7)*n33-n13*(-1+n33)-(-1+n7)*n+y-x > 0 /\ 1+z+n27*n33+n26-n13*n33-n-x > 0 /\ 1-n13+z+n26-x > 0 /\ 1+n13*(-1+n7)*n33+(-1+n7)*n-(-1+n7)*n26-z-n26-(-1+n7)*n27*n33+x >= 0 /\ -1+n >= 0 /\ -1+n27 >= 0 /\ 1-n13-n13*(-1+n33)+(-1+n33)*n27+z+n26-x > 0 /\ 1-z-n26+x >= 0 /\ -n13*(-1+n7)*n33-(-1+n7)*n+y-x > 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {18[T], 19[T], 20[T]}, {21[T]}] Covered Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {18[T], 19[T], 20[T], 21[T]}] Step with 22 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 22[(-(-1+n15)*n+y-x > 0 /\ y-x > 0 /\ 1-z-(-1+n15)*n28+(-1+n15)*n-n28+x >= 0 /\ 1-(-1+n15)*n-n+y-x > 0 /\ -1+n15 >= 0 /\ 1+z-n+n28-x > 0 /\ 1-z-n28+x >= 0 /\ -1+n >= 0 /\ -1+n28 >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {18[T], 19[T], 20[T], 21[T]}, {22[T]}] Covered Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {18[T], 19[T], 20[T], 21[T], 22[T]}] Step with 3 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 3[(-y+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {11[T], 18[T], 19[T], 20[T], 21[T], 22[T]}, {}] Step with 16 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 3[(-y+x < 0)], 16[(-z+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {11[T], 18[T], 19[T], 20[T], 21[T], 22[T]}, {}, {}] Step with 10 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 3[(-y+x < 0)], 16[(-z+x < 0)], 10[T] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {11[T], 18[T], 19[T], 20[T], 21[T], 22[T]}, {}, {}, {}] Covered Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 3[(-y+x < 0)], 16[(-z+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {11[T], 18[T], 19[T], 20[T], 21[T], 22[T]}, {}, {10[T]}] Backtrack Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 3[(-y+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {11[T], 18[T], 19[T], 20[T], 21[T], 22[T]}, {16[T]}] Step with 17 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 3[(-y+x < 0)], 17[(-z+x >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {11[T], 18[T], 19[T], 20[T], 21[T], 22[T]}, {16[T]}, {}] Step with 10 Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 3[(-y+x < 0)], 17[(-z+x >= 0)], 10[T] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {11[T], 18[T], 19[T], 20[T], 21[T], 22[T]}, {16[T]}, {}, {}] Covered Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 3[(-y+x < 0)], 17[(-z+x >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {11[T], 18[T], 19[T], 20[T], 21[T], 22[T]}, {16[T]}, {10[T]}] Backtrack Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)], 3[(-y+x < 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {11[T], 18[T], 19[T], 20[T], 21[T], 22[T]}, {16[T], 17[T]}] Backtrack Trace 13[T], 19[(y-x > 0 /\ 1-z-n2+x >= 0 /\ -1+n2 >= 0)] Blocked [{}, {3[T], 11[T], 18[T], 20[T], 21[T], 22[T]}, {3[T], 11[T], 18[T], 19[T], 20[T], 21[T], 22[T]}] Backtrack Trace 13[T] Blocked [{}, {3[T], 11[T], 18[T], 19[T], 20[T], 21[T], 22[T]}] Backtrack Trace Blocked [{13[T]}] Accept unknown Build SHA: a05f16bf13df659c382799650051f91bf6828c7b