summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-12-07 22:07:47 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2012-12-07 22:07:47 -0800
commit5d74635f7bd626d9bf55882892e82cf110b3ff6b (patch)
treefea5e0848617fb31407d56b3c9fbd706d4ff3508
parent7b9132311ec663a9bed59017b7938ddd64029df4 (diff)
downloadabc-5d74635f7bd626d9bf55882892e82cf110b3ff6b.tar.gz
abc-5d74635f7bd626d9bf55882892e82cf110b3ff6b.tar.bz2
abc-5d74635f7bd626d9bf55882892e82cf110b3ff6b.zip
Restoring correct behavior of 'tempor' after a change in counting BMC frames in 'bmc2'.
-rw-r--r--src/aig/saig/saigTempor.c2
1 files changed, 1 insertions, 1 deletions
diff --git a/src/aig/saig/saigTempor.c b/src/aig/saig/saigTempor.c
index 4e884140..d459b664 100644
--- a/src/aig/saig/saigTempor.c
+++ b/src/aig/saig/saigTempor.c
@@ -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 )