This is a bit of a theoretical question. I was wondering if there's a difference in performance of z3 when solving universally quantified formulas over reals where the quantification is over a bounded infinite domain vs an unbounded infinite domain. I am working on something where I see that bounded infinite domains work much better in terms of performance and looking for a simple theoretical explanation for it. I am not able to find anything related in the literature, so any guidance would be appreciated.
The inner workings of most SMT solvers is black-box, where many heuristics/algorithms are in play. For arithmetic however, there are well-known techniques to deal with interesting fragments. I'd recommend reading through https://theory.stanford.edu/~nikolaj/programmingz3.html#sec-arithmetic, where they list what algorithms they use for each fragment.
Quantification is a totally different question. The usual approach is to apply quantifier elimination (https://en.wikipedia.org/wiki/Quantifier_elimination). z3 will perform quantifier elimination for linear-real arithmetic, but not for non-linear problems. See Does Z3 v4.3+ support quantifier elimination for NON-linear arithmetic, as the latter is a much more difficult problem and is not turned on by default.
Your particular case of putting bounds is an easy way to get rid of quantifiers, so it's not surprising that z3 might perform better. However, it's impossible to say without studying the internals if there are custom algorithms to take advantage of that. Your best bet is probably to ask at the z3 discussion forum, which I see you already have done: https://github.com/Z3Prover/z3/discussions/5949