mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-31 06:07:46 +00:00
Code Activity

fix warnings in nla_pp

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-11-25 21:48:23 -08:00
parent 2fd89c5921
commit 0c1ff55adf
1 changed files with 1 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -343,7 +343,7 @@ std::ostream& core::display_declarations_smt(std::ostream& out) const {
out << "); " << val(v) << " = "; out << "); " << val(v) << " = ";
rational p(1); rational p(1);
for (auto w : m.vars()) for (auto w : m.vars())
p *= val(v); p *= val(w);
out << p; out << p;
out << "\n"; out << "\n";
} }
@ -360,7 +360,6 @@ std::ostream& core::display_constraint_smt(std::ostream& out, unsigned id, lp::l
auto k = c.kind(); auto k = c.kind();
auto rhs = c.rhs(); auto rhs = c.rhs();
auto lhs = c.coeffs(); auto lhs = c.coeffs();
auto sz = lhs.size();
rational den = denominator(rhs); rational den = denominator(rhs);
for (auto [coeff, v] : lhs) for (auto [coeff, v] : lhs)
den = lcm(den, denominator(coeff)); den = lcm(den, denominator(coeff));