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

fix the build

Browse source
This commit is contained in:
Lev Nachmanson 2024-08-27 09:53:46 -10:00 committed by Lev Nachmanson
parent 3d5ee82bd1
commit bbeecc6f7c
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

@ -156,7 +156,6 @@ namespace lp {
void init() { void init() {
unsigned n_of_rows = lra.A_r().row_count(); unsigned n_of_rows = lra.A_r().row_count();
unsigned skipped = 0;
unsigned fn = 0; unsigned fn = 0;
auto all_vars_are_int = [this](const auto& row) { auto all_vars_are_int = [this](const auto& row) {
@ -189,7 +188,7 @@ namespace lp {
mpq gcd_of_coeffs(const term_o& t) { mpq gcd_of_coeffs(const term_o& t) {
mpq g(0); mpq g(0);
for (auto & p : t) { for (const auto & p : t) {
if (g.is_zero()) { if (g.is_zero()) {
g = abs(p.coeff()); g = abs(p.coeff());
} else { } else {
@ -287,7 +286,7 @@ namespace lp {
unsigned k; unsigned k;
int k_sign; int k_sign;
mpq t; mpq t;
for (auto& p : eh) { for (const auto& p : eh) {
t = abs(p.coeff()); t = abs(p.coeff());
if (first || t < ahk) { if (first || t < ahk) {
ahk = t; ahk = t;