fix regression
add support for portfolio SMT solving
We will now pick specialized solvers from Z3 depending on whether there are qantifiers
or not
This change improves predicatbility of running time, and should improve performance for
larger tests as a side-effect.
Thanks to Santosh Nagarakatte for reporting the performance issue.