Unbounded Infinite vs Bounded Infinite Domain for Universal Quantification over Reals in z3

[kgoyal40]

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.

[NikolajBjorner]

Is perf faster over integers than reals? Have you profiled overhead of the solver using a profiler with reals and measured whether it spends time resolving linear inequalities that don't exist in your other encoding?