From 153d6b7f823bea309f97742d820e26b007660ae9 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 30 Apr 2026 18:04:04 -0700 Subject: [PATCH] Fix out-of-bound bug in &glucose --- src/sat/glucose/AbcGlucose.cpp | 3 +++ src/sat/glucose2/AbcGlucose2.cpp | 3 +++ 2 files changed, 6 insertions(+) diff --git a/src/sat/glucose/AbcGlucose.cpp b/src/sat/glucose/AbcGlucose.cpp index d6f4c454d..3df050cbc 100644 --- a/src/sat/glucose/AbcGlucose.cpp +++ b/src/sat/glucose/AbcGlucose.cpp @@ -878,6 +878,9 @@ Vec_Int_t * Glucose_SolverFromAig( Gia_Man_t * p, SimpSolver& s ) abctime clk = Abc_Clock(); vec * 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(); diff --git a/src/sat/glucose2/AbcGlucose2.cpp b/src/sat/glucose2/AbcGlucose2.cpp index 6201779cb..2d7d1c3f5 100644 --- a/src/sat/glucose2/AbcGlucose2.cpp +++ b/src/sat/glucose2/AbcGlucose2.cpp @@ -896,6 +896,9 @@ Vec_Int_t * Glucose_SolverFromAig( Gia_Man_t * p, SimpSolver& s ) abctime clk = Abc_Clock(); vec * 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();