From 37ed4b04d078d6d1e35db2799d769e8d4b87f775 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Thu, 14 Aug 2014 12:18:00 +0100 Subject: [PATCH] Bugfix: param_refs didn't make it through to smt::solver (smt_params) in some cases. Thanks to user xor88 for pointing us in the right direction! Signed-off-by: Christoph M. Wintersteiger --- src/api/api_solver.cpp | 1 + 1 file changed, 1 insertion(+) diff --git a/src/api/api_solver.cpp b/src/api/api_solver.cpp index ac30a0c21..c8b1723f1 100644 --- a/src/api/api_solver.cpp +++ b/src/api/api_solver.cpp @@ -40,6 +40,7 @@ extern "C" { params_ref p = s->m_params; mk_c(c)->params().get_solver_params(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled); s->m_solver = (*(s->m_solver_factory))(mk_c(c)->m(), p, proofs_enabled, models_enabled, unsat_core_enabled, s->m_logic); + s->m_solver->updt_params(p); } static void init_solver(Z3_context c, Z3_solver s) {