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

fix the build

Browse source
This commit is contained in:
Lev Nachmanson 2024-10-21 14:21:02 -07:00 committed by Lev Nachmanson
parent 5f5f1d4fd1
commit 8904a50103
2 changed files with 2 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -219,7 +219,6 @@ namespace lp {
void init() { void init() {
m_e_matrix = static_matrix<mpq, mpq>(lra.row_count(), lra.column_count()); m_e_matrix = static_matrix<mpq, mpq>(lra.row_count(), lra.column_count());
m_report_branch = false; m_report_branch = false;
unsigned n_of_rows = lra.A_r().row_count();
m_k2s.clear(); m_k2s.clear();
m_k2s.resize(lra.column_count(), -1); m_k2s.resize(lra.column_count(), -1);
m_conflict_index = -1; m_conflict_index = -1;
@ -230,7 +229,7 @@ namespace lp {
for (unsigned i = 0; i < lra.terms().size(); i++) { for (unsigned i = 0; i < lra.terms().size(); i++) {
const lar_term* t = lra.terms()[i]; const lar_term* t = lra.terms()[i];
TRACE("dioph_eq", tout << "term "<< i <<":"; lra.print_term(*t, tout) << "\n"; TRACE("dioph_eq", tout << "term "<< i <<":"; lra.print_term(*t, tout) << "\n";
for(auto & p: *t) { for(const auto & p: *t) {
lra.print_column_info(p.var(), tout); lra.print_column_info(p.var(), tout);
} }
); );

2
src/math/lp/static_matrix.h
View file

@ -47,7 +47,7 @@ template <typename T>
using row_strip = vector<row_cell<T>>; using row_strip = vector<row_cell<T>>;
template <typename K> mpq get_denominators_lcm(const K & row) { template <typename K> mpq get_denominators_lcm(const K & row) {
mpq r = mpq(1); mpq r = mpq(1);
for (auto & c : row) for (const auto & c : row)
r = lcm(r, denominator(c.coeff())); r = lcm(r, denominator(c.coeff()));
return r; return r;
} }