diff --git a/examples/dtmc/synchronous_leader/leader4_8.pm b/examples/dtmc/synchronous_leader/leader4_8.pm
index fc8f167a0..188039cf3 100644
--- a/examples/dtmc/synchronous_leader/leader4_8.pm
+++ b/examples/dtmc/synchronous_leader/leader4_8.pm
@@ -4,8 +4,8 @@
 dtmc
 
 // CONSTANTS
-const N = 4; // number of processes
-const K = 8; // range of probabilistic choice
+const int N = 4; // number of processes
+const int K = 8; // range of probabilistic choice
 
 // counter module used to count the number of processes that have been read
 // and to know when a process has decided
diff --git a/examples/dtmc/synchronous_leader/leader5_8.pm b/examples/dtmc/synchronous_leader/leader5_8.pm
index 72139fda9..4723ed5b0 100644
--- a/examples/dtmc/synchronous_leader/leader5_8.pm
+++ b/examples/dtmc/synchronous_leader/leader5_8.pm
@@ -4,8 +4,8 @@
 dtmc
 
 // CONSTANTS
-const N = 5; // number of processes
-const K = 8; // range of probabilistic choice
+const int N = 5; // number of processes
+const int K = 8; // range of probabilistic choice
 
 // counter module used to count the number of processes that have been read
 // and to know when a process has decided
diff --git a/examples/dtmc/synchronous_leader/leader6_8.pm b/examples/dtmc/synchronous_leader/leader6_8.pm
index 283042ad5..a31773b1d 100644
--- a/examples/dtmc/synchronous_leader/leader6_8.pm
+++ b/examples/dtmc/synchronous_leader/leader6_8.pm
@@ -4,8 +4,8 @@
 dtmc
 
 // CONSTANTS
-const N = 6; // number of processes
-const K = 8; // range of probabilistic choice
+const int N = 6; // number of processes
+const int K = 8; // range of probabilistic choice
 
 // counter module used to count the number of processes that have been read
 // and to know when a process has decided
diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h
index be293ebf6..0612f86e1 100644
--- a/src/adapters/ExplicitModelAdapter.h
+++ b/src/adapters/ExplicitModelAdapter.h
@@ -19,6 +19,7 @@
 
 #include "src/storage/prism/Program.h"
 #include "src/storage/expressions/SimpleValuation.h"
+#include "src/utility/PrismUtility.h"
 #include "src/models/AbstractModel.h"
 #include "src/models/Dtmc.h"
 #include "src/models/Ctmc.h"
@@ -32,11 +33,16 @@
 
 namespace storm {
     namespace adapters {
+        
+        using namespace storm::utility::prism;
                 
         template<typename ValueType>
         class ExplicitModelAdapter {
         public:
             typedef storm::expressions::SimpleValuation StateType;
+            typedef storm::expressions::SimpleValuationPointerHash StateHash;
+            typedef storm::expressions::SimpleValuationPointerCompare StateCompare;
+            typedef storm::expressions::SimpleValuationPointerLess StateLess;
             
             // A structure holding information about the reachable state space.
             struct StateInformation {
@@ -47,8 +53,17 @@ namespace storm {
                 // A list of reachable states.
                 std::vector<StateType*> reachableStates;
                 
+                // A list of initial states.
+                std::vector<uint_fast64_t> initialStateIndices;
+                
                 // A mapping from states to indices in the list of reachable states.
-                std::unordered_map<StateType*, uint_fast64_t, storm::expressions::SimpleValuationPointerHash, storm::expressions::SimpleValuationPointerCompare> stateToIndexMap;
+                std::unordered_map<StateType*, uint_fast64_t, StateHash, StateCompare> stateToIndexMap;
+            };
+            
+            // A structure storing information about the used variables of the program.
+            struct VariableInformation {
+                // A mapping of (integer) variable to their lower/upper bounds.
+                std::map<std::string, std::pair<int_fast64_t, int_fast64_t>> variableToBoundsMap;
             };
             
             // A structure holding the individual components of a model.
@@ -146,10 +161,15 @@ namespace storm {
                 // First, we need to parse the constant definition string.
                 std::map<std::string, storm::expressions::Expression> constantDefinitions = parseConstantDefinitionString(program, constantDefinitionString);
                 
-                storm::prism::Program definedProgram = program.defineUndefinedConstants(constantDefinitions);
-                LOG_THROW(!definedProgram.hasUndefinedConstants(), storm::exceptions::InvalidArgumentException, "Program still contains undefined constants.");
+                storm::prism::Program preparedProgram = program.defineUndefinedConstants(constantDefinitions);
+                LOG_THROW(!preparedProgram.hasUndefinedConstants(), storm::exceptions::InvalidArgumentException, "Program still contains undefined constants.");
+                
+                // Now that we have defined all the constants in the program, we need to substitute their appearances in
+                // all expressions in the program so we can then evaluate them without having to store the values of the
+                // constants in the state (i.e., valuation).
+                preparedProgram = preparedProgram.substituteConstants();
                 
-                ModelComponents modelComponents = buildModelComponents(definedProgram, rewardModelName);
+                ModelComponents modelComponents = buildModelComponents(preparedProgram, rewardModelName);
                 
                 std::unique_ptr<storm::models::AbstractModel<ValueType>> result;
                 switch (program.getModelType()) {
@@ -183,8 +203,8 @@ namespace storm {
              * @params update The update to apply.
              * @return The resulting state.
              */
-            static StateType* applyUpdate(StateType const* state, storm::prism::Update const& update) {
-                return applyUpdate(state, state, update);
+            static StateType* applyUpdate(VariableInformation const& variableInformation, StateType const* state, storm::prism::Update const& update) {
+                return applyUpdate(variableInformation, state, state, update);
             }
             
             /*!
@@ -197,29 +217,23 @@ namespace storm {
              * @param update The update to apply.
              * @return The resulting state.
              */
-            static StateType* applyUpdate(StateType const* state, StateType const* baseState, storm::prism::Update const& update) {
+            static StateType* applyUpdate(VariableInformation const& variableInformation, StateType const* state, StateType const* baseState, storm::prism::Update const& update) {
                 StateType* newState = new StateType(*state);
+                
+                // This variable needs to be declared prior to the switch, because of C++ rules.
+                int_fast64_t newValue = 0;
                 for (auto const& assignment : update.getAssignments()) {
                     switch (assignment.getExpression().getReturnType()) {
-                        case storm::expressions::ExpressionReturnType::Bool: newState->setBooleanValue(assignment.getVariableName(), assignment.getExpression().evaluateAsBool(*baseState)); break;
+                        case storm::expressions::ExpressionReturnType::Bool: newState->setBooleanValue(assignment.getVariableName(), assignment.getExpression().evaluateAsBool(baseState)); break;
                         case storm::expressions::ExpressionReturnType::Int:
-                            int_fast64_t newValue = assignment.getExpression().evaluateAsInt(*baseState));
-                            newState->setIntegerValue(assignment.getVariableName(), assignment.getExpression().evaluateAsInt(*baseState)); break;
-                        default: LOG_ASSERT(false, "Invalid type of assignment.");
-                    }
-                }
-                for (auto variableAssignmentPair : update.getBooleanAssignments()) {
-                    setValue(newState, variableInformation.booleanVariableToIndexMap.at(variableAssignmentPair.first), variableAssignmentPair.second.getExpression()->getValueAsBool(baseState));
-                }
-                for (auto variableAssignmentPair : update.getIntegerAssignments()) {
-                    int_fast64_t newVariableValue = variableAssignmentPair.second.getExpression()->getValueAsInt(baseState);
-                    bool isLegalValueForVariable = newVariableValue >= variableInformation.lowerBounds.at(variableInformation.integerVariableToIndexMap.at(variableAssignmentPair.first)) && newVariableValue <= variableInformation.upperBounds.at(variableInformation.integerVariableToIndexMap.at(variableAssignmentPair.first));
-                    
-                    if (!isLegalValueForVariable) {
-                        throw storm::exceptions::InvalidStateException() << "Invalid value '" << newVariableValue << "' for variable \"" << variableInformation.integerVariables.at(variableInformation.integerVariableToIndexMap.at(variableAssignmentPair.first)).getName() << "\". Please strengthen the guards if necessary or enlarge the domains of the variables.";
+                        {
+                            newValue = assignment.getExpression().evaluateAsInt(baseState);
+                            auto const& boundsPair = variableInformation.variableToBoundsMap.find(assignment.getVariableName());
+                            LOG_THROW(boundsPair->second.first <= newValue && newValue <= boundsPair->second.second, storm::exceptions::InvalidArgumentException, "Invalid value " << newValue << " for variable '" << assignment.getVariableName() << "'.");
+                            newState->setIntegerValue(assignment.getVariableName(), newValue); break;
+                        }
+                        default: LOG_ASSERT(false, "Invalid type of assignment."); break;
                     }
-                    
-                    setValue(newState, variableInformation.integerVariableToIndexMap.at(variableAssignmentPair.first), newVariableValue);
                 }
                 return newState;
             }
@@ -278,7 +292,7 @@ namespace storm {
                         continue;
                     }
                     
-                    std::set<uint_fast64_t> const& commandIndices = module.getCommandsByAction(action);
+                    std::set<uint_fast64_t> const& commandIndices = module.getCommandIndicesByAction(action);
                     
                     // If the module contains the action, but there is no command in the module that is labeled with
                     // this action, we don't have any feasible command combinations.
@@ -291,7 +305,7 @@ namespace storm {
                     // Look up commands by their indices and add them if the guard evaluates to true in the given state.
                     for (uint_fast64_t commandIndex : commandIndices) {
                         storm::prism::Command const& command = module.getCommand(commandIndex);
-                        if (command.getGuard()->getValueAsBool(state)) {
+                        if (command.getGuardExpression().evaluateAsBool(state)) {
                             commands.push_back(command);
                         }
                     }
@@ -323,7 +337,7 @@ namespace storm {
                         // Only consider unlabeled commands.
                         if (command.getActionName() != "") continue;
                         // Skip the command, if it is not enabled.
-                        if (!command.getGuard()->getValueAsBool(currentState)) continue;
+                        if (!command.getGuardExpression().evaluateAsBool(currentState)) continue;
                         
                         result.push_back(Choice<ValueType>(""));
                         Choice<ValueType>& choice = result.back();
@@ -343,7 +357,7 @@ namespace storm {
                             }
                             
                             // Update the choice by adding the probability/target state to it.
-                            double probabilityToAdd = update.getLikelihoodExpression()->getValueAsDouble(currentState);
+                            double probabilityToAdd = update.getLikelihoodExpression().evaluateAsDouble(currentState);
                             probabilitySum += probabilityToAdd;
                             boost::container::flat_set<uint_fast64_t> labels;
 							labels.insert(update.getGlobalIndex());
@@ -351,10 +365,7 @@ namespace storm {
                         }
                         
                         // Check that the resulting distribution is in fact a distribution.
-                        if (std::abs(1 - probabilitySum) > storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble()) {
-                            LOG4CPLUS_ERROR(logger, "Sum of update probabilities should be one for command:\n\t"  << command.toString());
-                            throw storm::exceptions::WrongFormatException() << "Sum of update probabilities should be one for command:\n\t"  << command.toString();
-                        }
+                        LOG_THROW(std::abs(1 - probabilitySum) < storm::settings::Settings::getInstance()->getOptionByLongName("precision").getArgument(0).getValueAsDouble(), storm::exceptions::WrongFormatException, "Probabilities do not sum to one for command '" << command << "'.");
                     }
                 }
                 
@@ -398,7 +409,7 @@ namespace storm {
 
                                         storm::storage::LabeledValues<double> newProbability;
                                         
-                                        double updateProbability = update.getLikelihoodExpression()->getValueAsDouble(currentState);
+                                        double updateProbability = update.getLikelihoodExpression().evaluateAsDouble(currentState);
                                         for (auto const& valueLabelSetPair : stateProbabilityPair.second) {
                                             // Copy the label set, so we can modify it.
                                             boost::container::flat_set<uint_fast64_t> newLabelSet = valueLabelSetPair.second;
@@ -510,8 +521,36 @@ namespace storm {
                 
                 // Initialize a queue and insert the initial state.
                 std::queue<uint_fast64_t> stateQueue;
-                StateType* initialState = getInitialState(program, variableInformation);
-                getOrAddStateIndex(initialState, stateInformation);
+                uint_fast64_t numberOfBooleanVariables = program.getNumberOfGlobalBooleanVariables();
+                uint_fast64_t numberOfIntegerVariables = program.getNumberOfGlobalIntegerVariables();
+                for (auto const& module : program.getModules()) {
+                    numberOfBooleanVariables += module.getNumberOfBooleanVariables();
+                    numberOfIntegerVariables += module.getNumberOfIntegerVariables();
+                }
+                StateType* initialState = new StateType(numberOfBooleanVariables, numberOfIntegerVariables, 0);
+                uint_fast64_t booleanIndex = 0;
+                uint_fast64_t integerIndex = 0;
+                for (auto const& booleanVariable : program.getGlobalBooleanVariables()) {
+                    initialState->setIdentifierIndex(booleanVariable.getName(), booleanIndex++);
+                    initialState->setBooleanValue(booleanVariable.getName(), booleanVariable.getInitialValueExpression().evaluateAsBool());
+                }
+                for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
+                    initialState->setIdentifierIndex(integerVariable.getName(), booleanIndex++);
+                    initialState->setIntegerValue(integerVariable.getName(), integerVariable.getInitialValueExpression().evaluateAsInt());
+                }
+                for (auto const& module : program.getModules()) {
+                    for (auto const& booleanVariable : module.getBooleanVariables()) {
+                        initialState->setIdentifierIndex(booleanVariable.getName(), booleanIndex++);
+                        initialState->setBooleanValue(booleanVariable.getName(), booleanVariable.getInitialValueExpression().evaluateAsBool());
+                    }
+                    for (auto const& integerVariable : module.getIntegerVariables()) {
+                        initialState->setIdentifierIndex(integerVariable.getName(), integerIndex++);
+                        initialState->setIntegerValue(integerVariable.getName(), integerVariable.getInitialValueExpression().evaluateAsInt());
+                    }
+                }
+        
+                std::pair<bool, uint_fast64_t> addIndexPair = getOrAddStateIndex(initialState, stateInformation);
+                stateInformation.initialStateIndices.push_back(addIndexPair.second);
                 stateQueue.push(stateInformation.stateToIndexMap[initialState]);
                 
                 // Now explore the current state until there is no more reachable state.
@@ -551,8 +590,8 @@ namespace storm {
                                     
                                     // Now add all rewards that match this choice.
                                     for (auto const& transitionReward : transitionRewards) {
-                                        if (transitionReward.getActionName() == "" && transitionReward.getStatePredicate()->getValueAsBool(stateInformation.reachableStates.at(currentState))) {
-                                            stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValue()->getValueAsDouble(stateInformation.reachableStates.at(currentState)));
+                                        if (transitionReward.getActionName() == "" && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
+                                            stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
                                         }
                                     }
                                 }
@@ -564,8 +603,8 @@ namespace storm {
                                 
                                     // Now add all rewards that match this choice.
                                     for (auto const& transitionReward : transitionRewards) {
-                                        if (transitionReward.getActionName() == choice.getActionLabel() && transitionReward.getStatePredicate()->getValueAsBool(stateInformation.reachableStates.at(currentState))) {
-                                            stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValue()->getValueAsDouble(stateInformation.reachableStates.at(currentState)));
+                                        if (transitionReward.getActionName() == choice.getActionLabel() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
+                                            stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
                                         }
                                     }
                                 }
@@ -602,8 +641,8 @@ namespace storm {
                                     
                                     // Now add all rewards that match this choice.
                                     for (auto const& transitionReward : transitionRewards) {
-                                        if (transitionReward.getActionName() == "" && transitionReward.getStatePredicate()->getValueAsBool(stateInformation.reachableStates.at(currentState))) {
-                                            stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValue()->getValueAsDouble(stateInformation.reachableStates.at(currentState)));
+                                        if (transitionReward.getActionName() == "" && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
+                                            stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
                                         }
                                     }
 
@@ -629,8 +668,8 @@ namespace storm {
                                     
                                     // Now add all rewards that match this choice.
                                     for (auto const& transitionReward : transitionRewards) {
-                                        if (transitionReward.getActionName() == choice.getActionLabel() && transitionReward.getStatePredicate()->getValueAsBool(stateInformation.reachableStates.at(currentState))) {
-                                            stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValue()->getValueAsDouble(stateInformation.reachableStates.at(currentState)));
+                                        if (transitionReward.getActionName() == choice.getActionLabel() && transitionReward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates.at(currentState))) {
+                                            stateToRewardMap[stateProbabilityPair.first] += ValueType(transitionReward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates.at(currentState)));
                                         }
                                     }
 
@@ -665,7 +704,15 @@ namespace storm {
             static ModelComponents buildModelComponents(storm::prism::Program const& program, std::string const& rewardModelName) {
                 ModelComponents modelComponents;
                 
-                VariableInformation variableInformation = createVariableInformation(program);
+                VariableInformation variableInformation;
+                for (auto const& integerVariable : program.getGlobalIntegerVariables()) {
+                    variableInformation.variableToBoundsMap[integerVariable.getName()] = std::make_pair(integerVariable.getLowerBoundExpression().evaluateAsInt(), integerVariable.getUpperBoundExpression().evaluateAsInt());
+                }
+                for (auto const& module : program.getModules()) {
+                    for (auto const& integerVariable : module.getIntegerVariables()) {
+                        variableInformation.variableToBoundsMap[integerVariable.getName()] = std::make_pair(integerVariable.getLowerBoundExpression().evaluateAsInt(), integerVariable.getUpperBoundExpression().evaluateAsInt());
+                    }
+                }
                 
                 // Create the structure for storing the reachable state space.
                 StateInformation stateInformation;
@@ -675,7 +722,7 @@ namespace storm {
                 
                 // Determine whether we have to combine different choices to one or whether this model can have more than
                 // one choice per state.
-                bool deterministicModel = program.getModelType() == storm::prism::Program::DTMC || program.getModelType() == storm::prism::Program::CTMC;
+                bool deterministicModel = program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::CTMC;
 
                 // Build the transition and reward matrices.
                 storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, 0, 0, !deterministicModel, 0);
@@ -709,29 +756,28 @@ namespace storm {
              * @return The state labeling of the given program.
              */
             static storm::models::AtomicPropositionsLabeling buildStateLabeling(storm::prism::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation) {
-                std::map<std::string, std::unique_ptr<storm::prism::expressions::BaseExpression>> const& labels = program.getLabels();
+                std::vector<storm::prism::Label> const& labels = program.getLabels();
                 
                 storm::models::AtomicPropositionsLabeling result(stateInformation.reachableStates.size(), labels.size() + 1);
                 
                 // Initialize labeling.
-                for (auto const& labelExpressionPair : labels) {
-                    result.addAtomicProposition(labelExpressionPair.first);
+                for (auto const& label : labels) {
+                    result.addAtomicProposition(label.getLabelName());
                 }
                 for (uint_fast64_t index = 0; index < stateInformation.reachableStates.size(); index++) {
-                    for (auto const& labelExpressionPair: labels) {
+                    for (auto const& label : labels) {
                         // Add label to state, if the corresponding expression is true.
-                        if (labelExpressionPair.second->getValueAsBool(stateInformation.reachableStates[index])) {
-                            result.addAtomicPropositionToState(labelExpressionPair.first, index);
+                        if (label.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates[index])) {
+                            result.addAtomicPropositionToState(label.getLabelName(), index);
                         }
                     }
                 }
                 
                 // Also label the initial state with the special label "init".
                 result.addAtomicProposition("init");
-                StateType* initialState = getInitialState(program, variableInformation);
-                uint_fast64_t initialIndex = stateInformation.stateToIndexMap.at(initialState);
-                result.addAtomicPropositionToState("init", initialIndex);
-                delete initialState;
+                for (auto const& index : stateInformation.initialStateIndices) {
+                    result.addAtomicPropositionToState("init", index);
+                }
                 
                 return result;
             }
@@ -749,8 +795,8 @@ namespace storm {
                     result[index] = ValueType(0);
                     for (auto const& reward : rewards) {
                         // Add this reward to the state if the state is included in the state reward.
-                        if (reward.getStatePredicate()->getValueAsBool(stateInformation.reachableStates[index])) {
-                            result[index] += ValueType(reward.getRewardValue()->getValueAsDouble(stateInformation.reachableStates[index]));
+                        if (reward.getStatePredicateExpression().evaluateAsBool(stateInformation.reachableStates[index])) {
+                            result[index] += ValueType(reward.getRewardValueExpression().evaluateAsDouble(stateInformation.reachableStates[index]));
                         }
                     }
                 }
diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h
index f95bc2806..da5d4a7ad 100644
--- a/src/counterexamples/SMTMinimalCommandSetGenerator.h
+++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h
@@ -25,7 +25,7 @@
 #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
 
 #include "src/utility/counterexamples.h"
-#include "src/utility/IRUtility.h"
+#include "src/utility/PrismUtility.h"
 
 namespace storm {
     namespace counterexamples {
diff --git a/src/storage/expressions/BaseExpression.cpp b/src/storage/expressions/BaseExpression.cpp
index f66cd7dc3..b9734a9ad 100644
--- a/src/storage/expressions/BaseExpression.cpp
+++ b/src/storage/expressions/BaseExpression.cpp
@@ -24,15 +24,15 @@ namespace storm {
             return this->getReturnType() == ExpressionReturnType::Bool;
         }
         
-        int_fast64_t BaseExpression::evaluateAsInt(Valuation const& evaluation) const {
+        int_fast64_t BaseExpression::evaluateAsInt(Valuation const* valuation) const {
             LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer.");
         }
         
-        bool BaseExpression::evaluateAsBool(Valuation const& evaluation) const {
+        bool BaseExpression::evaluateAsBool(Valuation const* valuation) const {
             LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean.");
         }
         
-        double BaseExpression::evaluateAsDouble(Valuation const& evaluation) const {
+        double BaseExpression::evaluateAsDouble(Valuation const* valuation) const {
             LOG_THROW(false, storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double.");
         }
         
diff --git a/src/storage/expressions/BaseExpression.h b/src/storage/expressions/BaseExpression.h
index 4039209d3..41684255d 100644
--- a/src/storage/expressions/BaseExpression.h
+++ b/src/storage/expressions/BaseExpression.h
@@ -48,7 +48,7 @@ namespace storm {
              * @param valuation The valuation of unknowns under which to evaluate the expression.
              * @return The boolean value of the expression under the given valuation.
              */
-            virtual bool evaluateAsBool(Valuation const& valuation) const;
+            virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const;
 
             /*!
              * Evaluates the expression under the valuation of unknowns (variables and constants) given by the
@@ -58,7 +58,7 @@ namespace storm {
              * @param valuation The valuation of unknowns under which to evaluate the expression.
              * @return The integer value of the expression under the given valuation.
              */
-            virtual int_fast64_t evaluateAsInt(Valuation const& valuation) const;
+            virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const;
             
             /*!
              * Evaluates the expression under the valuation of unknowns (variables and constants) given by the
@@ -68,7 +68,7 @@ namespace storm {
              * @param valuation The valuation of unknowns under which to evaluate the expression.
              * @return The double value of the expression under the given valuation.
              */
-            virtual double evaluateAsDouble(Valuation const& valuation) const;
+            virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const;
 
             /*!
              * Retrieves whether the expression is constant, i.e., contains no variables or undefined constants.
diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp
index 8cc30aa19..9f5e5edeb 100644
--- a/src/storage/expressions/BinaryBooleanFunctionExpression.cpp
+++ b/src/storage/expressions/BinaryBooleanFunctionExpression.cpp
@@ -13,7 +13,7 @@ namespace storm {
             return this->operatorType;
         }
         
-        bool BinaryBooleanFunctionExpression::evaluateAsBool(Valuation const& valuation) const {
+        bool BinaryBooleanFunctionExpression::evaluateAsBool(Valuation const* valuation) const {
             LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean.");
             
             bool firstOperandEvaluation = this->getFirstOperand()->evaluateAsBool(valuation);
diff --git a/src/storage/expressions/BinaryBooleanFunctionExpression.h b/src/storage/expressions/BinaryBooleanFunctionExpression.h
index b4f8ad0a6..32dfc387d 100644
--- a/src/storage/expressions/BinaryBooleanFunctionExpression.h
+++ b/src/storage/expressions/BinaryBooleanFunctionExpression.h
@@ -30,7 +30,7 @@ namespace storm {
             virtual ~BinaryBooleanFunctionExpression() = default;
             
             // Override base class methods.
-            virtual bool evaluateAsBool(Valuation const& valuation) const override;
+            virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual void accept(ExpressionVisitor* visitor) const override;
 
diff --git a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp
index 521e554bb..225bea963 100644
--- a/src/storage/expressions/BinaryNumericalFunctionExpression.cpp
+++ b/src/storage/expressions/BinaryNumericalFunctionExpression.cpp
@@ -14,7 +14,7 @@ namespace storm {
             return this->operatorType;
         }
         
-        int_fast64_t BinaryNumericalFunctionExpression::evaluateAsInt(Valuation const& valuation) const {
+        int_fast64_t BinaryNumericalFunctionExpression::evaluateAsInt(Valuation const* valuation) const {
             LOG_THROW(this->hasIntegralReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer.");
             
             int_fast64_t firstOperandEvaluation = this->getFirstOperand()->evaluateAsInt(valuation);
@@ -29,7 +29,7 @@ namespace storm {
             }
         }
         
-        double BinaryNumericalFunctionExpression::evaluateAsDouble(Valuation const& valuation) const {
+        double BinaryNumericalFunctionExpression::evaluateAsDouble(Valuation const* valuation) const {
             LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double.");
             
             double firstOperandEvaluation = this->getFirstOperand()->evaluateAsDouble(valuation);
diff --git a/src/storage/expressions/BinaryNumericalFunctionExpression.h b/src/storage/expressions/BinaryNumericalFunctionExpression.h
index 8d49e541a..174763c84 100644
--- a/src/storage/expressions/BinaryNumericalFunctionExpression.h
+++ b/src/storage/expressions/BinaryNumericalFunctionExpression.h
@@ -30,8 +30,8 @@ namespace storm {
             virtual ~BinaryNumericalFunctionExpression() = default;
             
             // Override base class methods.
-            virtual int_fast64_t evaluateAsInt(Valuation const& valuation) const override;
-            virtual double evaluateAsDouble(Valuation const& valuation) const override;
+            virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override;
+            virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual void accept(ExpressionVisitor* visitor) const override;
 
diff --git a/src/storage/expressions/BinaryRelationExpression.cpp b/src/storage/expressions/BinaryRelationExpression.cpp
index e23df77c4..1b00485b6 100644
--- a/src/storage/expressions/BinaryRelationExpression.cpp
+++ b/src/storage/expressions/BinaryRelationExpression.cpp
@@ -9,7 +9,7 @@ namespace storm {
             // Intentionally left empty.
         }
                 
-        bool BinaryRelationExpression::evaluateAsBool(Valuation const& valuation) const {
+        bool BinaryRelationExpression::evaluateAsBool(Valuation const* valuation) const {
             LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean.");
 
             double firstOperandEvaluated = this->getFirstOperand()->evaluateAsDouble(valuation);
diff --git a/src/storage/expressions/BinaryRelationExpression.h b/src/storage/expressions/BinaryRelationExpression.h
index 70201313c..7e3e177c5 100644
--- a/src/storage/expressions/BinaryRelationExpression.h
+++ b/src/storage/expressions/BinaryRelationExpression.h
@@ -30,7 +30,7 @@ namespace storm {
             virtual ~BinaryRelationExpression() = default;
             
             // Override base class methods.
-            virtual bool evaluateAsBool(Valuation const& valuation) const override;
+            virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual void accept(ExpressionVisitor* visitor) const override;
 
diff --git a/src/storage/expressions/BooleanConstantExpression.cpp b/src/storage/expressions/BooleanConstantExpression.cpp
index b3b453097..de87dab48 100644
--- a/src/storage/expressions/BooleanConstantExpression.cpp
+++ b/src/storage/expressions/BooleanConstantExpression.cpp
@@ -1,4 +1,5 @@
 #include "src/storage/expressions/BooleanConstantExpression.h"
+#include "src/exceptions/ExceptionMacros.h"
 
 namespace storm {
     namespace expressions {
@@ -6,8 +7,9 @@ namespace storm {
             // Intentionally left empty.
         }
                 
-        bool BooleanConstantExpression::evaluateAsBool(Valuation const& valuation) const {
-            return valuation.getBooleanValue(this->getConstantName());
+        bool BooleanConstantExpression::evaluateAsBool(Valuation const* valuation) const {
+            LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation.");
+            return valuation->getBooleanValue(this->getConstantName());
         }
         
         void BooleanConstantExpression::accept(ExpressionVisitor* visitor) const {
diff --git a/src/storage/expressions/BooleanConstantExpression.h b/src/storage/expressions/BooleanConstantExpression.h
index d239f146d..fc2e3f8e4 100644
--- a/src/storage/expressions/BooleanConstantExpression.h
+++ b/src/storage/expressions/BooleanConstantExpression.h
@@ -22,7 +22,7 @@ namespace storm {
             virtual ~BooleanConstantExpression() = default;
             
             // Override base class methods.
-            virtual bool evaluateAsBool(Valuation const& valuation) const override;
+            virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override;
             virtual void accept(ExpressionVisitor* visitor) const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
         };
diff --git a/src/storage/expressions/BooleanLiteralExpression.cpp b/src/storage/expressions/BooleanLiteralExpression.cpp
index 7fb01cec4..6ef15fe83 100644
--- a/src/storage/expressions/BooleanLiteralExpression.cpp
+++ b/src/storage/expressions/BooleanLiteralExpression.cpp
@@ -6,7 +6,7 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        bool BooleanLiteralExpression::evaluateAsBool(Valuation const& valuation) const {
+        bool BooleanLiteralExpression::evaluateAsBool(Valuation const* valuation) const {
             return this->getValue();
         }
         
diff --git a/src/storage/expressions/BooleanLiteralExpression.h b/src/storage/expressions/BooleanLiteralExpression.h
index 1c7baed09..49794b59a 100644
--- a/src/storage/expressions/BooleanLiteralExpression.h
+++ b/src/storage/expressions/BooleanLiteralExpression.h
@@ -22,7 +22,7 @@ namespace storm {
             virtual ~BooleanLiteralExpression() = default;
 
             // Override base class methods.
-            virtual bool evaluateAsBool(Valuation const& valuation) const override;
+            virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override;
             virtual bool isConstant() const override;
             virtual bool isTrue() const override;
             virtual bool isFalse() const override;
diff --git a/src/storage/expressions/DoubleConstantExpression.cpp b/src/storage/expressions/DoubleConstantExpression.cpp
index d0f5a2799..e7d541975 100644
--- a/src/storage/expressions/DoubleConstantExpression.cpp
+++ b/src/storage/expressions/DoubleConstantExpression.cpp
@@ -1,4 +1,5 @@
 #include "src/storage/expressions/DoubleConstantExpression.h"
+#include "src/exceptions/ExceptionMacros.h"
 
 namespace storm {
     namespace expressions {
@@ -6,8 +7,9 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        double DoubleConstantExpression::evaluateAsDouble(Valuation const& valuation) const {
-            return valuation.getDoubleValue(this->getConstantName());
+        double DoubleConstantExpression::evaluateAsDouble(Valuation const* valuation) const {
+            LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation.");
+            return valuation->getDoubleValue(this->getConstantName());
         }
         
         std::shared_ptr<BaseExpression const> DoubleConstantExpression::simplify() const {
diff --git a/src/storage/expressions/DoubleConstantExpression.h b/src/storage/expressions/DoubleConstantExpression.h
index 349de5216..673ef007b 100644
--- a/src/storage/expressions/DoubleConstantExpression.h
+++ b/src/storage/expressions/DoubleConstantExpression.h
@@ -22,7 +22,7 @@ namespace storm {
             virtual ~DoubleConstantExpression() = default;
             
             // Override base class methods.
-            virtual double evaluateAsDouble(Valuation const& valuation) const override;
+            virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
             virtual void accept(ExpressionVisitor* visitor) const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
         };
diff --git a/src/storage/expressions/DoubleLiteralExpression.cpp b/src/storage/expressions/DoubleLiteralExpression.cpp
index 176823803..642a1817f 100644
--- a/src/storage/expressions/DoubleLiteralExpression.cpp
+++ b/src/storage/expressions/DoubleLiteralExpression.cpp
@@ -6,7 +6,7 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        double DoubleLiteralExpression::evaluateAsDouble(Valuation const& valuation) const {
+        double DoubleLiteralExpression::evaluateAsDouble(Valuation const* valuation) const {
             return this->getValue();
         }
         
diff --git a/src/storage/expressions/DoubleLiteralExpression.h b/src/storage/expressions/DoubleLiteralExpression.h
index 5d97e6b59..1ed293923 100644
--- a/src/storage/expressions/DoubleLiteralExpression.h
+++ b/src/storage/expressions/DoubleLiteralExpression.h
@@ -22,7 +22,7 @@ namespace storm {
             virtual ~DoubleLiteralExpression() = default;
             
             // Override base class methods.
-            virtual double evaluateAsDouble(Valuation const& valuation) const override;
+            virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
             virtual bool isConstant() const override;
             virtual std::set<std::string> getVariables() const override;
             virtual std::set<std::string> getConstants() const override;
diff --git a/src/storage/expressions/Expression.cpp b/src/storage/expressions/Expression.cpp
index 7da4f8b37..7eb94966b 100644
--- a/src/storage/expressions/Expression.cpp
+++ b/src/storage/expressions/Expression.cpp
@@ -37,15 +37,15 @@ namespace storm {
             return IdentifierSubstitutionVisitor<MapType>(identifierToIdentifierMap).substitute(this->getBaseExpressionPointer().get());
         }
         
-        bool Expression::evaluateAsBool(Valuation const& valuation) const {
+        bool Expression::evaluateAsBool(Valuation const* valuation) const {
             return this->getBaseExpression().evaluateAsBool(valuation);
         }
         
-        int_fast64_t Expression::evaluateAsInt(Valuation const& valuation) const {
+        int_fast64_t Expression::evaluateAsInt(Valuation const* valuation) const {
             return this->getBaseExpression().evaluateAsInt(valuation);
         }
         
-        double Expression::evaluateAsDouble(Valuation const& valuation) const {
+        double Expression::evaluateAsDouble(Valuation const* valuation) const {
             return this->getBaseExpression().evaluateAsDouble(valuation);
         }
         
diff --git a/src/storage/expressions/Expression.h b/src/storage/expressions/Expression.h
index 96f8ce6fd..2253c0548 100644
--- a/src/storage/expressions/Expression.h
+++ b/src/storage/expressions/Expression.h
@@ -94,7 +94,7 @@ namespace storm {
              * @param valuation The valuation of unknowns under which to evaluate the expression.
              * @return The boolean value of the expression under the given valuation.
              */
-            bool evaluateAsBool(Valuation const& valuation) const;
+            bool evaluateAsBool(Valuation const* valuation = nullptr) const;
             
             /*!
              * Evaluates the expression under the valuation of unknowns (variables and constants) given by the
@@ -104,7 +104,7 @@ namespace storm {
              * @param valuation The valuation of unknowns under which to evaluate the expression.
              * @return The integer value of the expression under the given valuation.
              */
-            int_fast64_t evaluateAsInt(Valuation const& valuation) const;
+            int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const;
             
             /*!
              * Evaluates the expression under the valuation of unknowns (variables and constants) given by the
@@ -114,7 +114,7 @@ namespace storm {
              * @param valuation The valuation of unknowns under which to evaluate the expression.
              * @return The double value of the expression under the given valuation.
              */
-            double evaluateAsDouble(Valuation const& valuation) const;
+            double evaluateAsDouble(Valuation const* valuation = nullptr) const;
             
             /*!
              * Simplifies the expression according to some basic rules.
diff --git a/src/storage/expressions/IfThenElseExpression.cpp b/src/storage/expressions/IfThenElseExpression.cpp
index dffee088d..81ebca670 100644
--- a/src/storage/expressions/IfThenElseExpression.cpp
+++ b/src/storage/expressions/IfThenElseExpression.cpp
@@ -6,7 +6,7 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        bool IfThenElseExpression::evaluateAsBool(Valuation const& valuation) const {
+        bool IfThenElseExpression::evaluateAsBool(Valuation const* valuation) const {
             bool conditionValue = this->condition->evaluateAsBool(valuation);
             if (conditionValue) {
                 return this->thenExpression->evaluateAsBool(valuation);
@@ -15,7 +15,7 @@ namespace storm {
             }
         }
         
-        int_fast64_t IfThenElseExpression::evaluateAsInt(Valuation const& valuation) const {
+        int_fast64_t IfThenElseExpression::evaluateAsInt(Valuation const* valuation) const {
             bool conditionValue = this->condition->evaluateAsBool(valuation);
             if (conditionValue) {
                 return this->thenExpression->evaluateAsInt(valuation);
@@ -24,7 +24,7 @@ namespace storm {
             }
         }
         
-        double IfThenElseExpression::evaluateAsDouble(Valuation const& valuation) const {
+        double IfThenElseExpression::evaluateAsDouble(Valuation const* valuation) const {
             bool conditionValue = this->condition->evaluateAsBool(valuation);
             if (conditionValue) {
                 return this->thenExpression->evaluateAsDouble(valuation);
diff --git a/src/storage/expressions/IfThenElseExpression.h b/src/storage/expressions/IfThenElseExpression.h
index 794a75bee..1f8e2db41 100644
--- a/src/storage/expressions/IfThenElseExpression.h
+++ b/src/storage/expressions/IfThenElseExpression.h
@@ -24,9 +24,9 @@ namespace storm {
             virtual ~IfThenElseExpression() = default;
             
             // Override base class methods.
-            virtual bool evaluateAsBool(Valuation const& valuation) const override;
-            virtual int_fast64_t evaluateAsInt(Valuation const& valuation) const override;
-            virtual double evaluateAsDouble(Valuation const& valuation) const override;
+            virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override;
+            virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override;
+            virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
             virtual bool isConstant() const override;
             virtual std::set<std::string> getVariables() const override;
             virtual std::set<std::string> getConstants() const override;
diff --git a/src/storage/expressions/IntegerConstantExpression.cpp b/src/storage/expressions/IntegerConstantExpression.cpp
index 92bedebc9..60ad8de89 100644
--- a/src/storage/expressions/IntegerConstantExpression.cpp
+++ b/src/storage/expressions/IntegerConstantExpression.cpp
@@ -1,4 +1,5 @@
 #include "src/storage/expressions/IntegerConstantExpression.h"
+#include "src/exceptions/ExceptionMacros.h"
 
 namespace storm {
     namespace expressions {
@@ -6,12 +7,13 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        int_fast64_t IntegerConstantExpression::evaluateAsInt(Valuation const& valuation) const {
-            return valuation.getIntegerValue(this->getConstantName());
+        int_fast64_t IntegerConstantExpression::evaluateAsInt(Valuation const* valuation) const {
+            LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation.");
+            return valuation->getIntegerValue(this->getConstantName());
         }
         
-        double IntegerConstantExpression::evaluateAsDouble(Valuation const& valuation) const {
-            return static_cast<double>(valuation.getIntegerValue(this->getConstantName()));
+        double IntegerConstantExpression::evaluateAsDouble(Valuation const* valuation) const {
+            return static_cast<double>(this->evaluateAsInt(valuation));
         }
         
         std::shared_ptr<BaseExpression const> IntegerConstantExpression::simplify() const {
diff --git a/src/storage/expressions/IntegerConstantExpression.h b/src/storage/expressions/IntegerConstantExpression.h
index 05deaf49c..6a808b215 100644
--- a/src/storage/expressions/IntegerConstantExpression.h
+++ b/src/storage/expressions/IntegerConstantExpression.h
@@ -22,8 +22,8 @@ namespace storm {
             virtual ~IntegerConstantExpression() = default;
             
             // Override base class methods.
-            virtual int_fast64_t evaluateAsInt(Valuation const& valuation) const override;
-            virtual double evaluateAsDouble(Valuation const& valuation) const override;
+            virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override;
+            virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual void accept(ExpressionVisitor* visitor) const;
         };
diff --git a/src/storage/expressions/IntegerLiteralExpression.cpp b/src/storage/expressions/IntegerLiteralExpression.cpp
index 16adeadc6..5e6404fc8 100644
--- a/src/storage/expressions/IntegerLiteralExpression.cpp
+++ b/src/storage/expressions/IntegerLiteralExpression.cpp
@@ -6,12 +6,12 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        int_fast64_t IntegerLiteralExpression::evaluateAsInt(Valuation const& valuation) const {
+        int_fast64_t IntegerLiteralExpression::evaluateAsInt(Valuation const* valuation) const {
             return this->getValue();
         }
         
-        double IntegerLiteralExpression::evaluateAsDouble(Valuation const& valuation) const {
-            return static_cast<double>(this->getValue());
+        double IntegerLiteralExpression::evaluateAsDouble(Valuation const* valuation) const {
+            return static_cast<double>(this->evaluateAsInt(valuation));
         }
         
         bool IntegerLiteralExpression::isConstant() const {
diff --git a/src/storage/expressions/IntegerLiteralExpression.h b/src/storage/expressions/IntegerLiteralExpression.h
index 1b71ea306..6cbce6e17 100644
--- a/src/storage/expressions/IntegerLiteralExpression.h
+++ b/src/storage/expressions/IntegerLiteralExpression.h
@@ -22,8 +22,8 @@ namespace storm {
             virtual ~IntegerLiteralExpression() = default;
             
             // Override base class methods.
-            virtual int_fast64_t evaluateAsInt(Valuation const& valuation) const override;
-            virtual double evaluateAsDouble(Valuation const& valuation) const override;
+            virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override;
+            virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
             virtual bool isConstant() const override;
             virtual std::set<std::string> getVariables() const override;
             virtual std::set<std::string> getConstants() const override;
diff --git a/src/storage/expressions/SimpleValuation.h b/src/storage/expressions/SimpleValuation.h
index 0c2231a63..16719be00 100644
--- a/src/storage/expressions/SimpleValuation.h
+++ b/src/storage/expressions/SimpleValuation.h
@@ -37,7 +37,6 @@ namespace storm {
             SimpleValuation(std::shared_ptr<std::unordered_map<std::string, uint_fast64_t>> identifierToIndexMap, std::vector<bool> booleanValues, std::vector<int_fast64_t> integerValues, std::vector<double> doubleValues);
 
             // Instantiate some constructors and assignments with their default implementations.
-            SimpleValuation() = default;
             SimpleValuation(SimpleValuation const&) = default;
             SimpleValuation(SimpleValuation&&) = default;
             SimpleValuation& operator=(SimpleValuation const&) = default;
diff --git a/src/storage/expressions/UnaryBooleanFunctionExpression.cpp b/src/storage/expressions/UnaryBooleanFunctionExpression.cpp
index 0b12b5bf6..7e405bb29 100644
--- a/src/storage/expressions/UnaryBooleanFunctionExpression.cpp
+++ b/src/storage/expressions/UnaryBooleanFunctionExpression.cpp
@@ -13,7 +13,7 @@ namespace storm {
             return this->operatorType;
         }
         
-        bool UnaryBooleanFunctionExpression::evaluateAsBool(Valuation const& valuation) const {
+        bool UnaryBooleanFunctionExpression::evaluateAsBool(Valuation const* valuation) const {
             LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as boolean.");
 
             bool operandEvaluated = this->getOperand()->evaluateAsBool(valuation);
diff --git a/src/storage/expressions/UnaryBooleanFunctionExpression.h b/src/storage/expressions/UnaryBooleanFunctionExpression.h
index fefbded86..954d3659d 100644
--- a/src/storage/expressions/UnaryBooleanFunctionExpression.h
+++ b/src/storage/expressions/UnaryBooleanFunctionExpression.h
@@ -29,7 +29,7 @@ namespace storm {
             virtual ~UnaryBooleanFunctionExpression() = default;
             
             // Override base class methods.
-            virtual bool evaluateAsBool(Valuation const& valuation) const override;
+            virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual void accept(ExpressionVisitor* visitor) const override;
 
diff --git a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp
index 31f9aeb1e..02a4bee30 100644
--- a/src/storage/expressions/UnaryNumericalFunctionExpression.cpp
+++ b/src/storage/expressions/UnaryNumericalFunctionExpression.cpp
@@ -14,7 +14,7 @@ namespace storm {
             return this->operatorType;
         }
         
-        int_fast64_t UnaryNumericalFunctionExpression::evaluateAsInt(Valuation const& valuation) const {
+        int_fast64_t UnaryNumericalFunctionExpression::evaluateAsInt(Valuation const* valuation) const {
             LOG_THROW(this->hasIntegralReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as integer.");
 
             int_fast64_t operandEvaluated = this->getOperand()->evaluateAsInt(valuation);
@@ -25,7 +25,7 @@ namespace storm {
             }
         }
         
-        double UnaryNumericalFunctionExpression::evaluateAsDouble(Valuation const& valuation) const {
+        double UnaryNumericalFunctionExpression::evaluateAsDouble(Valuation const* valuation) const {
             LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Unable to evaluate expression as double.");
 
             double operandEvaluated = this->getOperand()->evaluateAsDouble(valuation);
diff --git a/src/storage/expressions/UnaryNumericalFunctionExpression.h b/src/storage/expressions/UnaryNumericalFunctionExpression.h
index 2f50549ef..be717e564 100644
--- a/src/storage/expressions/UnaryNumericalFunctionExpression.h
+++ b/src/storage/expressions/UnaryNumericalFunctionExpression.h
@@ -29,8 +29,8 @@ namespace storm {
             virtual ~UnaryNumericalFunctionExpression() = default;
             
             // Override base class methods.
-            virtual int_fast64_t evaluateAsInt(Valuation const& valuation) const override;
-            virtual double evaluateAsDouble(Valuation const& valuation) const override;
+            virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override;
+            virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
             virtual void accept(ExpressionVisitor* visitor) const override;
      
diff --git a/src/storage/expressions/VariableExpression.cpp b/src/storage/expressions/VariableExpression.cpp
index b7a6ce6d2..d7765f14a 100644
--- a/src/storage/expressions/VariableExpression.cpp
+++ b/src/storage/expressions/VariableExpression.cpp
@@ -12,27 +12,33 @@ namespace storm {
             return this->variableName;
         }
         
-        bool VariableExpression::evaluateAsBool(Valuation const& evaluation) const {
+        bool VariableExpression::evaluateAsBool(Valuation const* valuation) const {
+            LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation.");
             LOG_THROW(this->hasBooleanReturnType(), storm::exceptions::InvalidTypeException, "Cannot evaluate expression as boolean: return type is not a boolean.");
             
-            return evaluation.getBooleanValue(this->getVariableName());
+            return valuation->getBooleanValue(this->getVariableName());
         }
 
-        int_fast64_t VariableExpression::evaluateAsInt(Valuation const& evaluation) const {
+        int_fast64_t VariableExpression::evaluateAsInt(Valuation const* valuation) const {
+            LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation.");
             LOG_THROW(this->hasIntegralReturnType(), storm::exceptions::InvalidTypeException, "Cannot evaluate expression as integer: return type is not an integer.");
             
-            return evaluation.getIntegerValue(this->getVariableName());
+            return valuation->getIntegerValue(this->getVariableName());
         }
         
-        double VariableExpression::evaluateAsDouble(Valuation const& evaluation) const {
+        double VariableExpression::evaluateAsDouble(Valuation const* valuation) const {
+            LOG_ASSERT(valuation != nullptr, "Evaluating expressions with unknowns without valuation.");
             LOG_THROW(this->hasNumericalReturnType(), storm::exceptions::InvalidTypeException, "Cannot evaluate expression as double: return type is not a double.");
             
             switch (this->getReturnType()) {
-                case ExpressionReturnType::Int: return static_cast<double>(evaluation.getIntegerValue(this->getVariableName())); break;
-                case ExpressionReturnType::Double: evaluation.getDoubleValue(this->getVariableName()); break;
+                case ExpressionReturnType::Int: return static_cast<double>(valuation->getIntegerValue(this->getVariableName())); break;
+                case ExpressionReturnType::Double: valuation->getDoubleValue(this->getVariableName()); break;
                 default: break;
             }
-            LOG_THROW(false, storm::exceptions::InvalidTypeException, "Type of variable is required to be numeric.");
+            LOG_ASSERT(false, "Type of variable is required to be numeric.");
+            
+            // Silence warning. This point can never be reached.
+            return 0;
         }
         
         std::set<std::string> VariableExpression::getVariables() const {
diff --git a/src/storage/expressions/VariableExpression.h b/src/storage/expressions/VariableExpression.h
index 7e4732eda..1b86274a9 100644
--- a/src/storage/expressions/VariableExpression.h
+++ b/src/storage/expressions/VariableExpression.h
@@ -23,9 +23,9 @@ namespace storm {
             virtual ~VariableExpression() = default;
 
             // Override base class methods.
-            virtual bool evaluateAsBool(Valuation const& valuation) const override;
-            virtual int_fast64_t evaluateAsInt(Valuation const& valuation) const override;
-            virtual double evaluateAsDouble(Valuation const& valuation) const override;
+            virtual bool evaluateAsBool(Valuation const* valuation = nullptr) const override;
+            virtual int_fast64_t evaluateAsInt(Valuation const* valuation = nullptr) const override;
+            virtual double evaluateAsDouble(Valuation const* valuation = nullptr) const override;
             virtual std::set<std::string> getVariables() const override;
             virtual std::set<std::string> getConstants() const override;
             virtual std::shared_ptr<BaseExpression const> simplify() const override;
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index c635cbf63..49ebd7724 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -19,7 +19,7 @@ namespace storm {
                     return true;
                 }
             }
-            return true;
+            return false;
         }
         
         bool Program::hasConstant(std::string const& constantName) const {
@@ -255,46 +255,58 @@ namespace storm {
                 LOG_THROW(definedUndefinedConstants.find(constantExpressionPair.first) != definedUndefinedConstants.end(), storm::exceptions::InvalidArgumentException, "Unable to define non-existant constant.");
             }
             
+            return Program(this->getModelType(), newConstants, this->getGlobalBooleanVariables(), this->getGlobalIntegerVariables(), this->getFormulas(), this->getModules(), this->getRewardModels(), this->definesInitialStatesExpression(), this->getInitialStatesExpression(), this->getLabels());
+        }
+        
+        Program Program::substituteConstants() const {
+            // We start by creating the appropriate substitution
+            std::map<std::string, storm::expressions::Expression> constantSubstitution;
+            for (auto const& constant : this->getConstants()) {
+                LOG_THROW(constant.isDefined(), storm::exceptions::InvalidArgumentException, "Cannot substitute constants in program that contains undefined constants.");
+                
+                constantSubstitution.emplace(constant.getConstantName(), constant.getExpression());
+            }
+            
             // Now we can substitute the constants in all expressions appearing in the program.
             std::vector<BooleanVariable> newBooleanVariables;
             newBooleanVariables.reserve(this->getNumberOfGlobalBooleanVariables());
             for (auto const& booleanVariable : this->getGlobalBooleanVariables()) {
-                newBooleanVariables.emplace_back(booleanVariable.substitute(constantDefinitions));
+                newBooleanVariables.emplace_back(booleanVariable.substitute(constantSubstitution));
             }
             
             std::vector<IntegerVariable> newIntegerVariables;
             newBooleanVariables.reserve(this->getNumberOfGlobalIntegerVariables());
             for (auto const& integerVariable : this->getGlobalIntegerVariables()) {
-                newIntegerVariables.emplace_back(integerVariable.substitute(constantDefinitions));
+                newIntegerVariables.emplace_back(integerVariable.substitute(constantSubstitution));
             }
-        
+            
             std::vector<Formula> newFormulas;
             newFormulas.reserve(this->getNumberOfFormulas());
             for (auto const& formula : this->getFormulas()) {
-                newFormulas.emplace_back(formula.substitute(constantDefinitions));
+                newFormulas.emplace_back(formula.substitute(constantSubstitution));
             }
-
+            
             std::vector<Module> newModules;
             newModules.reserve(this->getNumberOfModules());
             for (auto const& module : this->getModules()) {
-                newModules.emplace_back(module.substitute(constantDefinitions));
+                newModules.emplace_back(module.substitute(constantSubstitution));
             }
             
             std::vector<RewardModel> newRewardModels;
             newRewardModels.reserve(this->getNumberOfRewardModels());
             for (auto const& rewardModel : this->getRewardModels()) {
-                newRewardModels.emplace_back(rewardModel.substitute(constantDefinitions));
+                newRewardModels.emplace_back(rewardModel.substitute(constantSubstitution));
             }
             
-            storm::expressions::Expression newInitialStateExpression = this->getInitialStatesExpression().substitute<std::map>(constantDefinitions);
+            storm::expressions::Expression newInitialStateExpression = this->getInitialStatesExpression().substitute<std::map>(constantSubstitution);
             
             std::vector<Label> newLabels;
             newLabels.reserve(this->getNumberOfLabels());
             for (auto const& label : this->getLabels()) {
-                newLabels.emplace_back(label.substitute(constantDefinitions));
+                newLabels.emplace_back(label.substitute(constantSubstitution));
             }
             
-            return Program(this->getModelType(), newConstants, newBooleanVariables, newIntegerVariables, newFormulas, newModules, newRewardModels, this->definesInitialStatesExpression(), newInitialStateExpression, newLabels);
+            return Program(this->getModelType(), std::vector<Constant>(), newBooleanVariables, newIntegerVariables, newFormulas, newModules, newRewardModels, this->definesInitialStatesExpression(), newInitialStateExpression, newLabels);
         }
         
         std::ostream& operator<<(std::ostream& stream, Program const& program) {
diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h
index 2c2e17b6f..6f4c5e3b1 100644
--- a/src/storage/prism/Program.h
+++ b/src/storage/prism/Program.h
@@ -274,6 +274,14 @@ namespace storm {
              */
             Program defineUndefinedConstants(std::map<std::string, storm::expressions::Expression> const& constantDefinitions) const;
             
+            /*!
+             * Substitutes all constants appearing in the expressions of the program by their defining expressions. For
+             * this to work, all constants need to be defined prior to calling this.
+             *
+             * @return The resulting program that only contains expressions over variables of the program.
+             */
+            Program substituteConstants() const;
+            
             friend std::ostream& operator<<(std::ostream& stream, Program const& program);
             
         private:
diff --git a/src/storm.cpp b/src/storm.cpp
index 16fa59806..c7b40247a 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -34,7 +34,7 @@
 #include "src/solver/GmmxxNondeterministicLinearEquationSolver.h"
 #include "src/solver/GurobiLpSolver.h"
 #include "src/counterexamples/MILPMinimalLabelSetGenerator.h"
-#include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
+// #include "src/counterexamples/SMTMinimalCommandSetGenerator.h"
 #include "src/counterexamples/PathBasedSubsystemGenerator.h"
 #include "src/parser/AutoParser.h"
 #include "src/parser/MarkovAutomatonParser.h"
@@ -58,7 +58,7 @@ log4cplus::Logger logger;
 
 #include "src/parser/PrismParser.h"
 #include "src/adapters/ExplicitModelAdapter.h"
-#include "src/adapters/SymbolicModelAdapter.h"
+// #include "src/adapters/SymbolicModelAdapter.h"
 
 #include "src/exceptions/InvalidSettingsException.h"
 
@@ -534,7 +534,7 @@ int main(const int argc, const char* argv[]) {
             // First, we build the model using the given symbolic model description and constant definitions.
             std::string const& programFile = s->getOptionByLongName("symbolic").getArgument(0).getValueAsString();
             std::string const& constants = s->getOptionByLongName("constants").getArgument(0).getValueAsString();
-            storm::ir::Program program = storm::parser::PrismParserFromFile(programFile);
+            storm::prism::Program program = storm::parser::PrismParser::parse(programFile);
             std::shared_ptr<storm::models::AbstractModel<double>> model = storm::adapters::ExplicitModelAdapter<double>::translateProgram(program, constants);
             model->printModelInformationToStream(std::cout);
             
@@ -558,7 +558,7 @@ int main(const int argc, const char* argv[]) {
                     if (useMILP) {
                         storm::counterexamples::MILPMinimalLabelSetGenerator<double>::computeCounterexample(program, *mdp, formulaPtr);
                     } else {
-                        storm::counterexamples::SMTMinimalCommandSetGenerator<double>::computeCounterexample(program, constants, *mdp, formulaPtr);
+                        // storm::counterexamples::SMTMinimalCommandSetGenerator<double>::computeCounterexample(program, constants, *mdp, formulaPtr);
                     }
                     
                     // Once we are done with the formula, delete it.
diff --git a/src/utility/IRUtility.h b/src/utility/IRUtility.h
deleted file mode 100644
index 7efe08bbe..000000000
--- a/src/utility/IRUtility.h
+++ /dev/null
@@ -1,517 +0,0 @@
-/*
- * IRUtility.h
- *
- *  Created on: 05.10.2013
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_UTILITY_IRUTILITY_H_
-#define STORM_UTILITY_IRUTILITY_H_
-
-#include <boost/algorithm/string.hpp>
-
-#include "src/storage/LabeledValues.h"
-#include "src/storage/prism/Program.h"
-#include "src/exceptions/InvalidArgumentException.h"
-
-#include "log4cplus/logger.h"
-#include "log4cplus/loggingmacros.h"
-
-extern log4cplus::Logger logger;
-
-namespace storm {
-    namespace utility {
-        namespace ir {
-
-            /*!
-             * A state of the model, i.e. a valuation of all variables.
-             */
-            typedef std::pair<std::vector<bool>, std::vector<int_fast64_t>> StateType;
-            
-            /*!
-             * A helper class that provides the functionality to compute a hash value for states of the model.
-             */
-            class StateHash {
-            public:
-                std::size_t operator()(StateType* state) const {
-                    size_t seed = 0;
-                    for (auto it : state->first) {
-                        boost::hash_combine<bool>(seed, it);
-                    }
-                    for (auto it : state->second) {
-                        boost::hash_combine<int_fast64_t>(seed, it);
-                    }
-                    return seed;
-                }
-            };
-            
-            /*!
-             * A helper class that provides the functionality to compare states of the model wrt. equality.
-             */
-            class StateCompare {
-            public:
-                bool operator()(StateType* state1, StateType* state2) const {
-                    return *state1 == *state2;
-                }
-            };
-            
-            /*!
-             * A helper class that provides the functionality to compare states of the model wrt. the relation "<".
-             */
-            class StateLess {
-            public:
-                bool operator()(StateType* state1, StateType* state2) const {
-                    // Compare boolean variables.
-                    for (uint_fast64_t i = 0; i < state1->first.size(); ++i) {
-                        if (!state1->first.at(i) && state2->first.at(i)) {
-                            return true;
-                        }
-                    }
-                    // Then compare integer variables.
-                    for (uint_fast64_t i = 0; i < state1->second.size(); ++i) {
-                        if (!state1->second.at(i) && state2->second.at(i)) {
-                            return true;
-                        }
-                    }
-                    return false;
-                }
-            };
-            
-            // A structure holding information about a particular choice.
-            template<typename ValueType, typename KeyType=uint_fast64_t, typename Compare=std::less<uint_fast64_t>>
-            struct Choice {
-            public:
-                Choice(std::string const& actionLabel) : distribution(), actionLabel(actionLabel), choiceLabels() {
-                    // Intentionally left empty.
-                }
-                
-                /*!
-                 * Returns an iterator to the first element of this choice.
-                 *
-                 * @return An iterator to the first element of this choice.
-                 */
-                typename std::map<KeyType, ValueType>::iterator begin() {
-                    return distribution.begin();
-                }
-                
-                /*!
-                 * Returns an iterator to the first element of this choice.
-                 *
-                 * @return An iterator to the first element of this choice.
-                 */
-                typename std::map<KeyType, ValueType>::const_iterator begin() const {
-                    return distribution.cbegin();
-                }
-                
-                /*!
-                 * Returns an iterator that points past the elements of this choice.
-                 *
-                 * @return An iterator that points past the elements of this choice.
-                 */
-                typename std::map<KeyType, ValueType>::iterator end() {
-                    return distribution.end();
-                }
-                
-                /*!
-                 * Returns an iterator that points past the elements of this choice.
-                 *
-                 * @return An iterator that points past the elements of this choice.
-                 */
-                typename std::map<KeyType, ValueType>::const_iterator end() const {
-                    return distribution.cend();
-                }
-                
-                /*!
-                 * Returns an iterator to the element with the given key, if there is one. Otherwise, the iterator points to
-                 * distribution.end().
-                 *
-                 * @param value The value to find.
-                 * @return An iterator to the element with the given key, if there is one.
-                 */
-                typename std::map<KeyType, ValueType>::iterator find(uint_fast64_t value) {
-                    return distribution.find(value);
-                }
-                
-                /*!
-                 * Inserts the contents of this object to the given output stream.
-                 *
-                 * @param out The stream in which to insert the contents.
-                 */
-                friend std::ostream& operator<<(std::ostream& out, Choice<ValueType> const& choice) {
-                    out << "<";
-                    for (auto const& stateProbabilityPair : choice.distribution) {
-                        out << stateProbabilityPair.first << " : " << stateProbabilityPair.second << ", ";
-                    }
-                    out << ">";
-                    return out;
-                }
-                
-                /*!
-                 * Adds the given label to the labels associated with this choice.
-                 *
-                 * @param label The label to associate with this choice.
-                 */
-                void addChoiceLabel(uint_fast64_t label) {
-                    choiceLabels.insert(label);
-                }
-                
-                /*!
-                 * Adds the given label set to the labels associated with this choice.
-                 *
-                 * @param labelSet The label set to associate with this choice.
-                 */
-                void addChoiceLabels(boost::container::flat_set<uint_fast64_t> const& labelSet) {
-                    for (uint_fast64_t label : labelSet) {
-                        addChoiceLabel(label);
-                    }
-                }
-                
-                /*!
-                 * Retrieves the set of labels associated with this choice.
-                 *
-                 * @return The set of labels associated with this choice.
-                 */
-                boost::container::flat_set<uint_fast64_t> const& getChoiceLabels() const {
-                    return choiceLabels;
-                }
-                
-                /*!
-                 * Retrieves the action label of this choice.
-                 *
-                 * @return The action label of this choice.
-                 */
-                std::string const& getActionLabel() const {
-                    return actionLabel;
-                }
-                
-                /*!
-                 * Retrieves the entry in the choice that is associated with the given state and creates one if none exists,
-                 * yet.
-                 *
-                 * @param state The state for which to add the entry.
-                 * @return A reference to the entry that is associated with the given state.
-                 */
-                ValueType& getOrAddEntry(uint_fast64_t state) {
-                    auto stateProbabilityPair = distribution.find(state);
-                    
-                    if (stateProbabilityPair == distribution.end()) {
-                        distribution[state] = ValueType();
-                    }
-                    return distribution.at(state);
-                }
-                
-                /*!
-                 * Retrieves the entry in the choice that is associated with the given state and creates one if none exists,
-                 * yet.
-                 *
-                 * @param state The state for which to add the entry.
-                 * @return A reference to the entry that is associated with the given state.
-                 */
-                ValueType const& getOrAddEntry(uint_fast64_t state) const {
-                    auto stateProbabilityPair = distribution.find(state);
-                    
-                    if (stateProbabilityPair == distribution.end()) {
-                        distribution[state] = ValueType();
-                    }
-                    return distribution.at(state);
-                }
-                
-            private:
-                // The distribution that is associated with the choice.
-                std::map<KeyType, ValueType, Compare> distribution;
-                
-                // The label of the choice.
-                std::string actionLabel;
-                
-                // The labels that are associated with this choice.
-                boost::container::flat_set<uint_fast64_t> choiceLabels;
-            };
-            
-            /*!
-             * Adds the target state and probability to the given choice and ignores the labels. This function overloads with
-             * other functions to ensure the proper treatment of labels.
-             *
-             * @param choice The choice to which to add the target state and probability.
-             * @param state The target state of the probability.
-             * @param probability The probability to reach the target state in one step.
-             * @param labels A set of labels that is supposed to be associated with this state and probability. NOTE: this
-             * is ignored by this particular function but not by the overloaded functions.
-             */
-            template<typename ValueType>
-            void addProbabilityToChoice(Choice<ValueType>& choice, uint_fast64_t state, ValueType probability, boost::container::flat_set<uint_fast64_t> const& labels) {
-                choice.getOrAddEntry(state) += probability;
-            }
-            
-            /*!
-             * Adds the target state and probability to the given choice and labels it accordingly. This function overloads
-             * with other functions to ensure the proper treatment of labels.
-             *
-             * @param choice The choice to which to add the target state and probability.
-             * @param state The target state of the probability.
-             * @param probability The probability to reach the target state in one step.
-             * @param labels A set of labels that is supposed to be associated with this state and probability.
-             */
-            template<typename ValueType>
-            void addProbabilityToChoice(Choice<storm::storage::LabeledValues<ValueType>>& choice, uint_fast64_t state, ValueType probability, boost::container::flat_set<uint_fast64_t> const& labels) {
-                auto& labeledEntry = choice.getOrAddEntry(state);
-                labeledEntry.addValue(probability, labels);
-            }
-            
-            // A structure storing information about the used variables of the program.
-            struct VariableInformation {
-                VariableInformation() : booleanVariables(), booleanVariableToIndexMap(), integerVariables(), integerVariableToIndexMap() {
-                    // Intentinally left empty.
-                }
-                
-                // List of all boolean variables.
-                std::vector<storm::ir::BooleanVariable> booleanVariables;
-                
-                // A mapping of boolean variable names to their indices.
-                std::map<std::string, uint_fast64_t> booleanVariableToIndexMap;
-                                
-                // List of all integer variables.
-                std::vector<storm::ir::IntegerVariable> integerVariables;
-                
-                // List of all lower bounds for integer variables.
-                std::vector<int_fast64_t> lowerBounds;
-                
-                // List of all upper bounds for integer variables.
-                std::vector<int_fast64_t> upperBounds;
-                
-                // A mapping of integer variable names to their indices.
-                std::map<std::string, uint_fast64_t> integerVariableToIndexMap;
-            };
-
-            /*!
-             * Aggregates information about the variables in the program.
-             *
-             * @param program The program whose variables to aggregate.
-             * @return A structure containing information about the variables in the program.
-             */
-            static VariableInformation createVariableInformation(storm::ir::Program const& program) {
-                VariableInformation result;
-                
-                uint_fast64_t numberOfIntegerVariables = 0;
-                uint_fast64_t numberOfBooleanVariables = 0;
-                
-                // Count number of variables.
-                numberOfBooleanVariables += program.getNumberOfGlobalBooleanVariables();
-                numberOfIntegerVariables += program.getNumberOfGlobalIntegerVariables();
-                for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
-                    numberOfBooleanVariables += program.getModule(i).getNumberOfBooleanVariables();
-                    numberOfIntegerVariables += program.getModule(i).getNumberOfIntegerVariables();
-                }
-                
-                // Resize the variable vectors appropriately.
-                result.booleanVariables.resize(numberOfBooleanVariables);
-                result.integerVariables.resize(numberOfIntegerVariables);
-                result.lowerBounds.resize(numberOfIntegerVariables);
-                result.upperBounds.resize(numberOfIntegerVariables);
-                
-                // Create variables.
-                for (uint_fast64_t i = 0; i < program.getNumberOfGlobalBooleanVariables(); ++i) {
-                    storm::ir::BooleanVariable const& var = program.getGlobalBooleanVariable(i);
-                    result.booleanVariables[var.getGlobalIndex()] = var;
-                    result.booleanVariableToIndexMap[var.getName()] = var.getGlobalIndex();
-                }
-                for (uint_fast64_t i = 0; i < program.getNumberOfGlobalIntegerVariables(); ++i) {
-                    storm::ir::IntegerVariable const& var = program.getGlobalIntegerVariable(i);
-                    result.integerVariables[var.getGlobalIndex()] = var;
-                    result.integerVariableToIndexMap[var.getName()] = var.getGlobalIndex();
-                    result.lowerBounds[var.getGlobalIndex()] = var.getLowerBound()->getValueAsInt(nullptr);
-                    result.upperBounds[var.getGlobalIndex()] = var.getUpperBound()->getValueAsInt(nullptr);
-                }
-                for (uint_fast64_t i = 0; i < program.getNumberOfModules(); ++i) {
-                    storm::ir::Module const& module = program.getModule(i);
-                    
-                    for (uint_fast64_t j = 0; j < module.getNumberOfBooleanVariables(); ++j) {
-                        storm::ir::BooleanVariable const& var = module.getBooleanVariable(j);
-                        result.booleanVariables[var.getGlobalIndex()] = var;
-                        result.booleanVariableToIndexMap[var.getName()] = var.getGlobalIndex();
-                    }
-                    for (uint_fast64_t j = 0; j < module.getNumberOfIntegerVariables(); ++j) {
-                        storm::ir::IntegerVariable const& var = module.getIntegerVariable(j);
-                        result.integerVariables[var.getGlobalIndex()] = var;
-                        result.integerVariableToIndexMap[var.getName()] = var.getGlobalIndex();
-                        result.lowerBounds[var.getGlobalIndex()] = var.getLowerBound()->getValueAsInt(nullptr);
-                        result.upperBounds[var.getGlobalIndex()] = var.getUpperBound()->getValueAsInt(nullptr);
-                    }
-                }
-                
-                return result;
-            }
-            
-            /*!
-             * Generates the initial state of the given program.
-             *
-             * @param program The program for which to construct the initial state.
-             * @param variableInformation A structure with information about the variables in the program.
-             * @return The initial state.
-             */
-            static StateType* getInitialState(storm::ir::Program const& program, VariableInformation const& variableInformation) {
-                StateType* initialState = new StateType();
-                initialState->first.resize(variableInformation.booleanVariables.size());
-                initialState->second.resize(variableInformation.integerVariables.size());
-                
-                // Start with boolean variables.
-                for (uint_fast64_t i = 0; i < variableInformation.booleanVariables.size(); ++i) {
-                    // Check if an initial value is given
-                    if (variableInformation.booleanVariables[i].getInitialValue().get() == nullptr) {
-                        // If no initial value was given, we assume that the variable is initially false.
-                        std::get<0>(*initialState)[i] = false;
-                    } else {
-                        // Initial value was given.
-                        bool initialValue = variableInformation.booleanVariables[i].getInitialValue()->getValueAsBool(nullptr);
-                        std::get<0>(*initialState)[i] = initialValue;
-                    }
-                }
-                
-                // Now process integer variables.
-                for (uint_fast64_t i = 0; i < variableInformation.integerVariables.size(); ++i) {
-                    // Check if an initial value was given.
-                    if (variableInformation.integerVariables[i].getInitialValue().get() == nullptr) {
-                        // No initial value was given, so we assume that the variable initially has the least value it can take.
-                        std::get<1>(*initialState)[i] = variableInformation.integerVariables[i].getLowerBound()->getValueAsInt(nullptr);
-                    } else {
-                        // Initial value was given.
-                        int_fast64_t initialValue = variableInformation.integerVariables[i].getInitialValue()->getValueAsInt(nullptr);
-                        std::get<1>(*initialState)[i] = initialValue;
-                    }
-                }
-                
-                LOG4CPLUS_DEBUG(logger, "Generated initial state.");
-                return initialState;
-            }
-            
-            /*!
-             * Sets some boolean variable in the given state object.
-             *
-             * @param state The state to modify.
-             * @param index The index of the boolean variable to modify.
-             * @param value The new value of the variable.
-             */
-            static void setValue(StateType* state, uint_fast64_t index, bool value) {
-                std::get<0>(*state)[index] = value;
-            }
-            
-            /*!
-             * Set some integer variable in the given state object.
-             *
-             * @param state The state to modify.
-             * @param index index of the integer variable to modify.
-             * @param value The new value of the variable.
-             */
-            static void setValue(StateType* state, uint_fast64_t index, int_fast64_t value) {
-                std::get<1>(*state)[index] = value;
-            }
-
-            /*!
-             * Defines the undefined constants of the given program using the given string.
-             *
-             * @param program The program in which to define the constants.
-             * @param constantDefinitionString A comma-separated list of constant definitions.
-             */
-            static void defineUndefinedConstants(storm::ir::Program& program, std::string const& constantDefinitionString) {
-                if (!constantDefinitionString.empty()) {
-                    // Parse the string that defines the undefined constants of the model and make sure that it contains exactly
-                    // one value for each undefined constant of the model.
-                    std::vector<std::string> definitions;
-                    boost::split(definitions, constantDefinitionString, boost::is_any_of(","));
-                    for (auto& definition : definitions) {
-                        boost::trim(definition);
-                        
-                        // Check whether the token could be a legal constant definition.
-                        uint_fast64_t positionOfAssignmentOperator = definition.find('=');
-                        if (positionOfAssignmentOperator == std::string::npos) {
-                            throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: syntax error.";
-                        }
-                        
-                        // Now extract the variable name and the value from the string.
-                        std::string constantName = definition.substr(0, positionOfAssignmentOperator);
-                        boost::trim(constantName);
-                        std::string value = definition.substr(positionOfAssignmentOperator + 1);
-                        boost::trim(value);
-                        
-                        // Check whether the constant is a legal undefined constant of the program and if so, of what type it is.
-                        if (program.hasUndefinedBooleanConstant(constantName)) {
-                            if (value == "true") {
-                                program.getUndefinedBooleanConstantExpression(constantName)->define(true);
-                            } else if (value == "false") {
-                                program.getUndefinedBooleanConstantExpression(constantName)->define(false);
-                            } else {
-                                throw storm::exceptions::InvalidArgumentException() << "Illegal value for boolean constant: " << value << ".";
-                            }
-                        } else if (program.hasUndefinedIntegerConstant(constantName)) {
-                            try {
-                                int_fast64_t integerValue = std::stoi(value);
-                                program.getUndefinedIntegerConstantExpression(constantName)->define(integerValue);
-                            } catch (std::invalid_argument const&) {
-                                throw storm::exceptions::InvalidArgumentException() << "Illegal value of integer constant: " << value << ".";
-                            } catch (std::out_of_range const&) {
-                                throw storm::exceptions::InvalidArgumentException() << "Illegal value of integer constant: " << value << " (value too big).";
-                            }
-                        } else if (program.hasUndefinedDoubleConstant(constantName)) {
-                            try {
-                                double doubleValue = std::stod(value);
-                                program.getUndefinedDoubleConstantExpression(constantName)->define(doubleValue);
-                            } catch (std::invalid_argument const&) {
-                                throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << ".";
-                            } catch (std::out_of_range const&) {
-                                throw storm::exceptions::InvalidArgumentException() << "Illegal value of double constant: " << value << " (value too big).";
-                            }
-                            
-                        } else {
-                            throw storm::exceptions::InvalidArgumentException() << "Illegal constant definition string: unknown undefined constant " << constantName << ".";
-                        }
-                    }
-                }
-            }
-            
-            /*!
-             * Undefines all previously defined constants in the given program.
-             *
-             * @param program The program in which to undefine the constants.
-             */
-            static void undefineUndefinedConstants(storm::ir::Program& program) {
-                for (auto const& nameExpressionPair : program.getBooleanUndefinedConstantExpressionsMap()) {
-                    nameExpressionPair.second->undefine();
-                }
-                for (auto const& nameExpressionPair : program.getIntegerUndefinedConstantExpressionsMap()) {
-                    nameExpressionPair.second->undefine();
-                }
-                for (auto const& nameExpressionPair : program.getDoubleUndefinedConstantExpressionsMap()) {
-                    nameExpressionPair.second->undefine();
-                }
-            }
-
-            /*!
-             * Computes the weakest precondition of the given boolean expression wrt. the given updates. The weakest
-             * precondition is the most liberal expression that must hold in order to satisfy the given boolean
-             * expression after performing the updates. The updates must be disjoint in the sense that they must not
-             * assign an expression to a variable twice or more.
-             *
-             * @param expression The expression for which to build the weakest precondition.
-             * @param update The update with respect to which to compute the weakest precondition.
-             */
-            std::unique_ptr<storm::ir::expressions::BaseExpression> getWeakestPrecondition(std::unique_ptr<storm::ir::expressions::BaseExpression> const& booleanExpression, std::vector<std::reference_wrapper<storm::ir::Update const>> const& updates) {
-                std::map<std::string, std::reference_wrapper<storm::ir::expressions::BaseExpression>> variableToExpressionMap;
-                
-                // Construct the full substitution we need to perform later.
-                for (auto const& update : updates) {
-                    for (auto const& variableAssignmentPair : update.get().getBooleanAssignments()) {
-                        variableToExpressionMap.emplace(variableAssignmentPair.first, *variableAssignmentPair.second.getExpression());
-                    }
-                    for (auto const& variableAssignmentPair : update.get().getIntegerAssignments()) {
-                        variableToExpressionMap.emplace(variableAssignmentPair.first, *variableAssignmentPair.second.getExpression());
-                    }
-                }
-                
-                // Copy the given expression and apply the substitution.
-                return storm::ir::expressions::BaseExpression::substitute(booleanExpression->clone(), variableToExpressionMap);
-            }
-            
-        } // namespace ir
-    } // namespace utility
-} // namespace storm
-
-#endif /* STORM_UTILITY_IRUTILITY_H_ */
diff --git a/src/utility/PrismUtility.h b/src/utility/PrismUtility.h
new file mode 100644
index 000000000..9ed15411a
--- /dev/null
+++ b/src/utility/PrismUtility.h
@@ -0,0 +1,195 @@
+#ifndef STORM_UTILITY_PRISMUTILITY
+#define STORM_UTILITY_PRISMUTILITY
+
+#include "src/storage/LabeledValues.h"
+#include "src/storage/prism/Program.h"
+#include "src/exceptions/ExceptionMacros.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+    namespace utility {
+        namespace prism {
+            // A structure holding information about a particular choice.
+            template<typename ValueType, typename KeyType=uint_fast64_t, typename Compare=std::less<uint_fast64_t>>
+            struct Choice {
+            public:
+                Choice(std::string const& actionLabel) : distribution(), actionLabel(actionLabel), choiceLabels() {
+                    // Intentionally left empty.
+                }
+                
+                /*!
+                 * Returns an iterator to the first element of this choice.
+                 *
+                 * @return An iterator to the first element of this choice.
+                 */
+                typename std::map<KeyType, ValueType>::iterator begin() {
+                    return distribution.begin();
+                }
+                
+                /*!
+                 * Returns an iterator to the first element of this choice.
+                 *
+                 * @return An iterator to the first element of this choice.
+                 */
+                typename std::map<KeyType, ValueType>::const_iterator begin() const {
+                    return distribution.cbegin();
+                }
+                
+                /*!
+                 * Returns an iterator that points past the elements of this choice.
+                 *
+                 * @return An iterator that points past the elements of this choice.
+                 */
+                typename std::map<KeyType, ValueType>::iterator end() {
+                    return distribution.end();
+                }
+                
+                /*!
+                 * Returns an iterator that points past the elements of this choice.
+                 *
+                 * @return An iterator that points past the elements of this choice.
+                 */
+                typename std::map<KeyType, ValueType>::const_iterator end() const {
+                    return distribution.cend();
+                }
+                
+                /*!
+                 * Returns an iterator to the element with the given key, if there is one. Otherwise, the iterator points to
+                 * distribution.end().
+                 *
+                 * @param value The value to find.
+                 * @return An iterator to the element with the given key, if there is one.
+                 */
+                typename std::map<KeyType, ValueType>::iterator find(uint_fast64_t value) {
+                    return distribution.find(value);
+                }
+                
+                /*!
+                 * Inserts the contents of this object to the given output stream.
+                 *
+                 * @param out The stream in which to insert the contents.
+                 */
+                friend std::ostream& operator<<(std::ostream& out, Choice<ValueType> const& choice) {
+                    out << "<";
+                    for (auto const& stateProbabilityPair : choice.distribution) {
+                        out << stateProbabilityPair.first << " : " << stateProbabilityPair.second << ", ";
+                    }
+                    out << ">";
+                    return out;
+                }
+                
+                /*!
+                 * Adds the given label to the labels associated with this choice.
+                 *
+                 * @param label The label to associate with this choice.
+                 */
+                void addChoiceLabel(uint_fast64_t label) {
+                    choiceLabels.insert(label);
+                }
+                
+                /*!
+                 * Adds the given label set to the labels associated with this choice.
+                 *
+                 * @param labelSet The label set to associate with this choice.
+                 */
+                void addChoiceLabels(boost::container::flat_set<uint_fast64_t> const& labelSet) {
+                    for (uint_fast64_t label : labelSet) {
+                        addChoiceLabel(label);
+                    }
+                }
+                
+                /*!
+                 * Retrieves the set of labels associated with this choice.
+                 *
+                 * @return The set of labels associated with this choice.
+                 */
+                boost::container::flat_set<uint_fast64_t> const& getChoiceLabels() const {
+                    return choiceLabels;
+                }
+                
+                /*!
+                 * Retrieves the action label of this choice.
+                 *
+                 * @return The action label of this choice.
+                 */
+                std::string const& getActionLabel() const {
+                    return actionLabel;
+                }
+                
+                /*!
+                 * Retrieves the entry in the choice that is associated with the given state and creates one if none exists,
+                 * yet.
+                 *
+                 * @param state The state for which to add the entry.
+                 * @return A reference to the entry that is associated with the given state.
+                 */
+                ValueType& getOrAddEntry(uint_fast64_t state) {
+                    auto stateProbabilityPair = distribution.find(state);
+                    
+                    if (stateProbabilityPair == distribution.end()) {
+                        distribution[state] = ValueType();
+                    }
+                    return distribution.at(state);
+                }
+                
+                /*!
+                 * Retrieves the entry in the choice that is associated with the given state and creates one if none exists,
+                 * yet.
+                 *
+                 * @param state The state for which to add the entry.
+                 * @return A reference to the entry that is associated with the given state.
+                 */
+                ValueType const& getOrAddEntry(uint_fast64_t state) const {
+                    auto stateProbabilityPair = distribution.find(state);
+                    
+                    if (stateProbabilityPair == distribution.end()) {
+                        distribution[state] = ValueType();
+                    }
+                    return distribution.at(state);
+                }
+                
+            private:
+                // The distribution that is associated with the choice.
+                std::map<KeyType, ValueType, Compare> distribution;
+                
+                // The label of the choice.
+                std::string actionLabel;
+                
+                // The labels that are associated with this choice.
+                boost::container::flat_set<uint_fast64_t> choiceLabels;
+            };
+            
+            /*!
+             * Adds the target state and probability to the given choice and ignores the labels. This function overloads with
+             * other functions to ensure the proper treatment of labels.
+             *
+             * @param choice The choice to which to add the target state and probability.
+             * @param state The target state of the probability.
+             * @param probability The probability to reach the target state in one step.
+             * @param labels A set of labels that is supposed to be associated with this state and probability. NOTE: this
+             * is ignored by this particular function but not by the overloaded functions.
+             */
+            template<typename ValueType>
+            void addProbabilityToChoice(Choice<ValueType>& choice, uint_fast64_t state, ValueType probability, boost::container::flat_set<uint_fast64_t> const& labels) {
+                choice.getOrAddEntry(state) += probability;
+            }
+            
+            /*!
+             * Adds the target state and probability to the given choice and labels it accordingly. This function overloads
+             * with other functions to ensure the proper treatment of labels.
+             *
+             * @param choice The choice to which to add the target state and probability.
+             * @param state The target state of the probability.
+             * @param probability The probability to reach the target state in one step.
+             * @param labels A set of labels that is supposed to be associated with this state and probability.
+             */
+            template<typename ValueType>
+            void addProbabilityToChoice(Choice<storm::storage::LabeledValues<ValueType>>& choice, uint_fast64_t state, ValueType probability, boost::container::flat_set<uint_fast64_t> const& labels) {
+                auto& labeledEntry = choice.getOrAddEntry(state);
+                labeledEntry.addValue(probability, labels);
+            }
+        } // namespace prism
+    } // namespace utility
+} // namespace storm
+
+#endif /* STORM_UTILITY_PRISMUTILITY_H_ */