mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-06 07:16:13 +00:00
Code Activity

apply gcd test also before saturation

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-11-24 18:08:30 -08:00
parent b50286084e
commit 66141dfdfa
1 changed files with 8 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/math/lp/nla_grobner.cpp
View file

@ -76,6 +76,14 @@ namespace nla {
find_nl_cluster(); find_nl_cluster();
if (!configure()) if (!configure())
return; return;
try {
if (propagate_gcd_test())
return;
}
catch (...) {
}
m_solver.saturate(); m_solver.saturate();
TRACE(grobner, m_solver.display(tout)); TRACE(grobner, m_solver.display(tout));