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

Correctly updating the failed output when recording the CEX in bmc3 -a.

This commit is contained in:
Alan Mishchenko 2020-04-03 23:35:47 -07:00
parent 5a20a27c62
commit 71fd9165e3
1 changed files with 5 additions and 1 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

6
src/sat/bmc/bmcBmc3.c
View File

@ -1772,6 +1772,7 @@ nTimeSat += clkSatRun;
// check if other outputs failed under the same counter-example // check if other outputs failed under the same counter-example
Saig_ManForEachPo( pAig, pObj, k ) Saig_ManForEachPo( pAig, pObj, k )
{ {
Abc_Cex_t * pCexDup;
if ( k >= Saig_ManPoNum(pAig) ) if ( k >= Saig_ManPoNum(pAig) )
break; break;
// skip solved outputs // skip solved outputs
@ -1807,7 +1808,10 @@ nTimeSat += clkSatRun;
Gia_ManToBridgeResult( stdout, 0, pCexNew0, pCexNew0->iPo ); Gia_ManToBridgeResult( stdout, 0, pCexNew0, pCexNew0->iPo );
} }
// remember solved output // remember solved output
Vec_PtrWriteEntry( p->vCexes, k, Abc_CexDup(pCexNew, Saig_ManRegNum(pAig)) ); //Vec_PtrWriteEntry( p->vCexes, k, Abc_CexDup(pCexNew, Saig_ManRegNum(pAig)) );
pCexDup = Abc_CexDup(pCexNew, Saig_ManRegNum(pAig));
pCexDup->iPo = k;
Vec_PtrWriteEntry( p->vCexes, k, pCexDup );
} }
Abc_CexFreeP( &pCexNew0 ); Abc_CexFreeP( &pCexNew0 );
Abc_CexFree( pCexNew ); Abc_CexFree( pCexNew );