diff --git a/CMakeLists.txt b/CMakeLists.txt
index f1a741bb7..6f1c9d174 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -20,6 +20,7 @@ include(ExternalProject)
 #############################################################
 option(STORM_DEVELOPER "Sets whether the development mode is used" OFF)
 option(STORM_USE_POPCNT "Sets whether the popcnt instruction is going to be used." ON)
+MARK_AS_ADVANCED(STORM_USE_POPCNT)
 option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be linked statically." ON)
 option(STORM_USE_INTELTBB "Sets whether the Intel TBB libraries should be used." OFF)
 option(STORM_USE_GUROBI "Sets whether Gurobi should be used." OFF)
@@ -29,8 +30,10 @@ option(USE_LIBCXX "Sets whether the standard library is libc++." OFF)
 option(USE_CARL "Sets whether carl should be included." ON)
 option(USE_XERCES "Sets whether xerces should be used." OFF)
 option(FORCE_COLOR "Force color output" OFF)
+mark_as_advanced(FORCE_COLOR)
 option(STORM_PYTHON "Builds the API for Python" OFF)
-option(STORM_COMPILE_WITH_CCACHE "Compile using CCache" ON)
+option(STORM_COMPILE_WITH_CCACHE "Compile using CCache [if found]" ON)
+mark_as_advanced(STORM_COMPILE_WITH_CCACHE)
 option(STORM_LOG_DISABLE_DEBUG "Disable log and trace message support" OFF)
 set(BOOST_ROOT "" CACHE STRING "A hint to the root directory of Boost (optional).")
 set(GUROBI_ROOT "" CACHE STRING "A hint to the root directory of Gurobi (optional).")
@@ -40,6 +43,12 @@ set(MSAT_ROOT "" CACHE STRING "The hint to the root directory of MathSAT (option
 set(ADDITIONAL_INCLUDE_DIRS "" CACHE STRING "Additional directories added to the include directories.")
 set(ADDITIONAL_LINK_DIRS "" CACHE STRING "Additional directories added to the link directories.")
 
+
+# Set some CMAKE Variables as advanced
+mark_as_advanced(CMAKE_OSX_ARCHITECTURES)
+mark_as_advanced(CMAKE_OSX_SYSROOT)
+mark_as_advanced(CMAKE_OSX_DEPLOYMENT_TARGET)
+
 # If the STORM_DEVELOPER option was turned on, we will target a debug version.
 if (STORM_DEVELOPER)
     message(STATUS "StoRM - Using development mode")
@@ -50,6 +59,7 @@ message(STATUS "StoRM - Building ${CMAKE_BUILD_TYPE} version.")
 
 if(STORM_COMPILE_WITH_CCACHE)
 	find_program(CCACHE_FOUND ccache)
+	mark_as_advanced(CCACHE_FOUND)
 	if(CCACHE_FOUND)
 		message(STATUS "StoRM - Using ccache")
 		set_property(GLOBAL PROPERTY RULE_LAUNCH_COMPILE ccache)
@@ -129,7 +139,9 @@ if(CMAKE_COMPILER_IS_GNUCC)
 
     set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} ${STORM_CXX_STD_COMMAND} -Wall -pedantic -Wno-deprecated-declarations -Wno-unused-local-typedefs -Wno-unknown-pragmas")
     set(CMAKE_C_FLAGS "${CMAKE_C_FLAGS} -Wall -pedantic -Wno-deprecated-declarations")
-
+	if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 5.0)
+		message(FATAL_ERROR "GCC version must be at least 5.0!")
+	endif()
     # Turn on popcnt instruction if desired (yes by default)
     if (STORM_USE_POPCNT)
         set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -mpopcnt")
@@ -160,6 +172,19 @@ else(CLANG)
 	set (CLANG ON)
     # Set standard flags for clang
     set (CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -funroll-loops -O3")
+
+	if(UNIX AND NOT APPLE)
+		if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 3.2)
+			message(FATAL_ERROR "Clang version must be at least 3.2!")
+		endif()
+	endif()
+
+	if(UNIX AND APPLE)
+		if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 7.3)
+			message(FATAL_ERROR "Clang version must be at least 7.3!")
+		endif()
+	endif()
+
     if(UNIX AND NOT APPLE AND NOT USE_LIBCXX)
 		set(CLANG_STDLIB libstdc++)
 		message(STATUS "StoRM - Linking against libstdc++")
@@ -189,6 +214,7 @@ else(CLANG)
 	set_source_files_properties(${CONVERSIONHELPER_TARGET} PROPERTIES COMPILE_FLAGS " -fno-strict-aliasing ")
 endif()
 
+
 if(CCACHE_FOUND)
 	set(STORM_COMPILED_BY  "${STORM_COMPILED_BY} (ccache)")
 endif()
@@ -211,515 +237,8 @@ message(STATUS "StoRM - Using Compiler Configuration: ${STORM_COMPILED_BY}")
 
 # In 3rdparty, targets are being defined that can be used
 # in the the system does not have a library
-add_subdirectory(resources/3rdparty)
-
-#############################################################
-##
-##	l3pp
-##
-#############################################################
-
-# l3pp is set up as external project
-include_directories(${l3pp_INCLUDE})
-add_dependencies(resources l3pp)
-
-#############################################################
-##
-##	gmm
-##
-#############################################################
-
-# Add the shipped version of GMM to the include pathes
-set(GMMXX_INCLUDE_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/gmm-5.0/include")
-include_directories(${GMMXX_INCLUDE_DIR})
-
-#############################################################
-##
-##	Eigen
-##
-#############################################################
-
-# Add the shipped version of Eigen to the include pathes
-set(EIGEN_INCLUDE_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/eigen-3.3-beta1")
-include_directories(${EIGEN_INCLUDE_DIR})
-
-#############################################################
-##
-##	gmp
-##
-#############################################################
-
-# GMP is optional (unless MathSAT is used, see below)
-find_package(GMP QUIET)
-
-#############################################################
-##
-##	Boost
-##
-#############################################################
-
-# Boost Option variables
-set(Boost_USE_STATIC_LIBS        ${USE_BOOST_STATIC_LIBRARIES})
-set(Boost_USE_MULTITHREADED      ON)
-set(Boost_USE_STATIC_RUNTIME    OFF)
-
-find_package(Boost 1.56.0 QUIET REQUIRED)
-
-if ((NOT Boost_LIBRARY_DIRS) OR ("${Boost_LIBRARY_DIRS}" STREQUAL ""))
-    set(Boost_LIBRARY_DIRS "${Boost_INCLUDE_DIRS}/stage/lib")
-endif ()
-link_directories(${Boost_LIBRARY_DIRS})
-
-include_directories(${Boost_INCLUDE_DIRS})
-list(APPEND STORM_LINK_LIBRARIES ${Boost_LIBRARIES})
-message(STATUS "StoRM - Using Boost ${Boost_VERSION} (lib ${Boost_LIB_VERSION})")
-#message(STATUS "StoRM - BOOST_INCLUDE_DIRS is ${Boost_INCLUDE_DIRS}")
-#message(STATUS "StoRM - BOOST_LIBRARY_DIRS is ${Boost_LIBRARY_DIRS}")
-
-#############################################################
-##
-##	ExprTk
-##
-#############################################################
-
-# Use the shipped version of ExprTK
-message (STATUS "StoRM - Including ExprTk")
-include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/exprtk")
-
-#############################################################
-##
-##	ModernJSON
-##
-#############################################################
+include(resources/3rdparty/CMakeLists.txt)
 
-#use the shipped version of modernjson
-message (STATUS "StoRM - Including ModernJSON")
-include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/modernjson/src/")
-
-#############################################################
-##
-##	Z3 (optional)
-##
-#############################################################
-
-find_package(Z3 QUIET)
-
-# Z3 Defines
-set(STORM_HAVE_Z3 ${Z3_FOUND})
-
-if(Z3_FOUND)
-    message (STATUS "StoRM - Linking with Z3")
-    include_directories(${Z3_INCLUDE_DIRS})
-    list(APPEND STORM_LINK_LIBRARIES ${Z3_LIBRARIES})
-endif(Z3_FOUND)
-
-#############################################################
-##
-##	glpk
-##
-#############################################################
-
-find_package(GLPK QUIET)
-if(GLPK_FOUND)
-	message (STATUS "StoRM - Using system version of GLPK")
-else()
-	message (STATUS "StoRM - Using shipped version of GLPK")
-	set(GLPK_LIBRARIES  ${CMAKE_BINARY_DIR}/resources/3rdparty/glpk-4.57/lib/libglpk${DYNAMIC_EXT})
-	set(GLPK_INCLUDE_DIR ${CMAKE_BINARY_DIR}/resources/3rdparty/glpk-4.57/include)
-	set(GLPK_VERSION_STRING 4.57)
-	add_dependencies(resources glpk)
-endif()
-
-# Since there is a shipped version, always use GLPK
-set(STORM_HAVE_GLPK ON)
-message (STATUS "StoRM - Linking with glpk ${GLPK_VERSION_STRING}")
-include_directories(${GLPK_INCLUDE_DIR})
-list(APPEND STORM_LINK_LIBRARIES ${GLPK_LIBRARIES})
-
-#############################################################
-##
-##	Gurobi (optional)
-##
-#############################################################
-
-if (STORM_USE_GUROBI)
-	find_package(Gurobi QUIET REQUIRED)
-	set(STORM_HAVE_GUROBI ${GUROBI_FOUND})
-	if (GUROBI_FOUND)
-		message (STATUS "StoRM - Linking with Gurobi")
-		include_directories(${GUROBI_INCLUDE_DIRS})
-		list(APPEND STORM_LINK_LIBRARIES ${GUROBI_LIBRARY})
-		#link_directories("${GUROBI_ROOT}/lib")
-	else()
-		#message(FATAL_ERROR "StoRM - Gurobi was requested, but not found!")
-	endif()
-else()
-	set(STORM_HAVE_GUROBI OFF)
-endif()
-
-#############################################################
-##
-##	CUDD
-##
-#############################################################
-
-# Do not use system CUDD, StoRM has a modified version
-set(CUDD_INCLUDE_DIR ${CMAKE_BINARY_DIR}/resources/3rdparty/cudd-3.0.0/include)
-set(CUDD_SHARED_LIBRARY ${CMAKE_BINARY_DIR}/resources/3rdparty/cudd-3.0.0/lib/libcudd${DYNAMIC_EXT})
-set(CUDD_STATIC_LIBRARY ${CMAKE_BINARY_DIR}/resources/3rdparty/cudd-3.0.0/lib/libcudd${STATIC_EXT})
-set(CUDD_VERSION_STRING 3.0.0)
-list(APPEND STORM_LINK_LIBRARIES ${CUDD_SHARED_LIBRARY})
-add_dependencies(resources cudd3)
-
-message(STATUS "StoRM - Linking with CUDD ${CUDD_VERSION_STRING}")
-#message("StoRM - CUDD include dir: ${CUDD_INCLUDE_DIR}")
-include_directories(${CUDD_INCLUDE_DIR})
-
-#############################################################
-##
-##      CLN
-##
-#############################################################
-
-find_package(CLN QUIET)
-
-if(CLN_FOUND)
-    set(STORM_HAVE_CLN ON)
-    message(STATUS "StoRM - Linking with CLN ${CLN_VERSION_STRING}")
-    include_directories("${CLN_INCLUDE_DIR}")
-    list(APPEND STORM_LINK_LIBRARIES ${CLN_LIBRARIES})
-else()
-    set(STORM_HAVE_CLN OFF)
-    if(NOT GMP_FOUND)
-        message(FATAL_ERROR "StoRM - Neither CLN nor GMP found")
-    endif()
-endif()
-
-#############################################################
-##
-##      carl
-##
-#############################################################
-
-set(STORM_HAVE_CARL OFF)
-if(USE_CARL)
-	find_package(carl QUIET REQUIRED)
-	if(carl_FOUND)
-		set(STORM_HAVE_CARL ON)
-		message(STATUS "StoRM - Linking with carl ${carl_VERSION_STRING}")
-		include_directories("${carl_INCLUDE_DIR}")
-		list(APPEND STORM_LINK_LIBRARIES ${carl_LIBRARIES})
-	else()
-		message(FATAL_ERROR "StoRM - CARL was requested but not found")
-	endif()
-endif()
-
-#############################################################
-##
-##      SMT-RAT
-##
-#############################################################
-
-# No find routine yet
-#find_package(smtrat QUIET)
-# Not yet supported
-set(smtrat_FOUND OFF)
-set(STORM_HAVE_SMTRAT OFF)
-if(smtrat_FOUND)
-	set(STORM_HAVE_SMTRAT ON)
-	message(STATUS "StoRM - Linking with smtrat.")
-    include_directories("${smtrat_INCLUDE_DIR}")
-    list(APPEND STORM_LINK_LIBRARIES ${smtrat_LIBRARIES})
-endif()
-
-#############################################################
-##
-##      GiNaC
-##
-#############################################################
-
-find_package(GiNaC QUIET)
-
-if(GINAC_FOUND)
-    set(STORM_HAVE_GINAC ON)
-    message(STATUS "StoRM - Linking with GiNaC ${GINAC_VERSION_STRING}")
-    # Right now only link with GiNaC for carl
-    #include_directories("${GINAC_INCLUDE_DIR}")
-    list(APPEND STORM_LINK_LIBRARIES ${GINAC_LIBRARIES})
-else()
-    set(STORM_HAVE_GINAC OFF)
-    #TODO: Check if CARL actually requires the use of GiNaC
-endif()
-
-#############################################################
-##
-##	MathSAT (optional)
-##
-#############################################################
-
-if ("${MSAT_ROOT}" STREQUAL "")
-    set(ENABLE_MSAT OFF)
-else()
-    set(ENABLE_MSAT ON)
-endif()
-
-# MathSAT Defines
-set(STORM_HAVE_MSAT ${ENABLE_MSAT})
-if (ENABLE_MSAT)
-    message (STATUS "StoRM - Linking with MathSAT")
-    link_directories("${MSAT_ROOT}/lib")
-    include_directories("${MSAT_ROOT}/include")
-    list(APPEND STORM_LINK_LIBRARIES "mathsat")
-    if(GMP_FOUND)
-        include_directories("${GMP_INCLUDE_DIR}")
-        list(APPEND STORM_LINK_LIBRARIES "gmp")
-    elseif(MPIR_FOUND)
-        include_directories("${GMP_INCLUDE_DIR}")
-        list(APPEND STORM_LINK_LIBRARIES "mpir" "mpirxx")
-    else(GMP_FOUND)
-        message(FATAL_ERROR "GMP is required for MathSAT, but was not found!")
-    endif(GMP_FOUND)
-endif(ENABLE_MSAT)
-
-#############################################################
-##
-##	Xerces
-##
-#############################################################
-
-if(USE_XERCES)
-	find_package(Xerces QUIET REQUIRED)
-	if(XERCES_FOUND)
-		message(STATUS "StoRM - Use system version of xerces")
-    else()
-		message(STATUS "StoRM - Use shipped version of xerces")
-		set(XERCES_ROOT ${CMAKE_BINARY_DIR}/resources/3rdparty/xercesc-3.1.2)
-		set(XERCESC_INCLUDE ${XERCES_ROOT}/include)
-		set(XERCES_LIBRARY_PATH ${XERCES_ROOT}/lib)
-		set(XERCESC_LIBRARIES ${XERCES_LIBRARY_PATH}/libxerces-c.a)
-
-		add_dependencies(resources xercesc)
-    endif()
-
-	message (STATUS "StoRM - Linking with xercesc")
-    set(STORM_HAVE_XERCES ON)
-	include_directories(${XERCESC_INCLUDE})
-	list(APPEND STORM_LINK_LIBRARIES ${XERCESC_LIBRARIES})
-endif(USE_XERCES)
-
-#############################################################
-##
-##	Sylvan
-##
-#############################################################
-
-message(STATUS "StoRM - Using shipped version of sylvan")
-message(STATUS "StoRM - Linking with sylvan")
-include_directories("${Sylvan_INCLUDE_DIR}")
-list(APPEND STORM_LINK_LIBRARIES ${Sylvan_LIBRARY})
-add_dependencies(resources sylvan)
-
-if(${OPERATING_SYSTEM} MATCHES "Linux")
-	find_package(Hwloc QUIET REQUIRED)
-	if(Hwloc_FOUND)
-		message(STATUS "StoRM - Linking with hwloc ${Hwloc_VERSION}")
-		list(APPEND STORM_LINK_LIBRARIES ${Hwloc_LIBRARIES})
-	else()
-		message(FATAL_ERROR "HWLOC is required but was not found.")
-	endif()
-endif()
-
-#############################################################
-##
-##	Google Test gtest
-##
-#############################################################
-
-add_dependencies(test-resources googletest)
-list(APPEND STORM_TEST_LINK_LIBRARIES ${GTEST_LIBRARIES})
-
-#############################################################
-##
-##	Intel Threading Building Blocks (optional)
-##
-#############################################################
-
-set(STORM_HAVE_INTELTBB OFF)
-if (STORM_USE_INTELTBB)
-	# Point to shipped TBB directory
-	set(TBB_INSTALL_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/tbb42_20140122_merged-win-lin-mac")
-	find_package(TBB QUIET REQUIRED)
-
-	if (TBB_FOUND)
-		message(STATUS "StoRM - Found Intel TBB with interface version ${TBB_INTERFACE_VERSION}.")
-		message(STATUS "StoRM - Linking with Intel TBB in ${TBB_LIBRARY_DIRS}.")
-		set(STORM_HAVE_INTELTBB ON)
-		link_directories(${TBB_LIBRARY_DIRS})
-		include_directories(${TBB_INCLUDE_DIRS})
-		list(APPEND STORM_LINK_LIBRARIES tbb tbbmalloc)	
-	else(TBB_FOUND)
-		message(FATAL_ERROR "StoRM - TBB was requested, but not found!")
-	endif(TBB_FOUND)
-endif(STORM_USE_INTELTBB)
-
-#############################################################
-##
-##	Threads
-##
-#############################################################
-
-find_package(Threads QUIET REQUIRED)
-if (NOT Threads_FOUND)
-	message(FATAL_ERROR "StoRM - Threads was requested, but not found!")
-endif()
-include_directories(${THREADS_INCLUDE_DIRS})
-list(APPEND STORM_LINK_LIBRARIES ${CMAKE_THREAD_LIBS_INIT})
-if (STORM_USE_COTIRE)
-	target_link_libraries(storm_unity ${CMAKE_THREAD_LIBS_INIT})
-endif(STORM_USE_COTIRE)
-
-if (MSVC)
-	# Add the DebugHelper DLL
-	set(CMAKE_CXX_STANDARD_LIBRARIES "${CMAKE_CXX_STANDARD_LIBRARIES} Dbghelp.lib")
-	target_link_libraries(storm "Dbghelp.lib")
-endif(MSVC)
-
-#############################################################
-##
-##	CUDA Library generation
-##
-#############################################################
-
-
-if ("${CUDA_ROOT}" STREQUAL "")
-    set(ENABLE_CUDA OFF)
-else()
-    set(ENABLE_CUDA ON)
-endif()
-
-# CUDA Defines
-if (ENABLE_CUDA)
-	set(STORM_CPP_CUDA_DEF "define")
-else()
-	set(STORM_CPP_CUDA_DEF "undef")
-endif()
-
-
-# CUDA Defines
-set(STORM_CPP_CUDAFORSTORM_DEF "undef")
-
-
-if(ENABLE_CUDA)
-
-	# Test for type alignment
-	try_run(STORM_CUDA_RUN_RESULT_TYPEALIGNMENT STORM_CUDA_COMPILE_RESULT_TYPEALIGNMENT
-		${PROJECT_BINARY_DIR} "${PROJECT_SOURCE_DIR}/cuda/CMakeAlignmentCheck.cpp"
-		COMPILE_OUTPUT_VARIABLE OUTPUT_TEST_VAR
-	)
-	if(NOT STORM_CUDA_COMPILE_RESULT_TYPEALIGNMENT)
-		message(FATAL_ERROR "StoRM (CudaPlugin) - Could not test type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}")
-	elseif(STORM_CUDA_RUN_RESULT_TYPEALIGNMENT EQUAL 0)
-		message(STATUS "StoRM (CudaPlugin) - Result of Type Alignment Check: OK.")
-	else()
-		message(FATAL_ERROR "StoRM (CudaPlugin) - Result of Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_TYPEALIGNMENT})")
-	endif()
-
-	# Test for Float 64bit Alignment
-	try_run(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT STORM_CUDA_COMPILE_RESULT_FLOATALIGNMENT
-		${PROJECT_BINARY_DIR} "${PROJECT_SOURCE_DIR}/cuda/CMakeFloatAlignmentCheck.cpp"
-		COMPILE_OUTPUT_VARIABLE OUTPUT_TEST_VAR
-	)
-	if(NOT STORM_CUDA_COMPILE_RESULT_FLOATALIGNMENT)
-		message(FATAL_ERROR "StoRM (CudaPlugin) - Could not test float type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeFloatAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}")
-	elseif(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT EQUAL 2)
-		message(STATUS "StoRM (CudaPlugin) - Result of Float Type Alignment Check: 64bit alignment active.")
-		set(STORM_CUDAPLUGIN_FLOAT_64BIT_ALIGN_DEF "define")
-	elseif(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT EQUAL 3)
-		message(STATUS "StoRM (CudaPlugin) - Result of Float Type Alignment Check: 64bit alignment disabled.")
-		set(STORM_CUDAPLUGIN_FLOAT_64BIT_ALIGN_DEF "undef")
-	else()
-		message(FATAL_ERROR "StoRM (CudaPlugin) - Result of Float Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_FLOATALIGNMENT})")
-	endif()
-	#
-	# Make a version file containing the current version from git.
-	#
-	include(GetGitRevisionDescription)
-	git_describe_checkout(STORM_GIT_VERSION_STRING)
-	# Parse the git Tag into variables
-	string(REGEX REPLACE "^([0-9]+)\\..*" "\\1" STORM_CUDAPLUGIN_VERSION_MAJOR "${STORM_GIT_VERSION_STRING}")
-	string(REGEX REPLACE "^[0-9]+\\.([0-9]+).*" "\\1" STORM_CUDAPLUGIN_VERSION_MINOR "${STORM_GIT_VERSION_STRING}")
-	string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.([0-9]+).*" "\\1" STORM_CUDAPLUGIN_VERSION_PATCH "${STORM_GIT_VERSION_STRING}")
-	string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-([0-9]+)\\-.*" "\\1" STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD "${STORM_GIT_VERSION_STRING}")
-	string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-([a-z0-9]+).*" "\\1" STORM_CUDAPLUGIN_VERSION_HASH "${STORM_GIT_VERSION_STRING}")
-	string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-[a-z0-9]+\\-(.*)" "\\1" STORM_CUDAPLUGIN_VERSION_APPENDIX "${STORM_GIT_VERSION_STRING}")
-	if ("${STORM_CUDAPLUGIN_VERSION_APPENDIX}" MATCHES "^.*dirty.*$")
-		set(STORM_CUDAPLUGIN_VERSION_DIRTY 1)
-	else()
-		set(STORM_CUDAPLUGIN_VERSION_DIRTY 0)
-	endif()
-	message(STATUS "StoRM (CudaPlugin) - Version information: ${STORM_CUDAPLUGIN_VERSION_MAJOR}.${STORM_CUDAPLUGIN_VERSION_MINOR}.${STORM_CUDAPLUGIN_VERSION_PATCH} (${STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD} commits ahead of Tag) build from ${STORM_CUDAPLUGIN_VERSION_HASH} (Dirty: ${STORM_CUDAPLUGIN_VERSION_DIRTY})")
-
-
-	# Configure a header file to pass some of the CMake settings to the source code
-	configure_file (
-		"${PROJECT_SOURCE_DIR}/cuda/storm-cudaplugin-config.h.in"
-		"${PROJECT_BINARY_DIR}/include/storm-cudaplugin-config.h"
-	)
-
-	#create library
-	find_package(CUDA REQUIRED)
-	set(CUSP_INCLUDE_DIRS "${PROJECT_SOURCE_DIR}/resources/3rdparty/cusplibrary")
-	find_package(Cusp REQUIRED)
-	find_package(Thrust REQUIRED)
-
-	set(STORM_CUDA_LIB_NAME "storm-cuda")
-
-	file(GLOB_RECURSE STORM_CUDA_KERNEL_FILES ${PROJECT_SOURCE_DIR}/cuda/kernels/*.cu)
-	file(GLOB_RECURSE STORM_CUDA_HEADER_FILES ${PROJECT_SOURCE_DIR}/cuda/kernels/*.h)
-
-	source_group(kernels FILES ${STORM_CUDA_KERNEL_FILES} ${STORM_CUDA_HEADER_FILES})
-	include_directories(${PROJECT_SOURCE_DIR}/cuda/kernels/)
-
-	#set(CUDA_PROPAGATE_HOST_FLAGS OFF)
-	set(CUDA_NVCC_FLAGS "-arch=sm_30")
-
-	#############################################################
-	##
-	##	CUSP
-	##
-	#############################################################
-	if(CUSP_FOUND)
-		include_directories(${CUSP_INCLUDE_DIR})
-		cuda_include_directories(${CUSP_INCLUDE_DIR})
-		message(STATUS "StoRM (CudaPlugin) - Found CUSP Version ${CUSP_VERSION} in location ${CUSP_INCLUDE_DIR}")
-	else()
-		message(FATAL_ERROR "StoRM (CudaPlugin) - Could not find CUSP!")
-	endif()
-
-	#############################################################
-	##
-	##	Thrust
-	##
-	#############################################################
-	if(THRUST_FOUND)
-		include_directories(${THRUST_INCLUDE_DIR})
-		cuda_include_directories(${THRUST_INCLUDE_DIR})
-		message(STATUS "StoRM (CudaPlugin) - Found Thrust Version ${THRUST_VERSION} in location ${THRUST_INCLUDE_DIR}")
-	else()
-		message(FATAL_ERROR "StoRM (CudaPlugin) - Could not find Thrust! Check your CUDA installation.")
-	endif()
-
-	include_directories(${CUDA_INCLUDE_DIRS})
-	include_directories(${ADDITIONAL_INCLUDE_DIRS})
-
-	cuda_add_library(${STORM_CUDA_LIB_NAME}
-	    ${STORM_CUDA_KERNEL_FILES} ${STORM_CUDA_HEADER_FILES}
-	)
-
-        message (STATUS "StoRM - Linking with CUDA")
-        list(APPEND STORM_LINK_LIBRARIES ${STORM_CUDA_LIB_NAME})
-        include_directories("${PROJECT_SOURCE_DIR}/cuda/kernels/")
-endif()
 
 #############################################################
 ##
@@ -763,7 +282,7 @@ if(DOXYGEN_FOUND)
     set(CMAKE_DOXYGEN_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/doc")
     string(REGEX REPLACE ";" " " CMAKE_DOXYGEN_INPUT_LIST "${PROJECT_SOURCE_DIR}/src")
 
-    configure_file("${CMAKE_CURRENT_SOURCE_DIR}/doc/Doxyfile.in" "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" @ONLY)
+    configure_file("${CMAKE_CURRENT_SOURCE_DIR}/resources/doxygen/Doxyfile.in" "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" @ONLY)
 
     add_custom_target(doc ${DOXYGEN_EXECUTABLE} "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" DEPENDS "${CMAKE_CURRENT_BINARY_DIR}/Doxyfile" COMMENT "Generating API documentation with Doxygen" VERBATIM)
 endif(DOXYGEN_FOUND)
@@ -826,6 +345,6 @@ add_custom_target(memcheck-functional-tests valgrind --leak-check=full --show-re
 add_custom_target(memcheck-performance-tests valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm-performance-tests -v --fix-deadlocks DEPENDS storm-performance-tests)
 
 set(CPPLINT_ARGS --filter=-whitespace/tab,-whitespace/line_length,-legal/copyright,-readability/streams)
-add_custom_target(style python cpplint.py ${CPPLINT_ARGS} `find ./src/ -iname "*.h" -or -iname "*.cpp" `)
+add_custom_target(style python resources/3rdparty/cpplint/cpplint.py ${CPPLINT_ARGS} `find ./src/ -iname "*.h" -or -iname "*.cpp" `)
 
 include(StormCPackConfig.cmake)
diff --git a/README.md b/README.md
new file mode 100644
index 000000000..4a76de895
--- /dev/null
+++ b/README.md
@@ -0,0 +1 @@
+For more instructions, check out the documentation found in [Getting Started](doc/getting-started.md)
diff --git a/doc/build.md b/doc/build.md
new file mode 100644
index 000000000..23f2fc67e
--- /dev/null
+++ b/doc/build.md
@@ -0,0 +1,23 @@
+CMake >= 2.8.11
+ CMake is required as it is used to generate the Makefiles or Projects/Solutions required to build StoRM.
+
+ Compiler:
+ A C++11 compliant compiler is required to build StoRM. It is tested and known to work with the following compilers:
+ - GCC 5.0
+ - Clang 3.5.0
+
+ Other versions or compilers might work, but are not tested.
+
+ The following Compilers are known NOT to work: Microsoft Visual Studio versions older than 2013, GCC versions 4.7 and older.
+
+Prerequisites:
+ Boost >= 1.60
+	Build using the Boost Build system, for x64 use "bjam address-model=64" or "bjam.exe address-model=64 --build-type=complete"
+
+
+It is recommended to make an out-of-source build, meaning that the folder in which CMake generates its Cache, Makefiles and output files should not be the Project Root nor its Source Directory.
+A typical build layout is to create a folder "build" in the project root alongside the CMakeLists.txt file, change into this folder and execute "cmake .." as this will leave all source files untouched
+and makes cleaning up the build tree very easy.
+There are several options available for the CMake Script as to control behaviour and included components.
+If no error occured during the last CMake Configure round, press Generate.
+Now you can build StoRM using the generated project/makefiles in the Build folder you selected.
\ No newline at end of file
diff --git a/doc/dependencies.md b/doc/dependencies.md
new file mode 100644
index 000000000..9b4b5c290
--- /dev/null
+++ b/doc/dependencies.md
@@ -0,0 +1,41 @@
+
+
+
+ Included Dependencies:
+ Carl 1.0
+
+ CUDD  3.0.0
+ 	CUDD is included in the StoRM Sources under /resources/3rdparty/cudd-2.5.0 and builds automatically alongside StoRM.
+ 	Its Sourced where heavily modified as to incorporate newer Versions of Boost, changes in C++ (TR1 to C++11) and
+ 	to remove components only available under UNIX.
+
+ Eigen 3.3 beta1
+ 	Eigen is included in the StoRM Sources under /resources/3rdparty/eigen and builds automatically alongside StoRM.
+
+
+ GTest  1.7.0
+	GTest is included in the StoRM Sources under /resources/3rdparty/gtest-1.7.0 and builds automatically alongside StoRM
+ GMM >= 4.2
+	GMM is included in the StoRM Sources under /resources/3rdparty/gmm-4.2 and builds automatically alongside StoRM.
+
+
+Optional:
+ Gurobi >= 5.6.2
+	Specify the path to the gurobi root dir using -DGUROBI_ROOT=/your/path/to/gurobi
+ Z3 >= 4.3.2
+	Specify the path to the z3 root dir using -DZ3_ROOT=/your/path/to/z3
+MathSAT >= 5.2.11
+	Specify the path to the mathsat root dir using -DMSAT_ROOT=/your/path/to/mathsat
+MPIR >= 2.7.0
+	MSVC only and only if linked with MathSAT
+	Specify the path to the gmp-include directory -DGMP_INCLUDE_DIR=/your/path/to/mathsat
+	Specify the path to the mpir.lib directory -DGMP_MPIR_LIBRARY=/your/path/to/mpir.lib
+	Specify the path to the mpirxx.lib directory -DGMP_MPIRXX_LIBRARY=/your/path/to/mpirxx.lib
+GMP
+	clang and gcc only
+CUDA Toolkit >= 6.5
+	Specify the path to the cuda toolkit root dir using -DCUDA_ROOT=/your/path/to/cuda
+CUSP >= 0.4.0
+	Only of built with CUDA Toolkit
+	CUSP is included in the StoRM Sources as a git-submodule unter /resources/3rdparty/cusplibrary
+
diff --git a/doc/getting-started.md b/doc/getting-started.md
new file mode 100644
index 000000000..8b1378917
--- /dev/null
+++ b/doc/getting-started.md
@@ -0,0 +1 @@
+
diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index 4192a5e8e..471a1f5c1 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -1,96 +1,555 @@
 add_custom_target(resources)
 add_custom_target(test-resources)
 
-ExternalProject_Add(
-    xercesc
-    SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/xercesc-3.1.2
-    CONFIGURE_COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/xercesc-3.1.2/configure --prefix=${CMAKE_CURRENT_BINARY_DIR}/xercesc-3.1.2 --libdir=${CMAKE_CURRENT_BINARY_DIR}/xercesc-3.1.2/lib CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} CFLAGS=-O3 CXXFLAGS=-O3
-    PREFIX ${CMAKE_CURRENT_BINARY_DIR}/xercesc-3.1.2
-    BUILD_COMMAND make
-    BUILD_IN_SOURCE 0
-    LOG_CONFIGURE ON
-    LOG_BUILD ON
-    LOG_INSTALL ON
-)
+set(STORM_3RDPARTY_SOURCE_DIR ${PROJECT_SOURCE_DIR}/resources/3rdparty)
+set(STORM_3RDPARTY_BINARY_DIR ${PROJECT_BINARY_DIR}/resources/3rdparty)
+
+####
+#### Find autoreconf for cudd update step
+find_program(AUTORECONF autoreconf)
+mark_as_advanced(AUTORECONF)
+
+#############################################################
+##
+##	l3pp
+##
+#############################################################
+
 
-ExternalProject_Add(
-    glpk
-    DOWNLOAD_COMMAND ""
-    PREFIX ${CMAKE_CURRENT_BINARY_DIR}/glpk-4.57
-    SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/glpk-4.57
-    CONFIGURE_COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/glpk-4.57/configure --prefix=${CMAKE_CURRENT_BINARY_DIR}/glpk-4.57  --libdir=${CMAKE_CURRENT_BINARY_DIR}/glpk-4.57/lib CC=${CMAKE_C_COMPILER}
-    BUILD_COMMAND make "CFLAGS=-O2 -w"
-    INSTALL_COMMAND make install
-    BUILD_IN_SOURCE 0
-    LOG_CONFIGURE ON
-    LOG_BUILD ON
-    LOG_INSTALL ON
-)
 
 ExternalProject_Add(
-    cudd3
-    DOWNLOAD_COMMAND ""
-    SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/cudd-3.0.0
-    PREFIX ${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0
-    UPDATE_COMMAND autoreconf
-    CONFIGURE_COMMAND ${CMAKE_CURRENT_SOURCE_DIR}/cudd-3.0.0/configure  --enable-shared   --enable-obj --prefix=${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0 --libdir=${CMAKE_CURRENT_BINARY_DIR}/cudd-3.0.0/lib CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER}
-    BUILD_COMMAND make "CFLAGS=-O2 -w"
-    INSTALL_COMMAND make install
-    BUILD_IN_SOURCE 0
-    LOG_CONFIGURE ON
-    LOG_BUILD ON
-    LOG_INSTALL ON
+        l3pp
+        GIT_REPOSITORY https://github.com/hbruintjes/l3pp.git
+        GIT_TAG master
+        SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/l3pp
+        CONFIGURE_COMMAND ""
+        BUILD_COMMAND ""
+        INSTALL_COMMAND ""
+        LOG_INSTALL ON
 )
+ExternalProject_Get_Property(l3pp source_dir)
+set(l3pp_INCLUDE "${source_dir}/")
+include_directories(${l3pp_INCLUDE})
+add_dependencies(resources l3pp)
+
+#############################################################
+##
+##	gmm
+##
+#############################################################
+
+# Add the shipped version of GMM to the include pathes
+set(GMMXX_INCLUDE_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/gmm-5.0/include")
+include_directories(${GMMXX_INCLUDE_DIR})
+
+#############################################################
+##
+##	Eigen
+##
+#############################################################
+
+# Add the shipped version of Eigen to the include pathes
+set(EIGEN_INCLUDE_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/eigen-3.3-beta1")
+include_directories(${EIGEN_INCLUDE_DIR})
+
+
+#############################################################
+##
+##	Boost
+##
+#############################################################
+
+# Boost Option variables
+set(Boost_USE_STATIC_LIBS        ${USE_BOOST_STATIC_LIBRARIES})
+set(Boost_USE_MULTITHREADED      ON)
+set(Boost_USE_STATIC_RUNTIME    OFF)
+
+find_package(Boost 1.57.0 QUIET REQUIRED)
+
+if ((NOT Boost_LIBRARY_DIRS) OR ("${Boost_LIBRARY_DIRS}" STREQUAL ""))
+    set(Boost_LIBRARY_DIRS "${Boost_INCLUDE_DIRS}/stage/lib")
+endif ()
+link_directories(${Boost_LIBRARY_DIRS})
+
+include_directories(${Boost_INCLUDE_DIRS})
+list(APPEND STORM_LINK_LIBRARIES ${Boost_LIBRARIES})
+message(STATUS "StoRM - Using Boost ${Boost_VERSION} (lib ${Boost_LIB_VERSION})")
+#message(STATUS "StoRM - BOOST_INCLUDE_DIRS is ${Boost_INCLUDE_DIRS}")
+#message(STATUS "StoRM - BOOST_LIBRARY_DIRS is ${Boost_LIBRARY_DIRS}")
+
+#############################################################
+##
+##	ExprTk
+##
+#############################################################
+
+# Use the shipped version of ExprTK
+message (STATUS "StoRM - Including ExprTk")
+include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/exprtk")
+
+#############################################################
+##
+##	ModernJSON
+##
+#############################################################
+
+#use the shipped version of modernjson
+message (STATUS "StoRM - Including ModernJSON")
+include_directories("${PROJECT_SOURCE_DIR}/resources/3rdparty/modernjson/src/")
+
+#############################################################
+##
+##	Z3 (optional)
+##
+#############################################################
+
+find_package(Z3 QUIET)
+
+# Z3 Defines
+set(STORM_HAVE_Z3 ${Z3_FOUND})
+
+if(Z3_FOUND)
+    message (STATUS "StoRM - Linking with Z3")
+    include_directories(${Z3_INCLUDE_DIRS})
+    list(APPEND STORM_LINK_LIBRARIES ${Z3_LIBRARIES})
+endif(Z3_FOUND)
+
+#############################################################
+##
+##	glpk
+##
+#############################################################
+
+include(${STORM_3RDPARTY_SOURCE_DIR}/include_glpk.cmake)
+
+#############################################################
+##
+##	Gurobi (optional)
+##
+#############################################################
+
+if (STORM_USE_GUROBI)
+    find_package(Gurobi QUIET REQUIRED)
+    set(STORM_HAVE_GUROBI ${GUROBI_FOUND})
+    if (GUROBI_FOUND)
+        message (STATUS "StoRM - Linking with Gurobi")
+        include_directories(${GUROBI_INCLUDE_DIRS})
+        list(APPEND STORM_LINK_LIBRARIES ${GUROBI_LIBRARY})
+        #link_directories("${GUROBI_ROOT}/lib")
+    else()
+        #message(FATAL_ERROR "StoRM - Gurobi was requested, but not found!")
+    endif()
+else()
+    set(STORM_HAVE_GUROBI OFF)
+endif()
+
+#############################################################
+##
+##	CUDD
+##
+#############################################################
+include(${STORM_3RDPARTY_SOURCE_DIR}/include_cudd.cmake)
+
+#############################################################
+##
+##      CLN
+##
+#############################################################
+
+find_package(CLN QUIET)
+
+if(CLN_FOUND)
+    set(STORM_HAVE_CLN ON)
+    message(STATUS "StoRM - Linking with CLN ${CLN_VERSION_STRING}")
+    include_directories("${CLN_INCLUDE_DIR}")
+    list(APPEND STORM_LINK_LIBRARIES ${CLN_LIBRARIES})
+else()
+    set(STORM_HAVE_CLN OFF)
+    if(NOT GMP_FOUND)
+        message(FATAL_ERROR "StoRM - Neither CLN nor GMP found")
+    endif()
+endif()
+
+#############################################################
+##
+##      carl
+##
+#############################################################
+
+set(STORM_HAVE_CARL OFF)
+if(USE_CARL)
+    find_package(carl QUIET)
+    if(carl_FOUND)
+        set(STORM_HAVE_CARL ON)
+        message(STATUS "StoRM - Use system version of carl")
+        message(STATUS "StoRM - Linking with carl ${carl_VERSION_STRING}")
+        include_directories("${carl_INCLUDE_DIR}")
+        list(APPEND STORM_LINK_LIBRARIES ${carl_LIBRARIES})
+    else()
+        message(STATUS "StoRM - Using shipped version of carl")
+        #
+        ExternalProject_Add(
+                carl
+                GIT_REPOSITORY https://github.com/smtrat/carl
+                GIT_TAG master
+                INSTALL_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl
+                SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/carl
+                CMAKE_ARGS -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DEXPORT_TO_CMAKE=0 -DUSE_CLN_NUMBERS=1 -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=1 -DCMAKE_INSTALL_PREFIX:PATH=${STORM_3RDPARTY_BINARY_DIR}/carl
+                BUILD_IN_SOURCE 0
+                BUILD_COMMAND make lib_carl
+                INSTALL_COMMAND make install
+                LOG_UPDATE ON
+                LOG_CONFIGURE ON
+                LOG_BUILD ON
+                LOG_INSTALL ON
+        )
+
+        add_dependencies(resources xercesc)
+        include_directories(${STORM_3RDPARTY_BINARY_DIR}/carl/include)
+        list(APPEND STORM_LINK_LIBRARIES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT})
+        set(STORM_HAVE_CARL ON)
+    endif()
+endif()
+
+#############################################################
+##
+##      SMT-RAT
+##
+#############################################################
+
+# No find routine yet
+#find_package(smtrat QUIET)
+# Not yet supported
+set(smtrat_FOUND OFF)
+set(STORM_HAVE_SMTRAT OFF)
+if(smtrat_FOUND)
+    set(STORM_HAVE_SMTRAT ON)
+    message(STATUS "StoRM - Linking with smtrat.")
+    include_directories("${smtrat_INCLUDE_DIR}")
+    list(APPEND STORM_LINK_LIBRARIES ${smtrat_LIBRARIES})
+endif()
+
+#############################################################
+##
+##      GiNaC
+##
+#############################################################
+
+find_package(GiNaC QUIET)
+
+if(GINAC_FOUND)
+    set(STORM_HAVE_GINAC ON)
+    message(STATUS "StoRM - Linking with GiNaC ${GINAC_VERSION_STRING}")
+    # Right now only link with GiNaC for carl
+    #include_directories("${GINAC_INCLUDE_DIR}")
+    list(APPEND STORM_LINK_LIBRARIES ${GINAC_LIBRARIES})
+else()
+    set(STORM_HAVE_GINAC OFF)
+    #TODO: Check if CARL actually requires the use of GiNaC
+endif()
+
+
+#############################################################
+##
+##	gmp
+##
+#############################################################
+
+# GMP is optional (unless MathSAT is used, see below)
+find_package(GMP QUIET)
+
+#############################################################
+##
+##	MathSAT (optional)
+##
+#############################################################
+
+if ("${MSAT_ROOT}" STREQUAL "")
+    set(ENABLE_MSAT OFF)
+else()
+    set(ENABLE_MSAT ON)
+endif()
+
+# MathSAT Defines
+set(STORM_HAVE_MSAT ${ENABLE_MSAT})
+if (ENABLE_MSAT)
+    message (STATUS "StoRM - Linking with MathSAT")
+    link_directories("${MSAT_ROOT}/lib")
+    include_directories("${MSAT_ROOT}/include")
+    list(APPEND STORM_LINK_LIBRARIES "mathsat")
+    if(GMP_FOUND)
+        include_directories("${GMP_INCLUDE_DIR}")
+        list(APPEND STORM_LINK_LIBRARIES "gmp")
+    elseif(MPIR_FOUND)
+        include_directories("${GMP_INCLUDE_DIR}")
+        list(APPEND STORM_LINK_LIBRARIES "mpir" "mpirxx")
+    else(GMP_FOUND)
+        message(FATAL_ERROR "GMP is required for MathSAT, but was not found!")
+    endif(GMP_FOUND)
+endif(ENABLE_MSAT)
+
+#############################################################
+##
+##	Xerces
+##
+#############################################################
+
+include(${STORM_3RDPARTY_SOURCE_DIR}/include_xerces.cmake)
+
+#############################################################
+##
+##	Sylvan
+##
+#############################################################
 
 ExternalProject_Add(
-    sylvan
-    DOWNLOAD_COMMAND ""
-    PREFIX "sylvan"
-    SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/sylvan
-    CMAKE_ARGS -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=On -DCMAKE_BUILD_TYPE=Release
-    BINARY_DIR "${PROJECT_BINARY_DIR}/sylvan"
-    INSTALL_COMMAND ""
-    INSTALL_DIR "${PROJECT_BINARY_DIR}/sylvan"
+        sylvan
+        DOWNLOAD_COMMAND ""
+        PREFIX "sylvan"
+        SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/sylvan
+        CMAKE_ARGS -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DSYLVAN_BUILD_TEST=Off -DSYLVAN_BUILD_EXAMPLES=Off -DCMAKE_BUILD_TYPE=Release
+        BINARY_DIR "${PROJECT_BINARY_DIR}/sylvan"
+        BUILD_IN_SOURCE 0
+        INSTALL_COMMAND ""
+        INSTALL_DIR "${STORM_3RDPARTY_BINARY_DIR}/sylvan"
+        LOG_CONFIGURE ON
+        LOG_BUILD ON
 )
 ExternalProject_Get_Property(sylvan source_dir)
 ExternalProject_Get_Property(sylvan binary_dir)
-set(Sylvan_INCLUDE_DIR "${source_dir}/src" PARENT_SCOPE)
-set(Sylvan_LIBRARY "${binary_dir}/src/libsylvan.a" PARENT_SCOPE)
+set(Sylvan_INCLUDE_DIR "${source_dir}/src")
+set(Sylvan_LIBRARY "${binary_dir}/src/libsylvan.a")
+
+
 
+message(STATUS "StoRM - Using shipped version of sylvan")
+message(STATUS "StoRM - Linking with sylvan")
+include_directories("${Sylvan_INCLUDE_DIR}")
+list(APPEND STORM_LINK_LIBRARIES ${Sylvan_LIBRARY})
+add_dependencies(resources sylvan)
+
+if(${OPERATING_SYSTEM} MATCHES "Linux")
+    find_package(Hwloc QUIET REQUIRED)
+    if(Hwloc_FOUND)
+        message(STATUS "StoRM - Linking with hwloc ${Hwloc_VERSION}")
+        list(APPEND STORM_LINK_LIBRARIES ${Hwloc_LIBRARIES})
+    else()
+        message(FATAL_ERROR "HWLOC is required but was not found.")
+    endif()
+endif()
+
+#############################################################
+##
+##	Google Test gtest
+##
+#############################################################
 ExternalProject_Add(
         googletest
         #For downloads (may be useful later!)
         #SVN_REPOSITORY http://googletest.googlecode.com/svn/trunk/
         #TIMEOUT 10
         DOWNLOAD_COMMAND ""
-        SOURCE_DIR "${CMAKE_CURRENT_SOURCE_DIR}/gtest-1.7.0"
+        SOURCE_DIR "${STORM_3RDPARTY_SOURCE_DIR}/gtest-1.7.0"
         # Force the same output paths for debug and release builds so that
         # we know in which place the binaries end up when using the Xcode generator
-        CMAKE_ARGS  -Dgtest_force_shared_crt=ON -DCXX=${CMAKE_CXX_COMPILER} -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_DEBUG:PATH=${CMAKE_CURRENT_BINARY_DIR}/gtest-1.7.0 -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_RELEASE:PATH=${CMAKE_CURRENT_BINARY_DIR}/gtest-1.7.0 
+        CMAKE_ARGS  -Dgtest_force_shared_crt=ON -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_DEBUG:PATH=${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0 -DCMAKE_ARCHIVE_OUTPUT_DIRECTORY_RELEASE:PATH=${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0
         # Disable install step
         INSTALL_COMMAND ""
-        BINARY_DIR "${CMAKE_CURRENT_BINARY_DIR}/gtest-1.7.0"
-        INSTALL_DIR "${CMAKE_CURRENT_BINARY_DIR}/gtest-1.7.0"
+        BINARY_DIR "${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0"
+        INSTALL_DIR "${STORM_3RDPARTY_BINARY_DIR}/gtest-1.7.0"
         # Wrap download, configure and build steps in a script to log output
         LOG_CONFIGURE ON
         LOG_BUILD ON)
 
 # Specify include dir
 ExternalProject_Get_Property(googletest source_dir)
-set(GTEST_INCLUDE_DIR ${source_dir}/include PARENT_SCOPE)
+set(GTEST_INCLUDE_DIR ${source_dir}/include)
 # Specify MainTest's link libraries
 ExternalProject_Get_Property(googletest binary_dir)
-set(GTEST_LIBRARIES ${binary_dir}/libgtest.a ${binary_dir}/libgtest_main.a PARENT_SCOPE)
+set(GTEST_LIBRARIES ${binary_dir}/libgtest.a ${binary_dir}/libgtest_main.a)
 
-ExternalProject_Add(
-    l3pp
-    GIT_REPOSITORY https://github.com/hbruintjes/l3pp.git
-    GIT_TAG master
-    SOURCE_DIR ${CMAKE_CURRENT_SOURCE_DIR}/l3pp
-    CONFIGURE_COMMAND ""
-    BUILD_COMMAND ""
-    INSTALL_COMMAND ""
-    LOG_INSTALL ON
-)
-ExternalProject_Get_Property(l3pp source_dir)
-set(l3pp_INCLUDE "${source_dir}/" PARENT_SCOPE)
+add_dependencies(test-resources googletest)
+list(APPEND STORM_TEST_LINK_LIBRARIES ${GTEST_LIBRARIES})
+
+#############################################################
+##
+##	Intel Threading Building Blocks (optional)
+##
+#############################################################
+
+set(STORM_HAVE_INTELTBB OFF)
+if (STORM_USE_INTELTBB)
+    # Point to shipped TBB directory
+    set(TBB_INSTALL_DIR "${PROJECT_SOURCE_DIR}/resources/3rdparty/tbb42_20140122_merged-win-lin-mac")
+    find_package(TBB QUIET REQUIRED)
+
+    if (TBB_FOUND)
+        message(STATUS "StoRM - Found Intel TBB with interface version ${TBB_INTERFACE_VERSION}.")
+        message(STATUS "StoRM - Linking with Intel TBB in ${TBB_LIBRARY_DIRS}.")
+        set(STORM_HAVE_INTELTBB ON)
+        link_directories(${TBB_LIBRARY_DIRS})
+        include_directories(${TBB_INCLUDE_DIRS})
+        list(APPEND STORM_LINK_LIBRARIES tbb tbbmalloc)
+    else(TBB_FOUND)
+        message(FATAL_ERROR "StoRM - TBB was requested, but not found!")
+    endif(TBB_FOUND)
+endif(STORM_USE_INTELTBB)
+
+#############################################################
+##
+##	Threads
+##
+#############################################################
+
+find_package(Threads QUIET REQUIRED)
+if (NOT Threads_FOUND)
+    message(FATAL_ERROR "StoRM - Threads was requested, but not found!")
+endif()
+include_directories(${THREADS_INCLUDE_DIRS})
+list(APPEND STORM_LINK_LIBRARIES ${CMAKE_THREAD_LIBS_INIT})
+if (STORM_USE_COTIRE)
+    target_link_libraries(storm_unity ${CMAKE_THREAD_LIBS_INIT})
+endif(STORM_USE_COTIRE)
+
+if (MSVC)
+    # Add the DebugHelper DLL
+    set(CMAKE_CXX_STANDARD_LIBRARIES "${CMAKE_CXX_STANDARD_LIBRARIES} Dbghelp.lib")
+    target_link_libraries(storm "Dbghelp.lib")
+endif(MSVC)
+
+#############################################################
+##
+##	CUDA Library generation
+##
+#############################################################
+
+
+if ("${CUDA_ROOT}" STREQUAL "")
+    set(ENABLE_CUDA OFF)
+else()
+    set(ENABLE_CUDA ON)
+endif()
+
+# CUDA Defines
+if (ENABLE_CUDA)
+    set(STORM_CPP_CUDA_DEF "define")
+else()
+    set(STORM_CPP_CUDA_DEF "undef")
+endif()
+
+
+# CUDA Defines
+set(STORM_CPP_CUDAFORSTORM_DEF "undef")
+
+
+if(ENABLE_CUDA)
+
+    # Test for type alignment
+    try_run(STORM_CUDA_RUN_RESULT_TYPEALIGNMENT STORM_CUDA_COMPILE_RESULT_TYPEALIGNMENT
+            ${PROJECT_BINARY_DIR} "${PROJECT_SOURCE_DIR}/cuda/CMakeAlignmentCheck.cpp"
+            COMPILE_OUTPUT_VARIABLE OUTPUT_TEST_VAR
+            )
+    if(NOT STORM_CUDA_COMPILE_RESULT_TYPEALIGNMENT)
+        message(FATAL_ERROR "StoRM (CudaPlugin) - Could not test type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}")
+    elseif(STORM_CUDA_RUN_RESULT_TYPEALIGNMENT EQUAL 0)
+        message(STATUS "StoRM (CudaPlugin) - Result of Type Alignment Check: OK.")
+    else()
+        message(FATAL_ERROR "StoRM (CudaPlugin) - Result of Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_TYPEALIGNMENT})")
+    endif()
+
+    # Test for Float 64bit Alignment
+    try_run(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT STORM_CUDA_COMPILE_RESULT_FLOATALIGNMENT
+            ${PROJECT_BINARY_DIR} "${PROJECT_SOURCE_DIR}/cuda/CMakeFloatAlignmentCheck.cpp"
+            COMPILE_OUTPUT_VARIABLE OUTPUT_TEST_VAR
+            )
+    if(NOT STORM_CUDA_COMPILE_RESULT_FLOATALIGNMENT)
+        message(FATAL_ERROR "StoRM (CudaPlugin) - Could not test float type alignment, there was an Error while compiling the file ${PROJECT_SOURCE_DIR}/cuda/CMakeFloatAlignmentCheck.cpp: ${OUTPUT_TEST_VAR}")
+    elseif(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT EQUAL 2)
+        message(STATUS "StoRM (CudaPlugin) - Result of Float Type Alignment Check: 64bit alignment active.")
+        set(STORM_CUDAPLUGIN_FLOAT_64BIT_ALIGN_DEF "define")
+    elseif(STORM_CUDA_RUN_RESULT_FLOATALIGNMENT EQUAL 3)
+        message(STATUS "StoRM (CudaPlugin) - Result of Float Type Alignment Check: 64bit alignment disabled.")
+        set(STORM_CUDAPLUGIN_FLOAT_64BIT_ALIGN_DEF "undef")
+    else()
+        message(FATAL_ERROR "StoRM (CudaPlugin) - Result of Float Type Alignment Check: FAILED (Code ${STORM_CUDA_RUN_RESULT_FLOATALIGNMENT})")
+    endif()
+    #
+    # Make a version file containing the current version from git.
+    #
+    include(GetGitRevisionDescription)
+    git_describe_checkout(STORM_GIT_VERSION_STRING)
+    # Parse the git Tag into variables
+    string(REGEX REPLACE "^([0-9]+)\\..*" "\\1" STORM_CUDAPLUGIN_VERSION_MAJOR "${STORM_GIT_VERSION_STRING}")
+    string(REGEX REPLACE "^[0-9]+\\.([0-9]+).*" "\\1" STORM_CUDAPLUGIN_VERSION_MINOR "${STORM_GIT_VERSION_STRING}")
+    string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.([0-9]+).*" "\\1" STORM_CUDAPLUGIN_VERSION_PATCH "${STORM_GIT_VERSION_STRING}")
+    string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-([0-9]+)\\-.*" "\\1" STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD "${STORM_GIT_VERSION_STRING}")
+    string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-([a-z0-9]+).*" "\\1" STORM_CUDAPLUGIN_VERSION_HASH "${STORM_GIT_VERSION_STRING}")
+    string(REGEX REPLACE "^[0-9]+\\.[0-9]+\\.[0-9]+\\-[0-9]+\\-[a-z0-9]+\\-(.*)" "\\1" STORM_CUDAPLUGIN_VERSION_APPENDIX "${STORM_GIT_VERSION_STRING}")
+    if ("${STORM_CUDAPLUGIN_VERSION_APPENDIX}" MATCHES "^.*dirty.*$")
+        set(STORM_CUDAPLUGIN_VERSION_DIRTY 1)
+    else()
+        set(STORM_CUDAPLUGIN_VERSION_DIRTY 0)
+    endif()
+    message(STATUS "StoRM (CudaPlugin) - Version information: ${STORM_CUDAPLUGIN_VERSION_MAJOR}.${STORM_CUDAPLUGIN_VERSION_MINOR}.${STORM_CUDAPLUGIN_VERSION_PATCH} (${STORM_CUDAPLUGIN_VERSION_COMMITS_AHEAD} commits ahead of Tag) build from ${STORM_CUDAPLUGIN_VERSION_HASH} (Dirty: ${STORM_CUDAPLUGIN_VERSION_DIRTY})")
+
+
+    # Configure a header file to pass some of the CMake settings to the source code
+    configure_file (
+            "${PROJECT_SOURCE_DIR}/cuda/storm-cudaplugin-config.h.in"
+            "${PROJECT_BINARY_DIR}/include/storm-cudaplugin-config.h"
+    )
+
+    #create library
+    find_package(CUDA REQUIRED)
+    set(CUSP_INCLUDE_DIRS "${PROJECT_SOURCE_DIR}/resources/3rdparty/cusplibrary")
+    find_package(Cusp REQUIRED)
+    find_package(Thrust REQUIRED)
+
+    set(STORM_CUDA_LIB_NAME "storm-cuda")
+
+    file(GLOB_RECURSE STORM_CUDA_KERNEL_FILES ${PROJECT_SOURCE_DIR}/cuda/kernels/*.cu)
+    file(GLOB_RECURSE STORM_CUDA_HEADER_FILES ${PROJECT_SOURCE_DIR}/cuda/kernels/*.h)
+
+    source_group(kernels FILES ${STORM_CUDA_KERNEL_FILES} ${STORM_CUDA_HEADER_FILES})
+    include_directories(${PROJECT_SOURCE_DIR}/cuda/kernels/)
+
+    #set(CUDA_PROPAGATE_HOST_FLAGS OFF)
+    set(CUDA_NVCC_FLAGS "-arch=sm_30")
+
+    #############################################################
+    ##
+    ##	CUSP
+    ##
+    #############################################################
+    if(CUSP_FOUND)
+        include_directories(${CUSP_INCLUDE_DIR})
+        cuda_include_directories(${CUSP_INCLUDE_DIR})
+        message(STATUS "StoRM (CudaPlugin) - Found CUSP Version ${CUSP_VERSION} in location ${CUSP_INCLUDE_DIR}")
+    else()
+        message(FATAL_ERROR "StoRM (CudaPlugin) - Could not find CUSP!")
+    endif()
+
+    #############################################################
+    ##
+    ##	Thrust
+    ##
+    #############################################################
+    if(THRUST_FOUND)
+        include_directories(${THRUST_INCLUDE_DIR})
+        cuda_include_directories(${THRUST_INCLUDE_DIR})
+        message(STATUS "StoRM (CudaPlugin) - Found Thrust Version ${THRUST_VERSION} in location ${THRUST_INCLUDE_DIR}")
+    else()
+        message(FATAL_ERROR "StoRM (CudaPlugin) - Could not find Thrust! Check your CUDA installation.")
+    endif()
+
+    include_directories(${CUDA_INCLUDE_DIRS})
+    include_directories(${ADDITIONAL_INCLUDE_DIRS})
+
+    cuda_add_library(${STORM_CUDA_LIB_NAME}
+            ${STORM_CUDA_KERNEL_FILES} ${STORM_CUDA_HEADER_FILES}
+            )
+
+    message (STATUS "StoRM - Linking with CUDA")
+    list(APPEND STORM_LINK_LIBRARIES ${STORM_CUDA_LIB_NAME})
+    include_directories("${PROJECT_SOURCE_DIR}/cuda/kernels/")
+endif()
diff --git a/resources/3rdparty/carl b/resources/3rdparty/carl
new file mode 160000
index 000000000..d67f98622
--- /dev/null
+++ b/resources/3rdparty/carl
@@ -0,0 +1 @@
+Subproject commit d67f986226cf846ba6366cdbe2abc21dff375542
diff --git a/cpplint.py b/resources/3rdparty/cpplint/cpplint.py
similarity index 100%
rename from cpplint.py
rename to resources/3rdparty/cpplint/cpplint.py
diff --git a/resources/3rdparty/include_cudd.cmake b/resources/3rdparty/include_cudd.cmake
new file mode 100644
index 000000000..d63e855d3
--- /dev/null
+++ b/resources/3rdparty/include_cudd.cmake
@@ -0,0 +1,31 @@
+if(NOT AUTORECONF)
+    message(ERROR "Cannot find autoreconf, cannot compile cudd3")
+endif()
+
+
+ExternalProject_Add(
+        cudd3
+        DOWNLOAD_COMMAND ""
+        SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/cudd-3.0.0
+        PREFIX ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0
+        UPDATE_COMMAND ${AUTORECONF}
+        CONFIGURE_COMMAND ${STORM_3RDPARTY_SOURCE_DIR}/cudd-3.0.0/configure  --enable-shared   --enable-obj --prefix=${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0 --libdir=${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0/lib CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER}
+        BUILD_COMMAND make "CFLAGS=-O2 -w"
+        INSTALL_COMMAND make install
+        BUILD_IN_SOURCE 0
+        LOG_CONFIGURE ON
+        LOG_BUILD ON
+        LOG_INSTALL ON
+)
+
+# Do not use system CUDD, StoRM has a modified version
+set(CUDD_INCLUDE_DIR ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0/include)
+set(CUDD_SHARED_LIBRARY ${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0/lib/libcudd${DYNAMIC_EXT})
+set(CUDD_STATIC_LIBRARY $${STORM_3RDPARTY_BINARY_DIR}/cudd-3.0.0/cudd-3.0.0/lib/libcudd${STATIC_EXT})
+set(CUDD_VERSION_STRING 3.0.0)
+list(APPEND STORM_LINK_LIBRARIES ${CUDD_SHARED_LIBRARY})
+add_dependencies(resources cudd3)
+
+message(STATUS "StoRM - Linking with CUDD ${CUDD_VERSION_STRING}")
+#message("StoRM - CUDD include dir: ${CUDD_INCLUDE_DIR}")
+include_directories(${CUDD_INCLUDE_DIR})
\ No newline at end of file
diff --git a/resources/3rdparty/include_glpk.cmake b/resources/3rdparty/include_glpk.cmake
new file mode 100644
index 000000000..2ac870b3d
--- /dev/null
+++ b/resources/3rdparty/include_glpk.cmake
@@ -0,0 +1,28 @@
+find_package(GLPK QUIET)
+if(GLPK_FOUND)
+    message (STATUS "StoRM - Using system version of GLPK")
+else()
+    message (STATUS "StoRM - Using shipped version of GLPK")
+    ExternalProject_Add(glpk
+        DOWNLOAD_COMMAND ""
+        PREFIX ${STORM_3RDPARTY_BINARY_DIR}/glpk-4.57
+        SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/glpk-4.57
+        CONFIGURE_COMMAND ${STORM_3RDPARTY_SOURCE_DIR}/glpk-4.57/configure --prefix=${STORM_3RDPARTY_BINARY_DIR}/glpk-4.57  --libdir=${STORM_3RDPARTY_BINARY_DIR}/glpk-4.57/lib CC=${CMAKE_C_COMPILER}
+        BUILD_COMMAND make "CFLAGS=-O2 -w"
+        INSTALL_COMMAND make install
+        BUILD_IN_SOURCE 0
+        LOG_CONFIGURE ON
+        LOG_BUILD ON
+        LOG_INSTALL ON
+    )
+    set(GLPK_LIBRARIES  ${CMAKE_BINARY_DIR}/resources/3rdparty/glpk-4.57/lib/libglpk${DYNAMIC_EXT})
+    set(GLPK_INCLUDE_DIR ${CMAKE_BINARY_DIR}/resources/3rdparty/glpk-4.57/include)
+    set(GLPK_VERSION_STRING 4.57)
+    add_dependencies(resources glpk)
+endif()
+
+# Since there is a shipped version, always use GLPK
+set(STORM_HAVE_GLPK ON)
+message (STATUS "StoRM - Linking with glpk ${GLPK_VERSION_STRING}")
+include_directories(${GLPK_INCLUDE_DIR})
+list(APPEND STORM_LINK_LIBRARIES ${GLPK_LIBRARIES})
diff --git a/resources/3rdparty/include_xerces.cmake b/resources/3rdparty/include_xerces.cmake
new file mode 100644
index 000000000..73f559cec
--- /dev/null
+++ b/resources/3rdparty/include_xerces.cmake
@@ -0,0 +1,36 @@
+if(USE_XERCES)
+    find_package(Xerces QUIET REQUIRED)
+    if(XERCES_FOUND)
+        message(STATUS "StoRM - Use system version of xerces")
+    else()
+        message(STATUS "StoRM - Use shipped version of xerces")
+        ExternalProject_Add(
+                xercesc
+                SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/xercesc-3.1.2
+                CONFIGURE_COMMAND ${STORM_3RDPARTY_SOURCE_DIR}/xercesc-3.1.2/configure --prefix=${STORM_3RDPARTY_BINARY_DIR}/xercesc-3.1.2 --libdir=${STORM_3RDPARTY_BINARY_DIR}/xercesc-3.1.2/lib CC=${CMAKE_C_COMPILER} CXX=${CMAKE_CXX_COMPILER} CFLAGS=-O3 CXXFLAGS=-O3
+                PREFIX ${STORM_3RDPARTY_BINARY_DIR}/xercesc-3.1.2
+                BUILD_COMMAND make
+                BUILD_IN_SOURCE 0
+                LOG_CONFIGURE ON
+                LOG_BUILD ON
+                LOG_INSTALL ON
+        )
+
+        set(XERCES_ROOT ${STORM_3RDPARTY_BINARY_DIR}/xercesc-3.1.2)
+        set(XERCESC_INCLUDE ${XERCES_ROOT}/include)
+        set(XERCES_LIBRARY_PATH ${XERCES_ROOT}/lib)
+        set(XERCESC_LIBRARIES ${XERCES_LIBRARY_PATH}/libxerces-c.a)
+
+        add_dependencies(resources xercesc)
+    endif()
+
+    message (STATUS "StoRM - Linking with xercesc")
+    set(STORM_HAVE_XERCES ON)
+    include_directories(${XERCESC_INCLUDE})
+    if(APPLE)
+        FIND_LIBRARY(COREFOUNDATION_LIBRARY CoreFoundation )
+        FIND_LIBRARY(CORESERVICES_LIBRARY CoreServices )
+    endif()
+    find_package(CURL)
+    list(APPEND STORM_LINK_LIBRARIES ${XERCESC_LIBRARIES} ${COREFOUNDATION_LIBRARY} ${CORESERVICES_LIBRARY} ${CURL_LIBRARIES})
+endif(USE_XERCES)
diff --git a/resources/BUILD.txt b/resources/BUILD.txt
deleted file mode 100644
index 4057b110a..000000000
--- a/resources/BUILD.txt
+++ /dev/null
@@ -1,64 +0,0 @@
-CMake >= 2.8.11
- CMake is required as it is used to generate the Makefiles or Projects/Solutions required to build StoRM.
-
- Compiler:
- A C++11 compliant compiler is required to build StoRM. It is tested and known to work with the following compilers:
- - GCC 4.9.1
- - Clang 3.5.0
- - Microsoft Visual Studio 2013
- 
- Other versions or compilers might work, but are not tested.
- 
- The following Compilers are known NOT to work: Microsoft Visual Studio versions older than 2013, GCC versions 4.7 and older.
- 
-Prerequisites:
- Boost >= 1.56
-	Build using the Boost Build system, for x64 use "bjam address-model=64" or "bjam.exe address-model=64 --build-type=complete"
-	You may use --toolset to specify the compiler, for ex. msvc-10.0, intel11.1, etc
- Doxygen
-	Set DOXYGEN_EXECUTABLE to your doxygen executable, e.g. "C:/Program Files/doxygen/bin/doxygen.exe"
- GTest >= 1.7.0
-	GTest is included in the StoRM Sources under /resources/3rdparty/gtest-1.7.0 and builds automatically alongside StoRM
- CUDD >= 2.5.0
-	CUDD is included in the StoRM Sources under /resources/3rdparty/cudd-2.5.0 and builds automatically alongside StoRM. 
-	Its Sourced where heavily modified as to incorporate newer Versions of Boost, changes in C++ (TR1 to C++11) and
-	to remove components only available under UNIX.
- Log4CPlus >= 1.1.2
-	Log4CPlus is included in the StoRM Sources under /resources/3rdparty/log4cplus-1.1.3-rc1 and builds automatically alongside StoRM. 
-	Its Sourced where slightly modified as to incorporate Unicode handling under Win32, Clang compatability and shared/static build options.
- Eigen >= 3.2.1
-	Eigen is included in the StoRM Sources under /resources/3rdparty/eigen and builds automatically alongside StoRM.
- GMM >= 4.2
-	GMM is included in the StoRM Sources under /resources/3rdparty/gmm-4.2 and builds automatically alongside StoRM.
- LTL2DStar >= 0.5.1
-	LTL2DStar is included in the StoRM Sources under /resources/3rdparty/ltl2dstar-0.5.1 and builds automatically alongside StoRM. 
-	Its Sourced where heavily modified as to incorporate changes in C++ (TR1 to C++11) and
-	to remove components only available under UNIX.
-
-Optional:
- Gurobi >= 5.6.2
-	Specify the path to the gurobi root dir using -DGUROBI_ROOT=/your/path/to/gurobi
- Z3 >= 4.3.2
-	Specify the path to the z3 root dir using -DZ3_ROOT=/your/path/to/z3
-MathSAT >= 5.2.11
-	Specify the path to the mathsat root dir using -DMSAT_ROOT=/your/path/to/mathsat
-MPIR >= 2.7.0
-	MSVC only and only if linked with MathSAT 
-	Specify the path to the gmp-include directory -DGMP_INCLUDE_DIR=/your/path/to/mathsat
-	Specify the path to the mpir.lib directory -DGMP_MPIR_LIBRARY=/your/path/to/mpir.lib
-	Specify the path to the mpirxx.lib directory -DGMP_MPIRXX_LIBRARY=/your/path/to/mpirxx.lib
-GMP
-	clang and gcc only and inly if linked with MathSAT
-CUDA Toolkit >= 6.5
-	Specify the path to the cuda toolkit root dir using -DCUDA_ROOT=/your/path/to/cuda
-CUSP >= 0.4.0
-	Only of built with CUDA Toolkit
-	CUSP is included in the StoRM Sources as a git-submodule unter /resources/3rdparty/cusplibrary
-	
-	
-It is recommended to make an out-of-source build, meaning that the folder in which CMake generates its Cache, Makefiles and output files should not be the Project Root nor its Source Directory.
-A typical build layout is to create a folder "build" in the project root alongside the CMakeLists.txt file, change into this folder and execute "cmake .." as this will leave all source files untouched
-and makes cleaning up the build tree very easy.
-There are several options available for the CMake Script as to control behaviour and included components.
-If no error occured during the last CMake Configure round, press Generate. 
-Now you can build StoRM using the generated project/makefiles in the Build folder you selected.
\ No newline at end of file
diff --git a/doc/Doxyfile.in b/resources/doxygen/Doxyfile.in
similarity index 100%
rename from doc/Doxyfile.in
rename to resources/doxygen/Doxyfile.in
diff --git a/src/adapters/EigenAdapter.cpp b/src/adapters/EigenAdapter.cpp
index 350ca8e20..94964964b 100644
--- a/src/adapters/EigenAdapter.cpp
+++ b/src/adapters/EigenAdapter.cpp
@@ -21,7 +21,10 @@ namespace storm {
         }
         
         template std::unique_ptr<Eigen::SparseMatrix<double>> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix<double> const& matrix);
+
+#ifdef STORM_HAVE_CARL
         template std::unique_ptr<Eigen::SparseMatrix<storm::RationalNumber>> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix<storm::RationalNumber> const& matrix);
         template std::unique_ptr<Eigen::SparseMatrix<storm::RationalFunction>> EigenAdapter::toEigenSparseMatrix(storm::storage::SparseMatrix<storm::RationalFunction> const& matrix);
+#endif
     }
 }
diff --git a/src/builder/ExplicitModelBuilder.cpp b/src/builder/ExplicitModelBuilder.cpp
index bb62757a4..5faf386e5 100644
--- a/src/builder/ExplicitModelBuilder.cpp
+++ b/src/builder/ExplicitModelBuilder.cpp
@@ -412,9 +412,11 @@ namespace storm {
         
         // Explicitly instantiate the class.
         template class ExplicitModelBuilder<double, storm::models::sparse::StandardRewardModel<double>, uint32_t>;
+
+#ifdef STORM_HAVE_CARL
         template class ExplicitModelBuilder<RationalNumber, storm::models::sparse::StandardRewardModel<RationalNumber>, uint32_t>;
-        
-        template class ExplicitModelBuilder<double, storm::models::sparse::StandardRewardModel<storm::Interval>, uint32_t>;
         template class ExplicitModelBuilder<RationalFunction, storm::models::sparse::StandardRewardModel<RationalFunction>, uint32_t>;
+        template class ExplicitModelBuilder<double, storm::models::sparse::StandardRewardModel<storm::Interval>, uint32_t>;
+#endif
     }
 }
diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp
index 0c2e80f53..f71f71264 100644
--- a/src/cli/cli.cpp
+++ b/src/cli/cli.cpp
@@ -228,9 +228,17 @@ namespace storm {
                 }
                 
                 if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isParametricSet()) {
+#ifdef STORM_HAVE_CARL
                     buildAndCheckSymbolicModel<storm::RationalFunction>(preprocessedProgram, preprocessedFormulas, true);
+#else
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No parameters are supported in this build.");
+#endif
                 } else if (storm::settings::getModule<storm::settings::modules::GeneralSettings>().isExactSet()) {
+#ifdef STORM_HAVE_CARL
                     buildAndCheckSymbolicModel<storm::RationalNumber>(preprocessedProgram, preprocessedFormulas, true);
+#else
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "No exact numbers are supported in this build.");
+#endif
                 } else {
                     buildAndCheckSymbolicModel<double>(preprocessedProgram, preprocessedFormulas, true);
                 }
diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h
index c2990b072..ccd48e42b 100644
--- a/src/cli/entrypoints.h
+++ b/src/cli/entrypoints.h
@@ -224,6 +224,7 @@ namespace storm {
             }
         }
         
+#ifdef STORM_HAVE_CARL
         template<>
         void buildAndCheckSymbolicModel<storm::RationalNumber>(storm::prism::Program const& program, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant) {
             STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one.");
@@ -235,6 +236,7 @@ namespace storm {
             STORM_LOG_THROW(storm::settings::getModule<storm::settings::modules::CoreSettings>().getEngine() == storm::settings::modules::CoreSettings::Engine::Sparse, storm::exceptions::InvalidSettingsException, "Cannot use this data type with an engine different than the sparse one.");
             buildAndCheckSymbolicModelWithSparseEngine<storm::RationalFunction>(program, formulas, onlyInitialStatesRelevant);
         }
+#endif
         
         template<typename ValueType>
         void buildAndCheckExplicitModel(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas, bool onlyInitialStatesRelevant = false) {
diff --git a/src/generator/Choice.cpp b/src/generator/Choice.cpp
index 7a209ccc4..7f91a4b4d 100644
--- a/src/generator/Choice.cpp
+++ b/src/generator/Choice.cpp
@@ -100,7 +100,10 @@ namespace storm {
         }
         
         template class Choice<double>;
+
+#ifdef STORM_HAVE_CARL
         template class Choice<storm::RationalNumber>;
         template class Choice<storm::RationalFunction>;
+#endif
     }
-}
\ No newline at end of file
+}
diff --git a/src/generator/CompressedState.cpp b/src/generator/CompressedState.cpp
index 3a229112f..d7707d740 100644
--- a/src/generator/CompressedState.cpp
+++ b/src/generator/CompressedState.cpp
@@ -30,8 +30,11 @@ namespace storm {
         }
 
         template void unpackStateIntoEvaluator<double>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<double>& evaluator);
+        storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager);
+
+#ifdef STORM_HAVE_CARL
         template void unpackStateIntoEvaluator<storm::RationalNumber>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<storm::RationalNumber>& evaluator);
         template void unpackStateIntoEvaluator<storm::RationalFunction>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<storm::RationalFunction>& evaluator);
-        storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager);
+#endif
     }
-}
\ No newline at end of file
+}
diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp
index 9e0f10b7f..cfb08fb79 100644
--- a/src/generator/JaniNextStateGenerator.cpp
+++ b/src/generator/JaniNextStateGenerator.cpp
@@ -492,8 +492,10 @@ namespace storm {
         }
         
         template class JaniNextStateGenerator<double>;
+
+#ifdef STORM_HAVE_CARL
         template class JaniNextStateGenerator<storm::RationalNumber>;
         template class JaniNextStateGenerator<storm::RationalFunction>;
-        
+#endif
     }
-}
\ No newline at end of file
+}
diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp
index 54fb2f280..9c1eefbd5 100644
--- a/src/generator/NextStateGenerator.cpp
+++ b/src/generator/NextStateGenerator.cpp
@@ -28,7 +28,7 @@ namespace storm {
         }
         
         std::string const& LabelOrExpression::getLabel() const {
-            return boost::get<std::string const&>(labelOrExpression);
+            return boost::get<std::string>(labelOrExpression);
         }
         
         bool LabelOrExpression::isExpression() const {
@@ -36,7 +36,7 @@ namespace storm {
         }
         
         storm::expressions::Expression const& LabelOrExpression::getExpression() const {
-            return boost::get<storm::expressions::Expression const&>(labelOrExpression);
+            return boost::get<storm::expressions::Expression>(labelOrExpression);
         }
         
         NextStateGeneratorOptions::NextStateGeneratorOptions(bool buildAllRewardModels, bool buildAllLabels) : buildAllRewardModels(buildAllRewardModels), buildAllLabels(buildAllLabels), buildChoiceLabels(false) {
@@ -303,8 +303,10 @@ namespace storm {
         }
 
         template class NextStateGenerator<double>;
+
+#ifdef STORM_HAVE_CARL
         template class NextStateGenerator<storm::RationalNumber>;
         template class NextStateGenerator<storm::RationalFunction>;
-        
+#endif
     }
 }
diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp
index 552cd30a9..c0026a98d 100644
--- a/src/generator/PrismNextStateGenerator.cpp
+++ b/src/generator/PrismNextStateGenerator.cpp
@@ -77,7 +77,11 @@ namespace storm {
         template<typename ValueType, typename StateType>
         void PrismNextStateGenerator<ValueType, StateType>::checkValid(storm::prism::Program const& program) {
             // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.
+#ifdef STORM_HAVE_CARL
             if (!std::is_same<ValueType, storm::RationalFunction>::value && program.hasUndefinedConstants()) {
+#else
+            if (program.hasUndefinedConstants()) {
+#endif
                 std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = program.getUndefinedConstants();
                 std::stringstream stream;
                 bool printComma = false;
@@ -91,9 +95,13 @@ namespace storm {
                 }
                 stream << ".";
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
-            } else if (std::is_same<ValueType, storm::RationalFunction>::value && !program.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) {
+            }
+
+#ifdef STORM_HAVE_CARL
+            else if (std::is_same<ValueType, storm::RationalFunction>::value && !program.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted.");
             }
+#endif
         }
         
         template<typename ValueType, typename StateType>
@@ -561,7 +569,10 @@ namespace storm {
         }
                 
         template class PrismNextStateGenerator<double>;
+
+#ifdef STORM_HAVE_CARL
         template class PrismNextStateGenerator<storm::RationalNumber>;
         template class PrismNextStateGenerator<storm::RationalFunction>;
+#endif
     }
 }
diff --git a/src/generator/StateBehavior.cpp b/src/generator/StateBehavior.cpp
index 28e256c18..4e71c537f 100644
--- a/src/generator/StateBehavior.cpp
+++ b/src/generator/StateBehavior.cpp
@@ -56,8 +56,10 @@ namespace storm {
         }
         
         template class StateBehavior<double>;
+
+#ifdef STORM_HAVE_CARL
         template class StateBehavior<storm::RationalNumber>;
         template class StateBehavior<storm::RationalFunction>;
-
+#endif
     }
-}
\ No newline at end of file
+}
diff --git a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
index 4d2d8fbea..914b71cc1 100644
--- a/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
+++ b/src/modelchecker/csl/SparseCtmcCslModelChecker.cpp
@@ -140,8 +140,11 @@ namespace storm {
 
         // Explicitly instantiate the model checker.
         template class SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<double>>;
+
+#ifdef STORM_HAVE_CARL
         template class SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<storm::RationalNumber>>;
         template class SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<storm::RationalFunction>>;
-        
+#endif
+
     } // namespace modelchecker
 } // namespace storm
diff --git a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
index dab1449de..c51563507 100644
--- a/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
+++ b/src/modelchecker/csl/helper/SparseCtmcCslHelper.cpp
@@ -688,44 +688,61 @@ namespace storm {
             
             
             template std::vector<double> SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<double> const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
-            template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<storm::RationalNumber> const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
-            template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<storm::RationalFunction> const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
             
             template std::vector<double> SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, std::vector<double> const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
-            template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
-            template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
 
             template std::vector<double> SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
-            template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
-            template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
             
             template std::vector<double> SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
-            template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
-            template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalFunction> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
             
             template std::vector<double> SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, std::vector<double> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
-            template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
-            template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
             
             template std::vector<double> SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
-            template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
-            template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalFunction> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
             
             template std::vector<double> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<double> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<double> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
-            template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<storm::RationalNumber> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
-            template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<storm::RationalFunction> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
             
             template std::vector<double> SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRateVector, storm::models::sparse::StandardRewardModel<double> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
-            template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
-            template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalFunction> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
             
             template storm::storage::SparseMatrix<double> SparseCtmcCslHelper::computeUniformizedMatrix(storm::storage::SparseMatrix<double> const& rateMatrix, storm::storage::BitVector const& maybeStates, double uniformizationRate, std::vector<double> const& exitRates);
             
+            template std::vector<double> SparseCtmcCslHelper::computeTransientProbabilities(storm::storage::SparseMatrix<double> const& uniformizedMatrix, std::vector<double> const* addVector, double timeBound, double uniformizationRate, std::vector<double> values, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
+
+#ifdef STORM_HAVE_CARL
+            template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<storm::RationalNumber> const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
+            template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeBoundedUntilProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, std::vector<storm::RationalFunction> const& exitRates, bool qualitative, double lowerBound, double upperBound, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
+
+            template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
+            template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeUntilProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
+
+            template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
+            template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeNextProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& nextStates, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
+
+            template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
+            template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeInstantaneousRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalFunction> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
+
+            template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
+            template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeReachabilityTimes(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
+
+            template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
+            template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeReachabilityRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalFunction> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
+
+            template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<storm::RationalNumber> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<storm::RationalNumber> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
+            template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeLongRunAverageProbabilities(storm::storage::SparseMatrix<storm::RationalFunction> const& probabilityMatrix, storm::storage::BitVector const& psiStates, std::vector<storm::RationalFunction> const* exitRateVector, bool qualitative, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
+
+            template std::vector<storm::RationalNumber> SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalNumber> const& linearEquationSolverFactory);
+            template std::vector<storm::RationalFunction> SparseCtmcCslHelper::computeCumulativeRewards(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRateVector, storm::models::sparse::StandardRewardModel<storm::RationalFunction> const& rewardModel, double timeBound, storm::solver::LinearEquationSolverFactory<storm::RationalFunction> const& linearEquationSolverFactory);
+
             template storm::storage::SparseMatrix<double> SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix<double> const& rateMatrix, std::vector<double> const& exitRates);
             template storm::storage::SparseMatrix<storm::RationalNumber> SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix<storm::RationalNumber> const& rateMatrix, std::vector<storm::RationalNumber> const& exitRates);
             template storm::storage::SparseMatrix<storm::RationalFunction> SparseCtmcCslHelper::computeProbabilityMatrix(storm::storage::SparseMatrix<storm::RationalFunction> const& rateMatrix, std::vector<storm::RationalFunction> const& exitRates);
-            
-            template std::vector<double> SparseCtmcCslHelper::computeTransientProbabilities(storm::storage::SparseMatrix<double> const& uniformizedMatrix, std::vector<double> const* addVector, double timeBound, double uniformizationRate, std::vector<double> values, storm::solver::LinearEquationSolverFactory<double> const& linearEquationSolverFactory);
+
+
+
+
+
+
+
+#endif
         }
     }
 }
diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
index bb3a1a701..1b36dd820 100644
--- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
@@ -146,7 +146,10 @@ namespace storm {
         }
         
         template class SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>>;
+
+#ifdef STORM_HAVE_CARL
         template class SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalNumber>>;
         template class SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>>;
+#endif
     }
-}
\ No newline at end of file
+}
diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
index 629cf29eb..25804c37a 100644
--- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
@@ -147,6 +147,9 @@ namespace storm {
 		}
                 
         template class SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<double>>;
+
+#ifdef STORM_HAVE_CARL
         template class SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalNumber>>;
+#endif
     }
-}
\ No newline at end of file
+}
diff --git a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
index 79a85fdfe..d6b721ade 100644
--- a/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/SparseDtmcPrctlHelper.cpp
@@ -401,8 +401,11 @@ namespace storm {
             }
             
             template class SparseDtmcPrctlHelper<double>;
+
+#ifdef STORM_HAVE_CARL
             template class SparseDtmcPrctlHelper<storm::RationalNumber>;
             template class SparseDtmcPrctlHelper<storm::RationalFunction>;
+#endif
         }
     }
 }
diff --git a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
index 75fbfdfea..c9f7e83c4 100644
--- a/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
+++ b/src/modelchecker/prctl/helper/SparseMdpPrctlHelper.cpp
@@ -650,11 +650,12 @@ namespace storm {
             template std::vector<double> SparseMdpPrctlHelper<double>::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::models::sparse::StandardRewardModel<double> const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);
             template std::vector<double> SparseMdpPrctlHelper<double>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& backwardTransitions, storm::models::sparse::StandardRewardModel<double> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<double> const& minMaxLinearEquationSolverFactory);
 
+#ifdef STORM_HAVE_CARL
             template class SparseMdpPrctlHelper<storm::RationalNumber>;
             template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeInstantaneousRewards(OptimizationDirection dir, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, uint_fast64_t stepCount, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory);
             template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeCumulativeRewards(OptimizationDirection dir, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, uint_fast64_t stepBound, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory);
             template std::vector<storm::RationalNumber> SparseMdpPrctlHelper<storm::RationalNumber>::computeReachabilityRewards(OptimizationDirection dir, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::models::sparse::StandardRewardModel<storm::RationalNumber> const& rewardModel, storm::storage::BitVector const& targetStates, bool qualitative, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& minMaxLinearEquationSolverFactory);
-
+#endif
         }
     }
 }
diff --git a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
index 5ffc50140..0725cc4a2 100644
--- a/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
+++ b/src/modelchecker/propositional/SparsePropositionalModelChecker.cpp
@@ -57,6 +57,7 @@ namespace storm {
         template class SparsePropositionalModelChecker<storm::models::sparse::Mdp<double>>;
         template class SparsePropositionalModelChecker<storm::models::sparse::MarkovAutomaton<double>>;
         
+#ifdef STORM_HAVE_CARL
         template class SparsePropositionalModelChecker<storm::models::sparse::Mdp<double, storm::models::sparse::StandardRewardModel<storm::Interval>>>;
 
         template class SparsePropositionalModelChecker<storm::models::sparse::Model<storm::RationalNumber>>;
@@ -70,5 +71,6 @@ namespace storm {
         template class SparsePropositionalModelChecker<storm::models::sparse::Ctmc<storm::RationalFunction>>;
         template class SparsePropositionalModelChecker<storm::models::sparse::Mdp<storm::RationalFunction>>;
         template class SparsePropositionalModelChecker<storm::models::sparse::MarkovAutomaton<storm::RationalFunction>>;
+#endif
     }
-}
\ No newline at end of file
+}
diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
index e6f0bbb2d..fdf541d97 100644
--- a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
@@ -986,7 +986,10 @@ namespace storm {
         }
         
         template class SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<double>>;
+
+#ifdef STORM_HAVE_CARL
         template class SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalNumber>>;
         template class SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>>;
+#endif
     } // namespace modelchecker
 } // namespace storm
diff --git a/src/modelchecker/results/CheckResult.cpp b/src/modelchecker/results/CheckResult.cpp
index 324fdd089..7d8fcd1ac 100644
--- a/src/modelchecker/results/CheckResult.cpp
+++ b/src/modelchecker/results/CheckResult.cpp
@@ -145,10 +145,12 @@ 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/modelchecker/results/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
index 652c094a5..dfe624f2a 100644
--- a/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
+++ b/src/modelchecker/results/ExplicitQuantitativeCheckResult.cpp
@@ -250,7 +250,10 @@ namespace storm {
         }
         
         template class ExplicitQuantitativeCheckResult<double>;
+
+#ifdef STORM_HAVE_CARL
         template class ExplicitQuantitativeCheckResult<storm::RationalNumber>;
         template class ExplicitQuantitativeCheckResult<storm::RationalFunction>;
+#endif
     }
 }
diff --git a/src/models/sparse/Ctmc.cpp b/src/models/sparse/Ctmc.cpp
index e48f4590f..26b106c59 100644
--- a/src/models/sparse/Ctmc.cpp
+++ b/src/models/sparse/Ctmc.cpp
@@ -46,11 +46,13 @@ namespace storm {
             }
             
             template class Ctmc<double>;
+
+#ifdef STORM_HAVE_CARL
             template class Ctmc<storm::RationalNumber>;
 
             template class Ctmc<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
             template class Ctmc<storm::RationalFunction>;
-            
+#endif
         } // namespace sparse
     } // namespace models
-} // namespace storm
\ No newline at end of file
+} // namespace storm
diff --git a/src/models/sparse/DeterministicModel.cpp b/src/models/sparse/DeterministicModel.cpp
index c2bd35b16..5962e6500 100644
--- a/src/models/sparse/DeterministicModel.cpp
+++ b/src/models/sparse/DeterministicModel.cpp
@@ -57,11 +57,13 @@ namespace storm {
             
             template class DeterministicModel<double>;
             template class DeterministicModel<float>;
+
+#ifdef STORM_HAVE_CARL
             template class DeterministicModel<storm::RationalNumber>;
             
             template class DeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
             template class DeterministicModel<storm::RationalFunction>;
-            
+#endif
         } // namespace sparse
     } // namespace models
-} // namespace storm
\ No newline at end of file
+} // namespace storm
diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp
index 7997a1494..ce9f9e5aa 100644
--- a/src/models/sparse/Dtmc.cpp
+++ b/src/models/sparse/Dtmc.cpp
@@ -69,11 +69,13 @@ namespace storm {
             
             template class Dtmc<double>;
             template class Dtmc<float>;
+
+#ifdef STORM_HAVE_CARL
             template class Dtmc<storm::RationalNumber>;
 
             template class Dtmc<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
             template class Dtmc<storm::RationalFunction>;
-
+#endif
         } // namespace sparse
     } // namespace models
 } // namespace storm
diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp
index b09da840e..887d3a13b 100644
--- a/src/models/sparse/MarkovAutomaton.cpp
+++ b/src/models/sparse/MarkovAutomaton.cpp
@@ -366,11 +366,12 @@ namespace storm {
             
             template class MarkovAutomaton<double>;
 //            template class MarkovAutomaton<float>;
+#ifdef STORM_HAVE_CARL
             template class MarkovAutomaton<storm::RationalNumber>;
             
             template class MarkovAutomaton<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
             template class MarkovAutomaton<storm::RationalFunction>;
-
+#endif
         } // namespace sparse
     } // namespace models
 } // namespace storm
diff --git a/src/models/sparse/Mdp.cpp b/src/models/sparse/Mdp.cpp
index cf436c7e1..8db2670f5 100644
--- a/src/models/sparse/Mdp.cpp
+++ b/src/models/sparse/Mdp.cpp
@@ -98,11 +98,13 @@ namespace storm {
 
             template class Mdp<double>;
             template class Mdp<float>;
+
+#ifdef STORM_HAVE_CARL
             template class Mdp<storm::RationalNumber>;
 
             template class Mdp<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
             template class Mdp<storm::RationalFunction>;
-
+#endif
         } // namespace sparse
     } // namespace models
-} // namespace storm
\ No newline at end of file
+} // namespace storm
diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp
index 8ea0710dc..d6eefe93a 100644
--- a/src/models/sparse/Model.cpp
+++ b/src/models/sparse/Model.cpp
@@ -312,7 +312,11 @@ namespace storm {
             
             template<typename ValueType, typename RewardModelType>
             bool Model<ValueType, RewardModelType>::supportsParameters() const {
+#ifdef STORM_HAVE_CARL
                 return std::is_same<ValueType, storm::RationalFunction>::value;
+#else
+		return false;
+#endif
             }
             
             template<typename ValueType, typename RewardModelType>
@@ -346,18 +350,21 @@ namespace storm {
                 return this->rewardModels;
             }
             
+#ifdef STORM_HAVE_CARL
             std::set<storm::RationalFunctionVariable> getProbabilityParameters(Model<storm::RationalFunction> const& model) {
                 return storm::storage::getVariables(model.getTransitionMatrix());
             }
+#endif
             
             template class Model<double>;
             template class Model<float>;
 
+#ifdef STORM_HAVE_CARL
             template class Model<storm::RationalNumber>;
 
             template class Model<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
             template class Model<storm::RationalFunction>;
-            
+#endif
         }
     }
 }
diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h
index a4422a8be..5936b0fe2 100644
--- a/src/models/sparse/Model.h
+++ b/src/models/sparse/Model.h
@@ -357,7 +357,9 @@ namespace storm {
                 boost::optional<std::vector<LabelSet>> choiceLabeling;
             };
             
+#ifdef STORM_HAVE_CARL
             std::set<storm::RationalFunctionVariable> getProbabilityParameters(Model<storm::RationalFunction> const& model);
+#endif
         } // namespace sparse
     } // namespace models
 } // namespace storm
diff --git a/src/models/sparse/NondeterministicModel.cpp b/src/models/sparse/NondeterministicModel.cpp
index 5dfaea955..0d97b87d0 100644
--- a/src/models/sparse/NondeterministicModel.cpp
+++ b/src/models/sparse/NondeterministicModel.cpp
@@ -169,6 +169,8 @@ namespace storm {
             
             template class NondeterministicModel<double>;
             template class NondeterministicModel<float>;
+
+#ifdef STORM_HAVE_CARL
             template class NondeterministicModel<storm::RationalNumber>;
 
             template class NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
@@ -176,7 +178,7 @@ namespace storm {
             template void NondeterministicModel<double, storm::models::sparse::StandardRewardModel<storm::Interval>>::modifyStateRewards(std::string const& modelName, std::map<uint_fast64_t, double> const& modifications);
 
             template class NondeterministicModel<storm::RationalFunction>;
-
+#endif
         }
     }
-}
\ No newline at end of file
+}
diff --git a/src/models/sparse/StandardRewardModel.cpp b/src/models/sparse/StandardRewardModel.cpp
index 823d3a884..a539cfd15 100644
--- a/src/models/sparse/StandardRewardModel.cpp
+++ b/src/models/sparse/StandardRewardModel.cpp
@@ -318,6 +318,7 @@ namespace storm {
             template class StandardRewardModel<float>;
             template std::ostream& operator<<<float>(std::ostream& out, StandardRewardModel<float> const& rewardModel);
 
+#ifdef STORM_HAVE_CARL
             template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(uint_fast64_t numberOfRows, storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::BitVector const& filter) const;
             template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix) const;
             template std::vector<storm::RationalNumber> StandardRewardModel<storm::RationalNumber>::getTotalRewardVector(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<storm::RationalNumber> const& weights) const;
@@ -346,6 +347,7 @@ namespace storm {
             template void StandardRewardModel<storm::Interval>::reduceToStateBasedRewards(storm::storage::SparseMatrix<double> const& transitionMatrix, bool reduceToStateRewards);
             template class StandardRewardModel<storm::Interval>;
             template std::ostream& operator<<<storm::Interval>(std::ostream& out, StandardRewardModel<storm::Interval> const& rewardModel);
+#endif
         }
         
     }
diff --git a/src/parser/DFTGalileoParser.cpp b/src/parser/DFTGalileoParser.cpp
index 2cdda4929..5fc2e7c5a 100644
--- a/src/parser/DFTGalileoParser.cpp
+++ b/src/parser/DFTGalileoParser.cpp
@@ -71,12 +71,16 @@ namespace storm {
                     toplevelId = stripQuotsFromName(line.substr(toplevelToken.size() + 1));
                 }
                 else if (boost::starts_with(line, parametricToken)) {
+#ifdef STORM_HAVE_CARL
                     STORM_LOG_THROW((std::is_same<ValueType, storm::RationalFunction>::value), storm::exceptions::NotSupportedException, "Parameters only allowed when using rational functions.");
                     std::string parameter = stripQuotsFromName(line.substr(parametricToken.size() + 1));
                     storm::expressions::Variable var = manager->declareRationalVariable(parameter);
                     identifierMapping.emplace(var.getName(), var);
                     parser.setIdentifierMapping(identifierMapping);
                     STORM_LOG_TRACE("Added parameter: " << var.getName());
+#else
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build.");
+#endif
                 } else {
                     std::vector<std::string> tokens;
                     boost::split(tokens, line, boost::is_any_of(" "));
diff --git a/src/solver/EigenLinearEquationSolver.cpp b/src/solver/EigenLinearEquationSolver.cpp
index 25c16f1ae..47117b9a3 100644
--- a/src/solver/EigenLinearEquationSolver.cpp
+++ b/src/solver/EigenLinearEquationSolver.cpp
@@ -94,6 +94,7 @@ namespace storm {
             return restart;
         }
         
+#ifdef STORM_HAVE_CARL
         EigenLinearEquationSolverSettings<storm::RationalNumber>::EigenLinearEquationSolverSettings() {
             // Intentionally left empty.
         }
@@ -101,6 +102,7 @@ namespace storm {
         EigenLinearEquationSolverSettings<storm::RationalFunction>::EigenLinearEquationSolverSettings() {
             // Intentionally left empty.
         }
+#endif
 
         template<typename ValueType>
         EigenLinearEquationSolver<ValueType>::EigenLinearEquationSolver(storm::storage::SparseMatrix<ValueType> const& A, EigenLinearEquationSolverSettings<ValueType> const& settings) : eigenA(storm::adapters::EigenAdapter::toEigenSparseMatrix<ValueType>(A)), settings(settings) {
@@ -255,8 +257,8 @@ namespace storm {
             return eigenA->cols();
         }
         
-        // Specialization form storm::RationalNumber
-        
+#ifdef STORM_HAVE_CARL
+        // Specialization for storm::RationalNumber
         template<>
         void EigenLinearEquationSolver<storm::RationalNumber>::solveEquations(std::vector<storm::RationalNumber>& x, std::vector<storm::RationalNumber> const& b) const {
             // Map the input vectors to Eigen's format.
@@ -268,8 +270,7 @@ namespace storm {
             solver._solve_impl(eigenB, eigenX);
         }
         
-        // Specialization form storm::RationalFunction
-        
+        // Specialization for storm::RationalFunction
         template<>
         void EigenLinearEquationSolver<storm::RationalFunction>::solveEquations(std::vector<storm::RationalFunction>& x, std::vector<storm::RationalFunction> const& b) const {
             // Map the input vectors to Eigen's format.
@@ -280,7 +281,8 @@ namespace storm {
             solver.compute(*eigenA);
             solver._solve_impl(eigenB, eigenX);
         }
-                
+#endif
+
         template<typename ValueType>
         std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> EigenLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
             return std::make_unique<storm::solver::EigenLinearEquationSolver<ValueType>>(matrix, settings);
@@ -307,16 +309,18 @@ namespace storm {
         }
         
         template class EigenLinearEquationSolverSettings<double>;
+        template class EigenLinearEquationSolver<double>;
+        template class EigenLinearEquationSolverFactory<double>;
+
+#ifdef STORM_HAVE_CARL
         template class EigenLinearEquationSolverSettings<storm::RationalNumber>;
         template class EigenLinearEquationSolverSettings<storm::RationalFunction>;
         
-        template class EigenLinearEquationSolver<double>;
         template class EigenLinearEquationSolver<storm::RationalNumber>;
         template class EigenLinearEquationSolver<storm::RationalFunction>;
         
-        template class EigenLinearEquationSolverFactory<double>;
         template class EigenLinearEquationSolverFactory<storm::RationalNumber>;
         template class EigenLinearEquationSolverFactory<storm::RationalFunction>;
-        
+#endif
     }
-}
\ No newline at end of file
+}
diff --git a/src/solver/EigenLinearEquationSolver.h b/src/solver/EigenLinearEquationSolver.h
index 04c6c9718..688dcae64 100644
--- a/src/solver/EigenLinearEquationSolver.h
+++ b/src/solver/EigenLinearEquationSolver.h
@@ -40,6 +40,7 @@ namespace storm {
             uint_fast64_t restart;
         };
         
+#ifdef STORM_HAVE_CARL
         template<>
         class EigenLinearEquationSolverSettings<storm::RationalNumber> {
         public:
@@ -51,6 +52,7 @@ namespace storm {
         public:
             EigenLinearEquationSolverSettings();
         };
+#endif
         
         /*!
          * A class that uses the Eigen library to implement the LinearEquationSolver interface.
@@ -96,4 +98,4 @@ namespace storm {
             EigenLinearEquationSolverSettings<ValueType> settings;
         };
     }
-}
\ No newline at end of file
+}
diff --git a/src/solver/EliminationLinearEquationSolver.cpp b/src/solver/EliminationLinearEquationSolver.cpp
index 982d2a54b..8cf773c16 100644
--- a/src/solver/EliminationLinearEquationSolver.cpp
+++ b/src/solver/EliminationLinearEquationSolver.cpp
@@ -173,16 +173,19 @@ namespace storm {
         }
         
         template class EliminationLinearEquationSolverSettings<double>;
+        template class EliminationLinearEquationSolver<double>;
+        template class EliminationLinearEquationSolverFactory<double>;
+
+#ifdef STORM_HAVE_CARL
         template class EliminationLinearEquationSolverSettings<storm::RationalNumber>;
         template class EliminationLinearEquationSolverSettings<storm::RationalFunction>;
         
-        template class EliminationLinearEquationSolver<double>;
         template class EliminationLinearEquationSolver<storm::RationalNumber>;
         template class EliminationLinearEquationSolver<storm::RationalFunction>;
         
-        template class EliminationLinearEquationSolverFactory<double>;
         template class EliminationLinearEquationSolverFactory<storm::RationalNumber>;
         template class EliminationLinearEquationSolverFactory<storm::RationalFunction>;
+#endif
     }
 }
 
diff --git a/src/solver/LinearEquationSolver.cpp b/src/solver/LinearEquationSolver.cpp
index 81dc4124b..c4d46cd46 100644
--- a/src/solver/LinearEquationSolver.cpp
+++ b/src/solver/LinearEquationSolver.cpp
@@ -121,6 +121,7 @@ namespace storm {
             return std::make_unique<GeneralLinearEquationSolverFactory<ValueType>>(*this);
         }
         
+#ifdef STORM_HAVE_CARL
         std::unique_ptr<LinearEquationSolver<storm::RationalNumber>> GeneralLinearEquationSolverFactory<storm::RationalNumber>::create(storm::storage::SparseMatrix<storm::RationalNumber> const& matrix) const {
             return selectSolver(matrix);
         }
@@ -162,18 +163,22 @@ namespace storm {
         std::unique_ptr<LinearEquationSolverFactory<storm::RationalFunction>> GeneralLinearEquationSolverFactory<storm::RationalFunction>::clone() const {
             return std::make_unique<GeneralLinearEquationSolverFactory<storm::RationalFunction>>(*this);
         }
+#endif
 
         template class LinearEquationSolver<double>;
+        template class LinearEquationSolverFactory<double>;
+        template class GeneralLinearEquationSolverFactory<double>;
+
+#ifdef STORM_HAVE_CARL
         template class LinearEquationSolver<storm::RationalNumber>;
         template class LinearEquationSolver<storm::RationalFunction>;
 
-        template class LinearEquationSolverFactory<double>;
         template class LinearEquationSolverFactory<storm::RationalNumber>;
         template class LinearEquationSolverFactory<storm::RationalFunction>;
         
-        template class GeneralLinearEquationSolverFactory<double>;
         template class GeneralLinearEquationSolverFactory<storm::RationalNumber>;
         template class GeneralLinearEquationSolverFactory<storm::RationalFunction>;
+#endif
 
     }
-}
\ No newline at end of file
+}
diff --git a/src/solver/LinearEquationSolver.h b/src/solver/LinearEquationSolver.h
index aa243d593..5adac8ea1 100644
--- a/src/solver/LinearEquationSolver.h
+++ b/src/solver/LinearEquationSolver.h
@@ -154,6 +154,7 @@ namespace storm {
             std::unique_ptr<LinearEquationSolver<ValueType>> selectSolver(MatrixType&& matrix) const;
         };
         
+#ifdef STORM_HAVE_CARL
         template<>
         class GeneralLinearEquationSolverFactory<storm::RationalNumber> : public LinearEquationSolverFactory<storm::RationalNumber> {
         public:
@@ -179,7 +180,7 @@ namespace storm {
             template<typename MatrixType>
             std::unique_ptr<LinearEquationSolver<storm::RationalFunction>> selectSolver(MatrixType&& matrix) const;
         };
-        
+#endif
     } // namespace solver
 } // namespace storm
 
diff --git a/src/solver/MinMaxLinearEquationSolver.cpp b/src/solver/MinMaxLinearEquationSolver.cpp
index a92f19dd9..c82514a37 100644
--- a/src/solver/MinMaxLinearEquationSolver.cpp
+++ b/src/solver/MinMaxLinearEquationSolver.cpp
@@ -144,6 +144,7 @@ namespace storm {
             return result;
         }
 
+#ifdef STORM_HAVE_CARL
         template<>
         template<typename MatrixType>
         std::unique_ptr<MinMaxLinearEquationSolver<storm::RationalNumber>> GeneralMinMaxLinearEquationSolverFactory<storm::RationalNumber>::selectSolver(MatrixType&& matrix) const {
@@ -152,15 +153,17 @@ namespace storm {
             STORM_LOG_THROW(method == MinMaxMethod::ValueIteration || method == MinMaxMethod::PolicyIteration, storm::exceptions::InvalidSettingsException, "For this data type only value iteration and policy iteration are available.");
             return std::make_unique<StandardMinMaxLinearEquationSolver<storm::RationalNumber>>(std::forward<MatrixType>(matrix), std::make_unique<GeneralLinearEquationSolverFactory<storm::RationalNumber>>());
         }
-
+#endif
         template class MinMaxLinearEquationSolver<float>;
         template class MinMaxLinearEquationSolver<double>;
-        template class MinMaxLinearEquationSolver<storm::RationalNumber>;
         
         template class MinMaxLinearEquationSolverFactory<double>;
         template class GeneralMinMaxLinearEquationSolverFactory<double>;
+
+#ifdef STORM_HAVE_CARL
+        template class MinMaxLinearEquationSolver<storm::RationalNumber>;
         template class MinMaxLinearEquationSolverFactory<storm::RationalNumber>;
         template class GeneralMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
-        
+#endif
     }
 }
diff --git a/src/solver/SolveGoal.cpp b/src/solver/SolveGoal.cpp
index 2f0cd365c..622a0c8de 100644
--- a/src/solver/SolveGoal.cpp
+++ b/src/solver/SolveGoal.cpp
@@ -51,8 +51,9 @@ namespace storm {
         template std::unique_ptr<storm::solver::LinearEquationSolver<double>> configureLinearEquationSolver(BoundedGoal<double> const& goal, storm::solver::LinearEquationSolverFactory<double> const& factory, storm::storage::SparseMatrix<double> const&  matrix);
         template std::unique_ptr<storm::solver::LinearEquationSolver<double>> configureLinearEquationSolver(SolveGoal const& goal, storm::solver::LinearEquationSolverFactory<double> const& factory, storm::storage::SparseMatrix<double> const&  matrix);
 
+#ifdef STORM_HAVE_CARL
         template std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<storm::RationalNumber>> configureMinMaxLinearEquationSolver(BoundedGoal<storm::RationalNumber> const& goal, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& factory, storm::storage::SparseMatrix<storm::RationalNumber> const& matrix);
         template std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<storm::RationalNumber>> configureMinMaxLinearEquationSolver(SolveGoal const& goal, storm::solver::MinMaxLinearEquationSolverFactory<storm::RationalNumber> const& factory, storm::storage::SparseMatrix<storm::RationalNumber> const&  matrix);
-
+#endif
     }
 }
diff --git a/src/solver/StandardMinMaxLinearEquationSolver.cpp b/src/solver/StandardMinMaxLinearEquationSolver.cpp
index 4e0609e80..1a1f1fcda 100644
--- a/src/solver/StandardMinMaxLinearEquationSolver.cpp
+++ b/src/solver/StandardMinMaxLinearEquationSolver.cpp
@@ -370,6 +370,7 @@ namespace storm {
             }
         }
         
+#ifdef STORM_HAVE_CARL
         template<>
         StandardMinMaxLinearEquationSolverFactory<storm::RationalNumber>::StandardMinMaxLinearEquationSolverFactory(EquationSolverType const& solverType, bool trackScheduler) : MinMaxLinearEquationSolverFactory<storm::RationalNumber>(trackScheduler) {
             switch (solverType) {
@@ -379,6 +380,7 @@ namespace storm {
                     STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Cannot create the requested solver for this data type.");
             }
         }
+#endif
         
         template<typename ValueType>
         std::unique_ptr<MinMaxLinearEquationSolver<ValueType>> StandardMinMaxLinearEquationSolverFactory<ValueType>::create(storm::storage::SparseMatrix<ValueType> const& matrix) const {
@@ -441,11 +443,12 @@ namespace storm {
         template class NativeMinMaxLinearEquationSolverFactory<double>;
         template class EliminationMinMaxLinearEquationSolverFactory<double>;
         
+#ifdef STORM_HAVE_CARL
         template class StandardMinMaxLinearEquationSolverSettings<storm::RationalNumber>;
         template class StandardMinMaxLinearEquationSolver<storm::RationalNumber>;
         template class StandardMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
         template class EigenMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
         template class EliminationMinMaxLinearEquationSolverFactory<storm::RationalNumber>;
-        
+#endif
     }
-}
\ No newline at end of file
+}
diff --git a/src/solver/TerminationCondition.cpp b/src/solver/TerminationCondition.cpp
index 0503723bc..b0f155470 100644
--- a/src/solver/TerminationCondition.cpp
+++ b/src/solver/TerminationCondition.cpp
@@ -40,8 +40,9 @@ namespace storm {
         template class TerminateIfFilteredSumExceedsThreshold<double>;
         template class TerminateIfFilteredExtremumExceedsThreshold<double>;
 
+#ifdef STORM_HAVE_CARL
         template class TerminateIfFilteredSumExceedsThreshold<storm::RationalNumber>;
         template class TerminateIfFilteredExtremumExceedsThreshold<storm::RationalNumber>;
-
+#endif
     }
 }
diff --git a/src/solver/stateelimination/ConditionalStateEliminator.cpp b/src/solver/stateelimination/ConditionalStateEliminator.cpp
index 0a86894bc..21ffec7ac 100644
--- a/src/solver/stateelimination/ConditionalStateEliminator.cpp
+++ b/src/solver/stateelimination/ConditionalStateEliminator.cpp
@@ -61,9 +61,11 @@ namespace storm {
             }
             
             template class ConditionalStateEliminator<double>;
+
+#ifdef STORM_HAVE_CARL
             template class ConditionalStateEliminator<storm::RationalNumber>;
             template class ConditionalStateEliminator<storm::RationalFunction>;
-            
+#endif
         } // namespace stateelimination
     } // namespace storage
 } // namespace storm
diff --git a/src/solver/stateelimination/DynamicStatePriorityQueue.cpp b/src/solver/stateelimination/DynamicStatePriorityQueue.cpp
index ec2c4fe3f..a0fede010 100644
--- a/src/solver/stateelimination/DynamicStatePriorityQueue.cpp
+++ b/src/solver/stateelimination/DynamicStatePriorityQueue.cpp
@@ -62,8 +62,11 @@ namespace storm {
             }
 
             template class DynamicStatePriorityQueue<double>;
+
+#ifdef STORM_HAVE_CARL
             template class DynamicStatePriorityQueue<storm::RationalNumber>;
             template class DynamicStatePriorityQueue<storm::RationalFunction>;
+#endif
         }
     }
 }
diff --git a/src/solver/stateelimination/EliminatorBase.cpp b/src/solver/stateelimination/EliminatorBase.cpp
index 43f94f329..4a083d5fc 100644
--- a/src/solver/stateelimination/EliminatorBase.cpp
+++ b/src/solver/stateelimination/EliminatorBase.cpp
@@ -274,13 +274,15 @@ namespace storm {
             }
             
             template class EliminatorBase<double, ScalingMode::Divide>;
+            template class EliminatorBase<double, ScalingMode::DivideOneMinus>;
+
+#ifdef STORM_HAVE_CARL
             template class EliminatorBase<storm::RationalNumber, ScalingMode::Divide>;
             template class EliminatorBase<storm::RationalFunction, ScalingMode::Divide>;
 
-            template class EliminatorBase<double, ScalingMode::DivideOneMinus>;
             template class EliminatorBase<storm::RationalNumber, ScalingMode::DivideOneMinus>;
             template class EliminatorBase<storm::RationalFunction, ScalingMode::DivideOneMinus>;
-
+#endif
         }
     }
-}
\ No newline at end of file
+}
diff --git a/src/solver/stateelimination/EquationSystemEliminator.cpp b/src/solver/stateelimination/EquationSystemEliminator.cpp
index 2ffe29705..f08f49107 100644
--- a/src/solver/stateelimination/EquationSystemEliminator.cpp
+++ b/src/solver/stateelimination/EquationSystemEliminator.cpp
@@ -10,8 +10,11 @@ namespace storm {
             }
             
             template class EquationSystemEliminator<double>;
+
+#ifdef STORM_HAVE_CARL
             template class EquationSystemEliminator<storm::RationalNumber>;
             template class EquationSystemEliminator<storm::RationalFunction>;
+#endif
         }
     }
-}
\ No newline at end of file
+}
diff --git a/src/solver/stateelimination/LongRunAverageEliminator.cpp b/src/solver/stateelimination/LongRunAverageEliminator.cpp
index 758f71a14..982342b5a 100644
--- a/src/solver/stateelimination/LongRunAverageEliminator.cpp
+++ b/src/solver/stateelimination/LongRunAverageEliminator.cpp
@@ -23,9 +23,11 @@ namespace storm {
             }
             
             template class LongRunAverageEliminator<double>;
+
+#ifdef STORM_HAVE_CARL
             template class LongRunAverageEliminator<storm::RationalNumber>;
             template class LongRunAverageEliminator<storm::RationalFunction>;
-            
+#endif
         } // namespace stateelimination
     } // namespace storage
 } // namespace storm
diff --git a/src/solver/stateelimination/PrioritizedStateEliminator.cpp b/src/solver/stateelimination/PrioritizedStateEliminator.cpp
index 134cb3264..1b8cca6ff 100644
--- a/src/solver/stateelimination/PrioritizedStateEliminator.cpp
+++ b/src/solver/stateelimination/PrioritizedStateEliminator.cpp
@@ -29,9 +29,11 @@ namespace storm {
             }
             
             template class PrioritizedStateEliminator<double>;
+
+#ifdef STORM_HAVE_CARL
             template class PrioritizedStateEliminator<storm::RationalNumber>;
             template class PrioritizedStateEliminator<storm::RationalFunction>;
-            
+#endif
         } // namespace stateelimination
     } // namespace storage
 } // namespace storm
diff --git a/src/solver/stateelimination/StateEliminator.cpp b/src/solver/stateelimination/StateEliminator.cpp
index 98b1d64b3..c134d9ffa 100644
--- a/src/solver/stateelimination/StateEliminator.cpp
+++ b/src/solver/stateelimination/StateEliminator.cpp
@@ -28,9 +28,11 @@ namespace storm {
             }
             
             template class StateEliminator<double>;
+
+#ifdef STORM_HAVE_CARL
             template class StateEliminator<storm::RationalNumber>;
             template class StateEliminator<storm::RationalFunction>;
-            
+#endif
         } // namespace stateelimination
     } // namespace storage
 } // namespace storm
diff --git a/src/storage/Distribution.cpp b/src/storage/Distribution.cpp
index 7c3b5d99f..78e4a477d 100644
--- a/src/storage/Distribution.cpp
+++ b/src/storage/Distribution.cpp
@@ -152,10 +152,12 @@ namespace storm {
         template class Distribution<double>;
         template std::ostream& operator<<(std::ostream& out, Distribution<double> const& distribution);
 
+#ifdef STORM_HAVE_CARL
         template class Distribution<storm::RationalNumber>;
         template std::ostream& operator<<(std::ostream& out, Distribution<storm::RationalNumber> const& distribution);
 
         template class Distribution<storm::RationalFunction>;
         template std::ostream& operator<<(std::ostream& out, Distribution<storm::RationalFunction> const& distribution);
+#endif
     }
 }
diff --git a/src/storage/FlexibleSparseMatrix.cpp b/src/storage/FlexibleSparseMatrix.cpp
index 563f86633..102d20304 100644
--- a/src/storage/FlexibleSparseMatrix.cpp
+++ b/src/storage/FlexibleSparseMatrix.cpp
@@ -269,13 +269,14 @@ namespace storm {
         // Explicitly instantiate the matrix.
         template class FlexibleSparseMatrix<double>;
         template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix<double> const& matrix);
+
+#ifdef STORM_HAVE_CARL
         template class FlexibleSparseMatrix<storm::RationalNumber>;
         template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix<storm::RationalNumber> const& matrix);
 
-#ifdef STORM_HAVE_CARL
         template class FlexibleSparseMatrix<storm::RationalFunction>;
         template std::ostream& operator<<(std::ostream& out, FlexibleSparseMatrix<storm::RationalFunction> const& matrix);
 #endif
 
     } // namespace storage
-} // namespace storm
\ No newline at end of file
+} // namespace storm
diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp
index d410b2546..0861513ce 100644
--- a/src/storage/MaximalEndComponentDecomposition.cpp
+++ b/src/storage/MaximalEndComponentDecomposition.cpp
@@ -193,8 +193,9 @@ namespace storm {
         template class MaximalEndComponentDecomposition<double>;
         template MaximalEndComponentDecomposition<double>::MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel<double> const& model);
 
+#ifdef STORM_HAVE_CARL
         template class MaximalEndComponentDecomposition<storm::RationalNumber>;
         template MaximalEndComponentDecomposition<storm::RationalNumber>::MaximalEndComponentDecomposition(storm::models::sparse::NondeterministicModel<storm::RationalNumber> const& model);
-
+#endif
     }
 }
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index 95f65ce99..add3debbb 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -1213,10 +1213,12 @@ namespace storm {
             }
         }
         
+#ifdef STORM_HAVE_CARL
         template<>
         void SparseMatrix<Interval>::performSuccessiveOverRelaxationStep(Interval omega, std::vector<Interval>& x, std::vector<Interval> const& b) const {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This operation is not supported.");
         }
+#endif
         
         template<typename ValueType>
         void SparseMatrix<ValueType>::multiplyVectorWithMatrix(std::vector<value_type> const& vector, std::vector<value_type>& result) const {
diff --git a/src/storage/StronglyConnectedComponentDecomposition.cpp b/src/storage/StronglyConnectedComponentDecomposition.cpp
index e129c8b85..c32184681 100644
--- a/src/storage/StronglyConnectedComponentDecomposition.cpp
+++ b/src/storage/StronglyConnectedComponentDecomposition.cpp
@@ -227,16 +227,17 @@ namespace storm {
         }
         
         // Explicitly instantiate the SCC decomposition.
-		template class StronglyConnectedComponentDecomposition<double>;
+        template class StronglyConnectedComponentDecomposition<double>;
         template StronglyConnectedComponentDecomposition<double>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<double> const& model, bool dropNaiveSccs, bool onlyBottomSccs);
         template StronglyConnectedComponentDecomposition<double>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<double> const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs);
         template StronglyConnectedComponentDecomposition<double>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<double> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs);
         
-		template class StronglyConnectedComponentDecomposition<float>;
+        template class StronglyConnectedComponentDecomposition<float>;
         template StronglyConnectedComponentDecomposition<float>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<float> const& model, bool dropNaiveSccs, bool onlyBottomSccs);
         template StronglyConnectedComponentDecomposition<float>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<float> const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs);
         template StronglyConnectedComponentDecomposition<float>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<float> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs);
 
+#ifdef STORM_HAVE_CARL
         template class StronglyConnectedComponentDecomposition<storm::RationalNumber>;
         template StronglyConnectedComponentDecomposition<storm::RationalNumber>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<storm::RationalNumber> const& model, bool dropNaiveSccs, bool onlyBottomSccs);
         template StronglyConnectedComponentDecomposition<storm::RationalNumber>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<storm::RationalNumber> const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs);
@@ -246,5 +247,6 @@ namespace storm {
         template StronglyConnectedComponentDecomposition<storm::RationalFunction>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<storm::RationalFunction> const& model, bool dropNaiveSccs, bool onlyBottomSccs);
         template StronglyConnectedComponentDecomposition<storm::RationalFunction>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<storm::RationalFunction> const& model, StateBlock const& block, bool dropNaiveSccs, bool onlyBottomSccs);
         template StronglyConnectedComponentDecomposition<storm::RationalFunction>::StronglyConnectedComponentDecomposition(storm::models::sparse::Model<storm::RationalFunction> const& model, storm::storage::BitVector const& subsystem, bool dropNaiveSccs, bool onlyBottomSccs);
+#endif
     } // namespace storage
-} // namespace storm
\ No newline at end of file
+} // namespace storm
diff --git a/src/storage/bisimulation/BisimulationDecomposition.cpp b/src/storage/bisimulation/BisimulationDecomposition.cpp
index 30fc5a2c9..dbad8c633 100644
--- a/src/storage/bisimulation/BisimulationDecomposition.cpp
+++ b/src/storage/bisimulation/BisimulationDecomposition.cpp
@@ -323,6 +323,7 @@ namespace storm {
         template class BisimulationDecomposition<storm::models::sparse::Ctmc<double>, bisimulation::DeterministicBlockData>;
         template class BisimulationDecomposition<storm::models::sparse::Mdp<double>, bisimulation::DeterministicBlockData>;
 
+#ifdef STORM_HAVE_CARL
         template class BisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalNumber>, bisimulation::DeterministicBlockData>;
         template class BisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalNumber>, bisimulation::DeterministicBlockData>;
         template class BisimulationDecomposition<storm::models::sparse::Mdp<storm::RationalNumber>, bisimulation::DeterministicBlockData>;
@@ -330,5 +331,6 @@ namespace storm {
         template class BisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalFunction>, bisimulation::DeterministicBlockData>;
         template class BisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalFunction>, bisimulation::DeterministicBlockData>;
         template class BisimulationDecomposition<storm::models::sparse::Mdp<storm::RationalFunction>, bisimulation::DeterministicBlockData>;
+#endif
     }
 }
diff --git a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
index 89408e620..3f70fd379 100644
--- a/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
+++ b/src/storage/bisimulation/DeterministicModelBisimulationDecomposition.cpp
@@ -652,10 +652,12 @@ namespace storm {
         template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<double>>;
         template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<double>>;
 
+#ifdef STORM_HAVE_CARL
         template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalNumber>>;
         template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalNumber>>;
 
         template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Dtmc<storm::RationalFunction>>;
         template class DeterministicModelBisimulationDecomposition<storm::models::sparse::Ctmc<storm::RationalFunction>>;
+#endif
     }
 }
diff --git a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp
index a1eea43dc..64a7efe45 100644
--- a/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp
+++ b/src/storage/bisimulation/NondeterministicModelBisimulationDecomposition.cpp
@@ -416,8 +416,10 @@ namespace storm {
         }
         
         template class NondeterministicModelBisimulationDecomposition<storm::models::sparse::Mdp<double>>;
+
+#ifdef STORM_HAVE_CARL
         template class NondeterministicModelBisimulationDecomposition<storm::models::sparse::Mdp<storm::RationalNumber>>;
         template class NondeterministicModelBisimulationDecomposition<storm::models::sparse::Mdp<storm::RationalFunction>>;
-        
+#endif
     }
 }
diff --git a/src/storage/expressions/ExpressionEvaluator.cpp b/src/storage/expressions/ExpressionEvaluator.cpp
index 6d44d680a..cf1493dac 100644
--- a/src/storage/expressions/ExpressionEvaluator.cpp
+++ b/src/storage/expressions/ExpressionEvaluator.cpp
@@ -30,6 +30,7 @@ namespace storm {
             this->variableToExpressionMap[variable] = this->getManager().rational(value);
         }
 
+#ifdef STORM_HAVE_CARL
         ExpressionEvaluator<RationalNumber>::ExpressionEvaluator(storm::expressions::ExpressionManager const& manager) : ExpressionEvaluatorWithVariableToExpressionMap<RationalNumber>(manager) {
             // Intentionally left empty.
         }
@@ -50,5 +51,6 @@ namespace storm {
         
         template class ExpressionEvaluatorWithVariableToExpressionMap<RationalNumber>;
         template class ExpressionEvaluatorWithVariableToExpressionMap<RationalFunction>;
+#endif
     }
-}
\ No newline at end of file
+}
diff --git a/src/storage/expressions/ExpressionEvaluator.h b/src/storage/expressions/ExpressionEvaluator.h
index 2480af12d..e75d1cdf1 100644
--- a/src/storage/expressions/ExpressionEvaluator.h
+++ b/src/storage/expressions/ExpressionEvaluator.h
@@ -35,6 +35,7 @@ namespace storm {
             std::unordered_map<storm::expressions::Variable, storm::expressions::Expression> variableToExpressionMap;
         };
         
+#ifdef STORM_HAVE_CARL
         template<>
         class ExpressionEvaluator<RationalNumber> : public ExpressionEvaluatorWithVariableToExpressionMap<RationalNumber> {
         public:
@@ -58,7 +59,8 @@ namespace storm {
             // A visitor that can be used to translate expressions to rational functions.
             mutable ToRationalFunctionVisitor<RationalFunction> rationalFunctionVisitor;
         };
+#endif
     }
 }
 
-#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONEVALUATOR_H_ */
\ No newline at end of file
+#endif /* STORM_STORAGE_EXPRESSIONS_EXPRESSIONEVALUATOR_H_ */
diff --git a/src/storage/expressions/ExpressionEvaluatorBase.cpp b/src/storage/expressions/ExpressionEvaluatorBase.cpp
index d98810886..aeca1b656 100644
--- a/src/storage/expressions/ExpressionEvaluatorBase.cpp
+++ b/src/storage/expressions/ExpressionEvaluatorBase.cpp
@@ -16,7 +16,10 @@ namespace storm {
         }
         
         template class ExpressionEvaluatorBase<double>;
+
+#ifdef STORM_HAVE_CARL
         template class ExpressionEvaluatorBase<storm::RationalNumber>;
         template class ExpressionEvaluatorBase<storm::RationalFunction>;
+#endif
     }
-}
\ No newline at end of file
+}
diff --git a/src/storage/expressions/ExprtkExpressionEvaluator.cpp b/src/storage/expressions/ExprtkExpressionEvaluator.cpp
index 942c17172..d24bc742c 100755
--- a/src/storage/expressions/ExprtkExpressionEvaluator.cpp
+++ b/src/storage/expressions/ExprtkExpressionEvaluator.cpp
@@ -83,7 +83,10 @@ namespace storm {
         }
         
         template class ExprtkExpressionEvaluatorBase<double>;
+
+#ifdef STORM_HAVE_CARL
         template class ExprtkExpressionEvaluatorBase<RationalNumber>;
         template class ExprtkExpressionEvaluatorBase<RationalFunction>;
+#endif
     }
-}
\ No newline at end of file
+}
diff --git a/src/storage/expressions/ToRationalFunctionVisitor.cpp b/src/storage/expressions/ToRationalFunctionVisitor.cpp
index 71e052bee..1a3dd0fc3 100644
--- a/src/storage/expressions/ToRationalFunctionVisitor.cpp
+++ b/src/storage/expressions/ToRationalFunctionVisitor.cpp
@@ -7,6 +7,8 @@
 
 namespace storm {
     namespace expressions {
+
+#ifdef STORM_HAVE_CARL
         template<typename RationalFunctionType>
         ToRationalFunctionVisitor<RationalFunctionType>::ToRationalFunctionVisitor() : ExpressionVisitor(), cache(new carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>()) {
             // Intentionally left empty.
@@ -95,6 +97,6 @@ namespace storm {
         }
 
         template class ToRationalFunctionVisitor<storm::RationalFunction>;
-        
+#endif
     }
 }
diff --git a/src/storage/expressions/ToRationalFunctionVisitor.h b/src/storage/expressions/ToRationalFunctionVisitor.h
index 6bd3a205b..12603f44e 100644
--- a/src/storage/expressions/ToRationalFunctionVisitor.h
+++ b/src/storage/expressions/ToRationalFunctionVisitor.h
@@ -10,6 +10,7 @@
 namespace storm {
     namespace expressions {
 
+#ifdef STORM_HAVE_CARL
         template<typename RationalFunctionType>
         class ToRationalFunctionVisitor : public ExpressionVisitor {
         public:
@@ -45,7 +46,8 @@ namespace storm {
             // The cache that is used in case the underlying type needs a cache.
             std::shared_ptr<carl::Cache<carl::PolynomialFactorizationPair<RawPolynomial>>> cache;
         };
+#endif
     }
 }
 
-#endif /* STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_ */
\ No newline at end of file
+#endif /* STORM_STORAGE_EXPRESSIONS_TORATIONALFUNCTIONVISITOR_H_ */
diff --git a/src/storage/expressions/ToRationalNumberVisitor.cpp b/src/storage/expressions/ToRationalNumberVisitor.cpp
index b17ec335a..785f36950 100644
--- a/src/storage/expressions/ToRationalNumberVisitor.cpp
+++ b/src/storage/expressions/ToRationalNumberVisitor.cpp
@@ -2,6 +2,7 @@
 
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidArgumentException.h"
+#include "src/exceptions/NotSupportedException.h"
 
 namespace storm {
     namespace expressions {
@@ -52,7 +53,7 @@ namespace storm {
         
         template<typename RationalNumberType>
         boost::any ToRationalNumberVisitor<RationalNumberType>::visit(BinaryRelationExpression const& expression) {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
+            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number.");
         }
         
         template<typename RationalNumberType>
@@ -62,30 +63,39 @@ namespace storm {
         
         template<typename RationalNumberType>
         boost::any ToRationalNumberVisitor<RationalNumberType>::visit(UnaryBooleanFunctionExpression const& expression) {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
+            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number.");
         }
         
         template<typename RationalNumberType>
         boost::any ToRationalNumberVisitor<RationalNumberType>::visit(UnaryNumericalFunctionExpression const& expression) {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
+            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number.");
         }
         
         template<typename RationalNumberType>
         boost::any ToRationalNumberVisitor<RationalNumberType>::visit(BooleanLiteralExpression const& expression) {
-            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational function.");
+            STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Expression cannot be translated into a rational number.");
         }
         
         template<typename RationalNumberType>
         boost::any ToRationalNumberVisitor<RationalNumberType>::visit(IntegerLiteralExpression const& expression) {
+#ifdef STORM_HAVE_CARL
             return RationalNumberType(carl::rationalize<storm::RationalNumber>(static_cast<size_t>(expression.getValue())));
+#else
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Rational numbers are not supported in this build.");
+#endif
         }
         
         template<typename RationalNumberType>
         boost::any ToRationalNumberVisitor<RationalNumberType>::visit(DoubleLiteralExpression const& expression) {
+#ifdef STORM_HAVE_CARL
             return RationalNumberType(carl::rationalize<storm::RationalNumber>(expression.getValue()));
+#else
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Rational numbers are not supported in this build.");
+#endif
         }
         
+#ifdef STORM_HAVE_CARL
         template class ToRationalNumberVisitor<storm::RationalNumber>;
-        
+#endif
     }
 }
diff --git a/src/storm-dyftee.cpp b/src/storm-dyftee.cpp
index 6b6f74d46..1bad1c994 100644
--- a/src/storm-dyftee.cpp
+++ b/src/storm-dyftee.cpp
@@ -139,7 +139,11 @@ int main(const int argc, const char** argv) {
         
         // From this point on we are ready to carry out the actual computations.
         if (parametric) {
+#ifdef STORM_HAVE_CARL
             analyzeDFT<storm::RationalFunction>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), allowModular && dftSettings.useModularisation(), !dftSettings.isDisableDC() );
+#else
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Parameters are not supported in this build.");
+#endif
         } else {
             analyzeDFT<double>(dftSettings.getDftFilename(), pctlFormula, dftSettings.useSymmetryReduction(), allowModular && dftSettings.useModularisation(), !dftSettings.isDisableDC());
         }
diff --git a/src/utility/constants.cpp b/src/utility/constants.cpp
index 4821d1b94..eafe4f1bd 100644
--- a/src/utility/constants.cpp
+++ b/src/utility/constants.cpp
@@ -40,6 +40,7 @@ namespace storm {
             return true;
         }
 
+#ifdef STORM_HAVE_CARL
         template<>
         bool isOne(storm::RationalNumber const& a) {
             return carl::isOne(a);
@@ -91,18 +92,19 @@ namespace storm {
             // FIXME: this should be treated more properly.
             return storm::RationalFunction(-1.0);
         }
+#endif
         
         template<typename ValueType>
         ValueType pow(ValueType const& value, uint_fast64_t exponent) {
             return std::pow(value, exponent);
         }
 
-		template<typename ValueType>
-		ValueType simplify(ValueType value) {
-            // In the general case, we don't do anything here, but merely return the value. If something else is
-            // supposed to happen here, the templated function can be specialized for this particular type.
-			return value;
-		}
+        template<typename ValueType>
+        ValueType simplify(ValueType value) {
+        // In the general case, we don't do anything here, but merely return the value. If something else is
+        // supposed to happen here, the templated function can be specialized for this particular type.
+                return value;
+        }
         
         template<>
         double convertNumber(double const& number){
@@ -114,6 +116,7 @@ namespace storm {
             return std::fabs(number);
         }
         
+#ifdef STORM_HAVE_CARL
         template<>
         RationalFunction& simplify(RationalFunction& value);
         
@@ -162,6 +165,7 @@ namespace storm {
         storm::RationalNumber abs(storm::RationalNumber const& number) {
             return carl::abs(number);
         }
+#endif
 
         template<typename IndexType, typename ValueType>
         storm::storage::MatrixEntry<IndexType, ValueType> simplify(storm::storage::MatrixEntry<IndexType, ValueType> matrixEntry) {
@@ -186,17 +190,17 @@ namespace storm {
         template bool isZero(double const& value);
         template bool isConstant(double const& value);
         
-		template double one();
-		template double zero();
-		template double infinity();
+        template double one();
+        template double zero();
+        template double infinity();
 
-		template double pow(double const& value, uint_fast64_t exponent);
+        template double pow(double const& value, uint_fast64_t exponent);
 
-		template double simplify(double value);
+        template double simplify(double value);
 
-		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double> matrixEntry);
-		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& matrixEntry);
-		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& matrixEntry);
+        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double> matrixEntry);
+        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& matrixEntry);
+        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& matrixEntry);
 
         template double abs(double const& number);
         
@@ -204,17 +208,17 @@ namespace storm {
         template bool isZero(float const& value);
         template bool isConstant(float const& value);
         
-		template float one();
-		template float zero();
-		template float infinity();
+        template float one();
+        template float zero();
+        template float infinity();
 
-		template float pow(float const& value, uint_fast64_t exponent);
+        template float pow(float const& value, uint_fast64_t exponent);
 
-		template float simplify(float value);
+        template float simplify(float value);
 
-		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> matrixEntry);
-		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& matrixEntry);
-		template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& matrixEntry);
+        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float> matrixEntry);
+        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>& matrixEntry);
+        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, float>&& matrixEntry);
         
         template bool isOne(int const& value);
         template bool isZero(int const& value);
@@ -252,6 +256,7 @@ namespace storm {
         template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>& matrixEntry);
         template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::storage::sparse::state_type>&& matrixEntry);
 
+#ifdef STORM_HAVE_CARL
         // Instantiations for rational number.
         template bool isOne(storm::RationalNumber const& value);
         template bool isZero(storm::RationalNumber const& value);
@@ -273,7 +278,7 @@ namespace storm {
         template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>& matrixEntry);
         template storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, storm::RationalNumber>&& matrixEntry);
         
-#ifdef STORM_HAVE_CARL
+        // Instantiations for rational function.
         template bool isOne(RationalFunction const& value);
         template bool isZero(RationalFunction const& value);
         template bool isConstant(RationalFunction const& value);
diff --git a/src/utility/graph.cpp b/src/utility/graph.cpp
index 8a7e1e185..79b4a32a0 100644
--- a/src/utility/graph.cpp
+++ b/src/utility/graph.cpp
@@ -22,6 +22,8 @@
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidArgumentException.h"
 
+#include <queue>
+
 namespace storm {
     namespace utility {
         namespace graph {
@@ -1180,24 +1182,21 @@ namespace storm {
             template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<float> const& matrix) ;
             
             // Instantiations for storm::RationalNumber.
+#ifdef STORM_HAVE_CARL
             template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps);
             
             template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix);
             
             template std::vector<uint_fast64_t> getDistances(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::BitVector const& initialStates, boost::optional<storm::storage::BitVector> const& subsystem);
             
-            
             template storm::storage::BitVector performProbGreater0(storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);
             
             template storm::storage::BitVector performProb1(storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0);
             
-            
             template storm::storage::BitVector performProb1(storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
             
-            
             template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::models::sparse::DeterministicModel<storm::RationalNumber> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
             
-            
             template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01(storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
             
             template storm::storage::PartialScheduler computeSchedulerProbGreater0E(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<storm::storage::BitVector> const& rowFilter);
@@ -1214,33 +1213,27 @@ namespace storm {
             
             template storm::storage::BitVector performProb1E(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
             
-            
             template storm::storage::BitVector performProb1E(storm::models::sparse::NondeterministicModel<storm::RationalNumber> const& model, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
             
             template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
             
-            
             template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Max(storm::models::sparse::NondeterministicModel<storm::RationalNumber> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
             
             template storm::storage::BitVector performProbGreater0A(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool useStepBound = false, uint_fast64_t maximalSteps = 0);
             
-            
             template storm::storage::BitVector performProb0E(storm::models::sparse::NondeterministicModel<storm::RationalNumber> const& model, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
-            template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,  storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
             
+            template storm::storage::BitVector performProb0E(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices,  storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
             
             template storm::storage::BitVector performProb1A( storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
             
             template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::storage::SparseMatrix<storm::RationalNumber> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::SparseMatrix<storm::RationalNumber> const& backwardTransitions, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) ;
             
-            
             template std::pair<storm::storage::BitVector, storm::storage::BitVector> performProb01Min(storm::models::sparse::NondeterministicModel<storm::RationalNumber> const& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
             
-            
             template std::vector<uint_fast64_t> getTopologicalSort(storm::storage::SparseMatrix<storm::RationalNumber> const& matrix);
             // End of instantiations for storm::RationalNumber.
             
-#ifdef STORM_HAVE_CARL
             template storm::storage::BitVector getReachableStates(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& constraintStates, storm::storage::BitVector const& targetStates, bool useStepBound, uint_fast64_t maximalSteps);
             
             template storm::storage::BitVector getBsccCover(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix);
diff --git a/src/utility/parametric.h b/src/utility/parametric.h
index 244e1c141..0805ec34d 100644
--- a/src/utility/parametric.h
+++ b/src/utility/parametric.h
@@ -10,6 +10,7 @@
 
 #include "src/adapters/CarlAdapter.h"
 
+#include <map>
 
 namespace storm {
     namespace utility {
diff --git a/src/utility/prism.cpp b/src/utility/prism.cpp
index 947d7e8a2..a34f5e531 100644
--- a/src/utility/prism.cpp
+++ b/src/utility/prism.cpp
@@ -9,6 +9,8 @@
 
 #include "src/exceptions/InvalidArgumentException.h"
 
+#include <boost/algorithm/string.hpp>
+
 namespace storm {
     namespace utility {
         namespace prism {
@@ -82,4 +84,4 @@ namespace storm {
             
         }
     }
-}
\ No newline at end of file
+}
diff --git a/src/utility/stateelimination.cpp b/src/utility/stateelimination.cpp
index 7076c3f15..e70bc6b02 100644
--- a/src/utility/stateelimination.cpp
+++ b/src/utility/stateelimination.cpp
@@ -202,6 +202,7 @@ namespace storm {
             template std::vector<uint_fast64_t> getDistanceBasedPriorities(storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<double> const& oneStepProbabilities, bool forward, bool reverse);
             template std::vector<uint_fast64_t> getStateDistances(storm::storage::SparseMatrix<double> const& transitionMatrix, storm::storage::SparseMatrix<double> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<double> const& oneStepProbabilities, bool forward);
             
+#ifdef STORM_HAVE_CARL
             template uint_fast64_t estimateComplexity(storm::RationalNumber const& value);
             template std::shared_ptr<StatePriorityQueue> createStatePriorityQueue(boost::optional<std::vector<uint_fast64_t>> const& distanceBasedStatePriorities, storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& oneStepProbabilities, storm::storage::BitVector const& states);
             template uint_fast64_t computeStatePenalty(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalNumber> const& backwardTransitions, std::vector<storm::RationalNumber> const& oneStepProbabilities);
@@ -215,6 +216,7 @@ namespace storm {
             template uint_fast64_t computeStatePenaltyRegularExpression(storm::storage::sparse::state_type const& state, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::FlexibleSparseMatrix<storm::RationalFunction> const& backwardTransitions, std::vector<storm::RationalFunction> const& oneStepProbabilities);
             template std::vector<uint_fast64_t> getDistanceBasedPriorities(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<storm::RationalFunction> const& oneStepProbabilities, bool forward, bool reverse);
             template std::vector<uint_fast64_t> getStateDistances(storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrix, storm::storage::SparseMatrix<storm::RationalFunction> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<storm::RationalFunction> const& oneStepProbabilities, bool forward);
+#endif
         }
     }
-}
\ No newline at end of file
+}
diff --git a/src/utility/storm.h b/src/utility/storm.h
index 49ef4bf04..d6b074832 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -220,6 +220,7 @@ namespace storm {
         }
     }
 
+#ifdef STORM_HAVE_CARL
     template<>
     inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> model, std::shared_ptr<storm::logic::Formula const> const& formula) {
         STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model.");
@@ -229,6 +230,7 @@ namespace storm {
     inline void generateCounterexample(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<storm::logic::Formula const> const& formula) {
         STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Unable to generate counterexample for parametric model.");
     }
+#endif
     
     template<typename ValueType>
     void generateCounterexamples(storm::prism::Program const& program, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
@@ -332,6 +334,7 @@ namespace storm {
 
     }
     
+#ifdef STORM_HAVE_CARL
     template<>
     inline std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> model, std::shared_ptr<storm::logic::Formula const> const& formula, bool onlyInitialStatesRelevant) {
         storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
@@ -349,7 +352,6 @@ namespace storm {
         return result;
     }
     
-#ifdef STORM_HAVE_CARL
     inline void exportParametricResultToFile(storm::RationalFunction const& result, storm::models::sparse::Dtmc<storm::RationalFunction>::ConstraintCollector const& constraintCollector, std::string const& path) {
         std::ofstream filestream;
         filestream.open(path);
diff --git a/src/utility/sylvan.h b/src/utility/sylvan.h
index 1dd236609..776b2640b 100644
--- a/src/utility/sylvan.h
+++ b/src/utility/sylvan.h
@@ -7,10 +7,14 @@
 #pragma clang diagnostic ignored "-Wgnu-zero-variadic-macro-arguments"
 #pragma clang diagnostic ignored "-Wdeprecated-register"
 #pragma clang diagnostic ignored "-Wc99-extensions"
+#pragma clang diagnostic ignored "-Wunknown-pragmas"
+#pragma GCC diagnostic push
+#pragma GCC diagnostic ignored "-Wpedantic"
 
 #include "sylvan_obj.hpp"
 #include "sylvan_storm_rational_function.h"
 
+#pragma GCC diagnostic pop
 #pragma clang diagnostic pop
 
 #endif /* STORM_STORAGE_DD_SYLVAN_SYLVAN_H_ */
\ No newline at end of file
diff --git a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
index 8caa788bb..b66c71f09 100644
--- a/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/EigenDtmcPrctlModelCheckerTest.cpp
@@ -60,6 +60,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die) {
     EXPECT_NEAR(11.0 / 3.0, quantitativeResult4[0], storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
 }
 
+#ifdef STORM_HAVE_CARL
 TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalNumber) {
     storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/die.pm");
     
@@ -159,7 +160,7 @@ TEST(EigenDtmcPrctlModelCheckerTest, Die_RationalFunction) {
     
     EXPECT_EQ(storm::RationalNumber(11) / storm::RationalNumber(3), quantitativeResult4[0].evaluate(instantiation));
 }
-
+#endif
 
 TEST(EigenDtmcPrctlModelCheckerTest, Crowds) {
     std::shared_ptr<storm::models::sparse::Model<double>> abstractModel = storm::parser::AutoParser<>::parseModel(STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.tra", STORM_CPP_BASE_PATH "/examples/dtmc/crowds/crowds5_5.lab", "", "");
diff --git a/test/functional/solver/EigenLinearEquationSolverTest.cpp b/test/functional/solver/EigenLinearEquationSolverTest.cpp
index 33d073c62..2cd90dc36 100644
--- a/test/functional/solver/EigenLinearEquationSolverTest.cpp
+++ b/test/functional/solver/EigenLinearEquationSolverTest.cpp
@@ -64,6 +64,7 @@ TEST(EigenLinearEquationSolver, SparseLU) {
     ASSERT_LT(std::abs(x[2] - (-1)), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
 }
 
+#ifdef STORM_HAVE_CARL
 TEST(EigenLinearEquationSolver, SparseLU_RationalNumber) {
     ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder<storm::RationalNumber> builder);
     storm::storage::SparseMatrixBuilder<storm::RationalNumber> builder;
@@ -115,6 +116,7 @@ TEST(EigenLinearEquationSolver, SparseLU_RationalFunction) {
     ASSERT_TRUE(x[1] == storm::RationalFunction(3));
     ASSERT_TRUE(x[2] == storm::RationalFunction(-1));
 }
+#endif
 
 TEST(EigenLinearEquationSolver, DGMRES) {
     ASSERT_NO_THROW(storm::storage::SparseMatrixBuilder<double> builder);
@@ -412,4 +414,4 @@ TEST(EigenLinearEquationSolver, MatrixVectorMultiplication) {
     storm::solver::EigenLinearEquationSolver<double> solver(A);
     ASSERT_NO_THROW(solver.repeatedMultiply(x, nullptr, 4));
     ASSERT_LT(std::abs(x[0] - 1), storm::settings::getModule<storm::settings::modules::EigenEquationSolverSettings>().getPrecision());
-}
\ No newline at end of file
+}