diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionRepresentation.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionRepresentation.java index 631afef262..366a946cb3 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionRepresentation.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionRepresentation.java @@ -147,6 +147,9 @@ public RecursiveIntObjCursor cursor(RecursiveIntObjMapView MddNode mddNode = mddNodeConstraint.get(mddNodeConstraint.statistics().lowestValue()); while (true) { + // This is needed because the constraint node might contain level-skips: of the domain is bounded, then default values are detected + if(mddNode.isTerminal()) break; + final IntStatistics statistics = mddNode.statistics(); final Decl decl = variable.getTraceInfo(Decl.class); final LitExpr lowerBound = LitExprConverter.toLitExpr(statistics.lowestValue(), decl.getType()); @@ -466,7 +469,8 @@ private static int generateMissingLiteral(MddExpressionRepresentation representa final IntSetView remaining = domain.minus(representation.explicitRepresentation.getCacheView().keySet()); if (remaining.isEmpty()) { representation.explicitRepresentation.setComplete(); - throw new UnsupportedOperationException("Not yet implemented"); + // Return the first element + newValue = representation.explicitRepresentation.getCacheView().keySet().statistics().lowestValue(); } else { final var cur = remaining.cursor(); Preconditions.checkState(cur.moveNext());