From 1a788d24fd5ad088a58d520783d6f16541a72e0d Mon Sep 17 00:00:00 2001 From: Lev Date: Fri, 1 Feb 2019 22:37:13 -0800 Subject: [PATCH] a fix in the initialization Signed-off-by: Lev --- src/util/lp/nla_solver.cpp | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index 04f438b33..da5bdc02f 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -710,9 +710,13 @@ struct solver::imp { } void init_abs_val_table() { - // register only those that a factors in a monomial - for (unsigned j = 0; j < m_lar_solver.number_of_vars(); j++) { - m_vars_equivalence.register_var_with_abs_val(j, vvr(j)); + // register those vars that a factors in a monomial + for (auto & p : m_monomials_containing_var) { + m_vars_equivalence.register_var_with_abs_val(p.first, vvr(p.first)); + } + // register monomial vars too + for (auto & p : m_var_to_its_monomial) { + m_vars_equivalence.register_var_with_abs_val(p.first, vvr(p.first)); } }