diff --git a/src/solver/MathsatSmtSolver.cpp b/src/solver/MathsatSmtSolver.cpp
index 9627c8dea..16610f4ad 100644
--- a/src/solver/MathsatSmtSolver.cpp
+++ b/src/solver/MathsatSmtSolver.cpp
@@ -191,6 +191,7 @@ namespace storm {
 #endif
 		}
 
+#ifndef WINDOWS
 		SmtSolver::CheckResult MathsatSmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions)
 		{
 #ifdef STORM_HAVE_MSAT
@@ -218,6 +219,7 @@ namespace storm {
 			STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without MathSAT support.");
 #endif
 		}
+#endif
 
 		storm::expressions::SimpleValuation MathsatSmtSolver::getModelAsValuation()
 		{
diff --git a/src/solver/MathsatSmtSolver.h b/src/solver/MathsatSmtSolver.h
index badca77a8..a1ec0810b 100644
--- a/src/solver/MathsatSmtSolver.h
+++ b/src/solver/MathsatSmtSolver.h
@@ -79,7 +79,9 @@ namespace storm {
 
 			virtual CheckResult checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) override;
 
+#ifndef WINDOWS
 			virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) override;
+#endif
 
 			virtual storm::expressions::SimpleValuation getModelAsValuation() override;
 
diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h
index d97481b09..475c3ee95 100644
--- a/src/solver/SmtSolver.h
+++ b/src/solver/SmtSolver.h
@@ -152,8 +152,10 @@ namespace storm {
              * @param assumptions The assumptions to add to the call.
              * @return Sat if the conjunction of the asserted expressions together with the provided assumptions is
              * satisfiable, Unsat if it is unsatisfiable and Unknown if the solver could not determine satisfiability.
-             */
+			 */
+#ifndef WINDOWS
 			virtual CheckResult checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) = 0;
+#endif
             
 			/*!
              * If the last call to check() or checkWithAssumptions() returned Sat, this method retrieves a model that
diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h
index 2c7360b08..777bde9f9 100644
--- a/src/storage/expressions/Expression.h
+++ b/src/storage/expressions/Expression.h
@@ -324,4 +324,14 @@ namespace storm {
     }
 }
 
+//specialize 
+namespace std {
+	template<>
+	struct less < storm::expressions::Expression > {
+		bool operator()(const storm::expressions::Expression& lhs, const storm::expressions::Expression& rhs) const {
+			return lhs.getBaseExpressionPointer() < rhs.getBaseExpressionPointer();
+		}
+	};
+}
+
 #endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSION_H_ */
\ No newline at end of file