mirror of
https://github.com/Z3Prover/z3
synced 2025-04-06 17:44:08 +00:00
non-fixed term should have bound 0
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
65e59e3ec4
commit
ddcd1ee992
|
@ -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) {
|
||||
|
|
|
@ -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;
|
||||
|
|
Loading…
Reference in a new issue