diff --git a/prism/src/parser/ast/ExpressionFunc.java b/prism/src/parser/ast/ExpressionFunc.java
index e34ae52d..848551cb 100644
--- a/prism/src/parser/ast/ExpressionFunc.java
+++ b/prism/src/parser/ast/ExpressionFunc.java
@@ -262,9 +262,12 @@ public class ExpressionFunc extends Expression
 	{
 		int i = getOperand(0).evaluateInt(ec);
 		int j = getOperand(1).evaluateInt(ec);
-		if (j == 0)
-			throw new PrismLangException("Attempt to compute modulo zero", this);
-		return new Integer(i % j);
+		// Non-positive divisor not allowed 
+		if (j <= 0)
+			throw new PrismLangException("Attempt to compute modulo with non-positive divisor", this);
+		// Take care of negative case (% is remainder, not modulo)
+		int rem = i % j;
+		return new Integer(rem < 0 ? rem + j : rem);
 	}
 
 	public Object evaluateLog(EvaluateContext ec) throws PrismLangException
diff --git a/prism/src/prism/StateModelChecker.java b/prism/src/prism/StateModelChecker.java
index 0a153e86..d53f2a0e 100644
--- a/prism/src/prism/StateModelChecker.java
+++ b/prism/src/prism/StateModelChecker.java
@@ -882,9 +882,11 @@ public class StateModelChecker implements ModelChecker
 				break;
 			case ExpressionFunc.MOD:
 				for (i = 0; i < n; i++) {
-					d = (int) dv2.getElement(i);
-					d = (d == 0) ? Double.NaN : (int) dv1.getElement(i) % (int) d;
-					dv1.setElement(i, d);
+					double div = (int) dv2.getElement(i);
+					// Non-positive divisor not allowed (flag as NaN)
+					d = (div <= 0) ? Double.NaN : (int) dv1.getElement(i) % (int) div;
+					// Take care of negative case (% is remainder, not modulo)
+					dv1.setElement(i, d < 0 ? d + div : d);
 				}
 				break;
 			case ExpressionFunc.LOG: