Solvers are no longer distinguished in 20 traits depending on what they
implement. It turns out that most leon solvers already implemented
everything:

1) Being interrupted
2) Push / Pop
3) checkAssertions/getUnsatCore (a naive implementation of these
   can be added by mixing NaiveAssumptionSolver in)