diff --git a/src/parser/ExpressionParser.cpp b/src/parser/ExpressionParser.cpp
index 052f4470c..19ff25040 100644
--- a/src/parser/ExpressionParser.cpp
+++ b/src/parser/ExpressionParser.cpp
@@ -5,7 +5,7 @@
 
 namespace storm {
     namespace parser {
-        ExpressionParser::ExpressionParser(qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), powerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), trueFalse_(), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) {
+        ExpressionParser::ExpressionParser(storm::expressions::ExpressionManager& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_) : ExpressionParser::base_type(expression), orOperator_(), andOperator_(), equalityOperator_(), relationalOperator_(), plusOperator_(), multiplicationOperator_(), powerOperator_(), unaryOperator_(), floorCeilOperator_(), minMaxOperator_(), trueFalse_(manager), manager(manager), createExpressions(false), acceptDoubleLiterals(true), identifiers_(nullptr), invalidIdentifiers_(invalidIdentifiers_) {
             identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&ExpressionParser::isValidIdentifier, phoenix::ref(*this), qi::_1)];
             identifier.name("identifier");
             
@@ -98,7 +98,7 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
                 }
             }
-            return storm::expressions::Expression::createFalse();
+            return manager.boolean(false);
         }
                 
         storm::expressions::Expression ExpressionParser::createOrExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@@ -113,7 +113,7 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
                 }
             }
-            return storm::expressions::Expression::createFalse();
+            return manager.boolean(false);
         }
         
         storm::expressions::Expression ExpressionParser::createAndExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@@ -127,7 +127,7 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
                 }
             }
-            return storm::expressions::Expression::createFalse();
+            return manager.boolean(false);
         }
         
         storm::expressions::Expression ExpressionParser::createRelationalExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@@ -144,7 +144,7 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
                 }
             }
-            return storm::expressions::Expression::createFalse();
+            return manager.boolean(false);
         }
         
         storm::expressions::Expression ExpressionParser::createEqualsExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@@ -159,7 +159,7 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
                 }
             }
-            return storm::expressions::Expression::createFalse();
+            return manager.boolean(false);
         }
         
         storm::expressions::Expression ExpressionParser::createPlusExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@@ -174,7 +174,7 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
                 }
             }
-            return storm::expressions::Expression::createFalse();
+            return manager.boolean(false);
         }
         
         storm::expressions::Expression ExpressionParser::createMultExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@@ -189,7 +189,7 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
                 }
             }
-            return storm::expressions::Expression::createFalse();
+            return manager.boolean(false);
         }
         
         storm::expressions::Expression ExpressionParser::createPowerExpression(storm::expressions::Expression const& e1, storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e2) const {
@@ -203,7 +203,7 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
                 }
             }
-            return storm::expressions::Expression::createFalse();
+            return manager.boolean(false);
         }
                 
         storm::expressions::Expression ExpressionParser::createUnaryExpression(boost::optional<storm::expressions::OperatorType> const& operatorType, storm::expressions::Expression const& e1) const {
@@ -222,7 +222,7 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
                 }
             }
-            return storm::expressions::Expression::createFalse();
+            return manager.boolean(false);
         }
                 
         storm::expressions::Expression ExpressionParser::createDoubleLiteralExpression(double value, bool& pass) const {
@@ -232,17 +232,17 @@ namespace storm {
             }
             
             if (this->createExpressions) {
-                return storm::expressions::Expression::createDoubleLiteral(value);
+                return manager.rational(value);
             } else {
-                return storm::expressions::Expression::createFalse();
+                return manager.boolean(false);
             }
         }
         
         storm::expressions::Expression ExpressionParser::createIntegerLiteralExpression(int value) const {
             if (this->createExpressions) {
-                return storm::expressions::Expression::createIntegerLiteral(static_cast<int_fast64_t>(value));
+                return manager.integer(value);
             } else {
-                return storm::expressions::Expression::createFalse();
+                return manager.boolean(false);
             }
         }
         
@@ -258,7 +258,7 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
                 }
             }
-            return storm::expressions::Expression::createFalse();
+            return manager.boolean(false);
         }
 
         storm::expressions::Expression ExpressionParser::createFloorCeilExpression(storm::expressions::OperatorType const& operatorType, storm::expressions::Expression const& e1) const {
@@ -273,7 +273,7 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": " << e.what());
                 }
             }
-            return storm::expressions::Expression::createFalse();
+            return manager.boolean(false);
         }
         
         storm::expressions::Expression ExpressionParser::getIdentifierExpression(std::string const& identifier) const {
@@ -283,7 +283,7 @@ namespace storm {
                 STORM_LOG_THROW(expression != nullptr, storm::exceptions::WrongFormatException, "Parsing error in line " << get_line(qi::_3) << ": Undeclared identifier '" << identifier << "'.");
                 return *expression;
             } else {
-                return storm::expressions::Expression::createFalse();
+                return manager.boolean(false);
             }
         }
         
diff --git a/src/parser/ExpressionParser.h b/src/parser/ExpressionParser.h
index 80721dfb2..bff79fc14 100644
--- a/src/parser/ExpressionParser.h
+++ b/src/parser/ExpressionParser.h
@@ -19,16 +19,17 @@ namespace storm {
              * generate the actual expressions, a mapping of valid identifiers to their expressions need to be provided
              * later.
              *
+             * @param manager The manager responsible for the expressions.
              * @param invalidIdentifiers_ A symbol table of identifiers that are to be rejected.
              */
-            ExpressionParser(qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_);
+            ExpressionParser(storm::expressions::ExpressionManager& manager, qi::symbols<char, uint_fast64_t> const& invalidIdentifiers_);
             
             /*!
              * Sets an identifier mapping that is used to determine valid variables in the expression. The mapped-to
              * expressions will be substituted wherever the key value appears in the parsed expression. After setting
              * this, the parser will generate expressions.
              *
-             * @param identifiers A pointer to a mapping from identifiers to expressions.
+             * @param identifiers_ A pointer to a mapping from identifiers to expressions.
              */
             void setIdentifierMapping(qi::symbols<char, storm::expressions::Expression> const* identifiers_);
             
@@ -157,16 +158,19 @@ namespace storm {
             minMaxOperatorStruct minMaxOperator_;
 
             struct trueFalseOperatorStruct : qi::symbols<char, storm::expressions::Expression> {
-                trueFalseOperatorStruct() {
+                trueFalseOperatorStruct(storm::expressions::ExpressionManager& manager) {
                     add
-                    ("true", storm::expressions::Expression::createTrue())
-                    ("false", storm::expressions::Expression::createFalse());
+                    ("true", manager.boolean(true))
+                    ("false", manager.boolean(false));
                 }
             };
             
             // A parser used for recognizing the literals true and false.
             trueFalseOperatorStruct trueFalse_;
             
+            // The manager responsible for the expressions.
+            storm::expressions::ExpressionManager& manager;
+            
             // A flag that indicates whether expressions should actually be generated or just a syntax check shall be
             // performed.
             bool createExpressions;
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index b327b0984..4a34af248 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -61,7 +61,7 @@ namespace storm {
             return result;
         }
         
-        PrismParser::PrismParser(std::string const& filename, Iterator first) : PrismParser::base_type(start), secondRun(false), filename(filename), annotate(first), expressionParser(keywords_) {
+        PrismParser::PrismParser(std::string const& filename, Iterator first) : PrismParser::base_type(start), secondRun(false), filename(filename), annotate(first), manager(new storm::expressions::ExpressionManager()), expressionParser(*manager, keywords_) {
             // Parse simple identifier.
             identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_')) >> *(qi::alnum | qi::char_('_')))]]][qi::_pass = phoenix::bind(&PrismParser::isValidIdentifier, phoenix::ref(*this), qi::_1)];
             identifier.name("identifier");
@@ -96,7 +96,7 @@ namespace storm {
             formulaDefinition = (qi::lit("formula") > identifier > qi::lit("=") > expressionParser > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             formulaDefinition.name("formula definition");
             
-            booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > ((qi::lit("init") > expressionParser) | qi::attr(storm::expressions::Expression::createFalse())) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_2)];
+            booleanVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("bool")) > ((qi::lit("init") > expressionParser) | qi::attr(manager->boolean(false))) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createBooleanVariable, phoenix::ref(*this), qi::_1, qi::_2)];
             booleanVariableDefinition.name("boolean variable definition");
             
             integerVariableDefinition = ((identifier >> qi::lit(":") >> qi::lit("[")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), false)]) > expressionParser[qi::_a = qi::_1] > qi::lit("..") > expressionParser > qi::lit("]")[phoenix::bind(&PrismParser::allowDoubleLiterals, phoenix::ref(*this), true)] > -(qi::lit("init") > expressionParser[qi::_a = qi::_1]) > qi::lit(";"))[qi::_val = phoenix::bind(&PrismParser::createIntegerVariable, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_a)];
@@ -133,7 +133,7 @@ namespace storm {
             assignmentDefinitionList %= +assignmentDefinition % "&";
             assignmentDefinitionList.name("assignment list");
             
-            updateDefinition = (((expressionParser > qi::lit(":")) | qi::attr(storm::expressions::Expression::createDoubleLiteral(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];
+            updateDefinition = (((expressionParser > qi::lit(":")) | qi::attr(manager->rational(1))) >> assignmentDefinitionList)[qi::_val = phoenix::bind(&PrismParser::createUpdate, phoenix::ref(*this), qi::_1, qi::_2, qi::_r1)];
             updateDefinition.name("update");
             
             updateListDefinition %= +updateDefinition(qi::_r1) % "+";
@@ -224,50 +224,98 @@ namespace storm {
         
         storm::prism::Constant PrismParser::createUndefinedBooleanConstant(std::string const& newConstant) const {
             if (!this->secondRun) {
-                STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
-                this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanVariable(newConstant));
+                try {
+                    storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getBooleanType());
+                    this->identifiers_.add(newConstant, newVariable.getExpression());
+                } catch (storm::exceptions::InvalidArgumentException const& e) {
+                    if (manager->hasVariable(newConstant)) {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'.");
+                    }
+                }
             }
-            return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, this->getFilename());
+            return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename());
         }
         
         storm::prism::Constant PrismParser::createUndefinedIntegerConstant(std::string const& newConstant) const {
             if (!this->secondRun) {
-                STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
-                this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerVariable(newConstant));
+                try {
+                    storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getIntegerType());
+                    this->identifiers_.add(newConstant, newVariable.getExpression());
+                } catch (storm::exceptions::InvalidArgumentException const& e) {
+                    if (manager->hasVariable(newConstant)) {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'.");
+                    }
+                }
             }
-            return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, this->getFilename());
+            return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename());
         }
         
         storm::prism::Constant PrismParser::createUndefinedDoubleConstant(std::string const& newConstant) const {
             if (!this->secondRun) {
-                STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
-                this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleVariable(newConstant));
+                try {
+                    storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getRationalType());
+                    this->identifiers_.add(newConstant, newVariable.getExpression());
+                } catch (storm::exceptions::InvalidArgumentException const& e) {
+                    if (manager->hasVariable(newConstant)) {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'.");
+                    }
+                }
             }
-            return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, this->getFilename());
+            return storm::prism::Constant(manager->getVariable(newConstant), this->getFilename());
         }
         
         storm::prism::Constant PrismParser::createDefinedBooleanConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
             if (!this->secondRun) {
-                STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
-                this->identifiers_.add(newConstant, storm::expressions::Expression::createBooleanVariable(newConstant));
+                try {
+                    storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getBooleanType());
+                    this->identifiers_.add(newConstant, newVariable.getExpression());
+                } catch (storm::exceptions::InvalidArgumentException const& e) {
+                    if (manager->hasVariable(newConstant)) {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'.");
+                    }
+                }
             }
-            return storm::prism::Constant(storm::expressions::ExpressionReturnType::Bool, newConstant, expression, this->getFilename());
+            return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename());
         }
         
         storm::prism::Constant PrismParser::createDefinedIntegerConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
             if (!this->secondRun) {
-                STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
-                this->identifiers_.add(newConstant, storm::expressions::Expression::createIntegerVariable(newConstant));
+                try {
+                    storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getIntegerType());
+                    this->identifiers_.add(newConstant, newVariable.getExpression());
+                } catch (storm::exceptions::InvalidArgumentException const& e) {
+                    if (manager->hasVariable(newConstant)) {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'.");
+                    }
+                }
             }
-            return storm::prism::Constant(storm::expressions::ExpressionReturnType::Int, newConstant, expression, this->getFilename());
+            return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename());
         }
         
         storm::prism::Constant PrismParser::createDefinedDoubleConstant(std::string const& newConstant, storm::expressions::Expression expression) const {
             if (!this->secondRun) {
-                STORM_LOG_THROW(this->identifiers_.find(newConstant) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
-                this->identifiers_.add(newConstant, storm::expressions::Expression::createDoubleVariable(newConstant));
+                try {
+                    storm::expressions::Variable newVariable = manager->declareVariable(newConstant, manager->getIntegerType());
+                    this->identifiers_.add(newConstant, newVariable.getExpression());
+                } catch (storm::exceptions::InvalidArgumentException const& e) {
+                    if (manager->hasVariable(newConstant)) {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << newConstant << "'.");
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << newConstant << "'.");
+                    }
+                }
             }
-            return storm::prism::Constant(storm::expressions::ExpressionReturnType::Double, newConstant, expression, this->getFilename());
+            return storm::prism::Constant(manager->getVariable(newConstant), expression, this->getFilename());
         }
         
         storm::prism::Formula PrismParser::createFormula(std::string const& formulaName, storm::expressions::Expression expression) {
@@ -312,18 +360,34 @@ namespace storm {
         
         storm::prism::BooleanVariable PrismParser::createBooleanVariable(std::string const& variableName, storm::expressions::Expression initialValueExpression) const {
             if (!this->secondRun) {
-                STORM_LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
-                this->identifiers_.add(variableName, storm::expressions::Expression::createBooleanVariable(variableName));
+                try {
+                    storm::expressions::Variable newVariable = manager->declareVariable(variableName, manager->getBooleanType());
+                    this->identifiers_.add(variableName, newVariable.getExpression());
+                } catch (storm::exceptions::InvalidArgumentException const& e) {
+                    if (manager->hasVariable(variableName)) {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << variableName << "'.");
+                    }
+                }
             }
-            return storm::prism::BooleanVariable(variableName, initialValueExpression, this->getFilename());
+            return storm::prism::BooleanVariable(manager->getVariable(variableName), initialValueExpression, this->getFilename());
         }
         
         storm::prism::IntegerVariable PrismParser::createIntegerVariable(std::string const& variableName, storm::expressions::Expression lowerBoundExpression, storm::expressions::Expression upperBoundExpression, storm::expressions::Expression initialValueExpression) const {
             if (!this->secondRun) {
-                STORM_LOG_THROW(this->identifiers_.find(variableName) == nullptr, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
-                this->identifiers_.add(variableName, storm::expressions::Expression::createIntegerVariable(variableName));
+                try {
+                    storm::expressions::Variable newVariable = manager->declareVariable(variableName, manager->getIntegerType());
+                    this->identifiers_.add(variableName, newVariable.getExpression());
+                } catch (storm::exceptions::InvalidArgumentException const& e) {
+                    if (manager->hasVariable(variableName)) {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Duplicate identifier '" << variableName << "'.");
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": illegal identifier '" << variableName << "'.");
+                    }
+                }
             }
-            return storm::prism::IntegerVariable(variableName, lowerBoundExpression, upperBoundExpression, initialValueExpression, this->getFilename());
+            return storm::prism::IntegerVariable(manager->getVariable(variableName), lowerBoundExpression, upperBoundExpression, initialValueExpression, this->getFilename());
         }
         
         storm::prism::Module PrismParser::createModule(std::string const& moduleName, std::vector<storm::prism::BooleanVariable> const& booleanVariables, std::vector<storm::prism::IntegerVariable> const& integerVariables, std::vector<storm::prism::Command> const& commands, GlobalProgramInformation& globalProgramInformation) const {
@@ -342,12 +406,14 @@ namespace storm {
                 for (auto const& variable : moduleToRename.getBooleanVariables()) {
                     auto const& renamingPair = renaming.find(variable.getName());
                     STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed.");
-                    this->identifiers_.add(renamingPair->second, storm::expressions::Expression::createBooleanVariable(renamingPair->second));
+                    storm::expressions::Variable renamedVariable = manager->declareVariable(renamingPair->second, manager->getBooleanType());
+                    this->identifiers_.add(renamingPair->first, renamedVariable.getExpression());
                 }
                 for (auto const& variable : moduleToRename.getIntegerVariables()) {
                     auto const& renamingPair = renaming.find(variable.getName());
                     STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed.");
-                    this->identifiers_.add(renamingPair->second, storm::expressions::Expression::createIntegerVariable(renamingPair->second));
+                    storm::expressions::Variable renamedVariable = manager->declareVariable(renamingPair->second, manager->getBooleanType());
+                    this->identifiers_.add(renamingPair->first, renamedVariable.getExpression());
                 }
                 
                 // Return a dummy module in the first pass.
@@ -357,12 +423,12 @@ namespace storm {
                 globalProgramInformation.moduleToIndexMap[newModuleName] = globalProgramInformation.modules.size();
                 
                 // Create a mapping from identifiers to the expressions they need to be replaced with.
-                std::map<std::string, storm::expressions::Expression> expressionRenaming;
+                std::map<storm::expressions::Variable, storm::expressions::Expression> expressionRenaming;
                 for (auto const& namePair : renaming) {
                     storm::expressions::Expression const* substitutedExpression = this->identifiers_.find(namePair.second);
                     // If the mapped-to-value is an expression, we need to replace it.
                     if (substitutedExpression != nullptr) {
-                        expressionRenaming.emplace(namePair.first, *substitutedExpression);
+                        expressionRenaming.emplace(manager->getVariable(namePair.first), *substitutedExpression);
                     }
                 }
                 
@@ -372,7 +438,7 @@ namespace storm {
                     auto const& renamingPair = renaming.find(variable.getName());
                     STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Boolean variable '" << variable.getName() << " was not renamed.");
                     
-                    booleanVariables.push_back(storm::prism::BooleanVariable(renamingPair->second, variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)));
+                    booleanVariables.push_back(storm::prism::BooleanVariable(manager->getVariable(renamingPair->second), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)));
                 }
                 
                 // Rename the integer variables.
@@ -381,7 +447,7 @@ namespace storm {
                     auto const& renamingPair = renaming.find(variable.getName());
                     STORM_LOG_THROW(renamingPair != renaming.end(), storm::exceptions::WrongFormatException, "Parsing error in " << this->getFilename() << ", line " << get_line(qi::_3) << ": Integer variable '" << variable.getName() << " was not renamed.");
                     
-                    integerVariables.push_back(storm::prism::IntegerVariable(renamingPair->second, variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)));
+                    integerVariables.push_back(storm::prism::IntegerVariable(manager->getVariable(renamingPair->second), variable.getLowerBoundExpression().substitute(expressionRenaming), variable.getUpperBoundExpression().substitute(expressionRenaming), variable.getInitialValueExpression().substitute(expressionRenaming), this->getFilename(), get_line(qi::_1)));
                 }
                 
                 // Rename commands.
@@ -417,7 +483,7 @@ namespace storm {
         }
         
         storm::prism::Program PrismParser::createProgram(GlobalProgramInformation const& globalProgramInformation) const {
-            return storm::prism::Program(globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.rewardModels, this->secondRun && !globalProgramInformation.hasInitialConstruct, globalProgramInformation.initialConstruct, globalProgramInformation.labels, this->getFilename(), 1, this->secondRun);
+            return storm::prism::Program(manager, globalProgramInformation.modelType, globalProgramInformation.constants, globalProgramInformation.globalBooleanVariables, globalProgramInformation.globalIntegerVariables, globalProgramInformation.formulas, globalProgramInformation.modules, globalProgramInformation.rewardModels, this->secondRun && !globalProgramInformation.hasInitialConstruct, globalProgramInformation.initialConstruct, globalProgramInformation.labels, this->getFilename(), 1, this->secondRun);
         }
     } // namespace parser
 } // namespace storm
diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h
index 2f6b13251..38e31a568 100644
--- a/src/parser/PrismParser.h
+++ b/src/parser/PrismParser.h
@@ -9,6 +9,7 @@
 #include "src/parser/SpiritParserDefinitions.h"
 #include "src/parser/ExpressionParser.h"
 #include "src/storage/prism/Program.h"
+#include "src/storage/expressions/ExpressionManager.h"
 #include "src/storage/expressions/Expression.h"
 #include "src/storage/expressions/Expressions.h"
 #include "src/utility/macros.h"
@@ -20,7 +21,7 @@ namespace storm {
         class GlobalProgramInformation {
         public:
             // Default construct the header information.
-			GlobalProgramInformation() : modelType(), constants(), formulas(), globalBooleanVariables(), globalIntegerVariables(), moduleToIndexMap(), modules(), rewardModels(), labels(),hasInitialConstruct(false), initialConstruct(storm::expressions::Expression::createFalse()), currentCommandIndex(0), currentUpdateIndex(0) {
+            GlobalProgramInformation() : modelType(), constants(), formulas(), globalBooleanVariables(), globalIntegerVariables(), moduleToIndexMap(), modules(), rewardModels(), labels(), hasInitialConstruct(false), initialConstruct(), currentCommandIndex(0), currentUpdateIndex(0) {
                 // Intentionally left empty.
             }
             
@@ -212,7 +213,8 @@ namespace storm {
             storm::parser::PrismParser::modelTypeStruct modelType_;
             qi::symbols<char, storm::expressions::Expression> identifiers_;
             
-            // Parser used for recognizing expressions.
+            // Parser and manager used for recognizing expressions.
+            std::shared_ptr<storm::expressions::ExpressionManager> manager;
             storm::parser::ExpressionParser expressionParser;
             
             // Helper methods used in the grammar.
diff --git a/src/solver/Z3SmtSolver.cpp b/src/solver/Z3SmtSolver.cpp
index 6527ed348..0ee80e469 100644
--- a/src/solver/Z3SmtSolver.cpp
+++ b/src/solver/Z3SmtSolver.cpp
@@ -201,7 +201,7 @@ namespace storm {
 
 #ifdef STORM_HAVE_Z3
 		storm::expressions::SimpleValuation Z3SmtSolver::convertZ3ModelToValuation(z3::model const& model) {
-			storm::expressions::SimpleValuation stormModel(this->getManager());
+			storm::expressions::SimpleValuation stormModel(this->getManager().getSharedPointer());
 
 			for (unsigned i = 0; i < model.num_consts(); ++i) {
 				z3::func_decl variableI = model.get_const_decl(i);
@@ -252,7 +252,7 @@ namespace storm {
 				z3::model model = this->solver->get_model();
 
 				z3::expr modelExpr = this->context->bool_val(true);
-				storm::expressions::SimpleValuation valuation(this->getManager());
+				storm::expressions::SimpleValuation valuation(this->getManager().getSharedPointer());
 
 				for (storm::expressions::Variable const& importantAtom : important) {
 					z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom.getExpression());
@@ -294,7 +294,7 @@ namespace storm {
 				z3::model model = this->solver->get_model();
 
 				z3::expr modelExpr = this->context->bool_val(true);
-				storm::expressions::SimpleValuation valuation(this->getManager());
+				storm::expressions::SimpleValuation valuation(this->getManager().getSharedPointer());
 
 				for (storm::expressions::Variable const& importantAtom : important) {
 					z3::expr z3ImportantAtom = this->expressionAdapter->translateExpression(importantAtom.getExpression());
diff --git a/src/storage/dd/CuddDd.cpp b/src/storage/dd/CuddDd.cpp
index bbd886f9f..6e474bebf 100644
--- a/src/storage/dd/CuddDd.cpp
+++ b/src/storage/dd/CuddDd.cpp
@@ -303,10 +303,10 @@ namespace storm {
                 }
             }
             
-            std::set<std::string> unionOfMetaVariableNames;
-            std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), otherMatrix.getContainedMetaVariables().begin(), otherMatrix.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariableNames, unionOfMetaVariableNames.begin()));
-            std::set<std::string> containedMetaVariableNames;
-            std::set_difference(unionOfMetaVariableNames.begin(), unionOfMetaVariableNames.end(), summationMetaVariables.begin(), summationMetaVariables.end(), std::inserter(containedMetaVariableNames, containedMetaVariableNames.begin()));
+            std::set<storm::expressions::Variable> unionOfMetaVariables;
+            std::set_union(this->getContainedMetaVariables().begin(), this->getContainedMetaVariables().end(), otherMatrix.getContainedMetaVariables().begin(), otherMatrix.getContainedMetaVariables().end(), std::inserter(unionOfMetaVariables, unionOfMetaVariables.begin()));
+            std::set<storm::expressions::Variable> containedMetaVariables;
+            std::set_difference(unionOfMetaVariables.begin(), unionOfMetaVariables.end(), summationMetaVariables.begin(), summationMetaVariables.end(), std::inserter(containedMetaVariables, containedMetaVariables.begin()));
             
             return Dd<DdType::CUDD>(this->getDdManager(), this->cuddAdd.MatrixMultiply(otherMatrix.getCuddAdd(), summationDdVariables), containedMetaVariables);
         }
diff --git a/src/storage/expressions/Variable.cpp b/src/storage/expressions/Variable.cpp
index 492a6ae32..1608c8b56 100644
--- a/src/storage/expressions/Variable.cpp
+++ b/src/storage/expressions/Variable.cpp
@@ -11,6 +11,10 @@ namespace storm {
             return manager == other.manager && index == other.index;
         }
         
+        bool Variable::operator<(Variable const& other) const {
+            return this->getIndex() < other.getIndex();
+        }
+        
         storm::expressions::Expression Variable::getExpression() const {
             return storm::expressions::Expression(*this);
         }
diff --git a/src/storage/expressions/Variable.h b/src/storage/expressions/Variable.h
index 8bb7e0ce8..fd9796658 100644
--- a/src/storage/expressions/Variable.h
+++ b/src/storage/expressions/Variable.h
@@ -40,6 +40,14 @@ namespace storm {
              * @return True iff the two variables are the same.
              */
             bool operator==(Variable const& other) const;
+
+            /*!
+             * Checks whether the variable appears earlier in the total ordering of variables.
+             *
+             * @param other The variable to compare with.
+             * @return True iff the first variable appears earlier than the given one.
+             */
+            bool operator<(Variable const& other) const;
             
             /*!
              * Retrieves the name of the variable.
@@ -129,14 +137,6 @@ namespace std {
             return std::hash<uint_fast64_t>()(variable.getIndex());
         }
     };
-    
-    // Provide a less operator, so we can put variables in ordered collections.
-    template <>
-    struct less<storm::expressions::Variable> {
-        std::size_t operator()(storm::expressions::Variable const& variable1, storm::expressions::Variable const& variable2) const {
-            return variable1.getIndex() < variable2.getIndex();
-        }
-    };
 }
 
 #endif /* STORM_STORAGE_EXPRESSIONS_VARIABLE_H_ */
\ No newline at end of file
diff --git a/src/storage/prism/Module.cpp b/src/storage/prism/Module.cpp
index 327ffbcc3..2233ababa 100644
--- a/src/storage/prism/Module.cpp
+++ b/src/storage/prism/Module.cpp
@@ -146,7 +146,7 @@ namespace storm {
             return Module(this->getName(), this->getBooleanVariables(), this->getIntegerVariables(), newCommands);
         }
         
-        Module Module::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
+        Module Module::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
             std::vector<BooleanVariable> newBooleanVariables;
             newBooleanVariables.reserve(this->getNumberOfBooleanVariables());
             for (auto const& booleanVariable : this->getBooleanVariables()) {
diff --git a/src/storage/prism/Module.h b/src/storage/prism/Module.h
index 1031cbf27..9fe981340 100644
--- a/src/storage/prism/Module.h
+++ b/src/storage/prism/Module.h
@@ -189,12 +189,12 @@ namespace storm {
             Module restrictCommands(boost::container::flat_set<uint_fast64_t> const& indexSet) const;
             
             /*!
-             * Substitutes all identifiers in the module according to the given map.
+             * Substitutes all variables in the module according to the given map.
              *
              * @param substitution The substitution to perform.
              * @return The resulting module.
              */
-            Module substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const;
+            Module substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
             
             friend std::ostream& operator<<(std::ostream& stream, Module const& module);
 
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 203e25e75..a405d601b 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -255,7 +255,7 @@ namespace storm {
                     STORM_LOG_THROW(constantDefinitions.find(constant.getExpressionVariable()) == constantDefinitions.end(), storm::exceptions::InvalidArgumentException, "Illegally defining already defined constant '" << constant.getName() << "'.");
                     
                     // Now replace the occurrences of undefined constants in its defining expression.
-                    newConstants.emplace_back(constant.getType(), constant.getName(), constant.getExpression().substitute(constantDefinitions), constant.getFilename(), constant.getLineNumber());
+                    newConstants.emplace_back(constant.getExpressionVariable(), constant.getExpression().substitute(constantDefinitions), constant.getFilename(), constant.getLineNumber());
                 } else {
                     auto const& variableExpressionPair = constantDefinitions.find(constant.getExpressionVariable());
                     
@@ -344,9 +344,6 @@ namespace storm {
         }
         
         void Program::checkValidity() const {
-            // We need to construct a mapping from identifiers to their types, so we can type-check the expressions later.
-            std::map<std::string, storm::expressions::ExpressionReturnType> identifierToTypeMap;
-            
             // Start by checking the constant declarations.
             std::set<std::string> allIdentifiers;
             std::set<std::string> globalIdentifiers;
@@ -362,9 +359,6 @@ namespace storm {
                     STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << constant.getFilename() << ", line " << constant.getLineNumber() << ": defining expression refers to unknown identifiers.");
                 }
                 
-                // Finally, register the type of the constant for later type checks.
-                identifierToTypeMap.emplace(constant.getName(), constant.getType());
-                
                 // Record the new identifier for future checks.
                 constantNames.insert(constant.getName());
                 allIdentifiers.insert(constant.getName());
@@ -382,9 +376,6 @@ namespace storm {
                 bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
 
-                // Register the type of the constant for later type checks.
-                identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Bool);
-                
                 // Record the new identifier for future checks.
                 variableNames.insert(variable.getName());
                 allIdentifiers.insert(variable.getName());
@@ -408,9 +399,6 @@ namespace storm {
                 isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                 STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
                 
-                // Register the type of the constant for later type checks.
-                identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Int);
-
                 // Record the new identifier for future checks.
                 variableNames.insert(variable.getName());
                 allIdentifiers.insert(variable.getName());
@@ -428,9 +416,6 @@ namespace storm {
                     bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
                     STORM_LOG_THROW(isValid, storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": initial value expression refers to unknown constants.");
                     
-                    // Register the type of the constant for later type checks.
-                    identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Bool);
-                    
                     // Record the new identifier for future checks.
                     variableNames.insert(variable.getName());
                     allIdentifiers.insert(variable.getName());
@@ -439,9 +424,6 @@ namespace storm {
                     // Check for duplicate identifiers.
                     STORM_LOG_THROW(allIdentifiers.find(variable.getName()) == allIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << variable.getFilename() << ", line " << variable.getLineNumber() << ": duplicate identifier '" << variable.getName() << "'.");
                     
-                    // Register the type of the constant for later type checks.
-                    identifierToTypeMap.emplace(variable.getName(), storm::expressions::ExpressionReturnType::Int);
-                    
                     // Check that bound expressions of the range.
                     std::set<std::string> containedIdentifiers = variable.getLowerBoundExpression().getVariables();
                     bool isValid = std::includes(constantNames.begin(), constantNames.end(), containedIdentifiers.begin(), containedIdentifiers.end());
@@ -500,8 +482,7 @@ namespace storm {
                                 }
                             }
                             STORM_LOG_THROW(alreadyAssignedIdentifiers.find(assignment.getVariableName()) == alreadyAssignedIdentifiers.end(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": duplicate assignment to variable '" << assignment.getVariableName() << "'.");
-                            auto variableTypePair = identifierToTypeMap.find(assignment.getVariableName());
-                            STORM_LOG_THROW(variableTypePair->second == assignment.getExpression().getReturnType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getReturnType() << "' to variable '" << variableTypePair->first << "' of type '" << variableTypePair->second << "'.");
+                            STORM_LOG_THROW(manager->getVariable(assignment.getVariableName()).getType() == assignment.getExpression().getType(), storm::exceptions::WrongFormatException, "Error in " << command.getFilename() << ", line " << command.getLineNumber() << ": illegally assigning a value of type '" << assignment.getExpression().getType() << "' to variable '" << assignment.getVariableName() << "' of type '" << manager->getVariable(assignment.getVariableName()).getType() << "'.");
                             
                             containedIdentifiers = assignment.getExpression().getVariables();
                             isValid = std::includes(variablesAndConstants.begin(), variablesAndConstants.end(), containedIdentifiers.begin(), containedIdentifiers.end());
@@ -572,11 +553,11 @@ namespace storm {
         }
         
         storm::expressions::ExpressionManager const& Program::getManager() const {
-            return this->manager;
+            return *this->manager;
         }
 
         storm::expressions::ExpressionManager& Program::getManager() {
-            return this->manager;
+            return *this->manager;
         }
 
         std::ostream& operator<<(std::ostream& stream, Program const& program) {
diff --git a/src/storage/prism/RewardModel.cpp b/src/storage/prism/RewardModel.cpp
index 7f9b8107a..2c1b49ae7 100644
--- a/src/storage/prism/RewardModel.cpp
+++ b/src/storage/prism/RewardModel.cpp
@@ -30,7 +30,7 @@ namespace storm {
             return this->transitionRewards;
         }
         
-        RewardModel RewardModel::substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const {
+        RewardModel RewardModel::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
             std::vector<StateReward> newStateRewards;
             newStateRewards.reserve(this->getStateRewards().size());
             for (auto const& stateReward : this->getStateRewards()) {
diff --git a/src/storage/prism/RewardModel.h b/src/storage/prism/RewardModel.h
index 62841ef5e..2a2b0ab97 100644
--- a/src/storage/prism/RewardModel.h
+++ b/src/storage/prism/RewardModel.h
@@ -76,12 +76,12 @@ namespace storm {
             std::vector<storm::prism::TransitionReward> const& getTransitionRewards() const;
             
             /*!
-             * Substitutes all identifiers in the reward model according to the given map.
+             * Substitutes all variables in the reward model according to the given map.
              *
              * @param substitution The substitution to perform.
              * @return The resulting reward model.
              */
-            RewardModel substitute(std::map<std::string, storm::expressions::Expression> const& substitution) const;
+            RewardModel substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
             
             friend std::ostream& operator<<(std::ostream& stream, RewardModel const& rewardModel);