No longer report warnings for empty unsat cores, as they represent a valid scenario where unrolling is insufficient.

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