[Z3] Switch from `Z3_mk_simple_solver()` to `Z3_mk_solver()`.

My discussions [1] with the Z3 team have revealed that
`Z3_mk_simple_solver()` is the wrong solver to use. That solver
basically runs the `simplify` tactic and then the `smt` tactic.
This by-passes Z3's attempt to probe for different logics and
apply its own specialized tactic.

Using `Z3_mk_solver()` should be closer to the behaviour of the
Z3 binary.

This partially addresses #653. We still need to try rolling our
own custom tactic.

[1] https://github.com/Z3Prover/z3/issues/1035

0 files changed, 0 insertions, 0 deletions