Restoring correct behavior of 'tempor' after a change in counting BMC frames in 'bmc2'.

This commit is contained in:
Alan Mishchenko 2012-12-07 22:07:47 -08:00
parent 7b9132311e
commit 5d74635f7b
1 changed files with 1 additions and 1 deletions

View File

@ -230,7 +230,7 @@ Aig_Man_t * Saig_ManTempor( Aig_Man_t * pAig, int nFrames, int TimeOut, int nCon
printf( "A cex found in the first %d frames.\n", nFrames );
return NULL;
}
if ( nFramesFinished < nFrames )
if ( nFramesFinished + 1 < nFrames )
{
int iLastBefore = Vec_IntLastNonZeroBeforeLimit( vTransSigs, nFramesFinished );
if ( iLastBefore < 1 || !fUseTransSigs )