Solvers now supports:
- pop(lvl)
- push
- check
- assertCnstr (assert would collapse with the usual assert())
- checkAssumptions
- getModel
- getUnsatCore

This API is supported naively by all non-z3 solvers