From 5d74635f7bd626d9bf55882892e82cf110b3ff6b Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 7 Dec 2012 22:07:47 -0800
Subject: Restoring correct behavior of 'tempor' after a change in counting BMC
 frames in 'bmc2'.

---
 src/aig/saig/saigTempor.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

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 )
-- 
cgit v1.2.3