Bug fix in processing NDR.

src/base/wlc/wlcBlast.c

@@ -2110,7 +2110,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
         // complement flop inputs whose init state is 1
         for ( i = 0; i < nFf2Regs; i++ )
             Gia_ManAppendCo( pNew, Gia_ManAppendCi(pNew) );
-        //Gia_ManSetRegNum( pNew, nFf2Regs );
+        Gia_ManSetRegNum( pNew, nFf2Regs );
     }
     else
     {

src/base/wlc/wlcNdr.c

@@ -368,7 +368,7 @@ Wlc_Ntk_t * Wlc_NtkFromNdr( void * pData )
     Ndr_Data_t * p = (Ndr_Data_t *)pData;  
     Wlc_Obj_t * pObj; Vec_Int_t * vName2Obj, * vFanins = Vec_IntAlloc( 100 );
     int Mod = 2, i, k, Obj, * pArray, nDigits, fFound, NameId, NameIdMax;
-    Vec_Wrd_t * vTruths = NULL;
+    Vec_Wrd_t * vTruths = NULL; int nTruths[2] = {0};
     Wlc_Ntk_t * pTemp, * pNtk = Wlc_NtkAlloc( "top", Ndr_DataObjNum(p, Mod)+1 );
     Wlc_NtkCheckIntegrity( pData );
     Vec_IntClear( &pNtk->vFfs );
@@ -415,11 +415,14 @@ Wlc_Ntk_t * Wlc_NtkFromNdr( void * pData )
             Vec_IntPush( &pNtk->vFfs2, iObj );
         if ( Type == ABC_OPER_LUT )
         {
+            word * pTruth;
             if ( vTruths == NULL )
                 vTruths = Vec_WrdStart( 1000 );
             if ( NameId >= Vec_WrdSize(vTruths) )
                 Vec_WrdFillExtra( vTruths, 2*NameId, 0 );
-            Vec_WrdWriteEntry( vTruths, NameId, *((word *)Ndr_ObjReadBodyP(p, Obj, NDR_FUNCTION)) );
+            pTruth = (word *)Ndr_ObjReadBodyP(p, Obj, NDR_FUNCTION);
+            Vec_WrdWriteEntry( vTruths, NameId, pTruth ? *pTruth : 0 );
+            nTruths[ pTruth != NULL ]++;
         }
         if ( Type == ABC_OPER_SLICE )
             Vec_IntPushTwo( vFanins, End, Beg );
@@ -437,6 +440,8 @@ Wlc_Ntk_t * Wlc_NtkFromNdr( void * pData )
             Wlc_ObjFanin1(pNtk, pObj)->Signed = 1;
         }
     }
+    if ( nTruths[0] )
+        printf( "Warning! The number of LUTs without function is %d (out of %d).\n", nTruths[0], nTruths[0]+nTruths[1] );
     // mark primary outputs
     Ndr_ModForEachPo( p, Mod, Obj )
     {

src/proof/acec/acecFadds.c

@@ -314,16 +314,21 @@ void Dtc_ManCutMerge( Gia_Man_t * p, int iObj, int * pList0, int * pList1, Vec_I
         if ( Type == 0 )
             continue;
         vTemp = Type == 1 ? vCutsXor : vCutsMaj;
-        if ( fVerbose )
-            printf( "%d = %s(", iObj, Type == 1 ? "XOR" : "MAJ" );
-        for ( c = 1; c <= pCut[0]; c++ )
+        if ( 0 && Type == 2 )
         {
+            fVerbose = 1;
+            if ( fVerbose )
+                printf( "%d = %s(", iObj, Type == 1 ? "XOR" : "MAJ" );
+            for ( c = 1; c <= pCut[0]; c++ )
+            {
+                if ( fVerbose )
+                    printf( " %d", pCut[c] );
+                Vec_IntPush( vTemp, pCut[c] );
+            }
             if ( fVerbose )
-                printf( " %d", pCut[c] );
-            Vec_IntPush( vTemp, pCut[c] );
+                printf( " )\n" );
+            fVerbose = 0;
         }
-        if ( fVerbose )
-            printf( " )\n" );
         Vec_IntPush( vTemp, iObj );
     }
 }
@@ -450,6 +455,16 @@ Vec_Int_t * Gia_ManDetectFullAdders( Gia_Man_t * p, int fVerbose, Vec_Int_t ** p
     Vec_IntFree( vCutsMaj );
     return vFadds;
 }
+void Gia_ManDetectFullAdders2( Gia_Man_t * p, int fVerbose )
+{
+    Vec_Int_t * vCutsXor2, * vCutsXor, * vCutsMaj;
+    Dtc_ManComputeCuts( p, &vCutsXor2, &vCutsXor, &vCutsMaj, fVerbose );
+    if ( fVerbose )
+        printf( "XOR3 cuts = %d.  MAJ cuts = %d.\n", Vec_IntSize(vCutsXor)/4, Vec_IntSize(vCutsMaj)/4 );
+    Vec_IntFree( vCutsXor2 );
+    Vec_IntFree( vCutsXor );
+    Vec_IntFree( vCutsMaj );
+}
 
 /**Function*************************************************************
 
@@ -1238,6 +1253,7 @@ Gia_Man_t * Gia_ManDupWithArtificialBoxes( Gia_Man_t * p, int DelayC, int nPathM
     return pNew;
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////