diff --git a/resources/3rdparty/cudd-2.5.0/Makefile b/resources/3rdparty/cudd-2.5.0/Makefile
index b1b5f32c8..6c7fbb4d3 100644
--- a/resources/3rdparty/cudd-2.5.0/Makefile
+++ b/resources/3rdparty/cudd-2.5.0/Makefile
@@ -201,7 +201,7 @@ IDIR	= $(DDWDIR)/include
 INCLUDE = -I$(IDIR)
 
 BDIRS	= cudd dddmp mtr st util epd obj
-DIRS	= $(BDIRS) nanotrav
+DIRS	= $(BDIRS)
 
 #------------------------------------------------------------------------
 
diff --git a/resources/3rdparty/cudd-2.5.0/cudd/cudd.h b/resources/3rdparty/cudd-2.5.0/cudd/cudd.h
index 4a54f8e05..2493cbae0 100644
--- a/resources/3rdparty/cudd-2.5.0/cudd/cudd.h
+++ b/resources/3rdparty/cudd-2.5.0/cudd/cudd.h
@@ -786,6 +786,12 @@ extern DdNode * Cudd_addXor (DdManager *dd, DdNode **f, DdNode **g);
 extern DdNode * Cudd_addXnor (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);
+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_addFindMax (DdManager *dd, DdNode *f);
 extern DdNode * Cudd_addFindMin (DdManager *dd, DdNode *f);
 extern DdNode * Cudd_addIthBit (DdManager *dd, DdNode *f, int bit);
diff --git a/resources/3rdparty/cudd-2.5.0/cudd/cuddAddApply.c b/resources/3rdparty/cudd-2.5.0/cudd/cuddAddApply.c
index 4ef228a99..9a4d2179d 100644
--- a/resources/3rdparty/cudd-2.5.0/cudd/cuddAddApply.c
+++ b/resources/3rdparty/cudd-2.5.0/cudd/cuddAddApply.c
@@ -783,7 +783,187 @@ Cudd_addLog(
 
 } /* end of Cudd_addLog */
 
+/**Function********************************************************************
+
+  Synopsis    [1 if f==g; 0 otherwise.]
+
+  Description [Returns NULL if not a terminal case; f op g otherwise,
+  where f op g is 1 if f==g; 0 otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_addApply]
+
+******************************************************************************/
+DdNode *
+Cudd_addEquals(
+  DdManager * dd,
+  DdNode ** f,
+  DdNode ** g)
+{
+    DdNode *F, *G;
+
+    F = *f; G = *g;
+    if (F == G) return(DD_ONE(dd));
+    if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ZERO(dd));
+    if (F > G) { /* swap f and g */
+	*f = G;
+	*g = F;
+    }
+    return(NULL);
+
+} /* end of Cudd_addEquals */
+
+
+/**Function********************************************************************
+
+  Synopsis    [1 if f!=g; 0 otherwise.]
+
+  Description [Returns NULL if not a terminal case; f op g otherwise,
+  where f op g is 1 if f!=g; 0 otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_addApply]
+
+******************************************************************************/
+DdNode *
+Cudd_addNotEquals(
+  DdManager * dd,
+  DdNode ** f,
+  DdNode ** g)
+{
+    DdNode *F, *G;
+
+    F = *f; G = *g;
+    if (F == G) return(DD_ZERO(dd));
+    if (cuddIsConstant(F) && cuddIsConstant(G)) return(DD_ONE(dd));
+    if (F > G) { /* swap f and g */
+	*f = G;
+	*g = F;
+    }
+    return(NULL);
+
+} /* end of Cudd_addNotEquals */
+
+/**Function********************************************************************
+
+  Synopsis    [1 if f>g; 0 otherwise.]
+
+  Description [Returns NULL if not a terminal case; f op g otherwise,
+  where f op g is 1 if f>g; 0 otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_addApply]
+
+******************************************************************************/
+DdNode *
+Cudd_addGreaterThan(
+  DdManager * dd,
+  DdNode ** f,
+  DdNode ** g)
+{
+    DdNode *F, *G;
+
+    F = *f; G = *g;
+    if (F == G) return(DD_ZERO(dd));
+    if (cuddIsConstant(F) && cuddIsConstant(G)) {
+		if (cuddV(F)>cuddV(G)) return (DD_ONE(dd)); else return (DD_ZERO(dd));
+    }
+    return(NULL);
+
+} /* end of Cudd_addGreaterThan */
+
+
+/**Function********************************************************************
+
+  Synopsis    [1 if f>=g; 0 otherwise.]
+
+  Description [Returns NULL if not a terminal case; f op g otherwise,
+  where f op g is 1 if f>=g; 0 otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_addApply]
+
+******************************************************************************/
+DdNode *
+Cudd_addGreaterThanEquals(
+  DdManager * dd,
+  DdNode ** f,
+  DdNode ** g)
+{
+    DdNode *F, *G;
+
+    F = *f; G = *g;
+    if (F == G) return(DD_ONE(dd));
+    if (cuddIsConstant(F) && cuddIsConstant(G)) {
+		if (cuddV(F)>=cuddV(G)) return (DD_ONE(dd)); else return (DD_ZERO(dd));
+    }
+    return(NULL);
+
+} /* end of Cudd_addGreaterThanEquals */
+
+
+/**Function********************************************************************
+
+  Synopsis    [1 if f<g; 0 otherwise.]
+
+  Description [Returns NULL if not a terminal case; f op g otherwise,
+  where f op g is 1 if f<g; 0 otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_addApply]
+
+******************************************************************************/
+DdNode *
+Cudd_addLessThan(
+  DdManager * dd,
+  DdNode ** f,
+  DdNode ** g)
+{
+    DdNode *F, *G;
+
+    F = *f; G = *g;
+    if (F == G) return(DD_ZERO(dd));
+    if (cuddIsConstant(F) && cuddIsConstant(G)) {
+		if (cuddV(F)<cuddV(G)) return (DD_ONE(dd)); else return (DD_ZERO(dd));
+    }
+    return(NULL);
+
+} /* end of Cudd_addLessThan */
+
+
+/**Function********************************************************************
+
+  Synopsis    [1 if f<=g; 0 otherwise.]
+
+  Description [Returns NULL if not a terminal case; f op g otherwise,
+  where f op g is 1 if f<=g; 0 otherwise.]
+
+  SideEffects [None]
+
+  SeeAlso     [Cudd_addApply]
+
+******************************************************************************/
+DdNode *
+Cudd_addLessThanEquals(
+  DdManager * dd,
+  DdNode ** f,
+  DdNode ** g)
+{
+    DdNode *F, *G;
+
+    F = *f; G = *g;
+    if (F == G) return(DD_ONE(dd));
+    if (cuddIsConstant(F) && cuddIsConstant(G)) {
+		if (cuddV(F)<=cuddV(G)) return (DD_ONE(dd)); else return (DD_ZERO(dd));
+    }
+    return(NULL);
 
+} /* end of Cudd_addLessThanEquals */
 /*---------------------------------------------------------------------------*/
 /* Definition of internal functions                                          */
 /*---------------------------------------------------------------------------*/