Merge remote-tracking branch 'upstream/master'

resources/3rdparty/CMakeLists.txt

@@ -155,6 +155,8 @@ if(Z3_FOUND)
 
     add_imported_library(z3 SHARED ${Z3_LIBRARIES} ${Z3_INCLUDE_DIRS})
     list(APPEND STORM_DEP_TARGETS z3_SHARED)
+else()
+    message (WARNING "Storm - Z3 not found. Building of Prism/JANI models will not be supported.")
 endif(Z3_FOUND)
 
 #############################################################
@@ -223,7 +225,7 @@ if(USE_CARL)
 		message("START CARL CONFIG PROCESS")
 		file(MAKE_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download) 
 		execute_process(
-		COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}" "-DUSE_CLN_NUMBERS=ON" "-DUSE_GINAC=ON" "-DBoost_LIBRARY_DIRS=${Boost_LIBRARY_DIRS}" "-DBoost_INCLUDE_DIRS=${Boost_INCLUDE_DIRS}" "-DTHREAD_SAFE=ON"
+		COMMAND ${CMAKE_COMMAND} ${STORM_3RDPARTY_SOURCE_DIR}/carl "-DSTORM_3RDPARTY_BINARY_DIR=${STORM_3RDPARTY_BINARY_DIR}"
 		WORKING_DIRECTORY ${STORM_3RDPARTY_BINARY_DIR}/carl_download
 		OUTPUT_VARIABLE carlconfig_out
 		RESULT_VARIABLE carlconfig_result)

resources/3rdparty/carl/CMakeLists.txt

@@ -12,7 +12,7 @@ ExternalProject_Add(carl-config
 	PREFIX here
 	SOURCE_DIR source_dir
 	BINARY_DIR ${STORM_3RDPARTY_BINARY_DIR}/carl
-	CMAKE_ARGS -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DBOOST_INCLUDEDIR=${Boost_INCLUDE_DIRS} -DBOOST_LIBRARYDIR=${Boost_LIBRARY_DIRS} -DBoost_NO_SYSTEM_PATHS=1 -DEXPORT_TO_CMAKE=0 -DUSE_CLN_NUMBERS=1 -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=1 -DCMAKE_INSTALL_PREFIX:PATH=${STORM_3RDPARTY_BINARY_DIR}/carl 
+	CMAKE_ARGS -DCMAKE_CXX_COMPILER=${CMAKE_CXX_COMPILER} -DBOOST_INCLUDEDIR=${Boost_INCLUDE_DIRS} -DBOOST_LIBRARYDIR=${Boost_LIBRARY_DIRS} -DBoost_NO_SYSTEM_PATHS=1 -DEXPORT_TO_CMAKE=0 -DUSE_CLN_NUMBERS=1 -DUSE_GINAC=ON -DTHREAD_SAFE=ON -DCMAKE_SKIP_INSTALL_ALL_DEPENDENCY=1 -DCMAKE_INSTALL_PREFIX:PATH=${STORM_3RDPARTY_BINARY_DIR}/carl
         BUILD_IN_SOURCE 0
         LOG_UPDATE OFF
         LOG_CONFIGURE OFF

src/storm/logic/BoundedUntilFormula.cpp

@@ -105,7 +105,7 @@ namespace storm {
         template <>
         double BoundedUntilFormula::getNonStrictUpperBound() const {
             double bound = getUpperBound<double>();
-            STORM_LOG_THROW(bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound.");
+            STORM_LOG_THROW(!isUpperBoundStrict() || bound > 0, storm::exceptions::InvalidPropertyException, "Cannot retrieve non-strict bound from strict zero-bound.");
             return bound;
         }