diff --git a/src/storm-pars/api/region.h b/src/storm-pars/api/region.h
index 85a481d2d..27d35d526 100644
--- a/src/storm-pars/api/region.h
+++ b/src/storm-pars/api/region.h
@@ -18,6 +18,8 @@
 #include "storm-pars/storage/ParameterRegion.h"
 #include "storm-pars/utility/parameterlifting.h"
 
+#include "storm/environment/Environment.h"
+
 #include "storm/api/transformation.h"
 #include "storm/utility/file.h"
 #include "storm/models/sparse/Model.h"
@@ -79,7 +81,7 @@ namespace storm {
         }
         
         template <typename ParametricType, typename ConstantType>
-        std::shared_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeParameterLiftingRegionModelChecker(std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task) {
+        std::shared_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeParameterLiftingRegionModelChecker(Environment const& env, std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task) {
             
             STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually...");
 
@@ -103,13 +105,13 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type.");
             }
             
-            checker->specify(consideredModel, task);
+            checker->specify(env, consideredModel, task);
             
             return checker;
         }
         
         template <typename ParametricType, typename ImpreciseType, typename PreciseType>
-        std::shared_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeValidatingRegionModelChecker(std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task) {
+        std::shared_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeValidatingRegionModelChecker(Environment const& env, std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task) {
             
             STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually...");
 
@@ -133,30 +135,37 @@ namespace storm {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type.");
             }
             
-            checker->specify(consideredModel, task);
+            checker->specify(env, consideredModel, task);
             
             return checker;
         }
         
         template <typename ValueType>
-        std::shared_ptr<storm::modelchecker::RegionModelChecker<ValueType>> initializeRegionModelChecker(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, storm::modelchecker::RegionCheckEngine engine) {
+        std::shared_ptr<storm::modelchecker::RegionModelChecker<ValueType>> initializeRegionModelChecker(Environment const& env, std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, storm::modelchecker::RegionCheckEngine engine) {
             switch (engine) {
                     case storm::modelchecker::RegionCheckEngine::ParameterLifting:
-                            return initializeParameterLiftingRegionModelChecker<ValueType, double>(model, task);
+                            return initializeParameterLiftingRegionModelChecker<ValueType, double>(env, model, task);
                     case storm::modelchecker::RegionCheckEngine::ExactParameterLifting:
-                            return initializeParameterLiftingRegionModelChecker<ValueType, storm::RationalNumber>(model, task);
+                            return initializeParameterLiftingRegionModelChecker<ValueType, storm::RationalNumber>(env, model, task);
                     case storm::modelchecker::RegionCheckEngine::ValidatingParameterLifting:
-                            return initializeValidatingRegionModelChecker<ValueType, double, storm::RationalNumber>(model, task);
+                            return initializeValidatingRegionModelChecker<ValueType, double, storm::RationalNumber>(env, model, task);
                     default:
                             STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected region model checker type.");
             }
             return nullptr;
         }
         
+        template <typename ValueType>
+        std::shared_ptr<storm::modelchecker::RegionModelChecker<ValueType>> initializeRegionModelChecker(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, storm::modelchecker::RegionCheckEngine engine) {
+            Environment env;
+            initializeRegionModelChecker(env, model, task, engine);
+        }
+        
         template <typename ValueType>
         std::unique_ptr<storm::modelchecker::RegionCheckResult<ValueType>> checkRegionsWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, std::vector<storm::storage::ParameterRegion<ValueType>> const& regions, storm::modelchecker::RegionCheckEngine engine, std::vector<storm::modelchecker::RegionResultHypothesis> const& hypotheses, bool sampleVerticesOfRegions) {
-            auto regionChecker = initializeRegionModelChecker(model, task, engine);
-            return regionChecker->analyzeRegions(regions, hypotheses, sampleVerticesOfRegions);
+            Environment env;
+            auto regionChecker = initializeRegionModelChecker(env, model, task, engine);
+            return regionChecker->analyzeRegions(env, regions, hypotheses, sampleVerticesOfRegions);
         }
     
         template <typename ValueType>
@@ -174,11 +183,11 @@ namespace storm {
          */
         template <typename ValueType>
         std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ValueType>> checkAndRefineRegionWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& task, storm::storage::ParameterRegion<ValueType> const& region, storm::modelchecker::RegionCheckEngine engine, boost::optional<ValueType> const& coverageThreshold, boost::optional<uint64_t> const& refinementDepthThreshold = boost::none, storm::modelchecker::RegionResultHypothesis hypothesis = storm::modelchecker::RegionResultHypothesis::Unknown) {
-            auto regionChecker = initializeRegionModelChecker(model, task, engine);
-            return regionChecker->performRegionRefinement(region, coverageThreshold, refinementDepthThreshold, hypothesis);
+            Environment env;
+            auto regionChecker = initializeRegionModelChecker(env, model, task, engine);
+            return regionChecker->performRegionRefinement(env, region, coverageThreshold, refinementDepthThreshold, hypothesis);
         }
         
-
         template <typename ValueType>
         void exportRegionCheckResultToFile(std::unique_ptr<storm::modelchecker::CheckResult> const& checkResult, std::string const& filename, bool onlyConclusiveResults = false) {
 
diff --git a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp
index 14d433e58..d13f3bf44 100644
--- a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp
+++ b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.cpp
@@ -17,7 +17,7 @@ namespace storm {
         }
 
         template <typename SparseModelType, typename ConstantType>
-        std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
+        std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::check(Environment const& env, storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
             STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before.");
             auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
             STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!");
@@ -25,18 +25,18 @@ namespace storm {
 
             // Check if there are some optimizations implemented for the specified property
             if(this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability())) {
-                return checkReachabilityProbabilityFormula(modelChecker);
+                return checkReachabilityProbabilityFormula(env, modelChecker);
             } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) {
-                return checkReachabilityRewardFormula(modelChecker);
+                return checkReachabilityRewardFormula(env, modelChecker);
             } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setProbabilityOperatorsAllowed(true).setBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) {
-                return checkBoundedUntilFormula(modelChecker);
+                return checkBoundedUntilFormula(env, modelChecker);
             } else {
-                return modelChecker.check(*this->currentCheckTask);
+                return modelChecker.check(env, *this->currentCheckTask);
             }
         }
         
         template <typename SparseModelType, typename ConstantType>
-        std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::checkReachabilityProbabilityFormula(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker) {
+        std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::checkReachabilityProbabilityFormula(Environment const& env, storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker) {
             
             if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
                 this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
@@ -47,11 +47,11 @@ namespace storm {
             // Check the formula and store the result as a hint for the next call.
             // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
             if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
-                result = modelChecker.check(*this->currentCheckTask);
+                result = modelChecker.check(env, *this->currentCheckTask);
                 hint.setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
             } else {
                 auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false);
-                std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeProbabilities(newCheckTask);
+                std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeProbabilities(env, newCheckTask);
                 result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
                 hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
             }
@@ -69,7 +69,7 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ConstantType>
-        std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::checkReachabilityRewardFormula(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker) {
+        std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::checkReachabilityRewardFormula(Environment const& env, storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker) {
             
             if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
                 this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
@@ -80,11 +80,11 @@ namespace storm {
             // Check the formula and store the result as a hint for the next call.
             // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
             if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
-                result = modelChecker.check(*this->currentCheckTask);
+                result = modelChecker.check(env, *this->currentCheckTask);
                 this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>().setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
             } else {
                 auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false);
-                std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeRewards(this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask);
+                std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeRewards(env, this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask);
                 result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
                 this->currentCheckTask->getHint().template asExplicitModelCheckerHint<ConstantType>().setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
             }
@@ -95,7 +95,7 @@ namespace storm {
                 storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint());
                 // We need to exclude the target states from the maybe states.
                 // Note that we can not consider the states with reward zero since a valuation might set a reward to zero
-                std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula());
+                std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(env, this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula());
                 maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
                 hint.setMaybeStates(std::move(maybeStates));
                 hint.setComputeOnlyMaybeStates(true);
@@ -105,7 +105,7 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ConstantType>
-        std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::checkBoundedUntilFormula(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker) {
+        std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::checkBoundedUntilFormula(Environment const& env, storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker) {
             
             if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
                 this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
@@ -117,11 +117,11 @@ namespace storm {
                 // We extract the maybestates from the quantitative result
                 // For qualitative properties, we still need a quantitative result. Hence we perform the check on the subformula
                 if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
-                    result = modelChecker.check(*this->currentCheckTask);
+                    result = modelChecker.check(env, *this->currentCheckTask);
                     hint.setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
                 } else {
                     auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false);
-                    std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeProbabilities(newCheckTask);
+                    std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeProbabilities(env, newCheckTask);
                     result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
                     hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
                 }
@@ -129,12 +129,12 @@ namespace storm {
                 storm::storage::BitVector maybeStates = storm::utility::vector::filterGreaterZero(hint.getResultHint());
                 // We need to exclude the target states from the maybe states.
                 // Note that we can not consider the states with probability one since a state might reach a target state with prob 1 within >0 steps
-                std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula());
+                std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(env, this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula());
                 maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
                 hint.setMaybeStates(std::move(maybeStates));
                 hint.setComputeOnlyMaybeStates(true);
             } else {
-                result = modelChecker.check(*this->currentCheckTask);
+                result = modelChecker.check(env, *this->currentCheckTask);
             }
             
             return result;
diff --git a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.h b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.h
index ad1ffead4..5d4468833 100644
--- a/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.h
+++ b/src/storm-pars/modelchecker/instantiation/SparseDtmcInstantiationModelChecker.h
@@ -20,14 +20,14 @@ namespace storm {
         public:
             SparseDtmcInstantiationModelChecker(SparseModelType const& parametricModel);
             
-            virtual std::unique_ptr<CheckResult> check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) override;
+            virtual std::unique_ptr<CheckResult> check(Environment const& env, storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) override;
 
         protected:
             
             // Optimizations for the different formula types
-            std::unique_ptr<CheckResult> checkReachabilityProbabilityFormula(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker);
-            std::unique_ptr<CheckResult> checkReachabilityRewardFormula(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker);
-            std::unique_ptr<CheckResult> checkBoundedUntilFormula(storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker);
+            std::unique_ptr<CheckResult> checkReachabilityProbabilityFormula(Environment const& env, storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker);
+            std::unique_ptr<CheckResult> checkReachabilityRewardFormula(Environment const& env, storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker);
+            std::unique_ptr<CheckResult> checkBoundedUntilFormula(Environment const& env, storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>>& modelChecker);
             
             storm::utility::ModelInstantiator<SparseModelType, storm::models::sparse::Dtmc<ConstantType>> modelInstantiator;
         };
diff --git a/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h b/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h
index 43ed587ec..6fba381f1 100644
--- a/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h
+++ b/src/storm-pars/modelchecker/instantiation/SparseInstantiationModelChecker.h
@@ -7,6 +7,9 @@
 #include "storm/modelchecker/hints/ModelCheckerHint.h"
 
 namespace storm {
+    
+    class Environment;
+    
     namespace modelchecker {
         
         /*!
@@ -20,7 +23,7 @@ namespace storm {
             
             void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
             
-            virtual std::unique_ptr<CheckResult> check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) = 0;
+            virtual std::unique_ptr<CheckResult> check(Environment const& env, storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) = 0;
             
             // If set, it is assumed that all considered model instantiations have the same underlying graph structure.
             // This bypasses the graph analysis for the different instantiations.
diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
index 887d3b7bf..a2a6c0094 100644
--- a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
+++ b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.cpp
@@ -20,26 +20,26 @@ namespace storm {
         }
 
        template <typename SparseModelType, typename ConstantType>
-        std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
+        std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::check(Environment const& env, storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) {
             STORM_LOG_THROW(this->currentCheckTask, storm::exceptions::InvalidStateException, "Checking has been invoked but no property has been specified before.");
             auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
             STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!");
             storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>> modelChecker(instantiatedModel);
 
             // Check if there are some optimizations implemented for the specified property
-            if(this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability())) {
-                return checkReachabilityProbabilityFormula(modelChecker, instantiatedModel);
+            if (this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability())) {
+                return checkReachabilityProbabilityFormula(env, modelChecker, instantiatedModel);
             } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) {
-                return checkReachabilityRewardFormula(modelChecker, instantiatedModel);
+                return checkReachabilityRewardFormula(env, modelChecker, instantiatedModel);
             } else if (this->currentCheckTask->getFormula().isInFragment(storm::logic::propositional().setProbabilityOperatorsAllowed(true).setBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true).setOperatorAtTopLevelRequired(true).setNestedOperatorsAllowed(false))) {
-                return checkBoundedUntilFormula(modelChecker);
+                return checkBoundedUntilFormula(env, modelChecker);
             } else {
-                return modelChecker.check(*this->currentCheckTask);
+                return modelChecker.check(env, *this->currentCheckTask);
             }
         }
         
         template <typename SparseModelType, typename ConstantType>
-        std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::checkReachabilityProbabilityFormula(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker, storm::models::sparse::Mdp<ConstantType> const& instantiatedModel) {
+        std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::checkReachabilityProbabilityFormula(Environment const& env, storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker, storm::models::sparse::Mdp<ConstantType> const& instantiatedModel) {
             
             this->currentCheckTask->setProduceSchedulers(true);
             
@@ -51,14 +51,14 @@ namespace storm {
             
             // Check the formula and store the result as a hint for the next call.
             // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
-            if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
-                result = modelChecker.check(*this->currentCheckTask);
+            if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
+                result = modelChecker.check(env, *this->currentCheckTask);
                 storm::storage::Scheduler<ConstantType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
                 hint.setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
                 hint.setSchedulerHint(dynamic_cast<storm::storage::Scheduler<ConstantType> const&>(scheduler));
             } else {
                 auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false);
-                std::unique_ptr<storm::modelchecker::CheckResult> quantitativeResult = modelChecker.computeProbabilities(newCheckTask);
+                std::unique_ptr<storm::modelchecker::CheckResult> quantitativeResult = modelChecker.computeProbabilities(env, newCheckTask);
                 result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
                 storm::storage::Scheduler<ConstantType>& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
                 hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
@@ -84,7 +84,7 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ConstantType>
-        std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::checkReachabilityRewardFormula(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker, storm::models::sparse::Mdp<ConstantType> const& instantiatedModel) {
+        std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::checkReachabilityRewardFormula(Environment const& env, storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker, storm::models::sparse::Mdp<ConstantType> const& instantiatedModel) {
             
             this->currentCheckTask->setProduceSchedulers(true);
             
@@ -97,13 +97,13 @@ namespace storm {
             // Check the formula and store the result as a hint for the next call.
             // For qualitative properties, we still want a quantitative result hint. Hence we perform the check on the subformula
             if(this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
-                std::unique_ptr<storm::modelchecker::CheckResult> result = modelChecker.check(*this->currentCheckTask);
+                std::unique_ptr<storm::modelchecker::CheckResult> result = modelChecker.check(env, *this->currentCheckTask);
                 storm::storage::Scheduler<ConstantType> const& scheduler = result->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
                 hint.setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
                 hint.setSchedulerHint(dynamic_cast<storm::storage::Scheduler<ConstantType> const&>(scheduler));
             } else {
                 auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false);
-                std::unique_ptr<storm::modelchecker::CheckResult> quantitativeResult = modelChecker.computeRewards(this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask);
+                std::unique_ptr<storm::modelchecker::CheckResult> quantitativeResult = modelChecker.computeRewards(env, this->currentCheckTask->getFormula().asRewardOperatorFormula().getMeasureType(), newCheckTask);
                 result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
                 storm::storage::Scheduler<ConstantType>& scheduler = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getScheduler();
                 hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
@@ -116,7 +116,7 @@ namespace storm {
                 storm::storage::BitVector maybeStates = ~storm::utility::vector::filterInfinity(hint.getResultHint());
                 // We need to exclude the target states from the maybe states.
                 // Note that we can not consider the states with reward zero since a valuation might set a reward to zero
-                std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula());
+                std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(env, this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asEventuallyFormula().getSubformula());
                 maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
                 hint.setMaybeStates(std::move(maybeStates));
                 hint.setComputeOnlyMaybeStates(true);
@@ -131,7 +131,7 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ConstantType>
-        std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::checkBoundedUntilFormula(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker) {
+        std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::checkBoundedUntilFormula(Environment const& env, storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker) {
             
             if (!this->currentCheckTask->getHint().isExplicitModelCheckerHint()) {
                 this->currentCheckTask->setHint(std::make_shared<ExplicitModelCheckerHint<ConstantType>>());
@@ -143,23 +143,23 @@ namespace storm {
                 // We extract the maybestates from the quantitative result
                 // For qualitative properties, we still need a quantitative result. Hence we perform the check on the subformula
                 if (this->currentCheckTask->getFormula().asOperatorFormula().hasQuantitativeResult()) {
-                    result = modelChecker.check(*this->currentCheckTask);
+                    result = modelChecker.check(env, *this->currentCheckTask);
                     hint.setResultHint(result->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector());
                 } else {
                     auto newCheckTask = this->currentCheckTask->substituteFormula(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula()).setOnlyInitialStatesRelevant(false);
-                    std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeProbabilities(newCheckTask);
+                    std::unique_ptr<CheckResult> quantitativeResult = modelChecker.computeProbabilities(env, newCheckTask);
                     result = quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
                     hint.setResultHint(std::move(quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().getValueVector()));
                 }
                 storm::storage::BitVector maybeStates = storm::utility::vector::filterGreaterZero(hint.getResultHint());
                 // We need to exclude the target states from the maybe states.
                 // Note that we can not consider the states with probability one since a state might reach a target state with prob 1 within >0 steps
-                std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula());
+                std::unique_ptr<CheckResult> subFormulaResult = modelChecker.check(env, this->currentCheckTask->getFormula().asOperatorFormula().getSubformula().asBoundedUntilFormula().getRightSubformula());
                 maybeStates = maybeStates & ~(subFormulaResult->asExplicitQualitativeCheckResult().getTruthValuesVector());
                 hint.setMaybeStates(std::move(maybeStates));
                 hint.setComputeOnlyMaybeStates(true);
             } else {
-                result = modelChecker.check(*this->currentCheckTask);
+                result = modelChecker.check(env, *this->currentCheckTask);
             }
             return result;
         }
diff --git a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h
index d8d5d46e8..ff6a6735e 100644
--- a/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h
+++ b/src/storm-pars/modelchecker/instantiation/SparseMdpInstantiationModelChecker.h
@@ -20,13 +20,13 @@ namespace storm {
         public:
             SparseMdpInstantiationModelChecker(SparseModelType const& parametricModel);
             
-            virtual std::unique_ptr<CheckResult> check(storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) override;
+            virtual std::unique_ptr<CheckResult> check(Environment const& env, storm::utility::parametric::Valuation<typename SparseModelType::ValueType> const& valuation) override;
 
         protected:
             // Optimizations for the different formula types
-            std::unique_ptr<CheckResult> checkReachabilityProbabilityFormula(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker, storm::models::sparse::Mdp<ConstantType> const& instantiatedModel);
-            std::unique_ptr<CheckResult> checkReachabilityRewardFormula(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker, storm::models::sparse::Mdp<ConstantType> const& instantiatedModel);
-            std::unique_ptr<CheckResult> checkBoundedUntilFormula(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker);
+            std::unique_ptr<CheckResult> checkReachabilityProbabilityFormula(Environment const& env, storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker, storm::models::sparse::Mdp<ConstantType> const& instantiatedModel);
+            std::unique_ptr<CheckResult> checkReachabilityRewardFormula(Environment const& env, storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker, storm::models::sparse::Mdp<ConstantType> const& instantiatedModel);
+            std::unique_ptr<CheckResult> checkBoundedUntilFormula(Environment const& env, storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelChecker);
             
             storm::utility::ModelInstantiator<SparseModelType, storm::models::sparse::Mdp<ConstantType>> modelInstantiator;
         };
diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp
index ab0142d0b..b3669e9b8 100644
--- a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp
@@ -29,14 +29,14 @@ namespace storm {
             }
         
             template <typename ParametricType>
-            std::unique_ptr<storm::modelchecker::RegionCheckResult<ParametricType>> RegionModelChecker<ParametricType>::analyzeRegions(std::vector<storm::storage::ParameterRegion<ParametricType>> const& regions, std::vector<RegionResultHypothesis> const& hypotheses, bool sampleVerticesOfRegion) {
+            std::unique_ptr<storm::modelchecker::RegionCheckResult<ParametricType>> RegionModelChecker<ParametricType>::analyzeRegions(Environment const& env, std::vector<storm::storage::ParameterRegion<ParametricType>> const& regions, std::vector<RegionResultHypothesis> const& hypotheses, bool sampleVerticesOfRegion) {
                 
                 STORM_LOG_THROW(regions.size() == hypotheses.size(), storm::exceptions::InvalidArgumentException, "The number of regions and the number of hypotheses do not match");
                 std::vector<std::pair<storm::storage::ParameterRegion<ParametricType>, storm::modelchecker::RegionResult>> result;
                 
                 auto hypothesisIt = hypotheses.begin();
                 for (auto const& region : regions) {
-                    storm::modelchecker::RegionResult regionRes = analyzeRegion(region, *hypothesisIt, storm::modelchecker::RegionResult::Unknown, sampleVerticesOfRegion);
+                    storm::modelchecker::RegionResult regionRes = analyzeRegion(env, region, *hypothesisIt, storm::modelchecker::RegionResult::Unknown, sampleVerticesOfRegion);
                     result.emplace_back(region, regionRes);
                     ++hypothesisIt;
                 }
@@ -45,13 +45,13 @@ namespace storm {
             }
 
             template <typename ParametricType>
-            ParametricType RegionModelChecker<ParametricType>::getBoundAtInitState(storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+            ParametricType RegionModelChecker<ParametricType>::getBoundAtInitState(Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
                 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The selected region model checker does not support this functionality.");
                 return storm::utility::zero<ParametricType>();
             }
         
             template <typename ParametricType>
-            std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>> RegionModelChecker<ParametricType>::performRegionRefinement(storm::storage::ParameterRegion<ParametricType> const& region, boost::optional<ParametricType> const& coverageThreshold, boost::optional<uint64_t> depthThreshold, RegionResultHypothesis const& hypothesis) {
+            std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>> RegionModelChecker<ParametricType>::performRegionRefinement(Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region, boost::optional<ParametricType> const& coverageThreshold, boost::optional<uint64_t> depthThreshold, RegionResultHypothesis const& hypothesis) {
                 STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " .");
                 
                 auto thresholdAsCoefficient = coverageThreshold ? storm::utility::convertNumber<CoefficientType>(coverageThreshold.get()) : storm::utility::zero<CoefficientType>();
@@ -91,7 +91,7 @@ namespace storm {
                     STORM_LOG_INFO("Analyzing region #" << numOfAnalyzedRegions << " (Refinement depth " << currentDepth << "; " << storm::utility::convertNumber<double>(fractionOfUndiscoveredArea) * 100 << "% still unknown)");
                     auto& currentRegion = unprocessedRegions.front().first;
                     auto& res = unprocessedRegions.front().second;
-                    res = analyzeRegion(currentRegion, hypothesis, res, false);
+                    res = analyzeRegion(env, currentRegion, hypothesis, res, false);
                     switch (res) {
                         case RegionResult::AllSat:
                             fractionOfUndiscoveredArea -= currentRegion.area() / areaOfParameterSpace;
diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.h b/src/storm-pars/modelchecker/region/RegionModelChecker.h
index 595d1e8f0..fc9997c3c 100644
--- a/src/storm-pars/modelchecker/region/RegionModelChecker.h
+++ b/src/storm-pars/modelchecker/region/RegionModelChecker.h
@@ -12,6 +12,9 @@
 #include "storm/modelchecker/CheckTask.h"
 
 namespace storm {
+    
+    class Environment;
+    
     namespace modelchecker{
         
         template<typename ParametricType>
@@ -24,7 +27,7 @@ namespace storm {
             virtual ~RegionModelChecker() = default;
             
             virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, ParametricType> const& checkTask) const = 0;
-            virtual void specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, ParametricType> const& checkTask) = 0;
+            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, ParametricType> const& checkTask) = 0;
             
             /*!
              * Analyzes the given region.
@@ -32,7 +35,7 @@ namespace storm {
              * @param initialResult encodes what is already known about this region
              * @param sampleVerticesOfRegion enables sampling of the vertices of the region in cases where AllSat/AllViolated could not be shown.
              */
-            virtual RegionResult analyzeRegion(storm::storage::ParameterRegion<ParametricType> const& region, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) = 0;
+            virtual RegionResult analyzeRegion(Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) = 0;
             
              /*!
              * Analyzes the given regions.
@@ -40,9 +43,9 @@ namespace storm {
 
              * If supported by this model checker, it is possible to sample the vertices of the regions whenever AllSat/AllViolated could not be shown.
              */
-            std::unique_ptr<storm::modelchecker::RegionCheckResult<ParametricType>> analyzeRegions(std::vector<storm::storage::ParameterRegion<ParametricType>> const& regions, std::vector<RegionResultHypothesis> const& hypotheses, bool sampleVerticesOfRegion = false) ;
+            std::unique_ptr<storm::modelchecker::RegionCheckResult<ParametricType>> analyzeRegions(Environment const& env, std::vector<storm::storage::ParameterRegion<ParametricType>> const& regions, std::vector<RegionResultHypothesis> const& hypotheses, bool sampleVerticesOfRegion = false) ;
             
-            virtual ParametricType getBoundAtInitState(storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
+            virtual ParametricType getBoundAtInitState(Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
             
             /*!
              * Iteratively refines the region until the region analysis yields a conclusive result (AllSat or AllViolated).
@@ -52,7 +55,7 @@ namespace storm {
              * @param hypothesis if not 'unknown', it is only checked whether the hypothesis holds within the given region.
              *
              */
-            std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>> performRegionRefinement(storm::storage::ParameterRegion<ParametricType> const& region, boost::optional<ParametricType> const& coverageThreshold, boost::optional<uint64_t> depthThreshold = boost::none, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown);
+            std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>> performRegionRefinement(Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region, boost::optional<ParametricType> const& coverageThreshold, boost::optional<uint64_t> depthThreshold = boost::none, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown);
             
         };
 
diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
index 502d1485c..e76b2b3af 100644
--- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
@@ -47,13 +47,13 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ConstantType>
-        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
             auto dtmc = parametricModel->template as<SparseModelType>();
-            specify(dtmc, checkTask, false);
+            specify(env, dtmc, checkTask, false);
         }
         
         template <typename SparseModelType, typename ConstantType>
-        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification) {
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification) {
 
             STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
          
@@ -61,20 +61,20 @@ namespace storm {
             
             if (skipModelSimplification) {
                 this->parametricModel = parametricModel;
-                this->specifyFormula(checkTask);
+                this->specifyFormula(env, checkTask);
             } else {
                 auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<SparseModelType>(*parametricModel);
                 if (!simplifier.simplify(checkTask.getFormula())) {
                     STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull.");
                 }
                 this->parametricModel = simplifier.getSimplifiedModel();
-                this->specifyFormula(checkTask.substituteFormula(*simplifier.getSimplifiedFormula()));
+                this->specifyFormula(env, checkTask.substituteFormula(*simplifier.getSimplifiedFormula()));
             }
         }
         
         
         template <typename SparseModelType, typename ConstantType>
-        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) {
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) {
             
             // get the step bound
             STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported.");
@@ -118,7 +118,7 @@ namespace storm {
         }
 
         template <typename SparseModelType, typename ConstantType>
-        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) {
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(Environment const& env, CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) {
             
             // get the results for the subformulas
             storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(*this->parametricModel);
@@ -147,14 +147,14 @@ namespace storm {
             upperResultBound = storm::utility::one<ConstantType>();
             
             // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations).
-            auto req = solverFactory->getRequirements(true);
+            auto req = solverFactory->getRequirements(env, true);
             req.clearBounds();
             STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "Unchecked solver requirement.");
             solverFactory->setRequirementsChecked(true);
         }
 
         template <typename SparseModelType, typename ConstantType>
-        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) {
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(Environment const& env, CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) {
             
             // get the results for the subformula
             storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(*this->parametricModel);
@@ -186,7 +186,7 @@ namespace storm {
             lowerResultBound = storm::utility::zero<ConstantType>();
         
             // The solution of the min-max equation system will always be unique (assuming graph-preserving instantiations).
-            auto req = solverFactory->getRequirements(true);
+            auto req = solverFactory->getRequirements(env, true);
             req.clearLowerBounds();
             if (req.requiresUpperBounds()) {
                 solvingRequiresUpperRewardBounds = true;
@@ -199,7 +199,7 @@ namespace storm {
         }
 
         template <typename SparseModelType, typename ConstantType>
-        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) {
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyCumulativeRewardFormula(Environment const& env, CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) {
             
             // Obtain the stepBound
             stepBound = checkTask.getFormula().getBound().evaluateAsInt();
@@ -239,20 +239,15 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ConstantType>
-        std::unique_ptr<CheckResult> SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+        std::unique_ptr<CheckResult> SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::computeQuantitativeValues(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
             
-            if(maybeStates.empty()) {
+            if (maybeStates.empty()) {
                 return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(resultsForNonMaybeStates);
             }
             
             parameterLifter->specifyRegion(region, dirForParameters);
             
-            // Set up the solver
-            if (storm::NumberTraits<ConstantType>::IsExact && solverFactory->getMinMaxMethod() == storm::solver::MinMaxMethod::ValueIteration) {
-                STORM_LOG_INFO("Parameter Lifting: Setting solution method for exact MinMaxSolver to policy iteration");
-                solverFactory->setMinMaxMethod(storm::solver::MinMaxMethod::PolicyIteration);
-            }
-            auto solver = solverFactory->create(parameterLifter->getMatrix());
+            auto solver = solverFactory->create(env, parameterLifter->getMatrix());
             solver->setHasUniqueSolution();
             if (lowerResultBound) solver->setLowerBound(lowerResultBound.get());
             if (upperResultBound) {
@@ -296,7 +291,7 @@ namespace storm {
                 solver->repeatedMultiply(dirForParameters, x, &parameterLifter->getVector(), *stepBound);
             } else {
                 x.resize(maybeStates.getNumberOfSetBits(), storm::utility::zero<ConstantType>());
-                solver->solveEquations(dirForParameters, x, parameterLifter->getVector());
+                solver->solveEquations(env, dirForParameters, x, parameterLifter->getVector());
                 if(storm::solver::minimize(dirForParameters)) {
                     minSchedChoices = solver->getSchedulerChoices();
                 } else {
@@ -314,7 +309,6 @@ namespace storm {
             return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(std::move(result));
         }
         
-        
         template <typename SparseModelType, typename ConstantType>
         void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::reset() {
             maybeStates.resize(0);
diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
index b4a8644b6..18bb302b9 100644
--- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
@@ -23,22 +23,22 @@ namespace storm {
             virtual ~SparseDtmcParameterLiftingModelChecker() = default;
             
             virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
-            virtual void specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
-            void specify(std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification);
+            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
+            void specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification);
             
             boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMinScheduler();
             boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMaxScheduler();
 
         protected:
                 
-            virtual void specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) override;
-            virtual void specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) override;
-            virtual void specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) override;
-            virtual void specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) override;
+            virtual void specifyBoundedUntilFormula(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) override;
+            virtual void specifyUntilFormula(Environment const& env, CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) override;
+            virtual void specifyReachabilityRewardFormula(Environment const& env, CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) override;
+            virtual void specifyCumulativeRewardFormula(Environment const& env, CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) override;
 
             virtual storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& getInstantiationChecker() override;
                 
-            virtual std::unique_ptr<CheckResult> computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) override;
+            virtual std::unique_ptr<CheckResult> computeQuantitativeValues(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) override;
                 
             virtual void reset() override;
                 
diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
index 19ac39b62..c21ef3d5b 100644
--- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
@@ -45,13 +45,13 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ConstantType>
-        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
             auto mdp = parametricModel->template as<SparseModelType>();
-            specify(mdp, checkTask, false);
+            specify(env, mdp, checkTask, false);
         }
         
         template <typename SparseModelType, typename ConstantType>
-        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification) {
+        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification) {
 
             STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
          
@@ -59,19 +59,19 @@ namespace storm {
             
             if (skipModelSimplification) {
                 this->parametricModel = parametricModel;
-                this->specifyFormula(checkTask);
+                this->specifyFormula(env, checkTask);
             } else {
                 auto simplifier = storm::transformer::SparseParametricMdpSimplifier<SparseModelType>(*parametricModel);
                 if (!simplifier.simplify(checkTask.getFormula())) {
                     STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull.");
                 }
                 this->parametricModel = simplifier.getSimplifiedModel();
-                this->specifyFormula(checkTask.substituteFormula(*simplifier.getSimplifiedFormula()));
+                this->specifyFormula(env, checkTask.substituteFormula(*simplifier.getSimplifiedFormula()));
             }
         }
         
         template <typename SparseModelType, typename ConstantType>
-        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) {
+        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) {
             
             // get the step bound
             STORM_LOG_THROW(!checkTask.getFormula().hasLowerBound(), storm::exceptions::NotSupportedException, "Lower step bounds are not supported.");
@@ -118,7 +118,7 @@ namespace storm {
         }
 
         template <typename SparseModelType, typename ConstantType>
-        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) {
+        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(Environment const& env, CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) {
             
             // get the results for the subformulas
             storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(*this->parametricModel);
@@ -155,7 +155,7 @@ namespace storm {
         }
 
         template <typename SparseModelType, typename ConstantType>
-        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) {
+        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(Environment const& env, CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) {
             
             // get the results for the subformula
             storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(*this->parametricModel);
@@ -200,7 +200,7 @@ namespace storm {
         }
 
         template <typename SparseModelType, typename ConstantType>
-        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) {
+        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyCumulativeRewardFormula(Environment const& env, CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) {
             
             // Obtain the stepBound
             stepBound = checkTask.getFormula().getBound().evaluateAsInt();
@@ -239,7 +239,7 @@ namespace storm {
         }
 
         template <typename SparseModelType, typename ConstantType>
-        std::unique_ptr<CheckResult> SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+        std::unique_ptr<CheckResult> SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::computeQuantitativeValues(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
             
             if (maybeStates.empty()) {
                 return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(resultsForNonMaybeStates);
diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h
index 346bb01f7..09a3e44cb 100644
--- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h
@@ -25,8 +25,8 @@ namespace storm {
             virtual ~SparseMdpParameterLiftingModelChecker() = default;
             
             virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
-            virtual void specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
-            void specify(std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification);
+            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
+            void specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification);
 
             boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMinScheduler();
             boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMaxScheduler();
@@ -34,14 +34,14 @@ namespace storm {
                 
         protected:
                 
-            virtual void specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) override;
-            virtual void specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) override;
-            virtual void specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) override;
-            virtual void specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) override;
+            virtual void specifyBoundedUntilFormula(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) override;
+            virtual void specifyUntilFormula(Environment const& env, CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) override;
+            virtual void specifyReachabilityRewardFormula(Environment const& env, CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) override;
+            virtual void specifyCumulativeRewardFormula(Environment const& env, CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask) override;
                 
             virtual storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& getInstantiationChecker() override;
 
-            virtual std::unique_ptr<CheckResult> computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) override;
+            virtual std::unique_ptr<CheckResult> computeQuantitativeValues(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) override;
                 
             virtual void reset() override;
                 
diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp
index 1accd68cc..bc927c8bd 100644
--- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp
@@ -21,7 +21,7 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ConstantType>
-        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyFormula(Environment const& env, storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
 
             currentFormula = checkTask.getFormula().asSharedPointer();
             currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, ConstantType>>(checkTask.substituteFormula(*currentFormula).template convertValueType<ConstantType>());
@@ -29,26 +29,26 @@ namespace storm {
             if(currentCheckTask->getFormula().isProbabilityOperatorFormula()) {
                 auto const& probOpFormula = currentCheckTask->getFormula().asProbabilityOperatorFormula();
                 if(probOpFormula.getSubformula().isBoundedUntilFormula()) {
-                    specifyBoundedUntilFormula(currentCheckTask->substituteFormula(probOpFormula.getSubformula().asBoundedUntilFormula()));
+                    specifyBoundedUntilFormula(env, currentCheckTask->substituteFormula(probOpFormula.getSubformula().asBoundedUntilFormula()));
                 } else if(probOpFormula.getSubformula().isUntilFormula()) {
-                    specifyUntilFormula(currentCheckTask->substituteFormula(probOpFormula.getSubformula().asUntilFormula()));
+                    specifyUntilFormula(env, currentCheckTask->substituteFormula(probOpFormula.getSubformula().asUntilFormula()));
                 } else if (probOpFormula.getSubformula().isEventuallyFormula()) {
-                    specifyReachabilityProbabilityFormula(currentCheckTask->substituteFormula(probOpFormula.getSubformula().asEventuallyFormula()));
+                    specifyReachabilityProbabilityFormula(env, currentCheckTask->substituteFormula(probOpFormula.getSubformula().asEventuallyFormula()));
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
                 }
             } else if (currentCheckTask->getFormula().isRewardOperatorFormula()) {
                 auto const& rewOpFormula = currentCheckTask->getFormula().asRewardOperatorFormula();
                 if(rewOpFormula.getSubformula().isEventuallyFormula()) {
-                    specifyReachabilityRewardFormula(currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asEventuallyFormula()));
+                    specifyReachabilityRewardFormula(env, currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asEventuallyFormula()));
                 } else if (rewOpFormula.getSubformula().isCumulativeRewardFormula()) {
-                    specifyCumulativeRewardFormula(currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asCumulativeRewardFormula()));
+                    specifyCumulativeRewardFormula(env, currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asCumulativeRewardFormula()));
                 }
             }
         }
         
         template <typename SparseModelType, typename ConstantType>
-        RegionResult SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResultHypothesis const& hypothesis, RegionResult const& initialResult, bool sampleVerticesOfRegion) {
+        RegionResult SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::analyzeRegion(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResultHypothesis const& hypothesis, RegionResult const& initialResult, bool sampleVerticesOfRegion) {
 
             STORM_LOG_THROW(this->currentCheckTask->isOnlyInitialStatesRelevantSet(), storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a property where only the value in the initial states is relevant.");
             STORM_LOG_THROW(this->currentCheckTask->isBoundSet(), storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a bounded property.");
@@ -58,25 +58,25 @@ namespace storm {
 
             // Check if we need to check the formula on one point to decide whether to show AllSat or AllViolated
             if (hypothesis == RegionResultHypothesis::Unknown && result == RegionResult::Unknown) {
-                 result = getInstantiationChecker().check(region.getCenterPoint())->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()] ? RegionResult::CenterSat : RegionResult::CenterViolated;
+                 result = getInstantiationChecker().check(env, region.getCenterPoint())->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()] ? RegionResult::CenterSat : RegionResult::CenterViolated;
             }
             
             // try to prove AllSat or AllViolated, depending on the hypothesis or the current result
             if (hypothesis == RegionResultHypothesis::AllSat || result == RegionResult::ExistsSat || result == RegionResult::CenterSat) {
                 // show AllSat:
                 storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize;
-                if (this->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
+                if (this->check(env, region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
                     result = RegionResult::AllSat;
                 } else if (sampleVerticesOfRegion) {
-                    result = sampleVertices(region, result);
+                    result = sampleVertices(env, region, result);
                 }
             } else if (hypothesis == RegionResultHypothesis::AllViolated || result == RegionResult::ExistsViolated || result == RegionResult::CenterViolated) {
                 // show AllViolated:
                 storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType) ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize;
-                if (!this->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
+                if (!this->check(env, region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
                     result = RegionResult::AllViolated;
                 } else if (sampleVerticesOfRegion) {
-                    result = sampleVertices(region, result);
+                    result = sampleVertices(env, region, result);
                 }
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "When analyzing a region, an invalid initial result was given: " << initialResult);
@@ -85,7 +85,7 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ConstantType>
-        RegionResult SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::sampleVertices(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult) {
+        RegionResult SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::sampleVertices(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult) {
             RegionResult result = initialResult;
             
             if (result == RegionResult::AllSat || result == RegionResult::AllViolated) {
@@ -99,7 +99,7 @@ namespace storm {
             auto vertices = region.getVerticesOfRegion(region.getVariables());
             auto vertexIt = vertices.begin();
             while (vertexIt != vertices.end() && !(hasSatPoint && hasViolatedPoint)) {
-                if (getInstantiationChecker().check(*vertexIt)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
+                if (getInstantiationChecker().check(env, *vertexIt)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
                     hasSatPoint = true;
                 } else {
                     hasViolatedPoint = true;
@@ -122,8 +122,8 @@ namespace storm {
 
 
         template <typename SparseModelType, typename ConstantType>
-        std::unique_ptr<CheckResult> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::check(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
-            auto quantitativeResult = computeQuantitativeValues(region, dirForParameters);
+        std::unique_ptr<CheckResult> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::check(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+            auto quantitativeResult = computeQuantitativeValues(env, region, dirForParameters);
             if(currentCheckTask->getFormula().hasQuantitativeResult()) {
                 return quantitativeResult;
             } else {
@@ -132,15 +132,15 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ConstantType>
-        std::unique_ptr<QuantitativeCheckResult<ConstantType>> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getBound(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+        std::unique_ptr<QuantitativeCheckResult<ConstantType>> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getBound(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
             STORM_LOG_WARN_COND(this->currentCheckTask->getFormula().hasQuantitativeResult(), "Computing quantitative bounds for a qualitative formula...");
-            return std::make_unique<ExplicitQuantitativeCheckResult<ConstantType>>(std::move(computeQuantitativeValues(region, dirForParameters)->template asExplicitQuantitativeCheckResult<ConstantType>()));
+            return std::make_unique<ExplicitQuantitativeCheckResult<ConstantType>>(std::move(computeQuantitativeValues(env, region, dirForParameters)->template asExplicitQuantitativeCheckResult<ConstantType>()));
         }
 
         template <typename SparseModelType, typename ConstantType>
-        typename SparseModelType::ValueType SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getBoundAtInitState(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+        typename SparseModelType::ValueType SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getBoundAtInitState(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
             STORM_LOG_THROW(this->parametricModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Getting a bound at the initial state requires a model with a single initial state.");
-            return storm::utility::convertNumber<typename SparseModelType::ValueType>(getBound(region, dirForParameters)->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()]);
+            return storm::utility::convertNumber<typename SparseModelType::ValueType>(getBound(env, region, dirForParameters)->template asExplicitQuantitativeCheckResult<ConstantType>()[*this->parametricModel->getInitialStates().begin()]);
         }
         
         template <typename SparseModelType, typename ConstantType>
@@ -154,29 +154,29 @@ namespace storm {
         }
 
         template <typename SparseModelType, typename ConstantType>
-        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(CheckTask<logic::BoundedUntilFormula, ConstantType> const& checkTask) {
+        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(Environment const& env, CheckTask<logic::BoundedUntilFormula, ConstantType> const& checkTask) {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
         }
 
         template <typename SparseModelType, typename ConstantType>
-        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(CheckTask<logic::UntilFormula, ConstantType> const& checkTask) {
+        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(Environment const& env, CheckTask<logic::UntilFormula, ConstantType> const& checkTask) {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
         }
 
         template <typename SparseModelType, typename ConstantType>
-        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityProbabilityFormula(CheckTask<logic::EventuallyFormula, ConstantType> const& checkTask) {
+        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityProbabilityFormula(Environment const& env, CheckTask<logic::EventuallyFormula, ConstantType> const& checkTask) {
             // transform to until formula
             auto untilFormula = std::make_shared<storm::logic::UntilFormula const>(storm::logic::Formula::getTrueFormula(), checkTask.getFormula().getSubformula().asSharedPointer());
-            specifyUntilFormula(currentCheckTask->substituteFormula(*untilFormula));
+            specifyUntilFormula(env, currentCheckTask->substituteFormula(*untilFormula));
         }
 
         template <typename SparseModelType, typename ConstantType>
-        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(CheckTask<logic::EventuallyFormula, ConstantType> const& checkTask) {
+        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(Environment const& env, CheckTask<logic::EventuallyFormula, ConstantType> const& checkTask) {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
         }
 
         template <typename SparseModelType, typename ConstantType>
-        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyCumulativeRewardFormula(CheckTask<logic::CumulativeRewardFormula, ConstantType> const& checkTask) {
+        void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyCumulativeRewardFormula(Environment const& env, CheckTask<logic::CumulativeRewardFormula, ConstantType> const& checkTask) {
             STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameter lifting is not supported for the given property.");
         }
 
diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h
index cb993ad4f..8caa2b6c5 100644
--- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h
@@ -29,12 +29,12 @@ namespace storm {
             /*!
              * Analyzes the given region by means of parameter lifting.
              */
-            virtual RegionResult analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override;
+            virtual RegionResult analyzeRegion(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override;
 
             /*!
              * Analyzes the 2^#parameters corner points of the given region.
              */
-            RegionResult sampleVertices(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult = RegionResult::Unknown);
+            RegionResult sampleVertices(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult = RegionResult::Unknown);
             
             /*!
              * Checks the specified formula on the given region by applying parameter lifting (Parameter choices are lifted to nondeterministic choices)
@@ -43,31 +43,31 @@ namespace storm {
              * @param region the region on which parameter lifting is applied
              * @param dirForParameters  The optimization direction for the parameter choices. If this is, e.g., minimize, then the returned result will be a lower bound for all results induced by the parameter evaluations inside the region.
              */
-            std::unique_ptr<CheckResult> check(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
+            std::unique_ptr<CheckResult> check(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
             
-            std::unique_ptr<QuantitativeCheckResult<ConstantType>> getBound(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
-            virtual typename SparseModelType::ValueType getBoundAtInitState(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) override;
+            std::unique_ptr<QuantitativeCheckResult<ConstantType>> getBound(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
+            virtual typename SparseModelType::ValueType getBoundAtInitState(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) override;
 
             
             SparseModelType const& getConsideredParametricModel() const;
             CheckTask<storm::logic::Formula, ConstantType> const& getCurrentCheckTask() const;
             
         protected:
-            void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
+            void specifyFormula(Environment const& env, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
             
             // Resets all data that correspond to the currently defined property.
             virtual void reset() = 0;
 
-            virtual void specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask);
-            virtual void specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask);
-            virtual void specifyReachabilityProbabilityFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask);
-            virtual void specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask);
-            virtual void specifyCumulativeRewardFormula(CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask);
+            virtual void specifyBoundedUntilFormula(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask);
+            virtual void specifyUntilFormula(Environment const& env, CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask);
+            virtual void specifyReachabilityProbabilityFormula(Environment const& env, CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask);
+            virtual void specifyReachabilityRewardFormula(Environment const& env, CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask);
+            virtual void specifyCumulativeRewardFormula(Environment const& env, CheckTask<storm::logic::CumulativeRewardFormula, ConstantType> const& checkTask);
 
             
             virtual storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& getInstantiationChecker() = 0;
             
-            virtual std::unique_ptr<CheckResult> computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) = 0;
+            virtual std::unique_ptr<CheckResult> computeQuantitativeValues(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) = 0;
             
             
             std::shared_ptr<SparseModelType> parametricModel;
diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp
index 2ab8c3103..e95cf2d61 100644
--- a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp
@@ -15,7 +15,7 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
-        void ValidatingSparseDtmcParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+        void ValidatingSparseDtmcParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
             STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
         
             auto dtmc = parametricModel->template as<SparseModelType>();
@@ -27,8 +27,8 @@ namespace storm {
             
             auto simplifiedTask = checkTask.substituteFormula(*simplifier.getSimplifiedFormula());
             
-            impreciseChecker.specify(simplifier.getSimplifiedModel(), simplifiedTask, true);
-            preciseChecker.specify(simplifier.getSimplifiedModel(), simplifiedTask, true);
+            impreciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, true);
+            preciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, true);
         }
         
         template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h
index 9fd696be2..f441353fb 100644
--- a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h
@@ -12,7 +12,7 @@ namespace storm {
             ValidatingSparseDtmcParameterLiftingModelChecker();
             virtual ~ValidatingSparseDtmcParameterLiftingModelChecker() = default;
             
-            virtual void specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
+            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
 
         protected:
             virtual SparseParameterLiftingModelChecker<SparseModelType, ImpreciseType>& getImpreciseChecker() override;
diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp
index 014cf6267..7cdb1c7b0 100644
--- a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp
@@ -16,7 +16,7 @@ namespace storm {
         
         
         template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
-        void ValidatingSparseMdpParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+        void ValidatingSparseMdpParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
             STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
         
             auto mdp = parametricModel->template as<SparseModelType>();
@@ -28,8 +28,8 @@ namespace storm {
             
             auto simplifiedTask = checkTask.substituteFormula(*simplifier.getSimplifiedFormula());
             
-            impreciseChecker.specify(simplifier.getSimplifiedModel(), simplifiedTask, true);
-            preciseChecker.specify(simplifier.getSimplifiedModel(), simplifiedTask, true);
+            impreciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, true);
+            preciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, true);
         }
         
         template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h
index 1f56818c6..fdb304747 100644
--- a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h
@@ -12,7 +12,7 @@ namespace storm {
             ValidatingSparseMdpParameterLiftingModelChecker();
             virtual ~ValidatingSparseMdpParameterLiftingModelChecker() = default;
             
-            virtual void specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
+            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
 
         protected:
             virtual SparseParameterLiftingModelChecker<SparseModelType, ImpreciseType>& getImpreciseChecker() override;
diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp
index 8f3ffaad3..002a43692 100644
--- a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.cpp
@@ -28,10 +28,10 @@ namespace storm {
         };
  
         template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
-        RegionResult ValidatingSparseParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResultHypothesis const& hypothesis, RegionResult const& initialResult, bool sampleVerticesOfRegion) {
+        RegionResult ValidatingSparseParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::analyzeRegion(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResultHypothesis const& hypothesis, RegionResult const& initialResult, bool sampleVerticesOfRegion) {
 
         
-            RegionResult currentResult = getImpreciseChecker().analyzeRegion(region, hypothesis, initialResult, false);
+            RegionResult currentResult = getImpreciseChecker().analyzeRegion(env, region, hypothesis, initialResult, false);
             
             if (currentResult == RegionResult::AllSat || currentResult == RegionResult::AllViolated) {
                 applyHintsToPreciseChecker();
@@ -41,7 +41,7 @@ namespace storm {
                     parameterOptDir = storm::solver::invert(parameterOptDir);
                 }
                 
-                bool preciseResult = getPreciseChecker().check(region, parameterOptDir)->asExplicitQualitativeCheckResult()[*getPreciseChecker().getConsideredParametricModel().getInitialStates().begin()];
+                bool preciseResult = getPreciseChecker().check(env, region, parameterOptDir)->asExplicitQualitativeCheckResult()[*getPreciseChecker().getConsideredParametricModel().getInitialStates().begin()];
                 bool preciseResultAgrees = preciseResult == (currentResult == RegionResult::AllSat);
                 
                 if (!preciseResultAgrees) {
@@ -52,7 +52,7 @@ namespace storm {
                     // Check the other direction in case no hypothesis was given
                     if (hypothesis == RegionResultHypothesis::Unknown) {
                         parameterOptDir = storm::solver::invert(parameterOptDir);
-                        preciseResult = getPreciseChecker().check(region, parameterOptDir)->asExplicitQualitativeCheckResult()[*getPreciseChecker().getConsideredParametricModel().getInitialStates().begin()];
+                        preciseResult = getPreciseChecker().check(env, region, parameterOptDir)->asExplicitQualitativeCheckResult()[*getPreciseChecker().getConsideredParametricModel().getInitialStates().begin()];
                         if (preciseResult && parameterOptDir == getPreciseChecker().getCurrentCheckTask().getOptimizationDirection()) {
                             currentResult = RegionResult::AllSat;
                         } else if (!preciseResult && parameterOptDir == storm::solver::invert(getPreciseChecker().getCurrentCheckTask().getOptimizationDirection())) {
@@ -63,7 +63,7 @@ namespace storm {
             }
             
             if (sampleVerticesOfRegion && currentResult != RegionResult::AllSat && currentResult != RegionResult::AllViolated) {
-                currentResult = getPreciseChecker().sampleVertices(region, currentResult);
+                currentResult = getPreciseChecker().sampleVertices(env, region, currentResult);
             }
     
             return currentResult;
diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h
index 8fa6a4114..f0dbf3534 100644
--- a/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/ValidatingSparseParameterLiftingModelChecker.h
@@ -23,7 +23,7 @@ namespace storm {
              * We first apply unsound solution methods (standard value iteratio with doubles) and then validate the obtained result
              * by means of exact and soud methods.
              */
-            virtual RegionResult analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override;
+            virtual RegionResult analyzeRegion(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override;
 
         protected: