mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

cosmetics

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2024-12-16 12:36:52 -10:00 committed by Lev Nachmanson
parent deac00ada3
commit 8d747865ae
1 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -301,7 +301,6 @@ namespace lp {
} }
// the term has form sum(a_i*x_i) - t.j() = 0, // the term has form sum(a_i*x_i) - t.j() = 0,
// i is the index of the term in the lra.m_terms
void fill_entry(const lar_term& t) { void fill_entry(const lar_term& t) {
TRACE("dioph_eq", print_lar_term_L(t, tout) << std::endl;); TRACE("dioph_eq", print_lar_term_L(t, tout) << std::endl;);
entry te = {lar_term(t.j()), mpq(0), entry_status::F}; entry te = {lar_term(t.j()), mpq(0), entry_status::F};
@ -323,9 +322,9 @@ namespace lp {
m_e_matrix.add_new_element(entry_index, lj, p.coeff()); m_e_matrix.add_new_element(entry_index, lj, p.coeff());
} }
} }
if (is_fixed(t.j())) if (is_fixed(t.j())) {
e.m_c -= lia.lower_bound(t.j()).x; e.m_c -= lia.lower_bound(t.j()).x;
else { } else {
unsigned lj = add_var(t.j()); unsigned lj = add_var(t.j());
while (lj >= m_e_matrix.column_count()) while (lj >= m_e_matrix.column_count())
m_e_matrix.add_column(); m_e_matrix.add_column();