Fixed a bug that could result in unsat terminal nodes

ftsrg · Feb 21, 2024 · ef9dfaa · ef9dfaa
1 parent 8548ad0
commit ef9dfaa
Showing 1 changed file with 14 additions and 1 deletion.
diff --git a/...heta/analysis/algorithm/symbolic/symbolicnode/expression/MddExpressionRepresentation.java b/...heta/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()))