
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.

