diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index c393f9519..84ed665f0 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -5816,10 +5816,12 @@ void Gia_ManProdAdderGen( int nArgA, int nArgB, int Seed, int fSigned, int fCla
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Adds a dummy flop to the design.]
+
+  Description [Duplicates the AIG while adding one flop with constant 0 input
+               and no fanout. Handles designs with boxes by also duplicating
+               the timing manager with an additional CI/CO pair.]
 
-  Description []
-               
   SideEffects []
 
   SeeAlso     []
@@ -5827,11 +5829,13 @@ void Gia_ManProdAdderGen( int nArgA, int nArgB, int Seed, int fSigned, int fCla
 ***********************************************************************/
 Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p )
 {
+    extern Tim_Man_t * Tim_ManDupAddFlop( Tim_Man_t * p, int fUnitDelay );
     Gia_Man_t * pNew;
     Gia_Obj_t * pObj;
     int i;
     pNew = Gia_ManStart( Gia_ManObjNum(p) + 2 );
     pNew->pName = Abc_UtilStrsav(p->pName);
+    pNew->pSpec = Abc_UtilStrsav(p->pSpec);
     Gia_ManConst0(p)->Value = 0;
     Gia_ManForEachCi( p, pObj, i )
         pObj->Value = Gia_ManAppendCi( pNew );
@@ -5840,8 +5844,40 @@ Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p )
         pObj->Value = Gia_ManAppendAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
-    Gia_ManAppendCo( pNew, 0 );    
+    Gia_ManAppendCo( pNew, 0 );
     Gia_ManSetRegNum( pNew, Gia_ManRegNum(p)+1 );
+    if ( p->pManTime )
+        pNew->pManTime = Tim_ManDupAddFlop( (Tim_Man_t *)p->pManTime, 0 );
+    if ( p->pAigExtra )
+        pNew->pAigExtra = Gia_ManDup( p->pAigExtra );
+    if ( p->vCiArrs )
+    {
+        pNew->vCiArrs = Vec_IntDup( p->vCiArrs );
+        Vec_IntPush( pNew->vCiArrs, 0.0 ); // default arrival for new flop output
+    }
+    if ( p->vCoReqs )
+    {
+        pNew->vCoReqs = Vec_IntDup( p->vCoReqs );
+        Vec_IntPush( pNew->vCoReqs, ABC_INFINITY ); // default required for new flop input
+    }
+    if ( p->vCoArrs )
+    {
+        pNew->vCoArrs = Vec_IntDup( p->vCoArrs );
+        Vec_IntPush( pNew->vCoArrs, 0.0 ); // default arrival for new flop input
+    }
+    if ( p->vCoAttrs )
+    {
+        pNew->vCoAttrs = Vec_IntDup( p->vCoAttrs );
+        Vec_IntPush( pNew->vCoAttrs, 0 ); // default attribute for new flop input
+    }
+    // copy other timing-related fields
+    pNew->And2Delay = p->And2Delay;
+    if ( p->vInArrs )
+        pNew->vInArrs = Vec_FltDup( p->vInArrs );
+    if ( p->vOutReqs )
+        pNew->vOutReqs = Vec_FltDup( p->vOutReqs );
+    pNew->DefInArrs = p->DefInArrs;
+    pNew->DefOutReqs = p->DefOutReqs;
     return pNew;
 }
 
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index cb48d1de9..080c74471 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -1128,6 +1128,16 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fS
     // compute the miter
     if ( fSeq )
     {
+        extern Gia_Man_t * Gia_ManDupAddFlop( Gia_Man_t * p );
+        if ( Gia_ManRegNum(pGia0) == 0 ) {
+            pGia0 = Gia_ManDupAddFlop( pMiter = pGia0 );
+            Gia_ManStop( pMiter );
+        }
+        if ( Gia_ManRegNum(pGia1) == 0 ) {
+            pGia1 = Gia_ManDupAddFlop( pMiter = pGia1 );
+            Gia_ManStop( pMiter );
+        }
+        
         pMiter = Gia_ManMiter( pGia0, pGia1, 0, 0, 1, 0, fVerbose );
         if ( pMiter )
         {
diff --git a/src/misc/tim/timMan.c b/src/misc/tim/timMan.c
index b90cb0b4d..2df6007cc 100644
--- a/src/misc/tim/timMan.c
+++ b/src/misc/tim/timMan.c
@@ -152,6 +152,103 @@ Tim_Man_t * Tim_ManDup( Tim_Man_t * p, int fUnitDelay )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the timing manager while adding one flop.]
+
+  Description [Creates a new timing manager with one additional CI/CO pair
+               for a new flop. The new CI and CO are added at the end,
+               after all box inputs/outputs.]
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Tim_Man_t * Tim_ManDupAddFlop( Tim_Man_t * p, int fUnitDelay )
+{
+    Tim_Man_t * pNew;
+    Tim_Box_t * pBox;
+    Tim_Obj_t * pObj;
+    float * pDelayTable, * pDelayTableNew;
+    int i, k, nInputs, nOutputs;
+
+    // clear traversal IDs
+    Tim_ManForEachCi( p, pObj, i )
+        pObj->TravId = 0;
+    Tim_ManForEachCo( p, pObj, i )
+        pObj->TravId = 0;
+
+    // create new manager with one additional CI and CO
+    pNew = Tim_ManStart( p->nCis + 1, p->nCos + 1 );
+
+    // copy existing CI connectivity information
+    memcpy( pNew->pCis, p->pCis, sizeof(Tim_Obj_t) * p->nCis );
+
+    // Initialize the new CI (flop output)
+    pNew->pCis[p->nCis].Id = p->nCis;
+    pNew->pCis[p->nCis].iObj2Box = -1;
+    pNew->pCis[p->nCis].iObj2Num = -1;
+    pNew->pCis[p->nCis].timeArr = 0.0;
+    pNew->pCis[p->nCis].timeReq = TIM_ETERNITY;
+
+    // copy existing CO connectivity information
+    memcpy( pNew->pCos, p->pCos, sizeof(Tim_Obj_t) * p->nCos );
+
+    // Initialize the new CO (flop input)
+    pNew->pCos[p->nCos].Id = p->nCos;
+    pNew->pCos[p->nCos].iObj2Box = -1;
+    pNew->pCos[p->nCos].iObj2Num = -1;
+    pNew->pCos[p->nCos].timeArr = 0.0;
+    pNew->pCos[p->nCos].timeReq = TIM_ETERNITY;
+
+    if ( fUnitDelay )
+    {
+        // clear PI arrival and PO required
+        Tim_ManInitPiArrivalAll( pNew, 0.0 );
+        Tim_ManInitPoRequiredAll( pNew, (float)TIM_ETERNITY );
+    }
+
+    // duplicate delay tables
+    if ( Tim_ManDelayTableNum(p) > 0 )
+    {
+        pNew->vDelayTables = Vec_PtrStart( Vec_PtrSize(p->vDelayTables) );
+        Tim_ManForEachTable( p, pDelayTable, i )
+        {
+            if ( pDelayTable == NULL )
+                continue;
+            assert( i == (int)pDelayTable[0] );
+            nInputs   = (int)pDelayTable[1];
+            nOutputs  = (int)pDelayTable[2];
+            pDelayTableNew = ABC_ALLOC( float, 3 + nInputs * nOutputs );
+            pDelayTableNew[0] = (int)pDelayTable[0];
+            pDelayTableNew[1] = (int)pDelayTable[1];
+            pDelayTableNew[2] = (int)pDelayTable[2];
+            for ( k = 0; k < nInputs * nOutputs; k++ )
+                if ( pDelayTable[3+k] == -ABC_INFINITY )
+                    pDelayTableNew[3+k] = -ABC_INFINITY;
+                else
+                    pDelayTableNew[3+k] = fUnitDelay ? (float)fUnitDelay : pDelayTable[3+k];
+            assert( Vec_PtrEntry(pNew->vDelayTables, i) == NULL );
+            Vec_PtrWriteEntry( pNew->vDelayTables, i, pDelayTableNew );
+        }
+    }
+
+    // duplicate boxes
+    if ( Tim_ManBoxNum(p) > 0 )
+    {
+        pNew->vBoxes = Vec_PtrAlloc( Tim_ManBoxNum(p) );
+        Tim_ManForEachBox( p, pBox, i )
+        {
+           Tim_ManCreateBox( pNew, pBox->Inouts[0], pBox->nInputs,
+                pBox->Inouts[pBox->nInputs], pBox->nOutputs, pBox->iDelayTable, pBox->fBlack );
+           Tim_ManBoxSetCopy( pNew, i, pBox->iCopy );
+        }
+    }
+
+    return pNew;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Trims the timing manager.]