diff --git a/resources/3rdparty/sylvan/src/storm_wrapper.cpp b/resources/3rdparty/sylvan/src/storm_wrapper.cpp
index 44f406f1f..4a9aeffe4 100644
--- a/resources/3rdparty/sylvan/src/storm_wrapper.cpp
+++ b/resources/3rdparty/sylvan/src/storm_wrapper.cpp
@@ -43,7 +43,7 @@ void storm_rational_number_init(storm_rational_number_ptr* a) {
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm_rational_number_ptr srn_ptr = new storm::RationalNumber(*((storm::RationalNumber*)(*a)));
+    storm_rational_number_ptr srn_ptr = new storm::RationalNumber(*(static_cast<storm::RationalNumber*>(*a)));
     *a = srn_ptr;
 }
 
@@ -52,7 +52,7 @@ void storm_rational_number_destroy(storm_rational_number_ptr a) {
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber* srn_ptr = (storm::RationalNumber*)a;
+    storm::RationalNumber* srn_ptr = static_cast<storm::RationalNumber*>(a);
     delete srn_ptr;
 }
 
@@ -61,8 +61,8 @@ int storm_rational_number_equals(storm_rational_number_ptr a, storm_rational_num
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber*)a;
-    storm::RationalNumber const& srn_b = *(storm::RationalNumber*)b;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber*>(a);
+    storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber*>(b);
 
     return (srn_a == srn_b) ? 1 : 0;
 }
@@ -73,14 +73,14 @@ char* storm_rational_number_to_str(storm_rational_number_ptr val, char *buf, siz
 #endif
 
     std::stringstream ss;
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber*)val;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber*>(val);
     ss << srn_a;
     std::string s = ss.str();
     if (s.size() + 1 < buflen) {
         std::memcpy(buf, s.c_str(), s.size() + 1);
         return buf;
     } else {
-        char* result = (char*)malloc(s.size() + 1);
+        char* result = static_cast<char*>(malloc(s.size() + 1));
         std::memcpy(result, s.c_str(), s.size() + 1);
         return result;
     }
@@ -91,8 +91,8 @@ storm_rational_number_ptr storm_rational_number_clone(storm_rational_number_ptr
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber* result_srn = new storm::RationalNumber(*((storm::RationalNumber const*)a));
-    return (storm_rational_number_ptr)result_srn;
+    storm::RationalNumber* result_srn = new storm::RationalNumber(*static_cast<storm::RationalNumber const*>(a));
+    return static_cast<storm_rational_number_ptr>(result_srn);
 }
 
 storm_rational_number_ptr storm_rational_number_get_zero() {
@@ -101,7 +101,7 @@ storm_rational_number_ptr storm_rational_number_get_zero() {
 #endif
 
     storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::zero<storm::RationalNumber>());
-    return (storm_rational_number_ptr)result_srn;
+    return static_cast<storm_rational_number_ptr>(result_srn);
 }
 
 storm_rational_number_ptr storm_rational_number_get_one() {
@@ -110,7 +110,7 @@ storm_rational_number_ptr storm_rational_number_get_one() {
 #endif
 
     storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::one<storm::RationalNumber>());
-    return (storm_rational_number_ptr)result_srn;
+    return static_cast<storm_rational_number_ptr>(result_srn);
 }
 
 storm_rational_number_ptr storm_rational_number_get_infinity() {
@@ -119,7 +119,7 @@ storm_rational_number_ptr storm_rational_number_get_infinity() {
 #endif
 
     storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::infinity<storm::RationalNumber>());
-    return (storm_rational_number_ptr)result_srn;
+    return static_cast<storm_rational_number_ptr>(result_srn);
 }
 
 int storm_rational_number_is_zero(storm_rational_number_ptr a) {
@@ -127,7 +127,7 @@ int storm_rational_number_is_zero(storm_rational_number_ptr a) {
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    return storm::utility::isZero(*(storm::RationalNumber const*)a) ? 1 : 0;
+    return storm::utility::isZero(*static_cast<storm::RationalNumber const*>(a)) ? 1 : 0;
 }
 
 uint64_t storm_rational_number_hash(storm_rational_number_ptr const a, uint64_t const seed) {
@@ -135,7 +135,7 @@ uint64_t storm_rational_number_hash(storm_rational_number_ptr const a, uint64_t
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a);
 
     // Taken from boost::hash_combine that we do not call here for the lack of boost headers.
     return seed ^ (std::hash<storm::RationalNumber>()(srn_a) + 0x9e3779b9 + (seed<<6) + (seed>>2));
@@ -146,7 +146,7 @@ double storm_rational_number_get_value_double(storm_rational_number_ptr a) {
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a);
     return storm::utility::convertNumber<double>(srn_a);
 }
 
@@ -164,11 +164,11 @@ storm_rational_number_ptr storm_rational_number_plus(storm_rational_number_ptr a
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
-    storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a);
+    storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber const*>(b);
 
     storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a + srn_b);
-    return (storm_rational_number_ptr)result_srn;
+    return static_cast<storm_rational_number_ptr>(result_srn);
 }
 
 storm_rational_number_ptr storm_rational_number_minus(storm_rational_number_ptr a, storm_rational_number_ptr b) {
@@ -176,11 +176,11 @@ storm_rational_number_ptr storm_rational_number_minus(storm_rational_number_ptr
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
-    storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a);
+    storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber const*>(b);
 
     storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a - srn_b);
-    return (storm_rational_number_ptr)result_srn;
+    return static_cast<storm_rational_number_ptr>(result_srn);
 }
 
 storm_rational_number_ptr storm_rational_number_times(storm_rational_number_ptr a, storm_rational_number_ptr b) {
@@ -188,11 +188,11 @@ storm_rational_number_ptr storm_rational_number_times(storm_rational_number_ptr
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
-    storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a);
+    storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber const*>(b);
 
     storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a * srn_b);
-    return (storm_rational_number_ptr)result_srn;
+    return static_cast<storm_rational_number_ptr>(result_srn);
 }
 
 storm_rational_number_ptr storm_rational_number_divide(storm_rational_number_ptr a, storm_rational_number_ptr b) {
@@ -200,11 +200,11 @@ storm_rational_number_ptr storm_rational_number_divide(storm_rational_number_ptr
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
-    storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a);
+    storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber const*>(b);
 
     storm::RationalNumber* result_srn = new storm::RationalNumber(srn_a / srn_b);
-    return (storm_rational_number_ptr)result_srn;
+    return static_cast<storm_rational_number_ptr>(result_srn);
 }
 
 storm_rational_number_ptr storm_rational_number_pow(storm_rational_number_ptr a, storm_rational_number_ptr b) {
@@ -212,12 +212,12 @@ storm_rational_number_ptr storm_rational_number_pow(storm_rational_number_ptr a,
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
-    storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a);
+    storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber const*>(b);
 
     carl::sint exponentAsInteger = carl::toInt<carl::sint>(srn_b);
     storm::RationalNumber* result_srn = new storm::RationalNumber(storm::utility::pow(srn_a, exponentAsInteger));
-    return (storm_rational_number_ptr)result_srn;
+    return static_cast<storm_rational_number_ptr>(result_srn);
 }
 
 storm_rational_number_ptr storm_rational_number_mod(storm_rational_number_ptr a, storm_rational_number_ptr b) {
@@ -225,11 +225,11 @@ storm_rational_number_ptr storm_rational_number_mod(storm_rational_number_ptr a,
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
-    storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a);
+    storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber const*>(b);
     if (carl::isInteger(srn_a) && carl::isInteger(srn_b)) {
         storm::RationalNumber* result_srn = new storm::RationalNumber(carl::mod(carl::getNum(srn_a), carl::getNum(srn_b)));
-        return (storm_rational_number_ptr)result_srn;
+        return static_cast<storm_rational_number_ptr>(result_srn);
     }
     throw storm::exceptions::InvalidOperationException() << "Modulo not supported for rational, non-integer numbers.";
 }
@@ -247,8 +247,8 @@ int storm_rational_number_less(storm_rational_number_ptr a, storm_rational_numbe
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
-    storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a);
+    storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber const*>(b);
 
     if (storm::utility::isInfinity<storm::RationalNumber>(srn_b)) {
         return storm::utility::isInfinity<storm::RationalNumber>(srn_a) ? 0 : 1;
@@ -264,8 +264,8 @@ int storm_rational_number_less_or_equal(storm_rational_number_ptr a, storm_ratio
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
-    storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a);
+    storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber const*>(b);
 
     if (storm::utility::isInfinity<storm::RationalNumber>(srn_b)) {
         return 1;
@@ -281,9 +281,9 @@ storm_rational_number_ptr storm_rational_number_negate(storm_rational_number_ptr
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a);
     storm::RationalNumber* result_srn = new storm::RationalNumber(-srn_a);
-    return (storm_rational_number_ptr)result_srn;
+    return static_cast<storm_rational_number_ptr>(result_srn);
 }
 
 storm_rational_number_ptr storm_rational_number_floor(storm_rational_number_ptr a) {
@@ -291,9 +291,9 @@ storm_rational_number_ptr storm_rational_number_floor(storm_rational_number_ptr
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a);
     storm::RationalNumber* result_srn = new storm::RationalNumber(carl::floor(srn_a));
-    return (storm_rational_number_ptr)result_srn;
+    return static_cast<storm_rational_number_ptr>(result_srn);
 }
 
 storm_rational_number_ptr storm_rational_number_ceil(storm_rational_number_ptr a) {
@@ -301,9 +301,9 @@ storm_rational_number_ptr storm_rational_number_ceil(storm_rational_number_ptr a
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a);
     storm::RationalNumber* result_srn = new storm::RationalNumber(carl::ceil(srn_a));
-    return (storm_rational_number_ptr)result_srn;
+    return static_cast<storm_rational_number_ptr>(result_srn);
 }
 
 storm_rational_number_ptr storm_double_sharpen(double value, size_t precision) {
@@ -314,9 +314,9 @@ storm_rational_number_ptr storm_double_sharpen(double value, size_t precision) {
     try {
         storm::RationalNumber tmp = storm::utility::kwek_mehlhorn::sharpen<storm::RationalNumber, double>(precision, value);
         storm::RationalNumber* result_srn = new storm::RationalNumber(tmp);
-        return (storm_rational_number_ptr)result_srn;
+        return static_cast<storm_rational_number_ptr>(result_srn);
     } catch (storm::exceptions::PrecisionExceededException const& e) {
-        return (storm_rational_number_ptr)0;
+        return nullptr;
     }
 }
 
@@ -325,10 +325,10 @@ storm_rational_number_ptr storm_rational_number_sharpen(storm_rational_number_pt
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a);
     storm::RationalNumber tmp = storm::utility::kwek_mehlhorn::sharpen<storm::RationalNumber, storm::RationalNumber>(precision, srn_a);
     storm::RationalNumber* result_srn = new storm::RationalNumber(tmp);
-    return (storm_rational_number_ptr)result_srn;
+    return static_cast<storm_rational_number_ptr>(result_srn);
 }
 
 int storm_rational_number_equal_modulo_precision(int relative, storm_rational_number_ptr a, storm_rational_number_ptr b, storm_rational_number_ptr precision) {
@@ -336,9 +336,9 @@ int storm_rational_number_equal_modulo_precision(int relative, storm_rational_nu
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
-    storm::RationalNumber const& srn_b = *(storm::RationalNumber const*)b;
-    storm::RationalNumber const& srn_p = *(storm::RationalNumber const*)precision;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a);
+    storm::RationalNumber const& srn_b = *static_cast<storm::RationalNumber const*>(b);
+    storm::RationalNumber const& srn_p = *static_cast<storm::RationalNumber const*>(precision);
 
     if (relative) {
         if (storm::utility::isZero<storm::RationalNumber>(srn_a)) {
@@ -356,7 +356,7 @@ void print_storm_rational_number(storm_rational_number_ptr a) {
     std::lock_guard<std::mutex> lock(rationalNumberMutex);
 #endif
 
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a);
 }
 
 void print_storm_rational_number_to_file(storm_rational_number_ptr a, FILE* out) {
@@ -365,7 +365,7 @@ void print_storm_rational_number_to_file(storm_rational_number_ptr a, FILE* out)
 #endif
 
     std::stringstream ss;
-    storm::RationalNumber const& srn_a = *(storm::RationalNumber const*)a;
+    storm::RationalNumber const& srn_a = *static_cast<storm::RationalNumber const*>(a);
     ss << srn_a;
     std::string s = ss.str();
     fprintf(out, "%s", s.c_str());
@@ -380,7 +380,7 @@ void storm_rational_function_init(storm_rational_function_ptr* a) {
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm_rational_function_ptr srf_ptr = new storm::RationalFunction(*((storm::RationalFunction*)(*a)));
+    storm_rational_function_ptr srf_ptr = new storm::RationalFunction(*static_cast<storm::RationalFunction*>(*a));
     *a = srf_ptr;
 }
 
@@ -389,7 +389,7 @@ void storm_rational_function_destroy(storm_rational_function_ptr a) {
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm::RationalFunction* srf = (storm::RationalFunction*)a;
+    storm::RationalFunction* srf = static_cast<storm::RationalFunction*>(a);
     delete srf;
 }
 
@@ -398,8 +398,8 @@ int storm_rational_function_equals(storm_rational_function_ptr a, storm_rational
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm::RationalFunction const& srf_a = *(storm::RationalFunction*)a;
-    storm::RationalFunction const& srf_b = *(storm::RationalFunction*)b;
+    storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction*>(a);
+    storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction*>(b);
 
     return (srf_a == srf_b) ? 1 : 0;
 }
@@ -410,14 +410,14 @@ char* storm_rational_function_to_str(storm_rational_function_ptr val, char* buf,
 #endif
 
     std::stringstream ss;
-    storm::RationalFunction const& srf_a = *(storm::RationalFunction*)val;
+    storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction*>(val);
     ss << srf_a;
     std::string s = ss.str();
     if (s.size() + 1 < buflen) {
         std::strcpy(buf, s.c_str());
         return buf;
     } else {
-        char* result = (char*)malloc(s.size() + 1);
+        char* result = static_cast<char*>(malloc(s.size() + 1));
         std::strcpy(result, s.c_str());
         return result;
     }
@@ -428,8 +428,8 @@ storm_rational_function_ptr storm_rational_function_clone(storm_rational_functio
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm::RationalFunction* result_srf = new storm::RationalFunction(*((storm::RationalFunction const*)a));
-    return (storm_rational_function_ptr)result_srf;
+    storm::RationalFunction* result_srf = new storm::RationalFunction(*static_cast<storm::RationalFunction const*>(a));
+    return static_cast<storm_rational_function_ptr>(result_srf);
 }
 
 storm_rational_function_ptr storm_rational_function_get_zero() {
@@ -438,7 +438,7 @@ storm_rational_function_ptr storm_rational_function_get_zero() {
 #endif
 
     storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::zero<storm::RationalFunction>());
-    return (storm_rational_function_ptr)result_srf;
+    return static_cast<storm_rational_function_ptr>(result_srf);
 }
 
 storm_rational_function_ptr storm_rational_function_get_one() {
@@ -447,7 +447,7 @@ storm_rational_function_ptr storm_rational_function_get_one() {
 #endif
 
     storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::one<storm::RationalFunction>());
-    return (storm_rational_function_ptr)result_srf;
+    return static_cast<storm_rational_function_ptr>(result_srf);
 }
 
 storm_rational_function_ptr storm_rational_function_get_infinity() {
@@ -456,7 +456,7 @@ storm_rational_function_ptr storm_rational_function_get_infinity() {
 #endif
 
     storm::RationalFunction* result_srf = new storm::RationalFunction(storm::utility::infinity<storm::RationalFunction>());
-    return (storm_rational_function_ptr)result_srf;
+    return static_cast<storm_rational_function_ptr>(result_srf);
 }
 
 
@@ -465,7 +465,7 @@ int storm_rational_function_is_zero(storm_rational_function_ptr a) {
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    return storm::utility::isZero(*(storm::RationalFunction const*)a) ? 1 : 0;
+    return storm::utility::isZero(*static_cast<storm::RationalFunction const*>(a)) ? 1 : 0;
 }
 
 uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint64_t const seed) {
@@ -473,7 +473,7 @@ uint64_t storm_rational_function_hash(storm_rational_function_ptr const a, uint6
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
+    storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a);
 
     // Taken from boost::hash_combine that we do not call here for the lack of boost headers.
     return seed ^ (std::hash<storm::RationalFunction>()(srf_a) + 0x9e3779b9 + (seed<<6) + (seed>>2));
@@ -484,7 +484,7 @@ double storm_rational_function_get_value_double(storm_rational_function_ptr a) {
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
+    storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a);
     if (srf_a.isConstant()) {
         return storm::utility::convertNumber<double>(srf_a);
     } else {
@@ -497,12 +497,12 @@ storm_rational_function_ptr storm_rational_function_plus(storm_rational_function
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
-    storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
+    storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a);
+    storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction const*>(b);
 
     storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
     *result_srf += srf_b;
-    return (storm_rational_function_ptr)result_srf;
+    return static_cast<storm_rational_function_ptr>(result_srf);
 }
 
 storm_rational_function_ptr storm_rational_function_minus(storm_rational_function_ptr a, storm_rational_function_ptr b) {
@@ -510,12 +510,12 @@ storm_rational_function_ptr storm_rational_function_minus(storm_rational_functio
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
-    storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
+    storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a);
+    storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction const*>(b);
 
     storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
     *result_srf -= srf_b;
-    return (storm_rational_function_ptr)result_srf;
+    return static_cast<storm_rational_function_ptr>(result_srf);
 }
 
 storm_rational_function_ptr storm_rational_function_times(storm_rational_function_ptr a, storm_rational_function_ptr b) {
@@ -523,12 +523,12 @@ storm_rational_function_ptr storm_rational_function_times(storm_rational_functio
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
-    storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
+    storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a);
+    storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction const*>(b);
 
     storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
     *result_srf *= srf_b;
-    return (storm_rational_function_ptr)result_srf;
+    return static_cast<storm_rational_function_ptr>(result_srf);
 }
 
 storm_rational_function_ptr storm_rational_function_divide(storm_rational_function_ptr a, storm_rational_function_ptr b) {
@@ -536,12 +536,12 @@ storm_rational_function_ptr storm_rational_function_divide(storm_rational_functi
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
-    storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
+    storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a);
+    storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction const*>(b);
 
     storm::RationalFunction* result_srf = new storm::RationalFunction(srf_a);
     *result_srf /= srf_b;
-    return (storm_rational_function_ptr)result_srf;
+    return static_cast<storm_rational_function_ptr>(result_srf);
 }
 
 storm_rational_function_ptr storm_rational_function_pow(storm_rational_function_ptr a, storm_rational_function_ptr b) {
@@ -549,12 +549,12 @@ storm_rational_function_ptr storm_rational_function_pow(storm_rational_function_
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
-    storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
+    storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a);
+    storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction const*>(b);
 
     carl::uint exponentAsInteger = carl::toInt<carl::uint>(srf_b.nominatorAsNumber());
     storm::RationalFunction* result_srf = new storm::RationalFunction(carl::pow(srf_a, exponentAsInteger));
-    return (storm_rational_function_ptr)result_srf;
+    return static_cast<storm_rational_function_ptr>(result_srf);
 }
 
 storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_ptr a, storm_rational_function_ptr b) {
@@ -562,8 +562,8 @@ storm_rational_function_ptr storm_rational_function_mod(storm_rational_function_
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
-    storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
+    storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a);
+    storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction const*>(b);
 
     if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b)) {
         throw storm::exceptions::InvalidOperationException() << "Operands of mod must not be non-constant rational functions.";
@@ -584,8 +584,8 @@ int storm_rational_function_less(storm_rational_function_ptr a, storm_rational_f
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
-    storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
+    storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a);
+    storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction const*>(b);
     if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b)) {
         throw storm::exceptions::InvalidOperationException() << "Operands of less must not be non-constant rational functions.";
     }
@@ -607,8 +607,8 @@ int storm_rational_function_less_or_equal(storm_rational_function_ptr a, storm_r
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
-    storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
+    storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a);
+    storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction const*>(b);
     if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b)) {
         throw storm::exceptions::InvalidOperationException() << "Operands of less-or-equal must not be non-constant rational functions.";
     }
@@ -630,9 +630,9 @@ storm_rational_function_ptr storm_rational_function_negate(storm_rational_functi
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
+    storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a);
     storm::RationalFunction* result_srf = new storm::RationalFunction(-srf_a);
-    return (storm_rational_function_ptr)result_srf;
+    return static_cast<storm_rational_function_ptr>(result_srf);
 }
 
 storm_rational_function_ptr storm_rational_function_floor(storm_rational_function_ptr a) {
@@ -640,12 +640,12 @@ storm_rational_function_ptr storm_rational_function_floor(storm_rational_functio
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
+    storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a);
     if (!storm::utility::isConstant(srf_a)) {
         throw storm::exceptions::InvalidOperationException() << "Operand of floor must not be non-constant rational function.";
     }
     storm::RationalFunction* result_srf = new storm::RationalFunction(carl::floor(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a)));
-    return (storm_rational_function_ptr)result_srf;
+    return static_cast<storm_rational_function_ptr>(result_srf);
 }
 
 storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function_ptr a) {
@@ -653,12 +653,12 @@ storm_rational_function_ptr storm_rational_function_ceil(storm_rational_function
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
+    storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a);
     if (!storm::utility::isConstant(srf_a)) {
         throw storm::exceptions::InvalidOperationException() << "Operand of ceil must not be non-constant rational function.";
     }
     storm::RationalFunction* result_srf = new storm::RationalFunction(carl::ceil(storm::utility::convertNumber<storm::RationalFunctionCoefficient>(srf_a)));
-    return (storm_rational_function_ptr)result_srf;
+    return static_cast<storm_rational_function_ptr>(result_srf);
 }
 
 int storm_rational_function_equal_modulo_precision(int relative, storm_rational_function_ptr a, storm_rational_function_ptr b, storm_rational_function_ptr precision) {
@@ -666,9 +666,9 @@ int storm_rational_function_equal_modulo_precision(int relative, storm_rational_
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
-    storm::RationalFunction const& srf_b = *(storm::RationalFunction const*)b;
-    storm::RationalFunction const& srf_p = *(storm::RationalFunction const*)precision;
+    storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a);
+    storm::RationalFunction const& srf_b = *static_cast<storm::RationalFunction const*>(b);
+    storm::RationalFunction const& srf_p = *static_cast<storm::RationalFunction const*>(precision);
 
     if (!storm::utility::isConstant(srf_a) || !storm::utility::isConstant(srf_b) || !storm::utility::isConstant(srf_p)) {
         throw storm::exceptions::InvalidOperationException() << "Operands of equal-modulo-precision must not be non-constant rational functions.";
@@ -690,7 +690,7 @@ void print_storm_rational_function(storm_rational_function_ptr a) {
     std::lock_guard<std::mutex> lock(rationalFunctionMutex);
 #endif
 
-    storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
+    storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a);
     std::cout << srf_a << std::flush;
 }
 
@@ -700,7 +700,7 @@ void print_storm_rational_function_to_file(storm_rational_function_ptr a, FILE*
 #endif
 
     std::stringstream ss;
-    storm::RationalFunction const& srf_a = *(storm::RationalFunction const*)a;
+    storm::RationalFunction const& srf_a = *static_cast<storm::RationalFunction const*>(a);
     ss << srf_a;
     std::string s = ss.str();
     fprintf(out, "%s", s.c_str());