diff --git a/src/storm/storage/prism/OverlappingGuardAnalyser.cpp b/src/storm/storage/prism/OverlappingGuardAnalyser.cpp index 2925bf3bc..7a5a94ab5 100644 --- a/src/storm/storage/prism/OverlappingGuardAnalyser.cpp +++ b/src/storm/storage/prism/OverlappingGuardAnalyser.cpp @@ -13,16 +13,7 @@ namespace storm { bool OverlappingGuardAnalyser::hasModuleWithInnerActionOverlap() { if(!initializedWithStateConstraints) { - for(auto const& integerVariable : program.getGlobalIntegerVariables()) { - smtSolver->add(integerVariable.getExpressionVariable().getExpression() >= integerVariable.getLowerBoundExpression()); - smtSolver->add(integerVariable.getExpressionVariable().getExpression() <= integerVariable.getUpperBoundExpression()); - } - for (auto const& module : program.getModules()) { - for(auto const& integerVariable : module.getIntegerVariables()) { - smtSolver->add(integerVariable.getExpressionVariable().getExpression() >= integerVariable.getLowerBoundExpression()); - smtSolver->add(integerVariable.getExpressionVariable().getExpression() <= integerVariable.getUpperBoundExpression()); - } - } + smtSolver->add(storm::expressions::conjunction((program.getAllRangeExpressions()))); } for(auto const& module : program.getModules()) { @@ -33,7 +24,7 @@ namespace storm { } else { for (uint64_t commandIndexA : commandIndices) { for (uint64_t commandIndexB : commandIndices) { - if (commandIndexA == commandIndexB) { + if (commandIndexA <= commandIndexB) { continue; } smtSolver->push();