From 55b64e1f29880ee230cba493cab1971303152c88 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 1 Nov 2024 13:57:56 -0700
Subject: [PATCH] use glue as computed without adjustment

---
 src/sat/smt/bv_ackerman.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/sat/smt/bv_ackerman.cpp b/src/sat/smt/bv_ackerman.cpp
index 940b1ebb0..a709c16f3 100644
--- a/src/sat/smt/bv_ackerman.cpp
+++ b/src/sat/smt/bv_ackerman.cpp
@@ -118,8 +118,8 @@ namespace bv {
             }
         }
         
-        if (glue < max_glue) 
-            v.m_glue = (sz > 6 && 2*glue <= sz) ? 0 : glue;
+        if (glue < max_glue)
+            v.m_glue = glue; // (sz > 6 && 2 * glue <= sz) ? 0 : glue;
     }
 
     void ackerman::remove(vv* p) {