Create a fresh Z3 Solver for each instance.
It's about 20% faster on bit-blasted inputs, since the SAT solver is faster because
there are no more push/pops