mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-18 06:39:02 +00:00
Code Activity

add a comment

Browse source 
Signed-off-by: Lev <levnach@hotmail.com>
This commit is contained in:
Lev 2018-10-02 11:06:42 -07:00 committed by Lev Nachmanson
parent 2fb63f559c
commit 17ed9c39be
1 changed files with 3 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

4
src/util/lp/nla_solver.cpp
View file

@ -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]);