mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-12-05 03:26:45 +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 324fb2194b
commit d1272defeb
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) << " = ";
rational p(1);
for (auto w : m.vars())
p *= val(v);
p *= val(w);
out << p;
out << "\n";
}
@ -360,7 +360,6 @@ std::ostream& core::display_constraint_smt(std::ostream& out, unsigned id, lp::l
auto k = c.kind();
auto rhs = c.rhs();
auto lhs = c.coeffs();
auto sz = lhs.size();
rational den = denominator(rhs);
for (auto [coeff, v] : lhs)
den = lcm(den, denominator(coeff));