From 275e1b8655f24e132637d7f310b2be4b87c008a0 Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Mon, 20 Aug 2012 19:26:30 +0000
Subject: [PATCH] Bugfix: c-closure on empty zone breaks when max clock
 constraint constant is 0.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@5582 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/pta/DBM.java | 2 ++
 1 file changed, 2 insertions(+)

diff --git a/prism/src/pta/DBM.java b/prism/src/pta/DBM.java
index bf7381be..62eee2c8 100644
--- a/prism/src/pta/DBM.java
+++ b/prism/src/pta/DBM.java
@@ -219,6 +219,8 @@ public class DBM extends Zone
 	public void cClosure(int c)
 	{
 		int i, j, n;
+		if (isEmpty())
+			return;
 		n = pta.numClocks;
 		for (i = 0; i < n + 1; i++) {
 			for (j = 0; j < n + 1; j++) {