diff --git a/scripts/nightly.yaml b/scripts/nightly.yaml index 2cf35b9ec..5ea90e0ef 100644 --- a/scripts/nightly.yaml +++ b/scripts/nightly.yaml @@ -264,7 +264,7 @@ stages: artifactName: 'Mac' targetPath: $(Agent.TempDirectory) - script: cd $(Agent.TempDirectory); mkdir osx-bin; cd osx-bin; unzip ../*osx*.zip - - script: cd $(Agent.TempDirectory); mkdir linux-bin; cd linux-bin; unzip ../*centos*.zip + - script: cd $(Agent.TempDirectory); mkdir linux-bin; cd linux-bin; unzip ../*glibc*.zip - script: cd $(Agent.TempDirectory); mkdir win32-bin; cd win32-bin; unzip ../*x86-win*.zip - script: cd $(Agent.TempDirectory); mkdir win64-bin; cd win64-bin; unzip ../*x64-win*.zip - script: python3 -m pip install --user -U setuptools wheel diff --git a/src/sat/sat_ddfw.cpp b/src/sat/sat_ddfw.cpp index f21e54fb7..d69c4516c 100644 --- a/src/sat/sat_ddfw.cpp +++ b/src/sat/sat_ddfw.cpp @@ -131,7 +131,7 @@ namespace sat { unsigned idx = m_clauses.size(); m_clauses.push_back(clause_info(cls, m_config.m_init_clause_weight)); for (literal lit : *cls) { - m_use_list.reserve(lit.index()+1); + m_use_list.reserve(2*(lit.var()+1)); m_vars.reserve(lit.var()+1); m_use_list[lit.index()].push_back(idx); } @@ -224,6 +224,7 @@ namespace sat { m_flat_use_list.append(ul); } m_use_list_index.push_back(m_flat_use_list.size()); +// m_use_list_index.push_back(m_flat_use_list.size()); } diff --git a/src/sat/sat_ddfw.h b/src/sat/sat_ddfw.h index 411c7010c..89d74f8f4 100644 --- a/src/sat/sat_ddfw.h +++ b/src/sat/sat_ddfw.h @@ -107,7 +107,12 @@ namespace sat { use_list(ddfw& p, literal lit): p(p), i(lit.index()) {} unsigned const* begin() { return p.m_flat_use_list.c_ptr() + p.m_use_list_index[i]; } - unsigned const* end() { return p.m_flat_use_list.c_ptr() + p.m_use_list_index[i+1]; } + unsigned const* end() { + if (p.m_use_list_index.size() <= i + 1) { + std::cout << "out of bounds\n"; + } + VERIFY(p.m_use_list_index.size() > i + 1); return p.m_flat_use_list.c_ptr() + p.m_use_list_index[i + 1]; + } }; void flatten_use_list();