Browse Source

fixed not respecting negative assignment indices in array eliminator

main
TimQu 7 years ago
parent
commit
10ae6a0dd8
  1. 4
      src/storm/storage/jani/ArrayEliminator.cpp

4
src/storm/storage/jani/ArrayEliminator.cpp

@ -468,7 +468,7 @@ namespace storm {
// Replace array occurrences in LValues and assigned expressions. // Replace array occurrences in LValues and assigned expressions.
std::vector<Assignment> newAssignments; std::vector<Assignment> newAssignments;
uint64_t level = 0; int64_t level = orderedAssignments.getLowestLevel();
std::unordered_map<storm::expressions::Variable, std::vector<Assignment const*>> collectedArrayAccessAssignments; std::unordered_map<storm::expressions::Variable, std::vector<Assignment const*>> collectedArrayAccessAssignments;
for (Assignment const& assignment : orderedAssignments) { for (Assignment const& assignment : orderedAssignments) {
if (assignment.getLevel() != level) { if (assignment.getLevel() != level) {
@ -563,7 +563,7 @@ namespace storm {
return nullptr; return nullptr;
} }
void insertLValueArrayAccessReplacements(std::vector<Assignment const*> const& arrayAccesses, std::vector<storm::jani::Variable const*> const& arrayVariableReplacements, uint64_t level, std::vector<Assignment>& newAssignments) const { void insertLValueArrayAccessReplacements(std::vector<Assignment const*> const& arrayAccesses, std::vector<storm::jani::Variable const*> const& arrayVariableReplacements, int64_t level, std::vector<Assignment>& newAssignments) const {
storm::expressions::Variable const& arrayVariable = arrayAccesses.front()->getLValue().getArray().getExpressionVariable(); storm::expressions::Variable const& arrayVariable = arrayAccesses.front()->getLValue().getArray().getExpressionVariable();
bool onlyConstantIndices = true; bool onlyConstantIndices = true;
for (auto const& aa : arrayAccesses) { for (auto const& aa : arrayAccesses) {

|||||||
100:0
Loading…
Cancel
Save