From 2e3f937a25e383dbd72a82a56c54f317e8a2814f Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Mon, 18 Sep 2017 14:43:54 +0200
Subject: [PATCH] StateValuesMTBDD.maxFiniteOverBDD: Fix CUDD leak in error
 case

If there are no finite values, the BDD node was not cleared.
---
 prism/src/prism/StateValuesMTBDD.java | 5 ++++-
 1 file changed, 4 insertions(+), 1 deletion(-)

diff --git a/prism/src/prism/StateValuesMTBDD.java b/prism/src/prism/StateValuesMTBDD.java
index 4c99e39d..b02686c9 100644
--- a/prism/src/prism/StateValuesMTBDD.java
+++ b/prism/src/prism/StateValuesMTBDD.java
@@ -425,7 +425,10 @@ public class StateValuesMTBDD implements StateValues
 		tmp = JDD.And(filter, reach);
 
 		// max of an empty set is -infinity
-		if (tmp.equals(JDD.ZERO)) return Double.NEGATIVE_INFINITY;
+		if (tmp.equals(JDD.ZERO)) {
+			JDD.Deref(tmp);
+			return Double.NEGATIVE_INFINITY;
+		}
 
 		// set non-reach states to infinity
 		JDD.Ref(values);