PortfolioSolver with incremental smtlib solvers

[colder]

Portfolio solvers cannot be used incrementally if the underlying solvers are smt-lib based.

The issue is that whenever portfolio runs check() it waits until the first solver finishes and then interrupts all other solvers (to make sure there is no out-of-order messages, e.g. assert while check). Since interrupt is implement in smt-lib solvers by killing the smt process, solvers become unusable for subsequent commands and thus cannot be used incrementally.