[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

1 files changed, 7 insertions, 5 deletions

diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index f32860f7..4443c246 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -223,11 +223,13 @@ bool Z3SolverImpl::internalRunSolver(
     std::vector<std::vector<unsigned char> > *values, bool &hasSolution) {
 
   TimerStatIncrementer t(stats::queryTime);
-  // TODO: Does making a new solver for each query have a performance
-  // impact vs making one global solver and using push and pop?
-  // TODO: is the "simple_solver" the right solver to use for
-  // best performance?
-  Z3_solver theSolver = Z3_mk_simple_solver(builder->ctx);
+  // NOTE: Z3 will switch to using a slower solver internally if push/pop are
+  // used so for now it is likely that creating a new solver each time is the
+  // right way to go until Z3 changes its behaviour.
+  //
+  // TODO: Investigate using a custom tactic as described in
+  // https://github.com/klee/klee/issues/653
+  Z3_solver theSolver = Z3_mk_solver(builder->ctx);
   Z3_solver_inc_ref(builder->ctx, theSolver);
   Z3_solver_set_params(builder->ctx, theSolver, solverParameters);