From 91d0cdf41db65be6afcb18044f156d72be864663 Mon Sep 17 00:00:00 2001
From: sjunges <sebastian.junges@gmail.com>
Date: Thu, 21 Dec 2017 00:36:57 +0100
Subject: [PATCH] fix non-terminating while loop in high level counterexamples

---
 src/storm/counterexamples/SMTMinimalLabelSetGenerator.h | 3 +++
 1 file changed, 3 insertions(+)

diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
index e8f2464a9..63f8b6ff8 100644
--- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
+++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
@@ -1709,6 +1709,9 @@ namespace storm {
                 
                 // Set up some variables for the iterations.
                 boost::container::flat_set<uint_fast64_t> commandSet(relevancyInformation.relevantLabels);
+                if (relevancyInformation.relevantLabels.empty()) {
+                    return commandSet;
+                }
                 bool done = false;
                 uint_fast64_t iterations = 0;
                 uint_fast64_t currentBound = 0;