mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-25 13:47:01 +00:00
Code Activity

cosmetics

Browse source 
Signed-off-by: Lev Nachmanson <levnach@hotmail.com>
This commit is contained in:
Lev Nachmanson 2025-03-07 12:57:30 -10:00
parent 4068720d06
commit 76b82318b8
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -2551,14 +2551,14 @@ namespace lp {
return print_lar_term_L(opened_ml, out); return print_lar_term_L(opened_ml, out);
} }
// collect only fixed variables // collect only fixed variables in a term
template <typename T> template <typename T>
term_with_index open_fixed_from_ml(const T& ml) const { term_with_index open_fixed_from_ml(const T& ml) const {
term_with_index r; term_with_index r;
for (const auto& v : ml) { for (const auto& v : ml) {
for (const auto & p : lra.get_term(v.var()).ext_coeffs()) { for (const auto & p : lra.get_term(v.var()).ext_coeffs()) {
if (lra.column_is_fixed(p.var())) if (lra.column_is_fixed(p.var()))
r.add(v.coeff()*p.coeff(), p.var()); r.add(v.coeff() * p.coeff(), p.var());
} }
} }
return r; return r;