From 5245d77bfc700f8adf73205686ad9fd128932243 Mon Sep 17 00:00:00 2001
From: Tim Quatmann <tim.quatmann@cs.rwth-aachen.de>
Date: Mon, 14 Dec 2020 11:56:21 +0100
Subject: [PATCH] SteadyState: Issue a warning in sound mode because it is not
 supported.

---
 .../infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp | 1 +
 1 file changed, 1 insertion(+)

diff --git a/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp b/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp
index 96c642116..a987b2c47 100644
--- a/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp
+++ b/src/storm/modelchecker/helper/infinitehorizon/SparseDeterministicInfiniteHorizonHelper.cpp
@@ -235,6 +235,7 @@ namespace storm {
                     subEnv.solver().setLinearEquationSolverType(subEnv.solver().topological().getUnderlyingEquationSolverType(), subEnv.solver().topological().isUnderlyingEquationSolverTypeSetFromDefault());
                 }
                 subEnv.solver().setLinearEquationSolverPrecision(env.solver().lra().getPrecision(), env.solver().lra().getRelativeTerminationCriterion());
+                STORM_LOG_WARN_COND(!subEnv.solver().isForceSoundness(), "Sound computations are not properly implemented for this computation. You might get incorrect results.");
                 
                 // Get a mapping from global state indices to local ones as well as a bitvector containing states within the BSCC.
                 std::unordered_map<uint64_t, uint64_t> toLocalIndexMap;