diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 2453b3d87..1c66c0c53 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -108,7 +108,9 @@ namespace nlsat { } bool is_irreducible(poly* p) { - return true; + polynomial::factors factors(m_pm); + factor(polynomial_ref(p, m_pm), factors); + return factors.total_factors() == 1; } /*