From d289495ca41463ac804fe3dc763dde79ecad52b9 Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Wed, 9 Apr 2025 10:23:55 -0700
Subject: [PATCH] allow gcd when dio ignores some terms

Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
---
 src/math/lp/int_solver.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/math/lp/int_solver.cpp b/src/math/lp/int_solver.cpp
index fc6e9c3e7..960287ab4 100644
--- a/src/math/lp/int_solver.cpp
+++ b/src/math/lp/int_solver.cpp
@@ -223,7 +223,7 @@ namespace lp {
         
             lia_move r = lia_move::undef;
 
-            if (m_gcd.should_apply())
+            if (m_gcd.should_apply() || (settings().dio() && m_dio.some_terms_are_ignored()))
                 r = m_gcd();
 
             check_return_helper pc(lra);