Dear Johannes,
but in these cases (complexity) I think that Aprove has some (trivial) bound very early, but keeps looking for better bounds, and prints the trivial bound only at the very last moment.
Yes, most likely that's what happening. AProVE keeps searching for better bounds until it either manages to prove a tight complexity bound, or all available techniques terminated. If the time limit is exceeded, it tries to output the best result that has been found so far before it gets killed, but that can fail if it's stuck in an expensive computation.
One could have a different mode for competition: output is a sequence of (true) statements BOUNDS(low,hi) (of nested intervals), and the last (narrowest) one counts. I think applications would prefer something like this as well.
That's a good idea (even though it might be quite a bit of work to adapt the implementation).
Best Florian