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 366a946cb3..7caa2b98fe 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
@@ -115,7 +115,20 @@ public MddNode get(int key) {
         } else {
             final Expr<BoolType> canonizedExpr = ExprUtils.canonize(ExprUtils.simplify(simplifiedExpr));
             MddGraph<Expr> mddGraph = (MddGraph<Expr>) mddVariable.getMddGraph();
-            childNode = canonizedExpr instanceof FalseExpr ? mddGraph.getTerminalZeroNode() : mddGraph.getNodeFor(canonizedExpr);
+
+            if (canonizedExpr instanceof FalseExpr) {
+                childNode = mddGraph.getTerminalZeroNode();
+            } else {
+                var solver = solverPool.requestSolver();
+                try (var wpp = new WithPushPop(solver)) {
+                    solver.add(canonizedExpr);
+                    if (solver.check().isSat()) {
+                        childNode = mddGraph.getNodeFor(canonizedExpr);
+                    } else {
+                        childNode = mddGraph.getTerminalZeroNode();
+                    }
+                }
+            }
         }
 
         if (!childNode.equals(mddVariable.getMddGraph().getTerminalZeroNode()))