diff --git a/.github/workflows/Dockerfile.archlinux b/.github/workflows/Dockerfile.archlinux
index 9e6312e2f..1bf44a4d1 100644
--- a/.github/workflows/Dockerfile.archlinux
+++ b/.github/workflows/Dockerfile.archlinux
@@ -16,6 +16,7 @@ ARG no_threads=1
 
 # Specify Storm configuration (ON/OFF)
 ARG gurobi_support="ON"
+ARG mathsat_support="ON"
 ARG soplex_support="ON"
 ARG spot_support="ON"
 ARG developer="OFF"
@@ -51,6 +52,7 @@ WORKDIR /opt/storm/build
 RUN cmake .. -DCMAKE_BUILD_TYPE=$build_type \
              -DSTORM_PORTABLE=ON \
              -DSTORM_USE_GUROBI=$gurobi_support \
+             -DSTORM_USE_MATHSAT=$mathsat_support \
              -DSTORM_USE_SOPLEX=$soplex_support \
              -DSTORM_USE_SPOT_SYSTEM=$spot_support \
              -DSTORM_DEVELOPER=$developer \
diff --git a/.github/workflows/Dockerfile.doxygen b/.github/workflows/Dockerfile.doxygen
index 749bce87a..a358bc1ac 100644
--- a/.github/workflows/Dockerfile.doxygen
+++ b/.github/workflows/Dockerfile.doxygen
@@ -36,6 +36,7 @@ WORKDIR /opt/storm/build
 RUN cmake .. -DCMAKE_BUILD_TYPE=Release \
              -DSTORM_PORTABLE=ON \
              -DSTORM_USE_GUROBI=ON \
+             -DSTORM_USE_MATHSAT=ON \
              -DSTORM_USE_SOPLEX=ON \
              -DSTORM_USE_SPOT_SYSTEM=ON
 
diff --git a/.github/workflows/buildtest.yml b/.github/workflows/buildtest.yml
index bb0894913..2bcff9228 100644
--- a/.github/workflows/buildtest.yml
+++ b/.github/workflows/buildtest.yml
@@ -4,8 +4,8 @@ name: Build Test
 
 on:
   schedule:
-      # run daily
-      - cron: '0 6 * * *'
+    # run daily
+    - cron: '0 6 * * *'
   # needed to trigger the workflow manually
   workflow_dispatch:
   pull_request:
@@ -26,62 +26,67 @@ jobs:
              baseImg: "storm-dependencies:latest-debug",
              buildType: "Debug",
              Gurobi: "ON",
+             Mathsat: "ON",
              Soplex: "ON",
              Spot: "ON",
              Developer: "ON",
              ClnExact: "OFF",
              ClnRatfunc: "OFF",
              AllSanitizers: "ON",
-             cmakeArgs: "-DMSAT_ROOT=/opt/mathsat5"
-            }
+             cmakeArgs: ""
+          }
           - {name: "CLN exact; GMP rational functions; All dependencies",
              baseImg: "storm-dependencies:latest-debug",
              buildType: "Debug",
              Gurobi: "ON",
+             Mathsat: "ON",
              Soplex: "ON",
              Spot: "ON",
              Developer: "ON",
              ClnExact: "ON",
              ClnRatfunc: "OFF",
              AllSanitizers: "ON",
-             cmakeArgs: "-DMSAT_ROOT=/opt/mathsat5"
-            }
+             cmakeArgs: ""
+          }
           - {name: "CLN exact; CLN rational functions; All dependencies",
              baseImg: "storm-dependencies:latest-debug",
              buildType: "Debug",
              Gurobi: "ON",
+             Mathsat: "ON",
              Soplex: "ON",
              Spot: "ON",
              Developer: "ON",
              ClnExact: "ON",
              ClnRatfunc: "ON",
              AllSanitizers: "ON",
-             cmakeArgs: "-DMSAT_ROOT=/opt/mathsat5"
-            }
+             cmakeArgs: ""
+          }
           - {name: "GMP exact; CLN rational functions; No dependencies",
              baseImg: "storm-dependencies:latest-debug",
              buildType: "Debug",
              Gurobi: "OFF",
+             Mathsat: "OFF",
              Soplex: "OFF",
              Spot: "OFF",
              Developer: "ON",
              ClnExact: "OFF",
              ClnRatfunc: "ON",
              AllSanitizers: "ON",
-             cmakeArgs: "-DMSAT_ROOT="
-            }
+             cmakeArgs: ""
+          }
           - {name: "Minimal dependencies",
-            baseImg: "storm-basesystem:minimal_dependencies",
-            buildType: "Debug",
+             baseImg: "storm-basesystem:minimal_dependencies",
+             buildType: "Debug",
              Gurobi: "OFF",
+             Mathsat: "OFF",
              Soplex: "OFF",
              Spot: "OFF",
              Developer: "ON",
              ClnExact: "OFF",
              ClnRatfunc: "ON",
              AllSanitizers: "ON",
-             cmakeArgs: "-DMSAT_ROOT="
-            }
+             cmakeArgs: ""
+          }
     steps:
       - name: Git clone
         uses: actions/checkout@v4
@@ -91,6 +96,7 @@ jobs:
             --build-arg BASE_IMG=movesrwth/${{ matrix.config.baseImg }} \
             --build-arg build_type="${{ matrix.config.buildType }}" \
             --build-arg gurobi_support="${{ matrix.config.Gurobi }}" \
+            --build-arg mathsat_support="${{ matrix.config.Mathsat }}" \
             --build-arg soplex_support="${{ matrix.config.Soplex }}" \
             --build-arg spot_support="${{ matrix.config.Spot }}" \
             --build-arg developer="${{ matrix.config.Developer }}" \
@@ -129,21 +135,23 @@ jobs:
           - {name: "GCC",
              buildType: "Debug",
              Gurobi: "OFF",
+             Mathsat: "OFF",
              Soplex: "OFF",
              Spot: "OFF",
              Developer: "ON",
              cmakeArgs: "-DCMAKE_C_COMPILER=gcc -DCMAKE_CXX_COMPILER=g++ -DSTORM_USE_SPOT_SHIPPED=ON",
              packages: ""
-            }
+          }
           - {name: "Clang",
              buildType: "Debug",
              Gurobi: "OFF",
+             Mathsat: "OFF",
              Soplex: "OFF",
              Spot: "OFF",
              Developer: "ON",
              cmakeArgs: "-DCMAKE_C_COMPILER=clang -DCMAKE_CXX_COMPILER=clang++ -DSTORM_USE_SPOT_SHIPPED=ON",
              packages: "clang"
-            }
+          }
     steps:
       - name: Git clone
         uses: actions/checkout@v4
@@ -154,6 +162,7 @@ jobs:
           docker build -t movesrwth/storm:ci . \
             --build-arg build_type="${{ matrix.config.buildType }}" \
             --build-arg gurobi_support="${{ matrix.config.Gurobi }}" \
+            --build-arg mathsat_support="${{ matrix.config.Mathsat }}" \
             --build-arg soplex_support="${{ matrix.config.Soplex }}" \
             --build-arg spot_support="${{ matrix.config.Spot }}" \
             --build-arg developer="${{ matrix.config.Developer }}" \
@@ -185,7 +194,7 @@ jobs:
     runs-on: ubuntu-latest
     strategy:
       matrix:
-        distro: ["debian-12", "ubuntu-22.04", "ubuntu-24.04"]
+        distro: ["debian-12", "ubuntu-24.04"]
         buildType: ["Release"]
     steps:
       - name: Git clone
@@ -196,6 +205,7 @@ jobs:
             --build-arg BASE_IMG=movesrwth/storm-basesystem:${{ matrix.distro }} \
             --build-arg build_type="${{ matrix.buildType }}" \
             --build-arg gurobi_support="OFF" \
+            --build-arg mathsat_support="OFF" \
             --build-arg soplex_support="OFF" \
             --build-arg spot_support="OFF" \
             --build-arg no_threads=${NR_JOBS}
@@ -229,12 +239,12 @@ jobs:
              dockerTag: "ci-debug",
              baseImg: "storm-dependencies:latest-debug",
              Developer: "ON"
-            }
+          }
           - {name: "Release",
              dockerTag: "ci",
              baseImg: "storm-dependencies:latest",
              Developer: "OFF"
-            }
+          }
     steps:
       - name: Git clone
         uses: actions/checkout@v4
@@ -251,7 +261,7 @@ jobs:
             --build-arg developer="${{ matrix.buildType.Developer }}" \
             --build-arg cmake_args="${{ matrix.buildType.cmakeArgs }}" \
             --build-arg no_threads=${NR_JOBS}
-            # Omitting arguments gurobi_support, soplex_support, spot_support, cln_exact, cln_ratfunc, all_sanitizers
+            # Omitting arguments gurobi_support, mathsat_support, soplex_support, spot_support, cln_exact, cln_ratfunc, all_sanitizers
       - name: Run Docker
         run: docker run -d -it --name ci movesrwth/storm:${{ matrix.buildType.dockerTag }}
 
@@ -303,4 +313,4 @@ jobs:
             For more information, see https://github.com/${{ github.repository }}/actions/runs/${{ github.run_id }}"
           to: ${{ secrets.STORM_CI_MAIL_RECIPIENTS }}
           from: Github Actions <you-broke-it@stormchecker.org>
-        if: env.WORKFLOW_CONCLUSION != 'success' # notify only if failure
+        if: env.WORKFLOW_CONCLUSION != 'success' # notify only if failure
\ No newline at end of file
diff --git a/.github/workflows/release_docker.yml b/.github/workflows/release_docker.yml
index 18f1178f0..3fb29f327 100644
--- a/.github/workflows/release_docker.yml
+++ b/.github/workflows/release_docker.yml
@@ -39,7 +39,7 @@ jobs:
             --build-arg developer="${{ matrix.buildType.Developer }}" \
             --build-arg cmake_args="${{ matrix.buildType.cmakeArgs }}" \
             --build-arg no_threads=${NR_JOBS}
-            # Omitting arguments gurobi_support, soplex_support, spot_support, cln_exact, cln_ratfunc, all_sanitizers
+            # Omitting arguments gurobi_support, soplex_support, mathsat_support, spot_support, cln_exact, cln_ratfunc, all_sanitizers
       - name: Login to Docker Hub
         # Only login if using original repo
         if: github.repository_owner == 'moves-rwth'
diff --git a/CMakeLists.txt b/CMakeLists.txt
index 5b5ed63ad..fafe7aa2f 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -1,15 +1,11 @@
-cmake_minimum_required (VERSION 3.22)
-
-set(CMAKE_CXX_STANDARD 20)
+cmake_minimum_required (VERSION 3.23)
 
 # Set project name
 project (storm CXX C)
 
-# Add base folder for better inclusion paths
-#  include_directories("${PROJECT_SOURCE_DIR}/src")
-
-# Add the resources/cmake folder to Module Search Path for FindTBB.cmake
+# Add the resources/cmake folder to Module Search Path
 set(CMAKE_MODULE_PATH ${CMAKE_MODULE_PATH} "${PROJECT_SOURCE_DIR}/resources/cmake/find_modules" "${PROJECT_SOURCE_DIR}/resources/cmake/macros")
+add_custom_target(storm_resources)
 
 include(ExternalProject)
 include(RegisterSourceGroup)
@@ -18,6 +14,8 @@ include(CheckCXXSourceCompiles)
 include(CheckCSourceCompiles)
 include(ProcessorCount)
 
+set(CMAKE_CXX_STANDARD 20)
+
 #############################################################
 ##
 ##	CMake options of Storm
@@ -35,14 +33,10 @@ MARK_AS_ADVANCED(STORM_PORTABLE)
 option(STORM_FORCE_POPCNT "Sets whether the popcnt instruction is forced to be used (advanced)." OFF)
 MARK_AS_ADVANCED(STORM_FORCE_POPCNT)
 option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be linked statically." OFF)
-option(STORM_USE_INTELTBB "Sets whether the Intel TBB libraries should be used." OFF)
+set(STORM_CARL_GIT_REPO "https://github.com/sjunges/carl-storm.git" CACHE STRING "For fetching carl: which git repo to use")
+set(STORM_CARL_GIT_TAG "cmakeupdates" CACHE STRING "For fetching carl: which git tag to use")
 option(STORM_USE_GUROBI "Sets whether Gurobi should be used." OFF)
 option(STORM_USE_SOPLEX "Sets whether Soplex should be used." OFF)
-set(STORM_CARL_DIR_HINT "" CACHE STRING "A hint where the preferred CArL version can be found. If CArL cannot be found there, it is searched in the OS's default paths.")
-option(STORM_FORCE_SHIPPED_CARL "Sets whether the shipped version of carl is to be used no matter whether carl is found or not." OFF)
-MARK_AS_ADVANCED(STORM_FORCE_SHIPPED_CARL)
-option(USE_SMTRAT "Sets whether SMT-RAT should be included." OFF)
-mark_as_advanced(USE_SMTRAT)
 option(STORM_USE_SPOT_SYSTEM "Sets whether the system version of Spot should be included (if found)." ON)
 option(STORM_USE_SPOT_SHIPPED "Sets whether Spot should be downloaded and installed (if system version is not available or not used)." OFF)
 option(XML_SUPPORT "Sets whether xml based format parsing should be included." ON)
@@ -55,7 +49,7 @@ option(STORM_USE_CLN_EA "Sets whether CLN instead of GMP numbers should be used
 export_option(STORM_USE_CLN_EA)
 option(STORM_USE_CLN_RF "Sets whether CLN instead of GMP numbers should be used for rational functions." ON)
 export_option(STORM_USE_CLN_RF)
-option(BUILD_SHARED_LIBS "Build the Storm library dynamically" OFF)
+option(STORM_BUILD_SHARED_LIBS "Build the Storm library dynamically" ON)
 option(STORM_DEBUG_CUDD "Build CUDD in debug mode." OFF)
 MARK_AS_ADVANCED(STORM_DEBUG_CUDD)
 option(STORM_EXCLUDE_TESTS_FROM_ALL "If set, tests will not be compiled by default" OFF )
@@ -64,7 +58,9 @@ MARK_AS_ADVANCED(STORM_EXCLUDE_TESTS_FROM_ALL)
 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).")
 set(Z3_ROOT "" CACHE STRING "A hint to the root directory of Z3 (optional).")
-set(MSAT_ROOT "" CACHE STRING "The hint to the root directory of MathSAT (optional).")
+option(STORM_USE_XERCES "Sets whether MathSat should be included." OFF)
+set(MATHSAT_ROOT "" CACHE STRING "The hint to the root directory of MathSAT (optional).")
+MARK_AS_ADVANCED(MATHSAT_ROOT)
 set(SPOT_ROOT "" CACHE STRING "The hint to the root directory of Spot (optional).")
 MARK_AS_ADVANCED(SPOT_ROOT)
 option(STORM_LOAD_QVBS "Sets whether the Quantitative Verification Benchmark Set (QVBS) should be downloaded." OFF)
@@ -72,7 +68,10 @@ set(STORM_QVBS_ROOT "" CACHE STRING "The root directory of the Quantitative Veri
 MARK_AS_ADVANCED(STORM_QVBS_ROOT)
 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(USE_XERCESC ${XML_SUPPORT})
+option(STORM_USE_XERCES "Sets whether Xerces should be included." ON)
+set(XERCESC_ROOT "" CACHE STRING "A hint to the root directory of Xerces (optional).")
+MARK_AS_ADVANCED(XERCESC_ROOT)
+
 mark_as_advanced(USE_XERCESC)
 option(STORM_COMPILE_WITH_ADDRESS_SANITIZER "Sets whether to compile with AddressSanitizer enabled" OFF)
 option(STORM_COMPILE_WITH_ALL_SANITIZERS "Sets whether to compile with all sanitizers enabled" OFF)
@@ -80,6 +79,7 @@ option(STORM_COMPILE_WITH_COMPILATION_PROFILING "Compile with output to profile
 MARK_AS_ADVANCED(STORM_COMPILE_WITH_COMPILATION_PROFILING)
 
 
+
 if (STORM_COMPILE_WITH_ALL_SANITIZERS)
     set(STORM_COMPILE_WITH_ADDRESS_SANITIZER ON)
 endif()
@@ -101,10 +101,10 @@ mark_as_advanced(CMAKE_OSX_SYSROOT)
 mark_as_advanced(CMAKE_OSX_DEPLOYMENT_TARGET)
 
 # Offer the user the choice of overriding the installation directories
-set(INCLUDE_INSTALL_DIR include/ CACHE PATH "Installation directory for header files" )
-set(LIB_INSTALL_DIR lib/ CACHE PATH "Installation directory for libraries")
+set(STORM_INCLUDE_INSTALL_DIR include/storm CACHE PATH "Installation directory for header files" )
+set(STORM_LIB_INSTALL_DIR lib/storm CACHE PATH "Installation directory for libraries")
 #set(SYSCONFIG_INSTALL_DIR etc/carl/  CACHE PATH "Installation for system configuration files)
-set(BIN_INSTALL_DIR lib/ CACHE PATH "Installation directory for executables")
+set(STORM_BIN_INSTALL_DIR lib/storm CACHE PATH "Installation directory for executables")
 
 
 # Install dir for cmake files (info for other libraries that include Storm)
@@ -178,37 +178,19 @@ else()
 ENDIF()
 message(STATUS "Storm - Detected operating system ${OPERATING_SYSTEM}.")
 
-# Set compile flags for dependencies
-if(STORM_USE_CLN_EA OR STORM_USE_CLN_RF)
-	set(SHIPPED_CARL_USE_CLN_NUMBERS ON)
-	set(SHIPPED_CARL_USE_GINAC ON)
-else()
-	set(SHIPPED_CARL_USE_CLN_NUMBERS OFF)
-	set(SHIPPED_CARL_USE_GINAC OFF)
-endif()
-
-# Warning for Apple Silicon
-if(APPLE_SILICON)
-	message(WARNING "Compiling natively on Apple Silicon is experimental. Please report any issues to support@stormchecker.org.")
-endif()
 
 
-set(DYNAMIC_EXT ".so")
 set(STATIC_EXT ".a")
 set(LIB_PREFIX "lib")
 if(MACOSX)
 	set(DYNAMIC_EXT ".dylib")
-	set(STATIC_EXT ".a")
-	set(LIB_PREFIX "lib")
-elseif (WIN32)
-	set(DYNAMIC_EXT ".dll")
-	set(STATIC_EXT ".lib")
-	set(LIB_PREFIX "")
+else()
+	set(DYNAMIC_EXT ".so")
 endif()
 message(STATUS "Storm - Assuming extension for shared libraries: ${DYNAMIC_EXT}")
 message(STATUS "Storm - Assuming extension for static libraries: ${STATIC_EXT}")
 
-if(BUILD_SHARED_LIBS)
+if(STORM_BUILD_SHARED_LIBS)
     set(LIB_EXT ${DYNAMIC_EXT})
     message(STATUS "Storm - Build dynamic libraries.")
 else()
@@ -235,11 +217,13 @@ elseif ("${CMAKE_CXX_COMPILER_ID}" STREQUAL "AppleClang")
 	if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 7.3)
 		message(FATAL_ERROR "AppleClang version must be at least 7.3.")
 	elseif ((CMAKE_CXX_COMPILER_VERSION VERSION_EQUAL 11.0.0) OR (CMAKE_CXX_COMPILER_VERSION VERSION_GREATER 11.0.0))
-		message(WARNING "Disabling stack checks for AppleClang version 11.0.0 or higher.")
-		# Stack checks are known to produce errors with the following Clang versions:
-		# 11.0.0: Runtime errors (stack_not_16_byte_aligned_error) when invoking storm in release mode
-		# 11.0.3 and  12.0.0: Catching exceptions thrown within PRISM parser does not work (The exception just falls through)
-		set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -fno-stack-check")
+		if (CMAKE_CXX_COMPILER_VERSION VERSION_LESS 15.0.0)
+			message(WARNING "Disabling stack checks for AppleClang version 11.0.0 or higher.")
+			# Stack checks are known to produce errors with the following Clang versions:
+			# 11.0.0: Runtime errors (stack_not_16_byte_aligned_error) when invoking storm in release mode
+			# 11.0.3 and  12.0.0: Catching exceptions thrown within PRISM parser does not work (The exception just falls through)
+			set(CMAKE_CXX_FLAGS_RELEASE "${CMAKE_CXX_FLAGS_RELEASE} -fno-stack-check")
+		endif()
 	endif()
 
 	set(STORM_COMPILER_APPLECLANG ON)
@@ -414,9 +398,6 @@ if (STORM_DEVELOPER)
 			set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-documentation-unknown-command")
 			set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-missing-noreturn")
 			set(CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wno-missing-prototypes")
-
-
-
 		endif ()
 	else ()
 	    set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -Wall -Wextra")
@@ -483,7 +464,7 @@ SET(CMAKE_SKIP_BUILD_RPATH  FALSE)
 SET(CMAKE_BUILD_WITH_INSTALL_RPATH FALSE)
 
 # the RPATH to be used when installing
-SET(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/lib")
+SET(CMAKE_INSTALL_RPATH "${CMAKE_INSTALL_PREFIX}/lib;${CMAKE_INSTALL_PREFIX}/lib/storm")
 
 # don't add the automatically determined parts of the RPATH
 # which point to directories outside the build tree to the install RPATH
@@ -560,14 +541,17 @@ if (STORM_GIT_VERSION_STRING MATCHES "NOTFOUND")
 	set(STORM_VERSION_SOURCE "VersionSource::Static")
 	set(STORM_VERSION_COMMITS_AHEAD 0)
 	set(STORM_VERSION_DIRTY DirtyState::Unknown)
+	set(STORM_VERSION_TWEAK 0)
 	include(version.cmake)
 	message(WARNING "Storm - Git version information not available, statically assuming version ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}.")
 else()
 	set(STORM_VERSION_SOURCE "VersionSource::Git")
 	if ("${STORM_VERSION_APPENDIX}" MATCHES "^.*dirty.*$")
 		set(STORM_VERSION_DIRTY "DirtyState::Dirty")
+		set(STORM_VERSION_TWEAK 1)
 	else()
 		set(STORM_VERSION_DIRTY "DirtyState::Clean")
+		set(STORM_VERSION_TWEAK 0)
 	endif()
 endif()
 
@@ -608,9 +592,6 @@ configure_file (
 	"${PROJECT_BINARY_DIR}/include/storm-config.h"
 )
 
-# Add the binary dir include directory for storm-config.h
-include_directories("${PROJECT_BINARY_DIR}/include")
-
 include(CTest)
 # Compiles all tests
 add_custom_target(tests)
@@ -620,8 +601,11 @@ set(CMAKE_CTEST_COMMAND_VERBOSE ${CMAKE_CTEST_COMMAND} -V)
 add_custom_target(check-verbose COMMAND ${CMAKE_CTEST_COMMAND_VERBOSE})
 add_dependencies(check tests)
 add_dependencies(check-verbose tests)
-# Apply code formatting
-add_custom_target(format COMMAND ${PROJECT_SOURCE_DIR}/resources/scripts/auto-format.sh)
+
+if(PROJECT_IS_TOP_LEVEL)
+	# Apply code formatting
+	add_custom_target(format COMMAND ${PROJECT_SOURCE_DIR}/resources/scripts/auto-format.sh)
+endif()
 
 set(STORM_TARGETS "")
 add_subdirectory(src)
@@ -632,8 +616,8 @@ export_option(STORM_HAVE_GUROBI)
 
 include(export)
 
-install(FILES ${CMAKE_BINARY_DIR}/stormConfig.install.cmake DESTINATION ${CMAKE_INSTALL_DIR} RENAME stormConfig.cmake)
-install(FILES ${CMAKE_BINARY_DIR}/stormConfigVersion.cmake DESTINATION ${CMAKE_INSTALL_DIR})
+install(FILES ${PROJECT_BINARY_DIR}/stormConfig.install.cmake DESTINATION ${CMAKE_INSTALL_DIR} RENAME stormConfig.cmake)
+install(FILES ${PROJECT_BINARY_DIR}/stormConfigVersion.cmake DESTINATION ${CMAKE_INSTALL_DIR})
 install(EXPORT storm_Targets FILE stormTargets.cmake DESTINATION ${CMAKE_INSTALL_DIR})
 
 include(StormCPackConfig.cmake)
diff --git a/Dockerfile b/Dockerfile
index b08afb16c..000a85a3d 100644
--- a/Dockerfile
+++ b/Dockerfile
@@ -26,6 +26,7 @@ ARG spot_support="ON"
 ARG developer="OFF"
 ARG cln_exact="OFF"
 ARG cln_ratfunc="ON"
+ARG mathsat_support="ON"
 ARG all_sanitizers="OFF"
 
 # Specify additional CMake arguments for Storm
@@ -48,6 +49,7 @@ WORKDIR /opt/storm/build
 RUN cmake .. -DCMAKE_BUILD_TYPE=$build_type \
              -DSTORM_PORTABLE=ON \
              -DSTORM_USE_GUROBI=$gurobi_support \
+             -DSTORM_USE_MATHSAT=$mathsat_support \
              -DSTORM_USE_SOPLEX=$soplex_support \
              -DSTORM_USE_SPOT_SYSTEM=$spot_support \
              -DSTORM_DEVELOPER=$developer \
diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index 14ea1b017..45ed35d44 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -1,4 +1,8 @@
-add_custom_target(resources)
+
+if(PROJECT_TOP_LEVEL)
+    add_custom_target(resources)
+    add_dependencies(resources storm_resources)
+endif()
 add_custom_target(test-resources)
 
 set(STORM_3RDPARTY_SOURCE_DIR ${PROJECT_SOURCE_DIR}/resources/3rdparty)
@@ -27,7 +31,7 @@ ExternalProject_Add(
 )
 ExternalProject_Get_Property(l3pp_ext source_dir)
 set(l3pp_INCLUDE "${source_dir}/")
-add_imported_library_interface(l3pp "${l3pp_INCLUDE}")
+storm_add_imported_library_interface(l3pp "${l3pp_INCLUDE}" "")
 list(APPEND STORM_DEP_TARGETS l3pp)
 add_dependencies(l3pp l3pp_ext)
 
@@ -37,7 +41,7 @@ add_dependencies(l3pp l3pp_ext)
 ##
 #############################################################
 
-add_imported_library_interface(gmm "${STORM_3RDPARTY_SOURCE_DIR}/gmm-5.2/include")
+storm_add_imported_library_interface(gmm "${STORM_3RDPARTY_SOURCE_DIR}/gmm-5.2/include" "")
 list(APPEND STORM_DEP_TARGETS gmm)
 
 #############################################################
@@ -65,12 +69,10 @@ ExternalProject_Add(
         INSTALL_COMMAND ""
         LOG_INSTALL ON
 )
-add_imported_library_interface(StormEigen "${STORM_3RDPARTY_INCLUDE_DIR}")
+storm_add_imported_library_interface(StormEigen "${STORM_3RDPARTY_INCLUDE_DIR}" "")
 list(APPEND STORM_DEP_TARGETS StormEigen)
 add_dependencies(StormEigen eigen_src)
 
-
-
 #############################################################
 ##
 ##	Boost
@@ -82,13 +84,14 @@ set(Boost_USE_STATIC_LIBS ${USE_BOOST_STATIC_LIBRARIES})
 set(Boost_USE_MULTITHREADED ON)
 set(Boost_USE_STATIC_RUNTIME OFF)
 set(Boost_NO_BOOST_CMAKE ON)
+set(Boost_NO_WARN_NEW_VERSIONS ON)
 
 find_package(Boost 1.65.1 QUIET REQUIRED COMPONENTS filesystem system)
 if (NOT Boost_FOUND)
     if (Boost_VERSION)
-	message(FATAL_ERROR "The required Boost version is 1.65.1 or newer, however, only ${Boost_VERSION} was found.")
+        message(FATAL_ERROR "The required Boost version is 1.65.1 or newer, however, only ${Boost_VERSION} was found.")
     else ()
-   	message(FATAL_ERROR "Boost was not found.")
+        message(FATAL_ERROR "Boost was not found.")
     endif ()
 endif ()
 if ((NOT Boost_LIBRARY_DIRS) OR ("${Boost_LIBRARY_DIRS}" STREQUAL ""))
@@ -97,7 +100,7 @@ endif ()
 
 if (${Boost_VERSION} VERSION_GREATER_EQUAL "1.81.0")
     message(STATUS "Storm - Using workaround for Boost >= 1.81")
-    set (CMAKE_CXX_FLAGS "${CMAKE_CXX_FLAGS} -DBOOST_PHOENIX_STL_TUPLE_H_")
+    add_compile_options(-DBOOST_PHOENIX_STL_TUPLE_H_) # or add compile_definitions?
 endif()
 
 set(CNTVAR 1)
@@ -110,6 +113,7 @@ message(STATUS "Storm - Using boost ${Boost_VERSION} (library version ${Boost_LI
 # set the information for the config header
 set(STORM_BOOST_INCLUDE_DIR "${Boost_INCLUDE_DIRS}")
 
+
 #############################################################
 ##
 ##	ExprTk
@@ -118,11 +122,9 @@ set(STORM_BOOST_INCLUDE_DIR "${Boost_INCLUDE_DIRS}")
 
 # Use the shipped version of ExprTK
 message (STATUS "Storm - Including ExprTk.")
-add_imported_library_interface(ExprTk "${STORM_3RDPARTY_SOURCE_DIR}/exprtk")
+storm_add_imported_library_interface(ExprTk "${STORM_3RDPARTY_SOURCE_DIR}/exprtk" "")
 list(APPEND STORM_DEP_TARGETS ExprTk)
 
-
-
 #############################################################
 ##
 ##	Parallel Hashmap
@@ -131,24 +133,8 @@ list(APPEND STORM_DEP_TARGETS ExprTk)
 
 # Use the shipped version of Parallel Hashmap
 message (STATUS "Storm - Including Parallel Hashmap.")
-set(PHMAP_INCLUDE_DIR "${STORM_3RDPARTY_SOURCE_DIR}/parallel_hashmap/parallel_hashmap")
-file(GLOB PHMAP_HEADERS "${PHMAP_INCLUDE_DIR}/*.h")
-
-# Add the parallel_hashmap headers to the headers that are copied to the include directory in the build directory.
-set(PHMAP_BINDIR_DIR ${STORM_3RDPARTY_INCLUDE_DIR}/parallel_hashmap)
-include_directories("${PHMAP_BINDIR_DIR}")
-foreach(HEADER ${PHMAP_HEADERS})
-    string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER})
-    string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH})
-    string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH})
-    add_custom_command(
-        OUTPUT ${PHMAP_BINDIR_DIR}/parallel_hashmap/${HEADER_FILENAME}
-        COMMAND ${CMAKE_COMMAND} -E make_directory ${PHMAP_BINDIR_DIR}/parallel_hashmap
-        COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${PHMAP_BINDIR_DIR}/parallel_hashmap/${HEADER_FILENAME}
-        DEPENDS ${PHMAP_INCLUDE_DIR}/${HEADER_FILENAME}
-    )
-    list(APPEND PHMAP_BINDIR_HEADERS ${PHMAP_BINDIR_DIR}/parallel_hashmap/${HEADER_FILENAME})
-endforeach()
+storm_add_imported_library_interface(phmap "${STORM_3RDPARTY_SOURCE_DIR}/parallel_hashmap" "")
+list(APPEND STORM_DEP_TARGETS phmap)
 
 #############################################################
 ##
@@ -158,7 +144,8 @@ endforeach()
 
 # Use the shipped version of cpphoafparser
 message (STATUS "Storm - Including cpphoafparser 0.99.2")
-include_directories("${STORM_3RDPARTY_SOURCE_DIR}/cpphoafparser-0.99.2/include")
+storm_add_imported_library_interface(cppHOAparser "${STORM_3RDPARTY_SOURCE_DIR}/cpphoafparser-0.99.2/include" "")
+list(APPEND STORM_DEP_TARGETS cppHOAparser)
 
 #############################################################
 ##
@@ -168,7 +155,7 @@ include_directories("${STORM_3RDPARTY_SOURCE_DIR}/cpphoafparser-0.99.2/include")
 
 #use the shipped version of modernjson
 message (STATUS "Storm - Including ModernJSON.")
-add_imported_library_interface(ModernJSON "${STORM_3RDPARTY_SOURCE_DIR}/modernjson/include/")
+storm_add_imported_library_interface(ModernJSON "${STORM_3RDPARTY_SOURCE_DIR}/modernjson/include/" "")
 list(APPEND STORM_DEP_TARGETS ModernJSON)
 
 #############################################################
@@ -276,218 +263,110 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_cudd.cmake)
 
 #############################################################
 ##
-##      carl
+##      carl (including cln and ginac)
 ##
 #############################################################
+# Boost must have been configured above. It would be good to check that.
 
-set(STORM_HAVE_CARL OFF)
-set(CARL_MINVERSION "14.26")
-set(CARL_C14VERSION "14")
-if (NOT STORM_FORCE_SHIPPED_CARL)
-    if (NOT "${STORM_CARL_DIR_HINT}" STREQUAL "")
-		find_package(carl QUIET PATHS ${STORM_CARL_DIR_HINT} NO_DEFAULT_PATH)
-    endif()
-	if (NOT carl_FOUND)
-		find_package(carl QUIET)
-    endif()
-endif()
 
-set(STORM_SHIPPED_CARL OFF)
-if(carl_FOUND AND NOT STORM_FORCE_SHIPPED_CARL)
-    get_target_property(carlLOCATION lib_carl LOCATION)
-    if("${carlLOCATION}" STREQUAL "carlLOCATION-NOTFOUND")
-        if(EXISTS ${STORM_3RDPARTY_BINARY_DIR}/carl)
-            message(WARNING "Storm - Library for carl location is not found but the directory ${STORM_3RDPARTY_BINARY_DIR}/carl exists. Will (re-)try to build a shipped version of carl.")
-            set(STORM_SHIPPED_CARL ON)
-        else()
-            message(FATAL_ERROR "Library location for carl is not found, did you build carl?")
-        endif()
-    elseif(EXISTS ${carlLOCATION})
-        #empty on purpose
-    else()
-        if(EXISTS ${STORM_3RDPARTY_BINARY_DIR}/carl)
-            message(WARNING "Storm - File ${carlLOCATION} does not exist but the directory ${STORM_3RDPARTY_BINARY_DIR}/carl exists. Will (re-)try to build a shipped version of carl.")
-            set(STORM_SHIPPED_CARL ON)
-        else()
-            message(FATAL_ERROR "File ${carlLOCATION} does not exist, did you build carl?")
-        endif()
-    endif()
-    if("${carl_VERSION_MAJOR}" STREQUAL "${CARL_C14VERSION}")
-        message(STATUS "Storm - Found carl-storm version")
-        # empty on purpose. Maybe put a warning here?
-        if("${carl_VERSION_MAJOR}.${carl_VERSION_MINOR}" VERSION_LESS "${CARL_MINVERSION}")
-            message(FATAL_ERROR "Carl version outdated. We require ${CARL_MINVERSION}. Found ${carl_VERSION_MAJOR}.${carl_VERSION_MINOR} at ${carlLOCATION}")
-        endif()
-    else()
-        message(FATAL_ERROR "We only support a diverged version of carl, indicated by Carl version 14.x. These versions can be found at https://github.com/moves-rwth/carl-storm. 
-			      On this system, we found ${carl_VERSION_MAJOR}.${carl_VERSION_MINOR} at ${carlLOCATION}")
-    endif()
-
-    set(STORM_HAVE_CARL ON)
-    message(STATUS "Storm - Use system version of carl.")
-    message(STATUS "Storm - Linking with preinstalled carl ${carl_VERSION} (include: ${carl_INCLUDE_DIR}, library ${carl_LIBRARIES}, CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}, CARL_USE_GINAC: ${CARL_USE_GINAC}).")
-    set(STORM_HAVE_CLN ${CARL_USE_CLN_NUMBERS})
-    set(STORM_HAVE_GINAC ${CARL_USE_GINAC})
+# Set compile flags for dependencies
+if(STORM_USE_CLN_EA OR STORM_USE_CLN_RF)
+    set(SHIPPED_CARL_USE_CLN_NUMBERS ON)
+    set(SHIPPED_CARL_USE_GINAC ON)
 else()
-    set(STORM_SHIPPED_CARL ON)
+    set(SHIPPED_CARL_USE_CLN_NUMBERS OFF)
+    set(SHIPPED_CARL_USE_GINAC OFF)
 endif()
 
-if (STORM_SHIPPED_CARL)
-	# The first external project will be built at *configure stage*
-	message(STATUS "Carl - Start of config process")
-	file(MAKE_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download)
-	execute_process(
-	COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}" "-DBoost_LIBRARY_DIRS=${Boost_LIBRARY_DIRS}" "-DBoost_INCLUDE_DIRS=${Boost_INCLUDE_DIRS}" "-DUse_CLN_NUMBERS=${SHIPPED_CARL_USE_CLN_NUMBERS}" "-DUse_GINAC=${SHIPPED_CARL_USE_GINAC}"
-	WORKING_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download
-	OUTPUT_VARIABLE carlconfig_out
-	RESULT_VARIABLE carlconfig_result)
-
-	if(NOT carlconfig_result)
-		message(STATUS "${carlconfig_out}")
-	endif()
-	execute_process(
-		COMMAND ${CMAKE_COMMAND} --build . --target carl-config
-		WORKING_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download
-		OUTPUT_VARIABLE carlconfig_out
-		RESULT_VARIABLE carlconfig_result
-		)
-		if(NOT carlconfig_result)
-		message(STATUS "${carlconfig_out}")
-	endif()
-    message(STATUS "Carl - End of config process")
-
-    message(STATUS "Storm - Using shipped version of carl.")
-    ExternalProject_Add(
-            carl
-            SOURCE_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl
-            CONFIGURE_COMMAND ""
-            BUILD_IN_SOURCE 1
-            BUILD_COMMAND make lib_carl -j${STORM_RESOURCES_BUILD_JOBCOUNT}
-            INSTALL_COMMAND make install -j${STORM_RESOURCES_BUILD_JOBCOUNT}
-            LOG_BUILD ON
-			LOG_INSTALL ON
-            BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT}
-    )
-    include(${STORM_3RDPARTY_BINARY_DIR}/carl/carlConfig.cmake)
-
-    set(STORM_HAVE_CLN ${CARL_USE_CLN_NUMBERS})
-    set(STORM_HAVE_GINAC ${CARL_USE_GINAC})
+set(STORM_HAVE_CARL OFF)
+set(CARL_MINVERSION "14.26")
+set(CARL_C14VERSION "14")
 
-	add_dependencies(resources carl)
-    set(carl_INCLUDE_DIR "${STORM_3RDPARTY_BINARY_DIR}/carl/include/")
-    set(carl_DIR "${STORM_3RDPARTY_BINARY_DIR}/carl/")
-    set(carl_LIBRARIES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT})
-    set(STORM_HAVE_CARL ON)
+include(FetchContent)
+FETCHCONTENT_DECLARE(
+        carl
+        GIT_REPOSITORY ${STORM_CARL_GIT_REPO}
+        GIT_TAG ${STORM_CARL_GIT_TAG}
+)
+SET(EXCLUDE_TESTS_FROM_ALL ON)
+SET(THREAD_SAFE ON)
+SET(Boost_NO_SYSTEM_PATHS ON)
+SET(BOOST_INCLUDEDIR ${Boost_INCLUDE_DIRS})
+SET(BOOST_LIBRARYDIR ${Boost_LIBRARY_DIRS})
+SET(USE_CLN_NUMBERS ${SHIPPED_CARL_USE_CLN_NUMBERS})
+SET(CARL_LIB_INSTALL_DIR "lib/storm")
+SET(CARL_INCLUDE_INSTALL_DIR "include/storm")
+SET(CARL_EXPORT_TO_CMAKE OFF)
+FETCHCONTENT_MAKEAVAILABLE(carl)
+
+
+include(${carl_BINARY_DIR}/carlConfig.cmake)
+#
+set(STORM_HAVE_CLN ${CARL_USE_CLN_NUMBERS})
+message(STATUS "carl version ${carl_VERSION} use cln: ${STORM_HAVE_CLN}")
+set(STORM_HAVE_GINAC ${CARL_USE_GINAC})
+#
+add_dependencies(storm_resources lib_carl)
+set(STORM_HAVE_CARL ON)
+set(STORM_CARL_SUPPORTS_FWD_DECL ON)
 
-    message(STATUS "Storm - Linking with shipped carl ${carl_VERSION} (include: ${carl_INCLUDE_DIR}, library ${carl_LIBRARIES}, CARL_USE_CLN_NUMBERS: ${CARL_USE_CLN_NUMBERS}, CARL_USE_GINAC: ${CARL_USE_GINAC}).")
 
-    # install the carl dynamic library if we built it
-    if(MACOSX)
-        install(FILES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl.${carl_VERSION}${DYNAMIC_EXT} DESTINATION lib)
-    else()
-        install(FILES ${STORM_3RDPARTY_BINARY_DIR}/carl/lib/libcarl${DYNAMIC_EXT}.${carl_VERSION} DESTINATION lib)
-    endif()
-endif()
+# The library that needs symbols must be first, then the library that resolves the symbol.
+list(APPEND STORM_DEP_IMP_TARGETS lib_carl)
+list(APPEND STORM_DEP_IMP_TARGETS GMPXX_SHARED GMP_SHARED)
 
-if("${carl_VERSION_MAJOR}.${carl_VERSION_MINOR}" VERSION_EQUAL "14.22")
-    # This version is too old for forward declarations and updating requires moving the git,
-    # so we warn users but start warning them now.
-    set(STORM_CARL_SUPPORTS_FWD_DECL OFF)
-    message(WARNING "Uses an outdated repo for Carl. Carl is now hosted at https://github.com/moves-rwth/carl-storm")
-elseif("${carl_VERSION_MAJOR}.${carl_VERSION_MINOR}" VERSION_EQUAL "14.23")
-    # This version is too old for forward declarations, but we keep supporting it for the moment.
-    set(STORM_CARL_SUPPORTS_FWD_DECL OFF)
-else()
-    set(STORM_CARL_SUPPORTS_FWD_DECL ON)
-endif()
 
 if(STORM_USE_CLN_RF AND NOT STORM_HAVE_CLN)
-	message(FATAL_ERROR "Cannot use CLN numbers if carl is build without.")
+    message(FATAL_ERROR "Cannot use CLN numbers if carl is build without.")
 endif()
 if(STORM_USE_CLN_RF AND NOT STORM_HAVE_GINAC)
     message(FATAL_ERROR "Cannot use CLN numbers if carl is build without ginac.")
 endif()
 
-# The library that needs symbols must be first, then the library that resolves the symbol.
-list(APPEND STORM_DEP_IMP_TARGETS lib_carl)
-if(STORM_USE_CLN_EA OR STORM_USE_CLN_RF)
-    list(APPEND STORM_DEP_IMP_TARGETS GINAC_SHARED CLN_SHARED)
-endif()
-list(APPEND STORM_DEP_IMP_TARGETS GMPXX_SHARED GMP_SHARED)
-
-
-#############################################################
-##
-##      SMT-RAT
-##
-#############################################################
 
-set(STORM_HAVE_SMTRAT OFF)
-if(USE_SMTRAT)
-	find_package(smtrat QUIET REQUIRED)
-	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})
-	else()
-		message(FATAL_ERROR "Storm - SMT-RAT was requested but not found")
-	endif()
+if(STORM_HAVE_CLN)
+    get_target_property(CLN_INCLUDE_DIR CLN_SHARED INTERFACE_INCLUDE_DIRECTORIES)
 endif()
 
-
-#############################################################
-##
-##	gmp
-##
-#############################################################
-
-get_target_property(GMPXX_LIB GMPXX_SHARED IMPORTED_LIB_LOCATION)
-get_target_property(GMP_LIB GMP_SHARED IMPORTED_LIB_LOCATION)
-get_target_property(GMPXX_INCLUDE_DIR GMPXX_SHARED INTERFACE_INCLUDE_DIRECTORIES)
-get_target_property(GMP_INCLUDE_DIR GMP_SHARED INTERFACE_INCLUDE_DIRECTORIES)
-get_filename_component(GMP_LIB_LOCATION ${GMP_LIB} DIRECTORY)
-get_filename_component(GMPXX_LIB_LOCATION ${GMPXX_LIB} DIRECTORY)
-
-
-#############################################################
-##
-##	cln
-##
-#############################################################
-
-if(STORM_HAVE_CLN)
-	get_target_property(CLN_INCLUDE_DIR CLN_SHARED INTERFACE_INCLUDE_DIRECTORIES)
+if(STORM_USE_CLN_EA OR STORM_USE_CLN_RF)
+    list(APPEND STORM_DEP_IMP_TARGETS GINAC_SHARED CLN_SHARED)
 endif()
 
+#
+#get_target_property(GMPXX_LIB GMPXX_SHARED IMPORTED_LIB_LOCATION)
+#get_target_property(GMP_LIB GMP_SHARED IMPORTED_LIB_LOCATION)
+#get_target_property(GMPXX_INCLUDE_DIR GMPXX_SHARED INTERFACE_INCLUDE_DIRECTORIES)
+#get_target_property(GMP_INCLUDE_DIR GMP_SHARED INTERFACE_INCLUDE_DIRECTORIES)
+#get_filename_component(GMP_LIB_LOCATION ${GMP_LIB} DIRECTORY)
+#get_filename_component(GMPXX_LIB_LOCATION ${GMPXX_LIB} DIRECTORY)
+#
+
 #############################################################
 ##
 ##	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.")
-    if(${OPERATING_SYSTEM} MATCHES "Linux")
-        find_library(MSAT_LIB mathsat PATHS "${MSAT_ROOT}/lib")
-        add_imported_library(msat SHARED ${MSAT_LIB} "${MSAT_ROOT}/include")
-        list(APPEND STORM_DEP_TARGETS msat_SHARED)
+if (STORM_USE_MATHSAT)
+    find_package(MATHSAT QUIET)
+    if(MATHSAT_FOUND)
+        set(STORM_HAVE_MATHSAT ON)
+        if(${OPERATING_SYSTEM} MATCHES "Linux")
+            add_imported_library(mathsat SHARED ${MATHSAT_LIBRARIES} ${MATHSAT_INCLUDE_DIRS})
+            list(APPEND STORM_DEP_TARGETS mathsat_SHARED)
+            message(STATUS "Storm - Linking with MathSAT: (library: ${mathsat_SHARED}; include: ${MATHSAT_INCLUDE_DIRS})")
+        else()
+            # on macOS, the .dylib file has some hard coded path (Version 5.5.4) and we therefore link statically
+            add_imported_library(mathsat STATIC ${MATHSAT_LIB} ${MATHSAT_INCLUDE_DIRS})
+            list(APPEND STORM_DEP_TARGETS mathsat_STATIC)
+            message(STATUS "Storm - Linking with MathSAT: (library: ${mathsat_STATIC}; include: ${MATHSAT_INCLUDE_DIRS})")
+        endif()
     else()
-		# on macOS, the .dylib file has some hard coded path (Version 5.5.4).
-		# we thus link statically
-        find_library(MSAT_LIB NAMES libmathsat${STATIC_EXT} mathsat PATHS "${MSAT_ROOT}/lib")
-        add_imported_library(msat STATIC ${MSAT_LIB} "${MSAT_ROOT}/include")
-        list(APPEND STORM_DEP_TARGETS msat_STATIC)
+        set(STORM_HAVE_MATHSAT OFF)
+        message(FATAL_ERROR "Storm - MathSAT library requested but was not found. Make sure that MATHSAT_ROOT points to the correct directory.")
     endif()
-endif(ENABLE_MSAT)
+else()
+    set(STORM_HAVE_MATHSAT OFF)
+endif()
 
 #############################################################
 ##
@@ -508,7 +387,7 @@ if (STORM_LOAD_QVBS)
             INSTALL_COMMAND ""
             LOG_INSTALL ON
     )
-    add_dependencies(resources download_qvbs)
+    add_dependencies(storm_resources download_qvbs)
     set(STORM_HAVE_QVBS ON)
     ExternalProject_Get_Property(download_qvbs source_dir)
     set(STORM_QVBS_ROOT "${source_dir}/benchmarks")
@@ -554,12 +433,6 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_spot.cmake)
 ##
 #############################################################
 
-if(STORM_SHIPPED_CARL)
-    set(sylvan_dep carl)
-else()
-    set(sylvan_dep lib_carl)
-endif()
-
 if (STORM_DEBUG_SYLVAN)
     set(SYLVAN_BUILD_TYPE "Debug")
 else()
@@ -571,14 +444,14 @@ ExternalProject_Add(
         DOWNLOAD_COMMAND ""
         PREFIX "sylvan"
         SOURCE_DIR ${STORM_3RDPARTY_SOURCE_DIR}/sylvan
-        CMAKE_ARGS -DPROJECT_NAME=storm -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DSYLVAN_BUILD_DOCS=OFF -DSYLVAN_BUILD_EXAMPLES=OFF -DCMAKE_BUILD_TYPE=${SYLVAN_BUILD_TYPE} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DSYLVAN_GMP=ON -DUSE_CARL=ON -Dcarl_DIR=${carl_DIR} -DBUILD_SHARED_LIBS=OFF
+        CMAKE_ARGS -DPROJECT_NAME=storm -DCMAKE_C_COMPILER=${CMAKE_C_COMPILER} -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DSYLVAN_BUILD_DOCS=OFF -DSYLVAN_BUILD_EXAMPLES=OFF -DCMAKE_BUILD_TYPE=${SYLVAN_BUILD_TYPE} -DCMAKE_POSITION_INDEPENDENT_CODE=ON -DSYLVAN_GMP=ON -DUSE_CARL=ON -Dcarl_DIR=${carl_BINARY_DIR} -DBUILD_SHARED_LIBS=OFF
         BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan
         BUILD_IN_SOURCE 0
         INSTALL_COMMAND ""
         INSTALL_DIR ${STORM_3RDPARTY_BINARY_DIR}/sylvan
         LOG_CONFIGURE ON
         LOG_BUILD ON
-        DEPENDS ${sylvan_dep}
+        DEPENDS lib_carl
         BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/sylvan/src/libsylvan${STATIC_EXT}
         BUILD_ALWAYS 1
 )
@@ -632,69 +505,14 @@ set(GTEST_LIBRARIES ${binary_dir}/lib/libgtest${STATIC_EXT} ${binary_dir}/lib/li
 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)
-    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)
-	# Under Linux libtbb.so contains a linker script to libtbb.so.2 instead of a symlink.
-	# This breaks CMake.
-        # As a workaround we manually try to add the necessary suffix ".2" to the so file and hope for the best.
-	if (LINUX)
-		# Check if the library is a linker script which only links to the correct library
-		# Read first bytes of file
-		file(READ "${TBB_LIBRARY}" TMPTXT LIMIT 128)
-		# Check if file starts with "INPUT (libtbb.so.2)"
-		if("${TMPTXT}" MATCHES "INPUT \\(libtbb\\.so\\.(.*)\\)")
-			# Manually set library by adding the suffix from the linker script.
-			# CMAKE_MATCH_1 contains the parsed suffix.
-			set(TBB_LIB_LINUX "${TBB_LIBRARY}.${CMAKE_MATCH_1}")
-			set(TBB_MALLOC_LIB_LINUX "${TBB_MALLOC_LIBRARY}.${CMAKE_MATCH_1}")
-			if (EXISTS "${TBB_LIB_LINUX}")
-				set(TBB_LIBRARY ${TBB_LIB_LINUX})
-				message(STATUS "Storm - Using Intel TBB library in manually set path ${TBB_LIBRARY}.")
-			endif()
-			if (EXISTS "${TBB_MALLOC_LIB_LINUX}")
-				set(TBB_MALLOC_LIBRARY ${TBB_MALLOC_LIB_LINUX})
-				message(STATUS "Storm - Using Intel TBB malloc library in manually set path ${TBB_MALLOC_LIBRARY}.")
-			endif()
-		endif()
-	endif()
-
-        add_imported_library(tbb SHARED ${TBB_LIBRARY} ${TBB_INCLUDE_DIRS})
-        list(APPEND STORM_DEP_TARGETS tbb_SHARED)
-        add_imported_library(tbb_malloc SHARED ${TBB_MALLOC_LIBRARY} ${TBB_INCLUDE_DIRS})
-        list(APPEND STORM_DEP_TARGETS tbb_malloc_SHARED)
-
-    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)
-
+set(CMAKE_THREAD_PREFER_PTHREAD TRUE)
+set(THREADS_PREFER_PTHREAD_FLAG TRUE)
+find_package(Threads REQUIRED)
+list(APPEND STORM_DEP_TARGETS Threads::Threads)
 
-add_custom_target(copy_resources_headers DEPENDS ${PHMAP_BINDIR_HEADERS})
diff --git a/resources/3rdparty/carl/CMakeLists.txt b/resources/3rdparty/carl/CMakeLists.txt
deleted file mode 100644
index 398a31ed2..000000000
--- a/resources/3rdparty/carl/CMakeLists.txt
+++ /dev/null
@@ -1,25 +0,0 @@
-project(carlext)
-cmake_minimum_required(VERSION 3.3)
-include(ExternalProject)
-
-option(STORM_3RDPARTY_BINARY_DIR "3rd party bin dir")
-
-message(STATUS "Carl-Storm - Storm 3rdparty binary dir: ${STORM_3RDPARTY_BINARY_DIR}")
-
-ExternalProject_Add(carl-config
-	GIT_REPOSITORY https://github.com/moves-rwth/carl-storm
-	GIT_TAG master
-	PREFIX here
-	SOURCE_DIR source_dir
-	BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl
-	CMAKE_ARGS -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DBOOST_INCLUDEDIR=${Boost_INCLUDE_DIRS} -DBOOST_LIBRARYDIR=${Boost_LIBRARY_DIRS} -DBoost_NO_SYSTEM_PATHS=ON -DEXPORT_TO_CMAKE=ON -DTHREAD_SAFE=ON -DUSE_CLN_NUMBERS=${Use_CLN_NUMBERS} -DUSE_GINAC=${Use_GINAC} -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=ON -DCMAKE_INSTALL_PREFIX:PATH=${STORM_3RDPARTY_BINARY_DIR}/carl
-	BUILD_IN_SOURCE 0
-	LOG_UPDATE OFF
-	LOG_CONFIGURE OFF
-	BUILD_COMMAND "" # Disable build step.
-	INSTALL_COMMAND "" # Disable install step too.
-)
-add_custom_target(build-carl)
-add_dependencies(build-carl carl-config)
-
-message(STATUS "Carl-Storm - Finished configuration.")
diff --git a/resources/3rdparty/include_cudd.cmake b/resources/3rdparty/include_cudd.cmake
index db7094872..a84c1c4b6 100644
--- a/resources/3rdparty/include_cudd.cmake
+++ b/resources/3rdparty/include_cudd.cmake
@@ -70,7 +70,7 @@ set(CUDD_VERSION_STRING 3.0.0)
 add_imported_library(cudd SHARED ${CUDD_SHARED_LIBRARY} ${CUDD_INCLUDE_DIR})
 add_imported_library(cudd STATIC ${CUDD_STATIC_LIBRARY} ${CUDD_INCLUDE_DIR})
 
-add_dependencies(resources cudd3)
+add_dependencies(storm_resources cudd3)
 
 if(BUILD_SHARED_LIBS)
 	list(APPEND STORM_DEP_TARGETS cudd_SHARED)
diff --git a/resources/3rdparty/include_glpk.cmake b/resources/3rdparty/include_glpk.cmake
index f869c31fa..77a2ebdc3 100644
--- a/resources/3rdparty/include_glpk.cmake
+++ b/resources/3rdparty/include_glpk.cmake
@@ -27,7 +27,7 @@ else()
     set(GLPK_LIBRARIES  ${GLPK_LIB_DIR}/libglpk${DYNAMIC_EXT})
     set(GLPK_INCLUDE_DIR ${STORM_3RDPARTY_BINARY_DIR}/glpk-5.0/include)
     set(GLPK_VERSION_STRING 5.0)
-    add_dependencies(resources glpk_ext)
+    add_dependencies(storm_resources glpk_ext)
 endif()
 
 # Since there is a shipped version, always use GLPK
diff --git a/resources/3rdparty/include_spot.cmake b/resources/3rdparty/include_spot.cmake
index e69977303..a46ff1d11 100644
--- a/resources/3rdparty/include_spot.cmake
+++ b/resources/3rdparty/include_spot.cmake
@@ -43,7 +43,7 @@ if(STORM_USE_SPOT_SHIPPED AND NOT STORM_HAVE_SPOT)
         LOG_INSTALL ON
         BUILD_BYPRODUCTS ${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libspot${DYNAMIC_EXT}
     )
-    add_dependencies(resources spot)
+    add_dependencies(storm_resources spot)
     set(SPOT_INCLUDE_DIR "${STORM_3RDPARTY_BINARY_DIR}/spot/include/")
     set(SPOT_DIR "${STORM_3RDPARTY_BINARY_DIR}/spot/")
     set(SPOT_LIBRARIES ${STORM_3RDPARTY_BINARY_DIR}/spot/lib/libspot${DYNAMIC_EXT})
diff --git a/resources/3rdparty/include_xerces.cmake b/resources/3rdparty/include_xerces.cmake
index f318251f9..952eb83e7 100644
--- a/resources/3rdparty/include_xerces.cmake
+++ b/resources/3rdparty/include_xerces.cmake
@@ -1,4 +1,4 @@
-if(USE_XERCESC)
+if(STORM_USE_XERCES)
 	find_package(XercesC QUIET)
     if(XercesC_FOUND)
         message(STATUS "Storm - Use system version of xerces.")
@@ -14,8 +14,6 @@ if(USE_XERCESC)
             endif()
         endif()
 
-
-        # find_package(CURL)
         message (STATUS "Storm (GSPN) - Linking with Xerces-c ${XercesC_VERSION}: ${XercesC_LIBRARIES}")
 
         list(APPEND STORM_GSPN_LINK_LIBRARIES ${XercesC_LIBRARIES} ${COREFOUNDATION_LIBRARY} ${CORESERVICES_LIBRARY} ${CURL_LIBRARIES})
@@ -26,5 +24,5 @@ if(USE_XERCESC)
 else()
     set(STORM_HAVE_XERCES OFF)
     message (STATUS "Storm - Building without Xerces disables parsing XML formats (for GSPNs)")
-endif(USE_XERCESC)
+endif(STORM_USE_XERCES)
 
diff --git a/resources/cmake/find_modules/FindCusp.cmake b/resources/cmake/find_modules/FindCusp.cmake
deleted file mode 100644
index bda100911..000000000
--- a/resources/cmake/find_modules/FindCusp.cmake
+++ /dev/null
@@ -1,56 +0,0 @@
-#
-# FindCusp
-#
-# This module finds the CUSP header files and extracts their version.  It
-# sets the following variables.
-#
-# CUSP_INCLUDE_DIR -  Include directory for cusp header files.  (All header
-#                       files will actually be in the cusp subdirectory.)
-# CUSP_VERSION -      Version of cusp in the form "major.minor.patch".
-#
-# CUSP_FOUND - Indicates whether Cusp has been found
-#
-
-find_path(CUSP_INCLUDE_DIR
-	HINTS
-		/usr/include/cusp
-		/usr/local/include
-		/usr/local/cusp/include
-		${CUSP_INCLUDE_DIRS}
-		${CUSP_HINT}
-	NAMES cusp/version.h
-	DOC "Cusp headers"
-)
-if(CUSP_INCLUDE_DIR)
-	list(REMOVE_DUPLICATES CUSP_INCLUDE_DIR)
-		
-	# Find cusp version
-	file(STRINGS ${CUSP_INCLUDE_DIR}/cusp/version.h
-		version
-		REGEX "#define CUSP_VERSION[ \t]+([0-9x]+)"
-	)
-	string(REGEX REPLACE
-		"#define CUSP_VERSION[ \t]+"
-		""
-		version
-		"${version}"
-	)
-
-	#define CUSP_MAJOR_VERSION     (CUSP_VERSION / 100000)
-	#define CUSP_MINOR_VERSION     (CUSP_VERSION / 100 % 1000)
-	#define CUSP_SUBMINOR_VERSION  (CUSP_VERSION % 100)
-
-	math(EXPR CUSP_MAJOR_VERSION "${version} / 100000")
-	math(EXPR CUSP_MINOR_VERSION "${version} / 100 % 1000")
-	math(EXPR CUSP_PATCH_VERSION "${version} % 100")
-
-	set(CUSP_VERSION "${CUSP_MAJOR_VERSION}.${CUSP_MINOR_VERSION}.${CUSP_PATCH_VERSION}")
-
-	# Check for required components
-	include(FindPackageHandleStandardArgs)
-	find_package_handle_standard_args(Cusp REQUIRED_VARS CUSP_INCLUDE_DIR VERSION_VAR CUSP_VERSION)
-
-	set(CUSP_INCLUDE_DIRS ${CUSP_INCLUDE_DIR})
-	mark_as_advanced(CUSP_INCLUDE_DIR)
-	
-endif(CUSP_INCLUDE_DIR)
\ No newline at end of file
diff --git a/resources/cmake/find_modules/FindHWLOC.cmake b/resources/cmake/find_modules/FindHWLOC.cmake
deleted file mode 100644
index b0027dd89..000000000
--- a/resources/cmake/find_modules/FindHWLOC.cmake
+++ /dev/null
@@ -1,52 +0,0 @@
-# Try to find hwloc libraries and headers.
-#
-# Usage of this module:
-#
-#  find_package(hwloc)
-#
-# Variables defined by this module:
-#
-#  HWLOC_FOUND              System has hwloc libraries and headers
-#  HWLOC_LIBRARIES          The hwloc library
-#  HWLOC_INCLUDE_DIRS       The location of HWLOC headers
-
-find_path(
-  HWLOC_PREFIX
-  NAMES include/hwloc.h
-)
-
-if (NOT HWLOC_PREFIX AND NOT $ENV{HWLOC_BASE} STREQUAL "")
-  set(HWLOC_PREFIX $ENV{HWLOC_BASE})
-endif()
-
-
-find_library(
-  HWLOC_LIBRARIES
-  NAMES hwloc
-  HINTS ${HWLOC_PREFIX}/lib
-)
-
-find_path(
-  HWLOC_INCLUDE_DIRS
-  NAMES hwloc.h
-  HINTS ${HWLOC_PREFIX}/include
-)
-
-include(FindPackageHandleStandardArgs)
-
-find_package_handle_standard_args(
-  HWLOC DEFAULT_MSG
-  HWLOC_LIBRARIES
-  HWLOC_INCLUDE_DIRS
-)
-
-mark_as_advanced(
-  HWLOC_LIBRARIES
-  HWLOC_INCLUDE_DIRS
-)
-
-if (HWLOC_FOUND)
-  if (NOT $ENV{HWLOC_LIB} STREQUAL "")
-# set(HWLOC_LIBRARIES "$ENV{HWLOC_LIB}")
-  endif()
-endif()
\ No newline at end of file
diff --git a/resources/cmake/find_modules/FindMATHSAT.cmake b/resources/cmake/find_modules/FindMATHSAT.cmake
new file mode 100644
index 000000000..4705b7c5e
--- /dev/null
+++ b/resources/cmake/find_modules/FindMATHSAT.cmake
@@ -0,0 +1,25 @@
+# Try to find libmathsat
+# Once done this will define
+#  MATHSAT_FOUND - System has mathsat
+#  MATHSAT_INCLUDE_DIRS - The mathsat include directory
+#  MATHSAT_LIBRARIES - The libraries needed to use mathsat
+find_path(MATHSAT_INCLUDE_DIRS NAMES mathsat.h
+PATHS ENV PATH INCLUDE "${MATHSAT_ROOT}/include" "/usr/include/mathsat" "/usr/local/include/mathsat/"
+)
+if(${OPERATING_SYSTEM} MATCHES "Linux")
+find_library(MATHSAT_LIBRARIES mathsat
+PATHS ENV PATH INCLUDE "${MATHSAT_ROOT}/lib"
+)
+else()
+# on macOS, the .dylib file has some hard coded path (Version 5.5.4) and we therefore link statically
+find_library(MATHSAT_LIBRARIES NAMES libmathsat${STATIC_EXT} mathsat
+PATHS ENV PATH INCLUDE "${MATHSAT_ROOT}/lib"
+)
+endif()
+# handle the QUIETLY and REQUIRED arguments and set MATHSAT_FOUND to TRUE if
+# all listed variables are TRUE
+include(FindPackageHandleStandardArgs)
+FIND_PACKAGE_HANDLE_STANDARD_ARGS(MATHSAT
+REQUIRED_VARS MATHSAT_LIBRARIES MATHSAT_INCLUDE_DIRS
+)
+mark_as_advanced(MATHSAT_INCLUDE_DIR MATHSAT_LIBRARIES)
\ No newline at end of file
diff --git a/resources/cmake/find_modules/FindTBB.cmake b/resources/cmake/find_modules/FindTBB.cmake
deleted file mode 100644
index 8a2ae28fc..000000000
--- a/resources/cmake/find_modules/FindTBB.cmake
+++ /dev/null
@@ -1,310 +0,0 @@
-# FindTBB.cmake can be found at https://code.google.com/p/findtbb/
-# Written by Hannes Hofmann &lt;hannes.hofmann _at_ informatik.uni-erlangen.de&gt;
-# Improvements by Gino van den Bergen &lt;gino _at_ dtecta.com&gt;,
-#   Florian Uhlig &lt;F.Uhlig _at_ gsi.de&gt;,
-#   Jiri Marsik &lt;jiri.marsik89 _at_ gmail.com&gt;
-
-# The MIT License
-#
-# Copyright (c) 2011 Hannes Hofmann
-#
-# Permission is hereby granted, free of charge, to any person obtaining a copy
-# of this software and associated documentation files (the "Software"), to deal
-# in the Software without restriction, including without limitation the rights
-# to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
-# copies of the Software, and to permit persons to whom the Software is
-# furnished to do so, subject to the following conditions:
-#
-# The above copyright notice and this permission notice shall be included in
-# all copies or substantial portions of the Software.
-#
-# THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
-# IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
-# FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
-# AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
-# LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
-# OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN
-# THE SOFTWARE.
-
-# GvdB: This module uses the environment variable TBB_ARCH_PLATFORM which defines architecture and compiler.
-#   e.g. "ia32/vc8" or "em64t/cc4.1.0_libc2.4_kernel2.6.16.21"
-#   TBB_ARCH_PLATFORM is set by the build script tbbvars[.bat|.sh|.csh], which can be found
-#   in the TBB installation directory (TBB_INSTALL_DIR).
-#
-# GvdB: Mac OS X distribution places libraries directly in lib directory.
-#
-# For backwards compatibility, you may explicitely set the CMake variables TBB_ARCHITECTURE and TBB_COMPILER.
-# TBB_ARCHITECTURE [ ia32 | em64t | itanium ]
-#   which architecture to use
-# TBB_COMPILER e.g. vc9 or cc3.2.3_libc2.3.2_kernel2.4.21 or cc4.0.1_os10.4.9
-#   which compiler to use (detected automatically on Windows)
-
-# This module respects
-# TBB_INSTALL_DIR or $ENV{TBB21_INSTALL_DIR} or $ENV{TBB_INSTALL_DIR}
-
-# This module defines
-# TBB_INCLUDE_DIRS, where to find task_scheduler_init.h, etc.
-# TBB_LIBRARY_DIRS, where to find libtbb, libtbbmalloc
-# TBB_DEBUG_LIBRARY_DIRS, where to find libtbb_debug, libtbbmalloc_debug
-# TBB_INSTALL_DIR, the base TBB install directory
-# TBB_LIBRARIES, the libraries to link against to use TBB.
-# TBB_DEBUG_LIBRARIES, the libraries to link against to use TBB with debug symbols.
-# TBB_FOUND, If false, don't try to use TBB.
-# TBB_INTERFACE_VERSION, as defined in tbb/tbb_stddef.h
-
-
-if (WIN32)
-    # has em64t/vc8 em64t/vc9
-    # has ia32/vc7.1 ia32/vc8 ia32/vc9
-    set(_TBB_DEFAULT_INSTALL_DIR "C:/Program Files/Intel/TBB" "C:/Program Files (x86)/Intel/TBB" "C:/Program Files (x86)/Intel/Composer XE 2013/tbb")
-    set(_TBB_LIB_NAME "tbb")
-    set(_TBB_LIB_MALLOC_NAME "${_TBB_LIB_NAME}malloc")
-    set(_TBB_LIB_DEBUG_NAME "${_TBB_LIB_NAME}_debug")
-    set(_TBB_LIB_MALLOC_DEBUG_NAME "${_TBB_LIB_MALLOC_NAME}_debug")
-    if (MSVC71)
-        set (_TBB_COMPILER "vc7.1")
-    endif(MSVC71)
-    if (MSVC80)
-        set(_TBB_COMPILER "vc8")
-    endif(MSVC80)
-    if (MSVC90)
-        set(_TBB_COMPILER "vc9")
-    endif(MSVC90)
-    if(MSVC10)
-        set(_TBB_COMPILER "vc10")
-    endif(MSVC10)
-	if(MSVC11)
-        set(_TBB_COMPILER "vc11")
-    endif(MSVC11)
-	if(MSVC12)
-        set(_TBB_COMPILER "vc12")
-    endif(MSVC12)
-    # Todo: add other Windows compilers such as ICL.
-    set(_TBB_ARCHITECTURE ${TBB_ARCHITECTURE})
-endif (WIN32)
-
-if (UNIX)
-    if (APPLE)
-        # MAC
-        set(_TBB_DEFAULT_INSTALL_DIR "/Library/Frameworks/Intel_TBB.framework/Versions")
-        # libs: libtbb.dylib, libtbbmalloc.dylib, *_debug
-        set(_TBB_LIB_NAME "tbb")
-        set(_TBB_LIB_MALLOC_NAME "${_TBB_LIB_NAME}malloc")
-        set(_TBB_LIB_DEBUG_NAME "${_TBB_LIB_NAME}_debug")
-        set(_TBB_LIB_MALLOC_DEBUG_NAME "${_TBB_LIB_MALLOC_NAME}_debug")
-        # default flavor on apple: ia32/cc4.0.1_os10.4.9
-        # Jiri: There is no reason to presume there is only one flavor and
-        #       that user's setting of variables should be ignored.
-        if(NOT TBB_COMPILER)
-            set(_TBB_COMPILER "cc4.0.1_os10.4.9")
-        elseif (NOT TBB_COMPILER)
-            set(_TBB_COMPILER ${TBB_COMPILER})
-        endif(NOT TBB_COMPILER)
-        if(NOT TBB_ARCHITECTURE)
-            set(_TBB_ARCHITECTURE "ia32")
-        elseif(NOT TBB_ARCHITECTURE)
-            set(_TBB_ARCHITECTURE ${TBB_ARCHITECTURE})
-        endif(NOT TBB_ARCHITECTURE)
-    else (APPLE)
-        # LINUX
-        set(_TBB_DEFAULT_INSTALL_DIR "/opt/intel/tbb" "/usr/local/include" "/usr/include")
-        set(_TBB_LIB_NAME "tbb")
-        set(_TBB_LIB_MALLOC_NAME "${_TBB_LIB_NAME}malloc")
-        set(_TBB_LIB_DEBUG_NAME "${_TBB_LIB_NAME}_debug")
-        set(_TBB_LIB_MALLOC_DEBUG_NAME "${_TBB_LIB_MALLOC_NAME}_debug")
-        # has em64t/cc3.2.3_libc2.3.2_kernel2.4.21 em64t/cc3.3.3_libc2.3.3_kernel2.6.5 em64t/cc3.4.3_libc2.3.4_kernel2.6.9 em64t/cc4.1.0_libc2.4_kernel2.6.16.21
-        # has ia32/*
-        # has itanium/*
-        set(_TBB_COMPILER ${TBB_COMPILER})
-        set(_TBB_ARCHITECTURE ${TBB_ARCHITECTURE})
-    endif (APPLE)
-endif (UNIX)
-
-if (CMAKE_SYSTEM MATCHES "SunOS.*")
-# SUN
-# not yet supported
-# has em64t/cc3.4.3_kernel5.10
-# has ia32/*
-endif (CMAKE_SYSTEM MATCHES "SunOS.*")
-
-
-#-- Clear the public variables
-set (TBB_FOUND "NO")
-
-
-#-- Find TBB install dir and set ${_TBB_INSTALL_DIR} and cached ${TBB_INSTALL_DIR}
-# first: use CMake variable TBB_INSTALL_DIR
-if (TBB_INSTALL_DIR)
-    set (_TBB_INSTALL_DIR ${TBB_INSTALL_DIR})
-endif (TBB_INSTALL_DIR)
-# second: use environment variable
-if (NOT _TBB_INSTALL_DIR)
-    if (NOT "$ENV{TBB_INSTALL_DIR}" STREQUAL "")
-        set (_TBB_INSTALL_DIR $ENV{TBB_INSTALL_DIR})
-    endif (NOT "$ENV{TBB_INSTALL_DIR}" STREQUAL "")
-    # Intel recommends setting TBB21_INSTALL_DIR
-    if (NOT "$ENV{TBB21_INSTALL_DIR}" STREQUAL "")
-        set (_TBB_INSTALL_DIR $ENV{TBB21_INSTALL_DIR})
-    endif (NOT "$ENV{TBB21_INSTALL_DIR}" STREQUAL "")
-    if (NOT "$ENV{TBB22_INSTALL_DIR}" STREQUAL "")
-        set (_TBB_INSTALL_DIR $ENV{TBB22_INSTALL_DIR})
-    endif (NOT "$ENV{TBB22_INSTALL_DIR}" STREQUAL "")
-    if (NOT "$ENV{TBB30_INSTALL_DIR}" STREQUAL "")
-        set (_TBB_INSTALL_DIR $ENV{TBB30_INSTALL_DIR})
-    endif (NOT "$ENV{TBB30_INSTALL_DIR}" STREQUAL "")
-endif (NOT _TBB_INSTALL_DIR)
-# third: try to find path automatically
-if (NOT _TBB_INSTALL_DIR)
-    if (_TBB_DEFAULT_INSTALL_DIR)
-        set (_TBB_INSTALL_DIR ${_TBB_DEFAULT_INSTALL_DIR})
-    endif (_TBB_DEFAULT_INSTALL_DIR)
-endif (NOT _TBB_INSTALL_DIR)
-# sanity check
-if (NOT _TBB_INSTALL_DIR)
-    message ("ERROR: Unable to find Intel TBB install directory. ${_TBB_INSTALL_DIR}")
-else (NOT _TBB_INSTALL_DIR)
-# finally: set the cached CMake variable TBB_INSTALL_DIR
-if (NOT TBB_INSTALL_DIR)
-    mark_as_advanced(TBB_INSTALL_DIR)
-endif (NOT TBB_INSTALL_DIR)
-
-
-#-- A macro to rewrite the paths of the library. This is necessary, because
-#   find_library() always found the em64t/vc9 version of the TBB libs
-macro(TBB_CORRECT_LIB_DIR var_name)
-#    if (NOT "${_TBB_ARCHITECTURE}" STREQUAL "em64t")
-        string(REPLACE em64t "${_TBB_ARCHITECTURE}" ${var_name} ${${var_name}})
-#    endif (NOT "${_TBB_ARCHITECTURE}" STREQUAL "em64t")
-    string(REPLACE ia32 "${_TBB_ARCHITECTURE}" ${var_name} ${${var_name}})
-    string(REPLACE vc7.1 "${_TBB_COMPILER}" ${var_name} ${${var_name}})
-    string(REPLACE vc8 "${_TBB_COMPILER}" ${var_name} ${${var_name}})
-    string(REPLACE vc9 "${_TBB_COMPILER}" ${var_name} ${${var_name}})
-    string(REPLACE vc10 "${_TBB_COMPILER}" ${var_name} ${${var_name}})
-	string(REPLACE vc11 "${_TBB_COMPILER}" ${var_name} ${${var_name}})
-	string(REPLACE vc12 "${_TBB_COMPILER}" ${var_name} ${${var_name}})
-endmacro(TBB_CORRECT_LIB_DIR var_content)
-
-
-#-- Look for include directory and set ${TBB_INCLUDE_DIR}
-set (TBB_INC_SEARCH_DIR ${_TBB_INSTALL_DIR}/include)
-# Jiri: tbbvars now sets the CPATH environment variable to the directory
-#       containing the headers.
-find_path(TBB_INCLUDE_DIR tbb/tbb_stddef.h PATHS "${TBB_INC_SEARCH_DIR}" ENV CPATH)
-mark_as_advanced(TBB_INCLUDE_DIR)
-
-#-- Look for libraries
-include(CheckSymbolExists)
-
-# Check if we are on Windows
-CHECK_SYMBOL_EXISTS("_WIN32" "" FINDTBB_HAVE_WIN32)
-CHECK_SYMBOL_EXISTS("_WIN64" "" FINDTBB_HAVE_WIN64)
-if(FINDTBB_HAVE_WIN64)
-	# this is a build on 64bit Windows
-	set(_TBB_ARCHITECTURE "intel64")
-	set (_TBB_LIBRARY_DIR "${_TBB_INSTALL_DIR}/lib/${_TBB_ARCHITECTURE}/${_TBB_COMPILER}" ${_TBB_LIBRARY_DIR})
-elseif(FINDTBB_HAVE_WIN32)
-	# this is a build on 32bit Windows
-	set(_TBB_ARCHITECTURE "ia32")
-	set (_TBB_LIBRARY_DIR "${_TBB_INSTALL_DIR}/lib/${_TBB_ARCHITECTURE}/${_TBB_COMPILER}" ${_TBB_LIBRARY_DIR})
-endif()
-	
-# GvdB: $ENV{TBB_ARCH_PLATFORM} is set by the build script tbbvars[.bat|.sh|.csh]
-if (NOT $ENV{TBB_ARCH_PLATFORM} STREQUAL "")
-    set (_TBB_LIBRARY_DIR 
-         ${_TBB_INSTALL_DIR}/lib/$ENV{TBB_ARCH_PLATFORM}
-         ${_TBB_INSTALL_DIR}/$ENV{TBB_ARCH_PLATFORM}/lib
-        )
-endif (NOT $ENV{TBB_ARCH_PLATFORM} STREQUAL "")
-# Jiri: This block isn't mutually exclusive with the previous one
-#       (hence no else), instead I test if the user really specified
-#       the variables in question.
-if ((NOT ${TBB_ARCHITECTURE} STREQUAL "") AND (NOT ${TBB_COMPILER} STREQUAL ""))
-    # HH: deprecated
-    message(STATUS "[Warning] FindTBB.cmake: The use of TBB_ARCHITECTURE and TBB_COMPILER is deprecated and may not be supported in future versions. Please set \$ENV{TBB_ARCH_PLATFORM} (using tbbvars.[bat|csh|sh]).")
-    # Jiri: It doesn't hurt to look in more places, so I store the hints from
-    #       ENV{TBB_ARCH_PLATFORM} and the TBB_ARCHITECTURE and TBB_COMPILER
-    #       variables and search them both.
-    set (_TBB_LIBRARY_DIR "${_TBB_INSTALL_DIR}/${_TBB_ARCHITECTURE}/${_TBB_COMPILER}/lib" ${_TBB_LIBRARY_DIR})
-endif ((NOT ${TBB_ARCHITECTURE} STREQUAL "") AND (NOT ${TBB_COMPILER} STREQUAL ""))
-
-# GvdB: Mac OS X distribution places libraries directly in lib directory.
-if (USE_LIBCXX OR LINK_LIBCXXABI)
-	message(STATUS "FindTBB - Detected libc++ usage, linking to TBB with libc++!")
-	list(APPEND _TBB_LIBRARY_DIR "${_TBB_INSTALL_DIR}/lib/libc++")
-else()
-	list(APPEND _TBB_LIBRARY_DIR "${_TBB_INSTALL_DIR}/lib")
-endif()
-
-message(STATUS "Searching for TBB: TBB_LIBRARY ${_TBB_LIB_NAME} HINTS ${_TBB_LIBRARY_DIR}, _TBB_COMPILER = ${_TBB_COMPILER} and _TBB_ARCHITECTURE = ${_TBB_ARCHITECTURE}")
-
-# Jiri: No reason not to check the default paths. From recent versions,
-#       tbbvars has started exporting the LIBRARY_PATH and LD_LIBRARY_PATH
-#       variables, which now point to the directories of the lib files.
-#       It all makes more sense to use the ${_TBB_LIBRARY_DIR} as a HINTS
-#       argument instead of the implicit PATHS as it isn't hard-coded
-#       but computed by system introspection. Searching the LIBRARY_PATH
-#       and LD_LIBRARY_PATH environment variables is now even more important
-#       that tbbvars doesn't export TBB_ARCH_PLATFORM and it facilitates
-#       the use of TBB built from sources.
-find_library(TBB_LIBRARY ${_TBB_LIB_NAME} HINTS ${_TBB_LIBRARY_DIR}
-        PATHS ENV LIBRARY_PATH ENV LD_LIBRARY_PATH)
-find_library(TBB_MALLOC_LIBRARY ${_TBB_LIB_MALLOC_NAME} HINTS ${_TBB_LIBRARY_DIR}
-        PATHS ENV LIBRARY_PATH ENV LD_LIBRARY_PATH)
-
-#Extract path from TBB_LIBRARY name
-get_filename_component(TBB_LIBRARY_DIR ${TBB_LIBRARY} PATH)
-
-#TBB_CORRECT_LIB_DIR(TBB_LIBRARY)
-#TBB_CORRECT_LIB_DIR(TBB_MALLOC_LIBRARY)
-mark_as_advanced(TBB_LIBRARY TBB_MALLOC_LIBRARY)
-
-#-- Look for debug libraries
-# Jiri: Changed the same way as for the release libraries.
-find_library(TBB_LIBRARY_DEBUG ${_TBB_LIB_DEBUG_NAME} HINTS ${_TBB_LIBRARY_DIR}
-        PATHS ENV LIBRARY_PATH ENV LD_LIBRARY_PATH)
-find_library(TBB_MALLOC_LIBRARY_DEBUG ${_TBB_LIB_MALLOC_DEBUG_NAME} HINTS ${_TBB_LIBRARY_DIR}
-        PATHS ENV LIBRARY_PATH ENV LD_LIBRARY_PATH)
-
-# Jiri: Self-built TBB stores the debug libraries in a separate directory.
-#       Extract path from TBB_LIBRARY_DEBUG name
-get_filename_component(TBB_LIBRARY_DEBUG_DIR ${TBB_LIBRARY_DEBUG} PATH)
-
-#TBB_CORRECT_LIB_DIR(TBB_LIBRARY_DEBUG)
-#TBB_CORRECT_LIB_DIR(TBB_MALLOC_LIBRARY_DEBUG)
-mark_as_advanced(TBB_LIBRARY_DEBUG TBB_MALLOC_LIBRARY_DEBUG)
-
-if (TBB_INCLUDE_DIR)
-    if (TBB_LIBRARY)
-        set (TBB_FOUND ON)
-        set (TBB_LIBRARIES ${TBB_LIBRARY} ${TBB_MALLOC_LIBRARY} ${TBB_LIBRARIES})
-        set (TBB_DEBUG_LIBRARIES ${TBB_LIBRARY_DEBUG} ${TBB_MALLOC_LIBRARY_DEBUG} ${TBB_DEBUG_LIBRARIES})
-        set (TBB_INCLUDE_DIRS ${TBB_INCLUDE_DIR} CACHE PATH "TBB include directory" FORCE)
-        set (TBB_LIBRARY_DIRS ${TBB_LIBRARY_DIR} CACHE PATH "TBB library directory" FORCE)
-        # Jiri: Self-built TBB stores the debug libraries in a separate directory.
-        set (TBB_DEBUG_LIBRARY_DIRS ${TBB_LIBRARY_DEBUG_DIR} CACHE PATH "TBB debug library directory" FORCE)
-        mark_as_advanced(TBB_INCLUDE_DIRS TBB_LIBRARY_DIRS TBB_DEBUG_LIBRARY_DIRS TBB_LIBRARIES TBB_DEBUG_LIBRARIES)
-        message(STATUS "Found Intel TBB")
-    endif (TBB_LIBRARY)
-endif (TBB_INCLUDE_DIR)
-
-if (NOT TBB_FOUND)
-    message("ERROR: Intel TBB NOT found!")
-    message(STATUS "Looked for Threading Building Blocks in ${_TBB_INSTALL_DIR}")
-    # do only throw fatal, if this pkg is REQUIRED
-    if (TBB_FIND_REQUIRED)
-        message(FATAL_ERROR "Could NOT find TBB library.")
-    endif (TBB_FIND_REQUIRED)
-endif (NOT TBB_FOUND)
-
-endif (NOT _TBB_INSTALL_DIR)
-
-if (TBB_FOUND)
-	set(TBB_INTERFACE_VERSION 0)
-	FILE(READ "${TBB_INCLUDE_DIRS}/tbb/tbb_stddef.h" _TBB_VERSION_CONTENTS)
-	STRING(REGEX REPLACE ".*#define TBB_INTERFACE_VERSION ([0-9]+).*" "\\1" TBB_INTERFACE_VERSION "${_TBB_VERSION_CONTENTS}")
-	STRING(REGEX REPLACE ".*#define TBB_VERSION_MAJOR ([0-9]+).*" "\\1" TBB_VERSION_MAJOR "${_TBB_VERSION_CONTENTS}")
-	STRING(REGEX REPLACE ".*#define TBB_VERSION_MINOR ([0-9]+).*" "\\1" TBB_VERSION_MINOR "${_TBB_VERSION_CONTENTS}")
-	set(TBB_INTERFACE_VERSION "${TBB_INTERFACE_VERSION}")
-	set(TBB_VERSION_MAJOR "${TBB_VERSION_MAJOR}")
-	set(TBB_VERSION_MINOR "${TBB_VERSION_MINOR}")
-endif (TBB_FOUND)
\ No newline at end of file
diff --git a/resources/cmake/macros/export.cmake b/resources/cmake/macros/export.cmake
index ab919d750..e7655528f 100644
--- a/resources/cmake/macros/export.cmake
+++ b/resources/cmake/macros/export.cmake
@@ -24,8 +24,8 @@ endforeach()
 include(CMakePackageConfigHelpers)
 
 write_basic_package_version_file(${CMAKE_CURRENT_BINARY_DIR}/stormConfigVersion.cmake
-     VERSION 0.1.0
-     COMPATIBILITY SameMajorVersion )
+     VERSION ${STORM_VERSION_MAJOR}.${STORM_VERSION_MINOR}.${STORM_VERSION_PATCH}.${STORM_VERSION_TWEAK}
+     COMPATIBILITY SameMinorVersion )
 
 # For the build tree
 set(CONF_INCLUDE_DIRS "${CMAKE_BINARY_DIR}/include/")
diff --git a/resources/cmake/macros/imported.cmake b/resources/cmake/macros/imported.cmake
index fb847eff6..e957e5e98 100644
--- a/resources/cmake/macros/imported.cmake
+++ b/resources/cmake/macros/imported.cmake
@@ -1,10 +1,17 @@
 # copied from CARL
 
 
-macro(add_imported_library_interface name include)
+macro(storm_add_imported_library_interface name include install_include)
 	add_library(${name} INTERFACE IMPORTED)
-	set_target_properties(${name} PROPERTIES INTERFACE_INCLUDE_DIRECTORIES "${include}")
-endmacro(add_imported_library_interface)
+	if("${install_include}" STREQUAL "")
+		target_include_directories(${name} INTERFACE ${include})
+	else()
+		target_include_directories(${name} INTERFACE
+				$<BUILD_INTERFACE:${include}>
+				$<INSTALL_INTERFACE:${install_include}>
+		)
+	endif()
+endmacro(storm_add_imported_library_interface)
 
 macro(add_imported_library name type lib include)
 # Workaround from https://cmake.org/Bug/view.php?id=15052
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 32ce46c25..9bfcf2f4a 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -1,7 +1,3 @@
-set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
-set(CMAKE_LIBRARY_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/lib)
-set(CMAKE_RUNTIME_OUTPUT_DIRECTORY ${CMAKE_BINARY_DIR}/bin)
-
 add_custom_target(binaries)
 
 add_subdirectory(storm)
@@ -12,7 +8,6 @@ add_subdirectory(storm-parsers)
 add_subdirectory(storm-version-info)
 add_subdirectory(storm-cli-utilities)
 add_subdirectory(storm-cli)
-# Additional libraries
 add_subdirectory(storm-conv)
 add_subdirectory(storm-conv-cli)
 add_subdirectory(storm-dft)
diff --git a/src/storm-cli-utilities/CMakeLists.txt b/src/storm-cli-utilities/CMakeLists.txt
index 6f43e020a..b3a1aa51e 100644
--- a/src/storm-cli-utilities/CMakeLists.txt
+++ b/src/storm-cli-utilities/CMakeLists.txt
@@ -1,38 +1,20 @@
-file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-cli-utilities/*.h ${PROJECT_SOURCE_DIR}/src/storm-cli-utilities/*.cpp)
-
-register_source_groups_from_filestructure("${ALL_FILES}" storm-cli-utilities)
-
 file(GLOB_RECURSE STORM_CLI_UTIL_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-cli-utilities/*.cpp)
-file(GLOB_RECURSE STORM_CLI_UTIL_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-cli-utilities/*.h)
+file(GLOB_RECURSE STORM_CLI_UTIL_HEADERS  RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-cli-utilities" ${PROJECT_SOURCE_DIR}/src/storm-cli-utilities/*.h)
 
 
 # Create storm-cli-utilities.
-add_library(storm-cli-utilities SHARED ${STORM_CLI_UTIL_SOURCES} ${STORM_CLI_UTIL_HEADERS})
+add_library(storm-cli-utilities SHARED)
+target_sources(storm-cli-utilities
+		PRIVATE
+		${STORM_CLI_UTIL_SOURCES}
+		PUBLIC
+		FILE_SET fs_storm_cli_utilities_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_CLI_UTIL_HEADERS})
 target_precompile_headers(storm-cli-utilities REUSE_FROM storm)
+target_link_libraries(storm-cli-utilities PUBLIC storm storm-counterexamples storm-gamebased-ar storm-parsers storm-version-info)
 
-# Remove define symbol for shared libstorm.
-set_target_properties(storm-cli-utilities PROPERTIES DEFINE_SYMBOL "")
 list(APPEND STORM_TARGETS storm-cli-utilities)
 set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
 
-target_link_libraries(storm-cli-utilities PUBLIC storm storm-counterexamples storm-gamebased-ar storm-parsers storm-version-info)
-
-# Install storm headers to include directory.
-foreach(HEADER ${STORM_CLI_UTIL_HEADERS})
-	string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER})
-	string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH})
-	string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH})
-	add_custom_command(
-		OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}
-		COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		DEPENDS ${HEADER}
-	)
-	list(APPEND STORM_CLI_UTIL_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}")
-endforeach()
-add_custom_target(copy_storm_cli_util_headers DEPENDS ${STORM_CLI_UTIL_OUTPUT_HEADERS} ${STORM_CLI_UTIL_HEADERS})
-add_dependencies(storm-cli-utilities copy_storm_cli_util_headers)
-
 # installation
-install(TARGETS storm-cli-utilities EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+install(TARGETS storm-cli-utilities EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL FILE_SET fs_storm_cli_utilities_headers)
 
diff --git a/src/storm-cli-utilities/print.cpp b/src/storm-cli-utilities/print.cpp
index d802caed2..eb23520e1 100644
--- a/src/storm-cli-utilities/print.cpp
+++ b/src/storm-cli-utilities/print.cpp
@@ -1,4 +1,4 @@
-#include "print.h"
+#include "storm-cli-utilities/print.h"
 
 #include "storm-version-info/storm-version.h"
 #include "storm/utility/cli.h"
@@ -16,7 +16,7 @@
 #ifdef STORM_HAVE_GUROBI
 #include "gurobi_c.h"
 #endif
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
 #include "mathsat.h"
 #endif
 #ifdef STORM_HAVE_SOPLEX
@@ -111,7 +111,7 @@ void printVersion() {
     STORM_PRINT("Linked with Intel Threading Building Blocks v" << TBB_VERSION_MAJOR << "." << TBB_VERSION_MINOR << " (Interface version "
                                                                 << TBB_INTERFACE_VERSION << ").\n");
 #endif
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     char* msatVersion = msat_get_version();
     STORM_PRINT("Linked with " << msatVersion << ".\n");
     msat_free(msatVersion);
diff --git a/src/storm-cli/CMakeLists.txt b/src/storm-cli/CMakeLists.txt
index 54e870fef..9f19854a6 100644
--- a/src/storm-cli/CMakeLists.txt
+++ b/src/storm-cli/CMakeLists.txt
@@ -2,6 +2,7 @@
 add_executable(storm-cli ${PROJECT_SOURCE_DIR}/src/storm-cli/storm-cli.cpp)
 target_link_libraries(storm-cli storm storm-cli-utilities)
 set_target_properties(storm-cli PROPERTIES OUTPUT_NAME "storm")
+set_target_properties(storm-cli PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION})
 target_precompile_headers(storm-cli PRIVATE ${STORM_PRECOMPILED_HEADERS})
 
 add_dependencies(binaries storm-cli)
diff --git a/src/storm-config.h.in b/src/storm-config.h.in
index 5245fd709..e5b0fd665 100644
--- a/src/storm-config.h.in
+++ b/src/storm-config.h.in
@@ -1,107 +1,98 @@
 /*
- * StoRM - Build-in Options
+ * Storm - Build Options
  *
- * This file is parsed by CMake during makefile generation
- * It contains information such as the base path to the test/example data
+ * This file is parsed by CMake during Makefile generation
+ * It contains build and configuration information
  */
 
-#ifndef STORM_GENERATED_STORMCONFIG_H_
-#define STORM_GENERATED_STORMCONFIG_H_
+#pragma once
 
+
+// Directories
+// ###########
 // The directory of the sources from which Storm was built.
 #define STORM_SOURCE_DIR "@PROJECT_SOURCE_DIR@"
-
-// The directory of the test resources used in the tests (model files, ...).
-#define STORM_TEST_RESOURCES_DIR "@STORM_TEST_RESOURCES_DIR@"
-
 // The directory in which Storm was built.
 #define STORM_BUILD_DIR "@CMAKE_BINARY_DIR@"
+// The directory of the test resources used in the tests (model files, ...).
+#define STORM_TEST_RESOURCES_DIR "@STORM_TEST_RESOURCES_DIR@"
 
 // Boost include directory used during compilation.
 #define STORM_BOOST_INCLUDE_DIR "@STORM_BOOST_INCLUDE_DIR@"
-
 // Carl include directory used during compilation.
 #define STORM_CARL_INCLUDE_DIR "@carl_INCLUDE_DIR@"
 
-// Whether Gurobi is available and to be used (define/undef)
-#cmakedefine STORM_HAVE_GUROBI
-
-// Whether GLPK is available and to be used (define/undef)
-#cmakedefine STORM_HAVE_GLPK
-
-// Whether Z3 is available and to be used (define/undef)
-#cmakedefine STORM_HAVE_Z3
-
-// Whether the optimization feature of Z3 is available and to be used (define/undef)
-#cmakedefine STORM_HAVE_Z3_OPTIMIZE
-
-// Version of Z3 used by Storm.
-#define STORM_Z3_VERSION_MAJOR @STORM_Z3_VERSION_MAJOR@
-#define STORM_Z3_VERSION_MINOR @STORM_Z3_VERSION_MINOR@
-#define STORM_Z3_VERSION_PATCH @STORM_Z3_VERSION_PATCH@
-#define STORM_Z3_VERSION @Z3_VERSION@
-#cmakedefine STORM_Z3_API_USES_STANDARD_INTEGERS
-
-// Whether MathSAT is available and to be used (define/undef)
-#cmakedefine STORM_HAVE_MSAT
-
-// Whether SoPlex is available and to be used
-#cmakedefine STORM_HAVE_SOPLEX
 
+// Storm configuration options
+// ###########################
 // Whether benchmarks from QVBS can be used as input
 #cmakedefine STORM_HAVE_QVBS
-
 // The root directory of QVBS
 #cmakedefine STORM_QVBS_ROOT "@STORM_QVBS_ROOT@"
+// Logging configuration
+#cmakedefine STORM_LOGGING_FRAMEWORK
+#cmakedefine STORM_LOG_DISABLE_DEBUG
 
-// Whether Intel Threading Building Blocks are available and to be used (define/undef)
-#cmakedefine STORM_HAVE_INTELTBB
-
-// Whether support for parametric systems should be enabled
-#cmakedefine PARAMETRIC_SYSTEMS
 
-// Whether CLN is available and to be used (define/undef)
-#cmakedefine STORM_HAVE_CLN
+// Carl configuration
+// ###################
+// Whether carl is available and to be used
+#cmakedefine STORM_HAVE_CARL
+// Whether carl has headers for forward declarations
+#cmakedefine STORM_CARL_SUPPORTS_FWD_DECL
+// Version of CARL used by Storm.
+#define STORM_CARL_VERSION_MAJOR @carl_VERSION_MAJOR@
+#define STORM_CARL_VERSION_MINOR @carl_VERSION_MINOR@
+#define STORM_CARL_VERSION @carl_VERSION@
 
-// Include directory for CLN headers
-#cmakedefine CLN_INCLUDE_DIR "@CLN_INCLUDE_DIR@"
 
+// GMP
+// ###
 // Whether GMP is available  (it is always available nowadays)
 #define STORM_HAVE_GMP
-
 // Include directory for GMP headers
 #cmakedefine GMP_INCLUDE_DIR "@GMP_INCLUDE_DIR@"
 #cmakedefine GMPXX_INCLUDE_DIR "@GMPXX_INCLUDE_DIR@"
 
-// Whether carl is available and to be used.
-#cmakedefine STORM_HAVE_CARL
-// Whether carl has headers for forward declarations
-#cmakedefine STORM_CARL_SUPPORTS_FWD_DECL
-// Version of CARL used by Storm.
-#define STORM_CARL_VERSION_MAJOR @carl_VERSION_MAJOR@
-#define STORM_CARL_VERSION_MINOR @carl_VERSION_MINOR@
-#define STORM_CARL_VERSION @carl_VERSION@
-#cmakedefine STORM_Z3_API_USES_STANDARD_INTEGERS
 
+// CLN
+// ###
+// Whether CLN is available and to be used
+#cmakedefine STORM_HAVE_CLN
+// Include directory for CLN headers
+#cmakedefine CLN_INCLUDE_DIR "@CLN_INCLUDE_DIR@"
+// Whether Storm uses CLN for rationals and rational functions
 #cmakedefine STORM_USE_CLN_EA
-
 #cmakedefine STORM_USE_CLN_RF
 
-#cmakedefine STORM_HAVE_XERCES
 
-// Whether Spot is available and to be used
-#cmakedefine STORM_HAVE_SPOT
+// Z3 configuration
+// ################
+// Whether Z3 is available and to be used
+#cmakedefine STORM_HAVE_Z3
+// Whether the optimization feature of Z3 is available and to be used
+#cmakedefine STORM_HAVE_Z3_OPTIMIZE
+// Whether Z3 uses standard integers
+#cmakedefine STORM_Z3_API_USES_STANDARD_INTEGERS
+// Version of Z3 used by Storm.
+#define STORM_Z3_VERSION_MAJOR @STORM_Z3_VERSION_MAJOR@
+#define STORM_Z3_VERSION_MINOR @STORM_Z3_VERSION_MINOR@
+#define STORM_Z3_VERSION_PATCH @STORM_Z3_VERSION_PATCH@
+#define STORM_Z3_VERSION @Z3_VERSION@
+
 
+// Dependencies
+// ############
+// Whether the libraries are available and to be used
+#cmakedefine STORM_HAVE_GLPK
+#cmakedefine STORM_HAVE_GUROBI
+#cmakedefine STORM_HAVE_MATHSAT
+#cmakedefine STORM_HAVE_SOPLEX
+#cmakedefine STORM_HAVE_SPOT
+#cmakedefine STORM_HAVE_XERCES
+// Whether Intel Threading Building Blocks are available and to be used
+#cmakedefine STORM_HAVE_INTELTBB
 // Whether LTL model checking shall be enabled
 #ifdef STORM_HAVE_SPOT
         #define STORM_HAVE_LTL_MODELCHECKING_SUPPORT
-#endif // STORM_HAVE_SPOT
-
-// Whether smtrat is available and to be used.
-#cmakedefine STORM_HAVE_SMTRAT
-
-#cmakedefine STORM_LOGGING_FRAMEWORK
-
-#cmakedefine STORM_LOG_DISABLE_DEBUG
-
-#endif // STORM_GENERATED_STORMCONFIG_H_
+#endif // STORM_HAVE_SPOT
\ No newline at end of file
diff --git a/src/storm-conv/CMakeLists.txt b/src/storm-conv/CMakeLists.txt
index d39af1a33..2cb49af1a 100644
--- a/src/storm-conv/CMakeLists.txt
+++ b/src/storm-conv/CMakeLists.txt
@@ -1,38 +1,21 @@
-file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-conv/*.h ${PROJECT_SOURCE_DIR}/src/storm-conv/*.cpp)
-
-register_source_groups_from_filestructure("${ALL_FILES}" storm-conv)
-
 file(GLOB_RECURSE STORM_CONV_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-conv/*/*.cpp)
-file(GLOB_RECURSE STORM_CONV_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-conv/*/*.h)
-
+file(GLOB_RECURSE STORM_CONV_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-conv" ${PROJECT_SOURCE_DIR}/src/storm-conv/*/*.h)
 
 # Create storm-conv.
-add_library(storm-conv SHARED ${STORM_CONV_SOURCES} ${STORM_CONV_HEADERS})
+add_library(storm-conv SHARED)
+target_sources(storm-conv
+        PRIVATE
+        ${STORM_CONV_SOURCES}
+        PUBLIC
+        FILE_SET fs_storm_conv_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_CONV_HEADERS})
 target_precompile_headers(storm-conv REUSE_FROM storm)
 
-# Remove define symbol for shared libstorm.
-set_target_properties(storm-conv PROPERTIES DEFINE_SYMBOL "")
+target_link_libraries(storm-conv PUBLIC storm)
+
 list(APPEND STORM_TARGETS storm-conv)
 set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
 
-target_link_libraries(storm-conv PUBLIC storm ${STORM_CONV_LINK_LIBRARIES})
-
-# Install storm headers to include directory.
-foreach(HEADER ${STORM_CONV_HEADERS})
-	string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER})
-	string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH})
-	string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH})
-	add_custom_command(
-		OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}
-		COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		DEPENDS ${HEADER}
-	)
-	list(APPEND STORM_CONV_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}")
-endforeach()
-add_custom_target(copy_storm_conv_headers DEPENDS ${STORM_CONV_OUTPUT_HEADERS} ${STORM_CONV_HEADERS})
-add_dependencies(storm-conv copy_storm_conv_headers)
 
 # installation
-install(TARGETS storm-conv EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+install(TARGETS storm-conv EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL FILE_SET fs_storm_conv_headers)
 
diff --git a/src/storm-counterexamples/CMakeLists.txt b/src/storm-counterexamples/CMakeLists.txt
index d86e5d1b9..bdc943f39 100644
--- a/src/storm-counterexamples/CMakeLists.txt
+++ b/src/storm-counterexamples/CMakeLists.txt
@@ -1,38 +1,18 @@
-file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*.cpp)
-
-register_source_groups_from_filestructure("${ALL_FILES}" storm-counterexamples)
-
 file(GLOB_RECURSE STORM_CEX_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*/*.cpp)
-file(GLOB_RECURSE STORM_CEX_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*/*.h)
+file(GLOB_RECURSE STORM_CEX_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-counterexamples" ${PROJECT_SOURCE_DIR}/src/storm-counterexamples/*/*.h)
 
-
-# Create storm-counterexamples.
 add_library(storm-counterexamples SHARED ${STORM_CEX_SOURCES} ${STORM_CEX_HEADERS})
+target_sources(storm-counterexamples
+        PRIVATE
+        ${STORM_CEX_SOURCES}
+        PUBLIC
+        FILE_SET fs_storm_cex_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_CEX_HEADERS})
 target_precompile_headers(storm-counterexamples REUSE_FROM storm)
+target_link_libraries(storm-counterexamples PUBLIC storm)
 
-# Remove define symbol for shared libstorm.
-set_target_properties(storm-counterexamples PROPERTIES DEFINE_SYMBOL "")
 list(APPEND STORM_TARGETS storm-counterexamples)
 set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
 
-target_link_libraries(storm-counterexamples PUBLIC storm)
-
-# Install storm headers to include directory.
-foreach(HEADER ${STORM_CEX_HEADERS})
-	string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER})
-	string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH})
-	string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH})
-	add_custom_command(
-		OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}
-		COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		DEPENDS ${HEADER}
-	)
-	list(APPEND STORM_CEX_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}")
-endforeach()
-add_custom_target(copy_storm_cex_headers DEPENDS ${STORM_CEX_OUTPUT_HEADERS} ${STORM_CEX_HEADERS})
-add_dependencies(storm-counterexamples copy_storm_cex_headers)
-
 # installation
-install(TARGETS storm-counterexamples EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+install(TARGETS storm-counterexamples EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL FILE_SET fs_storm_cex_headers)
 
diff --git a/src/storm-dft/CMakeLists.txt b/src/storm-dft/CMakeLists.txt
index 4c01771df..c536e6293 100644
--- a/src/storm-dft/CMakeLists.txt
+++ b/src/storm-dft/CMakeLists.txt
@@ -1,38 +1,19 @@
-file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-dft/*.h ${PROJECT_SOURCE_DIR}/src/storm-dft/*.cpp)
-
-register_source_groups_from_filestructure("${ALL_FILES}" storm-dft)
-
 file(GLOB_RECURSE STORM_DFT_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.cpp)
-file(GLOB_RECURSE STORM_DFT_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.h)
-
+file(GLOB_RECURSE STORM_DFT_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-dft" ${PROJECT_SOURCE_DIR}/src/storm-dft/*/*.h)
 
 # Create storm-dft.
-add_library(storm-dft SHARED ${STORM_DFT_SOURCES} ${STORM_DFT_HEADERS})
+add_library(storm-dft SHARED)
+target_sources(storm-dft
+        PRIVATE
+        ${STORM_DFT_SOURCES}
+        PUBLIC
+        FILE_SET fs_storm_dft_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_DFT_HEADERS})
 target_precompile_headers(storm-dft REUSE_FROM storm)
+target_link_libraries(storm-dft PUBLIC storm storm-gspn storm-conv storm-parsers storm-pars ${STORM_DFT_LINK_LIBRARIES})
 
-# Remove define symbol for shared libstorm.
-set_target_properties(storm-dft PROPERTIES DEFINE_SYMBOL "")
 list(APPEND STORM_TARGETS storm-dft)
 set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
 
-target_link_libraries(storm-dft PUBLIC storm storm-gspn storm-conv storm-parsers storm-pars ${STORM_DFT_LINK_LIBRARIES})
-
-# Install storm headers to include directory.
-foreach(HEADER ${STORM_DFT_HEADERS})
-	string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER})
-	string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH})
-	string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH})
-	add_custom_command(
-		OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}
-		COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		DEPENDS ${HEADER}
-	)
-	list(APPEND STORM_DFT_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}")
-endforeach()
-add_custom_target(copy_storm_dft_headers DEPENDS ${STORM_DFT_OUTPUT_HEADERS} ${STORM_DFT_HEADERS})
-add_dependencies(storm-dft copy_storm_dft_headers)
-
 # installation
-install(TARGETS storm-dft EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+install(TARGETS storm-dft EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL FILE_SET fs_storm_dft_headers )
 
diff --git a/src/storm-gamebased-ar/CMakeLists.txt b/src/storm-gamebased-ar/CMakeLists.txt
index f1809e592..14bff943e 100644
--- a/src/storm-gamebased-ar/CMakeLists.txt
+++ b/src/storm-gamebased-ar/CMakeLists.txt
@@ -1,38 +1,18 @@
-file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-gamebased-ar/*.h ${PROJECT_SOURCE_DIR}/src/storm-gamebased-ar/*.cpp)
-
-register_source_groups_from_filestructure("${ALL_FILES}" storm-gamebased-ar)
-
 file(GLOB_RECURSE STORM_GBAR_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-gamebased-ar/*/*.cpp)
-file(GLOB_RECURSE STORM_GBAR_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-gamebased-ar/*/*.h)
-
-
-# Create storm-gamebased-ar.
-add_library(storm-gamebased-ar SHARED ${STORM_GBAR_SOURCES} ${STORM_GBAR_HEADERS})
+file(GLOB_RECURSE STORM_GBAR_HEADERS RELATIVE " ${PROJECT_SOURCE_DIR}/src/storm-gamebased-ar" ${PROJECT_SOURCE_DIR}/src/storm-gamebased-ar/*/*.h)
+
+add_library(storm-gamebased-ar SHARED)
+target_sources(storm-gamebased-ar
+		PRIVATE
+		${STORM_GBAR_SOURCES}
+		PUBLIC
+		FILE_SET fs_storm_gbar_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_GBAR_HEADERS})
 target_precompile_headers(storm-gamebased-ar REUSE_FROM storm)
+target_link_libraries(storm-gamebased-ar PUBLIC storm)
 
-# Remove define symbol for shared libstorm.
-set_target_properties(storm-gamebased-ar PROPERTIES DEFINE_SYMBOL "")
 list(APPEND STORM_TARGETS storm-gamebased-ar)
 set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
 
-target_link_libraries(storm-gamebased-ar PUBLIC storm)
-
-# Install storm headers to include directory.
-foreach (HEADER ${STORM_GBAR_HEADERS})
-	string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER})
-	string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH})
-	string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH})
-	add_custom_command(
-		OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}
-		COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		DEPENDS ${HEADER}
-	)
-	list(APPEND STORM_GBAR_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}")
-endforeach()
-add_custom_target(copy_storm_gbar_headers DEPENDS ${STORM_GBAR_OUTPUT_HEADERS} ${STORM_GBAR_HEADERS})
-add_dependencies(storm-gamebased-ar copy_storm_gbar_headers)
-
 # installation
-install(TARGETS storm-gamebased-ar EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+install(TARGETS storm-gamebased-ar EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL FILE_SET fs_storm_gbar_headers)
 
diff --git a/src/storm-gspn/CMakeLists.txt b/src/storm-gspn/CMakeLists.txt
index 0b61ef9cb..08ed240a2 100644
--- a/src/storm-gspn/CMakeLists.txt
+++ b/src/storm-gspn/CMakeLists.txt
@@ -1,38 +1,19 @@
-file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-gspn/*.h ${PROJECT_SOURCE_DIR}/src/storm-gspn/*.cpp)
-
-register_source_groups_from_filestructure("${ALL_FILES}" storm-gspn)
-
 file(GLOB_RECURSE STORM_GSPN_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-gspn/*/*.cpp)
-file(GLOB_RECURSE STORM_GSPN_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-gspn/*/*.h)
-
-
-# Create storm-gspn.
-add_library(storm-gspn SHARED ${STORM_GSPN_SOURCES} ${STORM_GSPN_HEADERS})
+file(GLOB_RECURSE STORM_GSPN_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-gspn" ${PROJECT_SOURCE_DIR}/src/storm-gspn/*/*.h)
+
+add_library(storm-gspn SHARED)
+target_sources(storm-gspn
+		PRIVATE
+		${STORM_GSPN_SOURCES}
+		PUBLIC
+		FILE_SET fs_storm_gspn_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_GSPN_HEADERS})
 target_precompile_headers(storm-gspn REUSE_FROM storm)
+target_link_libraries(storm-gspn PUBLIC storm storm-conv storm-parsers ${STORM_GSPN_LINK_LIBRARIES})
 
 # Remove define symbol for shared libstorm.
-set_target_properties(storm-gspn PROPERTIES DEFINE_SYMBOL "")
 list(APPEND STORM_TARGETS storm-gspn)
 set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
 
-target_link_libraries(storm-gspn PUBLIC storm storm-conv storm-parsers ${STORM_GSPN_LINK_LIBRARIES})
-
-# Install storm headers to include directory.
-foreach(HEADER ${STORM_GSPN_HEADERS})
-	string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER})
-	string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH})
-	string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH})
-	add_custom_command(
-		OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}
-		COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		DEPENDS ${HEADER}
-	)
-	list(APPEND STORM_GSPN_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}")
-endforeach()
-add_custom_target(copy_storm_gspn_headers DEPENDS ${STORM_GSPN_OUTPUT_HEADERS} ${STORM_GSPN_HEADERS})
-add_dependencies(storm-gspn copy_storm_gspn_headers)
-
 # installation
-install(TARGETS storm-gspn EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+install(TARGETS storm-gspn EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL FILE_SET fs_storm_gspn_headers)
 
diff --git a/src/storm-pars/CMakeLists.txt b/src/storm-pars/CMakeLists.txt
index 8dca2969b..d6c1546aa 100644
--- a/src/storm-pars/CMakeLists.txt
+++ b/src/storm-pars/CMakeLists.txt
@@ -1,38 +1,19 @@
-file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-pars/*.h ${PROJECT_SOURCE_DIR}/src/storm-pars/*.cpp)
-
-register_source_groups_from_filestructure("${ALL_FILES}" storm-pars)
-
 file(GLOB_RECURSE STORM_PARS_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-pars/*/*.cpp)
-file(GLOB_RECURSE STORM_PARS_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-pars/*/*.h)
-
+file(GLOB_RECURSE STORM_PARS_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-pars"  ${PROJECT_SOURCE_DIR}/src/storm-pars/*/*.h)
 
 # Create storm-pars.
-add_library(storm-pars SHARED ${STORM_PARS_SOURCES} ${STORM_PARS_HEADERS})
+add_library(storm-pars SHARED)
+target_sources(storm-pars
+		PRIVATE
+		${STORM_PARS_SOURCES}
+		PUBLIC
+		FILE_SET fs_storm_pars_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_PARS_HEADERS})
 target_precompile_headers(storm-pars REUSE_FROM storm)
+target_link_libraries(storm-pars PUBLIC storm)
 
-# Remove define symbol for shared libstorm.
-set_target_properties(storm-pars PROPERTIES DEFINE_SYMBOL "")
 list(APPEND STORM_TARGETS storm-pars)
 set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
 
-target_link_libraries(storm-pars PUBLIC storm ${STORM_PARS_LINK_LIBRARIES})
-
-# Install storm headers to include directory.
-foreach(HEADER ${STORM_PARS_HEADERS})
-	string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER})
-	string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH})
-	string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH})
-	add_custom_command(
-		OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}
-		COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		DEPENDS ${HEADER}
-	)
-	list(APPEND STORM_PARS_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}")
-endforeach()
-add_custom_target(copy_storm_pars_headers DEPENDS ${STORM_PARS_OUTPUT_HEADERS} ${STORM_PARS_HEADERS})
-add_dependencies(storm-pars copy_storm_pars_headers)
-
 # installation
-install(TARGETS storm-pars EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+install(TARGETS storm-pars EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL FILE_SET fs_storm_pars_headers)
 
diff --git a/src/storm-parsers/CMakeLists.txt b/src/storm-parsers/CMakeLists.txt
index 3832c90d7..56acf15e4 100644
--- a/src/storm-parsers/CMakeLists.txt
+++ b/src/storm-parsers/CMakeLists.txt
@@ -1,41 +1,22 @@
-file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-parsers/*.h ${PROJECT_SOURCE_DIR}/src/storm-parsers/*.cpp)
-
-register_source_groups_from_filestructure("${ALL_FILES}" storm-parsers)
-
 file(GLOB_RECURSE STORM_PARSER_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-parsers/*/*.cpp)
-file(GLOB_RECURSE STORM_PARSER_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-parsers/*/*.h)
-
+file(GLOB_RECURSE STORM_PARSER_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-parsers" ${PROJECT_SOURCE_DIR}/src/storm-parsers/*/*.h)
 
 # Disable Debug compiler flags for PrismParser to lessen memory consumption during compilation
 SET_SOURCE_FILES_PROPERTIES(${PROJECT_SOURCE_DIR}/src/storm-parsers/parser/PrismParser.cpp PROPERTIES COMPILE_FLAGS -g0)
 
 # Create storm-parsers.
-add_library(storm-parsers SHARED ${STORM_PARSER_SOURCES} ${STORM_PARSER_HEADERS})
+add_library(storm-parsers SHARED)
+target_sources(storm-parsers
+        PRIVATE
+        ${STORM_PARSER_SOURCES}
+        PUBLIC
+        FILE_SET fs_storm_parsers_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_PARSER_HEADERS})
 target_precompile_headers(storm-parsers REUSE_FROM storm)
+target_link_libraries(storm-parsers PUBLIC storm)
 
-# Remove define symbol for shared libstorm.
-set_target_properties(storm-parsers PROPERTIES DEFINE_SYMBOL "")
 list(APPEND STORM_TARGETS storm-parsers)
 set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
 
-target_link_libraries(storm-parsers PUBLIC storm)
-
-# Install storm headers to include directory.
-foreach(HEADER ${STORM_PARSER_HEADERS})
-	string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER})
-	string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH})
-	string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH})
-	add_custom_command(
-		OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}
-		COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		DEPENDS ${HEADER}
-	)
-	list(APPEND STORM_PARSER_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}")
-endforeach()
-add_custom_target(copy_storm_parser_headers DEPENDS ${STORM_PARSER_OUTPUT_HEADERS} ${STORM_PARSER_HEADERS})
-add_dependencies(storm-parsers copy_storm_parser_headers)
-
 # installation
-install(TARGETS storm-parsers EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+install(TARGETS storm-parsers EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL FILE_SET fs_storm_parsers_headers)
 
diff --git a/src/storm-permissive/CMakeLists.txt b/src/storm-permissive/CMakeLists.txt
index 7a25c23ff..ee2bca7b0 100644
--- a/src/storm-permissive/CMakeLists.txt
+++ b/src/storm-permissive/CMakeLists.txt
@@ -1,38 +1,19 @@
-file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-permissive/*.h ${PROJECT_SOURCE_DIR}/src/storm-permissive/*.cpp)
-
-register_source_groups_from_filestructure("${ALL_FILES}" storm-permissive)
-
 file(GLOB_RECURSE STORM_PERMISSIVE_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-permissive/*/*.cpp)
-file(GLOB_RECURSE STORM_PERMISSIVE_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-permissive/*/*.h)
-
+file(GLOB_RECURSE STORM_PERMISSIVE_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-permissive" ${PROJECT_SOURCE_DIR}/src/storm-permissive/*/*.h)
 
 # Create storm-permissive.
-add_library(storm-permissive SHARED ${STORM_PERMISSIVE_SOURCES} ${STORM_PERMISSIVE_HEADERS})
+add_library(storm-permissive SHARED)
+target_sources(storm-permissive
+        PRIVATE
+        ${STORM_PERMISSIVE_SOURCES}
+        PUBLIC
+        FILE_SET fs_storm_permissive_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_PERMISSIVE_HEADERS})
 target_precompile_headers(storm-permissive REUSE_FROM storm)
+target_link_libraries(storm-permissive PUBLIC storm)
 
-# Remove define symbol for shared libstorm.
-set_target_properties(storm-permissive PROPERTIES DEFINE_SYMBOL "")
 list(APPEND STORM_TARGETS storm-permissive)
 set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
 
-target_link_libraries(storm-permissive PUBLIC storm)
-
-# Install storm headers to include directory.
-foreach (HEADER ${STORM_PERMISSIVE_HEADERS})
-	string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER})
-	string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH})
-	string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH})
-	add_custom_command(
-		OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}
-		COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		DEPENDS ${HEADER}
-	)
-	list(APPEND STORM_PERMISSIVE_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}")
-endforeach()
-add_custom_target(copy_storm_permissive_headers DEPENDS ${STORM_PERMISSIVE_OUTPUT_HEADERS} ${STORM_PERMISSIVE_HEADERS})
-add_dependencies(storm-permissive copy_storm_permissive_headers)
-
 # installation
-install(TARGETS storm-permissive EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+install(TARGETS storm-permissive EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL FILE_SET fs_storm_permissive_headers)
 
diff --git a/src/storm-pomdp/CMakeLists.txt b/src/storm-pomdp/CMakeLists.txt
index 2a9b8cdfe..18d5989e0 100644
--- a/src/storm-pomdp/CMakeLists.txt
+++ b/src/storm-pomdp/CMakeLists.txt
@@ -1,38 +1,19 @@
-file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-pomdp/*.h ${PROJECT_SOURCE_DIR}/src/storm-pomdp/*.cpp)
-
-register_source_groups_from_filestructure("${ALL_FILES}" storm-pomdp)
-
 file(GLOB_RECURSE STORM_POMDP_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-pomdp/*/*.cpp)
-file(GLOB_RECURSE STORM_POMDP_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-pomdp/*/*.h)
-
+file(GLOB_RECURSE STORM_POMDP_HEADERS RELATIVE " ${PROJECT_SOURCE_DIR}/src/storm-pomdp"  ${PROJECT_SOURCE_DIR}/src/storm-pomdp/*/*.h)
 
 # Create storm-pomdp.
-add_library(storm-pomdp SHARED ${STORM_POMDP_SOURCES} ${STORM_POMDP_HEADERS})
+add_library(storm-pomdp SHARED)
+target_sources(storm-pomdp
+		PRIVATE
+		${STORM_POMDP_SOURCES}
+		PUBLIC
+		FILE_SET fs_storm_pomdp_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_POMDP_HEADERS})
 target_precompile_headers(storm-pomdp REUSE_FROM storm)
+target_link_libraries(storm-pomdp PUBLIC storm storm-parsers storm-pars)
 
-# Remove define symbol for shared libstorm.
-set_target_properties(storm-pomdp PROPERTIES DEFINE_SYMBOL "")
 list(APPEND STORM_TARGETS storm-pomdp)
 set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
 
-target_link_libraries(storm-pomdp PUBLIC storm storm-parsers storm-pars ${STORM_POMDP_LINK_LIBRARIES})
-
-# Install storm headers to include directory.
-foreach(HEADER ${STORM_POMDP_HEADERS})
-	string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER})
-	string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH})
-	string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH})
-	add_custom_command(
-		OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}
-		COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		DEPENDS ${HEADER}
-	)
-	list(APPEND STORM_POMDP_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}")
-endforeach()
-add_custom_target(copy_storm_pomdp_headers DEPENDS ${STORM_POMDP_OUTPUT_HEADERS} ${STORM_POMDP_HEADERS})
-add_dependencies(storm-pomdp copy_storm_pomdp_headers)
-
 # installation
-install(TARGETS storm-pomdp RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+install(TARGETS storm-pomdp RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL FILE_SET fs_storm_pomdp_headers)
 
diff --git a/src/storm-version-info/CMakeLists.txt b/src/storm-version-info/CMakeLists.txt
index 272c176e3..f34d27ccf 100644
--- a/src/storm-version-info/CMakeLists.txt
+++ b/src/storm-version-info/CMakeLists.txt
@@ -1,9 +1,5 @@
-file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm-version-info/*.h ${PROJECT_SOURCE_DIR}/src/storm-version-info/*.cpp)
-
-register_source_groups_from_filestructure("${ALL_FILES}" storm-version-info)
-
 file(GLOB_RECURSE STORM_VERSION_INFO_SOURCES ${PROJECT_SOURCE_DIR}/src/storm-version-info/*.cpp)
-file(GLOB_RECURSE STORM_VERSION_INFO_HEADERS ${PROJECT_SOURCE_DIR}/src/storm-version-info/*.h)
+file(GLOB_RECURSE STORM_VERSION_INFO_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm-version-info" ${PROJECT_SOURCE_DIR}/src/storm-version-info/*.h)
 
 # Configure a source file to pass the Storm version to the source code
 configure_file (
@@ -14,33 +10,21 @@ configure_file (
 # Add the generated source file
 list(APPEND STORM_VERSION_INFO_SOURCES "${PROJECT_BINARY_DIR}/storm-version.cpp")
 
-
 # Create storm-version-info lib
-add_library(storm-version-info SHARED ${STORM_VERSION_INFO_SOURCES} ${STORM_VERSION_INFO_HEADERS})
-
-# Remove define symbol for shared libstorm.
-set_target_properties(storm-version-info PROPERTIES DEFINE_SYMBOL "")
-# Add dependency to core storm libary. We are not going to link against it to avoid unnecessary linking steps, but we still want to build storm-version-info as often as possible.
+add_library(storm-version-info SHARED)
+target_sources(storm-version-info
+		PRIVATE
+		${STORM_VERSION_INFO_SOURCES}
+		PUBLIC
+		FILE_SET fs_storm_version_info_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_VERSION_INFO_HEADERS})
+# Add dependency to core storm libary.
+# We are not going to link against it to avoid unnecessary linking steps,
+# but we still want to build storm-version-info as often as possible.
 add_dependencies(storm storm-version-info)
+
 list(APPEND STORM_TARGETS storm-version-info)
 set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
 
-# Install storm headers to include directory.
-foreach(HEADER ${STORM_VERSION_INFO_HEADERS})
-	string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER})
-	string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH})
-	string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH})
-	add_custom_command(
-		OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}
-		COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		DEPENDS ${HEADER}
-	)
-	list(APPEND STORM_VERSION_INFO_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}")
-endforeach()
-add_custom_target(copy_storm_version_info_headers DEPENDS ${STORM_VERSION_INFO_OUTPUT_HEADERS} ${STORM_VERSION_INFO_HEADERS})
-add_dependencies(storm-version-info copy_storm_version_info_headers)
-
 # installation
-install(TARGETS storm-version-info EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL)
+install(TARGETS storm-version-info EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib OPTIONAL FILE_SET fs_storm_version_info_headers)
 
diff --git a/src/storm/CMakeLists.txt b/src/storm/CMakeLists.txt
index 0775be6e1..cb85a671d 100644
--- a/src/storm/CMakeLists.txt
+++ b/src/storm/CMakeLists.txt
@@ -1,69 +1,31 @@
-file(GLOB_RECURSE ALL_FILES ${PROJECT_SOURCE_DIR}/src/storm/*.h ${PROJECT_SOURCE_DIR}/src/storm/*.cpp)
-
-register_source_groups_from_filestructure("${ALL_FILES}" storm)
-
 #############################################################
 ##
 ##	Source file aggregation and clustering
 ##
 #############################################################
 file(GLOB_RECURSE STORM_SOURCES ${PROJECT_SOURCE_DIR}/src/storm/*/*.cpp)
-file(GLOB_RECURSE STORM_HEADERS ${PROJECT_SOURCE_DIR}/src/storm/*.h)
+file(GLOB_RECURSE STORM_HEADERS RELATIVE "${PROJECT_SOURCE_DIR}/src/storm" ${PROJECT_SOURCE_DIR}/src/storm/*.h )
 
 # Additional include files like the storm-config.h
 file(GLOB_RECURSE STORM_BUILD_HEADERS ${PROJECT_BINARY_DIR}/include/*.h)
 
-# Add custom additional include or link directories
-if (ADDITIONAL_INCLUDE_DIRS)
-	message(STATUS "Storm - Using additional include directories ${ADDITIONAL_INCLUDE_DIRS}")
-	include_directories(${ADDITIONAL_INCLUDE_DIRS})
-endif(ADDITIONAL_INCLUDE_DIRS)
-if (ADDITIONAL_LINK_DIRS)
-	message(STATUS "Storm - Using additional link directories ${ADDITIONAL_LINK_DIRS}")
-	link_directories(${ADDITIONAL_LINK_DIRS})
-endif(ADDITIONAL_LINK_DIRS)
-
-
 ###############################################################################
 ##                                                                            
-##	Binary creation (All link_directories() calls must be made before this point.)
+##	Binary creation
 ##
 ###############################################################################
-
 # Create libstorm.
-add_library(storm SHARED ${STORM_3RDPARTY_SOURCES} ${STORM_SOURCES} ${STORM_HEADERS})
+add_library(storm SHARED)
+target_sources(storm PRIVATE ${STORM_SOURCES})
+target_sources(storm PUBLIC FILE_SET fs_storm_headers TYPE HEADERS BASE_DIRS "${PROJECT_SOURCE_DIR}/src" FILES ${STORM_HEADERS})
+target_sources(storm PUBLIC FILE_SET fs_storm_configured_headers TYPE HEADERS BASE_DIRS "${PROJECT_BINARY_DIR}/include" FILES ${STORM_BUILD_HEADERS})
 target_precompile_headers(storm PRIVATE ${STORM_PRECOMPILED_HEADERS})
-# Remove define symbol for shared libstorm.
-set_target_properties(storm PROPERTIES DEFINE_SYMBOL "")
-add_dependencies(storm resources)
+set_target_properties(storm PROPERTIES VERSION ${STORM_VERSION} SOVERSION ${STORM_VERSION})
+add_dependencies(storm storm_resources)
 #The library that needs symbols must be first, then the library that resolves the symbol.
 target_link_libraries(storm PUBLIC ${STORM_DEP_TARGETS} ${STORM_DEP_IMP_TARGETS} ${STORM_LINK_LIBRARIES})
-#target_include_directories(storm PUBLIC "$<BUILD_INTERFACE:${PROJECT_SOURCE_DIR}/src/storm>$<INSTALL_INTERFACE:include/storm>")
-target_include_directories(storm PUBLIC "$<BUILD_INTERFACE:${CMAKE_BINARY_DIR}/include/>$<INSTALL_INTERFACE:include/storm>")
-target_include_directories(storm PUBLIC "$<BUILD_INTERFACE:${STORM_3RDPARTY_BINARY_DIR}>$<INSTALL_INTERFACE:include>") # the interface loc is not right
-# Add base folder for better inclusion paths
 list(APPEND STORM_TARGETS storm)
 set(STORM_TARGETS ${STORM_TARGETS} PARENT_SCOPE)
 
-# Install storm headers to include directory.
-foreach(HEADER ${STORM_HEADERS})
-	string(REGEX REPLACE "${PROJECT_SOURCE_DIR}/src/?" "" RELATIVE_HEADER_PATH ${HEADER})
-	string(REGEX MATCH "(.*)[/\\]" RELATIVE_DIRECTORY ${RELATIVE_HEADER_PATH})
-	string(REGEX REPLACE "${RELATIVE_DIRECTORY}/?" "" HEADER_FILENAME ${RELATIVE_HEADER_PATH})
-	add_custom_command(
-		OUTPUT ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		COMMAND ${CMAKE_COMMAND} -E make_directory ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}
-		COMMAND ${CMAKE_COMMAND} -E copy ${HEADER} ${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}
-		DEPENDS ${HEADER}
-	)
-	list(APPEND STORM_OUTPUT_HEADERS "${CMAKE_BINARY_DIR}/include/${RELATIVE_DIRECTORY}${HEADER_FILENAME}")
-endforeach()
-add_custom_target(copy_storm_headers DEPENDS ${STORM_OUTPUT_HEADERS} ${STORM_HEADERS})
-add_dependencies(storm copy_storm_headers)
-add_dependencies(storm copy_resources_headers)
-
-
 # installation
-install(TARGETS storm EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib)
-install(DIRECTORY ${CMAKE_BINARY_DIR}/include/ DESTINATION include/storm
-		FILES_MATCHING PATTERN "*.h")
+install(TARGETS storm RUNTIME_DEPENDENCIES EXPORT storm_Targets RUNTIME DESTINATION bin LIBRARY DESTINATION lib FRAMEWORK DESTINATION lib FILE_SET fs_storm_headers FILE_SET fs_storm_configured_headers)
diff --git a/src/storm/adapters/MathsatExpressionAdapter.cpp b/src/storm/adapters/MathsatExpressionAdapter.cpp
index 9672aa9f8..d83fef868 100644
--- a/src/storm/adapters/MathsatExpressionAdapter.cpp
+++ b/src/storm/adapters/MathsatExpressionAdapter.cpp
@@ -1,6 +1,6 @@
 #include "storm/adapters/MathsatExpressionAdapter.h"
 
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
 bool operator==(msat_decl decl1, msat_decl decl2) {
     return decl1.repr == decl2.repr;
 }
diff --git a/src/storm/adapters/MathsatExpressionAdapter.h b/src/storm/adapters/MathsatExpressionAdapter.h
index c2eefae45..3f14acd36 100644
--- a/src/storm/adapters/MathsatExpressionAdapter.h
+++ b/src/storm/adapters/MathsatExpressionAdapter.h
@@ -5,7 +5,7 @@
 
 #include <stack>
 
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
 #include "mathsat.h"
 #endif
 
@@ -19,7 +19,7 @@
 #include "storm/utility/constants.h"
 #include "storm/utility/macros.h"
 
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
 namespace std {
 // Define hashing operator for MathSAT's declarations.
 template<>
@@ -37,7 +37,7 @@ bool operator==(msat_decl decl1, msat_decl decl2);
 namespace storm {
 namespace adapters {
 
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
 
 class MathsatExpressionAdapter : public storm::expressions::ExpressionVisitor {
    public:
diff --git a/src/storm/solver/MathsatSmtSolver.cpp b/src/storm/solver/MathsatSmtSolver.cpp
index d50227f9f..4c79b5c44 100644
--- a/src/storm/solver/MathsatSmtSolver.cpp
+++ b/src/storm/solver/MathsatSmtSolver.cpp
@@ -7,7 +7,7 @@
 namespace storm {
 namespace solver {
 
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
 MathsatSmtSolver::MathsatAllsatModelReference::MathsatAllsatModelReference(
     storm::expressions::ExpressionManager const& manager, msat_env const& env, msat_term* model,
     std::unordered_map<storm::expressions::Variable, uint_fast64_t> const& variableToSlotMapping)
@@ -115,14 +115,14 @@ std::string MathsatSmtSolver::MathsatModelReference::toString() const {
 
 MathsatSmtSolver::MathsatSmtSolver(storm::expressions::ExpressionManager& manager, Options const& options)
     : SmtSolver(manager)
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
       ,
       expressionAdapter(nullptr),
       lastCheckAssumptions(false),
       lastResult(CheckResult::Unknown)
 #endif
 {
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     msat_config config = msat_create_config();
     if (options.enableInterpolantGeneration) {
         msat_set_option(config, "interpolation", "true");
@@ -147,7 +147,7 @@ MathsatSmtSolver::MathsatSmtSolver(storm::expressions::ExpressionManager& manage
 }
 
 MathsatSmtSolver::~MathsatSmtSolver() {
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     if (!MSAT_ERROR_ENV(env)) {
         msat_destroy_env(env);
     } else {
@@ -159,7 +159,7 @@ MathsatSmtSolver::~MathsatSmtSolver() {
 }
 
 void MathsatSmtSolver::push() {
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     msat_push_backtrack_point(env);
 #else
     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
@@ -167,7 +167,7 @@ void MathsatSmtSolver::push() {
 }
 
 void MathsatSmtSolver::pop() {
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     msat_pop_backtrack_point(env);
 #else
     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
@@ -175,7 +175,7 @@ void MathsatSmtSolver::pop() {
 }
 
 void MathsatSmtSolver::pop(uint_fast64_t n) {
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     SmtSolver::pop(n);
 #else
     (void)n;
@@ -184,7 +184,7 @@ void MathsatSmtSolver::pop(uint_fast64_t n) {
 }
 
 void MathsatSmtSolver::reset() {
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     msat_reset_env(env);
 #else
     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Storm is compiled without MathSAT support.");
@@ -192,7 +192,7 @@ void MathsatSmtSolver::reset() {
 }
 
 void MathsatSmtSolver::add(storm::expressions::Expression const& e) {
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     msat_term expression = expressionAdapter->translateExpression(e);
     msat_assert_formula(env, expression);
     if (expressionAdapter->hasAdditionalConstraints()) {
@@ -207,7 +207,7 @@ void MathsatSmtSolver::add(storm::expressions::Expression const& e) {
 }
 
 SmtSolver::CheckResult MathsatSmtSolver::check() {
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     lastCheckAssumptions = false;
     switch (msat_solve(env)) {
         case MSAT_SAT:
@@ -227,7 +227,7 @@ SmtSolver::CheckResult MathsatSmtSolver::check() {
 }
 
 SmtSolver::CheckResult MathsatSmtSolver::checkWithAssumptions(std::set<storm::expressions::Expression> const& assumptions) {
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     lastCheckAssumptions = true;
     std::vector<msat_term> mathSatAssumptions;
     mathSatAssumptions.reserve(assumptions.size());
@@ -255,7 +255,7 @@ SmtSolver::CheckResult MathsatSmtSolver::checkWithAssumptions(std::set<storm::ex
 }
 
 SmtSolver::CheckResult MathsatSmtSolver::checkWithAssumptions(std::initializer_list<storm::expressions::Expression> const& assumptions) {
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     lastCheckAssumptions = true;
     std::vector<msat_term> mathSatAssumptions;
     mathSatAssumptions.reserve(assumptions.size());
@@ -283,7 +283,7 @@ SmtSolver::CheckResult MathsatSmtSolver::checkWithAssumptions(std::initializer_l
 }
 
 storm::expressions::SimpleValuation MathsatSmtSolver::getModelAsValuation() {
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException,
                     "Unable to create model for formula that was not determined to be satisfiable.");
     return this->convertMathsatModelToValuation();
@@ -293,7 +293,7 @@ storm::expressions::SimpleValuation MathsatSmtSolver::getModelAsValuation() {
 }
 
 std::shared_ptr<SmtSolver::ModelReference> MathsatSmtSolver::getModel() {
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     STORM_LOG_THROW(this->lastResult == SmtSolver::CheckResult::Sat, storm::exceptions::InvalidStateException,
                     "Unable to create model for formula that was not determined to be satisfiable.");
     return std::shared_ptr<SmtSolver::ModelReference>(new MathsatModelReference(this->getManager(), env, *expressionAdapter));
@@ -302,7 +302,7 @@ std::shared_ptr<SmtSolver::ModelReference> MathsatSmtSolver::getModel() {
 #endif
 }
 
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
 storm::expressions::SimpleValuation MathsatSmtSolver::convertMathsatModelToValuation() {
     storm::expressions::SimpleValuation stormModel(this->getManager().getSharedPointer());
 
@@ -332,7 +332,7 @@ storm::expressions::SimpleValuation MathsatSmtSolver::convertMathsatModelToValua
 #endif
 
 std::vector<storm::expressions::SimpleValuation> MathsatSmtSolver::allSat(std::vector<storm::expressions::Variable> const& important) {
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     std::vector<storm::expressions::SimpleValuation> valuations;
     this->allSat(important, [&valuations](storm::expressions::SimpleValuation const& valuation) -> bool {
         valuations.push_back(valuation);
@@ -345,7 +345,7 @@ std::vector<storm::expressions::SimpleValuation> MathsatSmtSolver::allSat(std::v
 #endif
 }
 
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
 class AllsatValuationCallbackUserData {
    public:
     AllsatValuationCallbackUserData(storm::expressions::ExpressionManager const& manager, storm::adapters::MathsatExpressionAdapter& adapter, msat_env& env,
@@ -426,7 +426,7 @@ class AllsatModelReferenceCallbackUserData {
 
 uint_fast64_t MathsatSmtSolver::allSat(std::vector<storm::expressions::Variable> const& important,
                                        std::function<bool(storm::expressions::SimpleValuation&)> const& callback) {
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     // Create a backtracking point, because MathSAT will modify the assertions stack during its AllSat procedure.
     this->push();
 
@@ -454,7 +454,7 @@ uint_fast64_t MathsatSmtSolver::allSat(std::vector<storm::expressions::Variable>
 
 uint_fast64_t MathsatSmtSolver::allSat(std::vector<storm::expressions::Variable> const& important,
                                        std::function<bool(SmtSolver::ModelReference&)> const& callback) {
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     // Create a backtracking point, because MathSAT will modify the assertions stack during its AllSat procedure.
     this->push();
 
@@ -483,7 +483,7 @@ uint_fast64_t MathsatSmtSolver::allSat(std::vector<storm::expressions::Variable>
 }
 
 std::vector<storm::expressions::Expression> MathsatSmtSolver::getUnsatAssumptions() {
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException,
                     "Unable to generate unsatisfiable core of assumptions, because the last check did not determine the formulas to be unsatisfiable.");
     STORM_LOG_THROW(lastCheckAssumptions, storm::exceptions::InvalidStateException,
@@ -506,7 +506,7 @@ std::vector<storm::expressions::Expression> MathsatSmtSolver::getUnsatAssumption
 }
 
 void MathsatSmtSolver::setInterpolationGroup(uint64_t group) {
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     auto groupIter = this->interpolationGroups.find(group);
     if (groupIter == this->interpolationGroups.end()) {
         int newGroup = msat_create_itp_group(env);
@@ -521,7 +521,7 @@ void MathsatSmtSolver::setInterpolationGroup(uint64_t group) {
 }
 
 storm::expressions::Expression MathsatSmtSolver::getInterpolant(std::vector<uint64_t> const& groupsA) {
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     STORM_LOG_THROW(lastResult == SmtSolver::CheckResult::Unsat, storm::exceptions::InvalidStateException,
                     "Unable to generate interpolant, because the last check did not determine the formulas to be unsatisfiable.");
     STORM_LOG_THROW(!lastCheckAssumptions, storm::exceptions::InvalidStateException,
diff --git a/src/storm/solver/MathsatSmtSolver.h b/src/storm/solver/MathsatSmtSolver.h
index 3444a1995..438386471 100644
--- a/src/storm/solver/MathsatSmtSolver.h
+++ b/src/storm/solver/MathsatSmtSolver.h
@@ -6,7 +6,7 @@
 #include "storm/adapters/MathsatExpressionAdapter.h"
 #include "storm/solver/SmtSolver.h"
 
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
 #include "mathsat.h"
 #endif
 
@@ -33,7 +33,7 @@ class MathsatSmtSolver : public SmtSolver {
         bool enableInterpolantGeneration = false;
     };
 
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     class MathsatAllsatModelReference : public SmtSolver::ModelReference {
        public:
         MathsatAllsatModelReference(storm::expressions::ExpressionManager const& manager, msat_env const& env, msat_term* model,
@@ -51,7 +51,7 @@ class MathsatSmtSolver : public SmtSolver {
     };
 #endif
 
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     class MathsatModelReference : public SmtSolver::ModelReference {
        public:
         MathsatModelReference(storm::expressions::ExpressionManager const& manager, msat_env const& env,
@@ -110,7 +110,7 @@ class MathsatSmtSolver : public SmtSolver {
    private:
     storm::expressions::SimpleValuation convertMathsatModelToValuation();
 
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
     // The MathSAT environment.
     msat_env env;
 
diff --git a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp
index dcd24495b..7a14c34bb 100644
--- a/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp
+++ b/src/storm/storage/dd/sylvan/InternalSylvanDdManager.cpp
@@ -122,13 +122,11 @@ InternalAdd<DdType::Sylvan, storm::RationalNumber> InternalDdManager<DdType::Syl
     return InternalAdd<DdType::Sylvan, storm::RationalNumber>(this, sylvan::Mtbdd::stormRationalNumberTerminal(storm::utility::one<storm::RationalNumber>()));
 }
 
-#ifdef STORM_HAVE_CARL
 template<>
 InternalAdd<DdType::Sylvan, storm::RationalFunction> InternalDdManager<DdType::Sylvan>::getAddOne() const {
     return InternalAdd<DdType::Sylvan, storm::RationalFunction>(this,
                                                                 sylvan::Mtbdd::stormRationalFunctionTerminal(storm::utility::one<storm::RationalFunction>()));
 }
-#endif
 
 InternalBdd<DdType::Sylvan> InternalDdManager<DdType::Sylvan>::getBddZero() const {
     return InternalBdd<DdType::Sylvan>(this, sylvan::Bdd::bddZero());
diff --git a/src/storm/storage/expressions/ToCppVisitor.cpp b/src/storm/storage/expressions/ToCppVisitor.cpp
deleted file mode 100644
index 61c423464..000000000
--- a/src/storm/storage/expressions/ToCppVisitor.cpp
+++ /dev/null
@@ -1,350 +0,0 @@
-#include "storm/storage/expressions/ToCppVisitor.h"
-
-#include "storm/storage/expressions/Expressions.h"
-
-#include "storm/adapters/RationalFunctionAdapter.h"
-
-#include "storm/exceptions/NotSupportedException.h"
-#include "storm/utility/macros.h"
-
-namespace storm {
-namespace expressions {
-
-ToCppTranslationOptions::ToCppTranslationOptions(std::unordered_map<storm::expressions::Variable, std::string> const& prefixes,
-                                                 std::unordered_map<storm::expressions::Variable, std::string> const& names, ToCppTranslationMode mode)
-    : prefixes(prefixes), names(names), mode(mode) {
-    // Intentionally left empty.
-}
-
-std::unordered_map<storm::expressions::Variable, std::string> const& ToCppTranslationOptions::getPrefixes() const {
-    return prefixes.get();
-}
-
-std::unordered_map<storm::expressions::Variable, std::string> const& ToCppTranslationOptions::getNames() const {
-    return names.get();
-}
-
-ToCppTranslationMode const& ToCppTranslationOptions::getMode() const {
-    return mode;
-}
-
-std::string ToCppVisitor::translate(storm::expressions::Expression const& expression, ToCppTranslationOptions const& options) {
-    expression.accept(*this, options);
-    std::string result = stream.str();
-    stream.str("");
-    return result;
-}
-
-boost::any ToCppVisitor::visit(IfThenElseExpression const& expression, boost::any const& data) {
-    ToCppTranslationOptions const& options = boost::any_cast<ToCppTranslationOptions>(data);
-
-    // Clear the type cast for the condition.
-    ToCppTranslationOptions conditionOptions(options.getPrefixes(), options.getNames());
-    stream << "(";
-    expression.getCondition()->accept(*this, conditionOptions);
-    stream << " ? ";
-    expression.getThenExpression()->accept(*this, data);
-    stream << " : ";
-    expression.getElseExpression()->accept(*this, data);
-    stream << ")";
-    return boost::none;
-}
-
-boost::any ToCppVisitor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
-    ToCppTranslationOptions newOptions = boost::any_cast<ToCppTranslationOptions>(data);
-
-    switch (expression.getOperatorType()) {
-        case BinaryBooleanFunctionExpression::OperatorType::And:
-            stream << "(";
-            expression.getFirstOperand()->accept(*this, newOptions);
-            stream << " && ";
-            expression.getSecondOperand()->accept(*this, newOptions);
-            stream << ")";
-            break;
-        case BinaryBooleanFunctionExpression::OperatorType::Or:
-            stream << "(";
-            expression.getFirstOperand()->accept(*this, newOptions);
-            stream << " || ";
-            expression.getSecondOperand()->accept(*this, newOptions);
-            stream << ")";
-            break;
-        case BinaryBooleanFunctionExpression::OperatorType::Xor:
-            stream << "(";
-            expression.getFirstOperand()->accept(*this, newOptions);
-            stream << " ^ ";
-            expression.getSecondOperand()->accept(*this, newOptions);
-            stream << ")";
-            break;
-        case BinaryBooleanFunctionExpression::OperatorType::Implies:
-            stream << "(!";
-            expression.getFirstOperand()->accept(*this, newOptions);
-            stream << " || ";
-            expression.getSecondOperand()->accept(*this, newOptions);
-            stream << ")";
-            break;
-        case BinaryBooleanFunctionExpression::OperatorType::Iff:
-            stream << "!(";
-            expression.getFirstOperand()->accept(*this, newOptions);
-            stream << " ^ ";
-            expression.getSecondOperand()->accept(*this, newOptions);
-            stream << ")";
-            break;
-    }
-    return boost::none;
-}
-
-boost::any ToCppVisitor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
-    switch (expression.getOperatorType()) {
-        case BinaryNumericalFunctionExpression::OperatorType::Plus:
-            stream << "(";
-            expression.getFirstOperand()->accept(*this, data);
-            stream << " + ";
-            expression.getSecondOperand()->accept(*this, data);
-            stream << ")";
-            break;
-        case BinaryNumericalFunctionExpression::OperatorType::Minus:
-            stream << "(";
-            expression.getFirstOperand()->accept(*this, data);
-            stream << " - ";
-            expression.getSecondOperand()->accept(*this, data);
-            stream << ")";
-            break;
-        case BinaryNumericalFunctionExpression::OperatorType::Times:
-            stream << "(";
-            expression.getFirstOperand()->accept(*this, data);
-            stream << " * ";
-            expression.getSecondOperand()->accept(*this, data);
-            stream << ")";
-            break;
-        case BinaryNumericalFunctionExpression::OperatorType::Divide:
-            stream << "(";
-            expression.getFirstOperand()->accept(*this, data);
-            stream << " / ";
-            expression.getSecondOperand()->accept(*this, data);
-            stream << ")";
-            break;
-        case BinaryNumericalFunctionExpression::OperatorType::Min:
-            stream << "std::min(";
-            expression.getFirstOperand()->accept(*this, data);
-            stream << ", ";
-            expression.getSecondOperand()->accept(*this, data);
-            stream << ")";
-            break;
-        case BinaryNumericalFunctionExpression::OperatorType::Max:
-            stream << "std::max(";
-            expression.getFirstOperand()->accept(*this, data);
-            stream << ", ";
-            expression.getSecondOperand()->accept(*this, data);
-            stream << ")";
-            break;
-        case BinaryNumericalFunctionExpression::OperatorType::Power:
-            stream << "std::pow(";
-            expression.getFirstOperand()->accept(*this, data);
-            stream << ", ";
-            expression.getSecondOperand()->accept(*this, data);
-            stream << ")";
-            break;
-        case BinaryNumericalFunctionExpression::OperatorType::Modulo:
-            stream << "(";
-            expression.getFirstOperand()->accept(*this, data);
-            stream << " % ";
-            expression.getSecondOperand()->accept(*this, data);
-            stream << ")";
-            break;
-        case BinaryNumericalFunctionExpression::OperatorType::Logarithm:
-            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Log expressions not implemented for C++ translation.");
-    }
-    return boost::none;
-}
-
-boost::any ToCppVisitor::visit(BinaryRelationExpression const& expression, boost::any const& data) {
-    ToCppTranslationOptions newOptions = boost::any_cast<ToCppTranslationOptions>(data);
-
-    switch (expression.getRelationType()) {
-        case RelationType::Equal:
-            stream << "(";
-            expression.getFirstOperand()->accept(*this, newOptions);
-            stream << " == ";
-            expression.getSecondOperand()->accept(*this, newOptions);
-            stream << ")";
-            break;
-        case RelationType::NotEqual:
-            stream << "(";
-            expression.getFirstOperand()->accept(*this, newOptions);
-            stream << " != ";
-            expression.getSecondOperand()->accept(*this, newOptions);
-            stream << ")";
-            break;
-        case RelationType::Less:
-            stream << "(";
-            expression.getFirstOperand()->accept(*this, newOptions);
-            stream << " < ";
-            expression.getSecondOperand()->accept(*this, newOptions);
-            stream << ")";
-            break;
-        case RelationType::LessOrEqual:
-            stream << "(";
-            expression.getFirstOperand()->accept(*this, newOptions);
-            stream << " <= ";
-            expression.getSecondOperand()->accept(*this, newOptions);
-            stream << ")";
-            break;
-        case RelationType::Greater:
-            stream << "(";
-            expression.getFirstOperand()->accept(*this, newOptions);
-            stream << " > ";
-            expression.getSecondOperand()->accept(*this, newOptions);
-            stream << ")";
-            break;
-        case RelationType::GreaterOrEqual:
-            stream << "(";
-            expression.getFirstOperand()->accept(*this, newOptions);
-            stream << " >= ";
-            expression.getSecondOperand()->accept(*this, newOptions);
-            stream << ")";
-            break;
-    }
-    return boost::none;
-}
-
-std::string getVariableName(storm::expressions::Variable const& variable, std::unordered_map<storm::expressions::Variable, std::string> const& prefixes,
-                            std::unordered_map<storm::expressions::Variable, std::string> const& names) {
-    auto prefixIt = prefixes.find(variable);
-    if (prefixIt != prefixes.end()) {
-        auto nameIt = names.find(variable);
-        if (nameIt != names.end()) {
-            return prefixIt->second + nameIt->second;
-        } else {
-            return prefixIt->second + variable.getName();
-        }
-    } else {
-        auto nameIt = names.find(variable);
-        if (nameIt != names.end()) {
-            return nameIt->second;
-        } else {
-            return variable.getName();
-        }
-    }
-}
-
-boost::any ToCppVisitor::visit(VariableExpression const& expression, boost::any const& data) {
-    ToCppTranslationOptions const& options = boost::any_cast<ToCppTranslationOptions const&>(data);
-    storm::expressions::Variable const& variable = expression.getVariable();
-    std::string variableName = getVariableName(variable, options.getPrefixes(), options.getNames());
-
-    if (variable.hasBooleanType()) {
-        stream << variableName;
-    } else {
-        switch (options.getMode()) {
-            case ToCppTranslationMode::KeepType:
-                stream << variableName;
-                break;
-            case ToCppTranslationMode::CastDouble:
-                stream << "static_cast<double>(" << variableName << ")";
-                break;
-            case ToCppTranslationMode::CastRationalNumber:
-                stream << "carl::rationalize<storm::RationalNumber>(" << variableName << ")";
-                break;
-            case ToCppTranslationMode::CastRationalFunction:
-                // Here, we rely on the variable name mapping to a rational function representing the variable being available.
-                stream << variableName;
-                break;
-        }
-    }
-    return boost::none;
-}
-
-boost::any ToCppVisitor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
-    ToCppTranslationOptions newOptions = boost::any_cast<ToCppTranslationOptions>(data);
-
-    switch (expression.getOperatorType()) {
-        case UnaryBooleanFunctionExpression::OperatorType::Not:
-            stream << "!(";
-            expression.getOperand()->accept(*this, newOptions);
-            stream << ")";
-            break;
-    }
-    return boost::none;
-}
-
-boost::any ToCppVisitor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
-    ToCppTranslationOptions const& options = boost::any_cast<ToCppTranslationOptions const&>(data);
-    switch (expression.getOperatorType()) {
-        case UnaryNumericalFunctionExpression::OperatorType::Minus:
-            stream << "-(";
-            expression.getOperand()->accept(*this, data);
-            stream << ")";
-            break;
-        case UnaryNumericalFunctionExpression::OperatorType::Floor:
-            STORM_LOG_THROW(options.getMode() != ToCppTranslationMode::CastRationalFunction, storm::exceptions::NotSupportedException,
-                            "Floor is not supported by rational functions.");
-            if (options.getMode() != ToCppTranslationMode::CastRationalNumber) {
-                stream << "std::floor";
-            } else {
-                stream << "carl::floor";
-            }
-            stream << "(";
-            expression.getOperand()->accept(*this, data);
-            stream << ")";
-            break;
-        case UnaryNumericalFunctionExpression::OperatorType::Ceil:
-            STORM_LOG_THROW(options.getMode() != ToCppTranslationMode::CastRationalFunction, storm::exceptions::NotSupportedException,
-                            "Ceil is not supported by rational functions.");
-            if (options.getMode() != ToCppTranslationMode::CastRationalNumber) {
-                stream << "std::ceil";
-            } else {
-                stream << "carl::ceil";
-            }
-            stream << "(";
-            expression.getOperand()->accept(*this, data);
-            stream << ")";
-            break;
-    }
-    return boost::none;
-}
-
-boost::any ToCppVisitor::visit(BooleanLiteralExpression const& expression, boost::any const&) {
-    stream << std::boolalpha << expression.getValue();
-    return boost::none;
-}
-
-boost::any ToCppVisitor::visit(IntegerLiteralExpression const& expression, boost::any const& data) {
-    ToCppTranslationOptions const& options = boost::any_cast<ToCppTranslationOptions const&>(data);
-    switch (options.getMode()) {
-        case ToCppTranslationMode::KeepType:
-            stream << expression.getValue();
-            break;
-        case ToCppTranslationMode::CastDouble:
-            stream << "static_cast<double>(" << expression.getValue() << ")";
-            break;
-        case ToCppTranslationMode::CastRationalNumber:
-            stream << "carl::rationalize<storm::RationalNumber>(\"" << expression.getValue() << "\")";
-            break;
-        case ToCppTranslationMode::CastRationalFunction:
-            stream << "storm::RationalFunction(carl::rationalize<storm::RationalNumber>(\"" << expression.getValue() << "\"))";
-            break;
-    }
-    return boost::none;
-}
-
-boost::any ToCppVisitor::visit(RationalLiteralExpression const& expression, boost::any const& data) {
-    ToCppTranslationOptions const& options = boost::any_cast<ToCppTranslationOptions const&>(data);
-    switch (options.getMode()) {
-        case ToCppTranslationMode::KeepType:
-            stream << "(static_cast<double>(" << carl::getNum(expression.getValue()) << ")/" << carl::getDenom(expression.getValue()) << ")";
-            break;
-        case ToCppTranslationMode::CastDouble:
-            stream << "static_cast<double>(" << expression.getValueAsDouble() << ")";
-            break;
-        case ToCppTranslationMode::CastRationalNumber:
-            stream << "carl::rationalize<storm::RationalNumber>(\"" << expression.getValue() << "\")";
-            break;
-        case ToCppTranslationMode::CastRationalFunction:
-            stream << "storm::RationalFunction(carl::rationalize<storm::RationalNumber>(\"" << expression.getValue() << "\"))";
-            break;
-    }
-    return boost::none;
-}
-
-}  // namespace expressions
-}  // namespace storm
diff --git a/src/storm/storage/expressions/ToCppVisitor.h b/src/storm/storage/expressions/ToCppVisitor.h
deleted file mode 100644
index 64c7828e8..000000000
--- a/src/storm/storage/expressions/ToCppVisitor.h
+++ /dev/null
@@ -1,51 +0,0 @@
-#pragma once
-
-#include <sstream>
-#include <unordered_map>
-
-#include "storm/storage/expressions/ExpressionVisitor.h"
-#include "storm/storage/expressions/Variable.h"
-
-namespace storm {
-namespace expressions {
-class Expression;
-
-enum class ToCppTranslationMode { KeepType, CastDouble, CastRationalNumber, CastRationalFunction };
-
-class ToCppTranslationOptions {
-   public:
-    ToCppTranslationOptions(std::unordered_map<storm::expressions::Variable, std::string> const& prefixes,
-                            std::unordered_map<storm::expressions::Variable, std::string> const& names,
-                            ToCppTranslationMode mode = ToCppTranslationMode::KeepType);
-
-    std::unordered_map<storm::expressions::Variable, std::string> const& getPrefixes() const;
-    std::unordered_map<storm::expressions::Variable, std::string> const& getNames() const;
-    ToCppTranslationMode const& getMode() const;
-
-   private:
-    std::reference_wrapper<std::unordered_map<storm::expressions::Variable, std::string> const> prefixes;
-    std::reference_wrapper<std::unordered_map<storm::expressions::Variable, std::string> const> names;
-    ToCppTranslationMode mode;
-};
-
-class ToCppVisitor : public ExpressionVisitor {
-   public:
-    std::string translate(storm::expressions::Expression const& expression, ToCppTranslationOptions const& options);
-
-    virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override;
-    virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override;
-    virtual boost::any visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) override;
-    virtual boost::any visit(BinaryRelationExpression const& expression, boost::any const& data) override;
-    virtual boost::any visit(VariableExpression const& expression, boost::any const& data) override;
-    virtual boost::any visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) override;
-    virtual boost::any visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) override;
-    virtual boost::any visit(BooleanLiteralExpression const& expression, boost::any const& data) override;
-    virtual boost::any visit(IntegerLiteralExpression const& expression, boost::any const& data) override;
-    virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override;
-
-   private:
-    std::stringstream stream;
-};
-
-}  // namespace expressions
-}  // namespace storm
diff --git a/src/storm/utility/solver.cpp b/src/storm/utility/solver.cpp
index 1ce9b35d3..13afc8331 100644
--- a/src/storm/utility/solver.cpp
+++ b/src/storm/utility/solver.cpp
@@ -128,7 +128,7 @@ std::unique_ptr<storm::solver::SmtSolver> SmtSolverFactory::create(storm::expres
     } else {
 #ifdef STORM_HAVE_Z3
         smtSolverType = storm::solver::SmtSolverType::Z3;
-#elif STORM_HAVE_MSAT
+#elif STORM_HAVE_MATHSAT
         smtSolverType = storm::solver::SmtSolverType::Mathsat;
 #else
         STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Requested an SMT solver but none was installed.");
diff --git a/src/test/storm-gamebased-ar/abstraction/GraphTest.cpp b/src/test/storm-gamebased-ar/abstraction/GraphTest.cpp
index 3b29126e8..70e7cf936 100644
--- a/src/test/storm-gamebased-ar/abstraction/GraphTest.cpp
+++ b/src/test/storm-gamebased-ar/abstraction/GraphTest.cpp
@@ -37,7 +37,7 @@ class GraphTestAR : public ::testing::Test {
 
    protected:
     void SetUp() override {
-#ifndef STORM_HAVE_MSAT
+#ifndef STORM_HAVE_MATHSAT
         GTEST_SKIP() << "MathSAT not available.";
 #endif
     }
diff --git a/src/test/storm-gamebased-ar/abstraction/PrismMenuGameTest.cpp b/src/test/storm-gamebased-ar/abstraction/PrismMenuGameTest.cpp
index 4330f09e9..dd31841ce 100644
--- a/src/test/storm-gamebased-ar/abstraction/PrismMenuGameTest.cpp
+++ b/src/test/storm-gamebased-ar/abstraction/PrismMenuGameTest.cpp
@@ -30,7 +30,7 @@ class PrismMenuGame : public ::testing::Test {
 
    protected:
     void SetUp() override {
-#ifndef STORM_HAVE_MSAT
+#ifndef STORM_HAVE_MATHSAT
         GTEST_SKIP() << "MathSAT not available.";
 #endif
     }
diff --git a/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedDtmcModelCheckerTest.cpp b/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedDtmcModelCheckerTest.cpp
index 358f2794f..ece1d5754 100644
--- a/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedDtmcModelCheckerTest.cpp
+++ b/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedDtmcModelCheckerTest.cpp
@@ -32,7 +32,7 @@ class GameBasedDtmcModelCheckerTest : public ::testing::Test {
 
    protected:
     void SetUp() override {
-#ifndef STORM_HAVE_MSAT
+#ifndef STORM_HAVE_MATHSAT
         GTEST_SKIP() << "MathSAT not available.";
 #endif
     }
diff --git a/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelCheckerTest.cpp b/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelCheckerTest.cpp
index fa17d4cb8..32b1801e5 100644
--- a/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelCheckerTest.cpp
+++ b/src/test/storm-gamebased-ar/modelchecker/abstraction/GameBasedMdpModelCheckerTest.cpp
@@ -30,7 +30,7 @@ class GameBasedMdpModelCheckerTest : public ::testing::Test {
 
    protected:
     void SetUp() override {
-#ifndef STORM_HAVE_MSAT
+#ifndef STORM_HAVE_MATHSAT
         GTEST_SKIP() << "MathSAT not available.";
 #endif
     }
diff --git a/src/test/storm/adapter/MathsatExpressionAdapterTest.cpp b/src/test/storm/adapter/MathsatExpressionAdapterTest.cpp
index df2d2c4c7..45943e85d 100644
--- a/src/test/storm/adapter/MathsatExpressionAdapterTest.cpp
+++ b/src/test/storm/adapter/MathsatExpressionAdapterTest.cpp
@@ -1,7 +1,7 @@
 #include "storm-config.h"
 #include "test/storm_gtest.h"
 
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
 #include "mathsat.h"
 #include "storm/adapters/MathsatExpressionAdapter.h"
 #include "storm/settings/SettingsManager.h"
diff --git a/src/test/storm/solver/MathsatSmtSolverTest.cpp b/src/test/storm/solver/MathsatSmtSolverTest.cpp
index ac5f88cee..a30ad9c0e 100644
--- a/src/test/storm/solver/MathsatSmtSolverTest.cpp
+++ b/src/test/storm/solver/MathsatSmtSolverTest.cpp
@@ -1,7 +1,7 @@
 #include "storm-config.h"
 #include "test/storm_gtest.h"
 
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
 #include "storm/solver/MathsatSmtSolver.h"
 
 TEST(MathsatSmtSolver, CheckSat) {
diff --git a/src/test/storm/storage/JaniModelTest.cpp b/src/test/storm/storage/JaniModelTest.cpp
index 7e3393a6b..445c438f5 100644
--- a/src/test/storm/storage/JaniModelTest.cpp
+++ b/src/test/storm/storage/JaniModelTest.cpp
@@ -6,7 +6,7 @@
 
 #include "storm/storage/jani/Model.h"
 
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
 TEST(JaniModelTest, FlattenComposition) {
     storm::prism::Program program;
     ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"));
diff --git a/src/test/storm/storage/PrismProgramTest.cpp b/src/test/storm/storage/PrismProgramTest.cpp
index feddcbb00..75590784d 100644
--- a/src/test/storm/storage/PrismProgramTest.cpp
+++ b/src/test/storm/storage/PrismProgramTest.cpp
@@ -6,7 +6,7 @@
 #include "storm/storage/jani/Model.h"
 #include "storm/utility/solver.h"
 
-#ifdef STORM_HAVE_MSAT
+#ifdef STORM_HAVE_MATHSAT
 TEST(PrismProgramTest, FlattenModules) {
     storm::prism::Program program;
     ASSERT_NO_THROW(program = storm::parser::PrismParser::parse(STORM_TEST_RESOURCES_DIR "/mdp/leader3.nm"));