diff --git a/src/modelchecker/ExplicitQualitativeCheckResult.cpp b/src/modelchecker/ExplicitQualitativeCheckResult.cpp index b688bb1d8..114819af6 100644 --- a/src/modelchecker/ExplicitQualitativeCheckResult.cpp +++ b/src/modelchecker/ExplicitQualitativeCheckResult.cpp @@ -111,10 +111,18 @@ namespace storm { out << std::boolalpha; map_type const& map = boost::get(truthValues); + +#ifndef WINDOWS typename map_type::const_iterator it = map.begin(); typename map_type::const_iterator itPlusOne = map.begin(); ++itPlusOne; typename map_type::const_iterator ite = map.end(); +#else + map_type::const_iterator it = map.begin(); + map_type::const_iterator itPlusOne = map.begin(); + ++itPlusOne; + map_type::const_iterator ite = map.end(); +#endif for (; it != ite; ++itPlusOne, ++it) { out << it->second; diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp index 4ac0cbd16..86ca64a6b 100644 --- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp +++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp @@ -1,6 +1,7 @@ #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h" #include +#include #ifdef PARAMETRIC_SYSTEMS #include "src/storage/parameters.h" diff --git a/src/solver/SmtSolver.h b/src/solver/SmtSolver.h index 7425e8187..d97481b09 100644 --- a/src/solver/SmtSolver.h +++ b/src/solver/SmtSolver.h @@ -70,9 +70,15 @@ namespace storm { virtual ~SmtSolver(); SmtSolver(SmtSolver const& other) = default; + +#ifndef WINDOWS SmtSolver(SmtSolver&& other) = default; +#endif SmtSolver& operator=(SmtSolver const& other) = default; + +#ifndef WINDOWS SmtSolver& operator=(SmtSolver&& other) = default; +#endif /*! * Pushes a backtracking point on the solver's stack. A following call to pop() deletes exactly those diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp index 0e89d1d6c..b8b93431a 100644 --- a/src/solver/Z3SmtSolver.cpp +++ b/src/solver/Z3SmtSolver.cpp @@ -155,6 +155,7 @@ namespace storm { #endif } +#ifndef WINDOWS SmtSolver::CheckResult Z3SmtSolver::checkWithAssumptions(std::initializer_list const& assumptions) { #ifdef STORM_HAVE_Z3 @@ -181,7 +182,7 @@ namespace storm { STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); #endif } - +#endif storm::expressions::SimpleValuation Z3SmtSolver::getModelAsValuation() { #ifdef STORM_HAVE_Z3 @@ -229,7 +230,7 @@ namespace storm { { #ifdef STORM_HAVE_Z3 std::vector valuations; - this->allSat(important, [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; }); + this->allSat(important, static_cast>([&valuations](storm::expressions::SimpleValuation const& valuation) -> bool { valuations.push_back(valuation); return true; })); return valuations; #else STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "StoRM is compiled without Z3 support."); diff --git a/src/solver/Z3SmtSolver.h b/src/solver/Z3SmtSolver.h index 1e0fd2a43..1873cb4df 100644 --- a/src/solver/Z3SmtSolver.h +++ b/src/solver/Z3SmtSolver.h @@ -51,7 +51,9 @@ namespace storm { virtual CheckResult checkWithAssumptions(std::set const& assumptions) override; +#ifndef WINDOWS virtual CheckResult checkWithAssumptions(std::initializer_list const& assumptions) override; +#endif virtual storm::expressions::SimpleValuation getModelAsValuation() override; diff --git a/src/storage/expressions/LinearCoefficientVisitor.h b/src/storage/expressions/LinearCoefficientVisitor.h index 3b675a60d..b48c53d09 100644 --- a/src/storage/expressions/LinearCoefficientVisitor.h +++ b/src/storage/expressions/LinearCoefficientVisitor.h @@ -18,8 +18,10 @@ namespace storm { VariableCoefficients(VariableCoefficients const& other) = default; VariableCoefficients& operator=(VariableCoefficients const& other) = default; +#ifndef WINDOWS VariableCoefficients(VariableCoefficients&& other) = default; VariableCoefficients& operator=(VariableCoefficients&& other) = default; +#endif VariableCoefficients& operator+=(VariableCoefficients&& other); VariableCoefficients& operator-=(VariableCoefficients&& other);