From 25db3f9d0f65fde97d3265ea3884d82601f9c3a7 Mon Sep 17 00:00:00 2001 From: dehnert Date: Thu, 8 Jan 2015 11:48:48 +0100 Subject: [PATCH] Fixed error that prevents compilation if Z3 is not present. Former-commit-id: d8de79f2ae7a32c64b814af5c3a394437c0d9ebe --- src/solver/Z3SmtSolver.cpp | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index 09daf9ae0..7db1816ce 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -46,11 +46,13 @@ namespace storm { : 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(*context, true)); +#endif } Z3SmtSolver::~Z3SmtSolver() {