diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 8c7349261..f85e14179 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -31765,7 +31765,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Pdr_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIaxrmuyfqipdegjonctkvwzh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSLIaxrmuyfqipdegjonctkvwzhb" ) ) != EOF )
     {
         switch ( c )
         {
@@ -31952,6 +31952,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'z':
             pPars->fNotVerbose ^= 1;
             break;
+        case 'b':
+            pPars->fBlocking ^= 1;
+            break;
         case 'h':
         default:
             goto usage;
@@ -32030,6 +32033,7 @@ usage:
     Abc_Print( -2, "\t-v     : toggle printing optimization summary [default = %s]\n",                       pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing detailed stats default = %s]\n",                              pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-z     : toggle suppressing report about solved outputs [default = %s]\n",             pPars->fNotVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-b     : toggle clause pushing with blocking [default = %s]\n",                        pPars->fBlocking? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n\n");
     Abc_Print( -2, "\t* Implementation of switches -S, -n, and -c is contributed by Zyad Hassan.\n");
     Abc_Print( -2, "\t  The theory and experiments supporting this work can be found in the following paper:\n");
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index d8a548d5c..01de9f858 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -84,6 +84,7 @@ struct Pdr_Par_t_
     abctime timeLastSolved; // the time when the last output was solved
     Vec_Int_t * vOutMap;  // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided)
     char * pInvFileName;  // invariable file name
+    int fBlocking;        // clause pushing with blocking
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 34a327034..5c93addd9 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -80,6 +80,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
     pPars->nDropOuts      =       0;  // the number of timed out outputs
     pPars->timeLastSolved =       0;  // last one solved
     pPars->pInvFileName   =    NULL;  // invariant file name
+    pPars->fBlocking      =       0;  // clause pushing with blocking
 }
 
 /**Function*************************************************************
@@ -241,6 +242,140 @@ int Pdr_ManPushClauses( Pdr_Man_t * p )
     return RetValue;
 }
 
+int ZPdr_ManDown_Exhaustive( Pdr_Man_t *, int, Pdr_Set_t **, Pdr_Set_t *, Hash_Int_t *, Pdr_Set_t *, int * );
+int Pdr_ManPushAndBlockClauses( Pdr_Man_t * p )
+{
+    Pdr_Set_t * pTemp, * pCubeK, * pCubeK1;
+    Vec_Ptr_t * vArrayK, * vArrayK1;
+    int i, j, k, m, RetValue = 0, RetValue2, kMax = Vec_PtrSize(p->vSolvers)-1;
+    int iStartFrame = p->pPars->fShiftStart ? p->iUseFrame : 1;
+    int Counter = 0;
+    
+    int blockCount;
+    int blockAttemp;
+    int added;
+    int l;
+    int RetValue3;
+    Pdr_Set_t *pPred = NULL;
+    Pdr_Set_t *pCubeCpy = NULL;
+
+    abctime clk = Abc_Clock();
+    assert( p->iUseFrame > 0 );
+    Vec_VecForEachLevelStartStop( p->vClauses, vArrayK, k, iStartFrame, kMax )
+    {
+        Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
+        vArrayK1 = Vec_VecEntry( p->vClauses, k+1 );
+        blockCount = 0;
+        blockAttemp = 0;
+        Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
+        {
+            Counter++;
+
+            // remove cubes in the same frame that are contained by pCubeK
+            Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
+            {
+                if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
+                    continue;
+                Pdr_SetDeref( pTemp );
+                Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
+                Vec_PtrPop(vArrayK);
+                m--;
+            }
+
+            // check if the clause can be moved to the next frame
+            added = 1;
+            RetValue2 = Pdr_ManCheckCube( p, k, pCubeK, &pPred, 0, 0, 1 ); // ************************
+            if ( RetValue2 == -1 )
+                return -1;
+            if ( !RetValue2 ) // try to block before pushing
+            {   
+                if ( blockCount < blockAttemp )
+                    continue;
+                else
+                {
+                    blockAttemp++;
+                    pCubeCpy = Pdr_SetDup(pCubeK);
+                    RetValue3 = ZPdr_ManDown_Exhaustive( p, k, &pCubeCpy, pPred, Hash_IntAlloc( 1 ), NULL, &added );
+                    if ( RetValue3 == -1 )
+                    {
+                        Pdr_SetDeref( pCubeCpy );
+                        return -1;
+                    }
+                    if ( RetValue3 == 0 )
+                    {
+                        Pdr_SetDeref( pCubeCpy );
+                        continue;
+                    }
+                    Pdr_SetDeref( pCubeK );
+                    pCubeK = pCubeCpy;
+
+                    for ( l = 1; l <= k; l++ )
+                        Pdr_ManSolverAddClause( p, l, pCubeK );
+                    blockCount++;
+                }
+            }
+            else // directly push
+            {
+                Pdr_Set_t * pCubeMin;
+                pCubeMin = Pdr_ManReduceClause( p, k, pCubeK );
+                if ( pCubeMin != NULL )
+                {
+//                Abc_Print( 1, "%d ", pCubeK->nLits - pCubeMin->nLits );
+                    Pdr_SetDeref( pCubeK );
+                    pCubeK = pCubeMin;
+                }
+            }
+
+            // if it can be moved, add it to the next frame
+            Pdr_ManSolverAddClause( p, k+1, pCubeK );
+            // check if the clause subsumes others
+            Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK1, pCubeK1, i )
+            {
+                if ( !Pdr_SetContains( pCubeK1, pCubeK ) ) // pCubeK contains pCubeK1
+                    continue;
+                Pdr_SetDeref( pCubeK1 );
+                Vec_PtrWriteEntry( vArrayK1, i, Vec_PtrEntryLast(vArrayK1) );
+                Vec_PtrPop(vArrayK1);
+                i--;
+            }
+            // add the last clause
+            Vec_PtrPush( vArrayK1, pCubeK );
+            Vec_PtrWriteEntry( vArrayK, j, Vec_PtrEntryLast(vArrayK) );
+            Vec_PtrPop(vArrayK);
+            j--;
+        }
+        // printf("%d, %d\n", blockCount, blockAtemp);
+        if ( Vec_PtrSize(vArrayK) == 0 )
+            RetValue = 1;
+    }
+
+    // clean up the last one
+    vArrayK = Vec_VecEntry( p->vClauses, kMax );
+    Vec_PtrSort( vArrayK, (int (*)(const void *, const void *))Pdr_SetCompare );
+    Vec_PtrForEachEntry( Pdr_Set_t *, vArrayK, pCubeK, j )
+    {
+        // remove cubes in the same frame that are contained by pCubeK
+        Vec_PtrForEachEntryStart( Pdr_Set_t *, vArrayK, pTemp, m, j+1 )
+        {
+            if ( !Pdr_SetContains( pTemp, pCubeK ) ) // pCubeK contains pTemp
+                continue;
+/*
+            Abc_Print( 1, "===\n" );
+            Pdr_SetPrint( stdout, pCubeK, Aig_ManRegNum(p->pAig), NULL );
+            Abc_Print( 1, "\n" );
+            Pdr_SetPrint( stdout, pTemp, Aig_ManRegNum(p->pAig), NULL );
+            Abc_Print( 1, "\n" );
+*/
+            Pdr_SetDeref( pTemp );
+            Vec_PtrWriteEntry( vArrayK, m, Vec_PtrEntryLast(vArrayK) );
+            Vec_PtrPop(vArrayK);
+            m--;
+        }
+    }
+    p->tPush += Abc_Clock() - clk;
+    return RetValue;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Returns 1 if the clause is contained in higher clauses.]
@@ -487,6 +622,225 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
     return 1;
 }
 
+int ZPdr_ManDown_Exhaustive( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred, Hash_Int_t * keep, Pdr_Set_t * pIndCube, int * added )
+{
+    int RetValue = 0, CtgRetValue, i, ctgAttempts, l, micResult;
+    int j;
+    int kMax = Vec_PtrSize(p->vSolvers)-1;
+    int kTmp = k;
+    Pdr_Set_t * pCubeTmp, * pCubeMin, * pCtg;
+    Pdr_Set_t * pPredTmp = pPred, * pCubePre = *ppCube;
+    Pdr_Set_t * pCubeMinCopy;
+    while ( RetValue == 0 )
+    {
+        ctgAttempts = 0;
+        while ( RetValue == 0 && kTmp > 1 && ctgAttempts < 3 )
+        {   
+            pCtg = Pdr_SetDup( pPredTmp );
+            //Check CTG for inductiveness
+            if ( Pdr_SetIsInit( pCtg, -1 ) )
+            {
+                Pdr_SetDeref( pCtg );
+                break;
+            }
+            if (*added == 0)
+            {
+                for ( i = 1; i <= k; i++ )
+                    Pdr_ManSolverAddClause( p, i, pIndCube);
+                *added = 1;
+            }
+            if ( pPredTmp != pPred )
+                Pdr_SetDeref( pPredTmp );
+            CtgRetValue = Pdr_ManCheckCube( p, kTmp-1, pCtg, &pPredTmp, p->pPars->nConfLimit, 0, 1 );
+            if ( CtgRetValue == -1 )
+            {
+                Pdr_SetDeref( pCtg );
+                Pdr_SetDeref( pPred );
+                if ( pCubePre != *ppCube )
+                    Pdr_SetDeref( pCubePre );
+                return -1;
+            }
+            if ( CtgRetValue == 0 )
+            {
+                if (pCubePre != *ppCube)
+                    Pdr_SetDeref( pCubePre );
+                if (kTmp == 1)
+                {   
+                    Pdr_SetDeref( pCtg );
+                    ctgAttempts++;
+                    kTmp = k;
+                    pPredTmp = pPred;
+                    pCubePre = *ppCube;
+                }
+                else
+                {
+                    pCubePre = pCtg;
+                    kTmp = kTmp - 1;
+                }
+                continue;
+            }
+
+
+            pCubeMin = Pdr_ManReduceClause( p, kTmp-1, pCtg );
+            if ( pCubeMin == NULL )
+                pCubeMin = Pdr_SetDup( pCtg );
+
+            pCubeMinCopy = Pdr_SetDup( pCubeMin );
+            // generalize before pushing
+            micResult = ZPdr_ManSimpleMic( p, kTmp-1, &pCubeMin );
+            if ( micResult == -1 )
+            {
+                Pdr_SetDeref( pCtg );
+                Pdr_SetDeref( pCubeMin );
+                Pdr_SetDeref( pCubeMinCopy );
+                Pdr_SetDeref( pPred );
+                if ( pCubePre != *ppCube )
+                    Pdr_SetDeref( pCubePre );
+                return -1;
+            }
+            for ( l = kTmp; l < kMax; l++ )
+                if ( Pdr_ManCheckCube( p, l, pCubeMin, NULL, p->pPars->nConfLimit, 0, 1 ) != 1 )
+                    break;
+            // add clause
+            for ( i = 1; i <= l; i++ )
+                Pdr_ManSolverAddClause( p, i, pCubeMin ); 
+            Vec_VecPush( p->vClauses, l, pCubeMin );   // consume ref
+            p->nCubes++;
+
+            // try to push the original cube farther
+            for ( j = l; j < kMax; j++ )
+                if ( Pdr_ManCheckCube( p, j, pCubeMinCopy, NULL, p->pPars->nConfLimit, 0, 1 ) != 1 )
+                    break;
+            if ( j > l )
+            {
+                micResult = ZPdr_ManSimpleMic( p, j-1, &pCubeMinCopy );
+                if ( micResult == -1 )
+                {
+                    Pdr_SetDeref( pCtg );
+                    Pdr_SetDeref( pCubeMinCopy );
+                    Pdr_SetDeref( pPred );
+                    if ( pCubePre != *ppCube )
+                        Pdr_SetDeref( pCubePre );
+                    return -1;
+                }
+                // add clause
+                for ( i = 1; i <= j; i++ )
+                    Pdr_ManSolverAddClause( p, i, pCubeMinCopy ); 
+                Vec_VecPush( p->vClauses, j, pCubeMinCopy ); 
+                p->nCubes++;
+            }
+
+            // add new clause
+            if ( p->pPars->fVeryVerbose )
+            {
+                Abc_Print( 1, "Adding cube " );
+                Pdr_SetPrint( stdout, pCubeMin, Aig_ManRegNum(p->pAig), NULL );
+                Abc_Print( 1, " to frame %d.\n", l );
+            }
+            // set priority flops for both cubes
+            for ( i = 0; i < pCubeMin->nLits; i++ )
+            {
+                assert( pCubeMin->Lits[i] >= 0 );
+                assert( (pCubeMin->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
+                if ( (Vec_IntEntry(p->vPrio, pCubeMin->Lits[i] / 2) >> p->nPrioShift) == 0 )
+                    p->nAbsFlops++;
+                Vec_IntAddToEntry( p->vPrio, pCubeMin->Lits[i] / 2, 1 << p->nPrioShift );
+            }
+            for ( i = 0; i < pCubeMinCopy->nLits; i++ )
+            {
+                assert( pCubeMinCopy->Lits[i] >= 0 );
+                assert( (pCubeMinCopy->Lits[i] / 2) < Aig_ManRegNum(p->pAig) );
+                if ( (Vec_IntEntry(p->vPrio, pCubeMinCopy->Lits[i] / 2) >> p->nPrioShift) == 0 )
+                    p->nAbsFlops++;
+                Vec_IntAddToEntry( p->vPrio, pCubeMinCopy->Lits[i] / 2, 1 << p->nPrioShift );
+            }
+
+            Pdr_SetDeref( pPred );
+            RetValue = Pdr_ManCheckCube( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0, 1 );
+            if ( RetValue == -1 )
+            {
+                if ( pCubePre != *ppCube )
+                    Pdr_SetDeref( pCubePre );
+                Pdr_SetDeref( pCtg );
+                return -1;
+            }
+            Pdr_SetDeref( pCtg );
+            if ( RetValue == 1 )
+            {
+                //printf ("IT'S A ONE\n");
+                if ( pCubePre != *ppCube )
+                    Pdr_SetDeref( pCubePre );
+                return 1;
+            }
+            RetValue = Pdr_ManCheckCube( p, kTmp, pCubePre, &pPredTmp, p->pPars->nConfLimit, 0, 1 );
+            if ( RetValue == -1 )
+            {
+                if ( pCubePre != *ppCube )
+                    Pdr_SetDeref( pCubePre );
+                Pdr_SetDeref( pPred );
+                return -1;
+            }
+            if (RetValue == 1)
+            {   
+                ctgAttempts++;
+                if ( pCubePre != *ppCube )
+                    Pdr_SetDeref( pCubePre );
+                kTmp = k;
+                pPredTmp = pPred;
+                pCubePre = *ppCube;
+            }    
+        }
+
+        if (pCubePre != *ppCube)
+            Pdr_SetDeref( pCubePre );
+        if ( pPredTmp != pPred )
+            Pdr_SetDeref( pPredTmp );
+        //join
+        if ( p->pPars->fVeryVerbose )
+        {
+            printf("Cube:\n");
+            ZPdr_SetPrint( *ppCube );
+            printf("\nPred:\n");
+            ZPdr_SetPrint( pPred );
+        }
+        *ppCube = ZPdr_SetIntersection( pCubeTmp = *ppCube, pPred, keep );
+        Pdr_SetDeref( pCubeTmp );
+        Pdr_SetDeref( pPred );
+        if ( *ppCube == NULL )
+            return 0;
+        if ( p->pPars->fVeryVerbose )
+        {
+            printf("Intersection:\n");
+            ZPdr_SetPrint( *ppCube );
+        }
+        if ( Pdr_SetIsInit( *ppCube, -1 ) )
+        {
+            if ( p->pPars->fVeryVerbose )
+                printf ("Failed initiation\n");
+            return 0;
+        }
+        RetValue = Pdr_ManCheckCube( p, k, *ppCube, &pPred, p->pPars->nConfLimit, 0, 1 );
+        if ( RetValue == -1 )
+            return -1;
+        if ( RetValue == 1 )
+        {
+            //printf ("*********IT'S A ONE\n");
+            break;
+        }
+        if ( RetValue == 0 && (*ppCube)->nLits == 1)
+        {
+            Pdr_SetDeref( pPred ); // fixed memory leak
+            // A workaround for the incomplete assignment returned by the SAT
+            // solver
+            return 0;
+        }
+        kTmp = k;
+        pPredTmp = pPred;
+        pCubePre = *ppCube;
+    }
+    return 1;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Specialized sorting of flops based on priority.]
@@ -1287,6 +1641,24 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             Pdr_ManPrintClauses( p, 0 );
         }
         // push clauses into this timeframe
+        if (p->pPars->fBlocking) // clause pushing with blocking
+        {
+            RetValue = Pdr_ManPushAndBlockClauses( p );
+            if ( RetValue == -1 )
+            {
+                if ( p->pPars->fVerbose )
+                    Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
+                if ( !p->pPars->fSilent )
+                {
+                    if ( p->timeToStop && Abc_Clock() > p->timeToStop )
+                        Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOut, iFrame );
+                    else
+                        Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n",  p->pPars->nConfLimit, iFrame );
+                }
+                p->pPars->iFrame = iFrame;
+                return -1;
+            }
+        }
         RetValue = Pdr_ManPushClauses( p );
         if ( RetValue == -1 )
         {