MAYBE Initial complexity problem: 1: T: (?, 1) f2(a, b) -> f2(d - 1, b) [ 0 >= c /\ 0 >= a + 1 ] (?, 1) f2(a, b) -> f2(d + 1, b) [ c >= 2 /\ 0 >= a + 1 ] (?, 1) f2(a, b) -> f2(d - 1, b) [ 0 >= c + 2 /\ a >= 1 ] (?, 1) f2(a, b) -> f2(d + 1, b) [ c >= 0 /\ a >= 1 ] (1, 1) f3(a, b) -> f2(a, b) (?, 1) f2(a, b) -> f300(0, d) [ 0 >= a + 1 ] (?, 1) f2(a, b) -> f300(0, d) [ a >= 1 ] (?, 1) f2(a, b) -> f300(a, d) [ a = 0 ] start location: f3 leaf cost: 0 Repeatedly removing leaves of the complexity graph in problem 1 produces the following problem: 2: T: (?, 1) f2(a, b) -> f2(d - 1, b) [ 0 >= c /\ 0 >= a + 1 ] (?, 1) f2(a, b) -> f2(d + 1, b) [ c >= 2 /\ 0 >= a + 1 ] (?, 1) f2(a, b) -> f2(d - 1, b) [ 0 >= c + 2 /\ a >= 1 ] (?, 1) f2(a, b) -> f2(d + 1, b) [ c >= 0 /\ a >= 1 ] (1, 1) f3(a, b) -> f2(a, b) start location: f3 leaf cost: 3 Complexity upper bound ? Time: 0.223 sec (SMT: 0.209 sec)