diff --git a/src/storm/adapters/RationalFunctionAdapter.h b/src/storm/adapters/RationalFunctionAdapter.h
index f403103f5..39490d81e 100644
--- a/src/storm/adapters/RationalFunctionAdapter.h
+++ b/src/storm/adapters/RationalFunctionAdapter.h
@@ -9,6 +9,27 @@
 #include <carl/core/Relation.h>
 #include <carl/util/stringparser.h>
 
+// Some header files on macOS (included via INTEL TBB) might #define TRUE and FALSE, which in carl/formula/Formula.h are used as FormulaTypes.
+// Hence, we temporarily #undef these:
+#ifdef TRUE
+#define STORM_TEMP_TRUE TRUE
+#undef TRUE
+#endif
+#ifdef FALSE
+#define STORM_TEMP_FALSE FALSE
+#undef FALSE
+#endif
+#include <carl/formula/Formula.h>
+// Restore TRUE / FALSE macros.
+#ifdef STORM_TEMP_TRUE
+#define TRUE STORM_TEMP_TRUE
+#undef STORM_TEMP_TRUE
+#endif
+#ifdef STORM_TEMP_FALSE
+#define FALSE STORM_TEMP_FALSE
+#undef STORM_TEMP_FALSE
+#endif
+
 namespace carl {
     // Define hash values for all polynomials and rational function.
     template<typename C, typename O, typename P>
@@ -57,5 +78,15 @@ namespace storm {
     
     typedef carl::RationalFunction<Polynomial, true> RationalFunction;
     typedef carl::Interval<double> Interval;
+    
+    template <typename ValueType, typename Enable=void>
+    struct ConstraintType {
+        typedef void* val;
+    };
+
+    template<typename ValueType>
+    struct ConstraintType<ValueType, typename std::enable_if<std::is_same<storm::RationalFunction, ValueType>::value>::type> {
+        typedef carl::Formula<typename ValueType::PolyType::PolyType> val;
+    };
 }
 
diff --git a/src/storm/analysis/GraphConditions.h b/src/storm/analysis/GraphConditions.h
index a901dfa68..04b5d7774 100644
--- a/src/storm/analysis/GraphConditions.h
+++ b/src/storm/analysis/GraphConditions.h
@@ -4,21 +4,10 @@
 #include <unordered_set>
 #include "storm/adapters/RationalFunctionAdapter.h"
 #include "storm/models/sparse/Dtmc.h"
-#include <carl/formula/Formula.h>
 
 namespace storm {
     namespace analysis {
 
-        template <typename ValueType, typename Enable=void>
-        struct ConstraintType {
-            typedef void* val;
-        };
-
-        template<typename ValueType>
-        struct ConstraintType<ValueType, typename std::enable_if<std::is_same<storm::RationalFunction, ValueType>::value>::type> {
-            typedef carl::Formula<typename ValueType::PolyType::PolyType> val;
-        };
-        
         /**
          * Class to collect constraints on parametric Markov chains.
          */
@@ -26,11 +15,11 @@ namespace storm {
         class ConstraintCollector {
         private:
             // A set of constraints that says that the DTMC actually has valid probability distributions in all states.
-            std::unordered_set<typename ConstraintType<ValueType>::val> wellformedConstraintSet;
+            std::unordered_set<typename storm::ConstraintType<ValueType>::val> wellformedConstraintSet;
             
             // A set of constraints that makes sure that the underlying graph of the model does not change depending
             // on the parameter values.
-            std::unordered_set<typename ConstraintType<ValueType>::val> graphPreservingConstraintSet;
+            std::unordered_set<typename storm::ConstraintType<ValueType>::val> graphPreservingConstraintSet;
 
             // A set of variables
             std::set<storm::RationalFunctionVariable> variableSet;