fixed out-of-bounds access in symbolic to explicit conversion of game-based abstraction

src/storm/abstraction/MenuGameRefiner.cpp

@@ -672,6 +672,8 @@ namespace storm {
                     if (!interpolant.isTrue() && !interpolant.isFalse()) {
                         STORM_LOG_DEBUG("Derived new predicate (based on interpolation): " << interpolant);
                         interpolants.push_back(interpolant);
+                    } else {
+                        STORM_LOG_TRACE("Found interpolant is '" << interpolant << "'.");
                     }
                 }
                 return boost::make_optional(RefinementPredicates(RefinementPredicates::Source::Interpolation, interpolants));

src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp

@@ -680,7 +680,7 @@ namespace storm {
             std::vector<uint64_t> player2BackwardTransitions(transitionMatrix.getRowGroupCount());
 
             uint64_t player2State = 0;
-            for (uint64_t player1State = 0; player1State < player2RowGrouping.size() - 1; ++player1State) {
+            for (uint64_t player1State = 0; player1State < player1RowGrouping.size() - 1; ++player1State) {
                 while (player1RowGrouping[player1State + 1] > player2RowGrouping[player2State]) {
                     player2BackwardTransitions[player2State] = player1State;
                     ++player2State;