From 7d6b899ef47a8daf428fea73e5fc86e836f7f80b 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: Fix divide by infinity.

Would throw an exception before, now we return NaN as for BigRational and other engines.
---
 prism/src/param/JasFunction.java | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/prism/src/param/JasFunction.java b/prism/src/param/JasFunction.java
index 3f2f1f18..4bdf5f2e 100644
--- a/prism/src/param/JasFunction.java
+++ b/prism/src/param/JasFunction.java
@@ -182,6 +182,9 @@ final class JasFunction extends Function {
 		if (this.isNaN() || other.isNaN()) {
 			return factory.getNaN();
 		}
+		if (other.isInf() || other.isMInf()) {
+			return factory.getNaN();
+		}
 		if (other.isZero()) {
 			if (this.isConstant()) {
 				// evaluate constant to return either NaN, Inf or -Inf, using BigRational division