diff --git a/src/base/io/io.c b/src/base/io/io.c
index fa7a961a5..8f805d639 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -44,6 +44,7 @@ static int IoCommandReadBblif   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadBlif    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadBlifMv  ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadBench   ( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandReadCex     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadDsd     ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadEdif    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandReadEqn     ( Abc_Frame_t * pAbc, int argc, char **argv );
@@ -116,6 +117,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "read_blif",     IoCommandReadBlif,     1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_blif_mv",  IoCommandReadBlifMv,   1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_bench",    IoCommandReadBench,    1 );
+    Cmd_CommandAdd( pAbc, "I/O", "read_cex",      IoCommandReadCex,      1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_dsd",      IoCommandReadDsd,      1 );
     Cmd_CommandAdd( pAbc, "I/O", "read_formula",  IoCommandReadDsd,      1 );
 //    Cmd_CommandAdd( pAbc, "I/O", "read_edif",     IoCommandReadEdif,     1 );
@@ -686,6 +688,331 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkReadCexFile( char * pFileName, Abc_Ntk_t * pNtk, Abc_Cex_t ** ppCex, Abc_Cex_t ** ppCexCare, int * pnFrames, int * fOldFormat, int xMode )
+{
+    FILE * pFile;
+    Abc_Cex_t * pCex;
+    Abc_Cex_t * pCexCare;
+    Vec_Int_t * vNums;
+    int c, nRegs = -1, nFrames = -1;
+    pFile = fopen( pFileName, "r" );
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open log file for reading \"%s\".\n" , pFileName );
+        return -1;
+    }
+
+    vNums = Vec_IntAlloc( 100 );
+    int usedX = 0;
+    *fOldFormat = 0;
+    
+    int MaxLine = 1000000;
+    char *Buffer;
+    int BufferLen = 0;
+    int state = 0;
+    int iPo = 0;
+    nFrames = -1;
+    int status = 0;
+    int i;
+    int nRegsNtk = 0;
+    Abc_Obj_t * pObj;
+    Abc_NtkForEachLatch( pNtk, pObj, i ) nRegsNtk++;
+
+    Buffer = ABC_ALLOC( char, MaxLine );
+    while ( fgets( Buffer, MaxLine, pFile ) != NULL )
+    {
+        if ( Buffer[0] == '#' || Buffer[0] == 'c' || Buffer[0] == 'f' || Buffer[0] == 'u' )
+            continue;
+        BufferLen = strlen(Buffer) - 1;
+        Buffer[BufferLen] = '\0';
+        if (state==0 && BufferLen>1) {
+            // old format detected
+            *fOldFormat = 1;
+            state = 2;
+            iPo = 0;
+            status = 1;
+        }
+        if (state==1 && Buffer[0]!='b' && Buffer[0]!='j') {
+            // old format detected, first line was actually register
+            *fOldFormat = 1;
+            state = 3;
+            Vec_IntPush( vNums, status );
+            status = 1;
+        }
+        if (Buffer[0] == '.' )
+            break;
+        switch(state) {
+            case 0 :
+                {
+                    char c = Buffer[0];
+                    if ( c == '0' || c == '1' || c == '2' ) {
+                        status = c - '0' ;
+                        state = 1;
+                    } else if ( c == 'x' ) {
+                        // old format with one x state latch
+                        usedX = 1;
+                        // set to 2 so we can Abc_LatchSetInitNone
+                        // acts like 0 when setting bits
+                        Vec_IntPush( vNums, 2 );
+                        nRegs = Vec_IntSize(vNums);
+                        state = 3;
+                    } else {
+                        printf( "ERROR: Bad aiger status line.\n" );
+                        return -1;
+                    }
+                }
+                break;
+            case 1 :
+                iPo = atoi(Buffer+1);
+                state = 2;
+                break;
+            case 2 :
+                for (i=0; i<BufferLen;i++) {
+                    char c = Buffer[i];
+                    if ( c == '0' || c == '1' )
+                        Vec_IntPush( vNums, c - '0' );
+                    else if ( c == 'x') {
+                        usedX = 1;
+                        // set to 2 so we can Abc_LatchSetInitNone
+                        // acts like 0 when setting bits
+                        Vec_IntPush( vNums, 2 );
+                    }
+                }
+                nRegs = Vec_IntSize(vNums);
+                if ( nRegs < nRegsNtk )
+                {
+                    printf( "WARNING: Register number is smaller than in Ntk. Appending.\n" );
+                    for (i=0; i<nRegsNtk-nRegs;i++) {
+                        Vec_IntPush( vNums, 0 );
+                    }
+                    nRegs = Vec_IntSize(vNums);
+                }
+                else if ( nRegs > nRegsNtk )
+                {
+                    printf( "WARNING: Register number is larger than in Ntk. Truncating.\n" );
+                    Vec_IntShrink( vNums, nRegsNtk );
+                    nRegs = nRegsNtk;
+                }
+                state = 3;
+                break;
+            default:
+                for (i=0; i<BufferLen;i++) {
+                    char c = Buffer[i];
+                    if ( c == '0' || c == '1' )
+                        Vec_IntPush( vNums, c - '0' );
+                    else if ( c == 'x') {
+                        usedX = 1;
+                        Vec_IntPush( vNums, 2 );
+                    }
+                }
+                nFrames++;
+                break;
+        }
+    }
+    fclose( pFile );
+
+    if (usedX && !xMode)
+        printf( "Warning: Using 0 instead of x in latches or primary inputs\n" );
+    int iFrameCex = nFrames;
+    if ( nRegs < 0 )
+    {
+        if (status == 0 || *fOldFormat == 0)
+            printf( "Counter-example is not available.\n" );
+        else
+            printf( "ERROR: Cannot read register number.\n" );
+        Vec_IntFree( vNums );
+        return -1;
+    }
+    if ( nRegs != nRegsNtk )
+    {
+        printf( "ERROR: Register number not coresponding to Ntk.\n" );
+        Vec_IntFree( vNums );
+        return -1;
+    }
+    if ( Vec_IntSize(vNums)-nRegs == 0 )
+    {
+        printf( "ERROR: Cannot read counter example.\n" );
+        Vec_IntFree( vNums );
+        return -1;
+    }
+    if ( (Vec_IntSize(vNums)-nRegs) % (iFrameCex + 1) != 0 )
+    {
+        printf( "ERROR: Incorrect number of bits.\n" );
+        Vec_IntFree( vNums );
+        return -1;
+    }
+    int nPi = (Vec_IntSize(vNums)-nRegs)/(iFrameCex + 1);
+    if ( nPi != Abc_NtkPiNum(pNtk) )
+    {
+        printf( "ERROR: Number of primary inputs not coresponding to Ntk.\n" );
+        Vec_IntFree( vNums );
+        return -1;
+    }
+    if ( iPo >= Abc_NtkPoNum(pNtk) )
+    {
+        printf( "WARNING: PO that failed verification not coresponding to Ntk, using first PO instead.\n" );
+        iPo = 0;
+    }
+    Abc_NtkForEachLatch( pNtk, pObj, i ) {
+        if ( Vec_IntEntry(vNums, i) == 1 )
+            Abc_LatchSetInit1(pObj);
+        else if ( Vec_IntEntry(vNums, i) == 2 && xMode )
+            Abc_LatchSetInitNone(pObj);
+        else
+            Abc_LatchSetInit0(pObj);
+    }
+
+    pCex = Abc_CexAlloc( nRegs, nPi, iFrameCex + 1 );
+    pCexCare = Abc_CexAlloc( nRegs, nPi, iFrameCex + 1);
+    // the zero-based number of PO, for which verification failed
+    // fails in Bmc_CexVerify if not less than actual number of PO
+    pCex->iPo    = iPo;
+    pCexCare->iPo = iPo;
+    // the zero-based number of the time-frame, for which verificaiton failed
+    pCex->iFrame = iFrameCex;
+    pCexCare->iFrame = iFrameCex;
+    assert( Vec_IntSize(vNums) == pCex->nBits );
+    for ( c = 0; c < pCex->nBits; c++ ) {
+        if ( Vec_IntEntry(vNums, c) == 1)
+        {
+            Abc_InfoSetBit( pCex->pData, c );
+            Abc_InfoSetBit( pCexCare->pData, c );
+        }
+        else if ( Vec_IntEntry(vNums, c) == 2 && xMode )
+        {
+            // nothing to set
+        }
+        else
+            Abc_InfoSetBit( pCexCare->pData, c );
+    }
+
+    Vec_IntFree( vNums );
+    Abc_CexFreeP( ppCex );
+    if ( ppCex )
+        *ppCex = pCex;
+    else
+        Abc_CexFree( pCex );
+    Abc_CexFreeP( ppCexCare );
+    if ( ppCexCare )
+        *ppCexCare = pCexCare;
+    else
+        Abc_CexFree( pCexCare );
+
+    if ( pnFrames )
+        *pnFrames = nFrames;
+    return status;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+int IoCommandReadCex( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Abc_Ntk_t * pNtk;
+    Abc_Cex_t * pCex = NULL;
+    Abc_Cex_t * pCexCare = NULL;
+    char * pFileName;
+    FILE * pFile;
+    int fCheck = 1;
+    int fXMode = 0;
+    int c;
+    int fOldFormat = 0;
+    int verified;
+
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cxh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'c':
+                fCheck ^= 1;
+                break;
+            case 'x':
+                fXMode ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+    if ( argc != globalUtilOptind + 1 )
+        goto usage;
+
+    // get the input file name
+    pFileName = argv[globalUtilOptind];
+    if ( (pFile = fopen( pFileName, "r" )) == NULL )
+    {
+        fprintf( pAbc->Err, "Cannot open input file \"%s\". \n", pFileName );
+        return 1;
+    }
+    fclose( pFile );
+
+    pNtk = pAbc->pNtkCur;
+    if ( pNtk == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
+    Abc_FrameClearVerifStatus( pAbc );
+    pAbc->Status = Abc_NtkReadCexFile( pFileName, pNtk, &pCex, &pCexCare, &pAbc->nFrames, &fOldFormat, fXMode);
+    if ( fOldFormat && !fCheck )
+        printf( "WARNING: Old witness format detected and checking is disabled. Reading might have failed.\n" );
+
+    if ( fCheck && pAbc->Status==1) {
+        extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
+        Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
+
+        verified = Bmc_CexCareVerify( pAig, pCex, pCexCare, false );
+        if (!verified)
+        {
+            printf( "Checking CEX for any PO.\n" );
+            int verified = Bmc_CexCareVerifyAnyPo( pAig, pCex, pCexCare, false );
+            Aig_ManStop( pAig );
+            if (verified < 0)
+            {
+                Abc_CexFreeP(&pCex);
+                Abc_CexFreeP(&pCexCare);
+                return 1;
+            }
+            pAbc->pCex->iPo = verified;
+        }
+
+        Abc_CexFreeP(&pCexCare);
+        Abc_FrameReplaceCex( pAbc, &pCex );
+    }
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: read_cex [-ch] <file>\n" );
+    fprintf( pAbc->Err, "\t         reads the witness cex\n" );
+    fprintf( pAbc->Err, "\t-c     : toggle check after reading [default = %s]\n", fCheck? "yes":"no" );
+    fprintf( pAbc->Err, "\t-x     : read x bits for verification [default = %s]\n", fXMode? "yes":"no" );
+    fprintf( pAbc->Err, "\t-h     : prints the command summary\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of a file to read\n" );
+    return 1;
+}
 /**Function*************************************************************
 
   Synopsis    []
@@ -2549,10 +2876,15 @@ void Abc_NtkDumpOneCexSpecial( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex
 }
 
 
+extern Abc_Cex_t * Bmc_CexInnerStates( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t ** ppCexImpl, int fVerbose );
+extern Abc_Cex_t * Bmc_CexEssentialBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexCare, int fVerbose );
+extern Abc_Cex_t * Bmc_CexCareBits( Gia_Man_t * p, Abc_Cex_t * pCexState, Abc_Cex_t * pCexImpl, Abc_Cex_t * pCexEss, int fFindAll, int fVerbose );
+
 void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex, 
-    int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin, 
-    int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose )
+    int fPrintFull, int fNames, int fUseFfNames, int fMinimize, int fUseOldMin, int fCexInfo,
+    int fCheckCex, int fUseSatBased, int fHighEffort, int fAiger, int fVerbose, int fExtended )
 {
+    Abc_Cex_t * pCare = NULL;
     Abc_Obj_t * pObj;
     int i, f;
     if ( fPrintFull )
@@ -2568,15 +2900,17 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex,
                 fprintf( pFile, "%s@%d=%c ", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCexFull->pData, Abc_NtkCiNum(pNtk)*f + i) );
         Abc_CexFreeP( &pCexFull );
     }
-    else if ( fNames )
+    else
     {
-        Abc_Cex_t * pCare = NULL;
+        if ( fNames )
+        {
+            fprintf( pFile, "# FALSIFYING OUTPUTS:");
+            fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) );
+        }
         if ( fMinimize )
         {
             extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
             Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 1 );
-            fprintf( pFile, "# FALSIFYING OUTPUTS:");                                       
-            fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) ); 
             if ( fUseOldMin )
             {
                 pCare = Saig_ManCbaFindCexCareBits( pAig, pCex, 0, fVerbose );
@@ -2584,21 +2918,47 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex,
                     Bmc_CexCareVerify( pAig, pCex, pCare, fVerbose );
             }
             else if ( fUseSatBased )
-                pCare = Bmc_CexCareSatBasedMinimize( pAig, Saig_ManPiNum(pAig), pCex, fHighEffort, fCheckCex, fVerbose );
+            {
+                if ( Abc_NtkPoNum( pNtk ) == 1 )
+                    pCare = Bmc_CexCareSatBasedMinimize( pAig, Saig_ManPiNum(pAig), pCex, fHighEffort, fCheckCex, fVerbose );
+                else
+                    printf( "SAT-based CEX minimization requires having a single PO.\n" );
+            }
+            else if ( fCexInfo )
+            {
+                Gia_Man_t * p = Gia_ManFromAigSimple( pAig );
+                Abc_Cex_t * pCexImpl   = NULL;
+                Abc_Cex_t * pCexStates = Bmc_CexInnerStates( p, pCex, &pCexImpl, fVerbose );
+                Abc_Cex_t * pCexCare   = Bmc_CexCareBits( p, pCexStates, pCexImpl, NULL, 1, fVerbose );
+                Abc_Cex_t * pCexEss;
+
+                if ( fCheckCex && !Bmc_CexVerify( p, pCex, pCexCare ) )
+                    printf( "Counter-example care-set verification has failed.\n" );
+
+                pCexEss = Bmc_CexEssentialBits( p, pCexStates, pCexCare, fVerbose );
+
+                // pCare is pCexMin from Bmc_CexTest
+                pCare = Bmc_CexCareBits( p, pCexStates, pCexImpl, pCexEss, 0, fVerbose );
+
+                if ( fCheckCex && !Bmc_CexVerify( p, pCex, pCare ) )
+                    printf( "Counter-example min-set verification has failed.\n" );
+                Abc_CexFreeP( &pCexStates );
+                Abc_CexFreeP( &pCexImpl );
+                Abc_CexFreeP( &pCexCare );
+                Abc_CexFreeP( &pCexEss );
+            }
             else
                 pCare = Bmc_CexCareMinimize( pAig, Saig_ManPiNum(pAig), pCex, 4, fCheckCex, fVerbose );
             Aig_ManStop( pAig );
-            if(pCare == NULL)                                           
+            if(pCare == NULL)
                 printf( "Counter-example minimization has failed.\n" ); 
         }
-        else
+        if (fNames)
         {
-            fprintf( pFile, "# FALSIFYING OUTPUTS:");                        
-            fprintf( pFile, " %s", Abc_ObjName(Abc_NtkCo(pNtk, pCex->iPo)) );
+                fprintf( pFile, "\n");
+                fprintf( pFile, "# COUNTEREXAMPLE LENGTH: %u\n", pCex->iFrame+1);
         }
-        fprintf( pFile, "\n");                                           
-        fprintf( pFile, "# COUNTEREXAMPLE LENGTH: %u\n", pCex->iFrame+1);
-        if ( fUseFfNames && Abc_NtkCheckSpecialPi(pNtk) )
+        if ( fNames && fUseFfNames && Abc_NtkCheckSpecialPi(pNtk) )
         {
             int * pValues;
             int nXValues = 0, iFlop = 0, iPivotPi = -1;
@@ -2638,29 +2998,36 @@ void Abc_NtkDumpOneCex( FILE * pFile, Abc_Ntk_t * pNtk, Abc_Cex_t * pCex,
         }
         else
         {
+            if (fExtended && fAiger && !fNames) {
+                fprintf( pFile, "1\n");
+                fprintf( pFile, "b%d\n", pCex->iPo);
+            }
             // output flop values (unaffected by the minimization)
             Abc_NtkForEachLatch( pNtk, pObj, i )
-                fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
+                if ( fNames )
+                    fprintf( pFile, "%s@0=%c\n", Abc_ObjName(Abc_ObjFanout0(pObj)), '0'+!Abc_LatchIsInit0(pObj) );
+                else
+                    fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) );
+            if ( !fNames && fAiger)
+                fprintf( pFile, "\n");
             // output PI values (while skipping the minimized ones)
-            for ( f = 0; f <= pCex->iFrame; f++ )
+            for ( f = 0; f <= pCex->iFrame; f++ ) {
                 Abc_NtkForEachPi( pNtk, pObj, i )
                     if ( !pCare || Abc_InfoHasBit(pCare->pData, pCare->nRegs+pCare->nPis*f + i) )
-                        fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
+                        if ( fNames )
+                            fprintf( pFile, "%s@%d=%c\n", Abc_ObjName(pObj), f, '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
+                        else
+                            fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, pCex->nRegs+pCex->nPis*f + i) );
+                    else if ( !fNames )
+                        fprintf( pFile, "x");
+                if ( !fNames && fAiger)
+                    fprintf( pFile, "\n");
+            }
+            if (fExtended && fAiger && !fNames)
+                fprintf( pFile, ".\n");
         }
         Abc_CexFreeP( &pCare );
     }
-    else
-    {
-        Abc_NtkForEachLatch( pNtk, pObj, i )
-            fprintf( pFile, "%c", '0'+!Abc_LatchIsInit0(pObj) );
-
-        for ( i = pCex->nRegs; i < pCex->nBits; i++ )
-        {
-            if ( fAiger && (i-pCex->nRegs)%pCex->nPis == 0)
-                fprintf( pFile, "\n");
-            fprintf( pFile, "%c", '0'+Abc_InfoHasBit(pCex->pData, i) );
-        }
-    }
 }
 
 /**Function*************************************************************
@@ -2689,9 +3056,11 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
     int fPrintFull = 0;
     int fUseFfNames = 0;
     int fVerbose   = 0;
+    int fCexInfo   = 0;
+    int fExtended  = 0;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafzvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafzvhxt" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2728,6 +3097,12 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
             case 'v':
                 fVerbose ^= 1;
                 break;
+            case 'x':
+                fCexInfo ^= 1;
+                break;
+            case 't':
+                fExtended ^= 1;
+                break;
             case 'h':
                 goto usage;
             default:
@@ -2776,8 +3151,8 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
         if ( pAbc->pCex )
         {
             Abc_NtkDumpOneCex( pFile, pNtk, pCex, 
-                fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, 
-                fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose );
+                fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, fCexInfo,
+                fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose, fExtended );
         }
         else if ( pAbc->vCexVec )
         {
@@ -2785,10 +3160,10 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
             {
                 if ( pCex == NULL )
                     continue;
-                fprintf( pFile, "#\n#\n# CEX for output %d\n#\n", i ); 
+                fprintf( pFile, "#\n#\n# CEX for output %d\n#\n", i );
                 Abc_NtkDumpOneCex( pFile, pNtk, pCex, 
-                    fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, 
-                    fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose );
+                    fPrintFull, fNames, fUseFfNames, fMinimize, fUseOldMin, fCexInfo,
+                    fCheckCex, fUseSatBased, fHighEffort, fAiger, fVerbose, fExtended );
             }
         }
         fprintf( pFile, "# DONE\n" ); 
@@ -2832,8 +3207,10 @@ usage:
     fprintf( pAbc->Err, "\t-u     : use fast SAT-based CEX minimization [default = %s]\n", fUseSatBased? "yes": "no" );
     fprintf( pAbc->Err, "\t-e     : use high-effort SAT-based CEX minimization [default = %s]\n", fHighEffort? "yes": "no" );
     fprintf( pAbc->Err, "\t-o     : use old CEX minimization algorithm [default = %s]\n", fUseOldMin? "yes": "no" );
+    fprintf( pAbc->Err, "\t-x     : minimize using algorithm from cexinfo command [default = %s]\n", fCexInfo? "yes": "no" );
     fprintf( pAbc->Err, "\t-c     : check generated CEX using ternary simulation [default = %s]\n", fCheckCex? "yes": "no" );
     fprintf( pAbc->Err, "\t-a     : print cex in AIGER 1.9 format [default = %s]\n", fAiger? "yes": "no" );
+    fprintf( pAbc->Err, "\t-t     : extended header info when cex in AIGER 1.9 format [default = %s]\n", fAiger? "yes": "no" );
     fprintf( pAbc->Err, "\t-f     : enable printing flop values in each timeframe [default = %s]\n", fPrintFull? "yes": "no" );  
     fprintf( pAbc->Err, "\t-z     : toggle using saved flop names [default = %s]\n", fUseFfNames? "yes": "no" );  
     fprintf( pAbc->Err, "\t-v     : enable verbose output [default = %s]\n", fVerbose? "yes": "no" );  
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 844497ad0..343563598 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -227,7 +227,8 @@ extern int               Gia_ManBmcPerform( Gia_Man_t * p, Bmc_AndPar_t * pPars
 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 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 );
+extern int               Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
+extern int               Bmc_CexCareVerifyAnyPo( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
 extern Abc_Cex_t *       Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int fHighEffort, int fCheck, int fVerbose );
 extern Abc_Cex_t *       Bmc_CexCareSatBasedMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int fHighEffort, int fVerbose );
 /*=== bmcCexCut.c ==========================================================*/
@@ -238,6 +239,7 @@ extern Abc_Cex_t *       Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pC
 /*=== bmcCexTool.c ==========================================================*/
 extern void              Bmc_CexPrint( Abc_Cex_t * pCex, int nRealPis, int fVerbose );
 extern int               Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare );
+extern int               Bmc_CexVerifyAnyPo( 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 fBackTopo, int fDump, int fVerbose );
diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c
index c274b04cb..d9a677c35 100644
--- a/src/sat/bmc/bmcCexCare.c
+++ b/src/sat/bmc/bmcCexCare.c
@@ -455,8 +455,9 @@ Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t
   SeeAlso     []
 
 ***********************************************************************/
-void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )
+int Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )
 {
+    int result;
     Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
     if ( fVerbose )
     {
@@ -465,11 +466,13 @@ void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, in
         printf( "Minimized:    " );
         Bmc_CexPrint( pCexMin, Gia_ManPiNum(pGia), 0 );
     }
-    if ( !Bmc_CexVerify( pGia, pCex, pCexMin ) )
+    result = Bmc_CexVerify( pGia, pCex, pCexMin );
+    if ( !result )
         printf( "Counter-example verification has failed.\n" );
     else 
         printf( "Counter-example verification succeeded.\n" );
     Gia_ManStop( pGia );
+    return result;
 }
 /*
     {
@@ -480,6 +483,37 @@ void Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, in
     }
 */
 
+/**Function*************************************************************
+
+  Synopsis    [Verifies the care set of the counter-example.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bmc_CexCareVerifyAnyPo( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose )
+{
+    int iPo;
+    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 );
+    }
+    iPo = Bmc_CexVerifyAnyPo( pGia, pCex, pCexMin );
+    if ( iPo < 0 )
+        printf( "Counter-example verification has failed.\n" );
+    else
+        printf( "Counter-example verification succeeded.\n" );
+    Gia_ManStop( pGia );
+    return iPo;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bmc/bmcCexTools.c b/src/sat/bmc/bmcCexTools.c
index 6cc298577..6bea6fc5f 100644
--- a/src/sat/bmc/bmcCexTools.c
+++ b/src/sat/bmc/bmcCexTools.c
@@ -374,6 +374,53 @@ int Bmc_CexVerify( Gia_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexCare )
     return Gia_ObjTerSimGet1(pObj);
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Verifies the care set of the counter-example for an arbitrary PO.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bmc_CexVerifyAnyPo( 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 );
+    Gia_ObjTerSimSet0( Gia_ManConst0(p) );
+    Gia_ManForEachRi( p, pObj, k )
+        Gia_ObjTerSimSet0( pObj );
+    for ( i = 0; i <= pCex->iFrame; i++ )
+    {
+        Gia_ManForEachPi( p, pObj, 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 );
+            else
+                Gia_ObjTerSimSet0( pObj );
+        }
+        Gia_ManForEachRo( p, pObj, k )
+            Gia_ObjTerSimRo( p, pObj );
+        Gia_ManForEachAnd( p, pObj, k )
+            Gia_ObjTerSimAnd( pObj );
+        Gia_ManForEachCo( p, pObj, k )
+            Gia_ObjTerSimCo( pObj );
+    }
+    for (i = 0; i < Gia_ManPoNum(p) - Gia_ManConstrNum(p); i++)
+    {
+        pObj = Gia_ManPo( p, i );
+        if (Gia_ObjTerSimGet1(pObj))
+            return i;
+    }
+    return -1;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Computes internal states of the CEX.]