Reporter should be silent, as it fails on under-constrained expressions using selectors, lift solveSat to the level of Solvers