diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-09 09:47:48 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-12-09 09:47:48 -0800 |
| commit | b65ae7349af7de36390ec916701b997cac2a00ed (patch) | |
| tree | 47ce553bcffa963d3debafc0459701a9f6d5ecaa /src/proof/pdr/pdrMan.c | |
| parent | 79aa1f00d6c00118442a240dab12d100e01fdd03 (diff) | |
| download | abc-b65ae7349af7de36390ec916701b997cac2a00ed.tar.gz abc-b65ae7349af7de36390ec916701b997cac2a00ed.tar.bz2 abc-b65ae7349af7de36390ec916701b997cac2a00ed.zip | |
Enabling multi-output solving in 'pdr'.
Diffstat (limited to 'src/proof/pdr/pdrMan.c')
| -rw-r--r-- | src/proof/pdr/pdrMan.c | 5 |
1 files changed, 4 insertions, 1 deletions
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c index 41941a37..78aa2b69 100644 --- a/src/proof/pdr/pdrMan.c +++ b/src/proof/pdr/pdrMan.c @@ -144,6 +144,8 @@ void Pdr_ManStop( Pdr_Man_t * p ) Vec_IntFree( p->vRes ); // final result Vec_IntFree( p->vSuppLits ); // support literals ABC_FREE( p->pCubeJust ); + if ( p->vCexes ) + Vec_PtrFreeFree( p->vCexes ); // additional AIG data-members if ( p->pAig->pFanData != NULL ) Aig_ManFanoutStop( p->pAig ); @@ -173,7 +175,8 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p ) nFrames++; // create the counter-example pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames ); - pCex->iPo = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput; +// pCex->iPo = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput; + pCex->iPo = p->iOutCur; pCex->iFrame = nFrames-1; for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ ) for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ ) |