From 6b7576c3e04993d620325057d7712a244bf95200 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 16 Jan 2026 10:50:26 -1000 Subject: [PATCH] Restrict noDisc optimization to section_lowest_degree only Match SMT-RAT behavior: noDisc (discriminant omission for leaves connected only to section polynomial) is only applied for sectionHeuristic == 3 (lowest_degree), not for biggest_cell or chain. Co-Authored-By: Claude Opus 4.5 --- src/nlsat/levelwise.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/nlsat/levelwise.cpp b/src/nlsat/levelwise.cpp index 33b8f0d5c..615138649 100644 --- a/src/nlsat/levelwise.cpp +++ b/src/nlsat/levelwise.cpp @@ -1120,7 +1120,9 @@ namespace nlsat { std_vector omit_lc; compute_omit_lc_section(level, level_ps, omit_lc); std_vector omit_disc; - compute_omit_disc_from_section_relation(level, level_ps, omit_disc); + // SMT-RAT only applies noDisc optimization for section_lowest_degree (heuristic 3) + if (m_section_relation_mode == section_lowest_degree) + compute_omit_disc_from_section_relation(level, level_ps, omit_disc); for (unsigned i = 0; i < level_ps.size(); ++i) { polynomial_ref p(level_ps.get(i), m_pm);