diff --git a/prism/src/sparse/sparse.cc b/prism/src/sparse/sparse.cc index 48fee5ff..9e608ef1 100644 --- 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);