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

Corner case bug fix in &sat -a.

This commit is contained in:
Alan Mishchenko 2020-03-18 19:00:29 -07:00
parent 488f949721
commit c54da1e990
1 changed files with 12 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

15
src/proof/cec/cecSolve.c
View File

@ -673,6 +673,14 @@ p->timeSatUndec += Abc_Clock() - clk;
SeeAlso [] SeeAlso []
***********************************************************************/ ***********************************************************************/
Abc_Cex_t * Cex_ManGenSimple( Cec_ManSat_t * p, int iOut )
{
Abc_Cex_t * pCex;
pCex = Abc_CexAlloc( 0, Gia_ManCiNum(p->pAig), 1 );
pCex->iPo = iOut;
pCex->iFrame = 0;
return pCex;
}
Abc_Cex_t * Cex_ManGenCex( Cec_ManSat_t * p, int iOut ) Abc_Cex_t * Cex_ManGenCex( Cec_ManSat_t * p, int iOut )
{ {
Abc_Cex_t * pCex; Abc_Cex_t * pCex;
@ -715,10 +723,11 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
{ {
if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) ) if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) )
{ {
pObj->fMark0 = 0; status = !Gia_ObjFaninC0(pObj);
pObj->fMark1 = 1; pObj->fMark0 = (status == 0);
pObj->fMark1 = (status == 1);
if ( pPars->fSaveCexes ) if ( pPars->fSaveCexes )
Vec_PtrWriteEntry( pAig->vSeqModelVec, i, (Abc_Cex_t *)(ABC_PTRINT_T)1 ); Vec_PtrWriteEntry( pAig->vSeqModelVec, i, status ? (Abc_Cex_t *)(ABC_PTRINT_T)1 : Cex_ManGenSimple(p, i) );
continue; continue;
} }
Bar_ProgressUpdate( pProgress, i, "SAT..." ); Bar_ProgressUpdate( pProgress, i, "SAT..." );