Better CEX minimization and renaming of write_counter into write_cex.

8 files changed, 366 insertions, 14 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 555e24cf..18348add 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -1423,6 +1423,10 @@ SOURCE=.\src\sat\bmc\bmcBmci.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\sat\bmc\bmcCexCare.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\sat\bmc\bmcCexCut.c
 # End Source File
 # Begin Source File
diff --git a/src/base/io/io.c b/src/base/io/io.c
index ef17c8fd..3e969915 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -22,6 +22,7 @@
 #include "base/main/mainInt.h"
 #include "aig/saig/saig.h"
 #include "proof/abs/abs.h"
+#include "sat/bmc/bmc.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -60,7 +61,7 @@ static int IoCommandWriteBook   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteCellNet( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteCnf    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteCnf2   ( Abc_Frame_t * pAbc, int argc, char **argv );
-static int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteCex    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteDot    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteEqn    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteGml    ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -124,7 +125,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "write_bench",   IoCommandWriteBench,   0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_book",    IoCommandWriteBook,    0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_cellnet", IoCommandWriteCellNet, 0 );
-    Cmd_CommandAdd( pAbc, "I/O", "write_counter", IoCommandWriteCounter, 0 );
+    Cmd_CommandAdd( pAbc, "I/O", "write_cex",     IoCommandWriteCex,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_cnf",     IoCommandWriteCnf,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "&write_cnf",    IoCommandWriteCnf2,    0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_dot",     IoCommandWriteDot,     0 );
@@ -2171,18 +2172,20 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
-int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
+int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
 {
     Abc_Ntk_t * pNtk;
     char * pFileName;
     int c, fNames  = 0;
     int fMinimize  = 0;
+    int fUseOldMin = 0;
+    int fCheckCex  = 0;
     int forceSeq   = 0;
     int fPrintFull = 0;
     int fVerbose   = 0;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "snmfvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "snmocfvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2195,6 +2198,12 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
             case 'm':
                 fMinimize ^= 1;
                 break;
+            case 'o':
+                fUseOldMin ^= 1;
+                break;
+            case 'c':
+                fCheckCex ^= 1;
+                break;
             case 'f':
                 fPrintFull ^= 1;
                 break;
@@ -2236,7 +2245,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
         Abc_NtkForEachLatch( pNtk, pObj, i )
             if ( !Abc_LatchIsInit0(pObj) )
             {
-                fprintf( stdout, "IoCommandWriteCounter(): The init-state should be all-0 for counter-example to work.\n" );
+                fprintf( stdout, "IoCommandWriteCex(): The init-state should be all-0 for counter-example to work.\n" );
                 fprintf( stdout, "Run commands \"undc\" and \"zero\" and then rerun the equivalence check.\n" );
                 return 1;
             }
@@ -2244,7 +2253,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
         pFile = fopen( pFileName, "w" );
         if ( pFile == NULL )
         {
-            fprintf( stdout, "IoCommandWriteCounter(): Cannot open the output file \"%s\".\n", pFileName );
+            fprintf( stdout, "IoCommandWriteCex(): Cannot open the output file \"%s\".\n", pFileName );
             return 1;
         }
         if ( fPrintFull )
@@ -2267,9 +2276,14 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
             {
                 extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
                 Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
-                pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, 0, fVerbose );
-                if ( pCare == NULL )
-                    printf( "Counter-example minimization has failed.\n" );
+                if ( fUseOldMin )
+                {
+                    pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, 0, fVerbose );
+                    if ( fCheckCex )
+                        Bmc_CexCareVerify( pAig, pCex, pCare, fVerbose );
+                }
+                else
+                    pCare = Bmc_CexCareMinimize( pAig, pCex, fCheckCex, fVerbose );
                 Aig_ManStop( pAig );
             }
             // output flop values (unaffected by the minimization)
@@ -2299,7 +2313,7 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
         int i;
         if ( pFile == NULL )
         {
-            fprintf( stdout, "IoCommandWriteCounter(): Cannot open the output file \"%s\".\n", pFileName );
+            fprintf( stdout, "IoCommandWriteCex(): Cannot open the output file \"%s\".\n", pFileName );
             return 1;
         }
         if ( fNames )
@@ -2321,12 +2335,14 @@ int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_counter [-snmfvh] <file>\n" );
+    fprintf( pAbc->Err, "usage: write_cex [-snmocfvh] <file>\n" );
     fprintf( pAbc->Err, "\t         saves counter-example derived by \"sat\", \"iprove\", or \"dprove\"\n" );
     fprintf( pAbc->Err, "\t         the file contains values for each PI in the natural order\n" );
     fprintf( pAbc->Err, "\t-s     : always report a sequential ctrex (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" );
     fprintf( pAbc->Err, "\t-n     : write input names into the file [default = %s]\n", fNames? "yes": "no" );
     fprintf( pAbc->Err, "\t-m     : minimize counter-example by dropping don't-care values [default = %s]\n", fMinimize? "yes": "no" );
+    fprintf( pAbc->Err, "\t-o     : use old counter-example minimization algorithm [default = %s]\n", fUseOldMin? "yes": "no" );
+    fprintf( pAbc->Err, "\t-c     : check generated counter-example using ternary simulation [default = %s]\n", fCheckCex? "yes": "no" );
     fprintf( pAbc->Err, "\t-f     : enable printing flop values in each timeframe [default = %s].\n", fPrintFull? "yes": "no" );  
     fprintf( pAbc->Err, "\t-v     : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );  
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
@@ -2334,7 +2350,6 @@ usage:
     return 1;
 }
 
-
 /**Function*************************************************************
 
   Synopsis    []
diff --git a/src/misc/util/utilCex.c b/src/misc/util/utilCex.c
index 1399f55d..2f2901e0 100644
--- a/src/misc/util/utilCex.c
+++ b/src/misc/util/utilCex.c
@@ -488,6 +488,33 @@ Abc_Cex_t * Abc_CexPermuteTwo( Abc_Cex_t * p, Vec_Int_t * vPermOld, Vec_Int_t *
     return pCex;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Count the number of 1s in the CEX.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Abc_CexOnes32( unsigned i )
+{
+    i = i - ((i >> 1) & 0x55555555);
+    i = (i & 0x33333333) + ((i >> 2) & 0x33333333);
+    i = ((i + (i >> 4)) & 0x0F0F0F0F);
+    return (i*(0x01010101))>>24;
+}
+int Abc_CexCountOnes( Abc_Cex_t * p )
+{
+    int nWords = Abc_BitWordNum( p->nBits );
+    int i, Count = 0;
+    for ( i = 0; i < nWords; i++ )
+        Count += Abc_CexOnes32( p->pData[i] );
+    return Count;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/util/utilCex.h b/src/misc/util/utilCex.h
index 98463410..c6904a60 100644
--- a/src/misc/util/utilCex.h
+++ b/src/misc/util/utilCex.h
@@ -72,6 +72,7 @@ extern Abc_Cex_t *   Abc_CexTransformPhase( Abc_Cex_t * p, int nPisOld, int nPos
 extern Abc_Cex_t *   Abc_CexTransformTempor( Abc_Cex_t * p, int nPisOld, int nPosOld, int nRegsOld );
 extern Abc_Cex_t *   Abc_CexPermute( Abc_Cex_t * p, Vec_Int_t * vMapOld2New );
 extern Abc_Cex_t *   Abc_CexPermuteTwo( Abc_Cex_t * p, Vec_Int_t * vPermOld, Vec_Int_t * vPermNew );
+extern int           Abc_CexCountOnes( Abc_Cex_t * p );
 
 ABC_NAMESPACE_HEADER_END
 
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 0bc7bb3f..3eeeb7b5 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -126,11 +126,17 @@ extern void              Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
 extern int               Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
 /*=== bmcBmcAnd.c ==========================================================*/
 extern int               Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars );
+/*=== bmcCexCare.c ==========================================================*/
+extern Abc_Cex_t *       Bmc_CexCareMinimize( Aig_Man_t * p, Abc_Cex_t * pCex, 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 );
 extern Aig_Man_t *       Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
 /*=== bmcCexMin.c ==========================================================*/
 extern Abc_Cex_t *       Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
+/*=== bmcCexTool.c ==========================================================*/
+extern void              Bmc_CexPrint( Abc_Cex_t * pCex, int nInputs, int fVerbose );
+extern int               Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
 /*=== bmcICheck.c ==========================================================*/
 extern void              Bmc_PerformICheck( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fEmpty, int fVerbose );
 extern Vec_Int_t *       Bmc_PerformISearch( Gia_Man_t * p, int nFramesMax, int nTimeOut, int fReverse, int fDump, int fVerbose );
diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c
new file mode 100644
index 00000000..addb89fd
--- /dev/null
+++ b/src/sat/bmc/bmcCexCare.c
@@ -0,0 +1,298 @@
+/**CFile****************************************************************
+
+  FileName    [bmcCexCare.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    [Computing care set of the counter-example.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmcCexCare.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bmc.h"
+#include "aig/gia/giaAig.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Backward propagation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bmc_CexCarePropagateFwdOne( Gia_Man_t * p, Abc_Cex_t * pCex, int f, int fGrow )
+{
+    Gia_Obj_t * pObj;
+    int Prio, Prio0, Prio1;
+    int i, Phase0, Phase1;
+    if ( (fGrow & 2) )
+    {
+        Gia_ManForEachPi( p, pObj, i )
+            pObj->Value = Abc_Var2Lit( f * pCex->nPis + (pCex->nPis-1-i) + 1, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) );
+    }
+    else
+    {
+        Gia_ManForEachPi( p, pObj, i )
+            pObj->Value = Abc_Var2Lit( f * pCex->nPis + i + 1, Abc_InfoHasBit(pCex->pData, pCex->nRegs + pCex->nPis * f + i) );
+    }
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        Prio0  = Abc_Lit2Var(Gia_ObjFanin0(pObj)->Value);
+        Prio1  = Abc_Lit2Var(Gia_ObjFanin1(pObj)->Value);
+        Phase0 = Abc_LitIsCompl(Gia_ObjFanin0(pObj)->Value) ^ Gia_ObjFaninC0(pObj);
+        Phase1 = Abc_LitIsCompl(Gia_ObjFanin1(pObj)->Value) ^ Gia_ObjFaninC1(pObj);
+        if ( Phase0 && Phase1 )
+            Prio = (fGrow & 1) ? Abc_MinInt(Prio0, Prio1) : Abc_MaxInt(Prio0, Prio1);
+        else if ( Phase0 && !Phase1 )
+            Prio = Prio1;
+        else if ( !Phase0 && Phase1 )
+            Prio = Prio0;
+        else // if ( !Phase0 && !Phase1 )
+            Prio = (fGrow & 1) ? Abc_MaxInt(Prio0, Prio1) : Abc_MinInt(Prio0, Prio1);
+        pObj->Value = Abc_Var2Lit( Prio, Phase0 & Phase1 );
+    }
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->Value = Abc_LitNotCond( Gia_ObjFanin0(pObj)->Value, Gia_ObjFaninC0(pObj) );
+}
+void Bmc_CexCarePropagateFwd( Gia_Man_t * p, Abc_Cex_t * pCex, int fGrow, Vec_Int_t * vPrios )
+{
+    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+    int f, i;
+    Gia_ManConst0( p )->Value = 0;
+    Gia_ManForEachRi( p, pObj, i )
+        pObj->Value = 0;
+    Vec_IntClear( vPrios );
+    for ( f = 0; f <= pCex->iFrame; f++ )
+    {
+        Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
+            Vec_IntPush( vPrios, (pObjRo->Value = pObjRi->Value) );
+        Bmc_CexCarePropagateFwdOne( p, pCex, f, fGrow );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Forward propagation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bmc_CexCarePropagateBwdOne( Gia_Man_t * p, Abc_Cex_t * pCex, int f, Abc_Cex_t * pCexMin )
+{
+    Gia_Obj_t * pObj;
+    int i, Phase0, Phase1;
+    Gia_ManForEachCand( p, pObj, i )
+        pObj->fPhase = 0;
+    Gia_ManForEachCo( p, pObj, i )
+        if ( pObj->fPhase )
+            Gia_ObjFanin0(pObj)->fPhase = 1;
+    Gia_ManForEachAndReverse( p, pObj, i )
+    {
+        if ( !pObj->fPhase )
+            continue;
+        Phase0 = Abc_LitIsCompl(Gia_ObjFanin0(pObj)->Value) ^ Gia_ObjFaninC0(pObj);
+        Phase1 = Abc_LitIsCompl(Gia_ObjFanin1(pObj)->Value) ^ Gia_ObjFaninC1(pObj);
+        if ( Phase0 && Phase1 )
+        {
+            Gia_ObjFanin0(pObj)->fPhase = 1;
+            Gia_ObjFanin1(pObj)->fPhase = 1;
+        }
+        else if ( Phase0 && !Phase1 )
+            Gia_ObjFanin1(pObj)->fPhase = 1;
+        else if ( !Phase0 && Phase1 )
+            Gia_ObjFanin0(pObj)->fPhase = 1;
+        else // if ( !Phase0 && !Phase1 )
+        {
+            if ( Abc_Lit2Var(Gia_ObjFanin0(pObj)->Value) <= Abc_Lit2Var(Gia_ObjFanin1(pObj)->Value) )
+                Gia_ObjFanin0(pObj)->fPhase = 1;
+            else
+                Gia_ObjFanin1(pObj)->fPhase = 1;
+        }
+    }
+    Gia_ManForEachPi( p, pObj, i )
+        if ( pObj->fPhase )
+            Abc_InfoSetBit( pCexMin->pData, pCexMin->nRegs + pCexMin->nPis * f + i );
+}
+Abc_Cex_t * Bmc_CexCarePropagateBwd( Gia_Man_t * p, Abc_Cex_t * pCex, Vec_Int_t * vPrios, int fGrow )
+{
+    Abc_Cex_t * pCexMin;
+    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+    int f, i;
+    pCexMin = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 );
+    pCexMin->iPo    = pCex->iPo;
+    pCexMin->iFrame = pCex->iFrame;
+    Gia_ManForEachCo( p, pObj, i )
+        pObj->fPhase = 0;
+    for ( f = pCex->iFrame; f >= 0; f-- )
+    {
+        Gia_ManPo(p, pCex->iPo)->fPhase = (int)(f == pCex->iFrame);
+        Gia_ManForEachRo( p, pObj, i )
+            pObj->Value = Vec_IntEntry( vPrios, f * pCex->nRegs + i );
+        Bmc_CexCarePropagateFwdOne( p, pCex, f, fGrow );
+        Bmc_CexCarePropagateBwdOne( p, pCex, f, pCexMin );
+        Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
+            pObjRi->fPhase = pObjRo->fPhase;
+    }
+    return pCexMin;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the care set of the counter-example.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Bmc_CexCareMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int fCheck, int fVerbose )
+{
+    int nTryCexes = 4; // belongs to range [1;4]
+    Abc_Cex_t * pCexBest, * pCexMin[4] = {NULL};
+    int k, nOnesBest, nOnesCur;
+    Vec_Int_t * vPrios;
+    if ( pCex->nPis != Gia_ManPiNum(p) )
+    {
+        printf( "Given CEX does to have same number of inputs as the AIG.\n" );
+        return NULL;
+    }
+    if ( pCex->nRegs != Gia_ManRegNum(p) )
+    {
+        printf( "Given CEX does to have same number of flops as the AIG.\n" );
+        return NULL;
+    }
+    if ( !(pCex->iPo >= 0 && pCex->iPo < Gia_ManPoNum(p)) )
+    {
+        printf( "Given CEX has PO whose index is out of range for the AIG.\n" );
+        return NULL;
+    }
+    assert( pCex->nPis == Gia_ManPiNum(p) );
+    assert( pCex->nRegs == Gia_ManRegNum(p) );
+    assert( pCex->iPo >= 0 && pCex->iPo < Gia_ManPoNum(p) );
+    if ( fVerbose )
+    {
+        printf( "Original :    " );
+        Bmc_CexPrint( pCex, Gia_ManPiNum(p), 0 );
+    }
+    vPrios = Vec_IntAlloc( pCex->nRegs * (pCex->iFrame + 1) );
+    for ( k = 0; k < nTryCexes; k++ )
+    {
+        Bmc_CexCarePropagateFwd(p, pCex, k, vPrios );
+        assert( Vec_IntSize(vPrios) == pCex->nRegs * (pCex->iFrame + 1) );
+        if ( !Abc_LitIsCompl(Gia_ManPo(p, pCex->iPo)->Value) )
+        {
+            printf( "Counter-example is invalid.\n" );
+            Vec_IntFree( vPrios );
+            return NULL;
+        }
+        pCexMin[k] = Bmc_CexCarePropagateBwd( p, pCex, vPrios, k );
+        if ( fVerbose )
+        {
+            if ( (k & 1) )
+                printf( "Decrease :    " );
+            else
+                printf( "Increase :    " );
+            Bmc_CexPrint( pCexMin[k], Gia_ManPiNum(p), 0 );
+        }
+    }
+    Vec_IntFree( vPrios );
+    // select the best one
+    pCexBest  = pCexMin[0];
+    nOnesBest = Abc_CexCountOnes(pCexMin[0]);
+    for ( k = 1; k < nTryCexes; k++ )
+    {
+        nOnesCur = Abc_CexCountOnes(pCexMin[k]);
+        if ( nOnesBest > nOnesCur )
+        {
+            nOnesBest = nOnesCur;
+            pCexBest  = pCexMin[k];
+        }
+    }
+    for ( k = 0; k < nTryCexes; k++ )
+        if ( pCexBest != pCexMin[k] )
+            Abc_CexFreeP( &pCexMin[k] );
+    // verify and return
+    if ( fVerbose )
+    {
+        printf( "Final    :    " );
+        Bmc_CexPrint( pCexBest, Gia_ManPiNum(p), 0 );
+    }
+    if ( !Bmc_CexVerify( p, pCex, pCexBest ) )
+        printf( "Counter-example verification has failed.\n" );
+    else if ( fCheck ) 
+        printf( "Counter-example verification succeeded.\n" );
+    return pCexBest;
+}
+Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, Abc_Cex_t * pCex, int fCheck, int fVerbose )
+{
+    Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
+    Abc_Cex_t * pCexMin = Bmc_CexCareMinimizeAig( pGia, pCex, fCheck, fVerbose );
+    Gia_ManStop( pGia );
+    return pCexMin;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Verifies the care set of the counter-example.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )
+{
+    Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
+    if ( fVerbose )
+    {
+        printf( "Original :    " );
+        Bmc_CexPrint( pCex, Gia_ManPiNum(pGia), 0 );
+        printf( "Minimized:    " );
+        Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 );
+    }
+    if ( !Bmc_CexVerify( pGia, pCex, pCexMin ) )
+        printf( "Counter-example verification has failed.\n" );
+    else 
+        printf( "Counter-example verification succeeded.\n" );
+    Gia_ManStop( pGia );
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c
index 811a90b7..05dade97 100644
--- a/src/sat/bmc/bmcCexTools.c
+++ b/src/sat/bmc/bmcCexTools.c
@@ -348,7 +348,7 @@ int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
     Gia_Obj_t * pObj;
     int i, k;
     assert( pCex->nRegs > 0 );
-    assert( pCexCare->nRegs == 0 );
+//    assert( pCexCare->nRegs == 0 );
     Gia_ObjTerSimSet0( Gia_ManConst0(p) );
     Gia_ManForEachRi( p, pObj, k )
         Gia_ObjTerSimSet0( pObj );
@@ -356,7 +356,7 @@ int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
     {
         Gia_ManForEachPi( p, pObj, k )
         {
-            if ( !Abc_InfoHasBit( pCexCare->pData, i * pCexCare->nPis + k ) )
+            if ( !Abc_InfoHasBit( pCexCare->pData, pCexCare->nRegs + i * pCexCare->nPis + k ) )
                 Gia_ObjTerSimSetX( pObj );
             else if ( Abc_InfoHasBit( pCex->pData, pCex->nRegs + i * pCex->nPis + k ) )
                 Gia_ObjTerSimSet1( pObj );
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index 3ff4b100..6deb9eb1 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -3,6 +3,7 @@ SRC +=    src/sat/bmc/bmcBmc.c \
     src/sat/bmc/bmcBmc3.c \
     src/sat/bmc/bmcBmcAnd.c \
     src/sat/bmc/bmcBmci.c \
+    src/sat/bmc/bmcCexCare.c \
     src/sat/bmc/bmcCexCut.c \
     src/sat/bmc/bmcCexDepth.c \
     src/sat/bmc/bmcCexMin1.c \