mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

no big nums in patching (#4705)

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2020-09-23 08:46:41 -07:00 committed by GitHub
parent 1e6d2fbbdc
commit 1e7998f03a
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
1 changed files with 3 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -89,6 +89,9 @@ void int_solver::patcher::patch_nbasic_column(unsigned j) {
if (inf_u) tout << "oo"; else tout << u;
tout << "]";
tout << ", m: " << m << ", val: " << val << ", is_int: " << lra.column_is_int(j) << "\n";);
if (m.is_big() || (!inf_l && l.x.is_big()) || (!inf_u && u.x.is_big())) {
return;
}
if (!inf_l) {
l = impq(m_is_one ? ceil(l) : m * ceil(l / m));
if (inf_u || l <= u) {