diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c
index 495861d90..7e90863d8 100644
--- a/src/base/wlc/wlcBlast.c
+++ b/src/base/wlc/wlcBlast.c
@@ -1434,6 +1434,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
     // create AIG manager
     pNew = Gia_ManStart( 5 * Wlc_NtkObjNum(p) + 1000 );
     pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
     pNew->fGiaSimple = pPar->fGiaSimple;
     if ( !pPar->fGiaSimple )
         Gia_ManHashAlloc( pNew );
@@ -2730,7 +2731,6 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn )
         Abc_FrameSetLibBox( pBoxLib );
     }
 
-    //pNew->pSpec = Abc_UtilStrsav( p->pSpec ? p->pSpec : p->pName );
     // dump the miter parts
     if ( 0 )
     {
diff --git a/src/opt/ufar/UfarMgr.cpp b/src/opt/ufar/UfarMgr.cpp
index 6973f69fb..45487af77 100755
--- a/src/opt/ufar/UfarMgr.cpp
+++ b/src/opt/ufar/UfarMgr.cpp
@@ -981,6 +981,10 @@ void UfarManager::Initialize(Wlc_Ntk_t * pNtk, const set<unsigned>& types) {
     profile = Profile();
 
     _pOrigNtk = Wlc_NtkDupDfsSimple(pNtk);
+    if ( _pOrigNtk->pName == NULL )
+        _pOrigNtk->pName = Abc_UtilStrsav( pNtk->pName ? pNtk->pName : pNtk->pSpec );
+    if ( _pOrigNtk->pSpec == NULL )
+        _pOrigNtk->pSpec = Abc_UtilStrsav( pNtk->pName ? pNtk->pName : pNtk->pSpec );
 
     Wlc_Obj_t * pObj;
     int i;
@@ -1083,6 +1087,16 @@ Wlc_Ntk_t * UfarManager::BuildCurrentAbstraction() {
     pNew = RemoveAuxPOs(pTemp = pNew, Wlc_NtkPoNum(_pOrigNtk));
     Wlc_NtkFree(pTemp);
 
+    // Preserve benchmark identity through abstraction refinements so
+    // downstream bit-level engines report a meaningful miter name.
+    if ( _pOrigNtk )
+    {
+        ABC_FREE( pNew->pName );
+        ABC_FREE( pNew->pSpec );
+        pNew->pName = Abc_UtilStrsav( _pOrigNtk->pName ? _pOrigNtk->pName : _pOrigNtk->pSpec );
+        pNew->pSpec = Abc_UtilStrsav( _pOrigNtk->pName ? _pOrigNtk->pName : _pOrigNtk->pSpec );
+    }
+
     // Wlc_WriteVer(pNew, "Abs.v", 0, 0);
 
     return pNew;
diff --git a/src/opt/ufar/UfarPth.cpp b/src/opt/ufar/UfarPth.cpp
index 85bb0e178..c6f8fd276 100755
--- a/src/opt/ufar/UfarPth.cpp
+++ b/src/opt/ufar/UfarPth.cpp
@@ -33,6 +33,28 @@ using namespace std;
 
 namespace UFAR {
 
+static inline void Ufar_CopyGiaNameToAig( Gia_Man_t * pGia, Aig_Man_t * pAig )
+{
+    char * pName = pGia->pName ? pGia->pName : pGia->pSpec;
+    if ( pName == NULL )
+        return;
+    if ( pAig->pName == NULL )
+        pAig->pName = Abc_UtilStrsav( pName );
+    if ( pAig->pSpec == NULL )
+        pAig->pSpec = Abc_UtilStrsav( pName );
+}
+
+static inline void Ufar_CopyAigNameToNtk( Aig_Man_t * pAig, Abc_Ntk_t * pNtk )
+{
+    char * pName = pAig->pName ? pAig->pName : pAig->pSpec;
+    if ( pName == NULL )
+        return;
+    if ( pNtk->pName == NULL )
+        pNtk->pName = Abc_UtilStrsav( pName );
+    if ( pNtk->pSpec == NULL )
+        pNtk->pSpec = Abc_UtilStrsav( pName );
+}
+
 // mutext to control access to shared variables
 pthread_mutex_t g_mutex;
 // cv to control timer
@@ -63,6 +85,7 @@ class PDR : public Solver {
         Pth_Data_t * pData = (Pth_Data_t *)pArg;
 
         _pAig = Gia_ManToAigSimple( pData->pGia );
+        Ufar_CopyGiaNameToAig( pData->pGia, _pAig );
 
         Pdr_Par_t * pPdrPars = &_PdrPars;
         Pdr_ManSetDefaultParams(pPdrPars);
@@ -93,6 +116,7 @@ class PDRA : public Solver {
         Pth_Data_t * pData = (Pth_Data_t *)pArg;
 
         _pAig = Gia_ManToAigSimple( pData->pGia );
+        Ufar_CopyGiaNameToAig( pData->pGia, _pAig );
 
         Pdr_Par_t * pPdrPars = &_PdrPars;
         Pdr_ManSetDefaultParams(pPdrPars);
@@ -126,7 +150,9 @@ class BMC3 : public Solver {
         BMC3 ( void * pArg ) {
             Pth_Data_t * pData = (Pth_Data_t *)pArg;
             Aig_Man_t * pAig = Gia_ManToAigSimple( pData->pGia );
+            Ufar_CopyGiaNameToAig( pData->pGia, pAig );
             _pNtk = Abc_NtkFromAigPhase( pAig );
+            Ufar_CopyAigNameToNtk( pAig, _pNtk );
             Aig_ManStop( pAig );
 
             Saig_ParBmc_t * pBmcPars = &_Pars;
diff --git a/src/opt/untk/NtkNtk.cpp b/src/opt/untk/NtkNtk.cpp
index 97625f8bb..9c2a1da85 100755
--- a/src/opt/untk/NtkNtk.cpp
+++ b/src/opt/untk/NtkNtk.cpp
@@ -52,11 +52,14 @@ static inline int create_buffer(Wlc_Ntk_t * p, Wlc_Obj_t * pObj, Vec_Int_t * vFa
 Gia_Man_t * BitBlast(Wlc_Ntk_t * pNtk) {
     Wlc_BstPar_t Par, * pPar = &Par;
     Wlc_BstParDefault( pPar );
-    return Wlc_NtkBitBlast(pNtk, pPar);
-    //Gia_Man_t * pGia = Wlc_NtkBitBlast2(pNtk, NULL);
-    //printf( "Usingn old bit-blaster: " );
-    //Gia_ManPrintStats( pGia, NULL );
-    //return pGia;
+    Gia_Man_t * pGia = Wlc_NtkBitBlast(pNtk, pPar);
+    if ( pGia == NULL )
+        return NULL;
+    if ( pGia->pName == NULL )
+        pGia->pName = Abc_UtilStrsav( pNtk->pName ? pNtk->pName : pNtk->pSpec );
+    if ( pGia->pSpec == NULL )
+        pGia->pSpec = Abc_UtilStrsav( pNtk->pName ? pNtk->pName : pNtk->pSpec );
+    return pGia;
 }
 
 template<typename Functor>
@@ -1292,7 +1295,15 @@ int bit_level_solve(Wlc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, const string* pFileNam
     }
 
     Aig_Man_t * pAig = Gia_ManToAig(pGia, 0);
+    if ( pAig->pName == NULL )
+        pAig->pName = Abc_UtilStrsav( pGia->pName ? pGia->pName : pGia->pSpec );
+    if ( pAig->pSpec == NULL )
+        pAig->pSpec = Abc_UtilStrsav( pGia->pName ? pGia->pName : pGia->pSpec );
     Abc_Ntk_t * pAbcNtk = Abc_NtkFromAigPhase(pAig);
+    if ( pAbcNtk->pName == NULL )
+        pAbcNtk->pName = Abc_UtilStrsav( pAig->pName ? pAig->pName : pAig->pSpec );
+    if ( pAbcNtk->pSpec == NULL )
+        pAbcNtk->pSpec = Abc_UtilStrsav( pAig->pName ? pAig->pName : pAig->pSpec );
 
     if (pFileName && !pFileName->empty())
         Gia_AigerWriteSimple(pGia, &((*pFileName + ".aig")[0u]));
diff --git a/src/proof/cec/cecProve.c b/src/proof/cec/cecProve.c
index 3c0fd3df6..273791fe4 100644
--- a/src/proof/cec/cecProve.c
+++ b/src/proof/cec/cecProve.c
@@ -83,6 +83,26 @@ typedef struct Par_ThData_t_
     Par_Share_t * pShare;
 } Par_ThData_t;
 static volatile Par_Share_t * g_pUfarShare = NULL;
+static inline void Cec_CopyGiaName( Gia_Man_t * pSrc, Gia_Man_t * pDst )
+{
+    char * pName = pSrc->pName ? pSrc->pName : pSrc->pSpec;
+    if ( pName == NULL )
+        return;
+    if ( pDst->pName == NULL )
+        pDst->pName = Abc_UtilStrsav( pName );
+    if ( pDst->pSpec == NULL )
+        pDst->pSpec = Abc_UtilStrsav( pName );
+}
+static inline void Cec_CopyGiaNameToAig( Gia_Man_t * pGia, Aig_Man_t * pAig )
+{
+    char * pName = pGia->pName ? pGia->pName : pGia->pSpec;
+    if ( pName == NULL )
+        return;
+    if ( pAig->pName == NULL )
+        pAig->pName = Abc_UtilStrsav( pName );
+    if ( pAig->pSpec == NULL )
+        pAig->pSpec = Abc_UtilStrsav( pName );
+}
 static int Cec_SProveStopUfar( int RunId )
 {
     (void)RunId;
@@ -161,6 +181,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
             pPars->pProgress     = (void *)pThData;
         }
         Aig_Man_t * pAig = Gia_ManToAigSimple( p );
+        Cec_CopyGiaNameToAig( p, pAig );
         RetValue = Saig_ManBmcScalable( pAig, pPars );
         p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
         Aig_ManStop( pAig );                 
@@ -177,6 +198,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
             pPars->pProgress     = (void *)pThData;
         }
         Aig_Man_t * pAig = Gia_ManToAigSimple( p );
+        Cec_CopyGiaNameToAig( p, pAig );
         RetValue = Pdr_ManSolve( pAig, pPars );
         p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
         Aig_ManStop( pAig );                
@@ -194,6 +216,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
             pPars->pProgress     = (void *)pThData;
         }
         Aig_Man_t * pAig = Gia_ManToAigSimple( p );
+        Cec_CopyGiaNameToAig( p, pAig );
         RetValue = Saig_ManBmcScalable( pAig, pPars );
         p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
         Aig_ManStop( pAig );                
@@ -211,6 +234,7 @@ int Cec_GiaProveOne( Gia_Man_t * p, int iEngine, int nTimeOut, int fVerbose, Par
             pPars->pProgress     = (void *)pThData;
         }
         Aig_Man_t * pAig = Gia_ManToAigSimple( p );
+        Cec_CopyGiaNameToAig( p, pAig );
         RetValue = Pdr_ManSolve( pAig, pPars );
         p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
         Aig_ManStop( pAig );                
@@ -313,6 +337,7 @@ void Cec_GiaInitThreads( Par_ThData_t * ThData, int nWorkers, Gia_Man_t * p, int
     for ( i = 0; i < nWorkers; i++ )
     {
         ThData[i].p        = Gia_ManDup(p);
+        Cec_CopyGiaName( p, ThData[i].p );
         ThData[i].iEngine  = (fUseUif && i == nWorkers - 1) ? PAR_ENGINE_UFAR : i;
         ThData[i].nTimeOut = nTimeOut;
         ThData[i].fWorking = 0;
@@ -414,7 +439,8 @@ int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, in
     }
     if ( !fSilent )
     {
-        printf( "Problem \"%s\" is ", p->pSpec );
+        char * pProbName = p->pSpec ? p->pSpec : Gia_ManName(p);
+        printf( "Problem \"%s\" is ", pProbName ? pProbName : "(none)" );
         if ( RetValue == 0 )
             printf( "SATISFIABLE (solved by %d).", RetEngine );
         else if ( RetValue == 1 )