From c99655eda974aaf553cbc567f576baf072a2a56d Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Sat, 6 Dec 2014 23:48:45 +0000
Subject: [PATCH] Catch some divide-by-zero errors in JasFunction.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@9385 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/param/JasFunction.java | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/prism/src/param/JasFunction.java b/prism/src/param/JasFunction.java
index b59f933f..2b06b567 100644
--- a/prism/src/param/JasFunction.java
+++ b/prism/src/param/JasFunction.java
@@ -182,6 +182,16 @@ final class JasFunction extends Function {
 		if (this.isNaN() || other.isNaN()) {
 			return factory.getNaN();
 		}
+		if (other.isZero()) {
+			if (this.isZero()) {
+				return factory.getNaN();
+			} else {
+				return factory.getInf();
+			}
+		}
+		if (this.isZero()) {
+			return factory.getZero();
+		}
 		return new JasFunction((JasFunctionFactory) factory, jas.divide(((JasFunction) other).jas), NORMAL);
 	}