diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h
index c942396cb..94f550141 100644
--- a/src/counterexamples/SMTMinimalCommandSetGenerator.h
+++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h
@@ -1818,6 +1818,7 @@ namespace storm {
                         psiStates = eventuallyFormula.getChild().check(modelchecker);
                     } catch (std::bad_cast const&) {
                         // If the nested formula is neither an until nor a finally formula, we throw an exception.
+						LOG4CPLUS_ERROR(logger, "Formula nested inside probability bound operator must be an until or eventually formula for counterexample generation.");
                         throw storm::exceptions::InvalidPropertyException() << "Formula nested inside probability bound operator must be an until or eventually formula for counterexample generation.";
                     }
                 }
diff --git a/src/storm.cpp b/src/storm.cpp
index 8e3ade79e..6357b11a1 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -46,6 +46,7 @@
 #include "src/utility/ErrorHandling.h"
 #include "src/formula/Prctl.h"
 #include "src/utility/vector.h"
+#include "src/utility/OsDetection.h"
 
 #include "src/settings/Settings.h"
 // Registers all standard options