Bug fix in &scorr

berkeley-abc · Oct 21, 2024 · 74e7c64 · 74e7c64
1 parent 707442e
commit 74e7c64
Showing 1 changed file with 7 additions and 3 deletions.
diff --git 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 )
         {