Bug fix in the naming of outputs in %blast -d.

src/base/wlc/wlcBlast.c

@@ -1701,6 +1701,23 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
     {
         char * pName = Wlc_ObjName(p, Wlc_ObjId(p, pObj));
         nRange = Wlc_ObjRange( pObj );
+        if ( pPar->fCreateMiter && nRange > 1 )
+        {
+            Wlc_Obj_t * pObj2 = Wlc_NtkCo( p, ++i );
+            char * pName2 = Wlc_ObjName(p, Wlc_ObjId(p, pObj2));
+            int nRange1 = Wlc_ObjRange( pObj );
+            assert( nRange == nRange1 );
+            for ( k = 0; k < nRange; k++ )
+            {
+                char Buffer[1000];
+                sprintf( Buffer, "%s[%d]", pName, k );
+                Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
+                sprintf( Buffer, "%s[%d]", pName2, k );
+                Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
+            }
+        }
+        else
+        {
             if ( fSkipBitRange && nRange == 1 )
                 Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(pName) );
             else
@@ -1711,6 +1728,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
                     Vec_PtrPush( pNew->vNamesOut, Abc_UtilStrsav(Buffer) );
                 }
         }
+    }
     if ( vAddObjs )
     {
         // add internal primary outputs