From b09aa06712500c3d2c2623d7b06170a9aef6026a Mon Sep 17 00:00:00 2001
From: Joachim Klein <klein@tcs.inf.tu-dresden.de>
Date: Mon, 28 Aug 2017 12:45:48 +0200
Subject: [PATCH] param.ConstraintChecker: If the constraint is constant, we
 can be sure about satisfaction

---
 prism/src/param/ConstraintChecker.java | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/prism/src/param/ConstraintChecker.java b/prism/src/param/ConstraintChecker.java
index 00902ee4..8adb24f6 100644
--- a/prism/src/param/ConstraintChecker.java
+++ b/prism/src/param/ConstraintChecker.java
@@ -166,6 +166,20 @@ class ConstraintChecker {
 	 */
 	boolean check(Region region, Function constraint, boolean strict)
 	{
+		// handle case where the constraint is a constant number
+		if (constraint.isConstant()) {
+			BigRational value = constraint.asBigRational();
+
+			if (value.isNaN())
+				return false;
+
+			if (strict) {
+				return value.signum() == 1;
+			} else {
+				return value.signum() >= 0;
+			}
+		}
+
 		Function constr = constraint.toConstraint();
 		DecisionEntryKey key = new DecisionEntryKey();
 		key.constraint = constr;