diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index 115fbccdd..2b73ba22f 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -232,11 +232,13 @@ if(USE_CARL)
         )
 
         add_dependencies(resources carl)
-        include_directories(${STORM_3RDPARTY_BINARY_DIR}/carl/include)
+        set(carl_INCLUDE_DIR "${STORM_3RDPARTY_BINARY_DIR}/carl/include")
+        include_directories("${carl_INCLUDE_DIR}")
         list(APPEND STORM_LINK_LIBRARIES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT})
         set(STORM_HAVE_CARL ON)
     endif()
 endif()
+set(STORM_CARL_INCLUDE_DIR "${carl_INCLUDE_DIR}")
 
 #############################################################
 ##
diff --git a/src/adapters/CarlAdapter.h b/src/adapters/CarlAdapter.h
index 05656aea7..05e9e7a52 100644
--- a/src/adapters/CarlAdapter.h
+++ b/src/adapters/CarlAdapter.h
@@ -4,8 +4,6 @@
 // Include config to know whether CARL is available or not.
 #include "storm-config.h"
 
-#include <boost/multiprecision/gmp.hpp>
-
 #ifdef STORM_HAVE_CARL
 
 #include <carl/numbers/numbers.h>
diff --git a/src/adapters/NumberAdapter.h b/src/adapters/NumberAdapter.h
index 73d567353..f300da9c7 100644
--- a/src/adapters/NumberAdapter.h
+++ b/src/adapters/NumberAdapter.h
@@ -2,8 +2,6 @@
 
 #include "storm-config.h"
 
-#include <boost/multiprecision/gmp.hpp>
-
 #ifdef STORM_HAVE_CARL
 
 #include <carl/numbers/numbers.h>
@@ -14,4 +12,4 @@ namespace storm {
     typedef mpq_class RationalNumber;
 #endif
 }
-#endif
\ No newline at end of file
+#endif
diff --git a/src/builder/jit/Choice.cpp b/src/builder/jit/Choice.cpp
index 4b101cb0b..12c81eb8c 100644
--- a/src/builder/jit/Choice.cpp
+++ b/src/builder/jit/Choice.cpp
@@ -2,6 +2,8 @@
 
 #include "src/adapters/CarlAdapter.h"
 
+#include "src/utility/constants.h"
+
 namespace storm {
     namespace builder {
         namespace jit {
@@ -72,8 +74,8 @@ namespace storm {
             }
         
             template <typename IndexType, typename ValueType>
-            void Choice<IndexType, ValueType>::resizeRewards(std::size_t numberOfRewards, ValueType const& fillValue) {
-                rewards.resize(numberOfRewards, fillValue);
+            void Choice<IndexType, ValueType>::resizeRewards(std::size_t numberOfRewards) {
+                rewards.resize(numberOfRewards, storm::utility::zero<ValueType>());
             }
             
             template <typename IndexType, typename ValueType>
diff --git a/src/builder/jit/Choice.h b/src/builder/jit/Choice.h
index 3bcc5b01d..d7600d141 100644
--- a/src/builder/jit/Choice.h
+++ b/src/builder/jit/Choice.h
@@ -59,9 +59,9 @@ namespace storm {
                 void setRewards(std::vector<ValueType>&& rewards);
                 
                 /*!
-                 * Resizes the rewards to the desired size and filles newly created values with the provided value.
+                 * Resizes the rewards to the desired size and filles newly created values the zero value of the value type.
                  */
-                void resizeRewards(std::size_t numberOfRewards, ValueType const& fillValue);
+                void resizeRewards(std::size_t numberOfRewards);
                 
                 /*!
                  * Retrieves the number of rewards of this choice.
diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp
index 353879fdb..19bf14d90 100644
--- a/src/builder/jit/ExplicitJitJaniModelBuilder.cpp
+++ b/src/builder/jit/ExplicitJitJaniModelBuilder.cpp
@@ -4,8 +4,6 @@
 #include <cstdio>
 #include <chrono>
 
-#include "src/adapters/CarlAdapter.h"
-
 #include "src/solver/SmtSolver.h"
 #include "src/storage/jani/AutomatonComposition.h"
 #include "src/storage/jani/ParallelComposition.h"
@@ -74,6 +72,11 @@ namespace storm {
                 } else {
                     stormRoot = STORM_CPP_BASE_PATH;
                 }
+                if (settings.isCarlIncludeDirectorySet()) {
+                    carlIncludeDir = settings.getCarlIncludeDirectory();
+                } else {
+                    carlIncludeDir = STORM_CARL_INCLUDE_DIR;
+                }
                 
                 // Register all transient variables as transient.
                 for (auto const& variable : this->model.getGlobalVariables().getTransientVariables()) {
@@ -125,7 +128,7 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The input model contains undefined constants that influence the graph structure of the underlying model, which is not allowed.");
                 }
 #endif
-      
+                    
                 // Comment this in to print the JANI model for debugging purposes. 
                 // this->model.makeStandardJaniCompliant();
                 // storm::jani::JsonExporter::toStream(this->model, std::vector<std::shared_ptr<storm::logic::Formula const>>(), std::cout, false);
@@ -347,7 +350,41 @@ namespace storm {
                 }
                 return result;
             }
-                
+
+            template <typename ValueType, typename RewardModelType>
+            bool ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::checkCarlAvailable() const {
+                bool result = true;
+                std::string problem = "Unable to compile program using Carl data structures. Is Carls's include directory '" + carlIncludeDir + "' set correctly?";
+                try {
+                    std::string program = R"(
+#include "src/adapters/NumberAdapter.h"
+                        
+                    int main() {
+                        return 0;
+                    }
+                    )";
+                    boost::filesystem::path temporaryFile = writeToTemporaryFile(program);
+                    std::string temporaryFilename = boost::filesystem::absolute(temporaryFile).string();
+                    boost::filesystem::path outputFile = temporaryFile;
+                    outputFile += ".out";
+                    std::string outputFilename = boost::filesystem::absolute(outputFile).string();
+                    // FIXME: get right of build_xcode
+                    boost::optional<std::string> error = execute(compiler + " " + compilerFlags + " " + temporaryFilename + " -I" + stormRoot + " -I" + stormRoot + "/build_xcode/include -I" + carlIncludeDir + " -o " + outputFilename);
+                    
+                    if (error) {
+                        result = false;
+                        STORM_LOG_ERROR(problem);
+                        STORM_LOG_TRACE(error.get());
+                    } else {
+                        boost::filesystem::remove(outputFile);
+                    }
+                } catch(std::exception const& e) {
+                    result = false;
+                    STORM_LOG_ERROR(problem);
+                }
+                return result;
+            }
+
             template <typename ValueType, typename RewardModelType>
             bool ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::doctor() const {
                 bool result = true;
@@ -389,9 +426,20 @@ namespace storm {
                 
                 STORM_LOG_DEBUG("Checking whether Storm's headers are available.");
                 result = checkStormAvailable();
-                if (result) {
+                if (!result) {
+                    return result;
+                }
+                STORM_LOG_DEBUG("Success.");
+
+                if (std::is_same<storm::RationalNumber, ValueType>::value) {
+                    STORM_LOG_DEBUG("Checking whether Carl's headers are available.");
+                    result = checkCarlAvailable();
+                    if (!result) {
+                        return result;
+                    }
                     STORM_LOG_DEBUG("Success.");
                 }
+                
                 return result;
             }
             
@@ -428,6 +476,8 @@ namespace storm {
                 std::shared_ptr<storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>> sparseModel(nullptr);
                 try {
                     sparseModel = std::shared_ptr<storm::models::sparse::Model<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>>(builder->build());
+                    STORM_LOG_THROW(sparseModel, storm::exceptions::UnexpectedException, "An unexpected error occurred.");
+                    STORM_LOG_TRACE("Successfully got model from jit-builder.");
                 } catch (std::exception const& e) {
                     STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Model building failed. Reason: " << e.what());
                 }
@@ -448,13 +498,33 @@ namespace storm {
                 modelData["deterministic_model"] = asString(model.isDeterministicModel());
                 modelData["discrete_time_model"] = asString(model.isDiscreteTimeModel());
                 
-                // Use a list here to enable if query in skeleton program.
+                // Use lists here to enable if query in skeleton program even if the property is just boolean.
                 cpptempl::data_list list;
                 if (options.isExplorationChecksSet()) {
                     list.push_back(cpptempl::data_map());
                 }
                 modelData["exploration_checks"] = cpptempl::make_data(list);
+                list = cpptempl::data_list();
+                if (std::is_same<storm::RationalNumber, ValueType>::value) {
+                    list.push_back(cpptempl::data_map());
+                }
+                modelData["exact"] = cpptempl::make_data(list);
+                list = cpptempl::data_list();
+                if (std::is_same<storm::RationalFunction, ValueType>::value) {
+                    list.push_back(cpptempl::data_map());
+                }
+                modelData["parametric"] = cpptempl::make_data(list);
+                list = cpptempl::data_list();
+                if (std::is_same<double, ValueType>::value) {
+                    list.push_back(cpptempl::data_map());
+                }
+                modelData["double"] = cpptempl::make_data(list);
 
+                // If we are building a possibly parametric model, we need to create the parameters.
+                if (std::is_same<storm::RationalFunction, ValueType>::value) {
+                    generateParameters(modelData);
+                }
+                
                 // Generate non-trivial model-information.
                 generateVariables(modelData);
                 generateInitialStates(modelData);
@@ -517,8 +587,15 @@ namespace storm {
                 cpptempl::data_map result;
                 
                 result["name"] = registerVariable(variable.getExpressionVariable(), variable.isTransient());
+                realVariables.insert(variable.getExpressionVariable());
                 if (variable.hasInitExpression()) {
-                    result["init"] = asString(variable.getInitExpression().evaluateAsDouble());
+                    if (std::is_same<double, ValueType>::value) {
+                        result["init"] = expressionTranslator.translate(variable.getInitExpression(), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble));
+                    } else if (std::is_same<storm::RationalNumber, ValueType>::value) {
+                        result["init"] = expressionTranslator.translate(variable.getInitExpression(), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalNumber));
+                    } else if (std::is_same<storm::RationalFunction, ValueType>::value) {
+                        result["init"] = expressionTranslator.translate(variable.getInitExpression(), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalFunction));
+                    }
                 }
                 
                 return result;
@@ -1032,7 +1109,7 @@ namespace storm {
                         indent(vectorSource, indentLevel + 2) << "Choice<IndexType, ValueType>& choice = behaviour.addChoice();" << std::endl;
                         
                         std::stringstream tmp;
-                        indent(tmp, indentLevel + 2) << "choice.resizeRewards({$edge_destination_rewards_count}, 0);" << std::endl;
+                        indent(tmp, indentLevel + 2) << "choice.resizeRewards({$edge_destination_rewards_count});" << std::endl;
                         indent(tmp, indentLevel + 2) << "{% for reward in edge_rewards %}choice.addReward({$reward.index}, transientOut.{$reward.variable});" << std::endl;
                         indent(tmp, indentLevel + 2) << "{% endfor %}" << std::endl;
                         
@@ -1247,10 +1324,13 @@ namespace storm {
                 cpptempl::data_list levels = generateLevels(destination.getOrderedAssignments());
                 destinationData["name"] = asString(destinationIndex);
                 destinationData["levels"] = cpptempl::make_data(levels);
-                if (rate) {
-                    destinationData["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(rate.get() * destination.getProbability()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, "double"));
-                } else {
-                    destinationData["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(destination.getProbability()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, "double"));
+                storm::expressions::Expression expressionToTranslate = rate ? shiftVariablesWrtLowerBound(rate.get() * destination.getProbability()) : shiftVariablesWrtLowerBound(destination.getProbability());
+                if (std::is_same<double, ValueType>::value) {
+                    destinationData["value"] = expressionTranslator.translate(expressionToTranslate, storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble));
+                } else if (std::is_same<storm::RationalNumber, ValueType>::value) {
+                    destinationData["value"] = expressionTranslator.translate(expressionToTranslate, storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalNumber));
+                } else if (std::is_same<storm::RationalFunction, ValueType>::value) {
+                    destinationData["value"] = expressionTranslator.translate(expressionToTranslate, storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalFunction));
                 }
                 if (destination.getOrderedAssignments().empty()) {
                     destinationData["lowestLevel"] = "0";
@@ -1333,16 +1413,28 @@ namespace storm {
                 cpptempl::data_map result;
                 result["variable"] = getVariableName(assignment.getExpressionVariable());
                 auto lowerBoundIt = lowerBounds.find(assignment.getExpressionVariable());
+                
+                storm::expressions::ToCppTranslationOptions options(variablePrefixes, variableToName);
+                if (realVariables.find(assignment.getExpressionVariable()) != realVariables.end()) {
+                    if (std::is_same<double, ValueType>::value) {
+                        options = storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastDouble);
+                    } else if (std::is_same<storm::RationalNumber, ValueType>::value) {
+                        options = storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalNumber);
+                    } else if (std::is_same<storm::RationalFunction, ValueType>::value) {
+                        options = storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName, storm::expressions::ToCppTranslationMode::CastRationalFunction);
+                    }
+                }
+                
                 if (lowerBoundIt != lowerBounds.end()) {
                     if (lowerBoundIt->second < 0) {
-                        result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) + model.getManager().integer(lowerBoundIt->second), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName));
+                        result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) + model.getManager().integer(lowerBoundIt->second), options);
                     } else if (lowerBoundIt->second == 0) {
-                        result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName));
+                        result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), options);
                     } else {
-                        result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) - model.getManager().integer(lowerBoundIt->second), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName));
+                        result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()) - model.getManager().integer(lowerBoundIt->second), options);
                     }
                 } else {
-                    result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), storm::expressions::ToCppTranslationOptions(variablePrefixes, variableToName));
+                    result["value"] = expressionTranslator.translate(shiftVariablesWrtLowerBound(assignment.getAssignedExpression()), options);
                 }
                 return result;
             }
@@ -1428,6 +1520,19 @@ namespace storm {
                 
                 modelData["terminalExpressions"] = cpptempl::make_data(terminalExpressions);
             }
+                
+            template <typename ValueType, typename RewardModelType>
+            void ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::generateParameters(cpptempl::data_map& modelData) {
+                cpptempl::data_list parameters;
+                for (auto const& constant : model.getConstants()) {
+                    if (!constant.isDefined() && constant.isRealConstant()) {
+                        cpptempl::data_map parameter;
+                        parameter["name"] = constant.getName();
+                        parameters.push_back(parameter);
+                    }
+                }
+                modelData["parameters"] = cpptempl::make_data(parameters);
+            }
 
             template <typename ValueType, typename RewardModelType>
             std::string const& ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::getVariableName(storm::expressions::Variable const& variable) const {
@@ -1470,7 +1575,7 @@ namespace storm {
             std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::asString(ValueTypePrime value) const {
                 return std::to_string(value);
             }
-            
+                
             template <typename ValueType, typename RewardModelType>
             std::string ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::createSourceCodeFromSkeleton(cpptempl::data_map& modelData) {
                 std::string sourceTemplate = R"(
@@ -1484,6 +1589,13 @@ namespace storm {
 #include <unordered_map>
 #include <boost/dll/alias.hpp>
                 
+{% if exact %}
+#include "src/adapters/NumberAdapter.h"
+{% endif %}
+{% if parametric %}
+#include "src/adapters/CarlAdapter.h"
+{% endif %}
+                
 #include "resources/3rdparty/sparsepp/sparsepp.h"
                 
 #include "src/builder/jit/StateSet.h"
@@ -1492,6 +1604,8 @@ namespace storm {
 #include "src/builder/jit/ModelComponentsBuilder.h"
 #include "src/builder/RewardModelInformation.h"
                 
+#include "src/utility/constants.h"
+                
 #include "src/exceptions/WrongFormatException.h"
                 
                 namespace storm {
@@ -1499,7 +1613,16 @@ namespace storm {
                         namespace jit {
                             
                             typedef uint32_t IndexType;
+                            
+                            {% if double %}
                             typedef double ValueType;
+                            {% endif %}
+                            {% if exact %}
+                            typedef storm::RationalNumber ValueType;
+                            {% endif %}
+                            {% if parametric %}
+                            typedef storm::RationalFunction ValueType;
+                            {% endif %}
                             
                             struct StateType {
                                 // Boolean variables.
@@ -1576,8 +1699,18 @@ namespace storm {
                                 {% for variable in transient_variables.unboundedInteger %}int64_t {$variable.name};
                                 {% endfor %}
                                 // Real variables.
+                                {% if double %}
                                 {% for variable in transient_variables.real %}double {$variable.name};
                                 {% endfor %}
+                                {% endif %}
+                                {% if exact %}
+                                {% for variable in transient_variables.real %}storm::RationalNumber {$variable.name};
+                                {% endfor %}
+                                {% endif %}
+                                {% if parametric %}
+                                {% for variable in transient_variables.real %}storm::RationalFunction {$variable.name};
+                                {% endfor %}
+                                {% endif %}
                             };
                             
                             std::ostream& operator<<(std::ostream& out, TransientVariables const& in) {
@@ -1694,6 +1827,19 @@ namespace storm {
                                 {% endif %}
                             }
                             
+                            {% if parametric %}
+                            {% for parameter in parameters %}static storm::RationalFunction {$parameter.name};
+                            {% endfor %}
+                            
+                            void initialize_parameters(std::vector<storm::RationalFunction> const& parameters) {
+#ifndef NDEBUG
+                                std::cout << "initializing parameters" << std::endl;
+#endif
+                                {% for parameter in parameters %}{$parameter.name} = parameters[{$loop.index} - 1];
+                                {% endfor %}
+                            }
+                            {% endif %}
+                            
                             // Non-synchronizing edges.
                             {% for edge in nonsynch_edges %}static bool edge_enabled_{$edge.name}(StateType const& in) {
                                 if ({$edge.guard}) {
@@ -2085,7 +2231,7 @@ namespace storm {
                                     }
                                 }
                                 
-                                bool isTerminalState(StateType const& state) const {
+                                bool isTerminalState(StateType const& in) const {
                                     {% for expression in terminalExpressions %}if ({$expression}) {
                                         return true;
                                     }
@@ -2097,7 +2243,7 @@ namespace storm {
                                     {% for edge in nonsynch_edges %}{
                                         if ({$edge.guard}) {
                                             Choice<IndexType, ValueType>& choice = behaviour.addChoice(!model_is_deterministic() && !model_is_discrete_time() && {$edge.markovian});
-                                            choice.resizeRewards({$edge_destination_rewards_count}, 0);
+                                            choice.resizeRewards({$edge_destination_rewards_count});
                                             {
                                                 {% if exploration_checks %}VariableWrites variableWrites;
                                                 {% endif %}
@@ -2188,6 +2334,7 @@ namespace storm {
                             };
                             
                             BOOST_DLL_ALIAS(storm::builder::jit::JitBuilder::create, create_builder)
+                            BOOST_DLL_ALIAS(storm::builder::jit::initialize_parameters, initialize_parameters)
                         }
                     }
                 }
@@ -2203,7 +2350,8 @@ namespace storm {
                 dynamicLibraryPath += DYLIB_EXTENSION;
                 std::string dynamicLibraryFilename = boost::filesystem::absolute(dynamicLibraryPath).string();
                 
-                std::string command = compiler + " " + sourceFilename + " " + compilerFlags + " -I" + stormRoot + " -I" + stormRoot + "/build_xcode/include -I" + boostIncludeDirectory + " -o " + dynamicLibraryFilename;
+                // FIXME: get right of build_xcode/include
+                std::string command = compiler + " " + sourceFilename + " " + compilerFlags + " -I" + stormRoot + " -I" + stormRoot + "/build_xcode/include -I" + boostIncludeDirectory + " -I" + carlIncludeDir + " -o " + dynamicLibraryFilename;
                 boost::optional<std::string> error = execute(command);
                 
                 if (error) {
@@ -2214,10 +2362,48 @@ namespace storm {
                 return dynamicLibraryPath;
             }
             
+            template<typename RationalFunctionType, typename TP = typename RationalFunctionType::PolyType, carl::EnableIf<carl::needs_cache<TP>> = carl::dummy>
+            RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable, std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache) {
+                return RationalFunctionType(typename RationalFunctionType::PolyType(typename RationalFunctionType::PolyType::PolyType(variable), cache));
+            }
+                
+            template<typename RationalFunctionType, typename TP = typename RationalFunctionType::PolyType, carl::DisableIf<carl::needs_cache<TP>> = carl::dummy>
+            RationalFunctionType convertVariableToPolynomial(carl::Variable const& variable, std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache) {
+                return RationalFunctionType(variable);
+            }
+            
+            template<typename ValueType>
+            std::vector<storm::RationalFunction> getParameters(storm::jani::Model const& model, std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache) {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidStateException, "This function must not be called for this type.");
+            }
+                
+            template<>
+            std::vector<storm::RationalFunction> getParameters<storm::RationalFunction>(storm::jani::Model const& model, std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache) {
+                std::vector<storm::RationalFunction> parameters;
+                for (auto const& constant : model.getConstants()) {
+                    if (!constant.isDefined() && constant.isRealConstant()) {
+                        parameters.push_back(convertVariableToPolynomial<storm::RationalFunction>(carl::freshRealVariable(constant.getName()), cache));
+                    }
+                }
+                return parameters;
+            }
+                
             template <typename ValueType, typename RewardModelType>
             void ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::createBuilder(boost::filesystem::path const& dynamicLibraryPath) {
                 jitBuilderCreateFunction = boost::dll::import_alias<typename ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::CreateFunctionType>(dynamicLibraryPath, "create_builder");
                 builder = std::unique_ptr<JitModelBuilderInterface<IndexType, ValueType>>(jitBuilderCreateFunction(modelComponentsBuilder));
+                
+                if (std::is_same<storm::RationalFunction, ValueType>::value) {
+                    typedef void (InitializeParametersFunctionType)(std::vector<storm::RationalFunction> const&);
+                    typedef boost::function<InitializeParametersFunctionType> ImportInitializeParametersFunctionType;
+
+                    // Create the carl cache if we are building a parametric model.
+                    cache = std::make_shared<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>>();
+
+                    ImportInitializeParametersFunctionType initializeParametersFunction = boost::dll::import_alias<InitializeParametersFunctionType>(dynamicLibraryPath, "initialize_parameters");
+                    std::vector<storm::RationalFunction> parameters = getParameters<ValueType>(this->model, cache);
+                    initializeParametersFunction(parameters);
+                }
             }
             
             template class ExplicitJitJaniModelBuilder<double, storm::models::sparse::StandardRewardModel<double>>;
diff --git a/src/builder/jit/ExplicitJitJaniModelBuilder.h b/src/builder/jit/ExplicitJitJaniModelBuilder.h
index 2a652befe..e8b8a5ee5 100644
--- a/src/builder/jit/ExplicitJitJaniModelBuilder.h
+++ b/src/builder/jit/ExplicitJitJaniModelBuilder.h
@@ -8,6 +8,8 @@
 
 #include "cpptempl.h"
 
+#include "src/adapters/CarlAdapter.h"
+
 #include "src/storage/jani/Model.h"
 #include "src/storage/jani/ParallelComposition.h"
 #include "src/storage/expressions/ToCppVisitor.h"
@@ -36,7 +38,7 @@ namespace storm {
             class ExplicitJitJaniModelBuilder {
             public:
                 typedef JitModelBuilderInterface<IndexType, ValueType>* (CreateFunctionType)(ModelComponentsBuilder<IndexType, ValueType>& modelComponentsBuilder);
-                typedef boost::function<CreateFunctionType> ImportFunctionType;
+                typedef boost::function<CreateFunctionType> ImportCreateFunctionType;
                 
                 /*!
                  * Creates a model builder for the given model. The provided options are used to determine which part of
@@ -63,6 +65,7 @@ namespace storm {
                 bool checkBoostAvailable() const;
                 bool checkBoostDllAvailable() const;
                 bool checkStormAvailable() const;
+                bool checkCarlAvailable() const;
                 
                 /*!
                  * Executes the given command. If the command fails with a non-zero error code, the error stream content
@@ -92,7 +95,8 @@ namespace storm {
                 void generateLocations(cpptempl::data_map& modelData);
                 void generateLabels(cpptempl::data_map& modelData);
                 void generateTerminalExpressions(cpptempl::data_map& modelData);
-
+                void generateParameters(cpptempl::data_map& modelData);
+                
                 // Functions related to the generation of edge data.
                 void generateEdges(cpptempl::data_map& modelData);
                 cpptempl::data_map generateSynchronizationVector(cpptempl::data_map& modelData, storm::jani::ParallelComposition const& parallelComposition, storm::jani::SynchronizationVector const& synchronizationVector, uint64_t synchronizationVectorIndex);
@@ -149,7 +153,7 @@ namespace storm {
                 
                 /// The function that was loaded from the shared library. We have to keep this function around, because
                 /// otherwise the shared library gets unloaded.
-                typename ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::ImportFunctionType jitBuilderCreateFunction;
+                typename ExplicitJitJaniModelBuilder<ValueType, RewardModelType>::ImportCreateFunctionType jitBuilderCreateFunction;
                 
                 /// The pointer to the builder object created via the shared library.
                 std::unique_ptr<JitModelBuilderInterface<IndexType, ValueType>> builder;
@@ -163,6 +167,7 @@ namespace storm {
                 std::map<storm::expressions::Variable, int_fast64_t> lowerBounds;
                 std::set<storm::expressions::Variable> transientVariables;
                 std::set<storm::expressions::Variable> nontransientVariables;
+                std::set<storm::expressions::Variable> realVariables;
                 std::unordered_map<storm::expressions::Variable, std::string> variablePrefixes;
 
                 /// The compiler binary.
@@ -176,6 +181,12 @@ namespace storm {
                 
                 /// The root directory of storm.
                 std::string stormRoot;
+                
+                /// The include directory of carl.
+                std::string carlIncludeDir;
+                
+                /// A cache that is used by carl.
+                std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache;
             };
 
         }
diff --git a/src/settings/modules/JitBuilderSettings.cpp b/src/settings/modules/JitBuilderSettings.cpp
index fa44ac4b3..4aa53d925 100644
--- a/src/settings/modules/JitBuilderSettings.cpp
+++ b/src/settings/modules/JitBuilderSettings.cpp
@@ -18,6 +18,7 @@ namespace storm {
             const std::string JitBuilderSettings::compilerOptionName = "compiler";
             const std::string JitBuilderSettings::stormRootOptionName = "storm";
             const std::string JitBuilderSettings::boostIncludeDirectoryOptionName = "boost";
+            const std::string JitBuilderSettings::carlIncludeDirectoryOptionName = "carl";
             const std::string JitBuilderSettings::compilerFlagsOptionName = "cxxflags";
 
             JitBuilderSettings::JitBuilderSettings() : ModuleSettings(moduleName) {
@@ -28,6 +29,8 @@ namespace storm {
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory that contains the src/ subtree of Storm.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, boostIncludeDirectoryOptionName, false, "The include directory of boost.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory containing the boost headers version >= 1.61.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, carlIncludeDirectoryOptionName, false, "The include directory of carl.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("dir", "The directory containing the carl headers.").build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, compilerFlagsOptionName, false, "The flags passed to the compiler.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("flags", "The compiler flags.").build()).build());
             }
@@ -56,6 +59,14 @@ namespace storm {
                 return this->getOption(boostIncludeDirectoryOptionName).getArgumentByName("dir").getValueAsString();
             }
 
+            bool JitBuilderSettings::isCarlIncludeDirectorySet() const {
+                return this->getOption(carlIncludeDirectoryOptionName).getHasOptionBeenSet();
+            }
+            
+            std::string JitBuilderSettings::getCarlIncludeDirectory() const {
+                return this->getOption(carlIncludeDirectoryOptionName).getArgumentByName("dir").getValueAsString();
+            }
+
             bool JitBuilderSettings::isDoctorSet() const {
                 return this->getOption(doctorOptionName).getHasOptionBeenSet();
             }
diff --git a/src/settings/modules/JitBuilderSettings.h b/src/settings/modules/JitBuilderSettings.h
index abb916170..948620900 100644
--- a/src/settings/modules/JitBuilderSettings.h
+++ b/src/settings/modules/JitBuilderSettings.h
@@ -23,7 +23,10 @@ namespace storm {
                 
                 bool isBoostIncludeDirectorySet() const;
                 std::string getBoostIncludeDirectory() const;
-                
+
+                bool isCarlIncludeDirectorySet() const;
+                std::string getCarlIncludeDirectory() const;
+
                 bool isCompilerFlagsSet() const;
                 std::string getCompilerFlags() const;
                 
@@ -36,6 +39,7 @@ namespace storm {
                 static const std::string compilerOptionName;
                 static const std::string stormRootOptionName;
                 static const std::string boostIncludeDirectoryOptionName;
+                static const std::string carlIncludeDirectoryOptionName;
                 static const std::string compilerFlagsOptionName;
                 static const std::string doctorOptionName;
             };
diff --git a/src/storage/expressions/ToCppVisitor.cpp b/src/storage/expressions/ToCppVisitor.cpp
index 108d95fe8..f705e7b6b 100644
--- a/src/storage/expressions/ToCppVisitor.cpp
+++ b/src/storage/expressions/ToCppVisitor.cpp
@@ -5,28 +5,20 @@
 namespace storm {
     namespace expressions {
         
-        ToCppTranslationOptions::ToCppTranslationOptions(std::unordered_map<storm::expressions::Variable, std::string> const& prefixes, std::unordered_map<storm::expressions::Variable, std::string> const& names, std::string const& valueTypeCast) : prefixes(prefixes), names(names), valueTypeCast(valueTypeCast) {
+        ToCppTranslationOptions::ToCppTranslationOptions(std::unordered_map<storm::expressions::Variable, std::string> const& prefixes, std::unordered_map<storm::expressions::Variable, std::string> const& names, ToCppTranslationMode mode) : prefixes(prefixes), names(names), mode(mode) {
             // Intentionally left empty.
         }
         
         std::unordered_map<storm::expressions::Variable, std::string> const& ToCppTranslationOptions::getPrefixes() const {
-            return prefixes;
+            return prefixes.get();
         }
         
         std::unordered_map<storm::expressions::Variable, std::string> const& ToCppTranslationOptions::getNames() const {
-            return names;
+            return names.get();
         }
         
-        bool ToCppTranslationOptions::hasValueTypeCast() const {
-            return !valueTypeCast.empty();
-        }
-        
-        std::string const& ToCppTranslationOptions::getValueTypeCast() const {
-            return valueTypeCast;
-        }
-        
-        void ToCppTranslationOptions::clearValueTypeCast() {
-            valueTypeCast = "";
+        ToCppTranslationMode const& ToCppTranslationOptions::getMode() const {
+            return mode;
         }
         
         std::string ToCppVisitor::translate(storm::expressions::Expression const& expression, ToCppTranslationOptions const& options) {
@@ -37,8 +29,10 @@ namespace storm {
         }
         
         boost::any ToCppVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) {
-            ToCppTranslationOptions conditionOptions = boost::any_cast<ToCppTranslationOptions>(data);
-            conditionOptions.clearValueTypeCast();
+            ToCppTranslationOptions const& options = boost::any_cast<ToCppTranslationOptions>(data);
+            
+            // Clear the type cast for the condition.
+            ToCppTranslationOptions conditionOptions(options.getPrefixes(), options.getNames());
             stream << "(";
             expression.getCondition()->accept(*this, conditionOptions);
             stream << " ? ";
@@ -51,7 +45,6 @@ namespace storm {
         
         boost::any ToCppVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
             ToCppTranslationOptions newOptions = boost::any_cast<ToCppTranslationOptions>(data);
-            newOptions.clearValueTypeCast();
             
             switch (expression.getOperatorType()) {
                     case BinaryBooleanFunctionExpression::OperatorType::And:
@@ -150,7 +143,6 @@ namespace storm {
         
         boost::any ToCppVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) {
             ToCppTranslationOptions newOptions = boost::any_cast<ToCppTranslationOptions>(data);
-            newOptions.clearValueTypeCast();
 
             switch (expression.getRelationType()) {
                 case BinaryRelationExpression::RelationType::Equal:
@@ -198,39 +190,55 @@ namespace storm {
             }
             return boost::none;
         }
-        
-        boost::any ToCppVisitor::visit(VariableExpression const& expression, boost::any const& data) {
-            ToCppTranslationOptions const& options = boost::any_cast<ToCppTranslationOptions const&>(data);
-            if (options.hasValueTypeCast()) {
-                stream << "static_cast<" << options.getValueTypeCast() << ">(";
-            }
-            
-            auto prefixIt = options.getPrefixes().find(expression.getVariable());
-            if (prefixIt != options.getPrefixes().end()) {
-                auto nameIt = options.getNames().find(expression.getVariable());
-                if (nameIt != options.getNames().end()) {
-                    stream << prefixIt->second << nameIt->second;
+
+        std::string getVariableName(storm::expressions::Variable const& variable, std::unordered_map<storm::expressions::Variable, std::string> const& prefixes, std::unordered_map<storm::expressions::Variable, std::string> const& names) {
+            auto prefixIt = prefixes.find(variable);
+            if (prefixIt != prefixes.end()) {
+                auto nameIt = names.find(variable);
+                if (nameIt != names.end()) {
+                    return prefixIt->second + nameIt->second;
                 } else {
-                    stream << prefixIt->second << expression.getVariableName();
+                    return prefixIt->second + variable.getName();
                 }
             } else {
-                auto nameIt = options.getNames().find(expression.getVariable());
-                if (nameIt != options.getNames().end()) {
-                    stream << nameIt->second;
+                auto nameIt = names.find(variable);
+                if (nameIt != names.end()) {
+                    return nameIt->second;
                 } else {
-                    stream << expression.getVariableName();
+                    return variable.getName();
                 }
             }
+        }
+        
+        boost::any ToCppVisitor::visit(VariableExpression const& expression, boost::any const& data) {
+            ToCppTranslationOptions const& options = boost::any_cast<ToCppTranslationOptions const&>(data);
+            storm::expressions::Variable const& variable = expression.getVariable();
+            std::string variableName = getVariableName(variable, options.getPrefixes(), options.getNames());
             
-            if (options.hasValueTypeCast()) {
-                stream << ")";
+            if (variable.hasBooleanType()) {
+                stream << variableName;
+            } else {
+                switch (options.getMode()) {
+                    case ToCppTranslationMode::KeepType:
+                        stream << variableName;
+                        break;
+                    case ToCppTranslationMode::CastDouble:
+                        stream << "static_cast<double>(" << variableName << ")";
+                        break;
+                    case ToCppTranslationMode::CastRationalNumber:
+                        stream << "carl::rationalize<storm::RationalNumber>(" << variableName << ")";
+                        break;
+                    case ToCppTranslationMode::CastRationalFunction:
+                        // Here, we rely on the variable name mapping to a rational function representing the variable being available.
+                        stream << variableName;
+                        break;
+                }
             }
             return boost::none;
         }
-        
+
         boost::any ToCppVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
             ToCppTranslationOptions newOptions = boost::any_cast<ToCppTranslationOptions>(data);
-            newOptions.clearValueTypeCast();
             
             switch (expression.getOperatorType()) {
                 case UnaryBooleanFunctionExpression::OperatorType::Not:
@@ -270,18 +278,39 @@ namespace storm {
         
         boost::any ToCppVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) {
             ToCppTranslationOptions const& options = boost::any_cast<ToCppTranslationOptions const&>(data);
-            if (options.hasValueTypeCast()) {
-                stream << "static_cast<" << options.getValueTypeCast() << ">(";
-            }
-            stream << expression.getValue();
-            if (options.hasValueTypeCast()) {
-                stream << ")";
+            switch (options.getMode()) {
+                case ToCppTranslationMode::KeepType:
+                    stream << expression.getValue();
+                    break;
+                case ToCppTranslationMode::CastDouble:
+                    stream << "static_cast<double>(" << expression.getValue() << ")";
+                    break;
+                case ToCppTranslationMode::CastRationalNumber:
+                    stream << "carl::rationalize<storm::RationalNumber>(\"" << expression.getValue() << "\")";
+                    break;
+                case ToCppTranslationMode::CastRationalFunction:
+                    stream << "storm::RationalFunction(carl::rationalize<storm::RationalNumber>(\"" << expression.getValue() << "\"))";
+                    break;
             }
             return boost::none;
         }
-        
+
         boost::any ToCppVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) {
-            stream << expression.getValueAsDouble();
+            ToCppTranslationOptions const& options = boost::any_cast<ToCppTranslationOptions const&>(data);
+            switch (options.getMode()) {
+                case ToCppTranslationMode::KeepType:
+                    stream << expression.getValue();
+                    break;
+                case ToCppTranslationMode::CastDouble:
+                    stream << "static_cast<double>(" << expression.getValueAsDouble() << ")";
+                    break;
+                case ToCppTranslationMode::CastRationalNumber:
+                    stream << "carl::rationalize<storm::RationalNumber>(\"" << expression.getValue() << "\")";
+                    break;
+                case ToCppTranslationMode::CastRationalFunction:
+                    stream << "storm::RationalFunction(carl::rationalize<storm::RationalNumber>(\"" << expression.getValue() << "\"))";
+                    break;
+            }
             return boost::none;
         }
 
diff --git a/src/storage/expressions/ToCppVisitor.h b/src/storage/expressions/ToCppVisitor.h
index a94af32de..3eb1a3120 100644
--- a/src/storage/expressions/ToCppVisitor.h
+++ b/src/storage/expressions/ToCppVisitor.h
@@ -10,21 +10,22 @@ namespace storm {
     namespace expressions {
         class Expression;
         
+        enum class ToCppTranslationMode {
+            KeepType, CastDouble, CastRationalNumber, CastRationalFunction
+        };
+        
         class ToCppTranslationOptions {
         public:
-            ToCppTranslationOptions(std::unordered_map<storm::expressions::Variable, std::string> const& prefixes, std::unordered_map<storm::expressions::Variable, std::string> const& names, std::string const& valueTypeCast = "");
+            ToCppTranslationOptions(std::unordered_map<storm::expressions::Variable, std::string> const& prefixes, std::unordered_map<storm::expressions::Variable, std::string> const& names, ToCppTranslationMode mode = ToCppTranslationMode::KeepType);
             
             std::unordered_map<storm::expressions::Variable, std::string> const& getPrefixes() const;
             std::unordered_map<storm::expressions::Variable, std::string> const& getNames() const;
-            
-            bool hasValueTypeCast() const;
-            std::string const& getValueTypeCast() const;
-            void clearValueTypeCast();
+            ToCppTranslationMode const& getMode() const;
             
         private:
-            std::unordered_map<storm::expressions::Variable, std::string> const& prefixes;
-            std::unordered_map<storm::expressions::Variable, std::string> const& names;
-            std::string valueTypeCast;
+            std::reference_wrapper<std::unordered_map<storm::expressions::Variable, std::string> const> prefixes;
+            std::reference_wrapper<std::unordered_map<storm::expressions::Variable, std::string> const> names;
+            ToCppTranslationMode mode;
         };
         
         class ToCppVisitor : public ExpressionVisitor {
diff --git a/src/utility/storm.h b/src/utility/storm.h
index 06089b763..7d8ac5526 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -223,7 +223,7 @@ namespace storm {
     
     template<typename ModelType>
     std::shared_ptr<storm::models::ModelBase> preprocessModel(std::shared_ptr<storm::models::ModelBase> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
-        if(model->getType() == storm::models::ModelType::MarkovAutomaton && model->isSparseModel()) {
+        if (model->getType() == storm::models::ModelType::MarkovAutomaton && model->isSparseModel()) {
             std::shared_ptr<storm::models::sparse::MarkovAutomaton<typename ModelType::ValueType>> ma = model->template as<storm::models::sparse::MarkovAutomaton<typename ModelType::ValueType>>();
             if (ma->hasOnlyTrivialNondeterminism()) {
                 // Markov automaton can be converted into CTMC
@@ -459,7 +459,7 @@ namespace storm {
         auto const& regionSettings = storm::settings::getModule<storm::settings::modules::RegionSettings>();
         storm::modelchecker::region::SparseRegionModelCheckerSettings settings(regionSettings.getSampleMode(), regionSettings.getApproxMode(), regionSettings.getSmtMode());
         // Preprocessing and ModelChecker
-        if(model->isOfType(storm::models::ModelType::Dtmc)){
+        if (model->isOfType(storm::models::ModelType::Dtmc)){
             preprocessModel<storm::models::sparse::Dtmc<storm::RationalFunction>>(model,formulas);
             regionModelChecker = std::make_shared<storm::modelchecker::region::SparseDtmcRegionModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>>(model->as<storm::models::sparse::Dtmc<storm::RationalFunction>>(), settings);
         } else if (model->isOfType(storm::models::ModelType::Mdp)){
diff --git a/storm-config.h.in b/storm-config.h.in
index fa69055be..a3887b691 100644
--- a/storm-config.h.in
+++ b/storm-config.h.in
@@ -14,9 +14,12 @@
 // The path used in the functional and performance tests to load the supplied example files
 #define STORM_CPP_TESTS_BASE_PATH "@STORM_CPP_TESTS_BASE_PATH@"
 
-// The path to boost used during compilation. 
+// Boost include directory used during compilation.
 #define STORM_BOOST_INCLUDE_DIR "@STORM_BOOST_INCLUDE_DIR@"
 
+// Carl include directory used during compilation.
+#define STORM_CARL_INCLUDE_DIR "@STORM_CARL_INCLUDE_DIR@"
+
 // Whether Gurobi is available and to be used (define/undef)
 #cmakedefine STORM_HAVE_GUROBI