#7003

minor tweaks to gomory and reset n3 within loop (but the entire function is dead code).
Z3Prover · Nov 19, 2023 · 35bc522 · 35bc522
1 parent 924c296
commit 35bc522
Show file tree

Hide file tree

Showing 3 changed files with 12 additions and 4 deletions.
diff --git a/src/api/dotnet/Constructor.cs b/src/api/dotnet/Constructor.cs
@@ -91,7 +91,13 @@ public FuncDecl[] AccessorDecls
         /// </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
@@ -338,14 +338,14 @@ class create_cut {
             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
@@ -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);