Bug fix in &satlut.

alanminko · alanminko · commit 41e73dbd8b2e · 2026-01-17T17:34:52.000+07:00
diff --git a/src/aig/gia/giaSatLut.c b/src/aig/gia/giaSatLut.c
@@ -1033,7 +1033,7 @@ int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot )
 
     StartSol = Vec_IntSize(p->vSolInit) + 1;
 //    StartSol = 30;
-    while ( fKeepTrying && StartSol-fKeepTrying > 0 )
+    while ( fKeepTrying && StartSol-fKeepTrying > 0 && StartSol-fKeepTrying < Vec_IntSize(p->vCardVars) )
     {
         int Count = 0, LitCount = 0;
         int nConfBef, nConfAft;

Original file line number	Diff line number	Diff line change
`@@ -1033,7 +1033,7 @@ int Sbl_ManTestSat( Sbl_Man_t * p, int iPivot )`
`1033`	`1033`
`1034`	`1034`	`StartSol = Vec_IntSize(p->vSolInit) + 1;`
`1035`	`1035`	`// StartSol = 30;`
`1036`		`- while ( fKeepTrying && StartSol-fKeepTrying > 0 )`
	`1036`	`+ while ( fKeepTrying && StartSol-fKeepTrying > 0 && StartSol-fKeepTrying < Vec_IntSize(p->vCardVars) )`
`1037`	`1037`	`{`
`1038`	`1038`	`int Count = 0, LitCount = 0;`
`1039`	`1039`	`int nConfBef, nConfAft;`