Serious bug fix in 'scorr -F <num>' with <num> > 1.

src/aig/aig/aigDfs.c

@@ -199,6 +199,20 @@ void Aig_ManDfsAll_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
     Aig_ManDfsAll_rec( p, Aig_ObjFanin1(pObj), vNodes );
     Vec_PtrPush( vNodes, pObj );
 }
+Vec_Ptr_t * Aig_ManDfsArray( Aig_Man_t * p, Aig_Obj_t ** pNodes, int nNodes )
+{
+    Vec_Ptr_t * vNodes;
+    int i;
+    Aig_ManIncrementTravId( p );
+    vNodes = Vec_PtrAlloc( Aig_ManObjNumMax(p) );
+    // add constant
+    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
+    Vec_PtrPush( vNodes, Aig_ManConst1(p) );
+    // collect nodes reachable in the DFS order
+    for ( i = 0; i < nNodes; i++ )
+        Aig_ManDfsAll_rec( p, pNodes[i], vNodes );
+    return vNodes;
+}
 
 /**Function*************************************************************
 

src/aig/aig/aigUtil.c

@@ -653,23 +653,36 @@ void Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, i
 void Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig )
 {
     assert( !Aig_IsComplement(pObj) );
-    printf( "Node %p : ", pObj );
+    printf( "Node %d : ", pObj->Id );
     if ( Aig_ObjIsConst1(pObj) )
         printf( "constant 1" );
     else if ( Aig_ObjIsCi(pObj) )
-        printf( "PI" );
+        printf( "CI" );
     else if ( Aig_ObjIsCo(pObj) )
     {
-        printf( "PO" );
-        printf( "%p%s", 
-            Aig_ObjFanin0(pObj), (Aig_ObjFaninC0(pObj)? "\'" : " ") );
+        printf( "CO( " );
+        printf( "%d%s )", 
+            Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " ") );
     }
     else
-        printf( "AND( %p%s, %p%s )", 
-            Aig_ObjFanin0(pObj), (Aig_ObjFaninC0(pObj)? "\'" : " "), 
-            Aig_ObjFanin1(pObj), (Aig_ObjFaninC1(pObj)? "\'" : " ") );
+        printf( "AND( %d%s, %d%s )", 
+            Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " "), 
+            Aig_ObjFanin1(pObj)->Id, (Aig_ObjFaninC1(pObj)? "\'" : " ") );
     printf( " (refs = %3d)", Aig_ObjRefs(pObj) );
 }
+void Aig_ObjPrintVerboseCone( Aig_Man_t * p, Aig_Obj_t * pRoot, int fHaig )
+{
+    extern Vec_Ptr_t * Aig_ManDfsArray( Aig_Man_t * p, Aig_Obj_t ** pNodes, int nNodes );
+    Vec_Ptr_t * vNodes;
+    Aig_Obj_t * pObj;
+    int i;
+    vNodes = Aig_ManDfsArray( p, &pRoot, 1 );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+        Aig_ObjPrintVerbose( pObj, fHaig ), printf( "\n" );
+    printf( "\n" );
+    Vec_PtrFree( vNodes );
+
+}
 
 /**Function*************************************************************
 

src/proof/ssw/sswSweep.c

@@ -287,6 +287,9 @@ clk = Abc_Clock();
         Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
         Saig_ManForEachPi( p->pAig, pObj, i )
             Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
+        // sweep flops
+        Saig_ManForEachLo( p->pAig, pObj, i )
+            p->fRefined |= Ssw_ManSweepNode( p, pObj, f, 1, NULL );
         // sweep internal nodes
         Aig_ManForEachNode( p->pAig, pObj, i )
         {