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/int | |
| 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/int')
| -rw-r--r-- | src/aig/int/intCtrex.c | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/aig/int/intCtrex.c b/src/aig/int/intCtrex.c index 28b1e293..0aa60040 100644 --- a/src/aig/int/intCtrex.c +++ b/src/aig/int/intCtrex.c @@ -133,7 +133,7 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose ) if ( status == l_True ) { int i, * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize ); - pCtrex = Ssw_SmlAllocCounterExample( Saig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames ); + pCtrex = Abc_CexAlloc( Saig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames ); pCtrex->iFrame = nFrames - 1; pCtrex->iPo = 0; for ( i = 0; i < Vec_IntSize(vCiIds); i++ ) @@ -145,7 +145,7 @@ void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose ) sat_solver_delete( pSat ); Vec_IntFree( vCiIds ); // verify counter-example - status = Ssw_SmlRunCounterExample( pAig, pCtrex ); + status = Saig_ManVerifyCex( pAig, pCtrex ); if ( status == 0 ) printf( "Inter_ManGetCounterExample(): Counter-example verification has FAILED.\n" ); // report the results |