global command indices may not be from 0 to N, so we have to check for highest command index explicitly

src/storm/storage/prism/Program.cpp

@@ -163,7 +163,8 @@ namespace storm {
                 }
             }
 
-            possiblySynchronizingCommands = storage::BitVector(this->getNumberOfCommands());
+            uint64_t highestGlobalIndex = this->getHighestCommandIndex();
+            possiblySynchronizingCommands = storage::BitVector(highestGlobalIndex + 1);
             std::set<uint64_t> possiblySynchronizingActionIndices;
             for(uint64_t syncAction : synchronizingActionIndices) {
                 if (getModuleIndicesByActionIndex(syncAction).size() > 1) {
@@ -173,7 +174,7 @@ namespace storm {
             for (auto const& module : getModules()) {
                 for (auto const& command : module.getCommands()) {
                     if (command.isLabeled()) {
-                        if (possiblySynchronizingActionIndices.count(command.getActionIndex())) {
+                        if (possiblySynchronizingActionIndices.count(command.getActionIndex()) > 0) {
                             possiblySynchronizingCommands.set(command.getGlobalIndex());
                         }
                     }
@@ -2100,6 +2101,16 @@ namespace storm {
             return std::make_pair(janiModel, newProperties);
         }
 
+        uint64_t Program::getHighestCommandIndex() const {
+            uint64_t highest = 0;
+            for (auto const& m : getModules()) {
+                for (auto const& c : m.getCommands()) {
+                    highest = std::max(highest, c.getGlobalIndex());
+                }
+            }
+            return highest;
+        }
+
         storm::expressions::ExpressionManager& Program::getManager() const {
             return *this->manager;
         }

src/storm/storage/prism/Program.h

@@ -765,6 +765,8 @@ namespace storm {
             // Creates the internal mappings.
             void createMappings();
 
+            uint64_t getHighestCommandIndex() const;
+
             // The type of the model.
             ModelType modelType;