diff --git a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc
index d59080a7d..fd2622c2a 100644
--- a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc
+++ b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.cc
@@ -3154,6 +3154,66 @@ ADD::GreaterThanOrEqual(const ADD& g) const
         
 } // ADD::GreaterThanOrEqual
 
+ADD
+ADD::EqualsBdd(const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addToBddEquals, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+        
+} // ADD::EqualsBdd
+    
+ADD
+ADD::NotEqualsBdd(const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addToBddNotEquals, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+    
+} // ADD::NotEqualsBdd
+    
+ADD
+ADD::LessThanBdd(const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addToBddLessThan, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+        
+} // ADD::LessThanBdd
+    
+ADD
+ADD::LessThanOrEqualBdd(const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addToBddLessThanEquals, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+        
+} // ADD::LessThanOrEqualBdd
+    
+ADD
+ADD::GreaterThanBdd(const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addToBddGreaterThan, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+        
+} // ADD::GreaterThanBdd
+    
+ADD
+ADD::GreaterThanOrEqualBdd(const ADD& g) const
+{
+    DdManager *mgr = checkSameManager(g);
+    DdNode *result = Cudd_addApply(mgr, Cudd_addToBddGreaterThanEquals, node, g.node);
+    checkReturnValue(result);
+    return ADD(p, result);
+        
+} // ADD::GreaterThanOrEqualBdd
+    
 BDD
 BDD::AndAbstract(
   const BDD& g,
diff --git a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh
index 15f3b7ae1..a4ea48a41 100644
--- a/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh
+++ b/resources/3rdparty/cudd-3.0.0/cplusplus/cuddObj.hh
@@ -376,6 +376,12 @@ public:
     ADD LessThanOrEqual(const ADD& g) const;
     ADD GreaterThan(const ADD& g) const;
     ADD GreaterThanOrEqual(const ADD& g) const;
+    BDD EqualsBdd(const ADD& g) const;
+    BDD NotEqualsBdd(const ADD& g) const;
+    BDD LessThanBdd(const ADD& g) const;
+    BDD LessThanOrEqualBdd(const ADD& g) const;
+    BDD GreaterThanBdd(const ADD& g) const;
+    BDD GreaterThanOrEqualBdd(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;
diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c
index d7a3c71cc..53b259db6 100644
--- a/resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c
+++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddAddApply.c
@@ -817,6 +817,38 @@ Cudd_addEquals(
     
 } /* 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]
+ 
+ Added 23/08/2016 by Christian Dehnert
+ 
+ ******************************************************************************/
+DdNode *
+Cudd_addToBddEquals(
+               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(Cudd_Not(DD_ONE(dd)));
+    if (F > G) { /* swap f and g */
+        *f = G;
+        *g = F;
+    }
+    return(NULL);
+    
+} /* end of Cudd_addToBddEquals */
 
 /**Function********************************************************************
  
@@ -849,6 +881,39 @@ Cudd_addNotEquals(
     
 } /* 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]
+ 
+ Added 23/08/2016 by Christian Dehnert
+
+ ******************************************************************************/
+DdNode *
+Cudd_addToBddNotEquals(
+                  DdManager * dd,
+                  DdNode ** f,
+                  DdNode ** g)
+{
+    DdNode *F, *G;
+    
+    F = *f; G = *g;
+    if (F == G) return(Cudd_Not(DD_ONE(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_addToBddNotEquals */
+
 /**Function********************************************************************
  
  Synopsis    [1 if f>g; 0 otherwise.]
@@ -878,6 +943,37 @@ Cudd_addGreaterThan(
     
 } /* 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]
+ 
+ Added 23/08/2016 by Christian Dehnert
+
+ ******************************************************************************/
+DdNode *
+Cudd_addToBddGreaterThan(
+                    DdManager * dd,
+                    DdNode ** f,
+                    DdNode ** g)
+{
+    DdNode *F, *G;
+    
+    F = *f; G = *g;
+    if (F == G) return(Cudd_Not(DD_ONE(dd)));
+    if (cuddIsConstant(F) && cuddIsConstant(G)) {
+        if (cuddV(F)>cuddV(G)) return (DD_ONE(dd)); else return (Cudd_Not(DD_ONE(dd)));
+    }
+    return(NULL);
+    
+} /* end of Cudd_addToBddGreaterThan */
+
 
 /**Function********************************************************************
  
@@ -908,6 +1004,36 @@ Cudd_addGreaterThanEquals(
     
 } /* 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]
+ 
+ Added 23/08/2016 by Christian Dehnert
+
+ ******************************************************************************/
+DdNode *
+Cudd_addToBddGreaterThanEquals(
+                          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 (Cudd_Not(DD_ONE(dd)));
+    }
+    return(NULL);
+    
+} /* end of Cudd_addToBddGreaterThanEquals */
 
 /**Function********************************************************************
  
@@ -938,6 +1064,36 @@ Cudd_addLessThan(
     
 } /* 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]
+ 
+ Added 23/08/2016 by Christian Dehnert
+
+ ******************************************************************************/
+DdNode *
+Cudd_addToBddLessThan(
+                 DdManager * dd,
+                 DdNode ** f,
+                 DdNode ** g)
+{
+    DdNode *F, *G;
+    
+    F = *f; G = *g;
+    if (F == G) return(Cudd_Not(DD_ONE(dd)));
+    if (cuddIsConstant(F) && cuddIsConstant(G)) {
+        if (cuddV(F)<cuddV(G)) return (DD_ONE(dd)); else return (Cudd_Not(DD_ONE(dd)));
+    }
+    return(NULL);
+    
+} /* end of Cudd_addToBddLessThan */
 
 /**Function********************************************************************
  
@@ -968,6 +1124,37 @@ Cudd_addLessThanEquals(
     
 } /* end of Cudd_addLessThanEquals */
 
+/**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]
+ 
+ Added 23/08/2016 by Christian Dehnert
+
+ ******************************************************************************/
+DdNode *
+Cudd_addToBddLessThanEquals(
+                       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 (Cudd_Not(DD_ONE(dd)));
+    }
+    return(NULL);
+    
+} /* end of Cudd_addToBddLessThanEquals */
+
 /**Function********************************************************************
  
  Synopsis    [f to the power of g.]
diff --git a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c
index ef0c3f6f8..118badbba 100644
--- a/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c
+++ b/resources/3rdparty/cudd-3.0.0/cudd/cuddBddAbs.c
@@ -521,7 +521,6 @@ cuddBddExistAbstractRepresentativeRecur(
   DdNode * f,
   DdNode * cube)
 {
-//    printf("entering exists abstract...\n");
     DdNode	*F, *T, *E, *res, *res1, *res2, *one, *zero, *left, *right, *tmp, *res1Inf, *res2Inf;
     
     statLine(manager);
@@ -535,12 +534,10 @@ cuddBddExistAbstractRepresentativeRecur(
     /* Cube is guaranteed to be a cube at this point. */
     if (F == one) {
         if (fIsNegated) {
-            //            printf("return in preprocessing...\n");
             return f;
         }
         
         if (cube == one) {
-            //            printf("return in preprocessing...\n");
             return one;
         } else {
             res = cuddBddExistAbstractRepresentativeRecur(manager, f, cuddT(cube));
@@ -549,7 +546,7 @@ cuddBddExistAbstractRepresentativeRecur(
             }
             cuddRef(res);
             
-            res1 = cuddBddIteRecur(manager, manager->vars[cube->index], zero, res);
+            res1 = cuddUniqueInter(manager, (int) cube->index, zero, res);
             if (res1 == NULL) {
                 Cudd_IterDerefBdd(manager,res);
                 Cudd_IterDerefBdd(manager,zero);
@@ -559,12 +556,10 @@ cuddBddExistAbstractRepresentativeRecur(
             return(res1);
         }
     } else if (cube == one) {
-        //        printf("return in preprocessing...\n");
         return f;
     }
     /* From now on, cube and f are non-constant. */
     
-//    printf("F perm %i and cube perm %i\n", manager->perm[F->index], manager->perm[cube->index]);
     
     /* Abstract a variable that does not appear in f. */
     if (manager->perm[F->index] > manager->perm[cube->index]) {
@@ -574,8 +569,7 @@ cuddBddExistAbstractRepresentativeRecur(
         }
         cuddRef(res);
         
-//        res1 = cuddUniqueInter(manager, (int) cube->index, zero, res);
-        res1 = cuddBddIteRecur(manager, manager->vars[cube->index], zero, res);
+        res1 = cuddUniqueInter(manager, (int) cube->index, zero, res);
 
         if (res1 == NULL) {
             Cudd_IterDerefBdd(manager,res);
@@ -584,20 +578,17 @@ cuddBddExistAbstractRepresentativeRecur(
         }
         cuddDeref(res);
 
-//        printf("return after abstr. var that does not appear in f...\n");
        	return(res1);
     }
     
     /* Check the cache. */
     if (F->ref != 1 && (res = cuddCacheLookup2(manager, Cudd_bddExistAbstractRepresentative, f, cube)) != NULL) {
-//        printf("return because of cache hit...\n");
         return(res);
     }
     
     /* Compute the cofactors of f. */
     T = cuddT(F); E = cuddE(F);
     if (f != F) {
-//        printf("negating T and E\n");
         T = Cudd_Not(T); E = Cudd_Not(E);
     }
     
@@ -655,8 +646,7 @@ cuddBddExistAbstractRepresentativeRecur(
         Cudd_IterDerefBdd(manager,left);
         
         assert(res1Inf != res2Inf);
-//        res = cuddUniqueInter(manager, (int) f->index, res2Inf, res1Inf);
-        res = cuddBddIteRecur(manager, manager->vars[F->index], res2Inf, res1Inf);
+        res = cuddUniqueInter(manager, (int) F->index, res2Inf, res1Inf);
 
         if (res == NULL) {
             Cudd_IterDerefBdd(manager,res1Inf);
@@ -665,12 +655,11 @@ cuddBddExistAbstractRepresentativeRecur(
         }
         cuddRef(res);
 
-        Cudd_IterDerefBdd(manager,res1Inf);
-        Cudd_IterDerefBdd(manager,res2Inf);
+        cuddDeref(res1Inf);
+        cuddDeref(res2Inf);
 
         cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, res);
         cuddDeref(res);
-//        printf("return properly computed result...\n");
         return(res);
     } else { /* if (cuddI(manager,F->index) < cuddI(manager,cube->index)) */
         res1 = cuddBddExistAbstractRepresentativeRecur(manager, E, cube);
@@ -688,7 +677,7 @@ cuddBddExistAbstractRepresentativeRecur(
         
         /* ITE takes care of possible complementation of res1 and of the
          ** case in which res1 == res2. */
-        res = cuddBddIteRecur(manager, manager->vars[F->index], res2, res1);
+        res = cuddUniqueInter(manager, (int)F->index, res2, res1);
         if (res == NULL) {
             Cudd_IterDerefBdd(manager, res1);
             Cudd_IterDerefBdd(manager, res2);
@@ -699,7 +688,6 @@ cuddBddExistAbstractRepresentativeRecur(
         if (F->ref != 1) {
             cuddCacheInsert2(manager, Cudd_bddExistAbstractRepresentative, f, cube, res);
         }
-//        printf("return of last case...\n");
         return(res);
     }	    
     
diff --git a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
index 90f858756..bb3aee05e 100644
--- a/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
+++ b/src/modelchecker/csl/helper/SparseMarkovAutomatonCslHelper.cpp
@@ -203,7 +203,7 @@ namespace storm {
                 }
                 
                 // Likewise, if all bits are set, we can avoid the computation and set.
-                if ((~psiStates).empty()) {
+                if (psiStates.full()) {
                     return std::vector<ValueType>(numberOfStates, storm::utility::one<ValueType>());
                 }
                 
diff --git a/src/storage/dd/cudd/InternalCuddAdd.cpp b/src/storage/dd/cudd/InternalCuddAdd.cpp
index d23a2c0e3..522477bd6 100644
--- a/src/storage/dd/cudd/InternalCuddAdd.cpp
+++ b/src/storage/dd/cudd/InternalCuddAdd.cpp
@@ -73,32 +73,32 @@ namespace storm {
         
         template<typename ValueType>
         InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::equals(InternalAdd<DdType::CUDD, ValueType> const& other) const {
-            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().Equals(other.getCuddAdd()).BddPattern());
+            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().EqualsBdd(other.getCuddAdd()));
         }
         
         template<typename ValueType>
         InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::notEquals(InternalAdd<DdType::CUDD, ValueType> const& other) const {
-            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().NotEquals(other.getCuddAdd()).BddPattern());
+            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().NotEqualsBdd(other.getCuddAdd()));
         }
         
         template<typename ValueType>
         InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::less(InternalAdd<DdType::CUDD, ValueType> const& other) const {
-            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().LessThan(other.getCuddAdd()).BddPattern());
+            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().LessThanBdd(other.getCuddAdd()));
         }
         
         template<typename ValueType>
         InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::lessOrEqual(InternalAdd<DdType::CUDD, ValueType> const& other) const {
-            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().LessThanOrEqual(other.getCuddAdd()).BddPattern());
+            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().LessThanOrEqualBdd(other.getCuddAdd()));
         }
         
         template<typename ValueType>
         InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::greater(InternalAdd<DdType::CUDD, ValueType> const& other) const {
-            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().GreaterThan(other.getCuddAdd()).BddPattern());
+            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().GreaterThanBdd(other.getCuddAdd()));
         }
         
         template<typename ValueType>
         InternalBdd<DdType::CUDD> InternalAdd<DdType::CUDD, ValueType>::greaterOrEqual(InternalAdd<DdType::CUDD, ValueType> const& other) const {
-            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().GreaterThanOrEqual(other.getCuddAdd()).BddPattern());
+            return InternalBdd<DdType::CUDD>(ddManager, this->getCuddAdd().GreaterThanOrEqualBdd(other.getCuddAdd()));
         }
         
         template<typename ValueType>