diff --git a/src/aig/gia/giaClp.c b/src/aig/gia/giaClp.c
index 5102d4973..4f83b49c4 100644
--- a/src/aig/gia/giaClp.c
+++ b/src/aig/gia/giaClp.c
@@ -53,7 +53,7 @@ extern int Gia_ManFactorNode( Gia_Man_t * p, char * pSop, Vec_Int_t * vLeaves );
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Gia_GetFakeNames( int nNames )
+Vec_Ptr_t * Gia_GetFakeNames( int nNames, int fCaps )
 {
     Vec_Ptr_t * vNames;
     char Buffer[5];
@@ -64,12 +64,12 @@ Vec_Ptr_t * Gia_GetFakeNames( int nNames )
     {
         if ( nNames < 26 )
         {
-            Buffer[0] = 'a' + i;
+            Buffer[0] = (fCaps ? 'A' : 'a') + i;
             Buffer[1] = 0;
         }
         else
         {
-            Buffer[0] = 'a' + i%26;
+            Buffer[0] = (fCaps ? 'A' : 'a') + i%26;
             Buffer[1] = '0' + i/26;
             Buffer[2] = 0;
         }
@@ -378,8 +378,8 @@ Gia_Man_t * Gia_ManCollapseTest( Gia_Man_t * p, int fVerbose )
     Dsd_Decompose( pManDsd, (DdNode **)Vec_PtrArray(vFuncs), Vec_PtrSize(vFuncs) );
     if ( fVerbose )
     {
-        Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p) );
-        Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p) );
+        Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p), 0 );
+        Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p), 1 );
         char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi );
         char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo );
         Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1, 0 );
@@ -464,8 +464,8 @@ void Gia_ManCheckDsd( Gia_Man_t * p, int OffSet, int fVerbose )
     
     if ( fVerbose )
     {
-        Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p) );
-        Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p) );
+        Vec_Ptr_t * vNamesCi = Gia_GetFakeNames( Gia_ManCiNum(p), 0 );
+        Vec_Ptr_t * vNamesCo = Gia_GetFakeNames( Gia_ManCoNum(p), 1 );
         char ** ppNamesCi = (char **)Vec_PtrArray( vNamesCi );
         char ** ppNamesCo = (char **)Vec_PtrArray( vNamesCo );
         Dsd_TreePrint( stdout, pManDsd, ppNamesCi, ppNamesCo, 0, -1, OffSet );
diff --git a/src/aig/gia/giaPat2.c b/src/aig/gia/giaPat2.c
index b557ac6f8..93c4b1da9 100644
--- a/src/aig/gia/giaPat2.c
+++ b/src/aig/gia/giaPat2.c
@@ -1372,6 +1372,65 @@ void Min_ManTest2( Gia_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Gia_GenerateCexesDumpBlif( char * pFileName, Gia_Man_t * p, Vec_Wec_t * vCexes )
+{
+    extern Vec_Ptr_t * Gia_GetFakeNames( int nNames, int fCaps );
+    FILE * pFile = fopen( pFileName, "wb" );
+    if ( pFile == NULL ) {
+        printf( "Cannot open output file name \"%s\".\n", pFileName );
+        return;
+    }
+    int fFakeIns = 0, fFakeOuts = 0;
+    if ( p->vNamesIn == NULL )
+        p->vNamesIn = Gia_GetFakeNames( Gia_ManCiNum(p), 0 ), fFakeIns = 1;
+    if ( p->vNamesOut == NULL )
+        p->vNamesOut = Gia_GetFakeNames( Gia_ManCoNum(p), 1 ), fFakeOuts = 1;
+
+    Gia_Obj_t * pObj, * pObj2; 
+    char * pLine = ABC_CALLOC( char, Gia_ManCiNum(p)+3 );
+    int i, k, c, iLit, nOuts[2] = {0}, nCexes = Vec_WecSize(vCexes) / Gia_ManCoNum(p);
+    fprintf( pFile, "# Satisfying assignments for the primary outputs generated by ABC on %s\n", Gia_TimeStamp() );
+    fprintf( pFile, ".model %s\n", p->pName );
+    fprintf( pFile, ".inputs" );
+    Gia_ManForEachCi( p, pObj, i )
+        fprintf( pFile, " %s", Gia_ObjCiName(p, i) );
+    fprintf( pFile, "\n.outputs" );
+    Gia_ManForEachCo( p, pObj, i )
+        fprintf( pFile, " %s", Gia_ObjCoName(p, i) );
+    fprintf( pFile, "\n" );
+    Gia_ManForEachCo( p, pObj, i ) {
+        if ( Gia_ObjFaninLit0p(p, pObj) == 0 ) {
+            fprintf( pFile, ".names %s\n", Gia_ObjCoName(p, i) );
+            nOuts[0]++;
+        }
+        else if ( Gia_ObjFaninLit0p(p, pObj) == 1 ) {
+            fprintf( pFile, ".names %s\n 1\n", Gia_ObjCiName(p, i) );
+            nOuts[1]++;
+        }
+        else {
+            fprintf( pFile, ".names" );
+            Gia_ManForEachCi( p, pObj2, c )
+                fprintf( pFile, " %s", Gia_ObjCiName(p, c) );
+            fprintf( pFile, " %s\n", Gia_ObjCoName(p, i) );
+            for ( c = 0; c < nCexes; c++ ) {
+                Vec_Int_t * vPat = Vec_WecEntry( vCexes, i*nCexes+c );
+                memset(pLine, '-', Gia_ManCiNum(p) );
+                Vec_IntForEachEntry( vPat, iLit, k )
+                    pLine[Abc_Lit2Var(iLit)-1] = '1' - Abc_LitIsCompl(iLit);
+                fprintf( pFile, "%s 1\n", pLine );
+            }
+            nOuts[1]++;
+        }
+    }
+    fprintf( pFile, ".end\n\n" );
+    fclose( pFile );
+    printf( "Information about %d sat, %d unsat, and %d undecided primary outputs was written into BLIF file \"%s\".\n", 
+        nOuts[1], nOuts[0], Gia_ManCoNum(p)-nOuts[1]-nOuts[0], pFileName );    
+    free( pLine );
+
+    if ( fFakeIns )  Vec_PtrFreeFree( p->vNamesIn  ), p->vNamesIn  = NULL;
+    if ( fFakeOuts ) Vec_PtrFreeFree( p->vNamesOut ), p->vNamesOut = NULL;
+}
 void Gia_GenerateCexesDumpFile( char * pFileName, Gia_Man_t * p, Vec_Wec_t * vCexes, int fShort )
 {
     FILE * pFile = fopen( pFileName, "wb" );
@@ -1416,13 +1475,16 @@ void Gia_GenerateCexesDumpFile( char * pFileName, Gia_Man_t * p, Vec_Wec_t * vCe
     fclose( pFile );
     free( pLine );
 }
-void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fVerbose, int fVeryVerbose )
+void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fBlif, int fVerbose, int fVeryVerbose )
 {
     unsigned Start = Abc_Random(1);
     Vec_Int_t * vStats[3] = {0}; int i;
     Vec_Wec_t * vCexes  = Min_ManComputeCexes( p, NULL, nMaxTries, nMinCexes, vStats, fUseSim, fUseSat, fVerbose );    
     assert( Vec_WecSize(vCexes) == Gia_ManCoNum(p) * nMinCexes );
-    Gia_GenerateCexesDumpFile( pFileName, p, vCexes, fShort );
+    if ( fBlif )
+        Gia_GenerateCexesDumpBlif( pFileName, p, vCexes );
+    else
+        Gia_GenerateCexesDumpFile( pFileName, p, vCexes, fShort );
     for ( i = 0; i < 3; i++ )
       Vec_IntFreeP( &vStats[i] );
     Vec_WecFree( vCexes );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c5ea7d801..c06c7da25 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -53541,17 +53541,18 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9GenCex( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fVerbose, int fVeryVerbose );
+    extern void Gia_GenerateCexes( char * pFileName, Gia_Man_t * p, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fShort, int fBlif, int fVerbose, int fVeryVerbose );
     char * pFileName = (char *)"cexes.txt";
     int nMinCexes =  1;
     int nMaxTries = 10;
     int fUseSim   =  1;
     int fUseSat   =  1;
     int fShort    =  0;
+    int fBlif     =  0;
     int fVerbose  =  0;
     int c;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CMFstcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CMFstcbvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -53595,6 +53596,9 @@ int Abc_CommandAbc9GenCex( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             fShort ^= 1;
             break;
+        case 'b':
+            fBlif ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -53609,11 +53613,11 @@ int Abc_CommandAbc9GenCex( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Bmci(): There is no AIG.\n" );
         return 0;
     }
-    Gia_GenerateCexes( pFileName, pAbc->pGia, nMaxTries, nMinCexes, fUseSim, fUseSat, fShort, fVerbose, 0 );
+    Gia_GenerateCexes( pFileName, pAbc->pGia, nMaxTries, nMinCexes, fUseSim, fUseSat, fShort, fBlif, fVerbose, 0 );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &gencex [-CM num] [-F file] [-stcvh]\n" );
+    Abc_Print( -2, "usage: &gencex [-CM num] [-F file] [-stcbvh]\n" );
     Abc_Print( -2, "\t          generates satisfying assignments for each output of the miter\n" );
     Abc_Print( -2, "\t-C num  : the number of timeframes [default = %d]\n",                  nMinCexes );
     Abc_Print( -2, "\t-M num  : the max simulation runs before using SAT [default = %d]\n",  nMaxTries );
@@ -53621,6 +53625,7 @@ usage:
     Abc_Print( -2, "\t-s      : toggles using reverse simulation [default = %s]\n",          fUseSim  ? "yes": "no" );
     Abc_Print( -2, "\t-t      : toggles using SAT solving [default = %s]\n",                 fUseSat  ? "yes": "no" );
     Abc_Print( -2, "\t-c      : toggles outputing care literals only [default = %s]\n",      fShort   ? "yes": "no" );
+    Abc_Print( -2, "\t-b      : toggles outputing the BLIF file [default = %s]\n",           fBlif    ? "yes": "no" );
     Abc_Print( -2, "\t-v      : toggles printing verbose information [default = %s]\n",      fVerbose ? "yes": "no" );
     Abc_Print( -2, "\t-h      : print the command usage\n");
     return 1;