diff --git a/src/storm-cli-utilities/cli.cpp b/src/storm-cli-utilities/cli.cpp
index c7b18fb7a..3d7096d1c 100644
--- a/src/storm-cli-utilities/cli.cpp
+++ b/src/storm-cli-utilities/cli.cpp
@@ -242,8 +242,20 @@ namespace storm {
             // Start by setting some urgent options (log levels, resources, etc.)
             setUrgentOptions();
             
-            // Parse and preprocess symbolic input (PRISM, JANI, properties, etc.)
-            SymbolicInput symbolicInput = parseAndPreprocessSymbolicInput();
+            // Parse symbolic input (PRISM, JANI, properties, etc.)
+            SymbolicInput symbolicInput = parseSymbolicInput();
+            
+            // Get the engine to use
+            // TODO: Create a new method that gets the used engine and the used environment (using portfolio engine)
+            auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
+            auto engine = coreSettings.getEngine();
+            auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
+            auto builderType = getBuilderType(engine, buildSettings.isJitSet());
+            // TODO: (end of method)
+            
+            symbolicInput = preprocessSymbolicInput(symbolicInput, builderType);
+            exportSymbolicInput(symbolicInput);
+
             
             auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
             if (generalSettings.isParametricSet()) {
diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index a49d244e5..7154e7399 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -10,6 +10,7 @@
 #include "storm/utility/storm-version.h"
 #include "storm/utility/macros.h"
 #include "storm/utility/NumberTraits.h"
+#include "storm/utility/Engine.h"
 
 #include "storm/utility/initialize.h"
 #include "storm/utility/Stopwatch.h"
@@ -62,13 +63,12 @@ namespace storm {
             boost::optional<std::vector<storm::jani::Property>> preprocessedProperties;
         };
         
-        void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input, storm::builder::BuilderType const& builderType) {
+        void parseSymbolicModelDescription(storm::settings::modules::IOSettings const& ioSettings, SymbolicInput& input) {
             if (ioSettings.isPrismOrJaniInputSet()) {
                 storm::utility::Stopwatch modelParsingWatch(true);
                 if (ioSettings.isPrismInputSet()) {
                     input.model = storm::api::parseProgram(ioSettings.getPrismInputFilename(), storm::settings::getModule<storm::settings::modules::BuildSettings>().isPrismCompatibilityEnabled());
                 } else {
-                    storm::jani::ModelFeatures supportedFeatures = storm::api::getSupportedJaniFeatures(builderType);
                     boost::optional<std::vector<std::string>> propertyFilter;
                     if (ioSettings.isJaniPropertiesSet()) {
                         if (ioSettings.areJaniPropertiesSelected()) {
@@ -79,7 +79,7 @@ namespace storm {
                     } else {
                         propertyFilter = std::vector<std::string>();
                     }
-                    auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename(), supportedFeatures, propertyFilter);
+                    auto janiInput = storm::api::parseJaniModel(ioSettings.getJaniInputFilename(), propertyFilter);
                     input.model = std::move(janiInput.first);
                     if (ioSettings.isJaniPropertiesSet()) {
                         input.properties = std::move(janiInput.second);
@@ -102,20 +102,48 @@ namespace storm {
                 input.properties.insert(input.properties.end(), newProperties.begin(), newProperties.end());
             }
         }
-        
-        SymbolicInput parseSymbolicInput(storm::builder::BuilderType const& builderType) {
-            auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+      
+        SymbolicInput parseSymbolicInputQvbs(storm::settings::modules::IOSettings const& ioSettings) {
+            // Parse the model input
+            SymbolicInput input;
+            storm::storage::QvbsBenchmark benchmark(ioSettings.getQvbsModelName());
+            STORM_PRINT_AND_LOG(benchmark.getInfo(ioSettings.getQvbsInstanceIndex(), ioSettings.getQvbsPropertyFilter()));
+            storm::utility::Stopwatch modelParsingWatch(true);
+            auto janiInput = storm::api::parseJaniModel(benchmark.getJaniFile(ioSettings.getQvbsInstanceIndex()), ioSettings.getQvbsPropertyFilter());
+            input.model = std::move(janiInput.first);
+            input.properties = std::move(janiInput.second);
+            modelParsingWatch.stop();
+            STORM_PRINT("Time for model input parsing: " << modelParsingWatch << "." << std::endl << std::endl);
             
-            // Parse the property filter, if any is given.
+            // Parse additional properties
             boost::optional<std::set<std::string>> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter());
-            
-            SymbolicInput input;
-            parseSymbolicModelDescription(ioSettings, input, builderType);
             parseProperties(ioSettings, input, propertyFilter);
             
+            // Substitute constant definitions
+            auto constantDefinitions = input.model.get().parseConstantDefinitions(benchmark.getConstantDefinition(ioSettings.getQvbsInstanceIndex()));
+            input.model = input.model.get().preprocess(constantDefinitions);
+            if (!input.properties.empty()) {
+                input.properties = storm::api::substituteConstantsInProperties(input.properties, constantDefinitions);
+            }
+            
             return input;
         }
         
+        SymbolicInput parseSymbolicInput() {
+            auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+            if (ioSettings.isQvbsInputSet()) {
+                return parseSymbolicInputQvbs(ioSettings);
+            } else {
+                // Parse the property filter, if any is given.
+                boost::optional<std::set<std::string>> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter());
+                
+                SymbolicInput input;
+                parseSymbolicModelDescription(ioSettings, input);
+                parseProperties(ioSettings, input, propertyFilter);
+                return input;
+            }
+        }
+        
         void ensureNoUndefinedPropertyConstants(std::vector<storm::jani::Property> const& properties) {
             // Make sure there are no undefined constants remaining in any property.
             for (auto const& property : properties) {
@@ -135,6 +163,11 @@ namespace storm {
             
             SymbolicInput output = input;
             
+            if (output.model && output.model.get().isJaniModel()) {
+                storm::jani::ModelFeatures supportedFeatures = storm::api::getSupportedJaniFeatures(builderType);
+                storm::api::simplifyJaniModel(output.model.get().asJaniModel(), output.properties, supportedFeatures);
+            }
+            
             // Substitute constant definitions in symbolic input.
             std::string constantDefinitionString = ioSettings.getConstantDefinitionString();
             std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
@@ -185,63 +218,28 @@ namespace storm {
             }
         }
         
-        storm::builder::BuilderType getBuilderType(storm::settings::modules::CoreSettings::Engine const& engine, bool useJit) {
-            if (engine == storm::settings::modules::CoreSettings::Engine::Dd || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::DdSparse || engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement) {
+        storm::builder::BuilderType getBuilderType(storm::utility::Engine const& engine, bool useJit) {
+            if (engine == storm::utility::Engine::Dd || engine == storm::utility::Engine::Hybrid || engine == storm::utility::Engine::DdSparse || engine == storm::utility::Engine::AbstractionRefinement) {
                 return storm::builder::BuilderType::Dd;
-            } else if (engine == storm::settings::modules::CoreSettings::Engine::Sparse) {
+            } else if (engine == storm::utility::Engine::Sparse) {
                 if (useJit) {
                     return storm::builder::BuilderType::Jit;
                 } else {
                     return storm::builder::BuilderType::Explicit;
                 }
-            } else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) {
+            } else if (engine == storm::utility::Engine::Exploration) {
                 return storm::builder::BuilderType::Explicit;
             }
             STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to determine the model builder type.");
         }
         
-        SymbolicInput parseAndPreprocessSymbolicInputQvbs(storm::settings::modules::IOSettings const& ioSettings, storm::builder::BuilderType const& builderType) {
-            // Parse the model input
-            SymbolicInput input;
-            storm::storage::QvbsBenchmark benchmark(ioSettings.getQvbsModelName());
-            STORM_PRINT_AND_LOG(benchmark.getInfo(ioSettings.getQvbsInstanceIndex(), ioSettings.getQvbsPropertyFilter()));
-            storm::utility::Stopwatch modelParsingWatch(true);
-            storm::jani::ModelFeatures supportedFeatures = storm::api::getSupportedJaniFeatures(builderType);
-            auto janiInput = storm::api::parseJaniModel(benchmark.getJaniFile(ioSettings.getQvbsInstanceIndex()), supportedFeatures, ioSettings.getQvbsPropertyFilter());
-            input.model = std::move(janiInput.first);
-            input.properties = std::move(janiInput.second);
-            modelParsingWatch.stop();
-            STORM_PRINT("Time for model input parsing: " << modelParsingWatch << "." << std::endl << std::endl);
-            
-            // Parse additional properties
-            boost::optional<std::set<std::string>> propertyFilter = storm::api::parsePropertyFilter(ioSettings.getPropertyFilter());
-            parseProperties(ioSettings, input, propertyFilter);
-            
-            // Substitute constant definitions
-            auto constantDefinitions = input.model.get().parseConstantDefinitions(benchmark.getConstantDefinition(ioSettings.getQvbsInstanceIndex()));
-            input.model = input.model.get().preprocess(constantDefinitions);
-            if (!input.properties.empty()) {
-                input.properties = storm::api::substituteConstantsInProperties(input.properties, constantDefinitions);
-            }
-            
-            ensureNoUndefinedPropertyConstants(input.properties);
-            return input;
-        }
-        
-        SymbolicInput parseAndPreprocessSymbolicInput() {
+        SymbolicInput parseAndPreprocessSymbolicInput(storm::utility::Engine const& engine) {
             // Get the used builder type to handle cases where preprocessing depends on it
             auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
-            auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
-            auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
-            auto builderType = getBuilderType(coreSettings.getEngine(), buildSettings.isJitSet());
+            auto builderType = getBuilderType(engine, buildSettings.isJitSet());
             
-            SymbolicInput input;
-            if (ioSettings.isQvbsInputSet()) {
-                input = parseAndPreprocessSymbolicInputQvbs(ioSettings, builderType);
-            } else {
-                input = parseSymbolicInput(builderType);
-                input = preprocessSymbolicInput(input, builderType);
-            }
+            SymbolicInput input = parseSymbolicInput();
+            input = preprocessSymbolicInput(input, builderType);
             exportSymbolicInput(input);
             return input;
         }
@@ -308,7 +306,7 @@ namespace storm {
         }
         
         template <storm::dd::DdType DdType, typename ValueType>
-        std::shared_ptr<storm::models::ModelBase> buildModel(storm::settings::modules::CoreSettings::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) {
+        std::shared_ptr<storm::models::ModelBase> buildModel(storm::utility::Engine const& engine, SymbolicInput const& input, storm::settings::modules::IOSettings const& ioSettings) {
             storm::utility::Stopwatch modelBuildingWatch(true);
 
             auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
@@ -321,7 +319,7 @@ namespace storm {
                     result = buildModelSparse<ValueType>(input, buildSettings);
                 }
             } else if (ioSettings.isExplicitSet() || ioSettings.isExplicitDRNSet() || ioSettings.isExplicitIMCASet()) {
-                STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input.");
+                STORM_LOG_THROW(engine == storm::utility::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Can only use sparse engine with explicit input.");
                 result = buildModelExplicit<ValueType>(ioSettings, buildSettings);
             }
             
@@ -479,7 +477,7 @@ namespace storm {
                 result = std::make_unique<std::pair<std::shared_ptr<storm::models::Model<ExportValueType>>, bool>>(symbolicModel->template toValueType<ExportValueType>(), !std::is_same<ValueType, ExportValueType>::value);
             }
             
-            if (result && result->first->isSymbolicModel() && storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::DdSparse) {
+            if (result && result->first->isSymbolicModel() && storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::utility::Engine::DdSparse) {
                 // Mark as changed.
                 result->second = true;
                 
@@ -903,10 +901,10 @@ namespace storm {
         
         template <storm::dd::DdType DdType, typename ValueType>
         typename std::enable_if<DdType != storm::dd::DdType::CUDD || std::is_same<ValueType, double>::value, void>::type verifySymbolicModel(std::shared_ptr<storm::models::ModelBase> const& model, SymbolicInput const& input, storm::settings::modules::CoreSettings const& coreSettings) {
-            storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine();;
-            if (engine == storm::settings::modules::CoreSettings::Engine::Hybrid) {
+            storm::utility::Engine engine = coreSettings.getEngine();;
+            if (engine == storm::utility::Engine::Hybrid) {
                 verifyWithHybridEngine<DdType, ValueType>(model, input);
-            } else if (engine == storm::settings::modules::CoreSettings::Engine::Dd) {
+            } else if (engine == storm::utility::Engine::Dd) {
                 verifyWithDdEngine<DdType, ValueType>(model, input);
             } else {
                 verifyWithAbstractionRefinementEngine<DdType, ValueType>(model, input);
@@ -929,7 +927,7 @@ namespace storm {
         }
         
         template <storm::dd::DdType DdType, typename BuildValueType, typename VerificationValueType = BuildValueType>
-        std::shared_ptr<storm::models::ModelBase> buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, storm::settings::modules::CoreSettings::Engine engine) {
+        std::shared_ptr<storm::models::ModelBase> buildPreprocessExportModelWithValueTypeAndDdlib(SymbolicInput const& input, storm::utility::Engine engine) {
             auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
             auto buildSettings = storm::settings::getModule<storm::settings::modules::BuildSettings>();
             std::shared_ptr<storm::models::ModelBase> model;
@@ -961,11 +959,11 @@ namespace storm {
             auto counterexampleSettings = storm::settings::getModule<storm::settings::modules::CounterexampleGeneratorSettings>();
 
             // For several engines, no model building step is performed, but the verification is started right away.
-            storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine();
+            storm::utility::Engine engine = coreSettings.getEngine();
             
-            if (engine == storm::settings::modules::CoreSettings::Engine::AbstractionRefinement && abstractionSettings.getAbstractionRefinementMethod() == storm::settings::modules::AbstractionSettings::Method::Games) {
+            if (engine == storm::utility::Engine::AbstractionRefinement && abstractionSettings.getAbstractionRefinementMethod() == storm::settings::modules::AbstractionSettings::Method::Games) {
                 verifyWithAbstractionRefinementEngine<DdType, VerificationValueType>(input);
-            } else if (engine == storm::settings::modules::CoreSettings::Engine::Exploration) {
+            } else if (engine == storm::utility::Engine::Exploration) {
                 verifyWithExplorationEngine<VerificationValueType>(input);
             } else {
                 std::shared_ptr<storm::models::ModelBase> model = buildPreprocessExportModelWithValueTypeAndDdlib<DdType, BuildValueType, VerificationValueType>(input, engine);
diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index d290dd47c..7fdf38c1c 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -39,6 +39,7 @@
 #include "storm/utility/initialize.h"
 #include "storm/utility/Stopwatch.h"
 #include "storm/utility/macros.h"
+#include "storm/utility/Engine.h"
 
 #include "storm/settings/modules/GeneralSettings.h"
 #include "storm/settings/modules/CoreSettings.h"
@@ -207,7 +208,7 @@ namespace storm {
 
             PreprocessResult result(model, false);
 
-            if (coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Hybrid) {
+            if (coreSettings.getEngine() == storm::utility::Engine::Hybrid) {
                 // Currently, hybrid engine for parametric models just refers to building the model symbolically.
                 STORM_LOG_INFO("Translating symbolic model to sparse model...");
                 result.model = storm::api::transformSymbolicToSparseModel(model);
@@ -219,7 +220,7 @@ namespace storm {
                     result.formulas = sparsePreprocessingResult.formulas;
                 }
             } else {
-                STORM_LOG_ASSERT(coreSettings.getEngine() == storm::settings::modules::CoreSettings::Engine::Dd, "Expected Dd engine.");
+                STORM_LOG_ASSERT(coreSettings.getEngine() == storm::utility::Engine::Dd, "Expected Dd engine.");
                 if (generalSettings.isBisimulationSet()) {
                     result.model = storm::cli::preprocessDdModelBisimulation(result.model->template as<storm::models::symbolic::Model<DdType, ValueType>>(), input, bisimulationSettings);
                     result.changed = true;
@@ -576,7 +577,7 @@ namespace storm {
             auto monSettings = storm::settings::getModule<storm::settings::modules::MonotonicitySettings>();
 
             auto engine = coreSettings.getEngine();
-            STORM_LOG_THROW(engine == storm::settings::modules::CoreSettings::Engine::Sparse || engine == storm::settings::modules::CoreSettings::Engine::Hybrid || engine == storm::settings::modules::CoreSettings::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models.");
+            STORM_LOG_THROW(engine == storm::utility::Engine::Sparse || engine == storm::utility::Engine::Hybrid || engine == storm::utility::Engine::Dd, storm::exceptions::InvalidSettingsException, "The selected engine is not supported for parametric models.");
 
             std::shared_ptr<storm::models::ModelBase> model;
             if (!buildSettings.isNoBuildModelSet()) {
@@ -783,13 +784,13 @@ namespace storm {
         void processOptions() {
             // Start by setting some urgent options (log levels, resources, etc.)
             storm::cli::setUrgentOptions();
-
-            // Parse and preprocess symbolic input (PRISM, JANI, properties, etc.)
-            SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput();
-
+            
             auto coreSettings = storm::settings::getModule<storm::settings::modules::CoreSettings>();
             auto engine = coreSettings.getEngine();
-            STORM_LOG_WARN_COND(engine != storm::settings::modules::CoreSettings::Engine::Dd || engine != storm::settings::modules::CoreSettings::Engine::Hybrid || coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "The selected DD library does not support parametric models. Switching to Sylvan...");
+            STORM_LOG_WARN_COND(engine != storm::utility::Engine::Dd || engine != storm::utility::Engine::Hybrid || coreSettings.getDdLibraryType() == storm::dd::DdType::Sylvan, "The selected DD library does not support parametric models. Switching to Sylvan...");
+            
+            // Parse and preprocess symbolic input (PRISM, JANI, properties, etc.)
+            SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput(engine);
 
             processInputWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalFunction>(symbolicInput);
         }
diff --git a/src/storm-parsers/api/model_descriptions.cpp b/src/storm-parsers/api/model_descriptions.cpp
index 983156279..4213b9c52 100644
--- a/src/storm-parsers/api/model_descriptions.cpp
+++ b/src/storm-parsers/api/model_descriptions.cpp
@@ -35,8 +35,7 @@ namespace storm {
             return std::make_pair(std::move(parsedResult.first), std::move(propertyMap));
         }
         
-        std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures, boost::optional<std::vector<std::string>> const& propertyFilter) {
-            
+        std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& filename, boost::optional<std::vector<std::string>> const& propertyFilter) {
             bool parseProperties = !propertyFilter.is_initialized() || !propertyFilter.get().empty();
             std::pair<storm::jani::Model, std::vector<storm::jani::Property>> modelAndFormulae = storm::parser::JaniParser::parse(filename, parseProperties);
             
@@ -57,13 +56,20 @@ namespace storm {
                 }
                 modelAndFormulae.second = std::move(newProperties);
             }
-            
             modelAndFormulae.first.checkValid();
-            auto nonEliminatedFeatures = modelAndFormulae.first.restrictToFeatures(allowedFeatures, modelAndFormulae.second);
-            STORM_LOG_THROW(nonEliminatedFeatures.empty(), storm::exceptions::NotSupportedException, "The used model feature(s) " << nonEliminatedFeatures.toString() << " is/are not in the list of allowed features.");
             return modelAndFormulae;
         }
         
+        std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& supportedFeatures, boost::optional<std::vector<std::string>> const& propertyFilter) {
+            auto modelAndFormulae = parseJaniModel(filename, propertyFilter);
+            simplifyJaniModel(modelAndFormulae.first, modelAndFormulae.second, supportedFeatures);
+            return modelAndFormulae;
+        }
+        
+        void simplifyJaniModel(storm::jani::Model& model, std::vector<storm::jani::Property>& properties , storm::jani::ModelFeatures const& supportedFeatures) {
+            auto nonEliminatedFeatures = model.restrictToFeatures(supportedFeatures, properties);
+            STORM_LOG_THROW(nonEliminatedFeatures.empty(), storm::exceptions::NotSupportedException, "The used model feature(s) " << nonEliminatedFeatures.toString() << " is/are not in the list of supported features.");
+        }
         
     }
 }
diff --git a/src/storm-parsers/api/model_descriptions.h b/src/storm-parsers/api/model_descriptions.h
index 8e45304c3..0d094b44c 100644
--- a/src/storm-parsers/api/model_descriptions.h
+++ b/src/storm-parsers/api/model_descriptions.h
@@ -20,6 +20,9 @@ namespace storm {
         storm::prism::Program parseProgram(std::string const& filename, bool prismCompatibility = false, bool simplify = true);
         
         std::pair<storm::jani::Model, std::map<std::string, storm::jani::Property>> parseJaniModel(std::string const& filename);
+        std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& filename, boost::optional<std::vector<std::string>> const& propertyFilter = boost::none);
         std::pair<storm::jani::Model, std::vector<storm::jani::Property>> parseJaniModel(std::string const& filename, storm::jani::ModelFeatures const& allowedFeatures, boost::optional<std::vector<std::string>> const& propertyFilter = boost::none);
+        void simplifyJaniModel(storm::jani::Model& model, std::vector<storm::jani::Property>& properties , storm::jani::ModelFeatures const& supportedFeatures);
+
     }
 }
diff --git a/src/storm-pomdp-cli/storm-pomdp.cpp b/src/storm-pomdp-cli/storm-pomdp.cpp
index 9fc95f904..25c0ac954 100644
--- a/src/storm-pomdp-cli/storm-pomdp.cpp
+++ b/src/storm-pomdp-cli/storm-pomdp.cpp
@@ -99,9 +99,9 @@ int main(const int argc, const char** argv) {
         auto const& pomdpSettings = storm::settings::getModule<storm::settings::modules::POMDPSettings>();
 
         // For several engines, no model building step is performed, but the verification is started right away.
-        storm::settings::modules::CoreSettings::Engine engine = coreSettings.getEngine();
+        storm::utility::Engine engine = coreSettings.getEngine();
 
-        storm::cli::SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput();
+        storm::cli::SymbolicInput symbolicInput = storm::cli::parseAndPreprocessSymbolicInput(engine);
         // We should not export here if we are going to do some processing first.
         auto model = storm::cli::buildPreprocessExportModelWithValueTypeAndDdlib<storm::dd::DdType::Sylvan, storm::RationalNumber>(symbolicInput, engine);
         STORM_LOG_THROW(model && model->getType() == storm::models::ModelType::Pomdp, storm::exceptions::WrongFormatException, "Expected a POMDP.");
diff --git a/src/storm/settings/modules/CoreSettings.cpp b/src/storm/settings/modules/CoreSettings.cpp
index bc9ea87fb..19df21f3e 100644
--- a/src/storm/settings/modules/CoreSettings.cpp
+++ b/src/storm/settings/modules/CoreSettings.cpp
@@ -32,8 +32,11 @@ namespace storm {
             const std::string CoreSettings::intelTbbOptionName = "enable-tbb";
             const std::string CoreSettings::intelTbbOptionShortName = "tbb";
             
-            CoreSettings::CoreSettings() : ModuleSettings(moduleName), engine(CoreSettings::Engine::Sparse) {
-                std::vector<std::string> engines = {"sparse", "hybrid", "dd", "dd-to-sparse", "expl", "abs"};
+            CoreSettings::CoreSettings() : ModuleSettings(moduleName), engine(storm::utility::Engine::Sparse) {
+                std::vector<std::string> engines;
+                for (auto e : storm::utility::getEngines()) {
+                    engines.push_back(storm::utility::toString(e));
+                }
                 this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName)
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use.").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator(engines)).setDefaultValueString("sparse").build()).build());
                 
@@ -133,32 +136,19 @@ namespace storm {
                 return this->getOption(cudaOptionName).getHasOptionBeenSet();
             }
             
-            CoreSettings::Engine CoreSettings::getEngine() const {
+            storm::utility::Engine CoreSettings::getEngine() const {
                 return engine;
             }
 
-            void CoreSettings::setEngine(Engine newEngine) {
+            void CoreSettings::setEngine(storm::utility::Engine const& newEngine) {
                 this->engine = newEngine;
             }
             
             void CoreSettings::finalize() {
                 // Finalize engine.
                 std::string engineStr = this->getOption(engineOptionName).getArgumentByName("name").getValueAsString();
-                if (engineStr == "sparse") {
-                    engine =  CoreSettings::Engine::Sparse;
-                } else if (engineStr == "hybrid") {
-                    engine = CoreSettings::Engine::Hybrid;
-                } else if (engineStr == "dd") {
-                    engine = CoreSettings::Engine::Dd;
-                } else if (engineStr == "dd-to-sparse") {
-                    engine = CoreSettings::Engine::DdSparse;
-                } else if (engineStr == "expl") {
-                    engine = CoreSettings::Engine::Exploration;
-                } else if (engineStr == "abs") {
-                    engine = CoreSettings::Engine::AbstractionRefinement;
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown engine '" << engineStr << "'.");
-                }
+                engine = storm::utility::engineFromString(engineStr);
+                STORM_LOG_THROW(engine != storm::utility::Engine::Unknown, storm::exceptions::IllegalArgumentValueException, "Unknown engine '" << engineStr << "'.");
             }
 
             bool CoreSettings::check() const {
diff --git a/src/storm/settings/modules/CoreSettings.h b/src/storm/settings/modules/CoreSettings.h
index 405fad91f..c7a2e6f4d 100644
--- a/src/storm/settings/modules/CoreSettings.h
+++ b/src/storm/settings/modules/CoreSettings.h
@@ -5,6 +5,7 @@
 #include "storm/settings/modules/ModuleSettings.h"
 
 #include "storm/builder/ExplorationOrder.h"
+#include "storm/utility/Engine.h"
 
 namespace storm {
     namespace solver {
@@ -26,10 +27,6 @@ namespace storm {
              */
             class CoreSettings : public ModuleSettings {
             public:
-                // An enumeration of all engines.
-                enum class Engine {
-                    Sparse, Hybrid, Dd, DdSparse, Exploration, AbstractionRefinement
-                };
 
                 /*!
                  * Creates a new set of core settings.
@@ -118,12 +115,12 @@ namespace storm {
                  *
                  * @return The selected engine.
                  */
-                Engine getEngine() const;
+                storm::utility::Engine getEngine() const;
 
                 /*!
                  * Sets the engine for further usage.
                  */
-                void setEngine(Engine);
+                void setEngine(storm::utility::Engine const& engine);
 
                 bool check() const override;
                 void finalize() override;
@@ -132,7 +129,7 @@ namespace storm {
                 static const std::string moduleName;
 
             private:
-                Engine engine;
+                storm::utility::Engine engine;
 
                 // Define the string names of the options as constants.
                 static const std::string eqSolverOptionName;
diff --git a/src/storm/settings/modules/ExplorationSettings.cpp b/src/storm/settings/modules/ExplorationSettings.cpp
index 6be2d8c3f..ef86740d2 100644
--- a/src/storm/settings/modules/ExplorationSettings.cpp
+++ b/src/storm/settings/modules/ExplorationSettings.cpp
@@ -7,6 +7,7 @@
 #include "storm/settings/SettingsManager.h"
 
 #include "storm/utility/macros.h"
+#include "storm/utility/Engine.h"
 #include "storm/exceptions/IllegalArgumentValueException.h"
 
 namespace storm {
@@ -91,7 +92,7 @@ namespace storm {
                                     this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getHasOptionBeenSet() ||
                                     this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getHasOptionBeenSet() ||
                                     this->getOption(nextStateHeuristicOptionName).getHasOptionBeenSet();
-                STORM_LOG_WARN_COND(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Exploration || !optionsSet, "Exploration engine is not selected, so setting options for it has no effect.");
+                STORM_LOG_WARN_COND(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::utility::Engine::Exploration || !optionsSet, "Exploration engine is not selected, so setting options for it has no effect.");
                 return true;
             }
         } // namespace modules
diff --git a/src/storm/utility/Engine.cpp b/src/storm/utility/Engine.cpp
new file mode 100644
index 000000000..19a719100
--- /dev/null
+++ b/src/storm/utility/Engine.cpp
@@ -0,0 +1,141 @@
+#include "storm/utility/Engine.h"
+
+#include "storm/utility/macros.h"
+
+#include "storm/models/ModelType.h"
+
+#include "storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
+#include "storm/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
+#include "storm/modelchecker/csl/SparseCtmcCslModelChecker.h"
+#include "storm/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
+
+#include "storm/modelchecker/prctl/HybridDtmcPrctlModelChecker.h"
+#include "storm/modelchecker/prctl/HybridMdpPrctlModelChecker.h"
+#include "storm/modelchecker/csl/HybridCtmcCslModelChecker.h"
+
+#include "storm/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
+#include "storm/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
+#include "storm/modelchecker/CheckTask.h"
+
+#include "storm/storage/SymbolicModelDescription.h"
+
+namespace storm {
+    namespace utility {
+        
+        // Returns a list of all available engines (excluding Unknown)
+        std::vector<Engine> getEngines() {
+            std::vector<Engine> res;
+            for (int i = 0; i != static_cast<int>(Engine::Unknown); ++i) {
+                res.push_back(static_cast<Engine>(i));
+            }
+            return res;
+        }
+        
+        std::string toString(Engine const& engine) {
+            switch (engine) {
+                case Engine::Sparse:
+                    return "sparse";
+                case Engine::Hybrid:
+                    return "hybrid";
+                case Engine::Dd:
+                    return "dd";
+                case Engine::DdSparse:
+                    return "dd-to-sparse";
+                case Engine::Exploration:
+                    return "expl";
+                case Engine::AbstractionRefinement:
+                    return "abs";
+                case Engine::Unknown:
+                    return "UNKNOWN";
+                default:
+                    STORM_LOG_ASSERT(false, "The given engine has no name assigned to it.");
+                    return "UNKNOWN";
+            }
+        }
+        
+        std::ostream& operator<<(std::ostream& os, Engine const& engine) {
+            os << toString(engine);
+            return os;
+        }
+
+        Engine engineFromString(std::string const& engineStr) {
+            for (Engine const& e : getEngines()) {
+                if (engineStr == toString(e)) {
+                    return e;
+                }
+            }
+            STORM_LOG_ERROR("The engine '" << engineStr << "' was not found.");
+            return Engine::Unknown;
+        }
+
+        template <storm::dd::DdType ddType, typename ValueType>
+        bool canHandle(storm::utility::Engine const& engine, storm::models::ModelType const& modelType, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
+            // Define types to improve readability
+            typedef storm::models::ModelType ModelType;
+#ifdef TODO_IMPLEMENT_CAN_HANDLE_STATIC
+            switch (engine) {
+                case Engine::Sparse:
+                case Engine::DdSparse:
+                    switch (modelType) {
+                        case ModelType::Dtmc:
+                            return storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>>::canHandleStatic(checkTask);
+                        case ModelType::Mdp:
+                            return storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>>::canHandleStatic(checkTask);
+                        case ModelType::Ctmc:
+                            return storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>>::canHandleStatic(checkTask);
+                        case ModelType::MarkovAutomaton:
+                            return storm::modelchecker::SparseMarkovAutomatonCslModelChecker<storm::models::sparse::MarkovAutomaton<ValueType>>::canHandleStatic(checkTask);
+                        case ModelType::S2pg:
+                        case ModelType::Pomdp:
+                            return false;
+                    }
+                    break;
+                case Engine::Hybrid:
+                    switch (modelType) {
+                        case ModelType::Dtmc:
+                            return storm::modelchecker::HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<ddType, ValueType>>::canHandleStatic(checkTask);
+                        case ModelType::Mdp:
+                            return storm::modelchecker::HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<ddType, ValueType>>::canHandleStatic(checkTask);
+                        case ModelType::Ctmc:
+                            return storm::modelchecker::HybridCtmcCslModelChecker<storm::models::symbolic::Ctmc<ddType, ValueType>>::canHandleStatic(checkTask);
+                        case ModelType::MarkovAutomaton:
+                        case ModelType::S2pg:
+                        case ModelType::Pomdp:
+                            return false;
+                    }
+                    break;
+                case Engine::Dd:
+                    switch (modelType) {
+                        case ModelType::Dtmc:
+                            return storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<ddType, ValueType>>::canHandleStatic(checkTask);
+                        case ModelType::Mdp:
+                            return storm::modelchecker::SymbolicMdpPrctlModelChecker<storm::models::symbolic::Mdp<ddType, ValueType>>::canHandleStatic(checkTask);
+                        case ModelType::Ctmc:
+                        case ModelType::MarkovAutomaton:
+                        case ModelType::S2pg:
+                        case ModelType::Pomdp:
+                            return false;
+                    }
+                    break;
+                default:
+                    STORM_LOG_ERROR("The selected engine" << engine << " is not considered.");
+            }
+#endif
+            STORM_LOG_ERROR("The selected combination of engine (" << engine << ") and model type (" << modelType << ") does not seem to be supported for this value type.");
+            return false;
+        }
+        
+        template <storm::dd::DdType ddType, typename ValueType>
+        bool canHandle(storm::utility::Engine const& engine, storm::storage::SymbolicModelDescription const& modelDescription, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
+            // Check handability based on model type
+            if (!canHandle(engine, modelDescription.getModelType(), checkTask)) {
+                return false;
+            }
+            // TODO
+            return true;
+        }
+        
+
+        
+    }
+}
\ No newline at end of file
diff --git a/src/storm/utility/Engine.h b/src/storm/utility/Engine.h
new file mode 100644
index 000000000..be14f1971
--- /dev/null
+++ b/src/storm/utility/Engine.h
@@ -0,0 +1,71 @@
+#pragma once
+
+#include <ostream>
+#include <vector>
+
+#include "storm/models/ModelType.h"
+#include "storm/storage/dd/DdType.h"
+
+namespace storm {
+    
+    // Forward Declarations
+    namespace logic {
+        class Formula;
+    }
+    namespace modelchecker{
+        template<typename FormulaType, typename ValueType>
+        class CheckTask;
+    }
+    namespace storage {
+        class SymbolicModelDescription;
+    }
+    
+    namespace utility {
+        
+        /// An enumeration of all engines.
+        enum class Engine {
+            // The last one should always be 'Unknown' to make sure that the getEngines() method below works.
+            Sparse, Hybrid, Dd, DdSparse, Exploration, AbstractionRefinement, Unknown
+        };
+        
+        /*!
+         * Returns a list of all available engines (excluding Unknown)
+         */
+        std::vector<Engine> getEngines();
+        
+        /*!
+         * Returns a string representation of the given engine.
+         */
+        std::string toString(Engine const& engine);
+        
+        /*!
+         * Writes the string representation of the given engine to the given stream
+         */
+        std::ostream& operator<<(std::ostream& os, Engine const& engine);
+        
+        /*!
+         * Parses the string representation of an engine and returns the corresponding engine.
+         * If the engine is not found, we print an error and return Engine::Unknown.
+         */
+        Engine engineFromString(std::string const& engineStr);
+
+        /*!
+         * Returns false if the given model type and checkTask can certainly not be handled by the given engine.
+         * Notice that the set of handable model checking queries is only overapproximated, i.e. if this returns true,
+         * the query could still be not supported by the engine. This behavior is due to the fact that we sometimes need
+         * to actually build the model in order to decide whether it is supported.
+         */
+        template <storm::dd::DdType ddType, typename ValueType>
+        bool canHandle(storm::utility::Engine const& engine, storm::models::ModelType const& modelType, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask);
+        
+        /*!
+         * Returns false if the given model description and checkTask can certainly not be handled by the given engine.
+         * Notice that the set of handable model checking queries is only overapproximated, i.e. if this returns true,
+         * the query could still be not supported by the engine. This behavior is due to the fact that we sometimes need
+         * to actually build the model in order to decide whether it is supported.
+         */
+        template <storm::dd::DdType ddType, typename ValueType>
+        bool canHandle(storm::utility::Engine const& engine, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask, storm::storage::SymbolicModelDescription const& modelDescription);
+        
+    }
+}
\ No newline at end of file