From 25db3f9d0f65fde97d3265ea3884d82601f9c3a7 Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Thu, 8 Jan 2015 11:48:48 +0100
Subject: [PATCH 1/2] 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<z3::context>(new z3::context(config));
             solver = std::unique_ptr<z3::solver>(new z3::solver(*context));
             expressionAdapter = std::unique_ptr<storm::adapters::Z3ExpressionAdapter>(new storm::adapters::Z3ExpressionAdapter(*context, true));
+#endif
         }
         
 		Z3SmtSolver::~Z3SmtSolver() {

From 43c63f1cb69bbb5664ce3c0263286dfa1623b72e Mon Sep 17 00:00:00 2001
From: svkurowski <sascha.kurowski@rwth-aachen.de>
Date: Thu, 8 Jan 2015 15:06:22 +0100
Subject: [PATCH 2/2] Fixed typo from aa025df9

Former-commit-id: 9d0328651cec904119a684ff5fcc61ccaae43a65
---
 src/solver/Z3SmtSolver.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp
index 7db1816ce..1a30d6a49 100644
--- a/src/solver/Z3SmtSolver.cpp
+++ b/src/solver/Z3SmtSolver.cpp
@@ -1,4 +1,4 @@
-#include "src/solver/Z3Smtsolver.h"
+#include "src/solver/Z3SmtSolver.h"
 
 #include "src/exceptions/NotSupportedException.h"
 #include "src/exceptions/InvalidStateException.h"