Optimize the quantifier instantiation profiler

[utaal]

--profile currently requires a very low --rlimit to terminate in reasonable time. We've had multiple reports of this.

We may be able to optimize it by reducing the amount of data z3tracer collects, maybe similarly to what #267 tried to do. We ultimately decided not to merge #267 because it hasn't proven necessary/useful recently, and we'd like to improve the performance of --profile instead.

[ahuoguo]

Maybe switch from z3tracer to axiom-profiler-2?

[parno]

Indeed, I think that would be worthwhile at some point. When we discussed it in a group (either at a meeting or the Retreat), the consensus was that most people aren't unduly bottlenecked on the profiler's performance, so this was put on the back burner.