From 1d9b6096e68eda51b95ae92b69b1f91c4cff0f7b Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 24 May 2017 18:45:40 +0100 Subject: [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 --- lib/Solver/Z3Solver.cpp | 12 +++++++----- 1 file changed, 7 insertions(+), 5 deletions(-) (limited to 'lib/Solver/Z3Solver.cpp') 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 > *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); -- cgit 1.4.1