Particularly, does it use DPLL(T)? Does it use under/over approximations? Does it handle linear arithmetic on a word level? What about non-linear arithmetic?
I found only a superficial mention of "simplifications similar to those in MathSAT/Boolector" in paper Efficiently Solving Quantified Bit-Vector Formulas.
It is extremely interesting what methods helped Z3 to get the first place in QF_BV section of smtcomp.