From c7d4d7e11d5681c7a9cb5d2699bd90f314e78402 Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Fri, 12 Oct 2018 14:24:52 +0200
Subject: [PATCH] sparse.cc: split_mdp_rec, protect against malformed MTBDD

---
 prism/src/sparse/sparse.cc | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

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);