diff --git a/CMakeLists.txt b/CMakeLists.txt
index bed5cc152..ba522f0e6 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -45,9 +45,9 @@ set(GMMXX_INCLUDE_DIR ${PROJECT_SOURCE_DIR}/resources/3rdparty/gmm-4.2/include)
 message(STATUS "GMMXX_INCLUDE_DIR is ${GMMXX_INCLUDE_DIR}")
 
 # Set all CUDD references to the version in the repository
-set(CUDD_INCLUDE_DIR ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/include)
+set(CUDD_INCLUDE_DIRS ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/include ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/obj ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/cudd ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/mtr ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/epd)
 set(CUDD_LIBRARY_DIRS ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/cudd ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/mtr ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/util ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/st ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/epd ${PROJECT_SOURCE_DIR}/resources/3rdparty/cudd-2.5.0/obj)
-message(STATUS "CUDD_INCLUDE_DIR is ${CUDD_INCLUDE_DIR}")
+message(STATUS "CUDD_INCLUDE_DIRS is ${CUDD_INCLUDE_DIRS}")
 message(STATUS "CUDD_LIBRARY_DIRS is ${CUDD_LIBRARY_DIRS}")
 
 # Now define all available custom options
@@ -165,9 +165,9 @@ if (ADDITIONAL_LINK_DIRS)
 	link_directories(${ADDITIONAL_LINK_DIRS})
 endif(ADDITIONAL_LINK_DIRS)
 
-if (CUDD_INCLUDE_DIR)
-    include_directories(${CUDD_INCLUDE_DIR})
-endif(CUDD_INCLUDE_DIR)
+if (CUDD_INCLUDE_DIRS)
+    include_directories(${CUDD_INCLUDE_DIRS})
+endif(CUDD_INCLUDE_DIRS)
 if (CUDD_LIBRARY_DIRS)
     link_directories(${CUDD_LIBRARY_DIRS})
 endif(CUDD_LIBRARY_DIRS)
diff --git a/resources/3rdparty/cudd-2.5.0/cudd/cudd.h b/resources/3rdparty/cudd-2.5.0/cudd/cudd.h
index 2493cbae0..d60d0c8f8 100644
--- a/resources/3rdparty/cudd-2.5.0/cudd/cudd.h
+++ b/resources/3rdparty/cudd-2.5.0/cudd/cudd.h
@@ -784,6 +784,12 @@ extern DdNode * Cudd_addNand (DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addNor (DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addXor (DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addXnor (DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addEquals (DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addNotEquals (DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addGreaterThan (DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addGreaterThanEquals (DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addLessThan (DdManager *dd, DdNode **f, DdNode **g);
+extern DdNode * Cudd_addLessThanEquals (DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addMonadicApply (DdManager * dd, DdNode * (*op)(DdManager *, DdNode *), DdNode * f);
 extern DdNode * Cudd_addLog (DdManager * dd, DdNode * f);
 extern DdNode * Cudd_addEquals (DdManager *dd, DdNode **f, DdNode **g);
diff --git a/resources/3rdparty/cudd-2.5.0/obj/cuddObj.cc b/resources/3rdparty/cudd-2.5.0/obj/cuddObj.cc
index 8722ca82f..b8a7f2179 100644
--- a/resources/3rdparty/cudd-2.5.0/obj/cuddObj.cc
+++ b/resources/3rdparty/cudd-2.5.0/obj/cuddObj.cc
@@ -2773,6 +2773,66 @@ Cudd::addResidue(
 
 } // Cudd::addResidue
 
+ADD
+ADD::Equals(const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addEquals, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+
+} // ADD::Equals
+
+ADD
+ADD::NotEquals(const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addNotEquals, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+
+} // ADD::NotEquals
+
+ADD
+ADD::LessThan(const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addLessThan, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+
+} // ADD::LessThan
+
+ADD
+ADD::LessThanOrEqual(const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addLessThanEquals, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+
+} // ADD::LessThanOrEqual
+
+ADD
+ADD::GreaterThan(const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addGreaterThan, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+
+} // ADD::GreaterThan
+
+ADD
+ADD::GreaterThanOrEqual(const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addGreaterThanEquals, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+
+} // ADD::GreaterThanOrEqual
+
 
 BDD
 BDD::AndAbstract(
diff --git a/resources/3rdparty/cudd-2.5.0/obj/cuddObj.hh b/resources/3rdparty/cudd-2.5.0/obj/cuddObj.hh
index 83a0a924a..726476448 100644
--- a/resources/3rdparty/cudd-2.5.0/obj/cuddObj.hh
+++ b/resources/3rdparty/cudd-2.5.0/obj/cuddObj.hh
@@ -401,6 +401,12 @@ public:
     ADD Cmpl() const;
     ADD Negate() const;
     ADD RoundOff(int N) const;
+    ADD Equals(const ADD& g) const;
+    ADD NotEquals(const ADD& g) const;
+    ADD LessThan(const ADD& g) const;
+    ADD LessThanOrEqual(const ADD& g) const;
+    ADD GreaterThan(const ADD& g) const;
+    ADD GreaterThanOrEqual(const ADD& g) const;
     BDD BddThreshold(CUDD_VALUE_TYPE value) const;
     BDD BddStrictThreshold(CUDD_VALUE_TYPE value) const;
     BDD BddInterval(CUDD_VALUE_TYPE lower, CUDD_VALUE_TYPE upper) const;