From ceea5198d63c3af8fc7bf2f461339904423d83bc Mon Sep 17 00:00:00 2001
From: dehnert <dehnert@cs.rwth-aachen.de>
Date: Tue, 15 May 2018 15:07:02 +0200
Subject: [PATCH] fixed detection of unreachability of target state in
 MaxSAT-based high-level counterexample generation

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

diff --git a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
index 1ede56684..f66205fbf 100644
--- a/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
+++ b/src/storm/counterexamples/SMTMinimalLabelSetGenerator.h
@@ -1785,7 +1785,10 @@ namespace storm {
                         }
                         
                         if (options.useDynamicConstraints) {
-                            if (maximalReachabilityProbability == storm::utility::zero<T>()) {
+                            // Determine which of the two analysis techniques to call by performing a reachability analysis.
+                            storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(subModel->getTransitionMatrix(), subModel->getInitialStates(), phiStates, psiStates);
+                            
+                            if (reachableStates.isDisjointFrom(psiStates)) {
                                 // If there was no target state reachable, analyze the solution and guide the solver into the right direction.
                                 analyzeZeroProbabilitySolution(*solver, *subModel, subLabelSets, model, labelSets, phiStates, psiStates, commandSet, variableInformation, relevancyInformation);
                             } else {