mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
more guards on cheap_eqs
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
parent
0ff18dd5a7
commit
4936ace7cd
|
@ -158,9 +158,12 @@ void lar_solver::substitute_basis_var_in_terms_for_row(unsigned i) {
|
|||
}
|
||||
|
||||
unsigned lar_solver::adjust_column_index_to_term_index(unsigned j) const {
|
||||
SASSERT(j < m_var_register.size());
|
||||
if (!tv::is_term(j)) {
|
||||
unsigned ext_var_or_term = m_var_register.local_to_external(j);
|
||||
j = !tv::is_term(ext_var_or_term) ? j : ext_var_or_term;
|
||||
} else {
|
||||
UNREACHABLE();
|
||||
}
|
||||
return j;
|
||||
}
|
||||
|
|
|
@ -214,8 +214,12 @@ public:
|
|||
display_row_of_vertex(v_j, tout);
|
||||
);
|
||||
lp::explanation exp = get_explanation_from_path(v_i, path, v_j);
|
||||
unsigned i_e = lp().adjust_column_index_to_term_index(get_column(m_vertices[v_i]));
|
||||
unsigned j_e = lp().adjust_column_index_to_term_index(get_column(m_vertices[v_j]));
|
||||
lpvar v_i_col = get_column(m_vertices[v_i]);
|
||||
lpvar v_j_col = get_column(m_vertices[v_j]);
|
||||
if (lp().column_is_int(v_i_col) != lp().column_is_int(v_j_col))
|
||||
return;
|
||||
unsigned i_e = lp().adjust_column_index_to_term_index(v_i_col);
|
||||
unsigned j_e = lp().adjust_column_index_to_term_index(v_j_col);
|
||||
m_imp.add_eq(i_e, j_e, exp);
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue