diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2015-06-22 23:04:59 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2015-06-22 23:04:59 -0700 |
commit | da65e88e3b346bcd70198b980e918ea9f1e11b4e (patch) | |
tree | ce660cd8d798ddd41787322db32e6ae21b2ceb11 /src/aig/fra/fraSec.c | |
parent | 270f6db24625e4838dcafe7d45e69cc9522d703e (diff) | |
download | abc-da65e88e3b346bcd70198b980e918ea9f1e11b4e.tar.gz abc-da65e88e3b346bcd70198b980e918ea9f1e11b4e.tar.bz2 abc-da65e88e3b346bcd70198b980e918ea9f1e11b4e.zip |
Version abc90804
committer: Baruch Sterin <baruchs@gmail.com>
Diffstat (limited to 'src/aig/fra/fraSec.c')
-rw-r--r-- | src/aig/fra/fraSec.c | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c index 72af2466..ccb3e7b1 100644 --- a/src/aig/fra/fraSec.c +++ b/src/aig/fra/fraSec.c @@ -480,6 +480,7 @@ clk = clock(); } else if ( pParSec->fInterSeparate ) { + Ssw_Cex_t * pCex = NULL; Aig_Man_t * pTemp, * pAux; Aig_Obj_t * pObjPo; int i, Counter = 0; @@ -495,8 +496,7 @@ clk = clock(); RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &Depth ); if ( pTemp->pSeqModel ) { - Ssw_Cex_t * pCex; - pCex = pNew->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL; + pCex = p->pSeqModel = Ssw_SmlDupCounterExample( pTemp->pSeqModel, Aig_ManRegNum(p) ); pCex->iPo = i; Aig_ManStop( pTemp ); break; @@ -520,7 +520,7 @@ clk = clock(); printf( "Solving output %3d (out of %3d) using interpolation.\r", i, Saig_ManPoNum(pNew) ); } Aig_ManCleanup( pNew ); - if ( pNew->pSeqModel == NULL ) + if ( pCex == NULL ) { printf( "Interpolation left %d (out of %d) outputs unsolved \n", Counter, Saig_ManPoNum(pNew) ); if ( Counter ) |