From 66141dfdfa6080e4413da9b697a2954cdc3fa69c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 24 Nov 2025 18:08:30 -0800
Subject: [PATCH] apply gcd test also before saturation

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/math/lp/nla_grobner.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/math/lp/nla_grobner.cpp b/src/math/lp/nla_grobner.cpp
index f0db19649..cbb941882 100644
--- a/src/math/lp/nla_grobner.cpp
+++ b/src/math/lp/nla_grobner.cpp
@@ -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));