diff --git a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionTemplate.java b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionTemplate.java index 14adc106e8..200ae2adde 100644 --- a/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionTemplate.java +++ b/subprojects/common/analysis/src/main/java/hu/bme/mit/theta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionTemplate.java @@ -68,16 +68,16 @@ public RecursiveIntObjMapView toCanonicalRepresentation(MddVa } // Check if default -// if (!ExprUtils.getConstants(canonizedExpr).contains(decl)) { -// final MddNode childNode; -// if (mddVariable.getLower().isPresent()) { -// childNode = mddVariable.getLower().get().checkInNode(new MddExpressionTemplate(canonizedExpr, o -> (Decl) o, solverPool)); -// } else { -// final MddGraph mddGraph = (MddGraph) mddVariable.getMddGraph(); -// childNode = mddGraph.getNodeFor(canonizedExpr); -// } -// return MddExpressionRepresentation.ofDefault(canonizedExpr, decl, mddVariable, solverPool, childNode); -// } + if (mddVariable.getDomainSize() == 0 && !ExprUtils.getConstants(canonizedExpr).contains(decl)) { + final MddNode childNode; + if (mddVariable.getLower().isPresent()) { + childNode = mddVariable.getLower().get().checkInNode(new MddExpressionTemplate(canonizedExpr, o -> (Decl) o, solverPool)); + } else { + final MddGraph mddGraph = (MddGraph) mddVariable.getMddGraph(); + childNode = mddGraph.getNodeFor(canonizedExpr); + } + return MddExpressionRepresentation.ofDefault(canonizedExpr, decl, mddVariable, solverPool, childNode); + } return MddExpressionRepresentation.of(canonizedExpr, decl, mddVariable, solverPool);