From abc4c5962b39e82c0dbe2402cc622b1800cee349 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 13 Mar 2020 16:32:49 -0700 Subject: [PATCH] fix #3269 Signed-off-by: Nikolaj Bjorner --- src/math/lp/nla_core.cpp | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index fdd019567..a38de126d 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -134,10 +134,9 @@ void core::add_monic(lpvar v, unsigned sz, lpvar const* vs) { for (unsigned i = 0; i < sz; i++) { lpvar j = vs[i]; if (m_lar_solver.is_term(j)) - j = m_lar_solver.adjust_term_index(j); + j = m_lar_solver.map_term_index_to_column_index(j); m_add_buffer[i] = j; } - m_emons.add(v, m_add_buffer); }