diff --git a/src/solver/MathsatSmtSolver.cpp b/src/solver/MathsatSmtSolver.cpp index e46ab0ceb..9627c8dea 100644 --- a/src/solver/MathsatSmtSolver.cpp +++ b/src/solver/MathsatSmtSolver.cpp @@ -64,9 +64,9 @@ namespace storm { } #endif - MathsatSmtSolver::MathsatSmtSolver(storm::expressions::ExpressionManager& manager, Options const& options) + MathsatSmtSolver::MathsatSmtSolver(storm::expressions::ExpressionManager& manager, Options const& options) : SmtSolver(manager) #ifdef STORM_HAVE_MSAT - : SmtSolver(manager), expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown) + , expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown) #endif { #ifdef STORM_HAVE_MSAT diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index b8dcdb75b..800cb696d 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -44,16 +44,18 @@ namespace storm { #endif } - Z3SmtSolver::Z3SmtSolver(storm::expressions::ExpressionManager& manager) + Z3SmtSolver::Z3SmtSolver(storm::expressions::ExpressionManager& manager) : SmtSolver(manager) #ifdef STORM_HAVE_Z3 - : SmtSolver(manager), context(nullptr), solver(nullptr), expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown) + , context(nullptr), solver(nullptr), expressionAdapter(nullptr), lastCheckAssumptions(false), lastResult(CheckResult::Unknown) #endif { +#ifdef STORM_HAVE_Z3 z3::config config; config.set("model", true); context = std::unique_ptr(new z3::context(config)); solver = std::unique_ptr(new z3::solver(*context)); expressionAdapter = std::unique_ptr(new storm::adapters::Z3ExpressionAdapter(this->getManager(), *context)); +#endif } Z3SmtSolver::~Z3SmtSolver() {