From 74e7c64662e20aa39cfabf413668fd94540013d1 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Mon, 21 Oct 2024 13:16:29 +0700
Subject: [PATCH] Bug fix in &scorr

---
 src/proof/cec/cecCorr.c | 10 +++++++---
 1 file changed, 7 insertions(+), 3 deletions(-)

diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c
index c3edf61ff..8d4c730a1 100644
--- a/src/proof/cec/cecCorr.c
+++ b/src/proof/cec/cecCorr.c
@@ -1320,9 +1320,9 @@ Vec_Int_t * Gia_ManFindStopFlops( Gia_Man_t * p, int nFlopIncFreq, int fVerbose
         if ( Spot >= 0 && Vec_IntEntry(vAvail, i) == 0 )
             Vec_IntPush( vHeads, i );
     Vec_IntForEachEntry( vHeads, Spot, i ) {
-        Vec_IntFill( vAvail, Gia_ManRegNum(p), 0 );
+        Gia_ManIncrementTravId( p );
         for ( k = 0, Temp = Spot; Vec_IntEntry(vNexts, Temp) >= 0; k++, Temp = Vec_IntEntry(vNexts, Temp) ) {
-            if ( Vec_IntEntry(vAvail, Temp) )
+            if ( Gia_ObjUpdateTravIdCurrentId(p, Temp) )
                 break;
             Vec_IntWriteEntry( vAvail, Temp, 1 );
         }
@@ -1331,9 +1331,13 @@ Vec_Int_t * Gia_ManFindStopFlops( Gia_Man_t * p, int nFlopIncFreq, int fVerbose
             nItems++;
             if ( vRes == NULL ) 
                 vRes = Vec_IntAlloc( 100 );
-            for ( k = 0, Temp = Spot; Vec_IntEntry(vNexts, Temp) >= 0; k++, Temp = Vec_IntEntry(vNexts, Temp) )
+            Gia_ManIncrementTravId( p );
+            for ( k = 0, Temp = Spot; Vec_IntEntry(vNexts, Temp) >= 0; k++, Temp = Vec_IntEntry(vNexts, Temp) ) {
+                if ( Gia_ObjUpdateTravIdCurrentId(p, Temp) )
+                    break;            
                 if ( k % nFlopIncFreq == 0 )
                     Vec_IntPush( vRes, Temp );
+            }
         }
         while ( Vec_IntEntry(vNexts, Spot) >= 0 )
         {