From 35bc522dae99fbafd1862d4c60336e8a0cc29517 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 19 Nov 2023 09:59:44 -0800
Subject: [PATCH] #7003

minor tweaks to gomory and reset n3 within loop (but the entire function is dead code).
---
 src/api/dotnet/Constructor.cs      | 8 +++++++-
 src/math/lp/gomory.cpp             | 4 ++--
 src/math/polynomial/polynomial.cpp | 4 +++-
 3 files changed, 12 insertions(+), 4 deletions(-)

diff --git a/src/api/dotnet/Constructor.cs b/src/api/dotnet/Constructor.cs
index f635d78e4..323301bf9 100644
--- a/src/api/dotnet/Constructor.cs
+++ b/src/api/dotnet/Constructor.cs
@@ -91,7 +91,13 @@ namespace Microsoft.Z3
         /// </summary>
         ~Constructor()
         {
-            Native.Z3_del_constructor(Context.nCtx, NativeObject);
+	    if (Context.nCtx != IntPtr.Zero) {
+               lock (Context) 
+	       { 
+                   if (Context.nCtx != IntPtr.Zero) 
+                       Native.Z3_del_constructor(Context.nCtx, NativeObject);
+               }
+            }
         }        
 
         #region Internal
diff --git a/src/math/lp/gomory.cpp b/src/math/lp/gomory.cpp
index c3e8651d3..406b2a290 100644
--- a/src/math/lp/gomory.cpp
+++ b/src/math/lp/gomory.cpp
@@ -338,14 +338,14 @@ public:
             for (auto const& [c, v] : pol)
                 m_lcm_den = lcm(m_lcm_den, denominator(c));
             lp_assert(m_lcm_den.is_pos());
-            bool int_row = true;
+            bool int_row = all_of(pol, [&](auto const& kv) { return is_int(kv.second); });
             TRACE("gomory_cut_detail", tout << "pol.size() > 1 den: " << m_lcm_den << std::endl;);
+                
             if (!m_lcm_den.is_one()) {
                 // normalize coefficients of integer parameters to be integers.
                 for (auto & [c,v]: pol) {
                     c *= m_lcm_den;
                     SASSERT(!is_int(v) || c.is_int());
-                    int_row &= is_int(v);
                 }
                 m_k *= m_lcm_den;
             }
diff --git a/src/math/polynomial/polynomial.cpp b/src/math/polynomial/polynomial.cpp
index 6c94d9b72..c303a1541 100644
--- a/src/math/polynomial/polynomial.cpp
+++ b/src/math/polynomial/polynomial.cpp
@@ -5658,7 +5658,9 @@ namespace polynomial {
                     if (!is_zero(Gh3) && d1%2 == 0)
                         Gh3 = neg(Gh3);
                 }
-
+                else
+                    n3 = 0;
+                
                 // Compute hi
                 if (i > 1) {
                     g1 = lc(G1, x);