Understanding performance of QFBV SMT solvers
The short answer is no, we don't understand it.  The long answer is yes, we have some bounds, but those bounds aren't very helpful.  It's quite clear that the worst-case running time is exponential.  That's not very helpful, because we know that in some/many practical situations, it seems to run fairly rapidly -- and we don't really know why.

We don't know why that is true for SAT solvers, let alone for QFBV.  Understanding why QFBV solvers are often fast seems at least as hard as understanding why SAT solvers are often fast, which is already beyond our current level of understanding.  If you search more on this site you can find a summary of current attempts to understand the latter topic.