diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 9ba9682dc..49d3355ca 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -38250,7 +38250,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fCbs = 1, approxLim = 600, subBatchSz = 1, adaRecycle = 500, nMaxNodes = 0;
     Cec4_ManSetParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMrmdckngxysopwqvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "JWRILDCNPMFrmdckngxysopwqvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -38364,6 +38364,15 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nMaxNodes < 0 )
                 goto usage;
             break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->pDumpName = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;            
         case 'r':
             pPars->fRewriting ^= 1;
             break;
@@ -38405,7 +38414,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
             break;
         case 'q':
             pPars->fBMiterInfo ^= 1;
-            break;
+            break;      
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -38445,7 +38454,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &fraig [-JWRILDCNPM <num>] [-rmdckngxysopwvh]\n" );
+    Abc_Print( -2, "usage: &fraig [-JWRILDCNPM <num>] [-F filename] [-rmdckngxysopwvh]\n" );
     Abc_Print( -2, "\t         performs combinational SAT sweeping\n" );
     Abc_Print( -2, "\t-J num : the solver type [default = %d]\n", pPars->jType );
     Abc_Print( -2, "\t-W num : the number of simulation words [default = %d]\n", pPars->nWords );
@@ -38457,6 +38466,7 @@ usage:
     Abc_Print( -2, "\t-N num : the min number of calls to recycle the solver [default = %d]\n", pPars->nCallsRecycle );
     Abc_Print( -2, "\t-P num : the number of pattern generation iterations [default = %d]\n", pPars->nGenIters );
     Abc_Print( -2, "\t-M num : the node count limit to call the old sweeper [default = %d]\n", nMaxNodes );
+    Abc_Print( -2, "\t-F file: the file name to dump primary output information [default = none]\n" );
     Abc_Print( -2, "\t-r     : toggle the use of AIG rewriting [default = %s]\n", pPars->fRewriting? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "miter": "circuit" );
     Abc_Print( -2, "\t-d     : toggle using double output miters [default = %s]\n", pPars->fDualOut? "yes": "no" );
diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index c9aa96658..10101e6c0 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -122,6 +122,7 @@ struct Cec_ParFra_t_
     int              iOutFail;      // the failed output
     int              fBMiterInfo;   // printing BMiter information
     int              nPO;           // number of po in original design given a bmiter
+    char *           pDumpName;     // file name to dump statistics
 };
 
 // combinational equivalence checking parameters
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c
index b198c7ffe..554fd550d 100644
--- a/src/proof/cec/cecSatG2.c
+++ b/src/proof/cec/cecSatG2.c
@@ -1783,6 +1783,48 @@ void Gia_ManRemoveWrongChoices( Gia_Man_t * p )
     //Abc_Print( 1, "Removed %d wrong choices.\n", Counter );
 }
 
+void Cec4_ManSimulateDumpInfo( Cec4_Man_t * pMan )
+{
+    Gia_Obj_t * pObj; int i, k, nWords = pMan->pAig->nSimWords, nOuts[2] = {0};
+    Vec_Wrd_t * vSims = NULL, * vSimsPi = NULL;
+    FILE * pFile = fopen( pMan->pPars->pDumpName, "wb" );
+    if ( pFile == NULL ) {
+        printf( "Cannot open file \"%s\" for writing primary output information.\n", pMan->pPars->pDumpName );
+        return;
+    }
+    vSimsPi = Vec_WrdDup( pMan->pAig->vSimsPi );
+    memmove( Vec_WrdArray(vSimsPi), Vec_WrdArray(vSimsPi) + nWords, Gia_ManCiNum(pMan->pAig) * nWords );
+    Vec_WrdShrink( vSimsPi, Gia_ManCiNum(pMan->pAig) * nWords );
+    if ( Abc_TtIsConst0(Vec_WrdArray(vSimsPi), Gia_ManCiNum(pMan->pAig) * nWords) ) {
+        Vec_WrdFree( vSimsPi );
+        vSimsPi = Vec_WrdStartRandom( Gia_ManCiNum(pMan->pAig) * nWords );
+    }
+    vSims = Gia_ManSimPatSimOut( pMan->pAig, vSimsPi, 1 );
+    assert( nWords * Gia_ManCiNum(pMan->pAig) == Vec_WrdSize(vSimsPi) );
+    Gia_ManForEachCo( pMan->pAig, pObj, i )
+    {
+        void Extra_PrintHex2( FILE * pFile, unsigned * pTruth, int nVars );
+        word * pSims = Vec_WrdEntryP( vSims, nWords*i );
+        //Extra_PrintHex2( stdout, (unsigned *)pSims, 8 ); printf( "\n" );
+        fprintf( pFile, "%d ", i );
+        if ( Gia_ObjFaninLit0p(pMan->pNew, Gia_ManCo(pMan->pNew, i)) == 0 ) 
+            nOuts[0]++;
+        else if ( Abc_TtIsConst0(pSims, nWords) )
+            fprintf( pFile, "-" );
+        else {
+            int iPat = Abc_TtFindFirstBit2(pSims, nWords);
+            for ( k = 0; k < Gia_ManPiNum(pMan->pAig); k++ )
+                fprintf( pFile, "%d", Abc_TtGetBit(Vec_WrdEntryP(vSimsPi, nWords*k), iPat) );
+            nOuts[1]++;
+        }
+        fprintf( pFile, "\n" );
+    }
+    printf( "Information about %d sat, %d unsat, and %d undecided primary outputs was written into file \"%s\".\n", 
+        nOuts[1], nOuts[0], Gia_ManCoNum(pMan->pAig)-nOuts[1]-nOuts[0], pMan->pPars->pDumpName );
+    fclose( pFile );
+    Vec_WrdFree( vSims );
+    Vec_WrdFree( vSimsPi );
+}
 int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** ppNew, int fSimOnly )
 {
 
@@ -1954,6 +1996,8 @@ finalize:
         ABC_FREE( pBase );
         printf( "Dumped miter \"%s\" with %d pairs.\n", pFileName, pMan->vPairs ? Vec_IntSize(pMan->vPairs)/2 : -1 );
     }
+    if ( pPars->pDumpName )
+        Cec4_ManSimulateDumpInfo( pMan );
     Cec4_ManDestroy( pMan );
     //Gia_ManStaticFanoutStop( p );
     //Gia_ManEquivPrintClasses( p, 1, 0 );