diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-13 17:46:48 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-02-13 17:46:48 -0800 |
| commit | 71cbf17e7f0352556af12ccccf9051e02c773e58 (patch) | |
| tree | 002afb74b25be94e512e4869d328959046529766 /src/aig/gia/giaAbs.c | |
| parent | 686d38d66754027cd29c64f1dc2975248eab7796 (diff) | |
| download | abc-71cbf17e7f0352556af12ccccf9051e02c773e58.tar.gz abc-71cbf17e7f0352556af12ccccf9051e02c773e58.tar.bz2 abc-71cbf17e7f0352556af12ccccf9051e02c773e58.zip | |
Unified the use of counter-examples in three packages.
Diffstat (limited to 'src/aig/gia/giaAbs.c')
| -rw-r--r-- | src/aig/gia/giaAbs.c | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/aig/gia/giaAbs.c b/src/aig/gia/giaAbs.c index 38e010f1..607e5ac6 100644 --- a/src/aig/gia/giaAbs.c +++ b/src/aig/gia/giaAbs.c @@ -530,8 +530,8 @@ void Gia_ManCexAbstractionStartNew( Gia_Man_t * pGia, Gia_ParAbs_t * pPars ) { printf( "Problem is satisfiable. Found counter-example in frame %d. ", nFrames-1 ); Abc_PrintTime( 1, "Time", clk ); - pGia->pCexSeq = Gia_ManDeriveCexFromArray( pGia, vCex, 0, nFrames-1 ); - if ( !Gia_ManVerifyCounterExample( pGia, pGia->pCexSeq, 0 ) ) + pGia->pCexSeq = Abc_CexCreate( Gia_ManRegNum(pGia), Gia_ManPiNum(pGia), Vec_IntArray(vCex), nFrames-1, 0, 0 ); + if ( !Gia_ManVerifyCex( pGia, pGia->pCexSeq, 0 ) ) Abc_Print( 1, "Generated counter-example is INVALID.\n" ); pPars->Status = 0; } |