Adding PDR with abstraction.

9 files changed, 330 insertions, 103 deletions

diff --git a/src/aig/gia/giaDup.c b/src/aig/gia/giaDup.c
index b0ba3472..2a0fe6e3 100644
--- a/src/aig/gia/giaDup.c
+++ b/src/aig/gia/giaDup.c
@@ -231,6 +231,80 @@ Gia_Man_t * Gia_ManDupOrderDfs( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+Gia_Man_t * Gia_ManDupAbs( Gia_Man_t * p, Vec_Int_t * vMapPpi2Ff, Vec_Int_t * vMapFf2Ppi )
+{
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    int k, Flop, Used;
+    assert( Vec_IntSize(vMapFf2Ppi) == Vec_IntSize(vMapPpi2Ff) + Vec_IntCountEntry(vMapFf2Ppi, -1) );
+    Gia_ManFillValue( p );
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    // create inputs
+    Gia_ManForEachPi( p, pObj, k )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Vec_IntForEachEntry( vMapPpi2Ff, Flop, k )
+    {
+        pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Flop );
+        pObj->Value = Gia_ManAppendCi(pNew);
+    }
+    Vec_IntForEachEntry( vMapFf2Ppi, Used, Flop )
+    {
+        if ( Used >= 0 )
+        {
+            assert( pObj->Value != ~0 );
+            continue;
+        }
+        pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Flop );
+        assert( pObj->Value == ~0 );
+        pObj->Value = Gia_ManAppendCi(pNew);
+    }
+    Gia_ManForEachCi( p, pObj, k )
+        assert( pObj->Value != ~0 );
+    // create nodes
+    Gia_ManForEachPo( p, pObj, k )
+        Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    Vec_IntForEachEntry( vMapFf2Ppi, Used, Flop )
+    {
+        if ( Used >= 0 )
+            continue;
+        pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Flop );
+        pObj = Gia_ObjRoToRi( p, pObj );
+        Gia_ManDupOrderDfs_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    }
+    // create outputs
+    Gia_ManForEachPo( p, pObj, k )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Vec_IntForEachEntry( vMapFf2Ppi, Used, Flop )
+    {
+        if ( Used >= 0 )
+            continue;
+        pObj = Gia_ManCi( p, Gia_ManPiNum(p) + Flop );
+        pObj = Gia_ObjRoToRi( p, pObj );
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    }
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) - Vec_IntSize(vMapPpi2Ff) );
+    assert( Gia_ManPiNum(pNew) == Gia_ManPiNum(p) + Vec_IntSize(vMapPpi2Ff) );
+    assert( Gia_ManCiNum(pNew) == Gia_ManCiNum(p) );
+    assert( Gia_ManPoNum(pNew) == Gia_ManPoNum(p) );
+    assert( Gia_ManCoNum(pNew) == Gia_ManCoNum(p) - Vec_IntSize(vMapPpi2Ff) );
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG while putting objects in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Gia_Man_t * Gia_ManDupOutputGroup( Gia_Man_t * p, int iOutStart, int iOutStop )
 {
     Gia_Man_t * pNew;
diff --git a/src/base/io/io.c b/src/base/io/io.c
index c2cf15d4..2e1ae591 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -2420,7 +2420,7 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
                         Bmc_CexCareVerify( pAig, pCex, pCare, fVerbose );
                 }
                 else
-                    pCare = Bmc_CexCareMinimize( pAig, 0, pCex, fCheckCex, fVerbose );
+                    pCare = Bmc_CexCareMinimize( pAig, Saig_ManPiNum(pAig), pCex, 4, fCheckCex, fVerbose );
                 Aig_ManStop( pAig );
             }
             // output flop values (unaffected by the minimization)
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 74a15e40..47f0ac8b 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -420,6 +420,8 @@ int ZPdr_ManDown( Pdr_Man_t * p, int k, Pdr_Set_t ** ppCube, Pdr_Set_t * pPred,
             {
                 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 );
             }
 
@@ -778,6 +780,8 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
             {
                 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 );
             }
             Vec_VecPush( p->vClauses, k, pCubeMin );   // consume ref
@@ -837,29 +841,43 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
     Pdr_Set_t * pCube = NULL;
     Aig_Obj_t * pObj;
     Abc_Cex_t * pCexNew;
-    int k, RetValue = -1;
+    int iFrame, RetValue = -1;
     int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
     abctime clkStart = Abc_Clock(), clkOne = 0;
     p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + Abc_Clock(): 0;
     assert( Vec_PtrSize(p->vSolvers) == 0 );
     // in the multi-output mode, mark trivial POs (those fed by const0) as solved 
     if ( p->pPars->fSolveAll )
-        Saig_ManForEachPo( p->pAig, pObj, k )
+        Saig_ManForEachPo( p->pAig, pObj, iFrame )
             if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
             {
-                Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat
+                Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
                 p->pPars->nProveOuts++;
                 if ( p->pPars->fUseBridge )
-                    Gia_ManToBridgeResult( stdout, 1, NULL, k );
+                    Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
             }
     // create the first timeframe
     p->pPars->timeLastSolved = Abc_Clock();
-    Pdr_ManCreateSolver( p, (k = 0) );
+    Pdr_ManCreateSolver( p, (iFrame = 0) );
     while ( 1 )
     {
-        p->nFrames = k;
-        assert( k == Vec_PtrSize(p->vSolvers)-1 );
-        p->iUseFrame = Abc_MaxInt(k, 1);
+        if ( p->pPars->fUseAbs && iFrame == 2 )
+        {
+            int i, Prio, Num = Saig_ManPiNum(p->pAig);
+            assert( p->vAbsFlops == NULL );
+            p->vAbsFlops  = Vec_IntStart( Saig_ManRegNum(p->pAig) );
+            p->vMapFf2Ppi = Vec_IntStartFull( Saig_ManRegNum(p->pAig) );
+            p->vMapPpi2Ff = Vec_IntAlloc( 100 );
+            Vec_IntForEachEntry( p->vPrio, Prio, i )
+                if ( Prio >> p->nPrioShift  )
+                    Vec_IntWriteEntry( p->vAbsFlops, i, 1 );
+        }
+        if ( p->pPars->fUseAbs && p->vAbsFlops )
+            printf( "Starting frame %d with %d flops.\n", iFrame, Vec_IntCountPositive(p->vAbsFlops) );
+
+        p->nFrames = iFrame;
+        assert( iFrame == Vec_PtrSize(p->vSolvers)-1 );
+        p->iUseFrame = Abc_MaxInt(iFrame, 1);
         Saig_ManForEachPo( p->pAig, pObj, p->iOutCur )
         {
             // skip disproved outputs
@@ -876,16 +894,16 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             {
                 if ( !p->pPars->fSolveAll )
                 {
-                    pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur );
+                    pCexNew = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur );
                     p->pAig->pSeqModel = pCexNew;
                     return 0; // SAT
                 }
-                pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
+                pCexNew = (p->pPars->fUseBridge || p->pPars->fStoreCex) ? Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), iFrame*Saig_ManPoNum(p->pAig)+p->iOutCur ) : (Abc_Cex_t *)(ABC_PTRINT_T)1;
                 p->pPars->nFailOuts++;
                 if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, 0 );
                 if ( !p->pPars->fNotVerbose )
                 Abc_Print( 1, "Output %*d was trivially asserted in frame %2d (solved %*d out of %*d outputs).\n",
-                    nOutDigits, p->iOutCur, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
+                    nOutDigits, p->iOutCur, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
                 assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
                 if ( p->pPars->fUseBridge )
                     Gia_ManToBridgeResult( stdout, 0, pCexNew, pCexNew->iPo );
@@ -895,8 +913,8 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                     if ( p->pPars->fVerbose )
                         Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
                     if ( !p->pPars->fSilent )
-                        Abc_Print( 1, "Quitting due to callback on fail.\n" );
-                    p->pPars->iFrame = k;
+                        Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame );
+                    p->pPars->iFrame = iFrame;
                     return -1;
                 }
                 if ( p->pPars->nFailOuts + p->pPars->nDropOuts == Saig_ManPoNum(p->pAig) )
@@ -918,11 +936,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                     if ( p->pPars->fVerbose )
                         Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
                     if ( !p->pPars->fSilent )
-                        Abc_Print( 1, "Reached gap timeout (%d seconds).\n",  p->pPars->nTimeOutGap );
-                    p->pPars->iFrame = k;
+                        Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOutGap, iFrame );
+                    p->pPars->iFrame = iFrame;
                     return -1;
                 }
-                RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit, 0 );
+                RetValue = Pdr_ManCheckCube( p, iFrame, NULL, &pCube, p->pPars->nConfLimit, 0 );
                 if ( RetValue == 1 )
                     break;
                 if ( RetValue == -1 )
@@ -930,9 +948,9 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                     if ( p->pPars->fVerbose )
                         Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
                     if ( p->timeToStop && Abc_Clock() > p->timeToStop )
-                        Abc_Print( 1, "Reached timeout (%d seconds).\n",  p->pPars->nTimeOut );
+                        Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOut, iFrame );
                     else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
-                        Abc_Print( 1, "Reached gap timeout (%d seconds).\n",  p->pPars->nTimeOutGap );
+                        Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOutGap, iFrame );
                     else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
                     {
                         Pdr_QueueClean( p );
@@ -940,10 +958,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                         break; // keep solving
                     }
                     else if ( p->pPars->nConfLimit )
-                        Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
+                        Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n",  p->pPars->nConfLimit, iFrame );
                     else if ( p->pPars->fVerbose )
-                        Abc_Print( 1, "Computation cancelled by the callback.\n" );
-                    p->pPars->iFrame = k;
+                        Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame );
+                    p->pPars->iFrame = iFrame;
                     return -1;
                 }
                 if ( RetValue == 0 )
@@ -954,9 +972,9 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                         if ( p->pPars->fVerbose )
                             Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
                         if ( p->timeToStop && Abc_Clock() > p->timeToStop )
-                            Abc_Print( 1, "Reached timeout (%d seconds).\n",  p->pPars->nTimeOut );
+                            Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOut, iFrame );
                         else if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
-                            Abc_Print( 1, "Reached gap timeout (%d seconds).\n",  p->pPars->nTimeOutGap );
+                            Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOutGap, iFrame );
                         else if ( p->timeToStopOne && Abc_Clock() > p->timeToStopOne )
                         {
                             Pdr_QueueClean( p );
@@ -964,25 +982,33 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                             break; // keep solving
                         }
                         else if ( p->pPars->nConfLimit )
-                            Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
+                            Abc_Print( 1, "Reached conflict limit (%d) in frame %d.\n",  p->pPars->nConfLimit, iFrame );
                         else if ( p->pPars->fVerbose )
-                            Abc_Print( 1, "Computation cancelled by the callback.\n" );
-                        p->pPars->iFrame = k;
+                            Abc_Print( 1, "Computation cancelled by the callback in frame %d.\n", iFrame );
+                        p->pPars->iFrame = iFrame;
                         return -1;
                     }
                     if ( RetValue == 0 )
                     {
                         if ( fPrintClauses )
                         {
-                            Abc_Print( 1, "*** Clauses after frame %d:\n", k );
+                            Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
                             Pdr_ManPrintClauses( p, 0 );
                         }
                         if ( p->pPars->fVerbose )
                             Pdr_ManPrintProgress( p, !p->pPars->fSolveAll, Abc_Clock() - clkStart );
-                        p->pPars->iFrame = k;
+                        p->pPars->iFrame = iFrame;
                         if ( !p->pPars->fSolveAll )
                         {
-                            p->pAig->pSeqModel = Pdr_ManDeriveCex(p);
+                            Abc_Cex_t * pCex = Pdr_ManDeriveCexAbs(p);
+                            if ( pCex == NULL )
+                            {
+                                assert( p->pPars->fUseAbs );
+                                Pdr_QueueClean( p );
+                                pCube = NULL;
+                                break; // keep solving
+                            }
+                            p->pAig->pSeqModel = pCex;
                             return 0; // SAT
                         }
                         p->pPars->nFailOuts++;
@@ -997,13 +1023,13 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                             if ( p->pPars->fVerbose )
                                 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
                             if ( !p->pPars->fSilent )
-                                Abc_Print( 1, "Quitting due to callback on fail.\n" );
-                            p->pPars->iFrame = k;
+                                Abc_Print( 1, "Quitting due to callback on fail in frame %d.\n", iFrame );
+                            p->pPars->iFrame = iFrame;
                             return -1;
                         }
                         if ( !p->pPars->fNotVerbose )
                             Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",
-                                nOutDigits, p->iOutCur, k, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
+                                nOutDigits, p->iOutCur, iFrame, iFrame, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
                         if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
                             return 0; // all SAT
                         Pdr_QueueClean( p );
@@ -1025,7 +1051,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                     if ( p->pPars->vOutMap ) 
                         Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
                     if ( !p->pPars->fNotVerbose ) 
-                        Abc_Print( 1, "Timing out on output %*d.\n", nOutDigits, p->iOutCur );
+                        Abc_Print( 1, "Timing out on output %*d in frame %d.\n", nOutDigits, p->iOutCur, iFrame );
                 }
                 p->timeToStopOne = 0;
             }
@@ -1036,11 +1062,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
         // open a new timeframe
         p->nQueLim = p->pPars->nRestLimit;
         assert( pCube == NULL );
-        Pdr_ManSetPropertyOutput( p, k );
-        Pdr_ManCreateSolver( p, ++k );
+        Pdr_ManSetPropertyOutput( p, iFrame );
+        Pdr_ManCreateSolver( p, ++iFrame );
         if ( fPrintClauses )
         {
-            Abc_Print( 1, "*** Clauses after frame %d:\n", k );
+            Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
             Pdr_ManPrintClauses( p, 0 );
         }
         // push clauses into this timeframe
@@ -1052,11 +1078,11 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             if ( !p->pPars->fSilent )
             {
                 if ( p->timeToStop && Abc_Clock() > p->timeToStop )
-                    Abc_Print( 1, "Reached timeout (%d seconds).\n",  p->pPars->nTimeOut );
+                    Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOut, iFrame );
                 else
-                    Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
+                    Abc_Print( 1, "Reached conflict limit (%d) in frame.\n",  p->pPars->nConfLimit, iFrame );
             }
-            p->pPars->iFrame = k;
+            p->pPars->iFrame = iFrame;
             return -1;
         }
         if ( RetValue )
@@ -1067,17 +1093,17 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                 Pdr_ManReportInvariant( p );
             if ( !p->pPars->fSilent )
                 Pdr_ManVerifyInvariant( p );
-            p->pPars->iFrame = k;
+            p->pPars->iFrame = iFrame;
             // count the number of UNSAT outputs
             p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts;
             // convert previously 'unknown' into 'unsat'
             if ( p->pPars->vOutMap )
-                for ( k = 0; k < Saig_ManPoNum(p->pAig); k++ )
-                    if ( Vec_IntEntry(p->pPars->vOutMap, k) == -2 ) // unknown
+                for ( iFrame = 0; iFrame < Saig_ManPoNum(p->pAig); iFrame++ )
+                    if ( Vec_IntEntry(p->pPars->vOutMap, iFrame) == -2 ) // unknown
                     {
-                        Vec_IntWriteEntry( p->pPars->vOutMap, k, 1 ); // unsat
+                        Vec_IntWriteEntry( p->pPars->vOutMap, iFrame, 1 ); // unsat
                         if ( p->pPars->fUseBridge )
-                            Gia_ManToBridgeResult( stdout, 1, NULL, k );
+                            Gia_ManToBridgeResult( stdout, 1, NULL, iFrame );
                     }
             if ( p->pPars->nProveOuts == Saig_ManPoNum(p->pAig) )
                 return 1; // UNSAT
@@ -1091,44 +1117,44 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
         // check termination
         if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
         {
-            p->pPars->iFrame = k;
+            p->pPars->iFrame = iFrame;
             return -1;
         }
         if ( p->timeToStop && Abc_Clock() > p->timeToStop )
         {
             if ( fPrintClauses )
             {
-                Abc_Print( 1, "*** Clauses after frame %d:\n", k );
+                Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
                 Pdr_ManPrintClauses( p, 0 );
             }
             if ( p->pPars->fVerbose )
                 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
             if ( !p->pPars->fSilent )
-                Abc_Print( 1, "Reached timeout (%d seconds).\n",  p->pPars->nTimeOut );
-            p->pPars->iFrame = k;
+                Abc_Print( 1, "Reached timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOut, iFrame );
+            p->pPars->iFrame = iFrame;
             return -1;
         }
         if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && Abc_Clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
         {
             if ( fPrintClauses )
             {
-                Abc_Print( 1, "*** Clauses after frame %d:\n", k );
+                Abc_Print( 1, "*** Clauses after frame %d:\n", iFrame );
                 Pdr_ManPrintClauses( p, 0 );
             }
             if ( p->pPars->fVerbose )
                 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
             if ( !p->pPars->fSilent )
-                Abc_Print( 1, "Reached gap timeout (%d seconds).\n",  p->pPars->nTimeOutGap );
-            p->pPars->iFrame = k;
+                Abc_Print( 1, "Reached gap timeout (%d seconds) in frame %d.\n",  p->pPars->nTimeOutGap, iFrame );
+            p->pPars->iFrame = iFrame;
             return -1;
         }
-        if ( p->pPars->nFrameMax && k >= p->pPars->nFrameMax )
+        if ( p->pPars->nFrameMax && iFrame >= p->pPars->nFrameMax )
         {
             if ( p->pPars->fVerbose )
                 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
             if ( !p->pPars->fSilent )
                 Abc_Print( 1, "Reached limit on the number of timeframes (%d).\n", p->pPars->nFrameMax );
-            p->pPars->iFrame = k;
+            p->pPars->iFrame = iFrame;
             return -1;
         }
     }
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index fb671700..2ee4ae09 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -31,6 +31,7 @@
 #include "sat/bsat/satSolver.h"
 #include "pdr.h" 
 #include "misc/hash/hashInt.h"
+#include "aig/gia/giaAig.h"
 
 ABC_NAMESPACE_HEADER_START
 
@@ -71,6 +72,7 @@ struct Pdr_Man_t_
     // input problem
     Pdr_Par_t * pPars;     // parameters
     Aig_Man_t * pAig;      // user's AIG
+    Gia_Man_t * pGia;      // user's AIG
     // static CNF representation
     Cnf_Man_t * pCnfMan;   // CNF manager
     Cnf_Dat_t * pCnf1;     // CNF for this AIG
@@ -90,7 +92,10 @@ struct Pdr_Man_t_
     int *       pOrder;    // ordering of the lits
     Vec_Int_t * vActVars;  // the counter of activation variables
     int         iUseFrame; // the first used frame
-    Vec_Int_t * vAbs;      // abstraction (mapping abstracted flop ID into its PPIs number)
+    int         nAbsFlops; // the number of flops used
+    Vec_Int_t * vAbsFlops; // flops currently used
+    Vec_Int_t * vMapFf2Ppi;
+    Vec_Int_t * vMapPpi2Ff;
     // terminary simulation
     Txs_Man_t * pTxs;      
     // internal use
@@ -161,8 +166,6 @@ static inline abctime      Pdr_ManTimeLimit( Pdr_Man_t * p )
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== pdrCex.c ==========================================================*/
-extern Abc_Cex_t *     Pdr_ManDeriveCex( Pdr_Man_t * p );
 /*=== pdrCnf.c ==========================================================*/
 extern int             Pdr_ObjSatVar( Pdr_Man_t * p, int k, int Pol, Aig_Obj_t * pObj );
 extern int             Pdr_ObjRegNum( Pdr_Man_t * p, int k, int iSatVar );
@@ -183,6 +186,7 @@ extern Vec_Int_t *     Pdr_ManDeriveInfinityClauses( Pdr_Man_t * p, int fReduce
 extern Pdr_Man_t *     Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrioInit );
 extern void            Pdr_ManStop( Pdr_Man_t * p );
 extern Abc_Cex_t *     Pdr_ManDeriveCex( Pdr_Man_t * p );
+extern Abc_Cex_t *     Pdr_ManDeriveCexAbs( Pdr_Man_t * p );
 /*=== pdrSat.c ==========================================================*/
 extern sat_solver *    Pdr_ManCreateSolver( Pdr_Man_t * p, int k );
 extern sat_solver *    Pdr_ManFetchSolver( Pdr_Man_t * p, int k );
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index fe759fff..7a8a66d6 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -81,6 +81,7 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, abctime Time )
     for ( i = ThisSize; i < 70; i++ )
         Abc_Print( 1, " " );
     Abc_Print( 1, "%6d", p->nQueMax );
+    Abc_Print( 1, "%6d", p->nAbsFlops );
     Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC );
     if ( p->pPars->fSolveAll )
         Abc_Print( 1, "  CEX =%4d", p->pPars->nFailOuts );
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index b2df5e01..e2807c92 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "pdrInt.h"
-#include "aig/gia/giaAig.h"
+#include "sat/bmc/bmc.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -233,13 +233,6 @@ Vec_Int_t * Pdr_ManDeriveFlopPriorities2( Gia_Man_t * p, int fMuxCtrls )
 //Vec_IntPrint( vCosts );
     return vCosts;
 }
-Vec_Int_t * Pdr_ManDeriveFlopPriorities( Aig_Man_t * pAig, int fMuxCtrls )
-{
-    Gia_Man_t * pGia = Gia_ManFromAigSimple(pAig);
-    Vec_Int_t * vRes = Pdr_ManDeriveFlopPriorities2(pGia, fMuxCtrls);
-    Gia_ManStop( pGia );
-    return vRes;
-}
 
 /**Function*************************************************************
 
@@ -258,6 +251,7 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
     p = ABC_CALLOC( Pdr_Man_t, 1 );
     p->pPars    = pPars;
     p->pAig     = pAig;
+    p->pGia     = (pPars->fFlopPrio || p->pPars->fNewXSim || p->pPars->fUseAbs) ? Gia_ManFromAigSimple(pAig) : NULL;
     p->vSolvers = Vec_PtrAlloc( 0 );
     p->vClauses = Vec_VecAlloc( 0 );
     p->pQueue   = NULL;
@@ -270,7 +264,7 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
     if ( vPrioInit )
         p->vPrio = vPrioInit;
     else if ( pPars->fFlopPrio )
-        p->vPrio = Pdr_ManDeriveFlopPriorities(pAig, 1);
+        p->vPrio = Pdr_ManDeriveFlopPriorities2(p->pGia, 1);
     else if ( p->pPars->fNewXSim )
         p->vPrio = Vec_IntStartNatural( Aig_ManRegNum(pAig) );
     else 
@@ -286,8 +280,6 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
     p->vCi2Rem  = Vec_IntAlloc( 100 );  // CIs to be removed
     p->vRes     = Vec_IntAlloc( 100 );  // final result
     p->pCnfMan  = Cnf_ManStart();
-    if ( p->vAbs )
-        p->vAbs = Vec_IntStart( Aig_ManRegNum(pAig) );
     // ternary simulation
     p->pTxs     = pPars->fNewXSim ? Txs_ManStart( p, pAig, p->vPrio ) : NULL;
     // additional AIG data-members
@@ -328,6 +320,7 @@ void Pdr_ManStop( Pdr_Man_t * p )
     Pdr_Set_t * pCla;
     sat_solver * pSat;
     int i, k;
+    Gia_ManStopP( &p->pGia );
     Aig_ManCleanMarkAB( p->pAig );
     if ( p->pPars->fVerbose ) 
     {
@@ -370,7 +363,9 @@ void Pdr_ManStop( Pdr_Man_t * p )
     Vec_WecFreeP( &p->vVLits );
     // CNF manager
     Cnf_ManStop( p->pCnfMan );
-    Vec_IntFreeP( &p->vAbs );
+    Vec_IntFreeP( &p->vAbsFlops );
+    Vec_IntFreeP( &p->vMapFf2Ppi );
+    Vec_IntFreeP( &p->vMapPpi2Ff );
     // terminary simulation
     if ( p->pPars->fNewXSim )
         Txs_ManStop( p->pTxs );
@@ -419,7 +414,6 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
         nFrames++;
     // create the counter-example
     pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames );
-//    pCex->iPo    = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput;
     pCex->iPo    = p->iOutCur;
     pCex->iFrame = nFrames-1;
     for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
@@ -428,6 +422,8 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
             Lit = pObl->pState->Lits[i];
             if ( lit_sign(Lit) )
                 continue;
+            if ( lit_var(Lit) >= pCex->nPis ) // allows PPI literals to be thrown away
+                continue;
             assert( lit_var(Lit) < pCex->nPis );
             Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
         }
@@ -437,6 +433,97 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
     return pCex;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Derives counter-example when abstraction is used.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p )
+{
+    extern Gia_Man_t * Gia_ManDupAbs( Gia_Man_t * p, Vec_Int_t * vMapPpi2Ff, Vec_Int_t * vMapFf2Ppi );
+
+    Gia_Man_t * pAbs;
+    Abc_Cex_t * pCex, * pCexCare;
+    Pdr_Obl_t * pObl;
+    int i, f, Lit, Flop, nFrames = 0;
+    int nPis = Saig_ManPiNum(p->pAig);
+    int nFfRefined = 0;
+    if ( !p->pPars->fUseAbs )
+        return Pdr_ManDeriveCex(p);
+    // restore previous map
+    Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i )
+    {
+        assert( Vec_IntEntry( p->vMapFf2Ppi, Flop ) == i );
+        Vec_IntWriteEntry( p->vMapFf2Ppi, Flop, -1 );
+    }
+    Vec_IntClear( p->vMapPpi2Ff );
+    // count the number of frames
+    for ( pObl = p->pQueue; pObl; pObl = pObl->pNext )
+    {
+        for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
+        {
+            Lit = pObl->pState->Lits[i]; 
+            if ( lit_var(Lit) < nPis ) // PI literal
+                continue;
+            Flop = lit_var(Lit) - nPis;
+            if ( Vec_IntEntry(p->vMapFf2Ppi, Flop) >= 0 ) // already used PPI literal
+                continue;
+            Vec_IntWriteEntry( p->vMapFf2Ppi, Flop, Vec_IntSize(p->vMapPpi2Ff) );
+            Vec_IntPush( p->vMapPpi2Ff, Flop );
+        }
+        nFrames++;
+    }
+    if ( Vec_IntSize(p->vMapPpi2Ff) == 0 ) // no PPIs -- this is a real CEX
+        return Pdr_ManDeriveCex(p);
+    // create the counter-example
+    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig) - Vec_IntSize(p->vMapPpi2Ff), Saig_ManPiNum(p->pAig) + Vec_IntSize(p->vMapPpi2Ff), nFrames );
+    pCex->iPo    = p->iOutCur;
+    pCex->iFrame = nFrames-1;
+    for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
+        for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
+        {
+            Lit = pObl->pState->Lits[i];
+            if ( lit_sign(Lit) )
+                continue;
+            if ( lit_var(Lit) < nPis ) // PI literal
+                Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
+            else
+            {
+                int iPPI = nPis + Vec_IntEntry(p->vMapFf2Ppi, lit_var(Lit) - nPis);
+                assert( iPPI < pCex->nPis );
+                Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + iPPI );
+            }
+        }
+    assert( f == nFrames );
+    // perform CEX minimization
+    pAbs = Gia_ManDupAbs( p->pGia, p->vMapPpi2Ff, p->vMapFf2Ppi );
+    pCexCare = Bmc_CexCareMinimizeAig( pAbs, nPis, pCex, 1, 1, 1 );
+    Gia_ManStop( pAbs );
+    assert( pCexCare->nPis == pCex->nPis );
+    Abc_CexFree( pCex );
+    // detect care PPIs
+    for ( f = 0; f < nFrames; f++ )
+    {
+        for ( i = nPis; i < pCexCare->nPis; i++ )
+            if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) )
+            {
+                if ( Vec_IntEntry(p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis)) == 0 ) // currently abstracted
+                    Vec_IntWriteEntry( p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis), 1 ), nFfRefined++;
+            }
+    }
+    Abc_CexFree( pCexCare );
+    if ( nFfRefined == 0 ) // no refinement -- this is a real CEX
+        return Pdr_ManDeriveCex(p);
+    printf( "CEX-based refinement refined %d flops.\n", nFfRefined );
+    return NULL;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index 0bcb6e0c..1cff03c7 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/src/proof/pdr/pdrTsim.c
@@ -440,7 +440,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
             if ( !Saig_ObjIsLo( p->pAig, pObj ) )
                 continue;
             Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
-            if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 )
+            if ( Vec_IntEntry(vPrio, Entry) )
                 continue;
             Vec_IntClear( vUndo );
             if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
@@ -454,7 +454,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL );
             if ( !Saig_ObjIsLo( p->pAig, pObj ) )
                 continue;
             Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
-            if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 )
+            if ( !Vec_IntEntry(vPrio, Entry) )
                 continue;
             Vec_IntClear( vUndo );
             if ( Pdr_ManExtendOne( p->pAig, pObj, vUndo, vVisits ) )
@@ -473,7 +473,39 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
     Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
     assert( Vec_IntSize(vRes) > 0 );
     //p->tTsim += Abc_Clock() - clk;
+    // move abstracted literals from flops to inputs
+    if ( p->pPars->fUseAbs && p->vAbsFlops )
+    {
+        int i, iLit, k = 0, fAllNegs = 1;
+        Vec_IntForEachEntry( vRes, iLit, i )
+        {
+            if ( Vec_IntEntry(p->vAbsFlops, Abc_Lit2Var(iLit)) ) // used flop
+            {
+                Vec_IntWriteEntry( vRes, k++, iLit );
+                fAllNegs &= Abc_LitIsCompl(iLit);
+            }
+            else
+                Vec_IntPush( vPiLits, 2*Saig_ManPiNum(p->pAig) + iLit );
+        }
+        Vec_IntShrink( vRes, k );
+        if ( fAllNegs ) // insert any positive literal
+        {
+            Aig_ManForEachObjVec( vCiObjs, p->pAig, pObj, i )
+            {
+                if ( !Saig_ObjIsLo( p->pAig, pObj ) )
+                    continue;
+                if ( Vec_IntEntry(vCiVals, i) )
+                {
+                    Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig);
+                    Vec_IntPush( vRes, Abc_Var2Lit(Entry, 0) );
+                    break;
+                }
+            }
+        }
+    }
     pRes = Pdr_SetCreate( vRes, vPiLits );
+    assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
+
     //ZH: Disabled assertion because this invariant doesn't hold with down
     //because of the join operation which can bring in initial states
     //assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 7820ebe6..a3f353c2 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -164,7 +164,8 @@ extern int               Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t *
 extern int               Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars );
 /*=== bmcCexCare.c ==========================================================*/
 extern Abc_Cex_t *       Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
-extern Abc_Cex_t *       Bmc_CexCareMinimize( Aig_Man_t * p, int nPPis, Abc_Cex_t * pCex, int fCheck, int fVerbose );
+extern Abc_Cex_t *       Bmc_CexCareMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose );
+extern Abc_Cex_t *       Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose );
 extern void              Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
 /*=== bmcCexCut.c ==========================================================*/
 extern Gia_Man_t *       Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c
index 9c0a30d3..cc3e85ea 100644
--- a/src/sat/bmc/bmcCexCare.c
+++ b/src/sat/bmc/bmcCexCare.c
@@ -251,9 +251,9 @@ Abc_Cex_t * Bmc_CexCareTotal( Abc_Cex_t ** pCexes, int nCexes )
     }
     return pCexMin;
 }
-Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nPPis, Abc_Cex_t * pCex, int fCheck, int fVerbose )
+Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose )
 {
-    int nTryCexes = 4; // belongs to range [1;4]
+    //int nTryCexes = 4; // belongs to range [1;4]
     Abc_Cex_t * pCexBest, * pCexMin[4] = {NULL};
     int k, f, i, nOnesBest, nOnesCur, Counter = 0;
     Vec_Int_t * vPriosIn, * vPriosFf;
@@ -278,7 +278,7 @@ Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nPPis, Abc_Cex_t * pCex,
     if ( fVerbose )
     {
         printf( "Original :    " );
-        Bmc_CexPrint( pCex, Gia_ManPiNum(p) - nPPis, 0 );
+        Bmc_CexPrint( pCex, nRealPis, 0 );
     }
     vPriosIn = Vec_IntAlloc( pCex->nPis  * (pCex->iFrame + 1) );
     vPriosFf = Vec_IntAlloc( pCex->nRegs * (pCex->iFrame + 1) );
@@ -290,37 +290,37 @@ Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nPPis, Abc_Cex_t * pCex,
         if ( k == 0 )
         {
             for ( f = 0; f <= pCex->iFrame; f++ )
-                for ( i = nPPis; i < Gia_ManPiNum(p); i++ )
+                for ( i = nRealPis; i < Gia_ManPiNum(p); i++ )
                     Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
             for ( f = 0; f <= pCex->iFrame; f++ )
-                for ( i = 0; i < nPPis; i++ )
+                for ( i = 0; i < nRealPis; i++ )
                     Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
         }
         else if ( k == 1 )
         {
             for ( f = pCex->iFrame; f >= 0; f-- )
-                for ( i = nPPis; i < Gia_ManPiNum(p); i++ )
+                for ( i = nRealPis; i < Gia_ManPiNum(p); i++ )
                     Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
             for ( f = pCex->iFrame; f >= 0; f-- )
-                for ( i = 0; i < nPPis; i++ )
+                for ( i = 0; i < nRealPis; i++ )
                     Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
         }
         else if ( k == 2 )
         {
             for ( f = 0; f <= pCex->iFrame; f++ )
-                for ( i = Gia_ManPiNum(p) - 1; i >= nPPis; i-- )
+                for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- )
                     Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
             for ( f = 0; f <= pCex->iFrame; f++ )
-                for ( i = nPPis - 1; i >= 0; i-- )
+                for ( i = nRealPis - 1; i >= 0; i-- )
                     Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
         }
         else if ( k == 3 )
         {
             for ( f = pCex->iFrame; f >= 0; f-- )
-                for ( i = Gia_ManPiNum(p) - 1; i >= nPPis; i-- )
+                for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- )
                     Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
             for ( f = pCex->iFrame; f >= 0; f-- )
-                for ( i = nPPis - 1; i >= 0; i-- )
+                for ( i = nRealPis - 1; i >= 0; i-- )
                     Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
         }
         else assert( 0 );
@@ -328,37 +328,37 @@ Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nPPis, Abc_Cex_t * pCex,
         if ( k == 0 )
         {
             for ( f = pCex->iFrame; f >= 0; f-- )
-                for ( i = nPPis; i < Gia_ManPiNum(p); i++ )
+                for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- )
                     Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
             for ( f = pCex->iFrame; f >= 0; f-- )
-                for ( i = 0; i < nPPis; i++ )
+                for ( i = nRealPis - 1; i >= 0; i-- )
                     Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
         }
         else if ( k == 1 )
         {
             for ( f = pCex->iFrame; f >= 0; f-- )
-                for ( i = nPPis; i < Gia_ManPiNum(p); i++ )
+                for ( i = Gia_ManPiNum(p) - 1; i >= nRealPis; i-- )
                     Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
             for ( f = pCex->iFrame; f >= 0; f-- )
-                for ( i = nPPis - 1; i >= 0; i-- )
+                for ( i = 0; i < nRealPis; i++ )
                     Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
         }
         else if ( k == 2 )
         {
             for ( f = pCex->iFrame; f >= 0; f-- )
-                for ( i = Gia_ManPiNum(p) - 1; i >= nPPis; i-- )
+                for ( i = nRealPis; i < Gia_ManPiNum(p); i++ )
                     Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
             for ( f = pCex->iFrame; f >= 0; f-- )
-                for ( i = 0; i < nPPis; i++ )
+                for ( i = nRealPis - 1; i >= 0; i-- )
                     Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
         }
         else if ( k == 3 )
         {
             for ( f = pCex->iFrame; f >= 0; f-- )
-                for ( i = Gia_ManPiNum(p) - 1; i >= nPPis; i-- )
+                for ( i = nRealPis; i < Gia_ManPiNum(p); i++ )
                     Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
             for ( f = pCex->iFrame; f >= 0; f-- )
-                for ( i = nPPis - 1; i >= 0; i-- )
+                for ( i = 0; i < nRealPis; i++ )
                     Vec_IntWriteEntry( vPriosIn, f * pCex->nPis + i, Abc_Var2Lit(Counter++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i)) );
         }
         else assert( 0 );
@@ -377,15 +377,15 @@ Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nPPis, Abc_Cex_t * pCex,
         if ( fVerbose )
         {
             if ( k == 0 )
-                printf( "PiUp FrUp:    " );
+                printf( "PI-  PPI-:    " );
             else if ( k == 1 )
-                printf( "PiUp FrDn:    " );
+                printf( "PI+  PPI-:    " );
             else if ( k == 2 )
-                printf( "PiDn FrUp:    " );
+                printf( "PI-  PPI+:    " );
             else if ( k == 3 )
-                printf( "PiDn FrDn:    " );
+                printf( "PI+  PPI+:    " );
             else assert( 0 );
-            Bmc_CexPrint( pCexMin[k], Gia_ManPiNum(p) - nPPis, 0 );
+            Bmc_CexPrint( pCexMin[k], nRealPis, 0 );
         }
     }
     Vec_IntFree( vPriosIn );
@@ -395,6 +395,8 @@ Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nPPis, Abc_Cex_t * pCex,
     nOnesBest = Abc_CexCountOnes(pCexMin[0]);
     for ( k = 1; k < nTryCexes; k++ )
     {
+        if ( pCexMin[k] == NULL )
+            continue;
         nOnesCur = Abc_CexCountOnes(pCexMin[k]);
         if ( nOnesBest > nOnesCur )
         {
@@ -406,13 +408,13 @@ Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nPPis, Abc_Cex_t * pCex,
     {
         //Abc_Cex_t * pTotal = Bmc_CexCareTotal( pCexMin, nTryCexes );
         printf( "Final    :    " );
-        Bmc_CexPrint( pCexBest, Gia_ManPiNum(p) - nPPis, 0 );
+        Bmc_CexPrint( pCexBest, nRealPis, 0 );
         //printf( "Total    :    " );
-        //Bmc_CexPrint( pTotal, Gia_ManPiNum(p) - nPPis, 0 );
+        //Bmc_CexPrint( pTotal, nRealPis, 0 );
         //Abc_CexFreeP( &pTotal );
     }
     for ( k = 0; k < nTryCexes; k++ )
-        if ( pCexBest != pCexMin[k] )
+        if ( pCexMin[k] && pCexBest != pCexMin[k] )
             Abc_CexFreeP( &pCexMin[k] );
     // verify and return
     if ( !Bmc_CexVerify( p, pCex, pCexBest ) )
@@ -421,10 +423,10 @@ Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nPPis, Abc_Cex_t * pCex,
         printf( "Counter-example verification succeeded.\n" );
     return pCexBest;
 }
-Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, int nPPis, Abc_Cex_t * pCex, int fCheck, int fVerbose )
+Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose )
 {
     Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
-    Abc_Cex_t * pCexMin = Bmc_CexCareMinimizeAig( pGia, nPPis, pCex, fCheck, fVerbose );
+    Abc_Cex_t * pCexMin = Bmc_CexCareMinimizeAig( pGia, nRealPis, pCex, nTryCexes, fCheck, fVerbose );
     Gia_ManStop( pGia );
     return pCexMin;
 }
@@ -459,7 +461,7 @@ void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, in
 /*
     {
         Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
-        Abc_Cex_t * pCex = Bmc_CexCareMinimize( pAig, 3*Saig_ManPiNum(pAig)/4, pAbc->pCex, 1, 1 );
+        Abc_Cex_t * pCex = Bmc_CexCareMinimize( pAig, 3*Saig_ManPiNum(pAig)/4, 4, pAbc->pCex, 1, 1 );
         Aig_ManStop( pAig );
         Abc_CexFree( pCex );
     }