Merge branch 'future' into next_state_generators

Former-commit-id: 93bfabf944

resources/3rdparty/CMakeLists.txt

@@ -71,6 +71,7 @@ ExternalProject_Get_Property(sylvan binary_dir)
 set(Sylvan_INCLUDE_DIR "${STORM_SYLVAN_ROOT}/src" PARENT_SCOPE)
 set(Sylvan_LIBRARY "${binary_dir}/src/libsylvan.a" PARENT_SCOPE)
 
+add_dependencies(resources sylvan)
 
 ExternalProject_Add(
         googletest

src/storage/BitVector.cpp

@@ -406,6 +406,7 @@ namespace storm {
         }
 
         uint_fast64_t BitVector::getAsInt(uint_fast64_t bitIndex, uint_fast64_t numberOfBits) const {
+            STORM_LOG_ASSERT(numberOfBits <= 64, "Number of bits must be <= 64.");
             uint64_t bucket = bitIndex >> 6;
             uint64_t bitIndexInBucket = bitIndex & mod64mask;
 
@@ -445,7 +446,8 @@ namespace storm {
         }
 
         void BitVector::setFromInt(uint_fast64_t bitIndex, uint_fast64_t numberOfBits, uint64_t value) {
-            STORM_LOG_ASSERT((value >> numberOfBits) == 0, "Integer value too large to fit in the given number of bits.");
+            STORM_LOG_ASSERT(numberOfBits <= 64, "Number of bits must be <= 64.");
+            STORM_LOG_ASSERT(numberOfBits == 64 || (value >> numberOfBits) == 0, "Integer value too large to fit in the given number of bits.");
 
             uint64_t bucket = bitIndex >> 6;
             uint64_t bitIndexInBucket = bitIndex & mod64mask;

src/utility/storm.h

@@ -307,7 +307,7 @@ namespace storm {
         // TODO: add checks.
         filestream << "!Parameters: ";
         std::set<storm::Variable> vars = result.gatherVariables();
-        std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::Variable>(filestream, ", "));
+        std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::Variable>(filestream, "; "));
         filestream << std::endl;
         filestream << "!Result: " << result << std::endl;
         filestream << "!Well-formed Constraints: " << std::endl;