From 75197e3d22c68a7a903a22e9a46ce57ee04517b1 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 13 Nov 2015 12:51:13 +0000
Subject: [PATCH] Handle NaN better as a constant. [from Joachim Klein]

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@10877 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 cudd/cudd/cuddTable.c | 20 +++++++++++---------
 1 file changed, 11 insertions(+), 9 deletions(-)

diff --git a/cudd/cudd/cuddTable.c b/cudd/cudd/cuddTable.c
index 6afe70c6..9737288f 100644
--- a/cudd/cudd/cuddTable.c
+++ b/cudd/cudd/cuddTable.c
@@ -1576,17 +1576,19 @@ cuddUniqueConst(
      * infinite, since Infinity - Infinity is NaN and NaN < X is 0 for
      * every X.
      */
+    // PRISM: check explicitly for not-a-number (NaN), as NaN != NaN
     while (looking != NULL) {
-	if (looking->type.value == value ||
-	ddEqualVal(looking->type.value,value,unique->epsilon)) {
-	    if (looking->ref == 0) {
-		cuddReclaim(unique,looking);
-	    }
-	    return(looking);
-	}
-	looking = looking->next;
+        if (looking->type.value == value ||
+            (isnan(value) && isnan(looking->type.value)) ||
+            ddEqualVal(looking->type.value,value,unique->epsilon)) {
+            if (looking->ref == 0) {
+                cuddReclaim(unique,looking);
+            }
+            return(looking);
+        }
+        looking = looking->next;
 #ifdef DD_UNIQUE_PROFILE
-	unique->uniqueLinks++;
+        unique->uniqueLinks++;
 #endif
     }