diff --git a/src/math/lp/monomial_bounds.cpp b/src/math/lp/monomial_bounds.cpp index 22b7ed6c6..8e049f059 100644 --- a/src/math/lp/monomial_bounds.cpp +++ b/src/math/lp/monomial_bounds.cpp @@ -293,7 +293,7 @@ namespace nla { lp::lpvar term_index = c().lra.add_term(coeffs, UINT_MAX); auto* dep = explain_fixed(m, k); term_index = c().lra.map_term_index_to_column_index(term_index); - c().lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::EQ, k, dep); + c().lra.update_column_type_and_bound(term_index, lp::lconstraint_kind::EQ, mpq(0), dep); } u_dependency* monomial_bounds::explain_fixed(monic const& m, rational const& k) { diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 1cf476db4..14cb12890 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -2144,7 +2144,7 @@ public: case l_true: propagate_basic_bounds(); propagate_bounds_with_lp_solver(); - // propagate_nla(); + // propagate_nla(); break; case l_undef: break;