luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Fix out-of-bound bug in &glucose

This commit is contained in:
Alan Mishchenko 2026-04-30 18:04:04 -07:00
parent b413eb90de
commit 153d6b7f82
2 changed files with 6 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

3
src/sat/glucose/AbcGlucose.cpp
View File

@ -878,6 +878,9 @@ Vec_Int_t * Glucose_SolverFromAig( Gia_Man_t * p, SimpSolver& s )
abctime clk = Abc_Clock();
vec<Lit> * lits = &s.user_lits;
Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 1/*fAddOrCla*/, 0, 0/*verbose*/ );
// CNF variable IDs are 1-based and may include unused variables.
// Create the full range so model[] can be indexed by pVarNums directly.
s.addVar( pCnf->nVars - 1 );
for ( int i = 0; i < pCnf->nClauses; i++ )
{
lits->clear();

3
src/sat/glucose2/AbcGlucose2.cpp
View File

@ -896,6 +896,9 @@ Vec_Int_t * Glucose_SolverFromAig( Gia_Man_t * p, SimpSolver& s )
abctime clk = Abc_Clock();
vec<Lit> * lits = &s.user_lits;
Cnf_Dat_t * pCnf = (Cnf_Dat_t *)Mf_ManGenerateCnf( p, 8 /*nLutSize*/, 0 /*fCnfObjIds*/, 1/*fAddOrCla*/, 0, 0/*verbose*/ );
// CNF variable IDs are 1-based and may include unused variables.
// Create the full range so model[] can be indexed by pVarNums directly.
s.addVar( pCnf->nVars - 1 );
for ( int i = 0; i < pCnf->nClauses; i++ )
{
lits->clear();