diff --git a/src/adapters/CarlAdapter.h b/src/adapters/CarlAdapter.h
index fb0a45749..b5a91248d 100644
--- a/src/adapters/CarlAdapter.h
+++ b/src/adapters/CarlAdapter.h
@@ -57,7 +57,7 @@ namespace storm {
 #else
     typedef mpq_class RationalNumber;
 #endif
-    typedef carl::Variable Variable;
+    typedef carl::Variable RationalFunctionVariable;
     typedef carl::MultivariatePolynomial<RationalNumber> RawPolynomial;
     typedef carl::FactorizedPolynomial<RawPolynomial> Polynomial;
     typedef carl::Relation CompareRelation;
diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp
index 5de59feb0..1173fc5d2 100644
--- a/src/generator/PrismNextStateGenerator.cpp
+++ b/src/generator/PrismNextStateGenerator.cpp
@@ -395,7 +395,7 @@ namespace storm {
                         if (rewardModel.get().hasStateActionRewards()) {
                             for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
                                 if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
-                                    stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass();
+                                    stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression()));
                                 }
                             }
                         }
diff --git a/src/modelchecker/results/CheckResult.cpp b/src/modelchecker/results/CheckResult.cpp
index 40ca4badb..324fdd089 100644
--- a/src/modelchecker/results/CheckResult.cpp
+++ b/src/modelchecker/results/CheckResult.cpp
@@ -145,9 +145,10 @@ namespace storm {
         template HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>& CheckResult::asHybridQuantitativeCheckResult();
         template HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double> const& CheckResult::asHybridQuantitativeCheckResult() const;
 
-#ifdef STORM_HAVE_CARL
+        template ExplicitQuantitativeCheckResult<storm::RationalNumber>& CheckResult::asExplicitQuantitativeCheckResult();
+        template ExplicitQuantitativeCheckResult<storm::RationalNumber> const& CheckResult::asExplicitQuantitativeCheckResult() const;
+
         template ExplicitQuantitativeCheckResult<storm::RationalFunction>& CheckResult::asExplicitQuantitativeCheckResult();
         template ExplicitQuantitativeCheckResult<storm::RationalFunction> const& CheckResult::asExplicitQuantitativeCheckResult() const;
-#endif
     }
 }
\ No newline at end of file
diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp
index 83d0c8aa2..8ea0710dc 100644
--- a/src/models/sparse/Model.cpp
+++ b/src/models/sparse/Model.cpp
@@ -346,9 +346,7 @@ namespace storm {
                 return this->rewardModels;
             }
             
-            
-
-            std::set<storm::Variable> getProbabilityParameters(Model<storm::RationalFunction> const& model) {
+            std::set<storm::RationalFunctionVariable> getProbabilityParameters(Model<storm::RationalFunction> const& model) {
                 return storm::storage::getVariables(model.getTransitionMatrix());
             }
             
diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h
index bd4c9921b..a4422a8be 100644
--- a/src/models/sparse/Model.h
+++ b/src/models/sparse/Model.h
@@ -357,7 +357,7 @@ namespace storm {
                 boost::optional<std::vector<LabelSet>> choiceLabeling;
             };
             
-            std::set<storm::Variable> getProbabilityParameters(Model<storm::RationalFunction> const& model);
+            std::set<storm::RationalFunctionVariable> getProbabilityParameters(Model<storm::RationalFunction> const& model);
         } // namespace sparse
     } // namespace models
 } // namespace storm
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index c84b03cef..e4e81e4c5 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -1417,9 +1417,9 @@ namespace storm {
         
         
 #ifdef STORM_HAVE_CARL
-        std::set<storm::Variable> getVariables(SparseMatrix<storm::RationalFunction> const& matrix)
+        std::set<storm::RationalFunctionVariable> getVariables(SparseMatrix<storm::RationalFunction> const& matrix)
         {
-            std::set<storm::Variable> result;
+            std::set<storm::RationalFunctionVariable> result;
             for(auto const& entry : matrix) {
                 entry.getValue().gatherVariables(result);
             }
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index 374859af5..95d209b07 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -1004,7 +1004,7 @@ namespace storm {
         };
         
 #ifdef STORM_HAVE_CARL
-        std::set<storm::Variable> getVariables(SparseMatrix<storm::RationalFunction> const& matrix);
+        std::set<storm::RationalFunctionVariable> getVariables(SparseMatrix<storm::RationalFunction> const& matrix);
 #endif
         
     } // namespace storage
diff --git a/src/utility/export.h b/src/utility/export.h
index 4d172bcdc..8ae336c32 100644
--- a/src/utility/export.h
+++ b/src/utility/export.h
@@ -24,8 +24,8 @@ void exportParametricMcResult(const ValueType& mcresult, storm::modelchecker::re
 	filestream.open(path);
 	// todo add checks.
 	filestream << "!Parameters: ";
-	std::set<storm::Variable> vars = mcresult.gatherVariables();
-	std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::Variable>(filestream, ", "));
+	std::set<storm::RationalFunctionVariable> vars = mcresult.gatherVariables();
+	std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::RationalFunctionVariable>(filestream, ", "));
 	filestream << std::endl;
 	filestream << "!Result: " << mcresult << std::endl;
 	filestream << "!Well-formed Constraints: " << std::endl;
diff --git a/src/utility/parametric.h b/src/utility/parametric.h
index 2ebf1e18c..244e1c141 100644
--- a/src/utility/parametric.h
+++ b/src/utility/parametric.h
@@ -28,7 +28,7 @@ namespace storm {
             
 #ifdef STORM_HAVE_CARL
             template<>
-            struct VariableType<storm::RationalFunction> { typedef storm::Variable type; };
+            struct VariableType<storm::RationalFunction> { typedef storm::RationalFunctionVariable type; };
             template<>
             struct CoefficientType<storm::RationalFunction> { typedef storm::RationalNumber type; };
 #endif
diff --git a/src/utility/solver.cpp b/src/utility/solver.cpp
index 43fadb20b..237d22b48 100644
--- a/src/utility/solver.cpp
+++ b/src/utility/solver.cpp
@@ -229,6 +229,9 @@ namespace storm {
             template class GameSolverFactory<double>;
 
             template class LinearEquationSolverFactory<storm::RationalNumber>;
+            template class EigenLinearEquationSolverFactory<storm::RationalNumber>;
+
+            template class LinearEquationSolverFactory<storm::RationalFunction>;
             template class EigenLinearEquationSolverFactory<storm::RationalFunction>;
         }
     }
diff --git a/src/utility/storm.h b/src/utility/storm.h
index d590aa033..e6f7a277c 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -344,8 +344,8 @@ namespace storm {
         filestream.open(path);
         // TODO: add checks.
         filestream << "!Parameters: ";
-        std::set<storm::Variable> vars = result.gatherVariables();
-        std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::Variable>(filestream, "; "));
+        std::set<storm::RationalFunctionVariable> vars = result.gatherVariables();
+        std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::RationalFunctionVariable>(filestream, "; "));
         filestream << std::endl;
         filestream << "!Result: " << result << std::endl;
         filestream << "!Well-formed Constraints: " << std::endl;
diff --git a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
index 8462fa8e6..113d0b1ba 100644
--- a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
@@ -61,55 +61,58 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die) {
 }
 
 TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalNumber) {
-    // FIXME: this should use rational numbers not functions.
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
-    std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program).build();
+    
+    storm::generator::NextStateGeneratorOptions options;
+    options.setBuildAllLabels().setBuildAllRewardModels();
+    std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> model = storm::builder::ExplicitModelBuilder<storm::RationalNumber>(program, options).build();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
     
     ASSERT_EQ(model->getType(), storm::models::ModelType::Dtmc);
     
-    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
+    std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalNumber>> dtmc = model->as<storm::models::sparse::Dtmc<storm::RationalNumber>>();
     
     ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
     ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
     
-    storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> checker(*dtmc, std::make_unique<storm::utility::solver::EigenLinearEquationSolverFactory<storm::RationalFunction>>());
+    storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalNumber>> checker(*dtmc, std::make_unique<storm::utility::solver::EigenLinearEquationSolverFactory<storm::RationalNumber>>());
     
     std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
     
     std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
-    storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
+    storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalNumber>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<storm::RationalNumber>();
     
-    EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult1[0]);
+    EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult1[0]);
     
     formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
     
     result = checker.check(*formula);
-    storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
+    storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalNumber>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<storm::RationalNumber>();
     
-    EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult2[0]);
+    EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult2[0]);
     
     formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
     
     result = checker.check(*formula);
-    storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
+    storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalNumber>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<storm::RationalNumber>();
     
-    EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult3[0]);
+    EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult3[0]);
     
     formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
     
     result = checker.check(*formula);
-    storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
+    storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalNumber>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<storm::RationalNumber>();
     
-    EXPECT_EQ(storm::RationalFunction(11) / storm::RationalFunction(3), quantitativeResult4[0]);
+    EXPECT_EQ(storm::RationalNumber(11) / storm::RationalNumber(3), quantitativeResult4[0]);
 }
 
 TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) {
-    // FIXME: this should use rational numbers not functions.
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/parametric_die.pm");
-    std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program).build();
+    storm::generator::NextStateGeneratorOptions options;
+    options.setBuildAllLabels().setBuildAllRewardModels();
+    std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model = storm::builder::ExplicitModelBuilder<storm::RationalFunction>(program, options).build();
     
     // A parser that we use for conveniently constructing the formulas.
     storm::parser::FormulaParser formulaParser;
@@ -121,6 +124,11 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) {
     ASSERT_EQ(dtmc->getNumberOfStates(), 13ull);
     ASSERT_EQ(dtmc->getNumberOfTransitions(), 20ull);
     
+    std::map<storm::RationalFunctionVariable, storm::RationalNumber> instantiation;
+    std::set<storm::RationalFunctionVariable> variables = storm::models::sparse::getProbabilityParameters(*dtmc);
+    ASSERT_EQ(variables.size(), 1ull);
+    instantiation.emplace(*variables.begin(), storm::RationalNumber(1) / storm::RationalNumber(2));
+    
     storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> checker(*dtmc, std::make_unique<storm::utility::solver::EigenLinearEquationSolverFactory<storm::RationalFunction>>());
     
     std::shared_ptr<storm::logic::Formula const> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"one\"]");
@@ -128,29 +136,28 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) {
     std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
     
-    std::cout << quantitativeResult1 << std::endl;
-//    EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult1[0]);
-//    
-//    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
-//    
-//    result = checker.check(*formula);
-//    storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
-//    
-//    EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult2[0]);
-//    
-//    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
-//    
-//    result = checker.check(*formula);
-//    storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
-//    
-//    EXPECT_EQ(storm::RationalFunction(1) / storm::RationalFunction(6), quantitativeResult3[0]);
-//    
-//    formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
-//    
-//    result = checker.check(*formula);
-//    storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
-//    
-//    EXPECT_EQ(storm::RationalFunction(11) / storm::RationalFunction(3), quantitativeResult4[0]);
+    EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult1[0].evaluate(instantiation));
+    
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"two\"]");
+    
+    result = checker.check(*formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
+    
+    EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult2[0].evaluate(instantiation));
+    
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"three\"]");
+    
+    result = checker.check(*formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
+    
+    EXPECT_EQ(storm::RationalNumber(1) / storm::RationalNumber(6), quantitativeResult3[0].evaluate(instantiation));
+    
+    formula = formulaParser.parseSingleFormulaFromString("R=? [F \"done\"]");
+    
+    result = checker.check(*formula);
+    storm::modelchecker::ExplicitQuantitativeCheckResult<storm::RationalFunction>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<storm::RationalFunction>();
+    
+    EXPECT_EQ(storm::RationalNumber(11) / storm::RationalNumber(3), quantitativeResult4[0].evaluate(instantiation));
 }
 
 
@@ -377,8 +384,10 @@ TEST(EigenDtmcPrctlModelCheckerTest, LRA) {
 
 TEST(EigenDtmcPrctlModelCheckerTest, Conditional) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/modelchecker/test_conditional.pm");
-    
-    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program).build();
+
+    storm::generator::NextStateGeneratorOptions options;
+    options.setBuildAllLabels().setBuildAllRewardModels();
+    std::shared_ptr<storm::models::sparse::Model<double>> model = storm::builder::ExplicitModelBuilder<double>(program, options).build();
     ASSERT_TRUE(model->getType() == storm::models::ModelType::Dtmc);
     ASSERT_EQ(4ul, model->getNumberOfStates());
     ASSERT_EQ(5ul, model->getNumberOfTransitions());
diff --git a/test/functional/utility/ModelInstantiatorTest.cpp b/test/functional/utility/ModelInstantiatorTest.cpp
index c7a9c0e31..2dd74c66a 100644
--- a/test/functional/utility/ModelInstantiatorTest.cpp
+++ b/test/functional/utility/ModelInstantiatorTest.cpp
@@ -36,10 +36,10 @@ TEST(ModelInstantiatorTest, BrpProb) {
     EXPECT_FALSE(dtmc->hasRewardModel());
     
     {
-        std::map<storm::Variable, storm::RationalNumber> valuation;
-        storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
+        std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
+        storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
         ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
-        storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
+        storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
         ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
         valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(0.8)));
         valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.9)));
@@ -69,10 +69,10 @@ TEST(ModelInstantiatorTest, BrpProb) {
     }
     
     {
-        std::map<storm::Variable, storm::RationalNumber> valuation;
-        storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
+        std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
+        storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
         ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
-        storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
+        storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
         ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
         valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1.0)));
         valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(1.0)));
@@ -102,10 +102,10 @@ TEST(ModelInstantiatorTest, BrpProb) {
     }
     
     {
-        std::map<storm::Variable, storm::RationalNumber> valuation;
-        storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
+        std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
+        storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
         ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
-        storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
+        storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
         ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
         valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1.0)));
         valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.9)));
@@ -153,14 +153,14 @@ TEST(ModelInstantiatorTest, Brp_Rew) {
     storm::utility::ModelInstantiator<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::models::sparse::Dtmc<double>> modelInstantiator(*dtmc);
     
     {
-        std::map<storm::Variable, storm::RationalNumber> valuation;
-        storm::Variable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
+        std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
+        storm::RationalFunctionVariable const& pL = carl::VariablePool::getInstance().findVariableWithName("pL");
         ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
-        storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
+        storm::RationalFunctionVariable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
         ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
-        storm::Variable const& TOMsg = carl::VariablePool::getInstance().findVariableWithName("TOMsg");
+        storm::RationalFunctionVariable const& TOMsg = carl::VariablePool::getInstance().findVariableWithName("TOMsg");
         ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
-        storm::Variable const& TOAck = carl::VariablePool::getInstance().findVariableWithName("TOAck");
+        storm::RationalFunctionVariable const& TOAck = carl::VariablePool::getInstance().findVariableWithName("TOAck");
         ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
         valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(0.9)));
         valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.3)));
@@ -222,10 +222,10 @@ TEST(ModelInstantiatorTest, Consensus) {
 
     storm::utility::ModelInstantiator<storm::models::sparse::Mdp<storm::RationalFunction>, storm::models::sparse::Mdp<double>> modelInstantiator(*mdp);
     
-    std::map<storm::Variable, storm::RationalNumber> valuation;
-    storm::Variable const& p1 = carl::VariablePool::getInstance().findVariableWithName("p1");
+    std::map<storm::RationalFunctionVariable, storm::RationalNumber> valuation;
+    storm::RationalFunctionVariable const& p1 = carl::VariablePool::getInstance().findVariableWithName("p1");
     ASSERT_NE(p1, carl::Variable::NO_VARIABLE);
-    storm::Variable const& p2 = carl::VariablePool::getInstance().findVariableWithName("p2");
+    storm::RationalFunctionVariable const& p2 = carl::VariablePool::getInstance().findVariableWithName("p2");
     ASSERT_NE(p2, carl::Variable::NO_VARIABLE);
     valuation.insert(std::make_pair(p1,carl::rationalize<storm::RationalNumber>(0.51)));
     valuation.insert(std::make_pair(p2,carl::rationalize<storm::RationalNumber>(0.49)));