From 17ed9c39bec9728d3d8e95c930b0eb0f34a36dad Mon Sep 17 00:00:00 2001 From: Lev Date: Tue, 2 Oct 2018 11:06:42 -0700 Subject: [PATCH] add a comment Signed-off-by: Lev --- src/util/lp/nla_solver.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/util/lp/nla_solver.cpp b/src/util/lp/nla_solver.cpp index f762cf941..c875d9f9a 100644 --- a/src/util/lp/nla_solver.cpp +++ b/src/util/lp/nla_solver.cpp @@ -1000,7 +1000,9 @@ struct solver::imp { typedef std::forward_iterator_tag iterator_category; void init_vars_by_the_mask(unsigned_vector & k_vars, unsigned_vector & j_vars) const { - k_vars.push_back(m_binary_factorizations.m_rooted_vars.back()); + // the last element for m_binary_factorizations.m_rooted_vars goes to k_vars + SASSERT(m_mask.size() + 1 == m_binary_factorizations.m_rooted_vars.size()); + k_vars.push_back(m_binary_factorizations.m_rooted_vars.back()); for (unsigned j = 0; j < m_mask.size(); j++) { if (m_mask[j] == 1) { k_vars.push_back(m_binary_factorizations.m_rooted_vars[j]);