mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

reject more terms with big numbers

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-04-07 11:49:39 -07:00 • committed by Lev Nachmanson
parent 1cde40bddb
commit cb1818f4b8
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/math/lp/dioph_eq.cpp
View file

@ -1065,9 +1065,11 @@ namespace lp {
void process_changed_columns(std_vector<unsigned> &f_vector) { void process_changed_columns(std_vector<unsigned> &f_vector) {
find_changed_terms_and_more_changed_rows(); find_changed_terms_and_more_changed_rows();
for (unsigned j: m_changed_terms) { for (unsigned j: m_changed_terms) {
if (j >= lra.column_count()) if (j >= lra.column_count() ||
!lra.column_has_term(j) ||
(ignore_big_nums() && term_has_big_number(lra.get_term(j)))
)
continue; continue;
SASSERT(!ignore_big_nums() || !term_has_big_number(lra.get_term(j)));
m_terms_to_tighten.insert(j); m_terms_to_tighten.insert(j);
if (j < m_l_matrix.column_count()) { if (j < m_l_matrix.column_count()) {
for (const auto& cs : m_l_matrix.column(j)) { for (const auto& cs : m_l_matrix.column(j)) {