diff --git a/CMakeLists.txt b/CMakeLists.txt
index c6d62bdde..a127d5bc1 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -30,6 +30,7 @@ option(LINK_LIBCXXABI "Sets whether libc++abi should be linked." OFF)
 option(USE_LIBCXX "Sets whether the standard library is libc++." OFF)
 set(GUROBI_ROOT "" CACHE STRING "The root directory of Gurobi (if available).")
 set(Z3_ROOT "" CACHE STRING "The root directory of Z3 (if available).")
+set(MathSAT_ROOT "" CACHE STRING "The root directory of MathSAT (if available).")
 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(CUSTOM_BOOST_ROOT "" CACHE STRING "A custom path to the Boost root directory.")
@@ -60,6 +61,7 @@ find_package(Boost REQUIRED)
 find_package(Doxygen REQUIRED)
 find_package(TBB)
 find_package(Threads REQUIRED)
+find_package(GMP)
 
 # If the DEBUG option was turned on, we will target a debug version and a release version otherwise
 if (STORM_DEBUG)
@@ -82,6 +84,12 @@ else()
 	set(Z3_LIB_NAME "z3")
 endif()
 
+if ("${MathSAT_ROOT}" STREQUAL "")
+    set(ENABLE_MathSAT OFF)
+else()
+    set(ENABLE_MathSAT ON)
+endif()
+
 message(STATUS "StoRM - CMAKE_BUILD_TYPE: ${CMAKE_BUILD_TYPE}")
 message(STATUS "StoRM - CMAKE_BUILD_TYPE (ENV): $ENV{CMAKE_BUILD_TYPE}")
 
@@ -207,6 +215,13 @@ else()
 	set(STORM_CPP_Z3_DEF "undef")
 endif()
 
+# MathSAT Defines
+if (ENABLE_MathSAT)
+	set(STORM_CPP_MathSAT_DEF "define")
+else()
+	set(STORM_CPP_MathSAT_DEF "undef")
+endif()
+
 # Intel TBB Defines
 if (TBB_FOUND AND STORM_USE_INTELTBB)
 	set(STORM_CPP_INTELTBB_DEF "define")
@@ -311,6 +326,17 @@ endif()
 if (ENABLE_Z3)
     link_directories("${Z3_ROOT}/bin")
 endif()
+if (ENABLE_MathSAT)
+    link_directories("${MathSAT_ROOT}/lib")
+endif()
+if(GMP_FOUND)
+	link_directories(${GMP_LIBRARY_DIR})
+elseif(MPIR_FOUND)
+	link_directories(${GMP_MPIR_LIBRARY_DIR} ${GMP_MPIRXX_LIBRARY_DIR})
+else(GMP_FOUND)
+	message(FATAL_ERROR "GMP is required for MathSAT, but was not found!")
+endif(GMP_FOUND)
+
 if ((NOT Boost_LIBRARY_DIRS) OR ("${Boost_LIBRARY_DIRS}" STREQUAL ""))
 	set(Boost_LIBRARY_DIRS "${Boost_INCLUDE_DIRS}/stage/lib")
 endif ()
@@ -408,6 +434,32 @@ if (ENABLE_Z3)
     target_link_libraries(storm-performance-tests ${Z3_LIB_NAME})
 endif(ENABLE_Z3)
 
+#############################################################
+##
+##	MathSAT (optional)
+##
+#############################################################
+if (ENABLE_MathSAT)
+    message (STATUS "StoRM - Linking with MathSAT")
+	include_directories("${MathSAT_ROOT}/include")
+    target_link_libraries(storm "mathsat")
+    target_link_libraries(storm-functional-tests "mathsat")
+    target_link_libraries(storm-performance-tests "mathsat")
+	if(GMP_FOUND)
+		include_directories("${GMP_INCLUDE_DIR}")
+		target_link_libraries(storm "gmp")
+		target_link_libraries(storm-functional-tests "gmp")
+		target_link_libraries(storm-performance-tests "gmp")
+	elseif(MPIR_FOUND)
+		include_directories("${GMP_INCLUDE_DIR}")
+		target_link_libraries(storm "mpir" "mpirxx")
+		target_link_libraries(storm-functional-tests "mpir" "mpirxx")
+		target_link_libraries(storm-performance-tests "mpir" "mpirxx")
+	else(GMP_FOUND)
+		message(FATAL_ERROR "GMP is required for MathSAT, but was not found!")
+	endif(GMP_FOUND)
+endif(ENABLE_MathSAT)
+
 #############################################################
 ##
 ##	Google Test gtest
diff --git a/resources/cmake/FindGMP.cmake b/resources/cmake/FindGMP.cmake
new file mode 100644
index 000000000..bec3d9a90
--- /dev/null
+++ b/resources/cmake/FindGMP.cmake
@@ -0,0 +1,54 @@
+# FindGMP.cmake can be found at https://code.google.com/p/origin/source/browse/trunk/cmake/FindGMP.cmake
+# Copyright (c) 2008-2010 Kent State University
+# Copyright (c) 2011-2012 Texas A&M University
+#
+# This file is distributed under the MIT License. See the accompanying file
+# LICENSE.txt or http://www.opensource.org/licenses/mit-license.php for terms
+# and conditions.
+# Modified by David Korzeniewski to also find MPIR as an alternative.
+
+# FIXME: How do I find the version of GMP that I want to use?
+# What versions are available?
+
+# NOTE: GMP prefix is understood to be the path to the root of the GMP
+# installation library.
+set(GMP_PREFIX "" CACHE PATH "The path to the prefix of a GMP installation")
+
+
+find_path(GMP_INCLUDE_DIR gmp.h 
+	PATHS ${GMP_PREFIX}/include /usr/include /usr/local/include)
+
+find_library(GMP_LIBRARY NAMES gmp
+	PATHS ${GMP_PREFIX}/lib /usr/lib /usr/local/lib)
+	
+find_library(GMP_MPIR_LIBRARY NAMES mpir
+	PATHS ${GMP_PREFIX}/lib /usr/lib /usr/local/lib)
+	
+find_library(GMP_MPIRXX_LIBRARY NAMES mpirxx
+	PATHS ${GMP_PREFIX}/lib /usr/lib /usr/local/lib)
+
+
+if(GMP_INCLUDE_DIR AND GMP_LIBRARY)
+	get_filename_component(GMP_LIBRARY_DIR ${GMP_LIBRARY} PATH)
+	set(GMP_FOUND TRUE)
+endif()
+
+if(GMP_INCLUDE_DIR AND GMP_MPIR_LIBRARY AND GMP_MPIRXX_LIBRARY)
+	get_filename_component(GMP_MPIR_LIBRARY_DIR ${GMP_MPIR_LIBRARY} PATH)
+	get_filename_component(GMP_MPIRXX_LIBRARY_DIR ${GMP_MPIRXX_LIBRARY} PATH)
+	set(MPIR_FOUND TRUE)
+endif()
+
+if(GMP_FOUND)
+   if(NOT GMP_FIND_QUIETLY)
+      MESSAGE(STATUS "Found GMP: ${GMP_LIBRARY}")
+   endif()
+elseif(MPIR_FOUND)
+   if(NOT GMP_FIND_QUIETLY)
+      MESSAGE(STATUS "Found GMP alternative MPIR: ${MPIR_LIBRARY} and ${MPIRXX_LIBRARY}")
+   endif()
+elseif(GMP_FOUND)
+   if(GMP_FIND_REQUIRED)
+      message(FATAL_ERROR "Could not find GMP")
+   endif()
+endif()
\ No newline at end of file
diff --git a/storm-config.h.in b/storm-config.h.in
index cb90e5af6..dd19cc6df 100644
--- a/storm-config.h.in
+++ b/storm-config.h.in
@@ -23,6 +23,9 @@
 // Whether Z3 is available and to be used (define/undef)
 #@STORM_CPP_Z3_DEF@ STORM_HAVE_Z3
 
+// Whether MathSAT is available and to be used (define/undef)
+#@STORM_CPP_MathSAT_DEF@ STORM_HAVE_MSAT
+
 // Whether Intel Threading Building Blocks are available and to be used (define/undef)
 #@STORM_CPP_INTELTBB_DEF@ STORM_HAVE_INTELTBB