sparse.cc: split_mdp_rec, protect against malformed MTBDD

7 years ago · c7d4d7e11d
1 changed files with 3 additions and 1 deletions
--- a/prism/src/sparse/sparse.cc
+++ b/prism/src/sparse/sparse.cc
@ -946,9 +946,11 @@ void split_mdp_rec(DdManager *ddman, DdNode *dd, DdNode **ndvars, int num_ndvars
 	if (dd->index > ndvars[level]->index) {
 		e = t = dd;
 	}
-	else {
+	else if (dd->index == ndvars[level]->index) {
 		e = Cudd_E(dd);
 		t = Cudd_T(dd);
+	} else {
+		throw std::logic_error("Unexpected variable or ordering in MTBDD");
 	}
 	
 	split_mdp_rec(ddman, e, ndvars, num_ndvars, level+1, matrices);