I'd definitely believe that cache plays a big role -- while I don't know nearly as much as the author about how SMT solvers work, I've seen how much Z3 bogs down when two instances are running in parallel. That's quite consistent with the cache explanation.