diff --git a/prism/src/dd/dd_abstr.cc b/prism/src/dd/dd_abstr.cc
index 9dbd35af..8649bd3b 100644
--- a/prism/src/dd/dd_abstr.cc
+++ b/prism/src/dd/dd_abstr.cc
@@ -40,7 +40,9 @@ int num_vars
 )
 {
 	DdNode *cube, *res;
-	
+
+	if (dd == NULL) return NULL;
+
 	cube = Cudd_addComputeCube(ddman, vars, NULL, num_vars);
 	if (cube == NULL) return NULL;
 	Cudd_Ref(cube);
@@ -64,7 +66,9 @@ int num_vars
 )
 {
 	DdNode *cube, *res;
-	
+
+	if (dd == NULL) return NULL;
+
 	cube = Cudd_addComputeCube(ddman, vars, NULL, num_vars);
 	if (cube == NULL) return NULL;
 	Cudd_Ref(cube);
@@ -88,7 +92,9 @@ int num_vars
 )
 {
 	DdNode *cube, *res;
-	
+
+	if (dd == NULL) return NULL;
+
 	cube = Cudd_addComputeCube(ddman, vars, NULL, num_vars);
 	if (cube == NULL) return NULL;
 	Cudd_Ref(cube);
@@ -112,7 +118,9 @@ int num_vars
 )
 {
 	DdNode *cube, *res;
-	
+
+	if (dd == NULL) return NULL;
+
 	cube = Cudd_addComputeCube(ddman, vars, NULL, num_vars);
 	if (cube == NULL) return NULL;
 	Cudd_Ref(cube);
@@ -136,7 +144,9 @@ int num_vars
 )
 {
 	DdNode *cube, *res;
-	
+
+	if (dd == NULL) return NULL;
+
 	cube = Cudd_addComputeCube(ddman, vars, NULL, num_vars);
 	if (cube == NULL) return NULL;
 	Cudd_Ref(cube);
@@ -160,7 +170,9 @@ int num_vars
 )
 {
 	DdNode *cube, *res;
-	
+
+	if (dd == NULL) return NULL;
+
 	cube = Cudd_addComputeCube(ddman, vars, NULL, num_vars);
 	if (cube == NULL) return NULL;
 	Cudd_Ref(cube);
diff --git a/prism/src/dd/dd_basics.cc b/prism/src/dd/dd_basics.cc
index 8ccd5cbf..da0e9fdc 100644
--- a/prism/src/dd/dd_basics.cc
+++ b/prism/src/dd/dd_basics.cc
@@ -102,6 +102,8 @@ DdNode *DD_Not(DdManager *ddman, DdNode *dd)
 {
 	DdNode *res;
 
+	if (dd == NULL) return NULL;
+
 	res = Cudd_addCmpl(ddman, dd);
 	if (res == NULL) return NULL;
 	Cudd_Ref(res);
@@ -116,6 +118,9 @@ DdNode *DD_Or(DdManager *ddman, DdNode *dd1, DdNode *dd2)
 {
 	DdNode *res;
 
+	if (dd1 == NULL) return NULL;
+	if (dd2 == NULL) return NULL;
+
 	res = Cudd_addApply(ddman, Cudd_addOr, dd1, dd2);
 	if (res == NULL) return NULL;
 	Cudd_Ref(res);
@@ -129,16 +134,10 @@ DdNode *DD_Or(DdManager *ddman, DdNode *dd1, DdNode *dd2)
 
 DdNode *DD_And(DdManager *ddman, DdNode *dd1, DdNode *dd2)
 {
-	DdNode *n1 = DD_Not(ddman, dd1);
-	if (n1 == NULL) return NULL;
-
-	DdNode *n2 = DD_Not(ddman, dd2);
-	if (n2 == NULL) return NULL;
+	if (dd1 == NULL) return NULL;
+	if (dd2 == NULL) return NULL;
 
-	DdNode *o = DD_Or(ddman, n1, n2);
-	if (o == NULL) return NULL;
-
-	return DD_Not(ddman, o);
+	return DD_Not(ddman, DD_Or(ddman, DD_Not(ddman, dd1), DD_Not(ddman, dd2))); 
 }
 
 //------------------------------------------------------------------------------
@@ -147,6 +146,9 @@ DdNode *DD_Xor(DdManager *ddman, DdNode *dd1, DdNode *dd2)
 {
 	DdNode *res;
 
+	if (dd1 == NULL) return NULL;
+	if (dd2 == NULL) return NULL;
+
 	res = Cudd_addApply(ddman, Cudd_addXor, dd1, dd2);
 	if (res == NULL) return NULL;
 	Cudd_Ref(res);
@@ -160,10 +162,10 @@ DdNode *DD_Xor(DdManager *ddman, DdNode *dd1, DdNode *dd2)
 
 DdNode *DD_Implies(DdManager *ddman, DdNode *dd1, DdNode *dd2)
 {
-	DdNode *n1 = DD_Not(ddman, dd1);
-	if (n1 == NULL) return NULL;
+	if (dd1 == NULL) return NULL;
+	if (dd2 == NULL) return NULL;
 
-	return DD_Or(ddman, n1, dd2);
+	return DD_Or(ddman, DD_Not(ddman, dd1), dd2);
 }
 
 //------------------------------------------------------------------------------
@@ -172,6 +174,9 @@ DdNode *DD_Apply(DdManager *ddman, int op, DdNode *dd1, DdNode *dd2)
 {
 	DdNode *res;
 
+	if (dd1 == NULL) return NULL;
+	if (dd2 == NULL) return NULL;
+
 	switch (op) {
 		case APPLY_PLUS: res = Cudd_addApply(ddman, Cudd_addPlus, dd1, dd2); break;
 		case APPLY_MINUS: res = Cudd_addApply(ddman, Cudd_addMinus, dd1, dd2); break;
@@ -204,6 +209,8 @@ DdNode *DD_MonadicApply(DdManager *ddman, int op, DdNode *dd)
 {
 	DdNode *res;
 
+	if (dd == NULL) return NULL;
+
 	switch (op) {
 		case APPLY_FLOOR: res = Cudd_addMonadicApply(ddman, Cudd_addFloor, dd); break;
 		case APPLY_CEIL: res = Cudd_addMonadicApply(ddman, Cudd_addCeil, dd); break;
@@ -222,6 +229,9 @@ DdNode *DD_Restrict(DdManager *ddman, DdNode *dd, DdNode *cube)
 {
 	DdNode *res;
 
+	if (dd == NULL) return NULL;
+	if (cube == NULL) return NULL;
+
 	res = Cudd_addRestrict(ddman, dd, cube);
 	if (res == NULL) return NULL;
 	Cudd_Ref(res);
@@ -237,6 +247,10 @@ DdNode *DD_ITE(DdManager *ddman, DdNode *dd1, DdNode *dd2, DdNode *dd3)
 {
 	DdNode *res;
 
+	if (dd1 == NULL) return NULL;
+	if (dd2 == NULL) return NULL;
+	if (dd3 == NULL) return NULL;
+
 	res = Cudd_addIte(ddman, dd1, dd2, dd3);
 	if (res == NULL) return NULL;
 	Cudd_Ref(res);
diff --git a/prism/src/dd/dd_matrix.cc b/prism/src/dd/dd_matrix.cc
index 6f83246e..117afee0 100644
--- a/prism/src/dd/dd_matrix.cc
+++ b/prism/src/dd/dd_matrix.cc
@@ -51,7 +51,9 @@ double value
 {
 	DdNode *tmp, *tmp2, *f, *tmp_f, *g, *res;
 	int i;
-		
+
+	if (dd == NULL) return NULL;
+
 	// build a 0-1 ADD to store position of element of the vector
 	f = DD_Constant(ddman, 1);
 	if (f == NULL) return NULL;
@@ -103,7 +105,9 @@ double value
 {
 	DdNode *tmp, *tmp2, *f, *tmp_f, *g, *res;
 	int i;
-		
+
+	if (dd == NULL) return NULL;
+
 	// build a 0-1 ADD to store position of element of the matrix
 	f = DD_Constant(ddman, 1);
 	if (f == NULL) return NULL;
@@ -174,7 +178,9 @@ double value
 {
 	DdNode *tmp, *tmp2, *f, *tmp_f, *g, *res;
 	int i;
-		
+
+	if (dd == NULL) return NULL;
+
 	// build a 0-1 ADD to store position of element of the matrix
 	f = DD_Constant(ddman, 1);
 	if (f == NULL) return NULL;
@@ -257,6 +263,8 @@ long x
 	int *inputs;
 	double val;
 
+	if (dd == NULL) return NULL;
+
 	// create array to store 0's & 1's used to query DD
 	inputs = new int[Cudd_ReadSize(ddman)];
 	
@@ -313,7 +321,10 @@ int method
 )
 {
 	DdNode *res;
-	
+
+	if (dd1 == NULL) return NULL;
+	if (dd2 == NULL) return NULL;
+
 	if (method == MM_CMU) {
 		res = Cudd_addTimesPlus(ddman, dd1, dd2, vars, num_vars);
 	}
@@ -348,7 +359,9 @@ int num_vars
 {
 	int i, *permut;
 	DdNode *res;
-		
+
+	if (dd == NULL) return NULL;
+
 	permut = new int[Cudd_ReadSize(ddman)];
 	for (i = 0; i < Cudd_ReadSize(ddman); i++) {
 		permut[i] = i;
diff --git a/prism/src/dd/dd_term.cc b/prism/src/dd/dd_term.cc
index 6fdd1046..8a4565fb 100644
--- a/prism/src/dd/dd_term.cc
+++ b/prism/src/dd/dd_term.cc
@@ -43,7 +43,9 @@ double threshold
 )
 {
 	DdNode *tmp, *tmp2;
-	
+
+	if (dd == NULL) return NULL;
+
 	tmp = Cudd_addBddThreshold(ddman, dd, threshold);
 	if (tmp == NULL) return NULL;
 	Cudd_Ref(tmp);
@@ -65,7 +67,9 @@ double threshold
 )
 {
 	DdNode *tmp, *tmp2;
-	
+
+	if (dd == NULL) return NULL;
+
 	tmp = Cudd_addBddStrictThreshold(ddman, dd, threshold);
 	if (tmp == NULL) return NULL;
 	Cudd_Ref(tmp);
@@ -111,6 +115,9 @@ double threshold
 )
 {
 	DdNode* res;
+
+	if (dd == NULL) return NULL;
+
 	res = DD_Threshold(ddman, dd, threshold);
 	if (res == NULL) return NULL;
 	return DD_Not(ddman, res);
@@ -126,6 +133,9 @@ double threshold
 )
 {
 	DdNode* res;
+
+	if (dd == NULL) return NULL;
+
 	res = DD_StrictThreshold(ddman, dd, threshold);
 	if (res == NULL) return NULL;
 	return DD_Not(ddman, res);
@@ -155,6 +165,8 @@ double upper
 {
 	DdNode *tmp, *tmp2;
 
+	if (dd == NULL) return NULL;
+
 	tmp = Cudd_addBddInterval(ddman, dd, lower, upper);
 	if (tmp == NULL) return NULL;
 	Cudd_Ref(tmp);
@@ -177,7 +189,9 @@ int places
 )
 {
 	DdNode *res;
-	
+
+	if (dd == NULL) return NULL;
+
 	res = Cudd_addRoundOff(ddman, dd, places);
 	if (res == NULL) return NULL;
 	Cudd_Ref(res);
@@ -262,7 +276,9 @@ int num_vars
 {
 	int i;
 	DdNode *ptr, *next_ptr, *filter, *res;
-	
+
+	if (dd == NULL) return NULL;
+
 	// construct filter to get first non-zero element
 	ptr = dd;
 	filter = DD_Constant(ddman, 1);
diff --git a/prism/src/dd/dd_vars.cc b/prism/src/dd/dd_vars.cc
index 60973945..738c2f65 100644
--- a/prism/src/dd/dd_vars.cc
+++ b/prism/src/dd/dd_vars.cc
@@ -45,7 +45,9 @@ int num_vars
 {
 	int i, *permut;
 	DdNode *res;
-		
+
+	if (dd == NULL) return NULL;
+
 	permut = new int[Cudd_ReadSize(ddman)];
 	for (i = 0; i < Cudd_ReadSize(ddman); i++) {
 		permut[i] = i;
@@ -79,7 +81,9 @@ int num_vars
 )
 {
 	DdNode *res;
-	
+
+	if (dd == NULL) return NULL;
+
 	res = Cudd_addSwapVariables(ddman, dd, old_vars, new_vars, num_vars);
 	if (res != NULL) Cudd_Ref(res);
 	Cudd_RecursiveDeref(ddman, dd);