The wiki page at https://github.com/FStarLang/FStar/wiki/Profiling-Z3-queries suggests using the Z3 Axiom Profiler; however, the Z3 Axiom Profiler seems to work reliably on Windows only.
How can I easily get the quantifiers that fire the most without the Z3 Axiom Profiler?
This command-line invocation works fine enough for me, relies only on z3's qi.profile feature, and leaves the top offenders at the bottom.
z3 smt.qi.profile=true queries-EverCrypt.Hash.Incremental-33.smt2 |& grep quantifier_instances | sort -t : -k 2 -n
(edited following Nik's answer to remove z3 options now embedded in the smt2 file)