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).

Specialized is necessary due to business requirements.

User requests aren't always "here's a problem + the data, solve this to optimal". Here are other examples:

1. "here's the problem + data, solve it well enough within 10s" 2. "here's the problem + data, solve it well enough with a subset of the data" 3. "here's the problem + data, solve it partially, and then when near real-time updates come in, update solution to take new information into account"