Z3's AST hash table is quite slow and has a lot of collisions. Instead of increasing the hash table, Z3 keeps pouring entries into long chains for collision'ed keys.

Increasing the initial size of this hash table helps a lot for larger formulas.

Here's the dramatic before and after when running just vcgen for a few Alive2 benchmarks:

sqlite3 goes from 5.5 hours to < 1 hour! 😁

The number of collisions is still in O(crazy). There are other uses of chashtable that need investigation.
Another thing is that on expansion, collision lists get flipped, which is then terrible for deletion as expressions are deleted in LIFO order. So flipping the collisions lists triggers a quadratic factor in the number of the lists' sizes.
I've a patch that avoids flipping, but that needs further testing.