diff --git a/src/storm/modelchecker/parametric/ParameterLifting.cpp b/src/storm/modelchecker/parametric/ParameterLifting.cpp
index 657b37d07..fb6ab1015 100644
--- a/src/storm/modelchecker/parametric/ParameterLifting.cpp
+++ b/src/storm/modelchecker/parametric/ParameterLifting.cpp
@@ -19,6 +19,12 @@
 #include "storm/exceptions/InvalidStateException.h"
 #include "storm/exceptions/InvalidArgumentException.h"
 
+#include "storm/utility/Stopwatch.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/IOSettings.h"
+#include "storm/settings/modules/DebugSettings.h"
+
+
 namespace storm {
     namespace modelchecker {
         namespace parametric {
@@ -34,7 +40,10 @@ namespace storm {
                 STORM_LOG_THROW(checkTask.isOnlyInitialStatesRelevantSet(), storm::exceptions::NotSupportedException, "Parameter lifting requires a property where only the value in the initial states is relevant.");
                 STORM_LOG_THROW(checkTask.isBoundSet(), storm::exceptions::NotSupportedException, "Parameter lifting requires a bounded property.");
                 
+                storm::utility::Stopwatch sw(true);
                 simplifyParametricModel(checkTask);
+                sw.stop();
+                std::cout << "SIStats: " << sw << std::endl;
                 initializeUnderlyingCheckers();
                 currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType>>(checkTask.substituteFormula(*currentFormula));
 
@@ -83,6 +92,36 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "When analyzing a region, an invalid initial result was given: " << initialResult);
                 }
                 
+                // TODO remove this:
+                if(storm::settings::getModule<storm::settings::modules::DebugSettings>().isDebugSet() && storm::settings::getModule<storm::settings::modules::IOSettings>().isPrismInputSet() &&  storm::settings::getModule<storm::settings::modules::IOSettings>().isPropertySet()) {
+                    std::vector<storm::utility::parametric::Valuation<typename SparseModelType::ValueType>> points;
+                    if(result == RegionCheckResult::AllSat || result == RegionCheckResult::AllViolated) {
+                        points = region.getVerticesOfRegion(region.getVariables());
+                        points.push_back(region.getCenterPoint());
+                    } else if (result == RegionCheckResult::CenterSat ||  result == RegionCheckResult::CenterViolated) {
+                        points.push_back(region.getCenterPoint());
+                    }
+                    if(!points.empty()) std::cout << "VALIDATE_REGION:" << region.toString(true) << std::endl;
+                    for (auto const& p : points) {
+                        if((result == RegionCheckResult::AllSat) || (result == RegionCheckResult::CenterSat)) {
+                            std::cout << "EXPECTTRUE:";
+                        } else {
+                            std::cout << "EXPECTFALSE:";
+                        }
+                        std::cout << "STORMEXECUTABLE --prism " << storm::settings::getModule<storm::settings::modules::IOSettings>().getPrismInputFilename()
+                                  <<                 " --prop " <<  storm::settings::getModule<storm::settings::modules::IOSettings>().getProperty();
+                        if( storm::settings::getModule<storm::settings::modules::IOSettings>().isConstantsSet()) {
+                            std::cout <<             " -const " <<  storm::settings::getModule<storm::settings::modules::IOSettings>().getConstantDefinitionString();
+                        }
+                        for(auto varDef = p.begin(); varDef != p.end(); ++varDef) {
+                            if(varDef!=p.begin())  std::cout << ",";
+                            std::cout << varDef->first << "=" << storm::utility::convertNumber<double>(varDef->second);
+                        }
+                        std::cout << std::endl;
+                    }
+                }
+
+                
                 return result;
             }
     
@@ -90,6 +129,8 @@ namespace storm {
             std::vector<std::pair<storm::storage::ParameterRegion<typename SparseModelType::ValueType>, RegionCheckResult>> ParameterLifting<SparseModelType, ConstantType>::performRegionRefinement(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType const& threshold) const {
                 STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " .");
                 
+                storm::utility::Stopwatch sw(true);
+                
                 auto areaOfParameterSpace = region.area();
                 auto fractionOfUndiscoveredArea = storm::utility::one<typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType>();
                 auto fractionOfAllSatArea = storm::utility::zero<typename storm::storage::ParameterRegion<typename SparseModelType::ValueType>::CoefficientType>();
@@ -131,6 +172,9 @@ namespace storm {
                     ++indexOfCurrentRegion;
                 }
                 resultRegions.resize(regions.size());
+                
+                sw.stop();
+                std::cout << "REStats: " << sw << std::endl;
                 return storm::utility::vector::filterVector(regions, resultRegions);
             }
     
diff --git a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp
index 830113f77..90dfd89fd 100644
--- a/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseDtmcInstantiationModelChecker.cpp
@@ -18,15 +18,25 @@ namespace storm {
             template <typename SparseModelType, typename ConstantType>
             std::unique_ptr<CheckResult> SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>::check(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.");
+                this->swInstantiation.start();
                 auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
+                this->swInstantiation.stop();
                 STORM_LOG_ASSERT(instantiatedModel.getTransitionMatrix().isProbabilistic(), "Instantiated matrix is not probabilistic!");
                 storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ConstantType>> modelChecker(instantiatedModel);
 
                 // Check if there are some optimizations implemented for the specified property
+                this->swCheck.start();
                 if(!this->currentCheckTask->isQualitativeSet() && this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true))) {
-                    return checkWithHint(modelChecker);
+                    auto result = checkWithHint(modelChecker);
+                    this->swCheck.stop();
+                    return result;
+                    //return checkWithHint(modelChecker);
                 } else {
-                    return modelChecker.check(*this->currentCheckTask);
+                    STORM_LOG_WARN("Checking without hint"); // todo:remove this warning
+                    auto result = modelChecker.check(*this->currentCheckTask);
+                    this->swCheck.stop();
+                    return result;
+                    //return modelChecker.check(*this->currentCheckTask);
                 }
             }
                 
diff --git a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
index 6578bd58c..40d20c21f 100644
--- a/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseDtmcParameterLiftingModelChecker.cpp
@@ -166,7 +166,10 @@ namespace storm {
                     return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(resultsForNonMaybeStates);
                 }
                 
+                this->swInstantiation.start();
                 parameterLifter->specifyRegion(region, dirForParameters);
+                this->swInstantiation.stop();
+                this->swCheck.start();
                 
                 // Set up the solver
                 auto solver = solverFactory->create(parameterLifter->getMatrix());
@@ -198,6 +201,7 @@ namespace storm {
                     result[maybeState] = *maybeStateResIt;
                     ++maybeStateResIt;
                 }
+                this->swCheck.stop();
                 return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(std::move(result));
             }
             
diff --git a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h
index fb39772e1..474082ff8 100644
--- a/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h
+++ b/src/storm/modelchecker/parametric/SparseInstantiationModelChecker.h
@@ -6,6 +6,8 @@
 #include "storm/modelchecker/hints/ModelCheckerHint.h"
 #include "storm/utility/parametric.h"
 
+#include "storm/utility/Stopwatch.h"
+
 namespace storm {
     namespace modelchecker {
         namespace parametric {
@@ -18,6 +20,11 @@ namespace storm {
             public:
                 SparseInstantiationModelChecker(SparseModelType const& parametricModel);
                 
+                                
+                ~SparseInstantiationModelChecker() {
+                    std::cout << "INStats (instantiation/check): " << swInstantiation << "\t" << swCheck << std::endl;
+                }
+                
                 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;
@@ -29,6 +36,8 @@ namespace storm {
                 
                 SparseModelType const& parametricModel;
                 std::unique_ptr<CheckTask<storm::logic::Formula, ConstantType>> currentCheckTask;
+                
+                storm::utility::Stopwatch swInstantiation, swCheck;
 
             private:
                 // store the current formula. Note that currentCheckTask only stores a reference to the formula.
diff --git a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp
index 675218d71..cfc13cda2 100644
--- a/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseMdpInstantiationModelChecker.cpp
@@ -19,19 +19,27 @@ namespace storm {
            template <typename SparseModelType, typename ConstantType>
             std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::check(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.");
+                this->swInstantiation.start();
                 auto const& instantiatedModel = modelInstantiator.instantiate(valuation);
+                this->swInstantiation.stop();
                 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
+                this->swCheck.start();
                 if(!this->currentCheckTask->isQualitativeSet() && this->currentCheckTask->getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true))) {
-                    return checkWithResultHint(modelChecker);
+                    auto result = checkWithResultHint(modelChecker);
+                    this->swCheck.stop();
+                    return result;
+                    //return checkWithResultHint(modelChecker);
                 } else {
-                    return modelChecker.check(*this->currentCheckTask);
+                    auto result = modelChecker.check(*this->currentCheckTask);
+                    this->swCheck.stop();
+                    return result;
+                    //return modelChecker.check(*this->currentCheckTask);
                 }
             }
             
-                
             template <typename SparseModelType, typename ConstantType>
             std::unique_ptr<CheckResult> SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>::checkWithResultHint(storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ConstantType>>& modelchecker) {
                 
diff --git a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp
index 227aea2eb..4410adf55 100644
--- a/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseMdpParameterLiftingModelChecker.cpp
@@ -200,7 +200,10 @@ namespace storm {
                     return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(resultsForNonMaybeStates);
                 }
                 
+                this->swInstantiation.start();
                 parameterLifter->specifyRegion(region, dirForParameters);
+                this->swInstantiation.stop();
+                this->swCheck.start();
                 
                 // Set up the solver
                 auto solver = solverFactory->create(player1Matrix, parameterLifter->getMatrix());
@@ -238,6 +241,7 @@ namespace storm {
                     result[maybeState] = *maybeStateResIt;
                     ++maybeStateResIt;
                 }
+                this->swCheck.stop();
                 return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(std::move(result));
             }
             
diff --git a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp
index 93fce21f7..ff9a4a7f9 100644
--- a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp
+++ b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.cpp
@@ -22,7 +22,7 @@ namespace storm {
             
             template <typename SparseModelType, typename ConstantType>
             void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
-                
+                swInit.start();
                 reset();
                 currentFormula = checkTask.getFormula().asSharedPointer();
                 currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, ConstantType>>(checkTask.substituteFormula(*currentFormula).template convertValueType<ConstantType>());
@@ -46,6 +46,7 @@ namespace storm {
                         specifyCumulativeRewardFormula(currentCheckTask->substituteFormula(rewOpFormula.getSubformula().asCumulativeRewardFormula()));
                     }
                 }
+                swInit.stop();
             }
             
             template <typename SparseModelType, typename ConstantType>
diff --git a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h
index 59fd8458b..0d5629dda 100644
--- a/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h
+++ b/src/storm/modelchecker/parametric/SparseParameterLiftingModelChecker.h
@@ -7,6 +7,8 @@
 #include "storm/solver/OptimizationDirection.h"
 #include "storm/utility/parametric.h"
 
+#include "storm/utility/Stopwatch.h"
+
 namespace storm {
     namespace modelchecker {
         namespace parametric {
@@ -22,6 +24,10 @@ namespace storm {
             public:
                 SparseParameterLiftingModelChecker(SparseModelType const& parametricModel);
                 
+                ~SparseParameterLiftingModelChecker() {
+                    std::cout << "PLStats (init/instantiation/check): " << swInit << "\t" << swInstantiation << "\t" << swCheck << std::endl;
+                }
+                
                 virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const = 0;
                 
                 void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
@@ -49,6 +55,8 @@ namespace storm {
                 
                 SparseModelType const& parametricModel;
                 std::unique_ptr<CheckTask<storm::logic::Formula, ConstantType>> currentCheckTask;
+              
+                storm::utility::Stopwatch swInit, swInstantiation, swCheck;
 
             private:
                 // store the current formula. Note that currentCheckTask only stores a reference to the formula.