From 7e88064da96d8fb914a7be50776e5e9ed363bad2 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 fe081fa6e..e3574d5de 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);