Nice, but I wonder if applying an SMT solver to just about every instruction in your program isn't likely to blow up sometimes. The solver is, after all, worst case NP complete.
The previous post states that the goal is to use the SMT solver offline to identify opportunities for improving the compiler: https://blog.regehr.org/archives/1709. Using the solver online isn't the goal.
Compilers don't need an exact solution, so they can always fall back to the simple heuristics based approach when the SMT based analysis is too expensive.
