mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

allow gcd when dio ignores some terms

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-04-09 10:23:55 -07:00
parent 7ee3415150
commit 7e88064da9
1 changed files with 1 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/int_solver.cpp
View file

@ -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);