diff --git a/src/adapters/ExplicitModelAdapter.h b/src/adapters/ExplicitModelAdapter.h
index a38b7c27b..3875eef8a 100644
--- a/src/adapters/ExplicitModelAdapter.h
+++ b/src/adapters/ExplicitModelAdapter.h
@@ -518,13 +518,13 @@ namespace storm {
              * @param program The program in which to undefine the constants.
              */
             static void undefineUndefinedConstants(storm::ir::Program& program) {
-                for (auto nameExpressionPair : program.getBooleanUndefinedConstantExpressionsMap()) {
+                for (auto const& nameExpressionPair : program.getBooleanUndefinedConstantExpressionsMap()) {
                     nameExpressionPair.second->undefine();
                 }
-                for (auto nameExpressionPair : program.getIntegerUndefinedConstantExpressionsMap()) {
+                for (auto const& nameExpressionPair : program.getIntegerUndefinedConstantExpressionsMap()) {
                     nameExpressionPair.second->undefine();
                 }
-                for (auto nameExpressionPair : program.getDoubleUndefinedConstantExpressionsMap()) {
+                for (auto const& nameExpressionPair : program.getDoubleUndefinedConstantExpressionsMap()) {
                     nameExpressionPair.second->undefine();
                 }
             }
@@ -1115,7 +1115,7 @@ namespace storm {
              * @return The state labeling of the given program.
              */
             static storm::models::AtomicPropositionsLabeling buildStateLabeling(storm::ir::Program const& program, VariableInformation const& variableInformation, StateInformation const& stateInformation) {
-                std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> const& labels = program.getLabels();
+                std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& labels = program.getLabels();
                 
                 storm::models::AtomicPropositionsLabeling result(stateInformation.reachableStates.size(), labels.size() + 1);
                 
diff --git a/src/adapters/SymbolicExpressionAdapter.h b/src/adapters/SymbolicExpressionAdapter.h
index efdd5e2d0..5acb90c9c 100644
--- a/src/adapters/SymbolicExpressionAdapter.h
+++ b/src/adapters/SymbolicExpressionAdapter.h
@@ -26,7 +26,7 @@ public:
 
 	}
 
-	ADD* translateExpression(std::shared_ptr<storm::ir::expressions::BaseExpression> expression) {
+	ADD* translateExpression(std::unique_ptr<storm::ir::expressions::BaseExpression> const& expression) {
 		expression->accept(this);
 		return stack.top();
 	}
diff --git a/src/ir/Assignment.cpp b/src/ir/Assignment.cpp
index 60a776b49..a50847afb 100644
--- a/src/ir/Assignment.cpp
+++ b/src/ir/Assignment.cpp
@@ -17,8 +17,8 @@ namespace storm {
             // Nothing to do here.
         }
         
-        Assignment::Assignment(std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& expression)
-        : variableName(variableName), expression(expression) {
+        Assignment::Assignment(std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& expression)
+        : variableName(variableName), expression(std::move(expression)) {
             // Nothing to do here.
         }
         
@@ -30,11 +30,26 @@ namespace storm {
             }
         }
         
+        Assignment::Assignment(Assignment const& otherAssignment) : variableName(otherAssignment.variableName), expression() {
+            if (otherAssignment.expression != nullptr) {
+                expression = otherAssignment.expression->clone();
+            }
+        }
+        
+        Assignment& Assignment::operator=(Assignment const& otherAssignment) {
+            if (this != &otherAssignment) {
+                this->variableName = otherAssignment.variableName;
+                this->expression = otherAssignment.expression->clone();
+            }
+            
+            return *this;
+        }
+        
         std::string const& Assignment::getVariableName() const {
             return variableName;
         }
         
-        std::shared_ptr<storm::ir::expressions::BaseExpression> const& Assignment::getExpression() const {
+        std::unique_ptr<storm::ir::expressions::BaseExpression> const& Assignment::getExpression() const {
             return expression;
         }
         
diff --git a/src/ir/Assignment.h b/src/ir/Assignment.h
index caf7c520c..12d96a413 100644
--- a/src/ir/Assignment.h
+++ b/src/ir/Assignment.h
@@ -38,7 +38,7 @@ namespace storm {
              * @param variableName The variable that this assignment targets.
              * @param expression The expression to assign to the variable.
              */
-            Assignment(std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& expression);
+            Assignment(std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& expression);
             
             /*!
              * Creates a copy of the given assignment and performs the provided renaming.
@@ -50,6 +50,20 @@ namespace storm {
              */
             Assignment(Assignment const& oldAssignment, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState);
             
+            /*!
+             * Performs a deep-copy of the given assignment.
+             *
+             * @param otherAssignment The assignment to copy.
+             */
+            Assignment(Assignment const& otherAssignment);
+            
+            /*!
+             * Performs a deep-copy of the given assignment and assigns it to the current one.
+             *
+             * @param otherAssignment The assignment to assign.
+             */
+            Assignment& operator=(Assignment const& otherAssignment);
+            
             /*!
              * Retrieves the name of the variable that this assignment targets.
              *
@@ -62,7 +76,7 @@ namespace storm {
              *
              * @return The expression that is assigned to the variable.
              */
-            std::shared_ptr<storm::ir::expressions::BaseExpression> const& getExpression() const;
+            std::unique_ptr<storm::ir::expressions::BaseExpression> const& getExpression() const;
             
             /*!
              * Retrieves a string representation of this assignment.
@@ -75,7 +89,7 @@ namespace storm {
             std::string variableName;
             
             // The expression that is assigned to the variable.
-            std::shared_ptr<storm::ir::expressions::BaseExpression> expression;
+            std::unique_ptr<storm::ir::expressions::BaseExpression> expression;
         };
         
     } // namespace ir
diff --git a/src/ir/BooleanVariable.cpp b/src/ir/BooleanVariable.cpp
index f673633a1..843655be9 100644
--- a/src/ir/BooleanVariable.cpp
+++ b/src/ir/BooleanVariable.cpp
@@ -17,8 +17,8 @@ namespace storm {
             // Nothing to do here.
         }
         
-        BooleanVariable::BooleanVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue)
-		: Variable(localIndex, globalIndex, variableName,  initialValue) {
+        BooleanVariable::BooleanVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue)
+		: Variable(localIndex, globalIndex, variableName, std::move(initialValue)) {
             // Nothing to do here.
         }
         
@@ -27,6 +27,14 @@ namespace storm {
             // Nothing to do here.
         }
         
+        BooleanVariable& BooleanVariable::operator=(BooleanVariable const& otherVariable) {
+            if (this != &otherVariable) {
+                Variable::operator=(otherVariable);
+            }
+            
+            return *this;
+        }
+        
         std::string BooleanVariable::toString() const {
             std::stringstream result;
             result << this->getName() << ": bool";
diff --git a/src/ir/BooleanVariable.h b/src/ir/BooleanVariable.h
index 491be1c6f..b968d7890 100644
--- a/src/ir/BooleanVariable.h
+++ b/src/ir/BooleanVariable.h
@@ -41,7 +41,7 @@ namespace storm {
              * @param variableName The name of the variable.
              * @param initialValue The expression that defines the initial value of the variable.
              */
-            BooleanVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr));
+            BooleanVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue = nullptr);
             
             /*!
              * Creates a copy of the given boolean variable and performs the provided renaming.
@@ -55,6 +55,8 @@ namespace storm {
              */
             BooleanVariable(BooleanVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState);
             
+            BooleanVariable& operator=(BooleanVariable const& otherVariable);
+            
             /*!
              * Retrieves a string representation of this variable.
              * @returns a string representation of this variable.
diff --git a/src/ir/Command.cpp b/src/ir/Command.cpp
index 570789480..9898c5187 100644
--- a/src/ir/Command.cpp
+++ b/src/ir/Command.cpp
@@ -14,12 +14,12 @@
 namespace storm {
     namespace ir {
         
-        Command::Command() : actionName(), guardExpression(), updates() {
+        Command::Command() : actionName(), guardExpression(), updates(), globalIndex() {
             // Nothing to do here.
         }
         
-        Command::Command(uint_fast64_t globalIndex, std::string const& actionName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> const& updates)
-        : actionName(actionName), guardExpression(guardExpression), updates(updates), globalIndex(globalIndex) {
+        Command::Command(uint_fast64_t globalIndex, std::string const& actionName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& guardExpression, std::vector<storm::ir::Update> const& updates)
+        : actionName(actionName), guardExpression(std::move(guardExpression)), updates(updates), globalIndex(globalIndex) {
             // Nothing to do here.
         }
         
@@ -36,11 +36,28 @@ namespace storm {
             }
         }
         
+        Command::Command(Command const& otherCommand) : actionName(otherCommand.actionName), guardExpression(), updates(otherCommand.updates), globalIndex(otherCommand.globalIndex) {
+            if (otherCommand.guardExpression != nullptr) {
+                guardExpression = otherCommand.guardExpression->clone();
+            }
+        }
+        
+        Command& Command::operator=(Command const& otherCommand) {
+            if (this != &otherCommand) {
+                this->actionName = otherCommand.actionName;
+                this->guardExpression = otherCommand.guardExpression->clone();
+                this->updates = otherCommand.updates;
+                this->globalIndex = otherCommand.globalIndex;
+            }
+            
+            return *this;
+        }
+        
         std::string const& Command::getActionName() const {
             return this->actionName;
         }
         
-        std::shared_ptr<storm::ir::expressions::BaseExpression> const& Command::getGuard() const {
+        std::unique_ptr<storm::ir::expressions::BaseExpression> const& Command::getGuard() const {
             return guardExpression;
         }
         
diff --git a/src/ir/Command.h b/src/ir/Command.h
index 67a431949..d6ae39ee8 100644
--- a/src/ir/Command.h
+++ b/src/ir/Command.h
@@ -43,7 +43,7 @@ namespace storm {
              * @param guardExpression the expression that defines the guard of the command.
              * @param updates A list of updates that is associated with this command.
              */
-            Command(uint_fast64_t globalIndex, std::string const& actionName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> const& updates);
+            Command(uint_fast64_t globalIndex, std::string const& actionName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& guardExpression, std::vector<storm::ir::Update> const& updates);
             
             /*!
              * Creates a copy of the given command and performs the provided renaming.
@@ -56,6 +56,15 @@ namespace storm {
              */
             Command(Command const& oldCommand, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState);
             
+            /*!
+             * Performs a deep-copy of the given command.
+             *
+             * @param otherCommand The command to copy.
+             */
+            Command(Command const& otherCommand);
+            
+            Command& operator=(Command const& otherCommand);
+            
             /*!
              * Retrieves the action name of this command.
              *
@@ -68,7 +77,7 @@ namespace storm {
              *
              * @return A reference to the guard of the command.
              */
-            std::shared_ptr<storm::ir::expressions::BaseExpression> const& getGuard() const;
+            std::unique_ptr<storm::ir::expressions::BaseExpression> const& getGuard() const;
             
             /*!
              * Retrieves the number of updates associated with this command.
@@ -103,7 +112,7 @@ namespace storm {
             std::string actionName;
             
             // The expression that defines the guard of the command.
-            std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression;
+            std::unique_ptr<storm::ir::expressions::BaseExpression> guardExpression;
             
             // The list of updates of the command.
             std::vector<storm::ir::Update> updates;
diff --git a/src/ir/IntegerVariable.cpp b/src/ir/IntegerVariable.cpp
index ace6735be..b98b30d07 100644
--- a/src/ir/IntegerVariable.cpp
+++ b/src/ir/IntegerVariable.cpp
@@ -12,18 +12,15 @@
 #include "src/parser/prismparser/VariableState.h"
 
 namespace storm {
-    
     namespace ir {
         
         IntegerVariable::IntegerVariable() : lowerBound(), upperBound() {
             // Nothing to do here.
         }
         
-        IntegerVariable::IntegerVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound, std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue)
-        : Variable(localIndex, globalIndex, variableName, initialValue), lowerBound(lowerBound), upperBound(upperBound) {
-            if (this->getInitialValue() == nullptr) {
-                this->setInitialValue(lowerBound);
-            }
+        IntegerVariable::IntegerVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& lowerBound, std::unique_ptr<storm::ir::expressions::BaseExpression>&& upperBound, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue)
+        : Variable(localIndex, globalIndex, variableName, std::move(initialValue)), lowerBound(std::move(lowerBound)), upperBound(std::move(upperBound)) {
+            // Nothing to do here.
         }
         
         IntegerVariable::IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState)
@@ -31,11 +28,33 @@ namespace storm {
             // Nothing to do here.
         }
         
-        std::shared_ptr<storm::ir::expressions::BaseExpression> IntegerVariable::getLowerBound() const {
+        IntegerVariable::IntegerVariable(IntegerVariable const& otherVariable) : Variable(otherVariable.getLocalIndex(), otherVariable.getGlobalIndex(), otherVariable.getName(), nullptr), lowerBound(), upperBound() {
+            if (otherVariable.getInitialValue() != nullptr) {
+                setInitialValue(otherVariable.getInitialValue()->clone());
+            }
+            if (otherVariable.lowerBound != nullptr) {
+                lowerBound = otherVariable.lowerBound->clone();
+            }
+            if (otherVariable.upperBound != nullptr) {
+                upperBound = otherVariable.upperBound->clone();
+            }
+        }
+        
+        IntegerVariable& IntegerVariable::operator=(IntegerVariable const& otherVariable) {
+            if (this != &otherVariable) {
+                Variable::operator=(otherVariable);
+                this->lowerBound = otherVariable.lowerBound->clone();
+                this->upperBound = otherVariable.upperBound->clone();
+            }
+            
+            return *this;
+        }
+        
+        std::unique_ptr<storm::ir::expressions::BaseExpression> const& IntegerVariable::getLowerBound() const {
             return this->lowerBound;
         }
         
-        std::shared_ptr<storm::ir::expressions::BaseExpression> IntegerVariable::getUpperBound() const {
+        std::unique_ptr<storm::ir::expressions::BaseExpression> const& IntegerVariable::getUpperBound() const {
             return this->upperBound;
         }
         
@@ -50,5 +69,4 @@ namespace storm {
         }
         
     } // namespace ir
-    
 } // namespace storm
diff --git a/src/ir/IntegerVariable.h b/src/ir/IntegerVariable.h
index cd1c20be4..930e1d0b8 100644
--- a/src/ir/IntegerVariable.h
+++ b/src/ir/IntegerVariable.h
@@ -43,7 +43,7 @@ namespace storm {
              * @param upperBound the upper bound of the domain of the variable.
              * @param initialValue the expression that defines the initial value of the variable.
              */
-            IntegerVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound, std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr));
+            IntegerVariable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& lowerBound, std::unique_ptr<storm::ir::expressions::BaseExpression>&& upperBound, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue = nullptr);
             
             /*!
              * Creates a copy of the given integer variable and performs the provided renaming.
@@ -57,17 +57,26 @@ namespace storm {
              */
             IntegerVariable(IntegerVariable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState);
             
+            /*!
+             * Performs a deep-copy of the given variable.
+             *
+             * @param otherVariable The variable to copy.
+             */
+            IntegerVariable(IntegerVariable const& otherVariable);
+            
+            IntegerVariable& operator=(IntegerVariable const& otherVariable);
+            
             /*!
              * Retrieves the lower bound for this integer variable.
              * @returns the lower bound for this integer variable.
              */
-            std::shared_ptr<storm::ir::expressions::BaseExpression> getLowerBound() const;
+            std::unique_ptr<storm::ir::expressions::BaseExpression> const& getLowerBound() const;
             
             /*!
              * Retrieves the upper bound for this integer variable.
              * @returns the upper bound for this integer variable.
              */
-            std::shared_ptr<storm::ir::expressions::BaseExpression> getUpperBound() const;
+            std::unique_ptr<storm::ir::expressions::BaseExpression> const& getUpperBound() const;
             
             /*!
              * Retrieves a string representation of this variable.
@@ -77,10 +86,10 @@ namespace storm {
             
         private:
             // The lower bound of the domain of the variable.
-            std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound;
+            std::unique_ptr<storm::ir::expressions::BaseExpression> lowerBound;
             
             // The upper bound of the domain of the variable.
-            std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound;
+            std::unique_ptr<storm::ir::expressions::BaseExpression> upperBound;
         };
         
     } // namespace ir
diff --git a/src/ir/Module.h b/src/ir/Module.h
index 03e4d0be8..ff96f266a 100644
--- a/src/ir/Module.h
+++ b/src/ir/Module.h
@@ -61,9 +61,6 @@ namespace storm {
                    std::map<std::string, uint_fast64_t> const& integerVariableToLocalIndexMap,
                    std::vector<storm::ir::Command> const& commands);
             
-            typedef uint_fast64_t (*addIntegerVariablePtr)(std::string const& name, std::shared_ptr<storm::ir::expressions::BaseExpression> const& lower, std::shared_ptr<storm::ir::expressions::BaseExpression> const upper, std::shared_ptr<storm::ir::expressions::BaseExpression> const& init);
-            typedef uint_fast64_t (*addBooleanVariablePtr)(std::string const& name, std::shared_ptr<storm::ir::expressions::BaseExpression> const& init);
-            
             /*!
              * Special copy constructor, implementing the module renaming functionality.
              * This will create a new module having all identifiers renamed according to the given map.
diff --git a/src/ir/Program.cpp b/src/ir/Program.cpp
index 782d9cb7a..08b4ec934 100644
--- a/src/ir/Program.cpp
+++ b/src/ir/Program.cpp
@@ -24,17 +24,34 @@ namespace storm {
         }
         
         Program::Program(ModelType modelType,
-                         std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> const& booleanUndefinedConstantExpressions,
-                         std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> const& integerUndefinedConstantExpressions,
-                         std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> const& doubleUndefinedConstantExpressions,
+                         std::map<std::string, std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>> const& booleanUndefinedConstantExpressions,
+                         std::map<std::string, std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>> const& integerUndefinedConstantExpressions,
+                         std::map<std::string, std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>> const& doubleUndefinedConstantExpressions,
                          std::vector<BooleanVariable> const& globalBooleanVariables,
                          std::vector<IntegerVariable> const& globalIntegerVariables,
                          std::map<std::string, uint_fast64_t> const& globalBooleanVariableToIndexMap,
                          std::map<std::string, uint_fast64_t> const& globalIntegerVariableToIndexMap,
                          std::vector<storm::ir::Module> const& modules,
                          std::map<std::string, storm::ir::RewardModel> const& rewards,
-                         std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> const& labels)
-        : modelType(modelType), booleanUndefinedConstantExpressions(booleanUndefinedConstantExpressions), integerUndefinedConstantExpressions(integerUndefinedConstantExpressions), doubleUndefinedConstantExpressions(doubleUndefinedConstantExpressions), globalBooleanVariables(globalBooleanVariables), globalIntegerVariables(globalIntegerVariables), globalBooleanVariableToIndexMap(globalBooleanVariableToIndexMap), globalIntegerVariableToIndexMap(globalIntegerVariableToIndexMap), modules(modules), rewards(rewards), labels(labels), actionsToModuleIndexMap(), variableToModuleIndexMap() {
+                         std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& labels)
+        : modelType(modelType), globalBooleanVariables(globalBooleanVariables), globalIntegerVariables(globalIntegerVariables),
+        globalBooleanVariableToIndexMap(globalBooleanVariableToIndexMap), globalIntegerVariableToIndexMap(globalIntegerVariableToIndexMap),
+        modules(modules), rewards(rewards), actionsToModuleIndexMap(), variableToModuleIndexMap() {
+            
+            // Perform a deep-copy of the maps.
+            for (auto const& booleanUndefinedConstant : booleanUndefinedConstantExpressions) {
+                this->booleanUndefinedConstantExpressions[booleanUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>(new storm::ir::expressions::BooleanConstantExpression(*booleanUndefinedConstant.second));
+            }
+            for (auto const& integerUndefinedConstant : integerUndefinedConstantExpressions) {
+                this->integerUndefinedConstantExpressions[integerUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>(new storm::ir::expressions::IntegerConstantExpression(*integerUndefinedConstant.second));
+            }
+            for (auto const& doubleUndefinedConstant : doubleUndefinedConstantExpressions) {
+                this->doubleUndefinedConstantExpressions[doubleUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>(new storm::ir::expressions::DoubleConstantExpression(*doubleUndefinedConstant.second));
+            }
+            for (auto const& label : labels) {
+                this->labels[label.first] = label.second->clone();
+            }
+            
             // Now build the mapping from action names to module indices so that the lookup can later be performed quickly.
             for (unsigned int moduleIndex = 0; moduleIndex < this->modules.size(); moduleIndex++) {
                 Module const& module = this->modules[moduleIndex];
@@ -57,6 +74,55 @@ namespace storm {
             }
         }
         
+        Program::Program(Program const& otherProgram) : modelType(otherProgram.modelType), globalBooleanVariables(otherProgram.globalBooleanVariables),
+        globalIntegerVariables(otherProgram.globalIntegerVariables), globalBooleanVariableToIndexMap(otherProgram.globalBooleanVariableToIndexMap),
+        globalIntegerVariableToIndexMap(otherProgram.globalIntegerVariableToIndexMap), modules(otherProgram.modules), rewards(otherProgram.rewards),
+        actionsToModuleIndexMap(), variableToModuleIndexMap() {
+            // Perform deep-copy of the maps.
+            for (auto const& booleanUndefinedConstant : otherProgram.booleanUndefinedConstantExpressions) {
+                this->booleanUndefinedConstantExpressions[booleanUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>(new storm::ir::expressions::BooleanConstantExpression(*booleanUndefinedConstant.second));
+            }
+            for (auto const& integerUndefinedConstant : otherProgram.integerUndefinedConstantExpressions) {
+                this->integerUndefinedConstantExpressions[integerUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>(new storm::ir::expressions::IntegerConstantExpression(*integerUndefinedConstant.second));
+            }
+            for (auto const& doubleUndefinedConstant : otherProgram.doubleUndefinedConstantExpressions) {
+                this->doubleUndefinedConstantExpressions[doubleUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>(new storm::ir::expressions::DoubleConstantExpression(*doubleUndefinedConstant.second));
+            }
+            for (auto const& label : otherProgram.labels) {
+                this->labels[label.first] = label.second->clone();
+            }
+        }
+        
+        Program& Program::operator=(Program const& otherProgram) {
+            if (this != &otherProgram) {
+                this->modelType = otherProgram.modelType;
+                this->globalBooleanVariables = otherProgram.globalBooleanVariables;
+                this->globalIntegerVariables = otherProgram.globalIntegerVariables;
+                this->globalBooleanVariableToIndexMap = otherProgram.globalBooleanVariableToIndexMap;
+                this->globalIntegerVariableToIndexMap = otherProgram.globalIntegerVariableToIndexMap;
+                this->modules = otherProgram.modules;
+                this->rewards = otherProgram.rewards;
+                this->actionsToModuleIndexMap = otherProgram.actionsToModuleIndexMap;
+                this->variableToModuleIndexMap = otherProgram.variableToModuleIndexMap;
+                
+                // Perform deep-copy of the maps.
+                for (auto const& booleanUndefinedConstant : otherProgram.booleanUndefinedConstantExpressions) {
+                    this->booleanUndefinedConstantExpressions[booleanUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>(new storm::ir::expressions::BooleanConstantExpression(*booleanUndefinedConstant.second));
+                }
+                for (auto const& integerUndefinedConstant : otherProgram.integerUndefinedConstantExpressions) {
+                    this->integerUndefinedConstantExpressions[integerUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>(new storm::ir::expressions::IntegerConstantExpression(*integerUndefinedConstant.second));
+                }
+                for (auto const& doubleUndefinedConstant : otherProgram.doubleUndefinedConstantExpressions) {
+                    this->doubleUndefinedConstantExpressions[doubleUndefinedConstant.first] = std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>(new storm::ir::expressions::DoubleConstantExpression(*doubleUndefinedConstant.second));
+                }
+                for (auto const& label : otherProgram.labels) {
+                    this->labels[label.first] = label.second->clone();
+                }
+            }
+            
+            return *this;
+        }
+        
         Program::ModelType Program::getModelType() const {
             return modelType;
         }
@@ -160,7 +226,7 @@ namespace storm {
             return nameRewardModelPair->second;
         }
         
-        std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> const& Program::getLabels() const {
+        std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& Program::getLabels() const {
             return this->labels;
         }
         
@@ -168,7 +234,7 @@ namespace storm {
             return this->booleanUndefinedConstantExpressions.find(constantName) != this->booleanUndefinedConstantExpressions.end();
         }
         
-        std::shared_ptr<storm::ir::expressions::BooleanConstantExpression> Program::getUndefinedBooleanConstantExpression(std::string const& constantName) const {
+        std::unique_ptr<storm::ir::expressions::BooleanConstantExpression> const& Program::getUndefinedBooleanConstantExpression(std::string const& constantName) const {
             auto constantExpressionPair = this->booleanUndefinedConstantExpressions.find(constantName);
             if (constantExpressionPair != this->booleanUndefinedConstantExpressions.end()) {
                 return constantExpressionPair->second;
@@ -181,7 +247,7 @@ namespace storm {
             return this->integerUndefinedConstantExpressions.find(constantName) != this->integerUndefinedConstantExpressions.end();
         }
         
-        std::shared_ptr<storm::ir::expressions::IntegerConstantExpression> Program::getUndefinedIntegerConstantExpression(std::string const& constantName) const {
+        std::unique_ptr<storm::ir::expressions::IntegerConstantExpression> const& Program::getUndefinedIntegerConstantExpression(std::string const& constantName) const {
             auto constantExpressionPair = this->integerUndefinedConstantExpressions.find(constantName);
             if (constantExpressionPair != this->integerUndefinedConstantExpressions.end()) {
                 return constantExpressionPair->second;
@@ -194,7 +260,7 @@ namespace storm {
             return this->doubleUndefinedConstantExpressions.find(constantName) != this->doubleUndefinedConstantExpressions.end();
         }
         
-        std::shared_ptr<storm::ir::expressions::DoubleConstantExpression> Program::getUndefinedDoubleConstantExpression(std::string const& constantName) const {
+        std::unique_ptr<storm::ir::expressions::DoubleConstantExpression> const& Program::getUndefinedDoubleConstantExpression(std::string const& constantName) const {
             auto constantExpressionPair = this->doubleUndefinedConstantExpressions.find(constantName);
             if (constantExpressionPair != this->doubleUndefinedConstantExpressions.end()) {
                 return constantExpressionPair->second;
@@ -203,22 +269,22 @@ namespace storm {
             }
         }
         
-        std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> const& Program::getBooleanUndefinedConstantExpressionsMap() const {
+        std::map<std::string, std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>> const& Program::getBooleanUndefinedConstantExpressionsMap() const {
             return this->booleanUndefinedConstantExpressions;
         }
         
-        std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> const& Program::getIntegerUndefinedConstantExpressionsMap() const {
+        std::map<std::string, std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>> const& Program::getIntegerUndefinedConstantExpressionsMap() const {
             return this->integerUndefinedConstantExpressions;
         }
-
-        std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> const& Program::getDoubleUndefinedConstantExpressionsMap() const {
+        
+        std::map<std::string, std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>> const& Program::getDoubleUndefinedConstantExpressionsMap() const {
             return this->doubleUndefinedConstantExpressions;
         }
         
         uint_fast64_t Program::getGlobalIndexOfBooleanVariable(std::string const& variableName) const {
             return this->globalBooleanVariableToIndexMap.at(variableName);
         }
-
+        
         uint_fast64_t Program::getGlobalIndexOfIntegerVariable(std::string const& variableName) const {
             return this->globalIntegerVariableToIndexMap.at(variableName);
         }
diff --git a/src/ir/Program.h b/src/ir/Program.h
index 6789edaae..2ddf31da3 100644
--- a/src/ir/Program.h
+++ b/src/ir/Program.h
@@ -60,16 +60,30 @@ namespace storm {
              * @param labels The labels defined for this model.
              */
             Program(ModelType modelType,
-                    std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> const& booleanUndefinedConstantExpressions,
-                    std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> const& integerUndefinedConstantExpressions,
-                    std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> const& doubleUndefinedConstantExpressions,
+                    std::map<std::string, std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>> const& booleanUndefinedConstantExpressions,
+                    std::map<std::string, std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>> const& integerUndefinedConstantExpressions,
+                    std::map<std::string, std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>> const& doubleUndefinedConstantExpressions,
                     std::vector<BooleanVariable> const& globalBooleanVariables,
                     std::vector<IntegerVariable> const& globalIntegerVariables,
                     std::map<std::string, uint_fast64_t> const& globalBooleanVariableToIndexMap,
                     std::map<std::string, uint_fast64_t> const& globalIntegerVariableToIndexMap,
                     std::vector<storm::ir::Module> const& modules,
                     std::map<std::string, storm::ir::RewardModel> const& rewards,
-                    std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> const& labels);
+                    std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& labels);
+            
+            /*!
+             * Performs a deep-copy of the given program.
+             *
+             * @param otherProgram The program to copy.
+             */
+            Program(Program const& otherProgram);
+
+            /*!
+             * Performs a deep-copy of the given program and assigns it to the current one.
+             *
+             * @param otherProgram The program to assign.
+             */
+            Program& operator=(Program const& otherProgram);
             
             /*!
              * Retrieves the number of modules in the program.
@@ -165,7 +179,7 @@ namespace storm {
              *
              * @return A set of labels that are defined in the program.
              */
-            std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> const& getLabels() const;
+            std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> const& getLabels() const;
             
             /*!
              * Retrieves whether the given constant name is an undefined boolean constant of the program.
@@ -180,7 +194,7 @@ namespace storm {
              * @param constantName The name of the undefined boolean constant for which to retrieve the expression.
              * @return The expression associated with the given undefined boolean constant.
              */
-            std::shared_ptr<storm::ir::expressions::BooleanConstantExpression> getUndefinedBooleanConstantExpression(std::string const& constantName) const;
+            std::unique_ptr<storm::ir::expressions::BooleanConstantExpression> const& getUndefinedBooleanConstantExpression(std::string const& constantName) const;
             
             /*!
              * Retrieves whether the given constant name is an undefined integer constant of the program.
@@ -195,7 +209,7 @@ namespace storm {
              * @param constantName The name of the undefined integer constant for which to retrieve the expression.
              * @return The expression associated with the given undefined integer constant.
              */
-            std::shared_ptr<storm::ir::expressions::IntegerConstantExpression> getUndefinedIntegerConstantExpression(std::string const& constantName) const;
+            std::unique_ptr<storm::ir::expressions::IntegerConstantExpression> const& getUndefinedIntegerConstantExpression(std::string const& constantName) const;
 
             /*!
              * Retrieves whether the given constant name is an undefined double constant of the program.
@@ -210,28 +224,28 @@ namespace storm {
              * @param constantName The name of the undefined double constant for which to retrieve the expression.
              * @return The expression associated with the given undefined double constant.
              */
-            std::shared_ptr<storm::ir::expressions::DoubleConstantExpression> getUndefinedDoubleConstantExpression(std::string const& constantName) const;
+            std::unique_ptr<storm::ir::expressions::DoubleConstantExpression> const& getUndefinedDoubleConstantExpression(std::string const& constantName) const;
             
             /*!
              * Retrieves the mapping of undefined boolean constant names to their expression objects.
              *
              * @return The mapping of undefined boolean constant names to their expression objects.
              */
-            std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> const& getBooleanUndefinedConstantExpressionsMap() const;
+            std::map<std::string, std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>> const& getBooleanUndefinedConstantExpressionsMap() const;
 
             /*!
              * Retrieves the mapping of undefined integer constant names to their expression objects.
              *
              * @return The mapping of undefined integer constant names to their expression objects.
              */
-            std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> const& getIntegerUndefinedConstantExpressionsMap() const;
+            std::map<std::string, std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>> const& getIntegerUndefinedConstantExpressionsMap() const;
 
             /*!
              * Retrieves the mapping of undefined double constant names to their expression objects.
              *
              * @return The mapping of undefined double constant names to their expression objects.
              */
-            std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> const& getDoubleUndefinedConstantExpressionsMap() const;
+            std::map<std::string, std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>> const& getDoubleUndefinedConstantExpressionsMap() const;
             
             /*!
              * Retrieves the global index of the given boolean variable.
@@ -252,13 +266,13 @@ namespace storm {
             ModelType modelType;
             
             // A map of undefined boolean constants to their expression nodes.
-            std::map<std::string, std::shared_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions;
+            std::map<std::string, std::unique_ptr<storm::ir::expressions::BooleanConstantExpression>> booleanUndefinedConstantExpressions;
             
             // A map of undefined integer constants to their expressions nodes.
-            std::map<std::string, std::shared_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions;
+            std::map<std::string, std::unique_ptr<storm::ir::expressions::IntegerConstantExpression>> integerUndefinedConstantExpressions;
             
             // A map of undefined double constants to their expressions nodes.
-            std::map<std::string, std::shared_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions;
+            std::map<std::string, std::unique_ptr<storm::ir::expressions::DoubleConstantExpression>> doubleUndefinedConstantExpressions;
             
             // A list of global boolean variables.
             std::vector<BooleanVariable> globalBooleanVariables;
@@ -279,7 +293,7 @@ namespace storm {
             std::map<std::string, storm::ir::RewardModel> rewards;
             
             // The labels that are defined for this model.
-            std::map<std::string, std::shared_ptr<storm::ir::expressions::BaseExpression>> labels;
+            std::map<std::string, std::unique_ptr<storm::ir::expressions::BaseExpression>> labels;
             
             // The set of actions present in this program.
             std::set<std::string> actions;
diff --git a/src/ir/StateReward.cpp b/src/ir/StateReward.cpp
index 605afcb21..ff3c815ce 100644
--- a/src/ir/StateReward.cpp
+++ b/src/ir/StateReward.cpp
@@ -10,31 +10,51 @@
 #include "StateReward.h"
 
 namespace storm {
-
-namespace ir {
-
-StateReward::StateReward() : statePredicate(), rewardValue() {
-	// Nothing to do here.
-}
-
-StateReward::StateReward(std::shared_ptr<storm::ir::expressions::BaseExpression> const& statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> const& rewardValue) : statePredicate(statePredicate), rewardValue(rewardValue) {
-	// Nothing to do here.
-}
-
-std::string StateReward::toString() const {
-	std::stringstream result;
-	result << "\t" << statePredicate->toString() << ": " << rewardValue->toString() << ";";
-	return result.str();
-}
-    
-std::shared_ptr<storm::ir::expressions::BaseExpression> StateReward::getStatePredicate() const {
-    return this->statePredicate;
-}
-
-std::shared_ptr<storm::ir::expressions::BaseExpression> StateReward::getRewardValue() const {
-    return this->rewardValue;
-}
-    
-} // namespace ir
-
+    namespace ir {
+        
+        StateReward::StateReward() : statePredicate(), rewardValue() {
+            // Nothing to do here.
+        }
+        
+        StateReward::StateReward(std::unique_ptr<storm::ir::expressions::BaseExpression>&& statePredicate, std::unique_ptr<storm::ir::expressions::BaseExpression>&& rewardValue) : statePredicate(std::move(statePredicate)), rewardValue(std::move(rewardValue)) {
+            // Nothing to do here.
+        }
+        
+        StateReward::StateReward(StateReward const& otherReward) {
+            if (otherReward.statePredicate != nullptr) {
+                statePredicate = otherReward.statePredicate->clone();
+            }
+            if (otherReward.rewardValue != nullptr) {
+                rewardValue = otherReward.rewardValue->clone();
+            }
+        }
+        
+        StateReward& StateReward::operator=(StateReward const& otherReward) {
+            if (this != & otherReward) {
+                if (otherReward.statePredicate != nullptr) {
+                    this->statePredicate = otherReward.statePredicate->clone();
+                }
+                if (otherReward.rewardValue != nullptr) {
+                    this->rewardValue = otherReward.rewardValue->clone();
+                }
+            }
+            
+            return *this;
+        }
+        
+        std::string StateReward::toString() const {
+            std::stringstream result;
+            result << "\t" << statePredicate->toString() << ": " << rewardValue->toString() << ";";
+            return result.str();
+        }
+        
+        std::unique_ptr<storm::ir::expressions::BaseExpression> const& StateReward::getStatePredicate() const {
+            return this->statePredicate;
+        }
+        
+        std::unique_ptr<storm::ir::expressions::BaseExpression> const& StateReward::getRewardValue() const {
+            return this->rewardValue;
+        }
+        
+    } // namespace ir
 } // namespace storm
diff --git a/src/ir/StateReward.h b/src/ir/StateReward.h
index 633c8c635..117544d6d 100644
--- a/src/ir/StateReward.h
+++ b/src/ir/StateReward.h
@@ -13,61 +13,73 @@
 #include "expressions/BaseExpression.h"
 
 namespace storm {
+    namespace ir {
+        
+        /*!
+         * A class representing a state reward.
+         */
+        class StateReward {
+        public:
+            /*!
+             * Default constructor. Creates an empty state reward.
+             */
+            StateReward();
+            
+            /*!
+             * Creates a state reward for the states satisfying the given expression with the value given
+             * by a second expression.
+             *
+             * @param statePredicate The predicate that states earning this state-based reward need to
+             * satisfy.
+             * @param rewardValue An expression specifying the values of the rewards to attach to the
+             * states.
+             */
+            StateReward(std::unique_ptr<storm::ir::expressions::BaseExpression>&& statePredicate, std::unique_ptr<storm::ir::expressions::BaseExpression>&& rewardValue);
+            
+            /*!
+             * Performs a deep-copy of the given reward.
+             *
+             * @param otherReward The reward to copy.
+             */
+            StateReward(StateReward const& otherReward);
 
-namespace ir {
-
-/*!
- * A class representing a state reward.
- */
-class StateReward {
-public:
-	/*!
-	 * Default constructor. Creates an empty state reward.
-	 */
-	StateReward();
-
-	/*!
-	 * Creates a state reward for the states satisfying the given expression with the value given
-	 * by a second expression.
-     *
-	 * @param statePredicate The predicate that states earning this state-based reward need to
-	 * satisfy.
-	 * @param rewardValue An expression specifying the values of the rewards to attach to the
-	 * states.
-	 */
-	StateReward(std::shared_ptr<storm::ir::expressions::BaseExpression> const& statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> const& rewardValue);
-
-	/*!
-	 * Retrieves a string representation of this state reward.
-     *
-	 * @return A string representation of this state reward.
-	 */
-	std::string toString() const;
-    
-    /*!
-     * Retrieves the state predicate that is associated with this state reward.
-     *
-     * @return The state predicate that is associated with this state reward.
-     */
-    std::shared_ptr<storm::ir::expressions::BaseExpression> getStatePredicate() const;
-    
-    /*!
-     * Retrieves the reward value associated with this state reward.
-     *
-     * @return The reward value associated with this state reward.
-     */
-    std::shared_ptr<storm::ir::expressions::BaseExpression> getRewardValue() const;
-    
-private:
-	// The predicate that characterizes the states that obtain this reward.
-	std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate;
-
-	// The expression that specifies the value of the reward obtained.
-	std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue;
-};
-
-} // namespace ir
-
+            /*!
+             * Performs a deep-copy of the given reward and assigns it to the current one.
+             *
+             * @param otherReward The reward to assign.
+             */
+            StateReward& operator=(StateReward const& otherReward);
+            
+            /*!
+             * Retrieves a string representation of this state reward.
+             *
+             * @return A string representation of this state reward.
+             */
+            std::string toString() const;
+            
+            /*!
+             * Retrieves the state predicate that is associated with this state reward.
+             *
+             * @return The state predicate that is associated with this state reward.
+             */
+            std::unique_ptr<storm::ir::expressions::BaseExpression> const& getStatePredicate() const;
+            
+            /*!
+             * Retrieves the reward value associated with this state reward.
+             *
+             * @return The reward value associated with this state reward.
+             */
+            std::unique_ptr<storm::ir::expressions::BaseExpression> const& getRewardValue() const;
+            
+        private:
+            // The predicate that characterizes the states that obtain this reward.
+            std::unique_ptr<storm::ir::expressions::BaseExpression> statePredicate;
+            
+            // The expression that specifies the value of the reward obtained.
+            std::unique_ptr<storm::ir::expressions::BaseExpression> rewardValue;
+        };
+        
+    } // namespace ir
 } // namespace storm
 
 #endif /* STORM_IR_STATEREWARD_H_ */
diff --git a/src/ir/TransitionReward.cpp b/src/ir/TransitionReward.cpp
index 60e504984..bd9664529 100644
--- a/src/ir/TransitionReward.cpp
+++ b/src/ir/TransitionReward.cpp
@@ -10,35 +10,56 @@
 #include "TransitionReward.h"
 
 namespace storm {
-
-namespace ir {
-
-TransitionReward::TransitionReward() : commandName(), statePredicate(), rewardValue() {
-	// Nothing to do here.
-}
-
-TransitionReward::TransitionReward(std::string const& commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> const& rewardValue) : commandName(commandName), statePredicate(statePredicate), rewardValue(rewardValue) {
-	// Nothing to do here.
-}
-
-std::string TransitionReward::toString() const {
-	std::stringstream result;
-	result << "\t[" << commandName << "] " << statePredicate->toString() << ": " << rewardValue->toString() << ";";
-	return result.str();
-}
-
-std::string const& TransitionReward::getActionName() const {
-    return this->commandName;
-}
-    
-std::shared_ptr<storm::ir::expressions::BaseExpression> TransitionReward::getStatePredicate() const {
-    return this->statePredicate;
-}
-    
-std::shared_ptr<storm::ir::expressions::BaseExpression> TransitionReward::getRewardValue() const {
-    return this->rewardValue;
-}
-    
-} // namespace ir
-
+    namespace ir {
+        
+        TransitionReward::TransitionReward() : commandName(), statePredicate(), rewardValue() {
+            // Nothing to do here.
+        }
+        
+        TransitionReward::TransitionReward(std::string const& commandName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& statePredicate, std::unique_ptr<storm::ir::expressions::BaseExpression>&& rewardValue) : commandName(commandName), statePredicate(std::move(statePredicate)), rewardValue(std::move(rewardValue)) {
+            // Nothing to do here.
+        }
+        
+        TransitionReward::TransitionReward(TransitionReward const& otherReward) : commandName(otherReward.commandName), statePredicate(), rewardValue() {
+            if (otherReward.statePredicate != nullptr) {
+                statePredicate = otherReward.statePredicate->clone();
+            }
+            if (otherReward.rewardValue != nullptr) {
+                rewardValue = otherReward.rewardValue->clone();
+            }
+        }
+        
+        TransitionReward& TransitionReward::operator=(TransitionReward const& otherReward) {
+            if (this != &otherReward) {
+                this->commandName = otherReward.commandName;
+                if (otherReward.statePredicate != nullptr) {
+                    this->statePredicate = otherReward.statePredicate->clone();
+                }
+                if (otherReward.rewardValue != nullptr) {
+                    this->rewardValue = otherReward.rewardValue->clone();
+                }
+            }
+            
+            return *this;
+        }
+        
+        std::string TransitionReward::toString() const {
+            std::stringstream result;
+            result << "\t[" << commandName << "] " << statePredicate->toString() << ": " << rewardValue->toString() << ";";
+            return result.str();
+        }
+        
+        std::string const& TransitionReward::getActionName() const {
+            return this->commandName;
+        }
+        
+        std::unique_ptr<storm::ir::expressions::BaseExpression> const& TransitionReward::getStatePredicate() const {
+            return this->statePredicate;
+        }
+        
+        std::unique_ptr<storm::ir::expressions::BaseExpression> const& TransitionReward::getRewardValue() const {
+            return this->rewardValue;
+        }
+        
+    } // namespace ir
 } // namespace storm
diff --git a/src/ir/TransitionReward.h b/src/ir/TransitionReward.h
index 479810755..298d17024 100644
--- a/src/ir/TransitionReward.h
+++ b/src/ir/TransitionReward.h
@@ -36,8 +36,22 @@ public:
 	 * @param rewardValue An expression specifying the values of the rewards to attach to the
 	 * transitions.
 	 */
-	TransitionReward(std::string const& commandName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& statePredicate, std::shared_ptr<storm::ir::expressions::BaseExpression> const& rewardValue);
+	TransitionReward(std::string const& commandName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& statePredicate, std::unique_ptr<storm::ir::expressions::BaseExpression>&& rewardValue);
 
+    /*!
+     * Performs a deep-copy of the given transition reward.
+     *
+     * @param otherReward The transition reward to copy.
+     */
+    TransitionReward(TransitionReward const& otherReward);
+    
+    /*!
+     * Performs a deep-copy of the given transition reward and assigns it to the current one.
+     *
+     * @param otherReward The reward to assign.
+     */
+    TransitionReward& operator=(TransitionReward const& otherReward);
+    
 	/*!
 	 * Retrieves a string representation of this transition reward.
      *
@@ -57,14 +71,14 @@ public:
      *
      * @return The state predicate that is associated with this state reward.
      */
-    std::shared_ptr<storm::ir::expressions::BaseExpression> getStatePredicate() const;
+    std::unique_ptr<storm::ir::expressions::BaseExpression> const& getStatePredicate() const;
     
     /*!
      * Retrieves the reward value associated with this state reward.
      *
      * @return The reward value associated with this state reward.
      */
-    std::shared_ptr<storm::ir::expressions::BaseExpression> getRewardValue() const;
+    std::unique_ptr<storm::ir::expressions::BaseExpression> const& getRewardValue() const;
 
 private:
 	// The name of the command this transition-based reward is attached to.
@@ -72,10 +86,10 @@ private:
 
 	// A predicate that needs to be satisfied by states for the reward to be obtained (by taking
 	// a corresponding command transition).
-	std::shared_ptr<storm::ir::expressions::BaseExpression> statePredicate;
+	std::unique_ptr<storm::ir::expressions::BaseExpression> statePredicate;
 
 	// The expression specifying the value of the reward obtained along the transitions.
-	std::shared_ptr<storm::ir::expressions::BaseExpression> rewardValue;
+	std::unique_ptr<storm::ir::expressions::BaseExpression> rewardValue;
 };
 
 } // namespace ir
diff --git a/src/ir/Update.cpp b/src/ir/Update.cpp
index 08728bd4c..aac7b3ca0 100644
--- a/src/ir/Update.cpp
+++ b/src/ir/Update.cpp
@@ -18,8 +18,8 @@ namespace storm {
             // Nothing to do here.
         }
         
-        Update::Update(uint_fast64_t globalIndex, std::shared_ptr<storm::ir::expressions::BaseExpression> const& likelihoodExpression, std::map<std::string, storm::ir::Assignment> const& booleanAssignments, std::map<std::string, storm::ir::Assignment> const& integerAssignments)
-        : likelihoodExpression(likelihoodExpression), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments), globalIndex(globalIndex) {
+        Update::Update(uint_fast64_t globalIndex, std::unique_ptr<storm::ir::expressions::BaseExpression>&& likelihoodExpression, std::map<std::string, storm::ir::Assignment> const& booleanAssignments, std::map<std::string, storm::ir::Assignment> const& integerAssignments)
+        : likelihoodExpression(std::move(likelihoodExpression)), booleanAssignments(booleanAssignments), integerAssignments(integerAssignments), globalIndex(globalIndex) {
             // Nothing to do here.
         }
         
@@ -41,7 +41,26 @@ namespace storm {
             this->likelihoodExpression = update.likelihoodExpression->clone(renaming, variableState);
         }
         
-        std::shared_ptr<storm::ir::expressions::BaseExpression> const& Update::getLikelihoodExpression() const {
+        Update::Update(Update const& otherUpdate) : likelihoodExpression(), booleanAssignments(otherUpdate.booleanAssignments), integerAssignments(otherUpdate.integerAssignments), globalIndex(otherUpdate.globalIndex) {
+            if (otherUpdate.likelihoodExpression != nullptr) {
+                likelihoodExpression = otherUpdate.likelihoodExpression->clone();
+            }
+        }
+        
+        Update& Update::operator=(Update const& otherUpdate) {
+            if (this != &otherUpdate) {
+                if (otherUpdate.likelihoodExpression != nullptr) {
+                    this->likelihoodExpression = otherUpdate.likelihoodExpression->clone();
+                }
+                this->booleanAssignments = otherUpdate.booleanAssignments;
+                this->integerAssignments = otherUpdate.integerAssignments;
+                this->globalIndex = otherUpdate.globalIndex;
+            }
+            
+            return *this;
+        }
+        
+        std::unique_ptr<storm::ir::expressions::BaseExpression> const& Update::getLikelihoodExpression() const {
             return likelihoodExpression;
         }
         
diff --git a/src/ir/Update.h b/src/ir/Update.h
index 88bdd4c16..07b9a7d24 100644
--- a/src/ir/Update.h
+++ b/src/ir/Update.h
@@ -42,7 +42,7 @@ namespace storm {
              * @param likelihoodExpression An expression specifying the likelihood of this update.
              * @param assignments A map of variable names to their assignments.
              */
-            Update(uint_fast64_t globalIndex, std::shared_ptr<storm::ir::expressions::BaseExpression> const& likelihoodExpression, std::map<std::string, storm::ir::Assignment> const& booleanAssignments, std::map<std::string, storm::ir::Assignment> const& integerAssignments);
+            Update(uint_fast64_t globalIndex, std::unique_ptr<storm::ir::expressions::BaseExpression>&& likelihoodExpression, std::map<std::string, storm::ir::Assignment> const& booleanAssignments, std::map<std::string, storm::ir::Assignment> const& integerAssignments);
             
             /*!
              * Creates a copy of the given update and performs the provided renaming.
@@ -55,12 +55,26 @@ namespace storm {
              */
             Update(Update const& update, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState& variableState);
             
+            /*!
+             * Peforms a deep-copy of the given update.
+             *
+             * @param otherUpdate The update to copy.
+             */
+            Update(Update const& otherUpdate);
+            
+            /*!
+             * Performs a deep-copy of the given update and assigns it to the current one.
+             *
+             * @param otherUpdate The update to assign.
+             */
+            Update& operator=(Update const& otherUpdate);
+            
             /*!
              * Retrieves the expression for the likelihood of this update.
              *
              * @return The expression for the likelihood of this update.
              */
-            std::shared_ptr<storm::ir::expressions::BaseExpression> const& getLikelihoodExpression() const;
+            std::unique_ptr<storm::ir::expressions::BaseExpression> const& getLikelihoodExpression() const;
             
             /*!
              * Retrieves the number of boolean assignments associated with this update.
@@ -120,7 +134,7 @@ namespace storm {
             
         private:
             // An expression specifying the likelihood of taking this update.
-            std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression;
+            std::unique_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression;
             
             // A mapping of boolean variable names to their assignments in this update.
             std::map<std::string, storm::ir::Assignment> booleanAssignments;
diff --git a/src/ir/Variable.cpp b/src/ir/Variable.cpp
index 7a7fe7cf8..83cb2a33a 100644
--- a/src/ir/Variable.cpp
+++ b/src/ir/Variable.cpp
@@ -19,18 +19,37 @@ namespace storm {
             // Nothing to do here.
         }
         
-        Variable::Variable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue)
-        : localIndex(localIndex), globalIndex(globalIndex), variableName(variableName), initialValue(initialValue) {
+        Variable::Variable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue)
+        : localIndex(localIndex), globalIndex(globalIndex), variableName(variableName), initialValue(std::move(initialValue)) {
             // Nothing to do here.
         }
         
+        Variable::Variable(Variable const& otherVariable) : localIndex(otherVariable.localIndex), globalIndex(otherVariable.globalIndex), variableName(otherVariable.variableName), initialValue() {
+            if (otherVariable.initialValue != nullptr) {
+                initialValue = otherVariable.initialValue->clone();
+            }
+        }
+        
         Variable::Variable(Variable const& var, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState)
-        : localIndex(var.getLocalIndex()), globalIndex(newGlobalIndex), variableName(newName) {
+        : localIndex(var.getLocalIndex()), globalIndex(newGlobalIndex), variableName(newName), initialValue() {
             if (var.initialValue != nullptr) {
                 this->initialValue = var.initialValue->clone(renaming, variableState);
             }
         }
         
+        Variable& Variable::operator=(Variable const& otherVariable) {
+            if (this != &otherVariable) {
+                this->localIndex = otherVariable.localIndex;
+                this->globalIndex = otherVariable.globalIndex;
+                this->variableName = otherVariable.variableName;
+                if (otherVariable.initialValue != nullptr) {
+                    this->initialValue = otherVariable.initialValue->clone();
+                }
+            }
+            
+            return *this;
+        }
+        
         std::string const& Variable::getName() const {
             return variableName;
         }
@@ -43,12 +62,12 @@ namespace storm {
             return localIndex;
         }
         
-        std::shared_ptr<storm::ir::expressions::BaseExpression> const& Variable::getInitialValue() const {
+        std::unique_ptr<storm::ir::expressions::BaseExpression> const& Variable::getInitialValue() const {
             return initialValue;
         }
         
-        void Variable::setInitialValue(std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue) {
-            this->initialValue = initialValue;
+        void Variable::setInitialValue(std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue) {
+            this->initialValue = std::move(initialValue);
         }
         
     } // namespace ir
diff --git a/src/ir/Variable.h b/src/ir/Variable.h
index 36bb6e669..53b2f3b98 100644
--- a/src/ir/Variable.h
+++ b/src/ir/Variable.h
@@ -41,7 +41,7 @@ namespace storm {
              * @param variableName the name of the variable.
              * @param initialValue the expression that defines the initial value of the variable.
              */
-            Variable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>());
+            Variable(uint_fast64_t localIndex, uint_fast64_t globalIndex, std::string const& variableName, std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue = nullptr);
             
             /*!
              * Creates a copy of the given variable and performs the provided renaming.
@@ -55,6 +55,18 @@ namespace storm {
              */
             Variable(Variable const& oldVariable, std::string const& newName, uint_fast64_t newGlobalIndex, std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState);
             
+            /*!
+             * Creates a deep-copy of the given variable.
+             *
+             * @param otherVariable The variable to copy.
+             */
+            Variable(Variable const& otherVariable);
+            
+            /*!
+             * Creates a deep-copy of the given variable and assigns it to the current one.
+             */
+            Variable& operator=(Variable const& otherVariable);
+            
             /*!
              * Retrieves the name of the variable.
              *
@@ -83,14 +95,14 @@ namespace storm {
              *
              * @return The expression defining the initial value of the variable.
              */
-            std::shared_ptr<storm::ir::expressions::BaseExpression> const& getInitialValue() const;
+            std::unique_ptr<storm::ir::expressions::BaseExpression> const& getInitialValue() const;
             
             /*!
              * Sets the initial value to the given expression.
              *
              * @param initialValue The new initial value.
              */
-            void setInitialValue(std::shared_ptr<storm::ir::expressions::BaseExpression> const& initialValue);
+            void setInitialValue(std::unique_ptr<storm::ir::expressions::BaseExpression>&& initialValue);
             
         private:
             // A unique (among the variables of equal type) index for the variable inside its module.
@@ -103,7 +115,7 @@ namespace storm {
             std::string variableName;
             
             // The expression defining the initial value of the variable.
-            std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue;
+            std::unique_ptr<storm::ir::expressions::BaseExpression> initialValue;
         };
         
     } // namespace ir
diff --git a/src/ir/expressions/BaseExpression.h b/src/ir/expressions/BaseExpression.h
index 636799f0d..2125287cd 100644
--- a/src/ir/expressions/BaseExpression.h
+++ b/src/ir/expressions/BaseExpression.h
@@ -69,7 +69,7 @@ namespace storm {
                  *
                  * @return A deep-copy of the expression.
                  */
-                virtual std::shared_ptr<BaseExpression> clone() const = 0;
+                virtual std::unique_ptr<BaseExpression> clone() const = 0;
                 
                 /*!
                  * Copies the expression tree underneath (including) the current node and performs the provided renaming.
@@ -77,7 +77,7 @@ namespace storm {
                  * @param renaming A mapping from identifier names to strings they are to be replaced with.
                  * @param variableState An object knowing about the global variable state.
                  */
-                virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const = 0;
+                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const = 0;
                                 
                 /*!
                  * Retrieves the value of the expression as an integer given the provided variable valuation.
diff --git a/src/ir/expressions/BinaryBooleanFunctionExpression.cpp b/src/ir/expressions/BinaryBooleanFunctionExpression.cpp
index 0bbbd647c..c55af9b38 100644
--- a/src/ir/expressions/BinaryBooleanFunctionExpression.cpp
+++ b/src/ir/expressions/BinaryBooleanFunctionExpression.cpp
@@ -13,8 +13,8 @@ namespace storm {
     namespace ir {
         namespace expressions {
             
-            BinaryBooleanFunctionExpression::BinaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right, FunctionType functionType)
-            : BinaryExpression(bool_, left, right), functionType(functionType) {
+            BinaryBooleanFunctionExpression::BinaryBooleanFunctionExpression(std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, FunctionType functionType)
+            : BinaryExpression(bool_, std::move(left), std::move(right)), functionType(functionType) {
                 // Nothing to do here.
             }
             
@@ -23,12 +23,12 @@ namespace storm {
                 // Nothing to do here.
             }
 
-            std::shared_ptr<BaseExpression> BinaryBooleanFunctionExpression::clone() const {
-                return std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(this->getLeft()->clone(), this->getRight()->clone(), functionType));
+            std::unique_ptr<BaseExpression> BinaryBooleanFunctionExpression::clone() const {
+                return std::unique_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(this->getLeft()->clone(), this->getRight()->clone(), functionType));
             }
             
-            std::shared_ptr<BaseExpression> BinaryBooleanFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->functionType));
+            std::unique_ptr<BaseExpression> BinaryBooleanFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
+                return std::unique_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->functionType));
             }
             
             bool BinaryBooleanFunctionExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
diff --git a/src/ir/expressions/BinaryBooleanFunctionExpression.h b/src/ir/expressions/BinaryBooleanFunctionExpression.h
index d637dd5a0..b0cec5906 100644
--- a/src/ir/expressions/BinaryBooleanFunctionExpression.h
+++ b/src/ir/expressions/BinaryBooleanFunctionExpression.h
@@ -31,7 +31,7 @@ namespace storm {
                  * @param right The right child of the node.
                  * @param functionType The operator that is to be applied to the two children.
                  */
-                BinaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right, FunctionType functionType);
+                BinaryBooleanFunctionExpression(std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, FunctionType functionType);
                 
                 /*!
                  * Copy-constructs from the given expression.
@@ -40,9 +40,9 @@ namespace storm {
                  */
                 BinaryBooleanFunctionExpression(BinaryBooleanFunctionExpression const& binaryBooleanFunctionExpression);
                 
-                virtual std::shared_ptr<BaseExpression> clone() const override;
+                virtual std::unique_ptr<BaseExpression> clone() const override;
                 
-                virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
+                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
                 
diff --git a/src/ir/expressions/BinaryExpression.cpp b/src/ir/expressions/BinaryExpression.cpp
index 10c623757..5ca3e186b 100644
--- a/src/ir/expressions/BinaryExpression.cpp
+++ b/src/ir/expressions/BinaryExpression.cpp
@@ -11,20 +11,20 @@ namespace storm {
     namespace ir {
         namespace expressions {
             
-            BinaryExpression::BinaryExpression(ReturnType type, std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right)
-            : BaseExpression(type), left(left), right(right) {
+            BinaryExpression::BinaryExpression(ReturnType type, std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right)
+            : BaseExpression(type), left(std::move(left)), right(std::move(right)) {
                 // Nothing to do here.
             }
             
-            BinaryExpression::BinaryExpression(BinaryExpression const& binaryExpression) : BaseExpression(binaryExpression.getType()), left(binaryExpression.left), right(binaryExpression.right) {
+            BinaryExpression::BinaryExpression(BinaryExpression const& binaryExpression) : BaseExpression(binaryExpression.getType()), left(binaryExpression.left->clone()), right(binaryExpression.right->clone()) {
                 // Nothing to do here.
             }
 
-            std::shared_ptr<BaseExpression> const& BinaryExpression::getLeft() const {
+            std::unique_ptr<BaseExpression> const& BinaryExpression::getLeft() const {
                 return left;
             }
             
-            std::shared_ptr<BaseExpression> const& BinaryExpression::getRight() const {
+            std::unique_ptr<BaseExpression> const& BinaryExpression::getRight() const {
                 return right;
             }
             
diff --git a/src/ir/expressions/BinaryExpression.h b/src/ir/expressions/BinaryExpression.h
index 655d597b6..e730aaebb 100644
--- a/src/ir/expressions/BinaryExpression.h
+++ b/src/ir/expressions/BinaryExpression.h
@@ -25,7 +25,7 @@ namespace storm {
                  * @param left The left child of the binary expression.
                  * @param right The right child of the binary expression.
                  */
-                BinaryExpression(ReturnType type, std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right);
+                BinaryExpression(ReturnType type, std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right);
                 
                 /*!
                  * Copy-constructs from the given expression.
@@ -39,21 +39,21 @@ namespace storm {
                  *
                  * @return The left child of the expression node.
                  */
-                std::shared_ptr<BaseExpression> const& getLeft() const;
+                std::unique_ptr<BaseExpression> const& getLeft() const;
                 
                 /*!
                  * Retrieves the right child of the expression node.
                  *
                  * @return The right child of the expression node.
                  */
-                std::shared_ptr<BaseExpression> const& getRight() const;
+                std::unique_ptr<BaseExpression> const& getRight() const;
                 
             private:
                 // The left child of the binary expression.
-                std::shared_ptr<BaseExpression> left;
+                std::unique_ptr<BaseExpression> left;
                 
                 // The right child of the binary expression.
-                std::shared_ptr<BaseExpression> right;
+                std::unique_ptr<BaseExpression> right;
             };
             
         } // namespace expressions
diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.cpp b/src/ir/expressions/BinaryNumericalFunctionExpression.cpp
index 3cd85c5e4..e11d82538 100644
--- a/src/ir/expressions/BinaryNumericalFunctionExpression.cpp
+++ b/src/ir/expressions/BinaryNumericalFunctionExpression.cpp
@@ -13,8 +13,8 @@ namespace storm {
     namespace ir {
         namespace expressions {
             
-            BinaryNumericalFunctionExpression::BinaryNumericalFunctionExpression(ReturnType type, std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right, FunctionType functionType)
-            : BinaryExpression(type, left, right), functionType(functionType) {
+            BinaryNumericalFunctionExpression::BinaryNumericalFunctionExpression(ReturnType type, std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, FunctionType functionType)
+            : BinaryExpression(type, std::move(left), std::move(right)), functionType(functionType) {
                 // Nothing to do here.
             }
             
@@ -23,12 +23,12 @@ namespace storm {
                 // Nothing to do here.
             }
 
-            std::shared_ptr<BaseExpression> BinaryNumericalFunctionExpression::clone() const {
-                return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(), this->getRight()->clone(), functionType));
+            std::unique_ptr<BaseExpression> BinaryNumericalFunctionExpression::clone() const {
+                return std::unique_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(), this->getRight()->clone(), functionType));
             }
 
-            std::shared_ptr<BaseExpression> BinaryNumericalFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->functionType));
+            std::unique_ptr<BaseExpression> BinaryNumericalFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
+                return std::unique_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->functionType));
             }
             
             BinaryNumericalFunctionExpression::FunctionType BinaryNumericalFunctionExpression::getFunctionType() const {
diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.h b/src/ir/expressions/BinaryNumericalFunctionExpression.h
index f4939d2a8..32b6b45fd 100644
--- a/src/ir/expressions/BinaryNumericalFunctionExpression.h
+++ b/src/ir/expressions/BinaryNumericalFunctionExpression.h
@@ -32,18 +32,18 @@ namespace storm {
                  * @param right The right child of the  expression tree node.
                  * @param functionType The function that is applied to the children of this node.
                  */
-                BinaryNumericalFunctionExpression(ReturnType type, std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right, FunctionType functionType);
+                BinaryNumericalFunctionExpression(ReturnType type, std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, FunctionType functionType);
                 
                 /*!
-                 * Copy-constructs from the given expression.
+                 * Performs a deep-copy of the given expression.
                  *
                  * @param binaryNumericalFunctionExpression The expression to copy.
                  */
                 BinaryNumericalFunctionExpression(BinaryNumericalFunctionExpression const& binaryNumericalFunctionExpression);
 
-                virtual std::shared_ptr<BaseExpression> clone() const override;
+                virtual std::unique_ptr<BaseExpression> clone() const override;
                 
-                virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
+                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 /*!
                  * Retrieves the operator that is associated with this node.
diff --git a/src/ir/expressions/BinaryRelationExpression.cpp b/src/ir/expressions/BinaryRelationExpression.cpp
index af51dadb8..87ef42141 100644
--- a/src/ir/expressions/BinaryRelationExpression.cpp
+++ b/src/ir/expressions/BinaryRelationExpression.cpp
@@ -13,8 +13,8 @@ namespace storm {
     namespace ir {
         namespace expressions {
             
-            BinaryRelationExpression::BinaryRelationExpression(std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right, RelationType relationType)
-            : BinaryExpression(bool_, left, right), relationType(relationType) {
+            BinaryRelationExpression::BinaryRelationExpression(std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, RelationType relationType)
+            : BinaryExpression(bool_, std::move(left), std::move(right)), relationType(relationType) {
                 // Nothing to do here.
             }
             
@@ -23,12 +23,12 @@ namespace storm {
                 // Nothing to do here.
             }
             
-            std::shared_ptr<BaseExpression> BinaryRelationExpression::clone() const {
-                return std::shared_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(), this->getRight()->clone(), relationType));
+            std::unique_ptr<BaseExpression> BinaryRelationExpression::clone() const {
+                return std::unique_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(), this->getRight()->clone(), relationType));
             }
 
-            std::shared_ptr<BaseExpression> BinaryRelationExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::shared_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->relationType));
+            std::unique_ptr<BaseExpression> BinaryRelationExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
+                return std::unique_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(renaming, variableState), this->getRight()->clone(renaming, variableState), this->relationType));
             }
             
             bool BinaryRelationExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
diff --git a/src/ir/expressions/BinaryRelationExpression.h b/src/ir/expressions/BinaryRelationExpression.h
index 82b83fb60..873cbe5bf 100644
--- a/src/ir/expressions/BinaryRelationExpression.h
+++ b/src/ir/expressions/BinaryRelationExpression.h
@@ -31,7 +31,7 @@ namespace storm {
                  * @param right The right child of the binary expression.
                  * @param relationType The type of the relation associated with this node.
                  */
-                BinaryRelationExpression(std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right, RelationType relationType);
+                BinaryRelationExpression(std::unique_ptr<BaseExpression>&& left, std::unique_ptr<BaseExpression>&& right, RelationType relationType);
                 
                 /*!
                  * Copy-constructs from the given expression.
@@ -40,9 +40,9 @@ namespace storm {
                  */
                 BinaryRelationExpression(BinaryRelationExpression const& binaryRelationExpression);
                 
-                virtual std::shared_ptr<BaseExpression> clone() const override;
+                virtual std::unique_ptr<BaseExpression> clone() const override;
                 
-                virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
+                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
                 
diff --git a/src/ir/expressions/BooleanConstantExpression.cpp b/src/ir/expressions/BooleanConstantExpression.cpp
index 006e32769..2022e8796 100644
--- a/src/ir/expressions/BooleanConstantExpression.cpp
+++ b/src/ir/expressions/BooleanConstantExpression.cpp
@@ -19,12 +19,12 @@ namespace storm {
                 // Nothing to do here.
             }
 
-            std::shared_ptr<BaseExpression> BooleanConstantExpression::clone() const {
-                return std::shared_ptr<BaseExpression>(new BooleanConstantExpression(*this));
+            std::unique_ptr<BaseExpression> BooleanConstantExpression::clone() const {
+                return std::unique_ptr<BaseExpression>(new BooleanConstantExpression(*this));
             }
 
-            std::shared_ptr<BaseExpression> BooleanConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::shared_ptr<BaseExpression>(new BooleanConstantExpression(*this));
+            std::unique_ptr<BaseExpression> BooleanConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
+                return std::unique_ptr<BaseExpression>(new BooleanConstantExpression(*this));
             }
             
             bool BooleanConstantExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
diff --git a/src/ir/expressions/BooleanConstantExpression.h b/src/ir/expressions/BooleanConstantExpression.h
index 47f1b5dd7..4838ba595 100644
--- a/src/ir/expressions/BooleanConstantExpression.h
+++ b/src/ir/expressions/BooleanConstantExpression.h
@@ -33,9 +33,9 @@ namespace storm {
                  */
                 BooleanConstantExpression(BooleanConstantExpression const& booleanConstantExpression);
                 
-                virtual std::shared_ptr<BaseExpression> clone() const override;
+                virtual std::unique_ptr<BaseExpression> clone() const override;
 
-                virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
+                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
                 
diff --git a/src/ir/expressions/BooleanLiteralExpression.cpp b/src/ir/expressions/BooleanLiteralExpression.cpp
index 35708e33a..89e6b7876 100644
--- a/src/ir/expressions/BooleanLiteralExpression.cpp
+++ b/src/ir/expressions/BooleanLiteralExpression.cpp
@@ -20,12 +20,12 @@ namespace storm {
                 // Nothing to do here.
             }
 
-            std::shared_ptr<BaseExpression> BooleanLiteralExpression::clone() const {
-                return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(*this));
+            std::unique_ptr<BaseExpression> BooleanLiteralExpression::clone() const {
+                return std::unique_ptr<BaseExpression>(new BooleanLiteralExpression(*this));
             }
                                                        
-            std::shared_ptr<BaseExpression> BooleanLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(this->value));
+            std::unique_ptr<BaseExpression> BooleanLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
+                return std::unique_ptr<BaseExpression>(new BooleanLiteralExpression(this->value));
             }
             
             bool BooleanLiteralExpression::getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
diff --git a/src/ir/expressions/BooleanLiteralExpression.h b/src/ir/expressions/BooleanLiteralExpression.h
index c4c6a85a1..1fb747a78 100644
--- a/src/ir/expressions/BooleanLiteralExpression.h
+++ b/src/ir/expressions/BooleanLiteralExpression.h
@@ -33,9 +33,9 @@ namespace storm {
                  */
                 BooleanLiteralExpression(BooleanLiteralExpression const& booleanLiteralExpression);
                 
-                virtual std::shared_ptr<BaseExpression> clone() const override;
+                virtual std::unique_ptr<BaseExpression> clone() const override;
                 
-                virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
+                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
                 
diff --git a/src/ir/expressions/DoubleConstantExpression.cpp b/src/ir/expressions/DoubleConstantExpression.cpp
index 3903b4b57..bc29cbf26 100644
--- a/src/ir/expressions/DoubleConstantExpression.cpp
+++ b/src/ir/expressions/DoubleConstantExpression.cpp
@@ -19,12 +19,12 @@ namespace storm {
                 // Nothing to do here.
             }
             
-            std::shared_ptr<BaseExpression> DoubleConstantExpression::clone() const {
-                return std::shared_ptr<BaseExpression>(new DoubleConstantExpression(*this));
+            std::unique_ptr<BaseExpression> DoubleConstantExpression::clone() const {
+                return std::unique_ptr<BaseExpression>(new DoubleConstantExpression(*this));
             }
             
-            std::shared_ptr<BaseExpression> DoubleConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::shared_ptr<BaseExpression>(new DoubleConstantExpression(*this));
+            std::unique_ptr<BaseExpression> DoubleConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
+                return std::unique_ptr<BaseExpression>(new DoubleConstantExpression(*this));
             }
             
             double DoubleConstantExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
diff --git a/src/ir/expressions/DoubleConstantExpression.h b/src/ir/expressions/DoubleConstantExpression.h
index cec0b23bc..9eaa6eb18 100644
--- a/src/ir/expressions/DoubleConstantExpression.h
+++ b/src/ir/expressions/DoubleConstantExpression.h
@@ -33,9 +33,9 @@ namespace storm {
                  */
                 DoubleConstantExpression(DoubleConstantExpression const& doubleConstantExpression);
                 
-                virtual std::shared_ptr<BaseExpression> clone() const override;
+                virtual std::unique_ptr<BaseExpression> clone() const override;
                 
-                virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
+                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
                 
diff --git a/src/ir/expressions/DoubleLiteralExpression.cpp b/src/ir/expressions/DoubleLiteralExpression.cpp
index b7a435051..08663f8f7 100644
--- a/src/ir/expressions/DoubleLiteralExpression.cpp
+++ b/src/ir/expressions/DoubleLiteralExpression.cpp
@@ -22,12 +22,12 @@ namespace storm {
                 // Nothing to do here.
             }
             
-            std::shared_ptr<BaseExpression> DoubleLiteralExpression::clone() const {
-                return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(*this));
+            std::unique_ptr<BaseExpression> DoubleLiteralExpression::clone() const {
+                return std::unique_ptr<BaseExpression>(new DoubleLiteralExpression(*this));
             }
 
-            std::shared_ptr<BaseExpression> DoubleLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(this->value));
+            std::unique_ptr<BaseExpression> DoubleLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
+                return std::unique_ptr<BaseExpression>(new DoubleLiteralExpression(this->value));
             }
             
             double DoubleLiteralExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
diff --git a/src/ir/expressions/DoubleLiteralExpression.h b/src/ir/expressions/DoubleLiteralExpression.h
index 5327fbfe0..7105858c2 100644
--- a/src/ir/expressions/DoubleLiteralExpression.h
+++ b/src/ir/expressions/DoubleLiteralExpression.h
@@ -33,9 +33,9 @@ namespace storm {
                  */
                 DoubleLiteralExpression(DoubleLiteralExpression const& doubleLiteralExpression);
                 
-                virtual std::shared_ptr<BaseExpression> clone() const override;
+                virtual std::unique_ptr<BaseExpression> clone() const override;
                 
-                virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
+                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
                 
diff --git a/src/ir/expressions/IntegerConstantExpression.cpp b/src/ir/expressions/IntegerConstantExpression.cpp
index b615061d7..bcc5cb0eb 100644
--- a/src/ir/expressions/IntegerConstantExpression.cpp
+++ b/src/ir/expressions/IntegerConstantExpression.cpp
@@ -19,12 +19,12 @@ namespace storm {
                 // Nothing to do here.
             }
             
-            std::shared_ptr<BaseExpression> IntegerConstantExpression::clone() const {
-                return std::shared_ptr<BaseExpression>(new IntegerConstantExpression(*this));
+            std::unique_ptr<BaseExpression> IntegerConstantExpression::clone() const {
+                return std::unique_ptr<BaseExpression>(new IntegerConstantExpression(*this));
             }
             
-            std::shared_ptr<BaseExpression> IntegerConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::shared_ptr<BaseExpression>(new IntegerConstantExpression(*this));
+            std::unique_ptr<BaseExpression> IntegerConstantExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
+                return std::unique_ptr<BaseExpression>(new IntegerConstantExpression(*this));
             }
             
             double IntegerConstantExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
diff --git a/src/ir/expressions/IntegerConstantExpression.h b/src/ir/expressions/IntegerConstantExpression.h
index 35c9458c0..04370574d 100644
--- a/src/ir/expressions/IntegerConstantExpression.h
+++ b/src/ir/expressions/IntegerConstantExpression.h
@@ -33,9 +33,9 @@ namespace storm {
                  */
                 IntegerConstantExpression(IntegerConstantExpression const& integerConstantExpression);
                 
-                virtual std::shared_ptr<BaseExpression> clone() const override;
+                virtual std::unique_ptr<BaseExpression> clone() const override;
                 
-                virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
+                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
                 
diff --git a/src/ir/expressions/IntegerLiteralExpression.cpp b/src/ir/expressions/IntegerLiteralExpression.cpp
index 96d3f7570..ed3277f18 100644
--- a/src/ir/expressions/IntegerLiteralExpression.cpp
+++ b/src/ir/expressions/IntegerLiteralExpression.cpp
@@ -22,12 +22,12 @@ namespace storm {
                 // Nothing to do here.
             }
             
-            std::shared_ptr<BaseExpression> IntegerLiteralExpression::clone() const {
-                return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(*this));
+            std::unique_ptr<BaseExpression> IntegerLiteralExpression::clone() const {
+                return std::unique_ptr<BaseExpression>(new IntegerLiteralExpression(*this));
             }
             
-            std::shared_ptr<BaseExpression> IntegerLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(this->value));
+            std::unique_ptr<BaseExpression> IntegerLiteralExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
+                return std::unique_ptr<BaseExpression>(new IntegerLiteralExpression(this->value));
             }
             
             double IntegerLiteralExpression::getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
diff --git a/src/ir/expressions/IntegerLiteralExpression.h b/src/ir/expressions/IntegerLiteralExpression.h
index 9df073415..cb1041684 100644
--- a/src/ir/expressions/IntegerLiteralExpression.h
+++ b/src/ir/expressions/IntegerLiteralExpression.h
@@ -33,9 +33,9 @@ namespace storm {
                  */
                 IntegerLiteralExpression(IntegerLiteralExpression const& integerLiteralExpression);
                 
-                virtual std::shared_ptr<BaseExpression> clone() const override;
+                virtual std::unique_ptr<BaseExpression> clone() const override;
                 
-                virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
+                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
                 
diff --git a/src/ir/expressions/UnaryBooleanFunctionExpression.cpp b/src/ir/expressions/UnaryBooleanFunctionExpression.cpp
index 6e27ba7c1..79eaa754c 100644
--- a/src/ir/expressions/UnaryBooleanFunctionExpression.cpp
+++ b/src/ir/expressions/UnaryBooleanFunctionExpression.cpp
@@ -13,7 +13,7 @@ namespace storm {
     namespace ir {
         namespace expressions {
             
-            UnaryBooleanFunctionExpression::UnaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> child, FunctionType functionType) : UnaryExpression(bool_, child), functionType(functionType) {
+            UnaryBooleanFunctionExpression::UnaryBooleanFunctionExpression(std::unique_ptr<BaseExpression>&& child, FunctionType functionType) : UnaryExpression(bool_, std::move(child)), functionType(functionType) {
                 // Nothing to do here.
             }
             
@@ -21,12 +21,12 @@ namespace storm {
                 // Nothing to do here.
             }
             
-            std::shared_ptr<BaseExpression> UnaryBooleanFunctionExpression::clone() const {
-                return std::shared_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getChild()->clone(), functionType));
+            std::unique_ptr<BaseExpression> UnaryBooleanFunctionExpression::clone() const {
+                return std::unique_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getChild()->clone(), functionType));
             }
             
-            std::shared_ptr<BaseExpression> UnaryBooleanFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::shared_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getChild()->clone(renaming, variableState), this->functionType));
+            std::unique_ptr<BaseExpression> UnaryBooleanFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
+                return std::unique_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getChild()->clone(renaming, variableState), this->functionType));
             }
             
             UnaryBooleanFunctionExpression::FunctionType UnaryBooleanFunctionExpression::getFunctionType() const {
diff --git a/src/ir/expressions/UnaryBooleanFunctionExpression.h b/src/ir/expressions/UnaryBooleanFunctionExpression.h
index 166a036eb..a3087f5e5 100644
--- a/src/ir/expressions/UnaryBooleanFunctionExpression.h
+++ b/src/ir/expressions/UnaryBooleanFunctionExpression.h
@@ -30,7 +30,7 @@ namespace storm {
                  * @param child The child of the node.
                  * @param functionType The operator that is to be applied to the two children.
                  */
-                UnaryBooleanFunctionExpression(std::shared_ptr<BaseExpression> child, FunctionType functionType);
+                UnaryBooleanFunctionExpression(std::unique_ptr<BaseExpression>&& child, FunctionType functionType);
                 
                 /*!
                  * Copy-constructs from the given expression.
@@ -39,9 +39,9 @@ namespace storm {
                  */
                 UnaryBooleanFunctionExpression(UnaryBooleanFunctionExpression const& unaryBooleanFunctionExpression);
                 
-                virtual std::shared_ptr<BaseExpression> clone() const override;
+                virtual std::unique_ptr<BaseExpression> clone() const override;
                 
-                virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
+                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
 
                 /*!
                  * Retrieves the operator that is associated with this node.
diff --git a/src/ir/expressions/UnaryExpression.cpp b/src/ir/expressions/UnaryExpression.cpp
index c49227cd6..a5c8c4be8 100644
--- a/src/ir/expressions/UnaryExpression.cpp
+++ b/src/ir/expressions/UnaryExpression.cpp
@@ -11,15 +11,15 @@ namespace storm {
     namespace ir {
         namespace expressions {
     
-            UnaryExpression::UnaryExpression(ReturnType type, std::shared_ptr<BaseExpression> child) : BaseExpression(type), child(child) {
+            UnaryExpression::UnaryExpression(ReturnType type, std::unique_ptr<BaseExpression>&& child) : BaseExpression(type), child(std::move(child)) {
                 // Nothing to do here.
             }
             
-            UnaryExpression::UnaryExpression(UnaryExpression const& unaryExpression) : BaseExpression(unaryExpression), child(unaryExpression.child) {
+            UnaryExpression::UnaryExpression(UnaryExpression const& unaryExpression) : BaseExpression(unaryExpression), child(unaryExpression.child->clone()) {
                 // Nothing to do here.
             }
             
-            std::shared_ptr<BaseExpression> const& UnaryExpression::getChild() const {
+            std::unique_ptr<BaseExpression> const& UnaryExpression::getChild() const {
                 return child;
             }
             
diff --git a/src/ir/expressions/UnaryExpression.h b/src/ir/expressions/UnaryExpression.h
index e33d48568..fa330aca6 100644
--- a/src/ir/expressions/UnaryExpression.h
+++ b/src/ir/expressions/UnaryExpression.h
@@ -24,7 +24,7 @@ namespace storm {
                  * @param type The type of the unary expression.
                  * @param right The child of the unary expression.
                  */
-                UnaryExpression(ReturnType type, std::shared_ptr<BaseExpression> child);
+                UnaryExpression(ReturnType type, std::unique_ptr<BaseExpression>&& child);
                 
                 /*!
                  * Copy-constructs from the given expression.
@@ -38,11 +38,11 @@ namespace storm {
                  *
                  * @return The child of the expression node.
                  */
-                std::shared_ptr<BaseExpression> const& getChild() const;
+                std::unique_ptr<BaseExpression> const& getChild() const;
                 
             private:
                 // The left child of the unary expression.
-                std::shared_ptr<BaseExpression> child;
+                std::unique_ptr<BaseExpression> child;
             };
             
         } // namespace expressions
diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.cpp b/src/ir/expressions/UnaryNumericalFunctionExpression.cpp
index aad3604b9..228731749 100644
--- a/src/ir/expressions/UnaryNumericalFunctionExpression.cpp
+++ b/src/ir/expressions/UnaryNumericalFunctionExpression.cpp
@@ -11,7 +11,7 @@ namespace storm {
     namespace ir {
         namespace expressions {
             
-            UnaryNumericalFunctionExpression::UnaryNumericalFunctionExpression(ReturnType type, std::shared_ptr<BaseExpression> child, FunctionType functionType) : UnaryExpression(type, child), functionType(functionType) {
+            UnaryNumericalFunctionExpression::UnaryNumericalFunctionExpression(ReturnType type, std::unique_ptr<BaseExpression>&& child, FunctionType functionType) : UnaryExpression(type, std::move(child)), functionType(functionType) {
                 // Nothing to do here.
             }
             
@@ -19,12 +19,12 @@ namespace storm {
                 // Nothing to do here.
             }
             
-            std::shared_ptr<BaseExpression> UnaryNumericalFunctionExpression::clone() const {
-                return std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(), functionType));
+            std::unique_ptr<BaseExpression> UnaryNumericalFunctionExpression::clone() const {
+                return std::unique_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(), functionType));
             }
             
-            std::shared_ptr<BaseExpression> UnaryNumericalFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
-                return std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(renaming, variableState), this->functionType));
+            std::unique_ptr<BaseExpression> UnaryNumericalFunctionExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
+                return std::unique_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(renaming, variableState), this->functionType));
             }
             
             int_fast64_t UnaryNumericalFunctionExpression::getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.h b/src/ir/expressions/UnaryNumericalFunctionExpression.h
index 1362497db..fbcbb7fe4 100644
--- a/src/ir/expressions/UnaryNumericalFunctionExpression.h
+++ b/src/ir/expressions/UnaryNumericalFunctionExpression.h
@@ -30,7 +30,7 @@ namespace storm {
                  * @param child The child of the node.
                  * @param functionType The operator that is to be applied to the two children.
                  */
-                UnaryNumericalFunctionExpression(ReturnType type, std::shared_ptr<BaseExpression> child, FunctionType functionType);
+                UnaryNumericalFunctionExpression(ReturnType type, std::unique_ptr<BaseExpression>&& child, FunctionType functionType);
                 
                 /*!
                  * Copy-constructs from the given expression.
@@ -39,9 +39,9 @@ namespace storm {
                  */
                 UnaryNumericalFunctionExpression(UnaryNumericalFunctionExpression const& unaryNumericalFunctionExpression);
                 
-                virtual std::shared_ptr<BaseExpression> clone() const override;
+                virtual std::unique_ptr<BaseExpression> clone() const override;
                 
-                virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
+                virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
                 
                 virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const override;
                 
diff --git a/src/ir/expressions/VariableExpression.cpp b/src/ir/expressions/VariableExpression.cpp
index 891417f58..177e1c316 100644
--- a/src/ir/expressions/VariableExpression.cpp
+++ b/src/ir/expressions/VariableExpression.cpp
@@ -26,24 +26,24 @@ namespace storm {
                 // Nothing to do here.
             }
             
-            std::shared_ptr<BaseExpression> VariableExpression::clone() const {
-                return std::shared_ptr<BaseExpression>(new VariableExpression(*this));
+            std::unique_ptr<BaseExpression> VariableExpression::clone() const {
+                return std::unique_ptr<BaseExpression>(new VariableExpression(*this));
             }
             
-            std::shared_ptr<BaseExpression> VariableExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
+            std::unique_ptr<BaseExpression> VariableExpression::clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const {
                 // Perform the proper cloning.
                 auto renamingPair = renaming.find(this->variableName);
                 if (renamingPair != renaming.end()) {
                     if (this->getType() == int_) {
-                        return variableState.getIntegerVariableExpression(renamingPair->second);
+                        return variableState.getIntegerVariableExpression(renamingPair->second)->clone();
                     } else {
-                        return variableState.getBooleanVariableExpression(renamingPair->second);
+                        return variableState.getBooleanVariableExpression(renamingPair->second)->clone();
                     }
                 } else {
                     if (this->getType() == int_) {
-                        return variableState.getIntegerVariableExpression(this->variableName);
+                        return variableState.getIntegerVariableExpression(this->variableName)->clone();
                     } else {
-                        return variableState.getBooleanVariableExpression(this->variableName);
+                        return variableState.getBooleanVariableExpression(this->variableName)->clone();
                     }
                 }
             }
diff --git a/src/ir/expressions/VariableExpression.h b/src/ir/expressions/VariableExpression.h
index 468144b85..d24229b9e 100644
--- a/src/ir/expressions/VariableExpression.h
+++ b/src/ir/expressions/VariableExpression.h
@@ -52,9 +52,9 @@ namespace storm {
                  */
                 VariableExpression(VariableExpression const& variableExpression);
                 
-                virtual std::shared_ptr<BaseExpression> clone() const override;
+                virtual std::unique_ptr<BaseExpression> clone() const override;
                 
-				virtual std::shared_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
+				virtual std::unique_ptr<BaseExpression> clone(std::map<std::string, std::string> const& renaming, storm::parser::prism::VariableState const& variableState) const override;
 				
 				virtual void accept(ExpressionVisitor* visitor) override;
 				
diff --git a/src/parser/prismparser/BaseGrammar.h b/src/parser/prismparser/BaseGrammar.h
index ab6059820..6b0b37a8a 100644
--- a/src/parser/prismparser/BaseGrammar.h
+++ b/src/parser/prismparser/BaseGrammar.h
@@ -26,14 +26,14 @@ namespace prism {
 		/*!
 		 * Constructor.
 		 */
-		BaseGrammar(std::shared_ptr<VariableState>& state) : state(state) {}
+		BaseGrammar(std::shared_ptr<VariableState> const& state) : state(state) {}
 
 		/*!
 		 * Create and return a new instance of class T, usually the subclass.
 		 * @param state VariableState to be given to the constructor.
 		 * @returns Instance of class T.
 		 */
-		static T& instance(std::shared_ptr<VariableState> state = nullptr) {
+		static T& instance(std::shared_ptr<VariableState> const& state = nullptr) {
 			if (BaseGrammar::instanceObject == nullptr) {
 				BaseGrammar::instanceObject = std::shared_ptr<T>(new T(state));
 				if (!state->firstRun) BaseGrammar::instanceObject->secondRun();
@@ -62,24 +62,24 @@ namespace prism {
 		 * @param value Value of the literal.
 		 * @returns Boolean literal.
 		 */
-		std::shared_ptr<BaseExpression> createBoolLiteral(const bool value) {
-			return std::shared_ptr<BooleanLiteralExpression>(new BooleanLiteralExpression(value));
+		std::shared_ptr<BaseExpression> createBoolLiteral(bool value) {
+			return std::shared_ptr<BaseExpression>(new BooleanLiteralExpression(value));
 		}
 		/*!
 		 * Create a new double literal with the given value.
 		 * @param value Value of the literal.
 		 * @returns Double literal.
 		 */
-		std::shared_ptr<BaseExpression> createDoubleLiteral(const double value) {
-			return std::shared_ptr<DoubleLiteralExpression>(new DoubleLiteralExpression(value));
+		std::shared_ptr<BaseExpression> createDoubleLiteral(double value) {
+			return std::shared_ptr<BaseExpression>(new DoubleLiteralExpression(value));
 		}
 		/*!
 		 * Create a new integer literal with the given value.
 		 * @param value Value of the literal.
 		 * @returns Integer literal.
 		 */
-		std::shared_ptr<BaseExpression> createIntLiteral(const int_fast64_t value) {
-			return std::shared_ptr<IntegerLiteralExpression>(new IntegerLiteralExpression(value));
+		std::shared_ptr<BaseExpression> createIntLiteral(int_fast64_t value) {
+			return std::shared_ptr<BaseExpression>(new IntegerLiteralExpression(value));
 		}
 		
 		/*!
@@ -90,11 +90,11 @@ namespace prism {
 		 * @param type Return type.
 		 * @returns Plus expression.
 		 */
-		std::shared_ptr<BaseExpression> createPlus(const std::shared_ptr<BaseExpression> left, bool addition, const std::shared_ptr<BaseExpression> right, BaseExpression::ReturnType type) {
+		std::shared_ptr<BaseExpression> createPlus(std::shared_ptr<BaseExpression> const& left, bool addition, std::shared_ptr<BaseExpression> const& right, BaseExpression::ReturnType type) {
 			if (addition) {
-				return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(type, left, right, BinaryNumericalFunctionExpression::PLUS));
+				return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(type, left->clone(), right->clone(), BinaryNumericalFunctionExpression::PLUS));
 			} else {
-				return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(type, left, right, BinaryNumericalFunctionExpression::MINUS));
+				return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(type, left->clone(), right->clone(), BinaryNumericalFunctionExpression::MINUS));
 			}
 		}
 		/*!
@@ -104,7 +104,7 @@ namespace prism {
 		 * @param right Right operand.
 		 * @returns Double plus expression.
 		 */
-		std::shared_ptr<BaseExpression> createDoublePlus(const std::shared_ptr<BaseExpression> left, bool addition, const std::shared_ptr<BaseExpression> right) {
+		std::shared_ptr<BaseExpression> createDoublePlus(std::shared_ptr<BaseExpression> const& left, bool addition, std::shared_ptr<BaseExpression> const& right) {
 			return this->createPlus(left, addition, right, BaseExpression::double_);
 		}
 		/*!
@@ -114,7 +114,7 @@ namespace prism {
 		 * @param right Right operand.
 		 * @returns Integer plus expression.
 		 */
-		std::shared_ptr<BaseExpression> createIntPlus(const std::shared_ptr<BaseExpression> left, bool addition, const std::shared_ptr<BaseExpression> right) {
+		std::shared_ptr<BaseExpression> createIntPlus(std::shared_ptr<BaseExpression> const& left, bool addition, std::shared_ptr<BaseExpression> const& right) {
 			return this->createPlus(left, addition, right, BaseExpression::int_);
 		}
 
@@ -124,8 +124,8 @@ namespace prism {
 		 * @param right Right operand.
 		 * @returns Integer multiplication expression.
 		 */
-		std::shared_ptr<BaseExpression> createIntMult(const std::shared_ptr<BaseExpression> left, const std::shared_ptr<BaseExpression> right) {
-			return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::int_, left, right, BinaryNumericalFunctionExpression::TIMES));
+		std::shared_ptr<BaseExpression> createIntMult(std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right) {
+			return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(BaseExpression::int_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::TIMES));
 		}
 		/*!
 		 * Create a new integer multiplication expression. If multiplication is true, it will be an multiplication, otherwise a division.
@@ -134,11 +134,11 @@ namespace prism {
 		 * @param right Right operand.
 		 * @returns Integer multiplication expression.
 		 */
-		std::shared_ptr<BaseExpression> createDoubleMult(const std::shared_ptr<BaseExpression> left, bool multiplication, const std::shared_ptr<BaseExpression> right) {
+		std::shared_ptr<BaseExpression> createDoubleMult(std::shared_ptr<BaseExpression> const& left, bool multiplication, std::shared_ptr<BaseExpression> const& right) {
 			if (multiplication) {
-				return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::TIMES));
+				return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::TIMES));
 			} else {
-				return std::shared_ptr<BinaryNumericalFunctionExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left, right, BinaryNumericalFunctionExpression::DIVIDE));
+				return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(BaseExpression::double_, left->clone(), right->clone(), BinaryNumericalFunctionExpression::DIVIDE));
 			}
 		}
 		/*!
@@ -148,16 +148,16 @@ namespace prism {
 		 * @param right Right operand.
 		 * @returns Binary relation expression.
 		 */
-		std::shared_ptr<BaseExpression> createRelation(std::shared_ptr<BaseExpression> left, BinaryRelationExpression::RelationType relationType, std::shared_ptr<BaseExpression> right) {
-			return std::shared_ptr<BinaryRelationExpression>(new BinaryRelationExpression(left, right, relationType));
+		std::shared_ptr<BaseExpression> createRelation(std::shared_ptr<BaseExpression> const& left, BinaryRelationExpression::RelationType relationType, std::shared_ptr<BaseExpression> const& right) {
+			return std::shared_ptr<BaseExpression>(new BinaryRelationExpression(left->clone(), right->clone(), relationType));
 		}
 		/*!
 		 * Create a new negation expression.
 		 * @param child Expression to be negated.
 		 * @returns Negation expression.
 		 */
-		std::shared_ptr<BaseExpression> createNot(std::shared_ptr<BaseExpression> child) {
-			return std::shared_ptr<UnaryBooleanFunctionExpression>(new UnaryBooleanFunctionExpression(child, UnaryBooleanFunctionExpression::NOT));
+		std::shared_ptr<BaseExpression> createNot(std::shared_ptr<BaseExpression> const& child) {
+			return std::shared_ptr<UnaryBooleanFunctionExpression>(new UnaryBooleanFunctionExpression(child->clone(), UnaryBooleanFunctionExpression::NOT));
 		}
 		/*!
 		 * Create a new And expression.
@@ -165,9 +165,8 @@ namespace prism {
 		 * @param right Right operand.
 		 * @returns And expression.
 		 */
-		std::shared_ptr<BaseExpression> createAnd(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right) {
-			//std::cerr << "Creating " << left->toString() << " & " << right->toString() << std::endl;
-			return std::shared_ptr<BinaryBooleanFunctionExpression>(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::AND));
+		std::shared_ptr<BaseExpression> createAnd(std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right) {
+			return std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(left->clone(), right->clone(), BinaryBooleanFunctionExpression::AND));
 		}
 		/*!
 		 * Create a new Or expression.
@@ -175,24 +174,24 @@ namespace prism {
 		 * @param right Right operand.
 		 * @returns Or expression.
 		 */
-		std::shared_ptr<BaseExpression> createOr(std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right) {
-			return std::shared_ptr<BinaryBooleanFunctionExpression>(new BinaryBooleanFunctionExpression(left, right, BinaryBooleanFunctionExpression::OR));
+		std::shared_ptr<BaseExpression> createOr(std::shared_ptr<BaseExpression> const& left, std::shared_ptr<BaseExpression> const& right) {
+			return std::shared_ptr<BinaryBooleanFunctionExpression>(new BinaryBooleanFunctionExpression(left->clone(), right->clone(), BinaryBooleanFunctionExpression::OR));
 		}
 		/*!
 		 * Retrieve boolean variable by name.
 		 * @param name Variable name.
 		 * @returns Boolean variable.
 		 */
-		std::shared_ptr<BaseExpression> getBoolVariable(const std::string name) {
-			return state->getBooleanVariableExpression(name);
+		std::shared_ptr<BaseExpression> getBoolVariable(std::string const& name) {
+			return std::shared_ptr<BaseExpression>(new VariableExpression(*state->getBooleanVariableExpression(name)));
 		}
 		/*!
 		 * Retrieve integer variable by name.
 		 * @param name Variable name.
 		 * @returns Integer variable.
 		 */
-		std::shared_ptr<BaseExpression> getIntVariable(const std::string name) {
-			return state->getIntegerVariableExpression(name);
+		std::shared_ptr<BaseExpression> getIntVariable(std::string const& name) {
+			return std::shared_ptr<BaseExpression>(new VariableExpression(*state->getIntegerVariableExpression(name)));
 		}
 
 		/*!
@@ -200,6 +199,7 @@ namespace prism {
 		 * Any subclass that needs to do something in order to proceed to the second run should override this method.
 		 */
 		virtual void prepareSecondRun() {}
+        
 	protected:
 		/*!
 		 * Pointer to variable state.
diff --git a/src/parser/prismparser/BooleanExpressionGrammar.cpp b/src/parser/prismparser/BooleanExpressionGrammar.cpp
index 6a2d421bb..380fd8ac9 100644
--- a/src/parser/prismparser/BooleanExpressionGrammar.cpp
+++ b/src/parser/prismparser/BooleanExpressionGrammar.cpp
@@ -4,39 +4,39 @@
 #include "ConstBooleanExpressionGrammar.h"
 
 namespace storm {
-namespace parser {
-namespace prism {
-
-	BooleanExpressionGrammar::BooleanExpressionGrammar(std::shared_ptr<VariableState>& state)
-		: BooleanExpressionGrammar::base_type(booleanExpression), BaseGrammar(state) {
-
-		booleanExpression %= orExpression;
-		booleanExpression.name("boolean expression");
-
-		orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::bind(&BaseGrammar::createOr, this, qi::_val, qi::_1)];
-		orExpression.name("boolean expression");
-
-		andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::bind(&BaseGrammar::createAnd, this, qi::_val, qi::_1)];
-		andExpression.name("boolean expression");
-
-		notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::bind(&BaseGrammar::createNot, this, qi::_1)];
-		notExpression.name("boolean expression");
-
-		atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | ConstBooleanExpressionGrammar::instance(this->state));
-		atomicBooleanExpression.name("boolean expression");
-
-		relativeExpression = (IntegerExpressionGrammar::instance(this->state) >> relations_ >> IntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&BaseGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)];
-		relativeExpression.name("relative expression");
-		
-		booleanVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getBoolVariable, this, qi::_1)];
-		booleanVariableExpression.name("boolean variable");
-	}
-
-	void BooleanExpressionGrammar::prepareSecondRun() {
-		booleanVariableExpression %= this->state->booleanVariables_;
-		booleanVariableExpression.name("boolean variable");
-	}
-
-}
-}
-}
\ No newline at end of file
+    namespace parser {
+        namespace prism {
+            
+            BooleanExpressionGrammar::BooleanExpressionGrammar(std::shared_ptr<VariableState> const& state)
+            : BooleanExpressionGrammar::base_type(booleanExpression), BaseGrammar(state) {
+                
+                booleanExpression %= orExpression;
+                booleanExpression.name("boolean expression");
+                
+                orExpression = andExpression[qi::_val = qi::_1] >> *(qi::lit("|") >> andExpression)[qi::_val = phoenix::bind(&BaseGrammar::createOr, this, qi::_val, qi::_1)];
+                orExpression.name("boolean expression");
+                
+                andExpression = notExpression[qi::_val = qi::_1] >> *(qi::lit("&") >> notExpression)[qi::_val = phoenix::bind(&BaseGrammar::createAnd, this, qi::_val, qi::_1)];
+                andExpression.name("boolean expression");
+                
+                notExpression = atomicBooleanExpression[qi::_val = qi::_1] | (qi::lit("!") >> atomicBooleanExpression)[qi::_val = phoenix::bind(&BaseGrammar::createNot, this, qi::_1)];
+                notExpression.name("boolean expression");
+                
+                atomicBooleanExpression %= (relativeExpression | booleanVariableExpression | qi::lit("(") >> booleanExpression >> qi::lit(")") | ConstBooleanExpressionGrammar::instance(this->state));
+                atomicBooleanExpression.name("boolean expression");
+                
+                relativeExpression = (IntegerExpressionGrammar::instance(this->state) >> relations_ >> IntegerExpressionGrammar::instance(this->state))[qi::_val = phoenix::bind(&BaseGrammar::createRelation, this, qi::_1, qi::_2, qi::_3)];
+                relativeExpression.name("relative expression");
+                
+                booleanVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getBoolVariable, this, qi::_1)];
+                booleanVariableExpression.name("boolean variable");
+            }
+            
+            void BooleanExpressionGrammar::prepareSecondRun() {
+                booleanVariableExpression %= this->state->booleanVariables_;
+                booleanVariableExpression.name("boolean variable");
+            }
+            
+        } // namespace prism
+    } // namespace parser
+} // namespace storm
\ No newline at end of file
diff --git a/src/parser/prismparser/BooleanExpressionGrammar.h b/src/parser/prismparser/BooleanExpressionGrammar.h
index 4f94dffbf..909219fa3 100644
--- a/src/parser/prismparser/BooleanExpressionGrammar.h
+++ b/src/parser/prismparser/BooleanExpressionGrammar.h
@@ -24,7 +24,7 @@ namespace prism {
  */
 class BooleanExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<BooleanExpressionGrammar> {
 public:
-	BooleanExpressionGrammar(std::shared_ptr<VariableState>& state);
+	BooleanExpressionGrammar(std::shared_ptr<VariableState> const& state);
 	/*!
 	 * Switch to second run.
 	 * Variable names may be any valid identifier in the first run, but only defined variables in the second run.
diff --git a/src/parser/prismparser/ConstBooleanExpressionGrammar.cpp b/src/parser/prismparser/ConstBooleanExpressionGrammar.cpp
index ffa0b219b..fa1fccab2 100644
--- a/src/parser/prismparser/ConstBooleanExpressionGrammar.cpp
+++ b/src/parser/prismparser/ConstBooleanExpressionGrammar.cpp
@@ -6,7 +6,7 @@ namespace storm {
 namespace parser {
 namespace prism {
 
-	ConstBooleanExpressionGrammar::ConstBooleanExpressionGrammar(std::shared_ptr<VariableState>& state)
+	ConstBooleanExpressionGrammar::ConstBooleanExpressionGrammar(std::shared_ptr<VariableState> const& state)
 		: ConstBooleanExpressionGrammar::base_type(constantBooleanExpression), BaseGrammar(state) {
 
 		constantBooleanExpression %= constantOrExpression;
diff --git a/src/parser/prismparser/ConstBooleanExpressionGrammar.h b/src/parser/prismparser/ConstBooleanExpressionGrammar.h
index f47c95bb5..8fea3ce95 100644
--- a/src/parser/prismparser/ConstBooleanExpressionGrammar.h
+++ b/src/parser/prismparser/ConstBooleanExpressionGrammar.h
@@ -22,7 +22,7 @@ namespace prism {
  */
 class ConstBooleanExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<ConstBooleanExpressionGrammar> {
 public:
-	ConstBooleanExpressionGrammar(std::shared_ptr<VariableState>& state);
+	ConstBooleanExpressionGrammar(std::shared_ptr<VariableState> const& state);
 
 
 private:
diff --git a/src/parser/prismparser/ConstDoubleExpressionGrammar.cpp b/src/parser/prismparser/ConstDoubleExpressionGrammar.cpp
index 1927909e1..0e3b45622 100644
--- a/src/parser/prismparser/ConstDoubleExpressionGrammar.cpp
+++ b/src/parser/prismparser/ConstDoubleExpressionGrammar.cpp
@@ -4,7 +4,7 @@ namespace storm {
 namespace parser {
 namespace prism {
 
-ConstDoubleExpressionGrammar::ConstDoubleExpressionGrammar(std::shared_ptr<VariableState>& state)
+ConstDoubleExpressionGrammar::ConstDoubleExpressionGrammar(std::shared_ptr<VariableState> const& state)
 	: ConstDoubleExpressionGrammar::base_type(constantDoubleExpression), BaseGrammar(state) {
 
 	constantDoubleExpression %= constantDoublePlusExpression;
diff --git a/src/parser/prismparser/ConstDoubleExpressionGrammar.h b/src/parser/prismparser/ConstDoubleExpressionGrammar.h
index a964ec367..41c503731 100644
--- a/src/parser/prismparser/ConstDoubleExpressionGrammar.h
+++ b/src/parser/prismparser/ConstDoubleExpressionGrammar.h
@@ -13,28 +13,28 @@
 #include "IdentifierGrammars.h"
 
 namespace storm {
-namespace parser {
-namespace prism {
-
-/*!
- * This grammar parses constant double expressions as used in prism models.
- */
-class ConstDoubleExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<ConstDoubleExpressionGrammar> {
-public:
-	ConstDoubleExpressionGrammar(std::shared_ptr<VariableState>& state);
-
-private:
-	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> constantDoubleExpression;
-	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantDoublePlusExpression;
-	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantDoubleMultExpression;
-	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicDoubleExpression;
-	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> doubleConstantExpression;
-	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> doubleLiteralExpression;
-};
-
-
-}
-}
+    namespace parser {
+        namespace prism {
+            
+            /*!
+             * This grammar parses constant double expressions as used in prism models.
+             */
+            class ConstDoubleExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<ConstDoubleExpressionGrammar> {
+            public:
+                ConstDoubleExpressionGrammar(std::shared_ptr<VariableState> const& state);
+                
+            private:
+                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> constantDoubleExpression;
+                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantDoublePlusExpression;
+                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantDoubleMultExpression;
+                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicDoubleExpression;
+                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> doubleConstantExpression;
+                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> doubleLiteralExpression;
+            };
+            
+            
+        }
+    }
 }
 
 #endif	/* CONSTDOUBLEEXPRESSIONGRAMMAR_H */
diff --git a/src/parser/prismparser/ConstIntegerExpressionGrammar.cpp b/src/parser/prismparser/ConstIntegerExpressionGrammar.cpp
index 233b4492a..d49e7f9ee 100644
--- a/src/parser/prismparser/ConstIntegerExpressionGrammar.cpp
+++ b/src/parser/prismparser/ConstIntegerExpressionGrammar.cpp
@@ -1,35 +1,35 @@
 #include "ConstIntegerExpressionGrammar.h"
 
 namespace storm {
-namespace parser {
-namespace prism {
-
-
-ConstIntegerExpressionGrammar::ConstIntegerExpressionGrammar(std::shared_ptr<VariableState>& state)
-	: ConstIntegerExpressionGrammar::base_type(constantIntegerExpression), BaseGrammar(state) {
-
-	constantIntegerExpression %= constantIntegerPlusExpression;
-	constantIntegerExpression.name("constant integer expression");
-
-	constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantIntegerMultExpression)
-			[qi::_val = phoenix::bind(&BaseGrammar::createIntPlus, this, qi::_val, qi::_a, qi::_1)];
-	constantIntegerPlusExpression.name("constant integer expression");
-
-	constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)
-			[qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)];
-	constantIntegerMultExpression.name("constant integer expression");
-
-	constantAtomicIntegerExpression %= (qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression);
-	constantAtomicIntegerExpression.name("constant integer expression");
-
-	integerConstantExpression %= (this->state->integerConstants_ | integerLiteralExpression);
-	integerConstantExpression.name("integer constant or literal");
-	
-	integerLiteralExpression = qi::int_[qi::_val = phoenix::bind(&BaseGrammar::createIntLiteral, this, qi::_1)];
-	integerLiteralExpression.name("integer literal");
-
-}
-
-}
-}
-}
\ No newline at end of file
+    namespace parser {
+        namespace prism {
+            
+            
+            ConstIntegerExpressionGrammar::ConstIntegerExpressionGrammar(std::shared_ptr<VariableState> const& state)
+            : ConstIntegerExpressionGrammar::base_type(constantIntegerExpression), BaseGrammar(state) {
+                
+                constantIntegerExpression %= constantIntegerPlusExpression;
+                constantIntegerExpression.name("constant integer expression");
+                
+                constantIntegerPlusExpression = constantIntegerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> constantIntegerMultExpression)
+                [qi::_val = phoenix::bind(&BaseGrammar::createIntPlus, this, qi::_val, qi::_a, qi::_1)];
+                constantIntegerPlusExpression.name("constant integer expression");
+                
+                constantIntegerMultExpression %= constantAtomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> constantAtomicIntegerExpression)
+                [qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)];
+                constantIntegerMultExpression.name("constant integer expression");
+                
+                constantAtomicIntegerExpression %= (qi::lit("(") >> constantIntegerExpression >> qi::lit(")") | integerConstantExpression);
+                constantAtomicIntegerExpression.name("constant integer expression");
+                
+                integerConstantExpression %= (this->state->integerConstants_ | integerLiteralExpression);
+                integerConstantExpression.name("integer constant or literal");
+                
+                integerLiteralExpression = qi::int_[qi::_val = phoenix::bind(&BaseGrammar::createIntLiteral, this, qi::_1)];
+                integerLiteralExpression.name("integer literal");
+                
+            }
+            
+        } // namespace prism
+    } // namespace parser
+} // namespace storm
\ No newline at end of file
diff --git a/src/parser/prismparser/ConstIntegerExpressionGrammar.h b/src/parser/prismparser/ConstIntegerExpressionGrammar.h
index c7360553e..a75654391 100644
--- a/src/parser/prismparser/ConstIntegerExpressionGrammar.h
+++ b/src/parser/prismparser/ConstIntegerExpressionGrammar.h
@@ -13,28 +13,28 @@
 #include "IdentifierGrammars.h"
 
 namespace storm {
-namespace parser {
-namespace prism {
-
-/*!
- * This grammar parses constant integer expressions as used in prism models.
- */
-class ConstIntegerExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<ConstIntegerExpressionGrammar> {
-public:
-	ConstIntegerExpressionGrammar(std::shared_ptr<VariableState>& state);
-	
-private:
-	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> constantIntegerExpression;
-	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantIntegerPlusExpression;
-	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantIntegerMultExpression;
-	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicIntegerExpression;
-	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerConstantExpression;
-	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerLiteralExpression;
-};
-
-
-}
-}
+    namespace parser {
+        namespace prism {
+            
+            /*!
+             * This grammar parses constant integer expressions as used in prism models.
+             */
+            class ConstIntegerExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<ConstIntegerExpressionGrammar> {
+            public:
+                ConstIntegerExpressionGrammar(std::shared_ptr<VariableState> const& state);
+                
+            private:
+                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> constantIntegerExpression;
+                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> constantIntegerPlusExpression;
+                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantIntegerMultExpression;
+                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantAtomicIntegerExpression;
+                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerConstantExpression;
+                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerLiteralExpression;
+            };
+            
+            
+        }
+    }
 }
 
 #endif	/* CONSTINTEGEREXPRESSIONGRAMMAR_H */
diff --git a/src/parser/prismparser/IdentifierGrammars.cpp b/src/parser/prismparser/IdentifierGrammars.cpp
index 552b6e2c0..ec6f14931 100644
--- a/src/parser/prismparser/IdentifierGrammars.cpp
+++ b/src/parser/prismparser/IdentifierGrammars.cpp
@@ -1,23 +1,23 @@
 #include "IdentifierGrammars.h"
 
 namespace storm {
-namespace parser {
-namespace prism {
-
-IdentifierGrammar::IdentifierGrammar(std::shared_ptr<VariableState>& state)
-	: IdentifierGrammar::base_type(identifierName), BaseGrammar(state) {
-
-	identifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isIdentifier, this->state.get(), qi::_1) ];
-	identifierName.name("identifier");
-}
-
-FreeIdentifierGrammar::FreeIdentifierGrammar(std::shared_ptr<VariableState>& state)
-	: FreeIdentifierGrammar::base_type(freeIdentifierName), BaseGrammar(state) {
-	
-	freeIdentifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isFreeIdentifier, this->state.get(), qi::_1) ];
-	freeIdentifierName.name("identifier");
-}
-
-}
-}
+    namespace parser {
+        namespace prism {
+            
+            IdentifierGrammar::IdentifierGrammar(std::shared_ptr<VariableState> const& state)
+            : IdentifierGrammar::base_type(identifierName), BaseGrammar(state) {
+                
+                identifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isIdentifier, this->state.get(), qi::_1) ];
+                identifierName.name("identifier");
+            }
+            
+            FreeIdentifierGrammar::FreeIdentifierGrammar(std::shared_ptr<VariableState> const& state)
+            : FreeIdentifierGrammar::base_type(freeIdentifierName), BaseGrammar(state) {
+                
+                freeIdentifierName %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][ qi::_pass = phoenix::bind(&VariableState::isFreeIdentifier, this->state.get(), qi::_1) ];
+                freeIdentifierName.name("identifier");
+            }
+            
+        }
+    }
 }
\ No newline at end of file
diff --git a/src/parser/prismparser/IdentifierGrammars.h b/src/parser/prismparser/IdentifierGrammars.h
index 5305cf277..ccb14bbc1 100644
--- a/src/parser/prismparser/IdentifierGrammars.h
+++ b/src/parser/prismparser/IdentifierGrammars.h
@@ -13,30 +13,30 @@
 #include "VariableState.h"
 
 namespace storm {
-namespace parser {
-namespace prism {
-
-	/*!
-	 * This grammar parses a (possibly used) identifier as used in a prism models.
-	 */
-	class IdentifierGrammar : public qi::grammar<Iterator, std::string(), Skipper, Unused>, public BaseGrammar<IdentifierGrammar> {
-	public:
-		IdentifierGrammar(std::shared_ptr<VariableState>& state);
-	private:
-		qi::rule<Iterator, std::string(), Skipper> identifierName;
-	};
-	
-	/*!
-	 * This grammar parses an used identifier as used in a prism models.
-	 */
-	class FreeIdentifierGrammar : public qi::grammar<Iterator, std::string(), Skipper, Unused>, public BaseGrammar<IdentifierGrammar>  {
-	public:
-		FreeIdentifierGrammar(std::shared_ptr<VariableState>& state);
-	private:
-		qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
-	};
-}
-}
+    namespace parser {
+        namespace prism {
+            
+            /*!
+             * This grammar parses a (possibly used) identifier as used in a prism models.
+             */
+            class IdentifierGrammar : public qi::grammar<Iterator, std::string(), Skipper, Unused>, public BaseGrammar<IdentifierGrammar> {
+            public:
+                IdentifierGrammar(std::shared_ptr<VariableState> const& state);
+            private:
+                qi::rule<Iterator, std::string(), Skipper> identifierName;
+            };
+            
+            /*!
+             * This grammar parses an used identifier as used in a prism models.
+             */
+            class FreeIdentifierGrammar : public qi::grammar<Iterator, std::string(), Skipper, Unused>, public BaseGrammar<IdentifierGrammar>  {
+            public:
+                FreeIdentifierGrammar(std::shared_ptr<VariableState> const& state);
+            private:
+                qi::rule<Iterator, std::string(), Skipper> freeIdentifierName;
+            };
+        }
+    }
 }
 #endif	/* IDENTIFIERGRAMMARS_H */
 
diff --git a/src/parser/prismparser/IntegerExpressionGrammar.cpp b/src/parser/prismparser/IntegerExpressionGrammar.cpp
index ba1a35eb6..1c34b0b56 100644
--- a/src/parser/prismparser/IntegerExpressionGrammar.cpp
+++ b/src/parser/prismparser/IntegerExpressionGrammar.cpp
@@ -4,33 +4,33 @@
 #include "ConstIntegerExpressionGrammar.h"
 
 namespace storm {
-namespace parser {
-namespace prism {
-
-	IntegerExpressionGrammar::IntegerExpressionGrammar(std::shared_ptr<VariableState>& state)
-		: IntegerExpressionGrammar::base_type(integerExpression), BaseGrammar(state) {
-
-		integerExpression %= integerPlusExpression;
-		integerExpression.name("integer expression");
-
-		integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> integerMultExpression)[qi::_val = phoenix::bind(&BaseGrammar::createIntPlus, this, qi::_val, qi::_a, qi::_1)];
-		integerPlusExpression.name("integer expression");
-
-		integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression[qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)]);
-		integerMultExpression.name("integer expression");
-
-		atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | ConstIntegerExpressionGrammar::instance(this->state));
-		atomicIntegerExpression.name("integer expression");
-
-		integerVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getIntVariable, this, qi::_1)];
-		integerVariableExpression.name("integer variable");
-	}
-
-	void IntegerExpressionGrammar::prepareSecondRun() {
-		integerVariableExpression %= this->state->integerVariables_;
-		integerVariableExpression.name("integer variable");
-	}
-
-}
-}
+    namespace parser {
+        namespace prism {
+            
+            IntegerExpressionGrammar::IntegerExpressionGrammar(std::shared_ptr<VariableState> const& state)
+            : IntegerExpressionGrammar::base_type(integerExpression), BaseGrammar(state) {
+                
+                integerExpression %= integerPlusExpression;
+                integerExpression.name("integer expression");
+                
+                integerPlusExpression = integerMultExpression[qi::_val = qi::_1] >> *((qi::lit("+")[qi::_a = true] | qi::lit("-")[qi::_a = false]) >> integerMultExpression)[qi::_val = phoenix::bind(&BaseGrammar::createIntPlus, this, qi::_val, qi::_a, qi::_1)];
+                integerPlusExpression.name("integer expression");
+                
+                integerMultExpression %= atomicIntegerExpression[qi::_val = qi::_1] >> *(qi::lit("*") >> atomicIntegerExpression[qi::_val = phoenix::bind(&BaseGrammar::createIntMult, this, qi::_val, qi::_1)]);
+                integerMultExpression.name("integer expression");
+                
+                atomicIntegerExpression %= (integerVariableExpression | qi::lit("(") >> integerExpression >> qi::lit(")") | ConstIntegerExpressionGrammar::instance(this->state));
+                atomicIntegerExpression.name("integer expression");
+                
+                integerVariableExpression = IdentifierGrammar::instance(this->state)[qi::_val = phoenix::bind(&BaseGrammar::getIntVariable, this, qi::_1)];
+                integerVariableExpression.name("integer variable");
+            }
+            
+            void IntegerExpressionGrammar::prepareSecondRun() {
+                integerVariableExpression %= this->state->integerVariables_;
+                integerVariableExpression.name("integer variable");
+            }
+            
+        }
+    }
 }
\ No newline at end of file
diff --git a/src/parser/prismparser/IntegerExpressionGrammar.h b/src/parser/prismparser/IntegerExpressionGrammar.h
index 5bc842192..c04150761 100644
--- a/src/parser/prismparser/IntegerExpressionGrammar.h
+++ b/src/parser/prismparser/IntegerExpressionGrammar.h
@@ -16,32 +16,32 @@
 #include <memory>
 
 namespace storm {
-namespace parser {
-namespace prism {
-
-/*!
- * This grammar parses a (non constant) integer expressions as used in prism models.
- */
-class IntegerExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<IntegerExpressionGrammar> {
-public:
-	IntegerExpressionGrammar(std::shared_ptr<VariableState>& state);
-	
-	/*!
-	 * Switch to second run.
-	 * Variable names may be any valid identifier in the first run, but only defined variables in the second run.
-	 */
-	virtual void prepareSecondRun();
-
-private:
-	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> integerExpression;
-	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> integerPlusExpression;
-	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerMultExpression;
-	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> atomicIntegerExpression;
-	qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerVariableExpression;
-};
-
-}
-}
+    namespace parser {
+        namespace prism {
+            
+            /*!
+             * This grammar parses a (non constant) integer expressions as used in prism models.
+             */
+            class IntegerExpressionGrammar : public qi::grammar<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused>, public BaseGrammar<IntegerExpressionGrammar> {
+            public:
+                IntegerExpressionGrammar(std::shared_ptr<VariableState> const& state);
+                
+                /*!
+                 * Switch to second run.
+                 * Variable names may be any valid identifier in the first run, but only defined variables in the second run.
+                 */
+                virtual void prepareSecondRun();
+                
+            private:
+                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper, Unused> integerExpression;
+                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), qi::locals<bool>, Skipper> integerPlusExpression;
+                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerMultExpression;
+                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> atomicIntegerExpression;
+                qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> integerVariableExpression;
+            };
+            
+        }
+    }
 }
 
 #endif	/* INTEGEREXPRESSIONGRAMMAR_H */
diff --git a/src/parser/prismparser/PrismGrammar.cpp b/src/parser/prismparser/PrismGrammar.cpp
index 0caa9b6aa..9a6819194 100644
--- a/src/parser/prismparser/PrismGrammar.cpp
+++ b/src/parser/prismparser/PrismGrammar.cpp
@@ -35,234 +35,243 @@ namespace qi = boost::spirit::qi;
 namespace phoenix = boost::phoenix;
 
 namespace storm {
-namespace parser {
-namespace prism {
-
-std::shared_ptr<BaseExpression> PrismGrammar::addIntegerConstant(std::string const& name, std::shared_ptr<BaseExpression> const& value) {
-	this->state->integerConstants_.add(name, value);
-	this->state->allConstantNames_.add(name, name);
-	return value;
-}
-
-void PrismGrammar::addLabel(std::string const& name, std::shared_ptr<BaseExpression> const& value, std::map<std::string, std::shared_ptr<BaseExpression>>& nameToExpressionMap) {
-	this->state->labelNames_.add(name, name);
-	nameToExpressionMap[name] = value;
-}
-    
-void PrismGrammar::addIntegerAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& value, std::map<std::string, Assignment>& variableToAssignmentMap) {
-	this->state->assignedIntegerVariables_.add(variable, variable);
-	variableToAssignmentMap[variable] = Assignment(variable, value);
-}
-    
-void PrismGrammar::addBooleanAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& value, std::map<std::string, Assignment>& variableToAssigmentMap) {
-	this->state->assignedBooleanVariables_.add(variable, variable);
-	variableToAssigmentMap[variable] = Assignment(variable, value);
-}
-    
-Module PrismGrammar::renameModule(std::string const& newName, std::string const& oldName, std::map<std::string, std::string> const& renaming) {
-	this->state->moduleNames_.add(newName, newName);
-	Module* old = this->moduleMap_.find(oldName);
-	if (old == nullptr) {
-		LOG4CPLUS_ERROR(logger, "Renaming module failed: module " << oldName << " does not exist.");
-		throw storm::exceptions::InvalidArgumentException() << "Renaming module failed: module " << oldName << " does not exist.";
-	}
-	Module res(*old, newName, renaming, *this->state);
-	this->moduleMap_.at(newName) = res;
-	return res;
-}
-    
-Module PrismGrammar::createModule(std::string const& name, std::vector<BooleanVariable> const& bools, std::vector<IntegerVariable> const& ints, std::map<std::string, uint_fast64_t> const& boolids, std::map<std::string, uint_fast64_t> const& intids, std::vector<storm::ir::Command> const& commands) {
-	this->state->moduleNames_.add(name, name);
-	Module res(name, bools, ints, boolids, intids, commands);
-	this->moduleMap_.at(name) = res;
-	return res;
-}
-
-void PrismGrammar::createIntegerVariable(std::string const& name, std::shared_ptr<BaseExpression> const& lower, std::shared_ptr<BaseExpression> const& upper, std::shared_ptr<BaseExpression> const& init, std::vector<IntegerVariable>& vars, std::map<std::string, uint_fast64_t>& varids, bool isGlobalVariable) {
-	uint_fast64_t id = this->state->addIntegerVariable(name);
-    uint_fast64_t newLocalIndex = this->state->nextLocalIntegerVariableIndex;
-	vars.emplace_back(newLocalIndex, id, name, lower, upper, init);
-	varids[name] = newLocalIndex;
-    ++this->state->nextLocalIntegerVariableIndex;
-	this->state->localIntegerVariables_.add(name, name);
-    if (isGlobalVariable) {
-        this->state->globalIntegerVariables_.add(name, name);
-    }
-}
-    
-void PrismGrammar::createBooleanVariable(std::string const& name, std::shared_ptr<BaseExpression> const& init, std::vector<BooleanVariable>& vars, std::map<std::string, uint_fast64_t>& varids, bool isGlobalVariable) {
-	uint_fast64_t id = this->state->addBooleanVariable(name);
-    uint_fast64_t newLocalIndex = this->state->nextLocalBooleanVariableIndex;
-	vars.emplace_back(newLocalIndex, id, name, init);
-	varids[name] = newLocalIndex;
-    ++this->state->nextLocalBooleanVariableIndex;
-	this->state->localBooleanVariables_.add(name, name);
-    if (isGlobalVariable) {
-        this->state->globalBooleanVariables_.add(name, name);
-    }
-}
-
-StateReward createStateReward(std::shared_ptr<BaseExpression> guard, std::shared_ptr<BaseExpression> reward) {
-	return StateReward(guard, reward);
-}
-TransitionReward createTransitionReward(std::string const& label, std::shared_ptr<BaseExpression> guard, std::shared_ptr<BaseExpression> reward) {
-	return TransitionReward(label, guard, reward);
-}
-void createRewardModel(std::string const& name, std::vector<StateReward>& stateRewards, std::vector<TransitionReward>& transitionRewards, std::map<std::string, RewardModel>& mapping) {
-	mapping[name] = RewardModel(name, stateRewards, transitionRewards);
-}
-Update PrismGrammar::createUpdate(std::shared_ptr<BaseExpression> likelihood, std::map<std::string, Assignment> const& bools, std::map<std::string, Assignment> const& ints) {
-    this->state->nextGlobalUpdateIndex++;
-	return Update(this->state->getNextGlobalUpdateIndex() - 1, likelihood, bools, ints);
-}
-Command PrismGrammar::createCommand(std::string const& label, std::shared_ptr<BaseExpression> guard, std::vector<Update> const& updates) {
-    this->state->nextGlobalCommandIndex++;
-	return Command(this->state->getNextGlobalCommandIndex() - 1, label, guard, updates);
-}
-Program createProgram(
-		Program::ModelType modelType,
-		std::map<std::string, std::shared_ptr<BooleanConstantExpression>> const& undefBoolConst,
-		std::map<std::string, std::shared_ptr<IntegerConstantExpression>> const& undefIntConst,
-		std::map<std::string, std::shared_ptr<DoubleConstantExpression>> const& undefDoubleConst,
-        GlobalVariableInformation const& globalVariableInformation,
-		std::vector<Module> const& modules,
-		std::map<std::string, RewardModel> const& rewards,
-		std::map<std::string, std::shared_ptr<BaseExpression>> const& labels) {
-	return Program(modelType, undefBoolConst, undefIntConst, undefDoubleConst,
-                   globalVariableInformation.booleanVariables, globalVariableInformation.integerVariables,
-                   globalVariableInformation.booleanVariableToIndexMap,
-                   globalVariableInformation.integerVariableToIndexMap, modules, rewards, labels);
-}
-
-PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new VariableState()) {
-
-	labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> FreeIdentifierGrammar::instance(this->state) >> -qi::lit("\"") >> qi::lit("=") >> BooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))
-			[phoenix::bind(&PrismGrammar::addLabel, this, qi::_1, qi::_2, qi::_r1)];
-	labelDefinition.name("label declaration");
-	labelDefinitionList %= *labelDefinition(qi::_r1);
-	labelDefinitionList.name("label declaration list");
-
-	// This block defines all entities that are needed for parsing a reward model.
-	stateRewardDefinition = (BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > ConstDoubleExpressionGrammar::instance(this->state) >> qi::lit(";"))[qi::_val = phoenix::bind(&createStateReward, qi::_1, qi::_2)];
-	stateRewardDefinition.name("state reward definition");
-	transitionRewardDefinition = (qi::lit("[") > -(commandName[qi::_a = qi::_1]) > qi::lit("]") > BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[qi::_val = phoenix::bind(&createTransitionReward, qi::_a, qi::_2, qi::_3)];
-	transitionRewardDefinition.name("transition reward definition");
-	rewardDefinition = (qi::lit("rewards") > qi::lit("\"") > FreeIdentifierGrammar::instance(this->state) > qi::lit("\"") > +(stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) >> qi::lit("endrewards"))
-			[phoenix::bind(&createRewardModel, qi::_1, qi::_a, qi::_b, qi::_r1)];
-	rewardDefinition.name("reward definition");
-	rewardDefinitionList = *rewardDefinition(qi::_r1);
-	rewardDefinitionList.name("reward definition list");
-
-	commandName %= this->state->commandNames_;
-	commandName.name("command name");
-	unassignedLocalBooleanVariableName %= (this->state->localBooleanVariables_ | this->state->globalBooleanVariables_) - this->state->assignedBooleanVariables_;
-	unassignedLocalBooleanVariableName.name("unassigned local/global boolean variable");
-	unassignedLocalIntegerVariableName %= (this->state->localIntegerVariables_ | this->state->globalIntegerVariables_) - this->state->assignedIntegerVariables_;
-	unassignedLocalIntegerVariableName.name("unassigned local/global integer variable");
-
-	// This block defines all entities that are needed for parsing a single command.
-	assignmentDefinition =
-			(qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > IntegerExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addIntegerAssignment, this, qi::_1, qi::_2, qi::_r2)] |
-			(qi::lit("(") >> unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > BooleanExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addBooleanAssignment, this, qi::_1, qi::_2, qi::_r1)];
-	assignmentDefinition.name("assignment");
-	assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&";
-	assignmentDefinitionList.name("assignment list");
-	updateDefinition = (ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, this, qi::_1, qi::_a, qi::_b)];
-	updateDefinition.name("update");
-	updateListDefinition = +updateDefinition % "+";
-	updateListDefinition.name("update list");
-	commandDefinition = (
-				qi::lit("[") > -(
-					(FreeIdentifierGrammar::instance(this->state)[phoenix::bind(this->state->commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1]
-				) > qi::lit("]") > BooleanExpressionGrammar::instance(this->state) > qi::lit("->") > updateListDefinition > qi::lit(";")
-                )[qi::_val = phoenix::bind(&PrismGrammar::createCommand, this, qi::_a, qi::_2, qi::_3)];
-	commandDefinition.name("command");
-
-	// This block defines all entities that are needed for parsing variable definitions.
-	booleanVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > ConstBooleanExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
-		[phoenix::bind(&PrismGrammar::createBooleanVariable, this, qi::_1, qi::_b, qi::_r1, qi::_r2, qi::_r3)];
-	booleanVariableDefinition.name("boolean variable declaration");
-
-	integerVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("[") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("..") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("]") > -(qi::lit("init") > ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
-        [phoenix::bind(&PrismGrammar::createIntegerVariable, this, qi::_1, qi::_2, qi::_3, qi::_b, qi::_r1, qi::_r2, qi::_r3)];
-	integerVariableDefinition.name("integer variable declaration");
-	variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3, false) | integerVariableDefinition(qi::_r2, qi::_r4, false));
-	variableDefinition.name("variable declaration");
-
-	// This block defines all entities that are needed for parsing a module.
-	moduleDefinition = (qi::lit("module") >> FreeIdentifierGrammar::instance(this->state)[phoenix::bind(&VariableState::clearLocalVariables, *this->state)]
-			>> *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) >> +commandDefinition > qi::lit("endmodule"))
-			[qi::_val = phoenix::bind(&PrismGrammar::createModule, this, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)];
-
-	moduleDefinition.name("module");
-	moduleRenaming = (qi::lit("module")	>> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=")
-			> this->state->moduleNames_ > qi::lit("[") > *(
-					(IdentifierGrammar::instance(this->state) > qi::lit("=") > IdentifierGrammar::instance(this->state) >> -qi::lit(","))[phoenix::insert(qi::_a, phoenix::construct<std::pair<std::string,std::string>>(qi::_1, qi::_2))]
-			) > qi::lit("]") > qi::lit("endmodule"))
-			[qi::_val = phoenix::bind(&PrismGrammar::renameModule, this, qi::_1, qi::_2, qi::_a)];
-	moduleRenaming.name("renamed module");
-	moduleDefinitionList %= +(moduleDefinition | moduleRenaming);
-	moduleDefinitionList.name("module list");
-
-    // This block defines all entities that are needed for parsing global variable definitions.
-    globalVariableDefinitionList = *(qi::lit("global") > (booleanVariableDefinition(bind(&GlobalVariableInformation::booleanVariables, qi::_r1), bind(&GlobalVariableInformation::booleanVariableToIndexMap, qi::_r1), true) | integerVariableDefinition(bind(&GlobalVariableInformation::integerVariables, qi::_r1), bind(&GlobalVariableInformation::integerVariableToIndexMap, qi::_r1), true)));
-    globalVariableDefinitionList.name("global variable declaration list");
-    
-	// This block defines all entities that are needed for parsing constant definitions.
-	definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstBooleanExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
-	definedBooleanConstantDefinition.name("defined boolean constant declaration");
-	definedIntegerConstantDefinition = (
-			qi::lit("const") >> qi::lit("int") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >>
-			ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";")
-		)[ qi::_val = phoenix::bind(&PrismGrammar::addIntegerConstant, this, qi::_1, qi::_2) ];
-	definedIntegerConstantDefinition.name("defined integer constant declaration");
-	definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
-	definedDoubleConstantDefinition.name("defined double constant declaration");
-	undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<BooleanConstantExpression>>(phoenix::new_<BooleanConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<BooleanConstantExpression>>>(qi::_1, qi::_a)), phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)];
-	undefinedBooleanConstantDefinition.name("undefined boolean constant declaration");
-	undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<IntegerConstantExpression>>(phoenix::new_<IntegerConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<IntegerConstantExpression>>>(qi::_1, qi::_a)), phoenix::bind(this->state->integerConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)];
-	undefinedIntegerConstantDefinition.name("undefined integer constant declaration");
-	undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[qi::_a = phoenix::construct<std::shared_ptr<DoubleConstantExpression>>(phoenix::new_<DoubleConstantExpression>(qi::_1)), phoenix::insert(qi::_r1, phoenix::construct<std::pair<std::string, std::shared_ptr<DoubleConstantExpression>>>(qi::_1, qi::_a)), phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_a), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1)];
-	undefinedDoubleConstantDefinition.name("undefined double constant declaration");
-	definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition);
-	definedConstantDefinition.name("defined constant declaration");
-	undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3));
-	undefinedConstantDefinition.name("undefined constant declaration");
-	constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3));
-	constantDefinitionList.name("constant declaration list");
-
-	// This block defines all entities that are needed for parsing a program.
-	modelTypeDefinition = modelType_;
-	modelTypeDefinition.name("model type");
-	start = (
-			modelTypeDefinition >
-			constantDefinitionList(qi::_a, qi::_b, qi::_c) >
-            globalVariableDefinitionList(qi::_d) >
-			moduleDefinitionList >
-			rewardDefinitionList(qi::_e) >
-			labelDefinitionList(qi::_f))[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2, qi::_e, qi::_f)];
-	start.name("probabilistic program declaration");
-}
-
-void PrismGrammar::prepareForSecondRun() {
-	LOG4CPLUS_INFO(logger, "Preparing parser for second run.");
-	this->state->prepareForSecondRun();
-	BooleanExpressionGrammar::secondRun();
-	ConstBooleanExpressionGrammar::secondRun();
-	ConstDoubleExpressionGrammar::secondRun();
-	ConstIntegerExpressionGrammar::secondRun();
-	IntegerExpressionGrammar::secondRun();
-}
-
-void PrismGrammar::resetGrammars() {
-	LOG4CPLUS_INFO(logger, "Resetting grammars.");
-	BooleanExpressionGrammar::resetInstance();
-	ConstBooleanExpressionGrammar::resetInstance();
-	ConstDoubleExpressionGrammar::resetInstance();
-	ConstIntegerExpressionGrammar::resetInstance();
-	IntegerExpressionGrammar::resetInstance();
-}
-
-} // namespace prism
-} // namespace parser
+    namespace parser {
+        namespace prism {
+            
+            void PrismGrammar::addLabel(std::string const& name, std::shared_ptr<BaseExpression> const& value, std::map<std::string, std::unique_ptr<BaseExpression>>& nameToExpressionMap) {
+                this->state->labelNames_.add(name, name);
+                nameToExpressionMap[name] = value->clone();
+            }
+            
+            void PrismGrammar::addIntegerAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& value, std::map<std::string, Assignment>& variableToAssignmentMap) {
+                this->state->assignedIntegerVariables_.add(variable, variable);
+                variableToAssignmentMap[variable] = Assignment(variable, value->clone());
+            }
+            
+            void PrismGrammar::addBooleanAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& value, std::map<std::string, Assignment>& variableToAssigmentMap) {
+                this->state->assignedBooleanVariables_.add(variable, variable);
+                variableToAssigmentMap[variable] = Assignment(variable, value->clone());
+            }
+            
+            void PrismGrammar::addUndefinedBooleanConstant(std::string const& name, std::map<std::string, std::unique_ptr<BooleanConstantExpression>>& nameToExpressionMap) {
+                this->state->booleanConstants_.add(name, std::shared_ptr<BaseExpression>(new BooleanConstantExpression(name)));
+                this->state->allConstantNames_.add(name, name);
+                nameToExpressionMap.emplace(name, std::unique_ptr<BooleanConstantExpression>(new BooleanConstantExpression(dynamic_cast<BooleanConstantExpression&>(*this->state->booleanConstants_.at(name)))));
+            }
+            
+            void PrismGrammar::addUndefinedIntegerConstant(std::string const& name, std::map<std::string, std::unique_ptr<IntegerConstantExpression>>& nameToExpressionMap) {
+                this->state->integerConstants_.add(name, std::shared_ptr<BaseExpression>(new IntegerConstantExpression(name)));
+                this->state->allConstantNames_.add(name, name);
+                nameToExpressionMap.emplace(name, std::unique_ptr<IntegerConstantExpression>(new IntegerConstantExpression(dynamic_cast<IntegerConstantExpression&>(*this->state->integerConstants_.at(name)))));
+            }
+            
+            void PrismGrammar::addUndefinedDoubleConstant(std::string const& name, std::map<std::string, std::unique_ptr<DoubleConstantExpression>>& nameToExpressionMap) {
+                this->state->doubleConstants_.add(name, std::shared_ptr<BaseExpression>(new DoubleConstantExpression(name)));
+                this->state->allConstantNames_.add(name, name);
+                nameToExpressionMap.emplace(name, std::unique_ptr<DoubleConstantExpression>(new DoubleConstantExpression(dynamic_cast<DoubleConstantExpression&>(*this->state->doubleConstants_.at(name)))));
+            }
+            
+            Module PrismGrammar::renameModule(std::string const& newName, std::string const& oldName, std::map<std::string, std::string> const& renaming) {
+                this->state->moduleNames_.add(newName, newName);
+                Module* old = this->moduleMap_.find(oldName);
+                if (old == nullptr) {
+                    LOG4CPLUS_ERROR(logger, "Renaming module failed: module " << oldName << " does not exist.");
+                    throw storm::exceptions::InvalidArgumentException() << "Renaming module failed: module " << oldName << " does not exist.";
+                }
+                Module res(*old, newName, renaming, *this->state);
+                this->moduleMap_.at(newName) = res;
+                return res;
+            }
+            
+            Module PrismGrammar::createModule(std::string const& name, std::vector<BooleanVariable> const& bools, std::vector<IntegerVariable> const& ints, std::map<std::string, uint_fast64_t> const& boolids, std::map<std::string, uint_fast64_t> const& intids, std::vector<storm::ir::Command> const& commands) {
+                this->state->moduleNames_.add(name, name);
+                Module res(name, bools, ints, boolids, intids, commands);
+                this->moduleMap_.at(name) = res;
+                return res;
+            }
+            
+            void PrismGrammar::createIntegerVariable(std::string const& name, std::shared_ptr<BaseExpression> const& lower, std::shared_ptr<BaseExpression> const& upper, std::shared_ptr<BaseExpression> const& init, std::vector<IntegerVariable>& vars, std::map<std::string, uint_fast64_t>& varids, bool isGlobalVariable) {
+                uint_fast64_t id = this->state->addIntegerVariable(name);
+                uint_fast64_t newLocalIndex = this->state->nextLocalIntegerVariableIndex;
+                vars.emplace_back(newLocalIndex, id, name, lower->clone(), upper->clone(), init->clone());
+                varids[name] = newLocalIndex;
+                ++this->state->nextLocalIntegerVariableIndex;
+                this->state->localIntegerVariables_.add(name, name);
+                if (isGlobalVariable) {
+                    this->state->globalIntegerVariables_.add(name, name);
+                }
+            }
+            
+            void PrismGrammar::createBooleanVariable(std::string const& name, std::shared_ptr<BaseExpression> const& init, std::vector<BooleanVariable>& vars, std::map<std::string, uint_fast64_t>& varids, bool isGlobalVariable) {
+                uint_fast64_t id = this->state->addBooleanVariable(name);
+                uint_fast64_t newLocalIndex = this->state->nextLocalBooleanVariableIndex;
+                vars.emplace_back(newLocalIndex, id, name, init->clone());
+                varids[name] = newLocalIndex;
+                ++this->state->nextLocalBooleanVariableIndex;
+                this->state->localBooleanVariables_.add(name, name);
+                if (isGlobalVariable) {
+                    this->state->globalBooleanVariables_.add(name, name);
+                }
+            }
+            
+            StateReward createStateReward(std::shared_ptr<BaseExpression> const& guard, std::shared_ptr<BaseExpression> const& reward) {
+                return StateReward(guard->clone(), reward->clone());
+            }
+            TransitionReward createTransitionReward(std::string const& label, std::shared_ptr<BaseExpression> const& guard, std::shared_ptr<BaseExpression> const& reward) {
+                return TransitionReward(label, guard->clone(), reward->clone());
+            }
+            void createRewardModel(std::string const& name, std::vector<StateReward>& stateRewards, std::vector<TransitionReward>& transitionRewards, std::map<std::string, RewardModel>& mapping) {
+                mapping[name] = RewardModel(name, stateRewards, transitionRewards);
+            }
+            Update PrismGrammar::createUpdate(std::shared_ptr<BaseExpression> const& likelihood, std::map<std::string, Assignment> const& bools, std::map<std::string, Assignment> const& ints) {
+                this->state->nextGlobalUpdateIndex++;
+                return Update(this->state->getNextGlobalUpdateIndex() - 1, likelihood->clone(), bools, ints);
+            }
+            Command PrismGrammar::createCommand(std::string const& label, std::shared_ptr<BaseExpression> const& guard, std::vector<Update> const& updates) {
+                this->state->nextGlobalCommandIndex++;
+                return Command(this->state->getNextGlobalCommandIndex() - 1, label, guard->clone(), updates);
+            }
+            Program createProgram(
+                                  Program::ModelType modelType,
+                                  std::map<std::string, std::unique_ptr<BooleanConstantExpression>> const& undefBoolConst,
+                                  std::map<std::string, std::unique_ptr<IntegerConstantExpression>> const& undefIntConst,
+                                  std::map<std::string, std::unique_ptr<DoubleConstantExpression>> const& undefDoubleConst,
+                                  GlobalVariableInformation const& globalVariableInformation,
+                                  std::vector<Module> const& modules,
+                                  std::map<std::string, RewardModel> const& rewards,
+                                  std::map<std::string, std::unique_ptr<BaseExpression>> const& labels) {
+                return Program(modelType, undefBoolConst, undefIntConst, undefDoubleConst,
+                               globalVariableInformation.booleanVariables, globalVariableInformation.integerVariables,
+                               globalVariableInformation.booleanVariableToIndexMap,
+                               globalVariableInformation.integerVariableToIndexMap, modules, rewards, labels);
+            }
+            
+            PrismGrammar::PrismGrammar() : PrismGrammar::base_type(start), state(new VariableState()) {
+                
+                labelDefinition = (qi::lit("label") >> -qi::lit("\"") >> FreeIdentifierGrammar::instance(this->state) >> -qi::lit("\"") >> qi::lit("=") >> BooleanExpressionGrammar::instance(this->state) >> qi::lit(";"))
+                [phoenix::bind(&PrismGrammar::addLabel, this, qi::_1, qi::_2, qi::_r1)];
+                labelDefinition.name("label declaration");
+                labelDefinitionList %= *labelDefinition(qi::_r1);
+                labelDefinitionList.name("label declaration list");
+                
+                // This block defines all entities that are needed for parsing a reward model.
+                stateRewardDefinition = (BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > ConstDoubleExpressionGrammar::instance(this->state) >> qi::lit(";"))[qi::_val = phoenix::bind(&createStateReward, qi::_1, qi::_2)];
+                stateRewardDefinition.name("state reward definition");
+                transitionRewardDefinition = (qi::lit("[") > -(commandName[qi::_a = qi::_1]) > qi::lit("]") > BooleanExpressionGrammar::instance(this->state) > qi::lit(":") > ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[qi::_val = phoenix::bind(&createTransitionReward, qi::_a, qi::_2, qi::_3)];
+                transitionRewardDefinition.name("transition reward definition");
+                rewardDefinition = (qi::lit("rewards") > qi::lit("\"") > FreeIdentifierGrammar::instance(this->state) > qi::lit("\"") > +(stateRewardDefinition[phoenix::push_back(qi::_a, qi::_1)] | transitionRewardDefinition[phoenix::push_back(qi::_b, qi::_1)]) >> qi::lit("endrewards"))
+                [phoenix::bind(&createRewardModel, qi::_1, qi::_a, qi::_b, qi::_r1)];
+                rewardDefinition.name("reward definition");
+                rewardDefinitionList = *rewardDefinition(qi::_r1);
+                rewardDefinitionList.name("reward definition list");
+                
+                commandName %= this->state->commandNames_;
+                commandName.name("command name");
+                unassignedLocalBooleanVariableName %= (this->state->localBooleanVariables_ | this->state->globalBooleanVariables_) - this->state->assignedBooleanVariables_;
+                unassignedLocalBooleanVariableName.name("unassigned local/global boolean variable");
+                unassignedLocalIntegerVariableName %= (this->state->localIntegerVariables_ | this->state->globalIntegerVariables_) - this->state->assignedIntegerVariables_;
+                unassignedLocalIntegerVariableName.name("unassigned local/global integer variable");
+                
+                // This block defines all entities that are needed for parsing a single command.
+                assignmentDefinition =
+                (qi::lit("(") >> unassignedLocalIntegerVariableName > qi::lit("'") > qi::lit("=") > IntegerExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addIntegerAssignment, this, qi::_1, qi::_2, qi::_r2)] |
+                (qi::lit("(") >> unassignedLocalBooleanVariableName > qi::lit("'") > qi::lit("=") > BooleanExpressionGrammar::instance(this->state) > qi::lit(")"))[phoenix::bind(&PrismGrammar::addBooleanAssignment, this, qi::_1, qi::_2, qi::_r1)];
+                assignmentDefinition.name("assignment");
+                assignmentDefinitionList = assignmentDefinition(qi::_r1, qi::_r2) % "&";
+                assignmentDefinitionList.name("assignment list");
+                updateDefinition = (ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(":")[phoenix::clear(phoenix::ref(this->state->assignedBooleanVariables_)), phoenix::clear(phoenix::ref(this->state->assignedIntegerVariables_))] > assignmentDefinitionList(qi::_a, qi::_b))[qi::_val = phoenix::bind(&PrismGrammar::createUpdate, this, qi::_1, qi::_a, qi::_b)];
+                updateDefinition.name("update");
+                updateListDefinition = +updateDefinition % "+";
+                updateListDefinition.name("update list");
+                commandDefinition = (
+                                     qi::lit("[") > -(
+                                                      (FreeIdentifierGrammar::instance(this->state)[phoenix::bind(this->state->commandNames_.add, qi::_1, qi::_1)] | commandName)[qi::_a = qi::_1]
+                                                      ) > qi::lit("]") > BooleanExpressionGrammar::instance(this->state) > qi::lit("->") > updateListDefinition > qi::lit(";")
+                                     )[qi::_val = phoenix::bind(&PrismGrammar::createCommand, this, qi::_a, qi::_2, qi::_3)];
+                commandDefinition.name("command");
+                
+                // This block defines all entities that are needed for parsing variable definitions.
+                booleanVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("bool") > -(qi::lit("init") > ConstBooleanExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
+                [phoenix::bind(&PrismGrammar::createBooleanVariable, this, qi::_1, qi::_b, qi::_r1, qi::_r2, qi::_r3)];
+                booleanVariableDefinition.name("boolean variable declaration");
+                
+                integerVariableDefinition = (FreeIdentifierGrammar::instance(this->state) >> qi::lit(":") >> qi::lit("[") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("..") > ConstIntegerExpressionGrammar::instance(this->state) > qi::lit("]") > -(qi::lit("init") > ConstIntegerExpressionGrammar::instance(this->state)[qi::_b = phoenix::construct<std::shared_ptr<BaseExpression>>(qi::_1)]) > qi::lit(";"))
+                [phoenix::bind(&PrismGrammar::createIntegerVariable, this, qi::_1, qi::_2, qi::_3, qi::_b, qi::_r1, qi::_r2, qi::_r3)];
+                integerVariableDefinition.name("integer variable declaration");
+                variableDefinition = (booleanVariableDefinition(qi::_r1, qi::_r3, false) | integerVariableDefinition(qi::_r2, qi::_r4, false));
+                variableDefinition.name("variable declaration");
+                
+                // This block defines all entities that are needed for parsing a module.
+                moduleDefinition = (qi::lit("module") >> FreeIdentifierGrammar::instance(this->state)[phoenix::bind(&VariableState::clearLocalVariables, *this->state)]
+                                    >> *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) >> +commandDefinition > qi::lit("endmodule"))
+                [qi::_val = phoenix::bind(&PrismGrammar::createModule, this, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)];
+                
+                moduleDefinition.name("module");
+                moduleRenaming = (qi::lit("module")	>> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=")
+                                  > this->state->moduleNames_ > qi::lit("[") > *(
+                                                                                 (IdentifierGrammar::instance(this->state) > qi::lit("=") > IdentifierGrammar::instance(this->state) >> -qi::lit(","))[phoenix::insert(qi::_a, phoenix::construct<std::pair<std::string,std::string>>(qi::_1, qi::_2))]
+                                                                                 ) > qi::lit("]") > qi::lit("endmodule"))
+                [qi::_val = phoenix::bind(&PrismGrammar::renameModule, this, qi::_1, qi::_2, qi::_a)];
+                moduleRenaming.name("renamed module");
+                moduleDefinitionList %= +(moduleDefinition | moduleRenaming);
+                moduleDefinitionList.name("module list");
+                
+                // This block defines all entities that are needed for parsing global variable definitions.
+                globalVariableDefinitionList = *(qi::lit("global") > (booleanVariableDefinition(bind(&GlobalVariableInformation::booleanVariables, qi::_r1), bind(&GlobalVariableInformation::booleanVariableToIndexMap, qi::_r1), true) | integerVariableDefinition(bind(&GlobalVariableInformation::integerVariables, qi::_r1), bind(&GlobalVariableInformation::integerVariableToIndexMap, qi::_r1), true)));
+                globalVariableDefinitionList.name("global variable declaration list");
+                
+                // This block defines all entities that are needed for parsing constant definitions.
+                definedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstBooleanExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->booleanConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
+                definedBooleanConstantDefinition.name("defined boolean constant declaration");
+                definedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") >> ConstIntegerExpressionGrammar::instance(this->state) >> qi::lit(";"))[phoenix::bind(this->state->integerConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
+                definedIntegerConstantDefinition.name("defined integer constant declaration");
+                definedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") >> FreeIdentifierGrammar::instance(this->state) >> qi::lit("=") > ConstDoubleExpressionGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(this->state->doubleConstants_.add, qi::_1, qi::_2), phoenix::bind(this->state->allConstantNames_.add, qi::_1, qi::_1), qi::_val = qi::_2];
+                definedDoubleConstantDefinition.name("defined double constant declaration");
+                undefinedBooleanConstantDefinition = (qi::lit("const") >> qi::lit("bool") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedBooleanConstant, this, qi::_1, qi::_r1)];
+                undefinedBooleanConstantDefinition.name("undefined boolean constant declaration");
+                undefinedIntegerConstantDefinition = (qi::lit("const") >> qi::lit("int") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedIntegerConstant, this, qi::_1, qi::_r1)]; 
+                undefinedIntegerConstantDefinition.name("undefined integer constant declaration");
+                undefinedDoubleConstantDefinition = (qi::lit("const") >> qi::lit("double") > FreeIdentifierGrammar::instance(this->state) > qi::lit(";"))[phoenix::bind(&PrismGrammar::addUndefinedDoubleConstant, this, qi::_1, qi::_r1)];
+                undefinedDoubleConstantDefinition.name("undefined double constant declaration");
+                definedConstantDefinition %= (definedBooleanConstantDefinition | definedIntegerConstantDefinition | definedDoubleConstantDefinition);
+                definedConstantDefinition.name("defined constant declaration");
+                undefinedConstantDefinition = (undefinedBooleanConstantDefinition(qi::_r1) | undefinedIntegerConstantDefinition(qi::_r2) | undefinedDoubleConstantDefinition(qi::_r3));
+                undefinedConstantDefinition.name("undefined constant declaration");
+                constantDefinitionList = *(definedConstantDefinition | undefinedConstantDefinition(qi::_r1, qi::_r2, qi::_r3));
+                constantDefinitionList.name("constant declaration list");
+                
+                // This block defines all entities that are needed for parsing a program.
+                modelTypeDefinition = modelType_;
+                modelTypeDefinition.name("model type");
+                start = (
+                         modelTypeDefinition >
+                         constantDefinitionList(qi::_a, qi::_b, qi::_c) >
+                         globalVariableDefinitionList(qi::_d) >
+                         moduleDefinitionList >
+                         rewardDefinitionList(qi::_e) >
+                         labelDefinitionList(qi::_f))[qi::_val = phoenix::bind(&createProgram, qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2, qi::_e, qi::_f)];
+                start.name("probabilistic program declaration");
+            }
+            
+            void PrismGrammar::prepareForSecondRun() {
+                LOG4CPLUS_INFO(logger, "Preparing parser for second run.");
+                this->state->prepareForSecondRun();
+                BooleanExpressionGrammar::secondRun();
+                ConstBooleanExpressionGrammar::secondRun();
+                ConstDoubleExpressionGrammar::secondRun();
+                ConstIntegerExpressionGrammar::secondRun();
+                IntegerExpressionGrammar::secondRun();
+            }
+            
+            void PrismGrammar::resetGrammars() {
+                LOG4CPLUS_INFO(logger, "Resetting grammars.");
+                BooleanExpressionGrammar::resetInstance();
+                ConstBooleanExpressionGrammar::resetInstance();
+                ConstDoubleExpressionGrammar::resetInstance();
+                ConstIntegerExpressionGrammar::resetInstance();
+                IntegerExpressionGrammar::resetInstance();
+            }
+            
+        } // namespace prism
+    } // namespace parser
 } // namespace storm
diff --git a/src/parser/prismparser/PrismGrammar.h b/src/parser/prismparser/PrismGrammar.h
index 7dd8e80a0..d71fefd9f 100644
--- a/src/parser/prismparser/PrismGrammar.h
+++ b/src/parser/prismparser/PrismGrammar.h
@@ -46,12 +46,12 @@ namespace storm {
             Iterator,
             Program(),
             qi::locals<
-            std::map<std::string, std::shared_ptr<BooleanConstantExpression>>,
-            std::map<std::string, std::shared_ptr<IntegerConstantExpression>>,
-            std::map<std::string, std::shared_ptr<DoubleConstantExpression>>,
+            std::map<std::string, std::unique_ptr<BooleanConstantExpression>>,
+            std::map<std::string, std::unique_ptr<IntegerConstantExpression>>,
+            std::map<std::string, std::unique_ptr<DoubleConstantExpression>>,
             GlobalVariableInformation,
             std::map<std::string, RewardModel>,
-            std::map<std::string, std::shared_ptr<BaseExpression>>
+            std::map<std::string, std::unique_ptr<BaseExpression>>
             >,
             Skipper> {
             public:
@@ -82,16 +82,16 @@ namespace storm {
                 Iterator,
                 Program(),
                 qi::locals<
-				std::map<std::string, std::shared_ptr<BooleanConstantExpression>>,
-				std::map<std::string, std::shared_ptr<IntegerConstantExpression>>,
-				std::map<std::string, std::shared_ptr<DoubleConstantExpression>>,
+				std::map<std::string, std::unique_ptr<BooleanConstantExpression>>,
+				std::map<std::string, std::unique_ptr<IntegerConstantExpression>>,
+				std::map<std::string, std::unique_ptr<DoubleConstantExpression>>,
                 GlobalVariableInformation,
 				std::map<std::string, RewardModel>,
-				std::map<std::string, std::shared_ptr<BaseExpression>>
+				std::map<std::string, std::unique_ptr<BaseExpression>>
                 >,
                 Skipper> start;
                 qi::rule<Iterator, Program::ModelType(), Skipper> modelTypeDefinition;
-                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), Skipper> constantDefinitionList;
+                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BooleanConstantExpression>>&, std::map<std::string, std::unique_ptr<IntegerConstantExpression>>&, std::map<std::string, std::unique_ptr<DoubleConstantExpression>>&), Skipper> constantDefinitionList;
                 qi::rule<Iterator, std::vector<Module>(), Skipper> moduleDefinitionList;
                 
                 // Rules for global variable definitions
@@ -125,16 +125,16 @@ namespace storm {
                 qi::rule<Iterator, TransitionReward(), qi::locals<std::string>, Skipper> transitionRewardDefinition;
                 
                 // Rules for label definitions.
-                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BaseExpression>>&), Skipper> labelDefinitionList;
-                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BaseExpression>>&), Skipper> labelDefinition;
+                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BaseExpression>>&), Skipper> labelDefinitionList;
+                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BaseExpression>>&), Skipper> labelDefinition;
                 
                 // Rules for constant definitions.
                 qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> constantDefinition;
-                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&, std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&, std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), Skipper> undefinedConstantDefinition;
+                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BooleanConstantExpression>>&, std::map<std::string, std::unique_ptr<IntegerConstantExpression>>&, std::map<std::string, std::unique_ptr<DoubleConstantExpression>>&), Skipper> undefinedConstantDefinition;
                 qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedConstantDefinition;
-                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<BooleanConstantExpression>>&), qi::locals<std::shared_ptr<BooleanConstantExpression>>, Skipper> undefinedBooleanConstantDefinition;
-                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<IntegerConstantExpression>>&), qi::locals<std::shared_ptr<IntegerConstantExpression>>, Skipper> undefinedIntegerConstantDefinition;
-                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::shared_ptr<DoubleConstantExpression>>&), qi::locals<std::shared_ptr<DoubleConstantExpression>>, Skipper> undefinedDoubleConstantDefinition;
+                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<BooleanConstantExpression>>&), Skipper> undefinedBooleanConstantDefinition;
+                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<IntegerConstantExpression>>&), Skipper> undefinedIntegerConstantDefinition;
+                qi::rule<Iterator, qi::unused_type(std::map<std::string, std::unique_ptr<DoubleConstantExpression>>&), Skipper> undefinedDoubleConstantDefinition;
                 qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedBooleanConstantDefinition;
                 qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedIntegerConstantDefinition;
                 qi::rule<Iterator, std::shared_ptr<BaseExpression>(), Skipper> definedDoubleConstantDefinition;
@@ -147,14 +147,6 @@ namespace storm {
                 storm::parser::prism::modelTypeStruct modelType_;
                 storm::parser::prism::relationalOperatorStruct relations_;
                 
-                /*!
-                 * Adds a constant of type integer with the given name and value.
-                 *
-                 * @param name The name of the constant.
-                 * @param value An expression definining the value of the constant.
-                 */
-                std::shared_ptr<BaseExpression> addIntegerConstant(std::string const& name, std::shared_ptr<BaseExpression> const& value);
-                
                 /*!
                  * Adds a label with the given name and expression to the given label-to-expression map.
                  *
@@ -162,7 +154,7 @@ namespace storm {
                  * @param expression The expression associated with the label.
                  * @param nameToExpressionMap The map to which the label is added.
                  */
-                void addLabel(std::string const& name, std::shared_ptr<BaseExpression> const& value, std::map<std::string, std::shared_ptr<BaseExpression>>& nameToExpressionMap);
+                void addLabel(std::string const& name, std::shared_ptr<BaseExpression> const& value, std::map<std::string, std::unique_ptr<BaseExpression>>& nameToExpressionMap);
                 
                 /*!
                  * Adds a boolean assignment for the given variable with the given expression and adds it to the
@@ -182,8 +174,14 @@ namespace storm {
                  * @param expression The expression that is assigned to the variable.
                  * @param variableToAssignmentMap The map to which the assignment is added.
                  */
-                void addIntegerAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& value, std::map<std::string, Assignment>& variableToAssignmentMap);
+                void addIntegerAssignment(std::string const& variable, std::shared_ptr<BaseExpression> const& expression, std::map<std::string, Assignment>& variableToAssignmentMap);
                 
+                void addUndefinedBooleanConstant(std::string const& name, std::map<std::string, std::unique_ptr<BooleanConstantExpression>>& nameToExpressionMap);
+
+                void addUndefinedIntegerConstant(std::string const& name, std::map<std::string, std::unique_ptr<IntegerConstantExpression>>& nameToExpressionMap);
+
+                void addUndefinedDoubleConstant(std::string const& name, std::map<std::string, std::unique_ptr<DoubleConstantExpression>>& nameToExpressionMap);
+
                 /*!
                  * Creates a module by renaming, i.e. takes the module given by the old name, creates a new module
                  * with the given name which renames all identifiers according to the given mapping.
@@ -237,7 +235,7 @@ namespace storm {
                  * @param guard The guard of the command.
                  * @param updates The updates associated with the command.
                  */
-                Command createCommand(std::string const& label, std::shared_ptr<BaseExpression> guard, std::vector<Update> const& updates);
+                Command createCommand(std::string const& label, std::shared_ptr<BaseExpression> const& guard, std::vector<Update> const& updates);
                 
                 /*!
                  * Creates an update with the given likelihood and the given assignments to boolean and integer variables, respectively.
@@ -246,7 +244,7 @@ namespace storm {
                  * @param booleanAssignments The assignments to boolean variables this update involves.
                  * @param integerAssignments The assignments to integer variables this update involves.
                  */
-                Update createUpdate(std::shared_ptr<BaseExpression> likelihood, std::map<std::string, Assignment> const& booleanAssignments, std::map<std::string, Assignment> const& integerAssignments);
+                Update createUpdate(std::shared_ptr<BaseExpression> const& likelihood, std::map<std::string, Assignment> const& booleanAssignments, std::map<std::string, Assignment> const& integerAssignments);
                 
             };