Update z3solver to handle unknown solution cases with error logging

ratioSolver · Jan 9, 2025 · 2d3bc38 · 2d3bc38
1 parent 52a6a97
commit 2d3bc38
Showing 1 changed file with 5 additions and 0 deletions.
diff --git a/src/z3/z3solver.cpp b/src/z3/z3solver.cpp
@@ -383,6 +383,11 @@ namespace ratio
                     if (!inconsistencies)
                         return true; // solution found..
                 }
+                else if (res == z3::unknown)
+                {
+                    LOG_ERR("Z3 solver failed to solve the problem: " << slv.reason_unknown());
+                    return false; // no solution..
+                }
                 else if (unexpanded_flaws.empty())
                     return false; // no solution..
                 else