From 779b8ed5687be0661e9008b126858d23ee199b7d Mon Sep 17 00:00:00 2001
From: Joachim Klein <joachim.klein@automata.tools>
Date: Sun, 5 Apr 2020 22:20:07 +0200
Subject: [PATCH] param: For constant division by zero, use BigRational
 division

---
 prism/src/param/JasFunction.java | 7 +++++--
 1 file changed, 5 insertions(+), 2 deletions(-)

diff --git a/prism/src/param/JasFunction.java b/prism/src/param/JasFunction.java
index d6eb4358..3f2f1f18 100644
--- a/prism/src/param/JasFunction.java
+++ b/prism/src/param/JasFunction.java
@@ -183,9 +183,12 @@ final class JasFunction extends Function {
 			return factory.getNaN();
 		}
 		if (other.isZero()) {
-			if (this.isZero()) {
-				return factory.getNaN();
+			if (this.isConstant()) {
+				// evaluate constant to return either NaN, Inf or -Inf, using BigRational division
+				return factory.fromBigRational(this.asBigRational().divide(BigRational.ZERO));
 			} else {
+				// non-constant
+				// TODO: Fix, should be 'this / 0', but that can't be represented by JAS...
 				return factory.getInf();
 			}
 		}