Adding procedures to find the care bits of a counter-example (update).

5 files changed, 746 insertions, 59 deletions

diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 39d11174..315e3a8a 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -176,7 +176,8 @@ extern Aig_Man_t *       Saig_ManDecPropertyOutput( Aig_Man_t * pAig, int nLits,
 /*=== saigPhase.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int nPref, int fIgnore, int fPrint, int fVerbose );
 /*=== saigRefSat.c ==========================================================*/
-extern Abc_Cex_t *       Saig_ManFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose );
+extern Vec_Int_t *       Saig_ManExtendCounterExampleTest3( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose );
+extern Abc_Cex_t *       Saig_ManFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fNewOrder, int fVerbose );
 /*=== saigRetFwd.c ==========================================================*/
 extern void              Saig_ManMarkAutonomous( Aig_Man_t * p );
 extern Aig_Man_t *       Saig_ManRetimeForward( Aig_Man_t * p, int nMaxIters, int fVerbose );
@@ -192,6 +193,7 @@ extern Vec_Int_t *       Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirst
 extern Vec_Int_t *       Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fTryFour, int fVerbose );
 /*=== saigSimExt.c ==========================================================*/
 extern Vec_Int_t *       Saig_ManExtendCounterExampleTest2( Aig_Man_t * p, int iFirstPi, Abc_Cex_t * pCex, int fVerbose );
+extern Abc_Cex_t *       Saig_ManFindCexCareBitsSense( Aig_Man_t * p, Abc_Cex_t * pCex, int iFirstFlopPi, int fVerbose );
 /*=== saigSimMv.c ==========================================================*/
 extern int               Saig_MvManSimulate( Aig_Man_t * pAig, int fVerbose );
 /*=== saigStrSim.c ==========================================================*/
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index bed5edaf..3cd508a6 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -225,7 +225,8 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
         return NULL;
     if ( pnUseStart )
         *pnUseStart = pAbs->pSeqModel->iFrame;
-    vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, 1, fVerbose );
+//    vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, 1, fVerbose );
+    vFlopsNew = Saig_ManExtendCounterExampleTest3( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pAbs->pSeqModel, fVerbose );
     if ( vFlopsNew == NULL )
         return NULL;
     if ( Vec_IntSize(vFlopsNew) == 0 )
@@ -238,7 +239,7 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
     }
     // vFlopsNew contains PI numbers that should be kept in pAbs
     if ( fVerbose )
-        printf( "Adding %d registers to the abstraction.\n", Vec_IntSize(vFlopsNew) );
+        printf( "Adding %d registers to the abstraction.\n\n", Vec_IntSize(vFlopsNew) );
     // add to the abstraction
     Vec_IntForEachEntry( vFlopsNew, Entry, i )
     {
@@ -276,7 +277,8 @@ int Saig_ManCexRefineStep( Aig_Man_t * p, Vec_Int_t * vFlops, Abc_Cex_t * pCex,
     if ( fSensePath )
         vFlopsNew = Saig_ManExtendCounterExampleTest2( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose );
     else
-        vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fTryFour, fVerbose );
+//        vFlopsNew = Saig_ManExtendCounterExampleTest( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fTryFour, fVerbose );
+        vFlopsNew = Saig_ManExtendCounterExampleTest3( pAbs, Saig_ManCexFirstFlopPi(p, pAbs), pCex, fVerbose );
     if ( vFlopsNew == NULL )
     {
         Aig_ManStop( pAbs );
diff --git a/src/aig/saig/saigRefSat.c b/src/aig/saig/saigRefSat.c
index bc053fca..0b3dff23 100644
--- a/src/aig/saig/saigRefSat.c
+++ b/src/aig/saig/saigRefSat.c
@@ -40,15 +40,189 @@ struct Saig_RefMan_t_
     int         fVerbose;   // verbose flag
     // unrolling
     Aig_Man_t * pFrames;    // unrolled timeframes
-    Vec_Int_t * vMapPiA3F;  // mapping of frame PIs into real PIs
+    Vec_Int_t * vMapPiF2A;  // mapping of frame PIs into real PIs
 };
 
+// performs ternary simulation
+extern int Saig_ManSimDataInit( Aig_Man_t * p, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, Vec_Int_t * vRes );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [Maps array of frame PI IDs into array of original PI IDs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Saig_RefManReason2Inputs( Saig_RefMan_t * p, Vec_Int_t * vReasons )
+{
+    Vec_Int_t * vOriginal, * vVisited;
+    int i, Entry;
+    vOriginal = Vec_IntAlloc( Saig_ManPiNum(p->pAig) ); 
+    vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) );
+    Vec_IntForEachEntry( vReasons, Entry, i )
+    {
+        int iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry );
+        assert( iInput >= 0 && iInput < Aig_ManPiNum(p->pAig) );
+        if ( Vec_IntEntry(vVisited, iInput) == 0 )
+            Vec_IntPush( vOriginal, iInput );
+        Vec_IntAddToEntry( vVisited, iInput, 1 );
+    }
+    Vec_IntFree( vVisited );
+    return vOriginal;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Saig_RefManReason2Cex( Saig_RefMan_t * p, Vec_Int_t * vReasons )
+{
+    Abc_Cex_t * pCare;
+    int i, Entry, iInput, iFrame;
+    pCare = Abc_CexDup( p->pCex, p->pCex->nRegs );
+    memset( pCare->pData, 0, sizeof(unsigned) * Aig_BitWordNum(pCare->nBits) );
+    Vec_IntForEachEntry( vReasons, Entry, i )
+    {
+        assert( Entry >= 0 && Entry < Aig_ManPiNum(p->pFrames) );
+        iInput = Vec_IntEntry( p->vMapPiF2A, 2*Entry );
+        iFrame = Vec_IntEntry( p->vMapPiF2A, 2*Entry+1 );
+        Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput );
+    }
+    return pCare;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns reasons for the property to fail.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_RefManFindReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vPrios, Vec_Int_t * vReasons )
+{
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        Vec_IntPush( vReasons, Aig_ObjPioNum(pObj) );
+        return;
+    }
+    assert( Aig_ObjIsNode(pObj) );
+    if ( pObj->fPhase )
+    {
+        Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
+        Saig_RefManFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
+    }
+    else
+    {
+        int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
+        int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
+        assert( !fPhase0 || !fPhase1 );
+        if ( !fPhase0 && fPhase1 )
+            Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
+        else if ( fPhase0 && !fPhase1 )
+            Saig_RefManFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
+        else 
+        {
+            int iPrio0 = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
+            int iPrio1 = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
+            if ( iPrio0 <= iPrio1 )
+                Saig_RefManFindReason_rec( p, Aig_ObjFanin0(pObj), vPrios, vReasons );
+            else
+                Saig_RefManFindReason_rec( p, Aig_ObjFanin1(pObj), vPrios, vReasons );
+        }
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns reasons for the property to fail.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Saig_RefManFindReason( Saig_RefMan_t * p )
+{
+    Aig_Obj_t * pObj;
+    Vec_Int_t * vPrios, * vPi2Prio, * vReasons;
+    int i, CountPrios;
+
+    vPi2Prio = Vec_IntStartFull( Saig_ManPiNum(p->pAig) );
+    vPrios   = Vec_IntStartFull( Aig_ManObjNumMax(p->pFrames) );
+
+    // set PI values according to CEX
+    CountPrios = 0;
+    Aig_ManConst1(p->pFrames)->fPhase = 1;
+    Aig_ManForEachPi( p->pFrames, pObj, i )
+    {
+        int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
+        int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
+        pObj->fPhase = Aig_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
+        // assign priority
+        if ( Vec_IntEntry(vPi2Prio, iInput) == ~0 )
+            Vec_IntWriteEntry( vPi2Prio, iInput, CountPrios++ );
+//        Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Vec_IntEntry(vPi2Prio, iInput) );
+        Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), i );
+    }
+//    printf( "Priority numbers = %d.\n", CountPrios );
+    Vec_IntFree( vPi2Prio );
+
+    // traverse and set the priority
+    Aig_ManForEachNode( p->pFrames, pObj, i )
+    {
+        int fPhase0 = Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase;
+        int fPhase1 = Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase;
+        int iPrio0  = Vec_IntEntry( vPrios, Aig_ObjFaninId0(pObj) );
+        int iPrio1  = Vec_IntEntry( vPrios, Aig_ObjFaninId1(pObj) );
+        pObj->fPhase = fPhase0 && fPhase1;
+        if ( fPhase0 && fPhase1 ) // both are one
+            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MaxInt(iPrio0, iPrio1) );
+        else if ( !fPhase0 && fPhase1 ) 
+            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio0 );
+        else if ( fPhase0 && !fPhase1 )
+            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), iPrio1 );
+        else // both are zero
+            Vec_IntWriteEntry( vPrios, Aig_ObjId(pObj), Abc_MinInt(iPrio0, iPrio1) );
+    }
+    // check the property output
+    pObj = Aig_ManPo( p->pFrames, 0 );
+    assert( (int)Aig_ObjFanin0(pObj)->fPhase == Aig_ObjFaninC0(pObj) );
+
+    // select the reason
+    vReasons = Vec_IntAlloc( 100 );
+    Aig_ManIncrementTravId( p->pFrames );
+    Saig_RefManFindReason_rec( p->pFrames, Aig_ObjFanin0(pObj), vPrios, vReasons );
+    Vec_IntFree( vPrios );
+    return vReasons;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Collect nodes in the unrolled timeframes.]
 
   Description []
@@ -86,7 +260,7 @@ void Saig_ManUnrollCollect_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t *
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, Vec_Int_t ** pvMapPiA3F )
+Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, Vec_Int_t ** pvMapPiF2A )
 {
     Aig_Man_t * pFrames;     // unrolled timeframes
     Vec_Vec_t * vFrameCos;   // the list of COs per frame
@@ -100,7 +274,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu
     assert( pCex->iPo >= 0 && pCex->iPo < Saig_ManPoNum(pAig) );
 
     // map PIs of the unrolled frames into PIs of the original design
-    *pvMapPiA3F = Vec_IntAlloc( 1000 );
+    *pvMapPiF2A = Vec_IntAlloc( 1000 );
 
     // collect COs and Objs visited in each frame
     vFrameCos  = Vec_VecStart( pCex->iFrame+1 );
@@ -149,8 +323,8 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu
                 else
                 {
                     pObj->pData = Aig_ObjCreatePi( pFrames );
-                    Vec_IntPush( *pvMapPiA3F, Aig_ObjPioNum(pObj) );
-                    Vec_IntPush( *pvMapPiA3F, f );
+                    Vec_IntPush( *pvMapPiF2A, Aig_ObjPioNum(pObj) );
+                    Vec_IntPush( *pvMapPiF2A, f );
                 }
             }
         }
@@ -164,6 +338,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu
     // create output
     pObj = Aig_ManPo( pAig, pCex->iPo );
     Aig_ObjCreatePo( pFrames, Aig_Not((Aig_Obj_t *)pObj->pData) );
+    Aig_ManSetRegNum( pFrames, 0 );
     // cleanup
     Vec_VecFree( vFrameCos );
     Vec_VecFree( vFrameObjs );
@@ -192,6 +367,7 @@ Saig_RefMan_t * Saig_RefManStart( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInput
     p->pCex = pCex;
     p->nInputs = nInputs;
     p->fVerbose = fVerbose;
+    p->pFrames = Saig_ManUnrollWithCex( pAig, pCex, nInputs, &p->vMapPiF2A );
     return p;
 }
 
@@ -209,7 +385,7 @@ Saig_RefMan_t * Saig_RefManStart( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInput
 void Saig_RefManStop( Saig_RefMan_t * p )
 {
     Aig_ManStopP( &p->pFrames );
-    Vec_IntFreeP( &p->vMapPiA3F );
+    Vec_IntFreeP( &p->vMapPiF2A );
     ABC_FREE( p );
 }
 
@@ -231,8 +407,8 @@ int Saig_RefManSetPhases( Saig_RefMan_t * p, Abc_Cex_t * pCare, int fValue1 )
     Aig_ManConst1( p->pFrames )->fPhase = 1;
     Aig_ManForEachPi( p->pFrames, pObj, i )
     {
-        iInput = Vec_IntEntry( p->vMapPiA3F, 2*i );
-        iFrame = Vec_IntEntry( p->vMapPiA3F, 2*i+1 );
+        iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
+        iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
         pObj->fPhase = Aig_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
         // update value if it is a don't-care
         if ( pCare && !Aig_InfoHasBit( pCare->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput ) )
@@ -249,6 +425,41 @@ int Saig_RefManSetPhases( Saig_RefMan_t * p, Abc_Cex_t * pCare, int fValue1 )
 
 /**Function*************************************************************
 
+  Synopsis    [Tries to remove literals from abstraction.]
+
+  Description [The literals are sorted more desirable first.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Saig_RefManOrderLiterals( Saig_RefMan_t * p, Vec_Int_t * vVar2PiId, Vec_Int_t * vAssumps )
+{
+    Vec_Vec_t * vLits;
+    Vec_Int_t * vVar2New;
+    int i, Entry, iInput, iFrame;
+    // collect literals
+    vLits = Vec_VecAlloc( 100 );
+    vVar2New = Vec_IntStartFull( Saig_ManPiNum(p->pAig) );
+    Vec_IntForEachEntry( vAssumps, Entry, i )
+    {
+        int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) );
+        assert( iPiNum >= 0 && iPiNum < Aig_ManPiNum(p->pFrames) );
+        iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum );
+        iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 );
+//        Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput );
+        if ( Vec_IntEntry( vVar2New, iInput ) == ~0 )
+            Vec_IntWriteEntry( vVar2New, iInput, Vec_VecSize(vLits) );
+        Vec_VecPushInt( vLits, Vec_IntEntry( vVar2New, iInput ), Entry );
+    }
+    Vec_IntFree( vVar2New );
+    return vLits;
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Generate the care set using SAT solver.]
 
   Description []
@@ -258,19 +469,51 @@ int Saig_RefManSetPhases( Saig_RefMan_t * p, Abc_Cex_t * pCare, int fValue1 )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p )
+Abc_Cex_t * Saig_RefManCreateCex( Saig_RefMan_t * p, Vec_Int_t * vVar2PiId, Vec_Int_t * vAssumps )
+{
+    Abc_Cex_t * pCare;
+    int i, Entry, iInput, iFrame;
+    // create counter-example
+    pCare = Abc_CexDup( p->pCex, p->pCex->nRegs );
+    memset( pCare->pData, 0, sizeof(unsigned) * Aig_BitWordNum(pCare->nBits) );
+    Vec_IntForEachEntry( vAssumps, Entry, i )
+    {
+        int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) );
+        assert( iPiNum >= 0 && iPiNum < Aig_ManPiNum(p->pFrames) );
+        iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum );
+        iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 );
+        Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput );
+    }
+    return pCare;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Generate the care set using SAT solver.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder )
 {
     int nConfLimit = 1000000;
     Abc_Cex_t * pCare;
     Cnf_Dat_t * pCnf;
     sat_solver * pSat;
     Aig_Obj_t * pObj;
+    Vec_Vec_t * vLits = NULL;
     Vec_Int_t * vAssumps, * vVar2PiId;
-    int i, f, iInput, iFrame, RetValue, Counter;
+    int i, k, f = 0, Entry, RetValue, Counter = 0;
     int nCoreLits, * pCoreLits;
+    int clk = clock();
     // create CNF
     assert( Aig_ManRegNum(p->pFrames) == 0 );
-    pCnf = Cnf_Derive( p->pFrames, 0 );
+//    pCnf = Cnf_Derive( p->pFrames, 0 ); // too slow
+    pCnf = Cnf_DeriveSimple( p->pFrames, 0 );
     RetValue = Saig_RefManSetPhases( p, NULL, 0 );
     if ( RetValue )
     {
@@ -286,6 +529,7 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p )
         Cnf_DataFree( pCnf );
         return NULL;
     }
+//Abc_PrintTime( 1, "Preparing", clock() - clk );
     // look for a true counter-example
     if ( p->nInputs > 0 )
     {
@@ -306,16 +550,43 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p )
     vAssumps = Vec_IntAlloc( Aig_ManPiNum(p->pFrames) );
     Aig_ManForEachPi( p->pFrames, pObj, i )
     {
-        iInput = Vec_IntEntry( p->vMapPiA3F, 2*i );
-        iFrame = Vec_IntEntry( p->vMapPiA3F, 2*i+1 );
+        int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
+        int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
 //        RetValue = Aig_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
 //        Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !RetValue ) );
         Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 ) );
         Vec_IntWriteEntry( vVar2PiId, pCnf->pVarNums[Aig_ObjId(pObj)], i );
     }
+
+    // reverse the order of assumptions
+//    if ( fNewOrder )
+//    Vec_IntReverseOrder( vAssumps );
+
+    if ( fNewOrder )
+    {
+        // create literals
+        vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps );
+        // sort literals
+        Vec_VecSort( vLits, 1 );
+        // save literals
+        Vec_IntClear( vAssumps );
+        Vec_VecForEachEntryInt( vLits, Entry, i, k )
+            Vec_IntPush( vAssumps, Entry );
+
+        for ( i = 0; i < Vec_VecSize(vLits); i++ )
+            printf( "%d ", Vec_IntSize( (Vec_Int_t *)Vec_VecEntry(vLits, i) ) );
+        printf( "\n" );
+
+        if ( p->fVerbose )
+            printf( "Total PIs = %d. Essential PIs = %d.\n", 
+                Saig_ManPiNum(p->pAig) - p->nInputs, Vec_VecSize(vLits) );
+    }
+
     // solve
+clk = clock();
     RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), 
         (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+//Abc_PrintTime( 1, "Solving", clock() - clk );
     if ( RetValue != l_False )
     {
         if ( RetValue == l_True )
@@ -328,46 +599,89 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p )
         Vec_IntFree( vVar2PiId );
         return NULL;
     }
+    assert( RetValue == l_False ); // UNSAT
+
     // get relevant SAT literals
     nCoreLits = sat_solver_final( pSat, &pCoreLits );
     assert( nCoreLits > 0 );
     if ( p->fVerbose )
-    printf( "Analize final selected %d assumptions out of %d.\n", nCoreLits, Vec_IntSize(vAssumps) );
-    // create counter-example
-    pCare = Abc_CexDup( p->pCex, p->pCex->nRegs );
-    memset( pCare->pData, 0, sizeof(unsigned) * Aig_BitWordNum(pCare->nBits) );
-    // set new values
+    printf( "AnalizeFinal selected %d assumptions (out of %d). Conflicts = %d.\n", 
+        nCoreLits, Vec_IntSize(vAssumps), (int)pSat->stats.conflicts );
+
+    // save literals
+    Vec_IntClear( vAssumps );
     for ( i = 0; i < nCoreLits; i++ )
-    {
-        int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(pCoreLits[i]) );
-        assert( iPiNum >= 0 && iPiNum < Aig_ManPiNum(p->pFrames) );
-        iInput = Vec_IntEntry( p->vMapPiA3F, 2*iPiNum );
-        iFrame = Vec_IntEntry( p->vMapPiA3F, 2*iPiNum+1 );
-        Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * iFrame + iInput );
-    }
+        Vec_IntPush( vAssumps, pCoreLits[i] );
+
+
+    // create literals
+    vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps );
+    // sort literals
+//    Vec_VecSort( vLits, 0 );
+    // save literals
+    Vec_IntClear( vAssumps );
+    Vec_VecForEachEntryInt( vLits, Entry, i, k )
+        Vec_IntPush( vAssumps, Entry );
+
+//    for ( i = 0; i < Vec_VecSize(vLits); i++ )
+//        printf( "%d ", Vec_IntSize( (Vec_Int_t *)Vec_VecEntry(vLits, i) ) );
+//    printf( "\n" );
 
-    // further reduce the CEX
-    Counter = 0;
-    for ( i = p->nInputs; i < Saig_ManPiNum(p->pAig); i++ )
+    if ( p->fVerbose )
+        printf( "Total PIs = %d. Essential PIs = %d.\n", 
+            Saig_ManPiNum(p->pAig) - p->nInputs, Vec_VecSize(vLits) );
+/*
+    // try assumptions in different order
+    RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), 
+        (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+    printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n", 
+        Vec_IntSize(vAssumps), (RetValue == l_False ? "UNSAT" : "SAT"), (int)pSat->stats.conflicts );
+
+    // create different sets of assumptions
+    Counter = Vec_VecSize(vLits);
+    for ( f = 0; f < Vec_VecSize(vLits); f++ )
     {
-        for ( f = 0; f <= pCare->iFrame; f++ )
-            if ( Aig_InfoHasBit( pCare->pData, pCare->nRegs + pCare->nPis * f + i ) )
-                break;
-        if ( f == pCare->iFrame + 1 )
+        Vec_IntClear( vAssumps );
+        Vec_VecForEachEntryInt( vLits, Entry, i, k )
+            if ( i != f )
+                Vec_IntPush( vAssumps, Entry );
+
+        // try the new assumptions
+        RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), 
+            (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+        printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n", 
+            Vec_IntSize(vAssumps), RetValue == l_False ? "UNSAT" : "SAT", (int)pSat->stats.conflicts );
+        if ( RetValue != l_False )
             continue;
-        Counter++;
 
-        // try removing this input
+        // UNSAT - remove literals
+        Vec_IntClear( (Vec_Int_t *)Vec_VecEntry(vLits, f) );
+        Counter--;
     }
-    if ( p->fVerbose )
-    printf( "Essential primary inputs %d out of %d.\n", Counter, Saig_ManPiNum(p->pAig) - p->nInputs );
 
+    for ( i = 0; i < Vec_VecSize(vLits); i++ )
+        printf( "%d ", Vec_IntSize( (Vec_Int_t *)Vec_VecEntry(vLits, i) ) );
+    printf( "\n" );
+
+    if ( p->fVerbose )
+        printf( "Total PIs = %d. Essential PIs = %d.\n", 
+            Saig_ManPiNum(p->pAig) - p->nInputs, Counter );
+
+    // save literals
+    Vec_IntClear( vAssumps );
+    Vec_VecForEachEntryInt( vLits, Entry, i, k )
+        Vec_IntPush( vAssumps, Entry );
+*/
+    // create counter-example
+    pCare = Saig_RefManCreateCex( p, vVar2PiId, vAssumps );
 
     // cleanup
     Cnf_DataFree( pCnf );
     sat_solver_delete( pSat );
     Vec_IntFree( vAssumps );
     Vec_IntFree( vVar2PiId );
+    Vec_VecFreeP( &vLits );
+
     // verify counter-example
     RetValue = Saig_RefManSetPhases( p, pCare, 0 );
     if ( RetValue )
@@ -375,10 +689,167 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p )
     RetValue = Saig_RefManSetPhases( p, pCare, 1 );
     if ( RetValue )
         printf( "Reduced CEX verification has failed.\n" );
-
     return pCare;
-} 
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []               
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Saig_RefManRefineWithSat( Saig_RefMan_t * p, Vec_Int_t * vAigPis )
+{
+    int nConfLimit = 1000000;
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    Aig_Obj_t * pObj;
+    Vec_Vec_t * vLits;
+    Vec_Int_t * vReasons, * vAssumps, * vVisited, * vVar2PiId;
+    int i, k, f, Entry, RetValue, Counter;
+
+    // create CNF and SAT solver
+    pCnf = Cnf_DeriveSimple( p->pFrames, 0 );
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    if ( pSat == NULL )
+    {
+        Cnf_DataFree( pCnf );
+        return NULL;
+    }
+
+    // mark used AIG inputs
+    vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) );
+    Vec_IntForEachEntry( vAigPis, Entry, i )
+    {
+        assert( Entry >= 0 && Entry < Aig_ManPiNum(p->pAig) );
+        Vec_IntWriteEntry( vVisited, Entry, 1 );
+    }
+
+    // create assumptions
+    vVar2PiId = Vec_IntStartFull( pCnf->nVars );
+    vAssumps = Vec_IntAlloc( Aig_ManPiNum(p->pFrames) );
+    Aig_ManForEachPi( p->pFrames, pObj, i )
+    {
+        int iInput = Vec_IntEntry( p->vMapPiF2A, 2*i );
+        int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*i+1 );
+        if ( Vec_IntEntry(vVisited, iInput) == 0 )
+            continue;
+        RetValue = Aig_InfoHasBit( p->pCex->pData, p->pCex->nRegs + p->pCex->nPis * iFrame + iInput );
+        Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], !RetValue ) );
+//        Vec_IntPush( vAssumps, toLitCond( pCnf->pVarNums[Aig_ObjId(pObj)], 1 ) );
+        Vec_IntWriteEntry( vVar2PiId, pCnf->pVarNums[Aig_ObjId(pObj)], i );
+    }
+    Vec_IntFree( vVisited );
+
+    // try assumptions in different order
+    RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), 
+        (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+    printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n", 
+        Vec_IntSize(vAssumps), (RetValue == l_False ? "UNSAT" : "SAT"), (int)pSat->stats.conflicts );
+
+/*
+    // AnalizeFinal does not work because it implications propagate directly
+    // and SAT solver does not kick in (the number of conflicts in 0).
+
+    // count the number of lits in the unsat core
+    {
+        int nCoreLits, * pCoreLits;
+        nCoreLits = sat_solver_final( pSat, &pCoreLits );
+        assert( nCoreLits > 0 );
+
+        // count the number of flops
+        vVisited = Vec_IntStart( Saig_ManPiNum(p->pAig) );
+        for ( i = 0; i < nCoreLits; i++ )
+        {
+            int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(pCoreLits[i]) );
+            int iInput = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum );
+            int iFrame = Vec_IntEntry( p->vMapPiF2A, 2*iPiNum+1 );
+            Vec_IntWriteEntry( vVisited, iInput, 1 );
+        }
+        // count the number of entries
+        Counter = 0;
+        Vec_IntForEachEntry( vVisited, Entry, i )
+            Counter += Entry;
+        Vec_IntFree( vVisited );
+
+//        if ( p->fVerbose )
+        printf( "AnalizeFinal: Assumptions %d (out of %d). Essential PIs = %d. Conflicts = %d.\n", 
+            nCoreLits, Vec_IntSize(vAssumps), Counter, (int)pSat->stats.conflicts );
+    }
+*/
+
+    // derive literals
+    vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps );
+    for ( i = 0; i < Vec_VecSize(vLits); i++ )
+        printf( "%d ", Vec_IntSize( (Vec_Int_t *)Vec_VecEntry(vLits, i) ) );
+    printf( "\n" );
+
+    // create different sets of assumptions
+    Counter = Vec_VecSize(vLits);
+    for ( f = 0; f < Vec_VecSize(vLits); f++ )
+    {
+        Vec_IntClear( vAssumps );
+        Vec_VecForEachEntryInt( vLits, Entry, i, k )
+            if ( i != f )
+                Vec_IntPush( vAssumps, Entry );
+
+        // try the new assumptions
+        RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), 
+            (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+        printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n", 
+            Vec_IntSize(vAssumps), RetValue == l_False ? "UNSAT" : "SAT", (int)pSat->stats.conflicts );
+        if ( RetValue != l_False )
+            continue;
+
+        // UNSAT - remove literals
+        Vec_IntClear( (Vec_Int_t *)Vec_VecEntry(vLits, f) );
+        Counter--;
+    }
 
+    for ( i = 0; i < Vec_VecSize(vLits); i++ )
+        printf( "%d ", Vec_IntSize( (Vec_Int_t *)Vec_VecEntry(vLits, i) ) );
+    printf( "\n" );
+
+    // create assumptions
+    Vec_IntClear( vAssumps );
+    Vec_VecForEachEntryInt( vLits, Entry, i, k )
+        Vec_IntPush( vAssumps, Entry );
+
+    // try assumptions in different order
+    RetValue = sat_solver_solve( pSat, Vec_IntArray(vAssumps), Vec_IntArray(vAssumps) + Vec_IntSize(vAssumps), 
+        (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+    printf( "Assumpts = %2d. Intermediate instance is %5s. Conflicts = %2d.\n", 
+        Vec_IntSize(vAssumps), (RetValue == l_False ? "UNSAT" : "SAT"), (int)pSat->stats.conflicts );
+
+//    if ( p->fVerbose )
+//        printf( "Total PIs = %d. Essential PIs = %d.\n", 
+//            Saig_ManPiNum(p->pAig) - p->nInputs, Counter );
+
+
+    // transform assumptions into reasons
+    vReasons = Vec_IntAlloc( 100 );
+    Vec_IntForEachEntry( vAssumps, Entry, i )
+    {
+        int iPiNum = Vec_IntEntry( vVar2PiId, lit_var(Entry) );
+        assert( iPiNum >= 0 && iPiNum < Aig_ManPiNum(p->pFrames) );
+        Vec_IntPush( vReasons, iPiNum );
+    }
+
+    // cleanup
+    Cnf_DataFree( pCnf );
+    sat_solver_delete( pSat );
+    Vec_IntFree( vAssumps );
+    Vec_IntFree( vVar2PiId );
+    Vec_VecFreeP( &vLits );
+
+    return vReasons;
+}
 
 /**Function*************************************************************
 
@@ -393,32 +864,119 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Cex_t * Saig_ManFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose )
+Abc_Cex_t * Saig_ManFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fNewOrder, int fVerbose )
 {
-    Abc_Cex_t * pCare = NULL;
+    Saig_RefMan_t * p;
+    Vec_Int_t * vReasons;
+    Abc_Cex_t * pCare;
     int clk = clock();
-    Saig_RefMan_t * p = Saig_RefManStart( pAig, pCex, nInputs, fVerbose );
-    p->pFrames = Saig_ManUnrollWithCex( pAig, pCex, nInputs, &p->vMapPiA3F );
-if ( p->fVerbose )
+
+    clk = clock();
+    p = Saig_RefManStart( pAig, pCex, nInputs, fVerbose );
+    vReasons = Saig_RefManFindReason( p );
+
+if ( fVerbose )
 Aig_ManPrintStats( p->pFrames );
 
-if ( p->fVerbose )
-Abc_PrintTime( 1, "Frames", clock() - clk );
+//    if ( fVerbose )
+    {
+        Vec_Int_t * vRes = Saig_RefManReason2Inputs( p, vReasons );
+        printf( "Frame PIs = %4d (essential = %4d)   AIG PIs = %4d (essential = %4d)   ",
+            Aig_ManPiNum(p->pFrames), Vec_IntSize(vReasons), 
+            Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
+ABC_PRT( "Time", clock() - clk );
+
+        Vec_IntFree( vRes );
+
+/*
+        ////////////////////////////////////
+        Vec_IntFree( vReasons );
+        vReasons = Saig_RefManRefineWithSat( p, vRes );
+        ////////////////////////////////////
+
+        Vec_IntFree( vRes );
+        vRes = Saig_RefManReason2Inputs( p, vReasons );
+        printf( "Frame PIs = %4d (essential = %4d)   AIG PIs = %4d (essential = %4d)   ",
+            Aig_ManPiNum(p->pFrames), Vec_IntSize(vReasons), 
+            Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
+
+        Vec_IntFree( vRes );
+ABC_PRT( "Time", clock() - clk );
+*/
+    }
 
-    clk = clock();
-    pCare = Saig_RefManRunSat( p );
+    pCare = Saig_RefManReason2Cex( p, vReasons );
+    Vec_IntFree( vReasons );
     Saig_RefManStop( p );
 
-if ( p->fVerbose )
-Abc_PrintTime( 1, "Filter", clock() - clk );
-
-if ( p->fVerbose )
+if ( fVerbose )
 Abc_CexPrintStats( pCex );
-if ( p->fVerbose )
+if ( fVerbose )
 Abc_CexPrintStats( pCare );
+
     return pCare;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of PIs for flops that should not be absracted.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Saig_ManExtendCounterExampleTest3( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose )
+{
+    Saig_RefMan_t * p;
+    Vec_Int_t * vRes, * vReasons;
+    int clk;
+    if ( Saig_ManPiNum(pAig) != pCex->nPis )
+    {
+        printf( "Saig_ManExtendCounterExampleTest3(): The PI count of AIG (%d) does not match that of cex (%d).\n", 
+            Aig_ManPiNum(pAig), pCex->nPis );
+        return NULL;
+    }
+
+clk = clock();
+
+    p = Saig_RefManStart( pAig, pCex, iFirstFlopPi, fVerbose );
+    vReasons = Saig_RefManFindReason( p );
+    vRes = Saig_RefManReason2Inputs( p, vReasons );
+
+//    if ( fVerbose )
+    {
+        printf( "Frame PIs = %4d (essential = %4d)   AIG PIs = %4d (essential = %4d)   ",
+            Aig_ManPiNum(p->pFrames), Vec_IntSize(vReasons), 
+            Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
+ABC_PRT( "Time", clock() - clk );
+    }
+
+/*
+    ////////////////////////////////////
+    Vec_IntFree( vReasons );
+    vReasons = Saig_RefManRefineWithSat( p, vRes );
+    ////////////////////////////////////
+
+    // derive new result
+    Vec_IntFree( vRes );
+    vRes = Saig_RefManReason2Inputs( p, vReasons );
+//    if ( fVerbose )
+    {
+        printf( "Frame PIs = %4d (essential = %4d)   AIG PIs = %4d (essential = %4d)   ",
+            Aig_ManPiNum(p->pFrames), Vec_IntSize(vReasons), 
+            Saig_ManPiNum(p->pAig) - p->nInputs, Vec_IntSize(vRes) );
+ABC_PRT( "Time", clock() - clk );
+    }
+*/
+
+    Vec_IntFree( vReasons );
+    Saig_RefManStop( p );
+    return vRes;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/saig/saigSimExt2.c b/src/aig/saig/saigSimExt2.c
index cb5d3b77..3d9cc88a 100644
--- a/src/aig/saig/saigSimExt2.c
+++ b/src/aig/saig/saigSimExt2.c
@@ -360,6 +360,118 @@ ABC_PRT( "Time", clock() - clk );
     return vRes;
 }
 
+
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of PIs for flops that should not be absracted.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Saig_ManDeriveCex( Aig_Man_t * p, int iFirstFlopPi, Abc_Cex_t * pCex, Vec_Ptr_t * vSimInfo, int fVerbose )
+{
+    Abc_Cex_t * pCare;
+    Aig_Obj_t * pObj;
+    Vec_Int_t * vRes, * vResInv;
+    int i, f, Value;
+//    assert( Aig_ManRegNum(p) > 0 );
+    assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) );
+    // start simulation data
+    Value = Saig_ManSimDataInit2( p, pCex, vSimInfo );
+    assert( Value == SAIG_ONE_NEW );
+    // derive implications of constants and primary inputs
+    Saig_ManForEachLo( p, pObj, i )
+        Saig_ManSetAndDriveImplications_rec( p, pObj, 0, pCex->iFrame, vSimInfo );
+    for ( f = pCex->iFrame; f >= 0; f-- )
+    {
+        Saig_ManSetAndDriveImplications_rec( p, Aig_ManConst1(p), f, pCex->iFrame, vSimInfo );
+        for ( i = 0; i < iFirstFlopPi; i++ )
+            Saig_ManSetAndDriveImplications_rec( p, Aig_ManPi(p, i), f, pCex->iFrame, vSimInfo );
+    }
+    // recursively compute justification
+    Saig_ManExplorePaths_rec( p, Aig_ManPo(p, pCex->iPo), pCex->iFrame, pCex->iFrame, vSimInfo );
+
+    // create CEX
+    pCare = Abc_CexDup( pCex, pCex->nRegs );
+    memset( pCare->pData, 0, sizeof(unsigned) * Aig_BitWordNum(pCare->nBits) );
+
+    // select the result
+    vRes = Vec_IntAlloc( 1000 );
+    vResInv = Vec_IntAlloc( 1000 );
+    for ( i = iFirstFlopPi; i < Saig_ManPiNum(p); i++ )
+    {
+        int fFound = 0;
+        for ( f = pCex->iFrame; f >= 0; f-- )
+        {
+            Value = Saig_ManSimInfo2Get( vSimInfo, Aig_ManPi(p, i), f );
+            if ( Saig_ManSimInfo2IsOld( Value ) )
+            {
+                fFound = 1;
+                Aig_InfoSetBit( pCare->pData, pCare->nRegs + pCare->nPis * f + i );
+            }
+        }
+        if ( fFound )
+            Vec_IntPush( vRes, i );
+        else
+            Vec_IntPush( vResInv, i );
+    }
+    // resimulate to make sure it is valid
+    Value = Saig_ManSimDataInit( p, pCex, vSimInfo, vResInv );
+    assert( Value == SAIG_ONE );
+    Vec_IntFree( vResInv );
+    Vec_IntFree( vRes );
+
+    return pCare;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the array of PIs for flops that should not be absracted.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Saig_ManFindCexCareBitsSense( Aig_Man_t * p, Abc_Cex_t * pCex, int iFirstFlopPi, int fVerbose )
+{
+    Abc_Cex_t * pCare;
+    Vec_Ptr_t * vSimInfo;
+    int clk;
+    if ( Saig_ManPiNum(p) != pCex->nPis )
+    {
+        printf( "Saig_ManExtendCounterExampleTest2(): The PI count of AIG (%d) does not match that of cex (%d).\n", 
+            Aig_ManPiNum(p), pCex->nPis );
+        return NULL;
+    }
+    Aig_ManFanoutStart( p );
+    vSimInfo = Vec_PtrAllocSimInfo( Aig_ManObjNumMax(p), Aig_BitWordNum(2*(pCex->iFrame+1)) );
+    Vec_PtrCleanSimInfo( vSimInfo, 0, Aig_BitWordNum(2*(pCex->iFrame+1)) );
+
+clk = clock();
+    pCare = Saig_ManDeriveCex( p, iFirstFlopPi, pCex, vSimInfo, fVerbose );
+    if ( fVerbose )
+    {
+//        printf( "Total new PIs = %3d. Non-removable PIs = %3d.  ", Saig_ManPiNum(p)-iFirstFlopPi, Vec_IntSize(vRes) );
+Abc_CexPrintStats( pCex );
+Abc_CexPrintStats( pCare );
+ABC_PRT( "Time", clock() - clk );
+    }
+
+    Vec_PtrFree( vSimInfo );
+    Aig_ManFanoutStop( p );
+    return pCare;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index aa6ec83c..581af654 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8626,11 +8626,13 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nLeafMax     = 10;
     int nDivMax      = 50;
     int nDecMax      =  3;
+    int fNewAlgo     =  0;
+    int fNewOrder    =  0;
     int fVerbose     =  0;
     int fVeryVerbose =  0;
     int c;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CKDNvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CKDNaovwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -8678,6 +8680,12 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nDecMax < 0 ) 
                 goto usage;
             break;
+        case 'a':
+            fNewAlgo ^= 1;
+            break;
+        case 'o':
+            fNewOrder ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -8770,7 +8778,10 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         Abc_Cex_t * pNew;
         Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
-        pNew = Saig_ManFindCexCareBits( pAig, pAbc->pCex, 0, 0 );
+        if ( fNewAlgo )
+            pNew = Saig_ManFindCexCareBitsSense( pAig, pAbc->pCex, 0, fVerbose );
+        else
+            pNew = Saig_ManFindCexCareBits( pAig, pAbc->pCex, 0, fNewOrder, fVerbose );
         Aig_ManStop( pAig );
         Abc_FrameReplaceCex( pAbc, &pNew );
     }
@@ -8779,12 +8790,14 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     return 0;
 usage:
-    Abc_Print( -2, "usage: test [-CKDN] [-vwh] <file_name>\n" );
+    Abc_Print( -2, "usage: test [-CKDN] [-aovwh] <file_name>\n" );
     Abc_Print( -2, "\t         testbench for new procedures\n" );
     Abc_Print( -2, "\t-C num : the max number of cuts [default = %d]\n", nCutMax );
     Abc_Print( -2, "\t-K num : the max number of leaves [default = %d]\n", nLeafMax );
     Abc_Print( -2, "\t-D num : the max number of divisors [default = %d]\n", nDivMax );
     Abc_Print( -2, "\t-N num : the max number of node inputs [default = %d]\n", nDecMax );
+    Abc_Print( -2, "\t-a     : toggle using new algorithm [default = %s]\n", fNewAlgo? "yes": "no" );
+    Abc_Print( -2, "\t-o     : toggle using new ordering [default = %s]\n", fNewOrder? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing very verbose information [default = %s]\n", fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");