From a34ca5c9ac49f6d1af562da185824c340e98d77c Mon Sep 17 00:00:00 2001
From: Sebastian Junges <sebastian.junges@rwth-aachen.de>
Date: Tue, 7 Aug 2018 21:08:01 -0700
Subject: [PATCH] dont go on as soon as trivial command set is necessary

---
 .../counterexamples/SMTMinimalLabelSetGenerator.h             | 4 ++++
 1 file changed, 4 insertions(+)

diff --git a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
index dd0ce03e9..1152c3799 100644
--- a/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
+++ b/src/storm-counterexamples/counterexamples/SMTMinimalLabelSetGenerator.h
@@ -1776,6 +1776,10 @@ namespace storm {
                         break;
                     }
 
+                    if (commandSet.size() == nrCommands(symbolicModel)) {
+                        result.push_back(commandSet);
+                        break;
+                    }
 
                     auto subChoiceOrigins = restrictModelToLabelSet(model, commandSet, psiStates.getNextSetIndex(0));
                     std::shared_ptr<storm::models::sparse::Model<T>> const& subModel = subChoiceOrigins.first;