diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index b6d22bff5..96a1c97a3 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -124,10 +124,12 @@ struct solver::imp { den = lcm(den, denominator(coeff)); for (auto const& [w, coeff] : lra.get_term(v)) { auto pw = definitions.get(w); + polynomial::polynomial_ref term(pm); + term = pm.mul(den * coeff, pw); if (!p) - p = pm.mul(den * coeff, pw); + p = term; else - p = pm.add(p, pm.mul(den * coeff, pw)); + p = pm.add(p, term); } } else {