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

Bug fix in &sprove.

This commit is contained in:
Alan Mishchenko 2026-05-11 13:49:26 -07:00
parent 60b3991a0e
commit 8c9e66205e
1 changed files with 6 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

10
src/proof/abs/absGla.c
View File

@ -1847,7 +1847,8 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
}
}
finish:
Prf_ManStopP( &p->pSat->pPrf2 );
if ( p->pSat )
Prf_ManStopP( &p->pSat->pPrf2 );
// cancel old one if it is proving
if ( iFrameTryToProve >= 0 )
Gia_GlaProveCancel( pPars->fVerbose );
@ -1860,9 +1861,9 @@ finish:
{
Vec_IntFreeP( &pAig->vGateClasses );
pAig->vGateClasses = Ga2_ManAbsTranslate( p );
if ( p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit )
if ( p->pSat && p->pPars->nTimeOut && Abc_Clock() >= p->pSat->nRuntimeLimit )
Abc_Print( 1, "GLA reached timeout %d sec in frame %d with a %d-stable abstraction. ", p->pPars->nTimeOut, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
else if ( pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
else if ( p->pSat && pPars->nConfLimit && sat_solver2_nconflicts(p->pSat) >= pPars->nConfLimit )
Abc_Print( 1, "GLA exceeded %d conflicts in frame %d with a %d-stable abstraction. ", pPars->nConfLimit, p->pPars->iFrameProved+1, p->pPars->nFramesNoChange );
else if ( pPars->nRatioMin2 && Vec_IntSize(p->vAbs) >= p->nMarked * pPars->nRatioMin2 / 100 )
Abc_Print( 1, "GLA found that the size of abstraction exceeds %d %% in frame %d during refinement. ", pPars->nRatioMin2, p->pPars->iFrameProved+1 );
@ -1893,7 +1894,8 @@ finish:
ABC_PRTP( "Runtime: Refinement ", p->timeCex, Abc_Clock() - clk );
ABC_PRTP( "Runtime: Other ", p->timeOther, Abc_Clock() - clk );
ABC_PRTP( "Runtime: TOTAL ", Abc_Clock() - clk, Abc_Clock() - clk );
Ga2_ManReportMemory( p );
if ( p->pSat )
Ga2_ManReportMemory( p );
}
// Ga2_ManDumpStats( p->pGia, p->pPars, p->pSat, p->pPars->iFrameProved, 0 );
Ga2_ManStop( p );