diff --git a/src/adapters/Z3ExpressionAdapter.h b/src/adapters/Z3ExpressionAdapter.h
index 428ccd0ce..81e8a222e 100644
--- a/src/adapters/Z3ExpressionAdapter.h
+++ b/src/adapters/Z3ExpressionAdapter.h
@@ -39,9 +39,9 @@ namespace storm {
             Z3ExpressionAdapter(z3::context& context, std::map<std::string, z3::expr> const& variableToExpressionMap)
 				: context(context)
 				, stack()
-				, variableToExpressionMap(variableToExpressionMap)
-				, additionalVariableCounter(0)
-				, additionalAssertions() {
+				, additionalAssertions()
+                , additionalVariableCounter(0)
+                , variableToExpressionMap(variableToExpressionMap) {
                 // Intentionally left empty.
             }
             
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index b026880d3..5d73e9d2a 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -265,10 +265,12 @@ namespace storm {
             return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, expression, this->getFilename());
         }
         
-        storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) const {
+        storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) {
             if (!this->secondRun) {
                 LOG_THROW(this->identifiers_.find(formulaName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << formulaName << "'.");
                 this->identifiers_.add(formulaName, expression);
+            } else {
+                this->identifiers_.at(formulaName) = expression;
             }
             return storm::prism::Formula(formulaName, expression, this->getFilename());
         }
diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h
index bdf84af24..ac36883e9 100644
--- a/src/parser/PrismParser.h
+++ b/src/parser/PrismParser.h
@@ -225,7 +225,7 @@ namespace storm {
             storm::prism::Constant createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const;
             storm::prism::Constant createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const;
             storm::prism::Constant createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const;
-            storm::prism::Formula createFormula(std::string const& formulaName, storm::expressions::Expression expression) const;
+            storm::prism::Formula createFormula(std::string const& formulaName, storm::expressions::Expression expression);
             storm::prism::Label createLabel(std::string const& labelName, storm::expressions::Expression expression) const;
             storm::prism::RewardModel createRewardModel(std::string const& rewardModelName, std::vector<storm::prism::StateReward> const& stateRewards, std::vector<storm::prism::TransitionReward> const& transitionRewards) const;
             storm::prism::StateReward createStateReward(storm::expressions::Expression statePredicateExpression, storm::expressions::Expression rewardValueExpression) const;
diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp
index c2d58367b..42ad53c2e 100644
--- a/src/solver/Z3SmtSolver.cpp
+++ b/src/solver/Z3SmtSolver.cpp
@@ -7,9 +7,9 @@ namespace storm {
 #ifdef STORM_HAVE_Z3
 			: m_context()
 			, m_solver(m_context)
-			, m_adapter(m_context, {})
-			, lastResult(CheckResult::UNKNOWN)
+			, m_adapter(m_context, std::map<std::string, z3::expr>())
 			, lastCheckAssumptions(false)
+            , lastResult(CheckResult::UNKNOWN)
 #endif
 		{
 			//intentionally left empty
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index c6bfd0214..5042bb2e7 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -778,8 +778,8 @@ namespace storm {
                                   const_iterator ite;
                                   std::vector<uint_fast64_t>::const_iterator rowIterator = this->rowIndications.begin() + startRow;
                                   std::vector<uint_fast64_t>::const_iterator rowIteratorEnd = this->rowIndications.begin() + endRow;
-                                  std::vector<T>::iterator resultIterator = result.begin() + startRow;
-                                  std::vector<T>::iterator resultIteratorEnd = result.begin() + endRow;
+                                  typename std::vector<T>::iterator resultIterator = result.begin() + startRow;
+                                  typename std::vector<T>::iterator resultIteratorEnd = result.begin() + endRow;
                                   
                                   for (; resultIterator != resultIteratorEnd; ++rowIterator, ++resultIterator) {
                                       *resultIterator = storm::utility::constantZero<T>();
diff --git a/test/functional/adapter/Z3ExpressionAdapterTest.cpp b/test/functional/adapter/Z3ExpressionAdapterTest.cpp
index ce7abc105..b92a0ec03 100644
--- a/test/functional/adapter/Z3ExpressionAdapterTest.cpp
+++ b/test/functional/adapter/Z3ExpressionAdapterTest.cpp
@@ -11,7 +11,7 @@ TEST(Z3ExpressionAdapter, StormToZ3Basic) {
 	z3::solver s(ctx);
 	z3::expr conjecture = ctx.bool_val(false);
 
-	storm::adapters::Z3ExpressionAdapter adapter(ctx, {});
+	storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map<std::string, z3::expr>());
 
 	storm::expressions::Expression exprTrue = storm::expressions::Expression::createTrue();
 	z3::expr z3True = ctx.bool_val(true);
@@ -54,7 +54,7 @@ TEST(Z3ExpressionAdapter, StormToZ3Integer) {
 	z3::solver s(ctx);
 	z3::expr conjecture = ctx.bool_val(false);
 
-	storm::adapters::Z3ExpressionAdapter adapter(ctx, {});
+	storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map<std::string, z3::expr>());
 
 	storm::expressions::Expression exprAdd = (storm::expressions::Expression::createIntegerVariable("x") + storm::expressions::Expression::createIntegerVariable("y") < -storm::expressions::Expression::createIntegerVariable("y"));
 	z3::expr z3Add = (ctx.int_const("x") + ctx.int_const("y") < -ctx.int_const("y"));
@@ -81,7 +81,7 @@ TEST(Z3ExpressionAdapter, StormToZ3Real) {
 	z3::solver s(ctx);
 	z3::expr conjecture = ctx.bool_val(false);
 
-	storm::adapters::Z3ExpressionAdapter adapter(ctx, {});
+	storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map<std::string, z3::expr>());
 
 	storm::expressions::Expression exprAdd = (storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createDoubleVariable("y") < -storm::expressions::Expression::createDoubleVariable("y"));
 	z3::expr z3Add = (ctx.real_const("x") + ctx.real_const("y") < -ctx.real_const("y"));
@@ -108,7 +108,7 @@ TEST(Z3ExpressionAdapter, StormToZ3TypeErrors) {
 	z3::solver s(ctx);
 	z3::expr conjecture = ctx.bool_val(false);
 
-	storm::adapters::Z3ExpressionAdapter adapter(ctx, {});
+	storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map<std::string, z3::expr>());
 
 	storm::expressions::Expression exprFail1 = (storm::expressions::Expression::createDoubleVariable("x") + storm::expressions::Expression::createIntegerVariable("y") < -storm::expressions::Expression::createDoubleVariable("y"));
 	ASSERT_THROW(conjecture = adapter.translateExpression(exprFail1, true), storm::exceptions::InvalidTypeException);
@@ -124,7 +124,7 @@ TEST(Z3ExpressionAdapter, StormToZ3FloorCeil) {
 	z3::solver s(ctx);
 	z3::expr conjecture = ctx.bool_val(false);
 
-	storm::adapters::Z3ExpressionAdapter adapter(ctx, {});
+	storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map<std::string, z3::expr>());
 
 	storm::expressions::Expression exprFloor = ((storm::expressions::Expression::createDoubleVariable("d").floor()) == storm::expressions::Expression::createIntegerVariable("i") && storm::expressions::Expression::createDoubleVariable("d") > storm::expressions::Expression::createDoubleLiteral(4.1) && storm::expressions::Expression::createDoubleVariable("d") < storm::expressions::Expression::createDoubleLiteral(4.991));
 	z3::expr z3Floor = ctx.int_val(4) == ctx.int_const("i");
@@ -167,7 +167,7 @@ TEST(Z3ExpressionAdapter, Z3ToStormBasic) {
 
 	unsigned args = 2;
 
-	storm::adapters::Z3ExpressionAdapter adapter(ctx, {});
+	storm::adapters::Z3ExpressionAdapter adapter(ctx, std::map<std::string, z3::expr>());
 
 	z3::expr z3True = ctx.bool_val(true);
 	storm::expressions::Expression exprTrue;