Power of ctx solver simplify

Feb 11, 2014 at 8:03 AM
If i use ctx solver simplify will it then always return false, if the sat solver finds the expression infeasible?

If i use the solver, is it then possible to extract a simplified version of the expression, that is close to as simplified as ctx solver simplify.

Basically i want to avoid to call both ctx solver simplify and then the regular sat solver.