diff --git a/prism/src/dd/dd_matrix.cc b/prism/src/dd/dd_matrix.cc
index 47c2415a..6f83246e 100644
--- a/prism/src/dd/dd_matrix.cc
+++ b/prism/src/dd/dd_matrix.cc
@@ -33,6 +33,7 @@
 #include <cuddInt.h>
 #include "dd_matrix.h"
 #include "dd_basics.h"
+#include "dd_cudd.h"
 
 extern FILE *dd_out;
 
@@ -53,15 +54,18 @@ double value
 		
 	// build a 0-1 ADD to store position of element of the vector
 	f = DD_Constant(ddman, 1);
+	if (f == NULL) return NULL;
 	for (i = 0; i < num_vars; i++) {
 		Cudd_Ref(tmp = vars[i]);				
 		if ((index & (1l<<(num_vars-i-1))) == 0) {
 			tmp2 = Cudd_addCmpl(ddman, tmp);
+			if (tmp2 == NULL) return NULL;
 			Cudd_Ref(tmp2);
 			Cudd_RecursiveDeref(ddman, tmp);
 			tmp = tmp2;
 		}
 		tmp_f = Cudd_addApply(ddman, Cudd_addTimes, tmp, f);
+		if (tmp_f == NULL) return NULL;
 		Cudd_Ref(tmp_f);
 		Cudd_RecursiveDeref(ddman, tmp);
 		Cudd_RecursiveDeref(ddman, f);
@@ -69,9 +73,11 @@ double value
 	}
 	
 	g = DD_Constant(ddman, value);
-				
+	if (g == NULL) return NULL;
+	
 	// compute new vector
 	res = Cudd_addIte(ddman, f, g, dd);
+	if (res == NULL) return NULL;
 	Cudd_Ref(res);
 	Cudd_RecursiveDeref(ddman, f);
 	Cudd_RecursiveDeref(ddman, g);
@@ -100,15 +106,18 @@ double value
 		
 	// build a 0-1 ADD to store position of element of the matrix
 	f = DD_Constant(ddman, 1);
+	if (f == NULL) return NULL;
 	for (i = 0; i < num_rvars; i++) {
 		Cudd_Ref(tmp = rvars[i]);				
 		if ((rindex & (1l<<(num_rvars-i-1))) == 0) {
 			tmp2 = Cudd_addCmpl(ddman, tmp);
+			if (tmp2 == NULL) return NULL;
 			Cudd_Ref(tmp2);
 			Cudd_RecursiveDeref(ddman, tmp);
 			tmp = tmp2;
 		}
 		tmp_f = Cudd_addApply(ddman, Cudd_addTimes, tmp, f);
+		if (tmp_f == NULL) return NULL;
 		Cudd_Ref(tmp_f);
 		Cudd_RecursiveDeref(ddman, tmp);
 		Cudd_RecursiveDeref(ddman, f);
@@ -118,11 +127,13 @@ double value
 		Cudd_Ref(tmp = cvars[i]);				
 		if ((cindex & (1l<<(num_cvars-i-1))) == 0) {
 			tmp2 = Cudd_addCmpl(ddman, tmp);
+			if (tmp2 == NULL) return NULL;
 			Cudd_Ref(tmp2);
 			Cudd_RecursiveDeref(ddman, tmp);
 			tmp = tmp2;
 		}
 		tmp_f = Cudd_addApply(ddman, Cudd_addTimes, tmp, f);
+		if (tmp_f == NULL) return NULL;
 		Cudd_Ref(tmp_f);
 		Cudd_RecursiveDeref(ddman, tmp);
 		Cudd_RecursiveDeref(ddman, f);
@@ -130,9 +141,11 @@ double value
 	}
 	
 	g = DD_Constant(ddman, value);
-				
+	if (g == NULL) return NULL;
+	
 	// compute new vector
 	res = Cudd_addIte(ddman, f, g, dd);
+	if (res == NULL) return NULL;
 	Cudd_Ref(res);
 	Cudd_RecursiveDeref(ddman, f);
 	Cudd_RecursiveDeref(ddman, g);
@@ -164,15 +177,18 @@ double value
 		
 	// build a 0-1 ADD to store position of element of the matrix
 	f = DD_Constant(ddman, 1);
+	if (f == NULL) return NULL;
 	for (i = 0; i < num_rvars; i++) {
 		Cudd_Ref(tmp = rvars[i]);				
 		if ((rindex & (1l<<(num_rvars-i-1))) == 0) {
 			tmp2 = Cudd_addCmpl(ddman, tmp);
+			if (tmp2 == NULL) return NULL;
 			Cudd_Ref(tmp2);
 			Cudd_RecursiveDeref(ddman, tmp);
 			tmp = tmp2;
 		}
 		tmp_f = Cudd_addApply(ddman, Cudd_addTimes, tmp, f);
+		if (tmp_f == NULL) return NULL;
 		Cudd_Ref(tmp_f);
 		Cudd_RecursiveDeref(ddman, tmp);
 		Cudd_RecursiveDeref(ddman, f);
@@ -182,11 +198,13 @@ double value
 		Cudd_Ref(tmp = cvars[i]);				
 		if ((cindex & (1l<<(num_cvars-i-1))) == 0) {
 			tmp2 = Cudd_addCmpl(ddman, tmp);
+			if (tmp2 == NULL) return NULL;
 			Cudd_Ref(tmp2);
 			Cudd_RecursiveDeref(ddman, tmp);
 			tmp = tmp2;
 		}
 		tmp_f = Cudd_addApply(ddman, Cudd_addTimes, tmp, f);
+		if (tmp_f == NULL) return NULL;
 		Cudd_Ref(tmp_f);
 		Cudd_RecursiveDeref(ddman, tmp);
 		Cudd_RecursiveDeref(ddman, f);
@@ -196,11 +214,13 @@ double value
 		Cudd_Ref(tmp = lvars[i]);				
 		if ((lindex & (1l<<(num_lvars-i-1))) == 0) {
 			tmp2 = Cudd_addCmpl(ddman, tmp);
+			if (tmp2 == NULL) return NULL;
 			Cudd_Ref(tmp2);
 			Cudd_RecursiveDeref(ddman, tmp);
 			tmp = tmp2;
 		}
 		tmp_f = Cudd_addApply(ddman, Cudd_addTimes, tmp, f);
+		if (tmp_f == NULL) return NULL;
 		Cudd_Ref(tmp_f);
 		Cudd_RecursiveDeref(ddman, tmp);
 		Cudd_RecursiveDeref(ddman, f);
@@ -208,9 +228,11 @@ double value
 	}
 	
 	g = DD_Constant(ddman, value);
-				
+	if (g == NULL) return NULL;
+	
 	// compute new vector
 	res = Cudd_addIte(ddman, f, g, dd);
+	if (res == NULL) return NULL;
 	Cudd_Ref(res);
 	Cudd_RecursiveDeref(ddman, f);
 	Cudd_RecursiveDeref(ddman, g);
@@ -246,6 +268,10 @@ long x
 		inputs[vars[i]->index] = ((x & (1l<<(num_vars-i-1))) == 0) ? 0 : 1;
 	}
 	node = Cudd_Eval(ddman, dd, inputs);
+	if (node == NULL) {
+		DD_SetErrorFlag();
+		return 0;
+	}
 	val = Cudd_V(node);
 	
 	if (inputs != NULL) {
@@ -268,6 +294,7 @@ int num_vars
 	DdNode *tmp;
 	
 	tmp = Cudd_addXeqy(ddman, num_vars, rvars, cvars);
+	if (tmp == NULL) return NULL;
 	Cudd_Ref(tmp);
 
 	return tmp;
@@ -330,7 +357,8 @@ int num_vars
 		permut[row_vars[i]->index] = col_vars[i]->index;
 		permut[col_vars[i]->index] = row_vars[i]->index;
 	}	
-	res = Cudd_addPermute(ddman, dd, permut);	
+	res = Cudd_addPermute(ddman, dd, permut);
+	if (res == NULL) return NULL;
 	Cudd_Ref(res);
 	Cudd_RecursiveDeref(ddman, dd);
 
@@ -385,6 +413,10 @@ int accuracy
 			inputs[vars[j]->index] = ((i & (1l<<(num_vars-j-1))) == 0) ? 0 : 1;
 		}
 		node = Cudd_Eval(ddman, dd, inputs);
+		if (node == NULL) {
+			DD_SetErrorFlag();
+			return;
+		}
 		val = Cudd_V(node);
 		switch (accuracy) {
 		case ACCURACY_ZERO_ONE: fprintf(dd_out, "%c", val>0?'1':'0'); break;
@@ -454,6 +486,10 @@ int accuracy
 				inputs[cvars[k]->index] = ((j & (1l<<(num_cvars-k-1))) == 0) ? 0 : 1;
 			}
 			node = Cudd_Eval(ddman, dd, inputs);
+			if (node == NULL) {
+				DD_SetErrorFlag();
+				return;
+			}
 			val = Cudd_V(node);
 			switch (accuracy) {
 			case ACCURACY_ZERO_ONE: fprintf(dd_out, "%c", val>0?'1':'0'); break;
@@ -521,6 +557,10 @@ int accuracy
 				inputs[vars[j]->index] = ((i & (1l<<(num_vars-j-1))) == 0) ? 0 : 1;
 			}
 			node = Cudd_Eval(ddman, dd, inputs);
+			if (node == NULL) {
+				DD_SetErrorFlag();
+				return;
+			}
 			val = Cudd_V(node);
 			switch (accuracy) {
 			case ACCURACY_ZERO_ONE: fprintf(dd_out, "%c", val>0?'1':'0'); break;