Right, the problem with SMT solvers (and the SAT solvers they're based on, although the problem there is slightly better) is that they're unpredictable and highly dependent on the form in which you pose the instance, often in very unintiitive ways (they can fail on an instance that you'd think would be as easy or even easier than another they do manage).