From ae470851f41b08a810e3a991c9a6f8d785924277 Mon Sep 17 00:00:00 2001
From: TimQu <tim.quatmann@cs.rwth-aachen.de>
Date: Thu, 29 Jun 2017 13:59:43 +0200
Subject: [PATCH] Do not segfault when a property could not be verified

---
 src/storm/cli/cli.cpp | 12 +++++++++---
 1 file changed, 9 insertions(+), 3 deletions(-)

diff --git a/src/storm/cli/cli.cpp b/src/storm/cli/cli.cpp
index b28f068c3..6d938735c 100644
--- a/src/storm/cli/cli.cpp
+++ b/src/storm/cli/cli.cpp
@@ -655,7 +655,9 @@ namespace storm {
             verifyProperties<ValueType>(input.properties,
                                         [&sparseModel] (std::shared_ptr<storm::logic::Formula const> const& formula) {
                                             std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(sparseModel, storm::api::createTask<ValueType>(formula, true));
-                                            result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(sparseModel->getInitialStates()));
+                                            if (result) {
+                                                result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(sparseModel->getInitialStates()));
+                                            }
                                             return result;
                                         });
         }
@@ -665,7 +667,9 @@ namespace storm {
             verifyProperties<ValueType>(input.properties, [&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
                 auto symbolicModel = model->as<storm::models::symbolic::Model<DdType, ValueType>>();
                 std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithHybridEngine<DdType, ValueType>(symbolicModel, storm::api::createTask<ValueType>(formula, true));
-                result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()));
+                if (result) {
+                    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()));
+                }
                 return result;
             });
         }
@@ -675,7 +679,9 @@ namespace storm {
             verifyProperties<ValueType>(input.properties, [&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
                 auto symbolicModel = model->as<storm::models::symbolic::Model<DdType, ValueType>>();
                 std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithDdEngine<DdType, ValueType>(model->as<storm::models::symbolic::Model<DdType, ValueType>>(), storm::api::createTask<ValueType>(formula, true));
-                result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()));
+                if (result) {
+                    result->filter(storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(symbolicModel->getReachableStates(), symbolicModel->getInitialStates()));
+                }
                 return result;
             });
         }