I am a user of SMT. Just switched and testing whether Mathematica can solve inequalities with constraints or not. Surprisingly, It can. But I need to know what procedures and algorithm Mathematica uses for quantifier elimination procedures. Is it the same as Z3, or other SMT tools or not. If not then what is the difference.
Kindly help me with the feedback.