3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-04 02:56:44 +00:00

apply gcd test also before saturation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-11-24 18:08:30 -08:00
parent 01afda6378
commit 40d8d5ad9a

View file

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