diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-04-03 23:35:47 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-04-03 23:35:47 -0700 |
| commit | 71fd9165e39b5bda06e88d5bb545a3ef38c94e96 (patch) | |
| tree | a46a891100a51c7d74a3f7a447ae57688d9e6ce2 | |
| parent | 5a20a27c620563e90694462df299dc3933844670 (diff) | |
| download | abc-71fd9165e39b5bda06e88d5bb545a3ef38c94e96.tar.gz abc-71fd9165e39b5bda06e88d5bb545a3ef38c94e96.tar.bz2 abc-71fd9165e39b5bda06e88d5bb545a3ef38c94e96.zip | |
Correctly updating the failed output when recording the CEX in bmc3 -a.
| -rw-r--r-- | src/sat/bmc/bmcBmc3.c | 6 |
1 files changed, 5 insertions, 1 deletions
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index 904a2d7f..6f408047 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -1772,6 +1772,7 @@ nTimeSat += clkSatRun; // check if other outputs failed under the same counter-example Saig_ManForEachPo( pAig, pObj, k ) { + Abc_Cex_t * pCexDup; if ( k >= Saig_ManPoNum(pAig) ) break; // skip solved outputs @@ -1807,7 +1808,10 @@ nTimeSat += clkSatRun; Gia_ManToBridgeResult( stdout, 0, pCexNew0, pCexNew0->iPo ); } // 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_CexFree( pCexNew ); |