From d1272defeb869af820313c7ece5b90c4bbe51bc1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 Nov 2025 21:48:23 -0800 Subject: [PATCH] fix warnings in nla_pp Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_pp.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/math/lp/nla_pp.cpp b/src/math/lp/nla_pp.cpp index f4bfc1f8f..567171119 100644 --- a/src/math/lp/nla_pp.cpp +++ b/src/math/lp/nla_pp.cpp @@ -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));