JDDNode.getThen() and getElse(): Protect against calls for a constant node, which is invalid.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10508 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/jdd/JDD.cc

@@ -807,7 +807,9 @@ JNIEXPORT jdouble JNICALL Java_jdd_JDDNode_DDN_1GetValue(JNIEnv *env, jclass cls
 
 JNIEXPORT jlong __jlongpointer JNICALL Java_jdd_JDDNode_DDN_1GetThen(JNIEnv *env, jclass cls, jlong __jlongpointer dd)
 {
-	return ptr_to_jlong(Cudd_T(jlong_to_DdNode(dd)));
+	DdNode *node = jlong_to_DdNode(dd);
+	if (Cudd_IsConstant(node)) return ptr_to_jlong(NULL);
+	return ptr_to_jlong(Cudd_T(node));
 }
 
 //------------------------------------------------------------------------------
@@ -815,7 +817,9 @@ JNIEXPORT jlong __jlongpointer JNICALL Java_jdd_JDDNode_DDN_1GetThen(JNIEnv *env
 
 JNIEXPORT jlong __jlongpointer JNICALL Java_jdd_JDDNode_DDN_1GetElse(JNIEnv *env, jclass cls, jlong __jlongpointer dd)
 {
-	return ptr_to_jlong(Cudd_E(jlong_to_DdNode(dd)));
+	DdNode *node = jlong_to_DdNode(dd);
+	if (Cudd_IsConstant(node)) return ptr_to_jlong(NULL);
+	return ptr_to_jlong(Cudd_E(node));
 }
 
 //==============================================================================

prism/src/jdd/JDDNode.java

@@ -91,6 +91,8 @@ public class JDDNode
 		assert !this.isConstant();
 
 		// just return the node, even if DebugJDD is enabled
+		// DDN_GetThen will return NULL if the current node is a
+		// constant, raising an Exception in the JDDNode constructor
 		return new JDDNode(DDN_GetThen(ptr));
 	}
 
@@ -106,7 +108,9 @@ public class JDDNode
 		assert !this.isConstant();
 
 		// just return the node, even if DebugJDD is enabled
-		return new JDDNode(DDN_GetElse(ptr));
+		// DDN_GetElse will return NULL if the current node is a
+		// constant, raising an Exception in the JDDNode constructor
+ 		return new JDDNode(DDN_GetElse(ptr));
 	}
 
 	public boolean equals(Object o)