Changing variable name goes slower?

[DAHeath]

It seems that the solver runs significantly slower after updating the variable names.

Investigate why this is happening. It probably is something really stupid inside of Z3.

[DAHeath]

Indeed, variable naming does seem to have a huge impact on performance. Unfortunately this is probably not predictable from benchmark to benchmark. Here is the relevant issue in Z3 Z3Prover/z3#909