From ddcd1ee992e999e061161e4541cf70d18d8d21b1 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 28 Sep 2023 09:25:36 -0700 Subject: [PATCH] non-fixed term should have bound 0 Signed-off-by: Nikolaj Bjorner --- src/math/lp/monomial_bounds.cpp | 2 +- src/smt/theory_lra.cpp | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) 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;