diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index b2349ebf7..9040f3cf4 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -142,7 +142,7 @@ namespace storm {
             assignmentDefinitionList = (assignmentDefinition % "&")[qi::_val = qi::_1] | (qi::lit("true"))[qi::_val = phoenix::construct<std::vector<storm::prism::Assignment>>()];
             assignmentDefinitionList.name("assignment list");
             
-            updateDefinition = (((expressionParser > qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];
+            updateDefinition = (((expressionParser >> qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];
             updateDefinition.name("update");
             
             updateListDefinition %= +updateDefinition(qi::_r1) % "+";
diff --git a/src/storage/dd/DdManager.cpp b/src/storage/dd/DdManager.cpp
index d3eeead6f..a6b267ae8 100644
--- a/src/storage/dd/DdManager.cpp
+++ b/src/storage/dd/DdManager.cpp
@@ -95,6 +95,12 @@ namespace storm {
             return result;
         }
         
+        template<DdType LibraryType>
+        Bdd<LibraryType> DdManager<LibraryType>::getCube(storm::expressions::Variable const& variable) const {
+            storm::dd::DdMetaVariable<LibraryType> const& metaVariable = this->getMetaVariable(variable);
+            return metaVariable.getCube();
+        }
+        
         template<DdType LibraryType>
         std::pair<storm::expressions::Variable, storm::expressions::Variable> DdManager<LibraryType>::addMetaVariable(std::string const& name, int_fast64_t low, int_fast64_t high, boost::optional<std::pair<MetaVariablePosition, storm::expressions::Variable>> const& position) {
             // Check whether the variable name is legal.
diff --git a/src/storage/dd/DdManager.h b/src/storage/dd/DdManager.h
index c299336d6..64588b91c 100644
--- a/src/storage/dd/DdManager.h
+++ b/src/storage/dd/DdManager.h
@@ -102,7 +102,7 @@ namespace storm {
             
             /*!
              * Retrieves the ADD representing the identity of the meta variable, i.e., a function that maps all legal
-             * values of the range of the meta variable to themselves.
+             * values of the range of the meta variable to the values themselves.
              *
              * @param variable The expression variable associated with the meta variable.
              * @return The identity of the meta variable.
@@ -110,6 +110,14 @@ namespace storm {
             template<typename ValueType>
             Add<LibraryType, ValueType> getIdentity(storm::expressions::Variable const& variable) const;
             
+            /*!
+             * Retrieves a BDD that is the cube of the variables representing the given meta variable.
+             *
+             * @param variable The expression variable associated with the meta variable.
+             * @return The cube of the meta variable.
+             */
+            Bdd<LibraryType> getCube(storm::expressions::Variable const& variable) const;
+            
             /*!
              * Adds an integer meta variable with the given range.
              *
diff --git a/src/storage/prism/menu_games/AbstractCommand.cpp b/src/storage/prism/menu_games/AbstractCommand.cpp
index 10f03967d..1c050cbc5 100644
--- a/src/storage/prism/menu_games/AbstractCommand.cpp
+++ b/src/storage/prism/menu_games/AbstractCommand.cpp
@@ -18,13 +18,13 @@ namespace storm {
     namespace prism {
         namespace menu_games {
             template <storm::dd::DdType DdType, typename ValueType>
-            AbstractCommand<DdType, ValueType>::AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.manager)), expressionInformation(expressionInformation), ddInformation(ddInformation), command(command), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), cachedDd(std::make_pair(ddInformation.manager->getBddZero(), 0)), decisionVariables() {
+            AbstractCommand<DdType, ValueType>::AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.getManager())), expressionInformation(expressionInformation), ddInformation(ddInformation), command(command), variablePartition(expressionInformation.getVariables()), relevantPredicatesAndVariables(), cachedDd(std::make_pair(ddInformation.manager->getBddZero(), 0)), decisionVariables() {
 
                 // Make the second component of relevant predicates have the right size.
                 relevantPredicatesAndVariables.second.resize(command.getNumberOfUpdates());
                 
                 // Assert all range expressions to enforce legal variable values.
-                for (auto const& rangeExpression : expressionInformation.rangeExpressions) {
+                for (auto const& rangeExpression : expressionInformation.getRangeExpressions()) {
                     smtSolver->add(rangeExpression);
                 }
                 
@@ -32,8 +32,8 @@ namespace storm {
                 smtSolver->add(command.getGuardExpression());
 
                 // Refine the command based on all initial predicates.
-                std::vector<uint_fast64_t> allPredicateIndices(expressionInformation.predicates.size());
-                for (auto index = 0; index < expressionInformation.predicates.size(); ++index) {
+                std::vector<uint_fast64_t> allPredicateIndices(expressionInformation.getPredicates().size());
+                for (auto index = 0; index < expressionInformation.getPredicates().size(); ++index) {
                     allPredicateIndices[index] = index;
                 }
                 this->refine(allPredicateIndices);
@@ -43,7 +43,7 @@ namespace storm {
             void AbstractCommand<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& predicates) {
                 // Add all predicates to the variable partition.
                 for (auto predicateIndex : predicates) {
-                    variablePartition.addExpression(expressionInformation.predicates[predicateIndex]);
+                    variablePartition.addExpression(expressionInformation.getPredicates()[predicateIndex]);
                 }
                 
                 STORM_LOG_TRACE("Current variable partition is: " << variablePartition);
@@ -173,9 +173,9 @@ namespace storm {
             template <storm::dd::DdType DdType, typename ValueType>
             void AbstractCommand<DdType, ValueType>::addMissingPredicates(std::pair<std::set<uint_fast64_t>, std::vector<std::set<uint_fast64_t>>> const& newRelevantPredicates) {
                 // Determine and add new relevant source predicates.
-                std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSourceVariables = AbstractionDdInformation<DdType, ValueType>::declareNewVariables(expressionInformation.manager, relevantPredicatesAndVariables.first, newRelevantPredicates.first);
+                std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSourceVariables = AbstractionDdInformation<DdType, ValueType>::declareNewVariables(expressionInformation.getManager(), relevantPredicatesAndVariables.first, newRelevantPredicates.first);
                 for (auto const& element : newSourceVariables) {
-                    smtSolver->add(storm::expressions::iff(element.first, expressionInformation.predicates[element.second]));
+                    smtSolver->add(storm::expressions::iff(element.first, expressionInformation.getPredicates()[element.second]));
                     decisionVariables.push_back(element.first);
                 }
                 
@@ -185,9 +185,9 @@ namespace storm {
                 
                 // Do the same for every update.
                 for (uint_fast64_t index = 0; index < command.get().getNumberOfUpdates(); ++index) {
-                    std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSuccessorVariables = AbstractionDdInformation<DdType, ValueType>::declareNewVariables(expressionInformation.manager, relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]);
+                    std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newSuccessorVariables = AbstractionDdInformation<DdType, ValueType>::declareNewVariables(expressionInformation.getManager(), relevantPredicatesAndVariables.second[index], newRelevantPredicates.second[index]);
                     for (auto const& element : newSuccessorVariables) {
-                        smtSolver->add(storm::expressions::iff(element.first, expressionInformation.predicates[element.second].substitute(command.get().getUpdate(index).getAsVariableToExpressionMap())));
+                        smtSolver->add(storm::expressions::iff(element.first, expressionInformation.getPredicates()[element.second].substitute(command.get().getUpdate(index).getAsVariableToExpressionMap())));
                         decisionVariables.push_back(element.first);
                     }
                     
@@ -277,7 +277,7 @@ namespace storm {
                 auto relevantIte = relevantPredicatesAndVariables.first.end();
                 
                 storm::dd::Bdd<DdType> result = ddInformation.manager->getBddOne();
-                for (uint_fast64_t predicateIndex = 0; predicateIndex < expressionInformation.predicates.size(); ++predicateIndex) {
+                for (uint_fast64_t predicateIndex = 0; predicateIndex < expressionInformation.getPredicates().size(); ++predicateIndex) {
                     if (relevantIt == relevantIte || relevantIt->second != predicateIndex) {
                         result &= ddInformation.predicateIdentities[predicateIndex];
                     } else {
diff --git a/src/storage/prism/menu_games/AbstractCommand.h b/src/storage/prism/menu_games/AbstractCommand.h
index c3396df6b..77db969fe 100644
--- a/src/storage/prism/menu_games/AbstractCommand.h
+++ b/src/storage/prism/menu_games/AbstractCommand.h
@@ -50,7 +50,7 @@ namespace storm {
                  * @param ddInformation The DD-related information including the manager.
                  * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                  */
-                AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
+                AbstractCommand(storm::prism::Command const& command, AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
                 
                 /*!
                  * Refines the abstract command with the given predicates.
@@ -156,7 +156,7 @@ namespace storm {
                 std::unique_ptr<storm::solver::SmtSolver> smtSolver;
 
                 // The expression-related information.
-                AbstractionExpressionInformation const& expressionInformation;
+                AbstractionExpressionInformation& expressionInformation;
                 
                 // The DD-related information.
                 AbstractionDdInformation<DdType, ValueType> const& ddInformation;
diff --git a/src/storage/prism/menu_games/AbstractModule.cpp b/src/storage/prism/menu_games/AbstractModule.cpp
index c13a64274..c9d597d02 100644
--- a/src/storage/prism/menu_games/AbstractModule.cpp
+++ b/src/storage/prism/menu_games/AbstractModule.cpp
@@ -13,7 +13,7 @@ namespace storm {
         namespace menu_games {
             
             template <storm::dd::DdType DdType, typename ValueType>
-            AbstractModule<DdType, ValueType>::AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), ddInformation(ddInformation), commands(), module(module) {
+            AbstractModule<DdType, ValueType>::AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolverFactory(smtSolverFactory), ddInformation(ddInformation), commands(), module(module) {
                 
                 // For each concrete command, we create an abstract counterpart.
                 for (auto const& command : module.getCommands()) {
diff --git a/src/storage/prism/menu_games/AbstractModule.h b/src/storage/prism/menu_games/AbstractModule.h
index 7013efaa0..473eb4913 100644
--- a/src/storage/prism/menu_games/AbstractModule.h
+++ b/src/storage/prism/menu_games/AbstractModule.h
@@ -31,7 +31,7 @@ namespace storm {
                  * @param ddInformation The DD-related information including the manager.
                  * @param smtSolverFactory A factory that is to be used for creating new SMT solvers.
                  */
-                AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
+                AbstractModule(storm::prism::Module const& module, AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
                 
                 /*!
                  * Refines the abstract module with the given predicates.
diff --git a/src/storage/prism/menu_games/AbstractProgram.cpp b/src/storage/prism/menu_games/AbstractProgram.cpp
index ad1e7e7e0..fd2403a91 100644
--- a/src/storage/prism/menu_games/AbstractProgram.cpp
+++ b/src/storage/prism/menu_games/AbstractProgram.cpp
@@ -17,7 +17,7 @@ namespace storm {
         namespace menu_games {
             
             template <storm::dd::DdType DdType, typename ValueType>
-            AbstractProgram<DdType, ValueType>::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared<storm::dd::DdManager<DdType>>(), initialPredicates), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(expressionInformation, ddInformation, program.getAllGuards(true), *this->smtSolverFactory), currentGame(nullptr) {
+            AbstractProgram<DdType, ValueType>::AbstractProgram(storm::expressions::ExpressionManager& expressionManager, storm::prism::Program const& program, std::vector<storm::expressions::Expression> const& initialPredicates, std::unique_ptr<storm::utility::solver::SmtSolverFactory>&& smtSolverFactory, bool addAllGuards) : smtSolverFactory(std::move(smtSolverFactory)), ddInformation(std::make_shared<storm::dd::DdManager<DdType>>()), expressionInformation(expressionManager, initialPredicates, program.getAllExpressionVariables(), program.getAllRangeExpressions()), modules(), program(program), initialStateAbstractor(expressionInformation, ddInformation, {program.getInitialConstruct().getInitialStatesExpression()}, *this->smtSolverFactory), addedAllGuards(addAllGuards), bottomStateAbstractor(expressionInformation, ddInformation, program.getAllGuards(true), *this->smtSolverFactory), currentGame(nullptr) {
                 
                 // For now, we assume that there is a single module. If the program has more than one module, it needs
                 // to be flattened before the procedure.
@@ -30,7 +30,8 @@ namespace storm {
                     // If we were requested to add all guards to the set of predicates, we do so now.
                     for (auto const& command : module.getCommands()) {
                         if (addAllGuards) {
-                            expressionInformation.predicates.push_back(command.getGuardExpression());
+                            expressionInformation.getPredicates().push_back(command.getGuardExpression());
+                            allGuards.push_back(command.getGuardExpression());
                         }
                         maximalUpdateCount = std::max(maximalUpdateCount, static_cast<uint_fast64_t>(command.getNumberOfUpdates()));
                     }
@@ -39,18 +40,28 @@ namespace storm {
                 }
                 
                 // Create DD variable for the command encoding.
-                ddInformation.commandDdVariable = ddInformation.manager->addMetaVariable("command", 0, totalNumberOfCommands - 1, std::make_pair(storm::dd::MetaVariablePosition::Above, ddInformation.predicateDdVariables.front().first)).first;
+                ddInformation.commandDdVariable = ddInformation.manager->addMetaVariable("command", 0, totalNumberOfCommands - 1).first;
                 
                 // Create DD variable for update encoding.
-                ddInformation.updateDdVariable = ddInformation.manager->addMetaVariable("update", 0, maximalUpdateCount - 1, std::make_pair(storm::dd::MetaVariablePosition::Above, ddInformation.predicateDdVariables.front().first)).first;
+                ddInformation.updateDdVariable = ddInformation.manager->addMetaVariable("update", 0, maximalUpdateCount - 1).first;
                 
                 // Create DD variables encoding the nondeterministic choices of player 2.
                 // NOTE: currently we assume that 100 variables suffice, which corresponds to 2^100 possible choices.
                 // If for some reason this should not be enough, we could grow this vector dynamically, but odds are
                 // that it's impossible to treat such models in any event.
                 for (uint_fast64_t index = 0; index < 100; ++index) {
-                    storm::expressions::Variable newOptionVar = ddInformation.manager->addMetaVariable("opt" + std::to_string(index), std::make_pair(storm::dd::MetaVariablePosition::Above, ddInformation.predicateDdVariables.front().first)).first;
-                    ddInformation.optionDdVariables.push_back(std::make_pair(newOptionVar, ddInformation.manager->template getIdentity<ValueType>(newOptionVar).toBdd()));
+                    storm::expressions::Variable newOptionVar = ddInformation.manager->addMetaVariable("opt" + std::to_string(index)).first;
+                    ddInformation.optionDdVariables.push_back(std::make_pair(newOptionVar, ddInformation.manager->getEncoding(newOptionVar, 1)));
+                }
+                
+                // Now that we have created all other DD variables, we create the DD variables for the predicates.
+                if (addAllGuards) {
+                    for (auto const& guard : allGuards) {
+                        ddInformation.addPredicate(guard);
+                    }
+                }
+                for (auto const& predicate : initialPredicates) {
+                    ddInformation.addPredicate(predicate);
                 }
                 
                 // For each module of the concrete program, we create an abstract counterpart.
@@ -70,7 +81,7 @@ namespace storm {
                 STORM_LOG_THROW(!predicates.empty(), storm::exceptions::InvalidArgumentException, "Cannot refine without predicates.");
                 
                 // Add the predicates to the global list of predicates.
-                uint_fast64_t firstNewPredicateIndex = expressionInformation.predicates.size();
+                uint_fast64_t firstNewPredicateIndex = expressionInformation.getPredicates().size();
                 expressionInformation.addPredicates(predicates);
                 
                 // Create DD variables and some auxiliary data structures for the new predicates.
@@ -81,7 +92,7 @@ namespace storm {
 
                 // Create a list of indices of the predicates, so we can refine the abstract modules and the state set abstractors.
                 std::vector<uint_fast64_t> newPredicateIndices;
-                for (uint_fast64_t index = firstNewPredicateIndex; index < expressionInformation.predicates.size(); ++index) {
+                for (uint_fast64_t index = firstNewPredicateIndex; index < expressionInformation.getPredicates().size(); ++index) {
                     newPredicateIndices.push_back(index);
                 }
                 
@@ -110,7 +121,7 @@ namespace storm {
             storm::dd::Bdd<DdType> AbstractProgram<DdType, ValueType>::getStates(storm::expressions::Expression const& predicate) {
                 STORM_LOG_ASSERT(currentGame != nullptr, "Game was not properly created.");
                 uint_fast64_t index = 0;
-                for (auto const& knownPredicate : expressionInformation.predicates) {
+                for (auto const& knownPredicate : expressionInformation.getPredicates()) {
                     if (knownPredicate.areSame(predicate)) {
                         return currentGame->getReachableStates() && ddInformation.predicateBdds[index].first;
                     }
diff --git a/src/storage/prism/menu_games/AbstractProgram.h b/src/storage/prism/menu_games/AbstractProgram.h
index ce30ec1cb..ceccb33fc 100644
--- a/src/storage/prism/menu_games/AbstractProgram.h
+++ b/src/storage/prism/menu_games/AbstractProgram.h
@@ -62,7 +62,7 @@ namespace storm {
                 storm::dd::Bdd<DdType> getStates(storm::expressions::Expression const& predicate);
                 
                 /*!
-                 * Refines the abstract module with the given predicates.
+                 * Refines the abstract program with the given predicates.
                  *
                  * @param predicates The new predicates.
                  */
diff --git a/src/storage/prism/menu_games/AbstractionDdInformation.cpp b/src/storage/prism/menu_games/AbstractionDdInformation.cpp
index 70eddd811..a60bdb80f 100644
--- a/src/storage/prism/menu_games/AbstractionDdInformation.cpp
+++ b/src/storage/prism/menu_games/AbstractionDdInformation.cpp
@@ -53,7 +53,7 @@ namespace storm {
                 
                 predicateDdVariables.push_back(newMetaVariable);
                 predicateBdds.emplace_back(manager->getEncoding(newMetaVariable.first, 1), manager->getEncoding(newMetaVariable.second, 1));
-                predicateIdentities.push_back(manager->template getIdentity<ValueType>(newMetaVariable.first).equals(manager->template getIdentity<ValueType>(newMetaVariable.second)));
+                predicateIdentities.push_back(manager->getEncoding(newMetaVariable.first, 1).iff(manager->getEncoding(newMetaVariable.second, 1)));
                 allPredicateIdentities &= predicateIdentities.back();
                 sourceVariables.insert(newMetaVariable.first);
                 successorVariables.insert(newMetaVariable.second);
diff --git a/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp b/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp
index b3fd5a64a..621d59c01 100644
--- a/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp
+++ b/src/storage/prism/menu_games/AbstractionExpressionInformation.cpp
@@ -20,6 +20,38 @@ namespace storm {
                     this->addPredicate(predicate);
                 }
             }
+         
+            storm::expressions::ExpressionManager& AbstractionExpressionInformation::getManager() {
+                return manager;
+            }
+            
+            storm::expressions::ExpressionManager const& AbstractionExpressionInformation::getManager() const {
+                return manager;
+            }
+ 
+            std::vector<storm::expressions::Expression>& AbstractionExpressionInformation::getPredicates() {
+                return predicates;
+            }
+            
+            std::vector<storm::expressions::Expression> const& AbstractionExpressionInformation::getPredicates() const {
+                return predicates;
+            }
+            
+            std::set<storm::expressions::Variable>& AbstractionExpressionInformation::getVariables() {
+                return variables;
+            }
+            
+            std::set<storm::expressions::Variable> const& AbstractionExpressionInformation::getVariables() const {
+                return variables;
+            }
+            
+            std::vector<storm::expressions::Expression>& AbstractionExpressionInformation::getRangeExpressions() {
+                return rangeExpressions;
+            }
+            
+            std::vector<storm::expressions::Expression> const& AbstractionExpressionInformation::getRangeExpressions() const {
+                return rangeExpressions;
+            }
             
         }
     }
diff --git a/src/storage/prism/menu_games/AbstractionExpressionInformation.h b/src/storage/prism/menu_games/AbstractionExpressionInformation.h
index 2037fa364..25c23cb30 100644
--- a/src/storage/prism/menu_games/AbstractionExpressionInformation.h
+++ b/src/storage/prism/menu_games/AbstractionExpressionInformation.h
@@ -40,6 +40,63 @@ namespace storm {
                  */
                 void addPredicates(std::vector<storm::expressions::Expression> const& predicates);
                 
+                /*!
+                 * Retrieves the expression manager.
+                 *
+                 * @return The manager.
+                 */
+                storm::expressions::ExpressionManager& getManager();
+
+                /*!
+                 * Retrieves the expression manager.
+                 *
+                 * @return The manager.
+                 */
+                storm::expressions::ExpressionManager const& getManager() const;
+                
+                /*!
+                 * Retrieves all currently known predicates.
+                 *
+                 * @return The list of known predicates.
+                 */
+                std::vector<storm::expressions::Expression>& getPredicates();
+
+                /*!
+                 * Retrieves all currently known predicates.
+                 *
+                 * @return The list of known predicates.
+                 */
+                std::vector<storm::expressions::Expression> const& getPredicates() const;
+
+                /*!
+                 * Retrieves all currently known variables.
+                 *
+                 * @return The set of known variables.
+                 */
+                std::set<storm::expressions::Variable>& getVariables();
+                
+                /*!
+                 * Retrieves all currently known variables.
+                 *
+                 * @return The set of known variables.
+                 */
+                std::set<storm::expressions::Variable> const& getVariables() const;
+                
+                /*!
+                 * Retrieves a list of expressions that ensure the ranges of the variables.
+                 *
+                 * @return The range expressions.
+                 */
+                std::vector<storm::expressions::Expression>& getRangeExpressions();
+                
+                /*!
+                 * Retrieves a list of expressions that ensure the ranges of the variables.
+                 *
+                 * @return The range expressions.
+                 */
+                std::vector<storm::expressions::Expression> const& getRangeExpressions() const;
+                
+            private:
                 // The manager responsible for the expressions of the program and the SMT solvers.
                 storm::expressions::ExpressionManager& manager;
                 
diff --git a/src/storage/prism/menu_games/StateSetAbstractor.cpp b/src/storage/prism/menu_games/StateSetAbstractor.cpp
index 06ac2728e..db8dab01d 100644
--- a/src/storage/prism/menu_games/StateSetAbstractor.cpp
+++ b/src/storage/prism/menu_games/StateSetAbstractor.cpp
@@ -13,10 +13,10 @@ namespace storm {
         namespace menu_games {
             
             template <storm::dd::DdType DdType, typename ValueType>
-            StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, std::vector<storm::expressions::Expression> const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.manager)), expressionInformation(expressionInformation), ddInformation(ddInformation), variablePartition(expressionInformation.variables), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(ddInformation.manager->getBddZero()), constraint(ddInformation.manager->getBddOne()) {
+            StateSetAbstractor<DdType, ValueType>::StateSetAbstractor(AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, std::vector<storm::expressions::Expression> const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory) : smtSolver(smtSolverFactory.create(expressionInformation.getManager())), expressionInformation(expressionInformation), ddInformation(ddInformation), variablePartition(expressionInformation.getVariables()), relevantPredicatesAndVariables(), concretePredicateVariables(), needsRecomputation(false), cachedBdd(ddInformation.manager->getBddZero()), constraint(ddInformation.manager->getBddOne()) {
                 
                 // Assert all range expressions to enforce legal variable values.
-                for (auto const& rangeExpression : expressionInformation.rangeExpressions) {
+                for (auto const& rangeExpression : expressionInformation.getRangeExpressions()) {
                     smtSolver->add(rangeExpression);
                 }
                 
@@ -31,8 +31,8 @@ namespace storm {
                 }
                 
                 // Refine the command based on all initial predicates.
-                std::vector<uint_fast64_t> allPredicateIndices(expressionInformation.predicates.size());
-                for (auto index = 0; index < expressionInformation.predicates.size(); ++index) {
+                std::vector<uint_fast64_t> allPredicateIndices(expressionInformation.getPredicates().size());
+                for (auto index = 0; index < expressionInformation.getPredicates().size(); ++index) {
                     allPredicateIndices[index] = index;
                 }
                 this->refine(allPredicateIndices);
@@ -40,10 +40,10 @@ namespace storm {
             
             template <storm::dd::DdType DdType, typename ValueType>
             void StateSetAbstractor<DdType, ValueType>::addMissingPredicates(std::set<uint_fast64_t> const& newRelevantPredicateIndices) {
-                std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newPredicateVariables = AbstractionDdInformation<DdType, ValueType>::declareNewVariables(expressionInformation.manager, relevantPredicatesAndVariables, newRelevantPredicateIndices);
+                std::vector<std::pair<storm::expressions::Variable, uint_fast64_t>> newPredicateVariables = AbstractionDdInformation<DdType, ValueType>::declareNewVariables(expressionInformation.getManager(), relevantPredicatesAndVariables, newRelevantPredicateIndices);
                 
                 for (auto const& element : newPredicateVariables) {
-                    smtSolver->add(storm::expressions::iff(element.first, expressionInformation.predicates[element.second]));
+                    smtSolver->add(storm::expressions::iff(element.first, expressionInformation.getPredicates()[element.second]));
                     decisionVariables.push_back(element.first);
                 }
                 
@@ -55,7 +55,7 @@ namespace storm {
             void StateSetAbstractor<DdType, ValueType>::refine(std::vector<uint_fast64_t> const& newPredicates) {
                 // Make the partition aware of the new predicates, which may make more predicates relevant to the abstraction.
                 for (auto const& predicateIndex : newPredicates) {
-                    variablePartition.addExpression(expressionInformation.predicates[predicateIndex]);
+                    variablePartition.addExpression(expressionInformation.getPredicates()[predicateIndex]);
                 }
                 needsRecomputation = true;
             }
@@ -135,7 +135,7 @@ namespace storm {
                 smtSolver->push();
                 
                 // Then add the constraint.
-                std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>> result = constraint.toExpression(expressionInformation.manager, ddInformation.bddVariableIndexToPredicateMap);
+                std::pair<std::vector<storm::expressions::Expression>, std::unordered_map<std::pair<uint_fast64_t, uint_fast64_t>, storm::expressions::Variable>> result = constraint.toExpression(expressionInformation.getManager(), ddInformation.bddVariableIndexToPredicateMap);
                 
                 for (auto const& expression : result.first) {
                     smtSolver->add(expression);
diff --git a/src/storage/prism/menu_games/StateSetAbstractor.h b/src/storage/prism/menu_games/StateSetAbstractor.h
index c722d695b..fef77eb29 100644
--- a/src/storage/prism/menu_games/StateSetAbstractor.h
+++ b/src/storage/prism/menu_games/StateSetAbstractor.h
@@ -58,7 +58,7 @@ namespace storm {
                  * supposed to abstract.
                  * @param smtSolverFactory A factory that can create new SMT solvers.
                  */
-                StateSetAbstractor(AbstractionExpressionInformation const& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, std::vector<storm::expressions::Expression> const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
+                StateSetAbstractor(AbstractionExpressionInformation& expressionInformation, AbstractionDdInformation<DdType, ValueType> const& ddInformation, std::vector<storm::expressions::Expression> const& statePredicates, storm::utility::solver::SmtSolverFactory const& smtSolverFactory);
                 
                 /*!
                  * Refines the abstractor by making the given predicates new abstract predicates.
@@ -116,7 +116,7 @@ namespace storm {
                 std::unique_ptr<storm::solver::SmtSolver> smtSolver;
                 
                 // The expression-related information.
-                AbstractionExpressionInformation const& expressionInformation;
+                AbstractionExpressionInformation& expressionInformation;
                 
                 // The DD-related information.
                 AbstractionDdInformation<DdType, ValueType> const& ddInformation;
diff --git a/src/storage/prism/menu_games/VariablePartition.h b/src/storage/prism/menu_games/VariablePartition.h
index ae6637943..b9d87dad1 100644
--- a/src/storage/prism/menu_games/VariablePartition.h
+++ b/src/storage/prism/menu_games/VariablePartition.h
@@ -74,7 +74,7 @@ namespace storm {
                 uint_fast64_t getBlockIndexOfVariable(storm::expressions::Variable const& variable) const;
                 
                 /*!
-                 * Retrieves the number of blocks of the varible partition.
+                 * Retrieves the number of blocks of the variable partition.
                  *
                  * @return The number of blocks in this partition.
                  */