From d36cb8496a77c2601c2306de209bbfbcac109914 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 22 Oct 2010 08:08:10 +0000
Subject: [PATCH] Correct handling of mod (error on non-positive divisor,
 positive result for negative dividend).

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@2183 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 cudd/cudd/cuddAddApply.c | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/cudd/cudd/cuddAddApply.c b/cudd/cudd/cuddAddApply.c
index 9e8d1e01..55a7de45 100644
--- a/cudd/cudd/cuddAddApply.c
+++ b/cudd/cudd/cuddAddApply.c
@@ -1076,11 +1076,20 @@ Cudd_addMod(
 {
     DdNode *res;
     DdNode *F, *G;
+    int rem;
     CUDD_VALUE_TYPE value;
 
     F = *f; G = *g;
     if (cuddIsConstant(F) && cuddIsConstant(G)) {
-	value = (cuddV(G) != 0.0) ? ((int)cuddV(F) % (int)cuddV(G)) : (0.0/0.0); // x mod 0 is NaN
+	// If g is <=0, then result is NaN
+	if (cuddV(G) <= 0) value = (0.0/0.0);
+	// Take care of negative case (% is remainder, not modulo)
+	else {
+		rem = ((int)cuddV(F) % (int)cuddV(G));
+		if (rem < 0) rem += (int)cuddV(G);
+		value = rem;
+	}
+	// Create/return result
 	res = cuddUniqueConst(dd,value);
 	return(res);
     }