In my experience SMT solvers tends to be an order of magnitude slower than MIP solvers, even when looking at the exact same constraints. But yes given a small enough problem SMT solvers like Z3 are an excellent choice and provide additional functionality like propositional logic (if A then B else C).