From 71fd9165e39b5bda06e88d5bb545a3ef38c94e96 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 3 Apr 2020 23:35:47 -0700 Subject: Correctly updating the failed output when recording the CEX in bmc3 -a. --- src/sat/bmc/bmcBmc3.c | 6 +++++- 1 file changed, 5 insertions(+), 1 deletion(-) (limited to 'src') 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 ); -- cgit v1.2.3