diff --git a/src/api/dotnet/Optimize.cs b/src/api/dotnet/Optimize.cs index 3bc06de16..3a54df5d9 100644 --- a/src/api/dotnet/Optimize.cs +++ b/src/api/dotnet/Optimize.cs @@ -156,7 +156,7 @@ namespace Microsoft.Z3 /// /// This API is an alternative to with assumptions for extracting unsat cores. /// Both APIs can be used in the same solver. The unsat core will contain a combination - /// of the Boolean variables provided using + /// of the Boolean variables provided using /// and the Boolean literals /// provided using with assumptions. /// diff --git a/src/math/lp/nra_solver.cpp b/src/math/lp/nra_solver.cpp index f083c0f82..c4fb91968 100644 --- a/src/math/lp/nra_solver.cpp +++ b/src/math/lp/nra_solver.cpp @@ -65,7 +65,7 @@ struct solver::imp { if (m_nla_core.emons().is_monic_var(v)) { auto const &m = m_nla_core.emons()[v]; for (auto v2 : m.vars()) { - den = lcm(denominators[v2], den); + den = denominators[v2] * den; polynomial_ref pw(definitions.get(v2), m_nlsat->pm()); if (!p) p = pw;