Enabled detecting CEXes in multiple POs without stopping (sim3 -a).

9 files changed, 103 insertions, 44 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c53133d1..56aaed9e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2301,10 +2301,24 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
         if ( pAbc->vCexVec )
         {
             Abc_Cex_t * pTemp;
+            int nCexes = 0;
+            int Counter = 0;
             printf( "\n" );
             Vec_PtrForEachEntry( Abc_Cex_t *, pAbc->vCexVec, pTemp, c )
+            {
+                if ( pTemp == (void *)(ABC_PTRINT_T)1 )
+                {
+                    Counter++;
+                    continue;
+                }
                 if ( pTemp )
+                {
+                    printf( "%4d : ", ++nCexes );
                     Abc_CexPrintStats( pTemp );
+                }
+            }
+            if ( Counter )
+                printf( "In total, %d (out of %d) outputs are \"sat\" but CEXes are not recorded.\n", Counter, Vec_PtrSize(pAbc->vCexVec) );
         }
     }
     return 0;
@@ -17749,7 +17763,8 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
     int TimeOut;
     int fSolveAll;
     int fVerbose;
-    extern int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose );
+    int fNotVerbose;
+    extern int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose, int fNotVerbose );
     // set defaults
     nFrames    =  20;
     nWords     =  50;
@@ -17760,9 +17775,10 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
     TimeOut    =   0;
     fSolveAll  =   0;
     fVerbose   =   0;
+    fNotVerbose=   0;
     // parse command line
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTavh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FWBRSNTavzh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -17849,6 +17865,9 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'v':
             fVerbose ^= 1;
             break;
+        case 'z':
+            fNotVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -17866,13 +17885,18 @@ int Abc_CommandSim3( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     ABC_FREE( pNtk->pSeqModel );
-    pAbc->Status = Abc_NtkDarSeqSim3( pNtk, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose );
+    pAbc->Status = Abc_NtkDarSeqSim3( pNtk, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose, fNotVerbose );
 //    pAbc->nFrames = pAbc->pCex->iFrame;
     Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
+    if ( pNtk->vSeqModelVec )
+    {
+        Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec );
+        pAbc->nFrames = -1;
+    }
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: sim3 [-FWBRSNT num] [-avh]\n" );
+    Abc_Print( -2, "usage: sim3 [-FWBRSNT num] [-avzh]\n" );
     Abc_Print( -2, "\t         performs random simulation of the sequential miter\n" );
     Abc_Print( -2, "\t-F num : the number of frames to simulate [default = %d]\n", nFrames );
     Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n",  nWords );
@@ -17883,6 +17907,7 @@ usage:
     Abc_Print( -2, "\t-T num : approximate runtime limit in seconds [default = %d]\n", TimeOut );
     Abc_Print( -2, "\t-a     : solve all outputs (do not stop when one is SAT) [default = %s]\n", fSolveAll? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-z     : toggle suppressing report about solved outputs [default = %s]\n", fNotVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -20781,7 +20806,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Saig_ParBmcSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "SFTCDJILadruvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "SFTCDJILadruvzh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -20883,6 +20908,9 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'v':
             pPars->fVerbose ^= 1;
             break;
+        case 'z':
+            pPars->fNotVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -20941,7 +20969,7 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: bmc3 [-SFTCDJI num] [-L file] [-aduvh]\n" );
+    Abc_Print( -2, "usage: bmc3 [-SFTCDJI num] [-L file] [-aduvzh]\n" );
     Abc_Print( -2, "\t         performs bounded model checking with dynamic unrolling\n" );
     Abc_Print( -2, "\t-S num : the starting time frame [default = %d]\n", pPars->nStart );
     Abc_Print( -2, "\t-F num : the max number of time frames (0 = unused) [default = %d]\n", pPars->nFramesMax );
@@ -20955,6 +20983,7 @@ usage:
     Abc_Print( -2, "\t-d     : drops (replaces by 0) satisfiable outputs [default = %s]\n", pPars->fDropSatOuts? "yes": "no" );
     Abc_Print( -2, "\t-u     : toggle performing structural OR-decomposition [default = %s]\n", fOrDecomp? "yes": "not" );
     Abc_Print( -2, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-z     : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -22337,7 +22366,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Pdr_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTarmsdgvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTarmsdgvwzh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -22433,6 +22462,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'w':
             pPars->fVeryVerbose ^= 1;
             break;
+        case 'z':
+            pPars->fNotVerbose ^= 1;
+            break;
         case 'h':
         default:
             goto usage;
@@ -22465,7 +22497,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: pdr [-MFCRT<num] [-armsdgvwh]\n" );
+    Abc_Print( -2, "usage: pdr [-MFCRT<num] [-armsdgvwzh]\n" );
     Abc_Print( -2, "\t         model checking using property directed reachability (aka IC3)\n" );
     Abc_Print( -2, "\t         pioneered by Aaron Bradley (http://ecee.colorado.edu/~bradleya/ic3/)\n" );
     Abc_Print( -2, "\t         with improvements by Niklas Een (http://een.se/niklas/)\n" );
@@ -22483,6 +22515,7 @@ usage:
     Abc_Print( -2, "\t-g     : toggle skipping expensive generalization step [default = %s]\n", pPars->fSkipGeneral? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing optimization summary [default = %s]\n", pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing detailed stats default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-z     : toggle suppressing report about solved outputs [default = %s]\n", pPars->fNotVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 424ab14c..8ca40bc0 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -3273,7 +3273,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose )
+int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose, int fNotVerbose )
 {
     Aig_Man_t * pMan;
     int status, RetValue = -1;
@@ -3284,7 +3284,7 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize,
         Abc_AigCleanup((Abc_Aig_t *)pNtk->pManFunc);
     }
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
-    if ( Ssw_RarSimulate( pMan, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose ) == 0 )
+    if ( Ssw_RarSimulate( pMan, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose, fNotVerbose ) == 0 )
     { 
         if ( pMan->pSeqModel )
         {
@@ -3304,6 +3304,9 @@ int Abc_NtkDarSeqSim3( Abc_Ntk_t * pNtk, int nFrames, int nWords, int nBinSize,
 //        Abc_Print( 1, "Simulation of %d frames with %d words did not assert the outputs.    ", 
 //            nFrames, nWords );
     }
+    if ( pNtk->vSeqModelVec )
+        Vec_PtrFreeFree( pNtk->vSeqModelVec );
+    pNtk->vSeqModelVec = pMan->vSeqModelVec;  pMan->vSeqModelVec = NULL;
 //    ABC_PRT( "Time", clock() - clk );
     Aig_ManStop( pMan );
     return RetValue;
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 9aedbed4..731cf9a1 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -554,7 +554,8 @@ static inline void Vec_PtrFreeFree( Vec_Ptr_t * p )
     int i;
     if ( p == NULL ) return;
     Vec_PtrForEachEntry( void *, p, pTemp, i )
-        ABC_FREE( pTemp );
+        if ( pTemp != (void *)(ABC_PTRINT_T)1 && pTemp != (void *)(ABC_PTRINT_T)2 )
+            ABC_FREE( pTemp );
     Vec_PtrFree( p );
 }
 
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index a815bb30..c2243761 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -53,6 +53,7 @@ struct Pdr_Par_t_
     int fSkipGeneral;     // skips expensive generalization step
     int fVerbose;         // verbose output`
     int fVeryVerbose;     // very verbose output
+    int fNotVerbose;      // not printing line by line progress
     int fSilent;          // totally silent execution
     int fSolveAll;        // do not stop when found a SAT output
     int nFailOuts;        // the number of failed outputs
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 46288925..314784d7 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -57,6 +57,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
     pPars->fShortest     =       0;  // forces bug traces to be shortest
     pPars->fVerbose      =       0;  // verbose output
     pPars->fVeryVerbose  =       0;  // very verbose output
+    pPars->fNotVerbose   =       0;  // not printing line-by-line progress
     pPars->iFrame        =      -1;  // explored up to this frame
 }
 
@@ -645,8 +646,9 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                         assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
                         pCex = Pdr_ManDeriveCex(p);
                         Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCex );
-                        Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",  
-                            nOutDigits, p->iOutCur, pCex->iFrame, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
+                        if ( !p->pPars->fNotVerbose )
+                            Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",  
+                                nOutDigits, p->iOutCur, pCex->iFrame, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
                         if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
                             return 0; // all SAT
                         Pdr_QueueClean( p );
diff --git a/src/proof/ssw/ssw.h b/src/proof/ssw/ssw.h
index 3ddcff37..4858ab89 100644
--- a/src/proof/ssw/ssw.h
+++ b/src/proof/ssw/ssw.h
@@ -118,7 +118,7 @@ extern int           Ssw_SecGeneral( Aig_Man_t * pAig1, Aig_Man_t * pAig2, Ssw_P
 extern int           Ssw_SecGeneralMiter( Aig_Man_t * pMiter, Ssw_Pars_t * pPars );
 /*=== sswRarity.c ===================================================*/
 extern int           Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fMiter, Abc_Cex_t * pCex, int fLatchOnly, int fVerbose );
-extern int           Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose );
+extern int           Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose, int fNotVerbose );
 /*=== sswSim.c ===================================================*/
 extern Ssw_Sml_t *   Ssw_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
 extern Ssw_Sml_t *   Ssw_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
diff --git a/src/proof/ssw/sswRarity.c b/src/proof/ssw/sswRarity.c
index 19dc3192..da96d218 100644
--- a/src/proof/ssw/sswRarity.c
+++ b/src/proof/ssw/sswRarity.c
@@ -546,7 +546,7 @@ int Ssw_RarManObjWhichOne( Ssw_RarMan_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p )
+int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p, int * pnSolvedNow, int iFrame, int fNotVerbose, clock_t Time )
 {
     Aig_Obj_t * pObj;
     int i;
@@ -556,12 +556,33 @@ int Ssw_RarManCheckNonConstOutputs( Ssw_RarMan_t * p )
     {
         if ( p->pAig->nConstrs && i >= Saig_ManPoNum(p->pAig) - p->pAig->nConstrs )
             return 0;
-        if ( Vec_PtrEntry(p->vCexes, i) )
+        if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
             continue;
         if ( !Ssw_RarManObjIsConst(p, pObj) )
         {
             p->iFailPo  = i;
             p->iFailPat = Ssw_RarManObjWhichOne( p, pObj );
+
+            // remember the one solved
+            if ( pnSolvedNow )
+            {
+                (*pnSolvedNow)++;
+                if ( p->vCexes == NULL )
+                    p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
+                assert( Vec_PtrEntry(p->vCexes, p->iFailPo) == NULL );
+                Vec_PtrWriteEntry( p->vCexes, p->iFailPo, (void *)(ABC_PTRINT_T)1 );
+                // print final report
+                if ( !fNotVerbose )
+                {
+                    int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
+                    Abc_Print( 1, "Output %*d was asserted in frame %4d (solved %*d out of %*d outputs).  ", 
+                        nOutDigits, p->iFailPo, iFrame, 
+                        nOutDigits, *pnSolvedNow, 
+                        nOutDigits, Saig_ManPoNum(p->pAig) );
+                    Abc_PrintTime( 1, "Time", Time );
+                }
+                continue;
+            }
             return 1;
         }
     }
@@ -697,7 +718,6 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames
     p->vUpdConst = Vec_PtrAlloc( 100 );
     p->vUpdClass = Vec_PtrAlloc( 100 );
     p->vPatBests = Vec_IntAlloc( 100 );
-    p->vCexes    = Vec_PtrStart( Saig_ManPoNum(pAig) );
     return p;
 }
 
@@ -714,7 +734,13 @@ static Ssw_RarMan_t * Ssw_RarManStart( Aig_Man_t * pAig, int nWords, int nFrames
 ***********************************************************************/
 static void Ssw_RarManStop( Ssw_RarMan_t * p )
 {
-    Vec_PtrFreeP( &p->vCexes );
+//    Vec_PtrFreeP( &p->vCexes );
+    if ( p->vCexes )
+    {
+        assert( p->pAig->vSeqModelVec == NULL );
+        p->pAig->vSeqModelVec = p->vCexes;
+        p->vCexes = NULL;
+    }
     if ( p->ppClasses ) Ssw_ClassesStop( p->ppClasses );
     Vec_IntFreeP( &p->vInits );
     Vec_IntFreeP( &p->vPatBests );
@@ -897,7 +923,7 @@ int Ssw_RarCheckTrivial( Aig_Man_t * pAig, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose )
+int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fSolveAll, int fVerbose, int fNotVerbose )
 {
     int fTryBmc = 0;
     int fMiter = 1;
@@ -905,7 +931,6 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
     int r, f = -1;
     clock_t clk, clkTotal = clock();
     clock_t nTimeToStop = TimeOut ? TimeOut * CLOCKS_PER_SEC + clock(): 0;
-    int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
     int nNumRestart = 0;
     int nSavedSeed = nRandSeed;
     int RetValue = -1;
@@ -913,6 +938,7 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
     int nSolved = 0;
     assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManConstrNum(pAig) == 0 );
+    ABC_FREE( pAig->pSeqModel );
     // consider the case of empty AIG
     if ( Aig_ManNodeNum(pAig) == 0 )
         return -1;
@@ -945,13 +971,13 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
         for ( f = 0; f < nFrames; f++ )
         {
             Ssw_RarManSimulate( p, f ? NULL : p->vInits, 0, 0 );
-            if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
+            if ( fMiter && Ssw_RarManCheckNonConstOutputs(p, fSolveAll ? &nSolved : NULL, r * p->nFrames + f, fNotVerbose, clock() - clkTotal) )
             {
+                RetValue = 0;
                 if ( !fSolveAll )
                 {
                     if ( fVerbose ) Abc_Print( 1, "\n" );
     //                Abc_Print( 1, "Simulation asserted a PO in frame f: %d <= f < %d.\n", r * nFrames, (r+1) * nFrames );
-                    ABC_FREE( pAig->pSeqModel );
                     Ssw_RarManPrepareRandom( nSavedSeed );
                     if ( fVerbose )
                         Abc_Print( 1, "Simulated %d frames for %d rounds with %d restarts.\n", nFrames, nNumRestart * nRestart + r, nNumRestart );
@@ -959,23 +985,8 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
                     // print final report
                     Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", pAig->pSeqModel->iPo, pAig->pName, pAig->pSeqModel->iFrame );
                     Abc_PrintTime( 1, "Time", clock() - clkTotal );
-                    RetValue = 0;
                     goto finish;
                 }
-                else
-                {
-                    nSolved++;
-                    assert( Vec_PtrEntry(p->vCexes, p->iFailPo) == NULL );
-                    Vec_PtrWriteEntry( p->vCexes, p->iFailPo, p->vCexes );
-                    // print final report
-                    ABC_FREE( pAig->pSeqModel );
-                    Abc_Print( 1, "Output %*d was asserted in frame %4d (solved %*d out of %*d outputs).  ", 
-                        nOutDigits, p->iFailPo, r * p->nFrames + f, 
-                        nOutDigits, nSolved, nOutDigits, Saig_ManPoNum(p->pAig) );
-                    Abc_PrintTime( 1, "Time", clock() - clkTotal );
-                    RetValue = 0;
-                }
-
             }
             // check timeout
             if ( TimeOut && clock() > nTimeToStop )
@@ -985,6 +996,9 @@ int Ssw_RarSimulate( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize, in
                 Abc_Print( 1, "Reached timeout (%d sec).\n",  TimeOut );
                 goto finish;
             }
+            // check if all outputs are solved by now
+            if ( fSolveAll && p->vCexes && Vec_PtrCountZero(p->vCexes) == 0 )
+                goto finish;
         }
         // get initialization patterns
         if ( nRestart && r == nRestart )
@@ -1012,7 +1026,7 @@ finish:
     if ( nSolved )
     {
         if ( fVerbose && !fSolveAll ) Abc_Print( 1, "\n" );
-        Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d POs.    ", nFrames, nNumRestart * nRestart + r, nNumRestart, nSolved );
+        Abc_Print( 1, "Simulation of %d frames for %d rounds with %d restarts asserted %d (out of %d) POs.    ", nFrames, nNumRestart * nRestart + r, nNumRestart, nSolved, Saig_ManPoNum(p->pAig) );
         Abc_PrintTime( 1, "Time", clock() - clkTotal );
     }
     else if ( r == nRounds && f == nFrames )
@@ -1041,10 +1055,11 @@ finish:
 int Ssw_RarSimulateGia( Gia_Man_t * p, int nFrames, int nWords, int nBinSize, int nRounds, int nRestart, int nRandSeed, int TimeOut, int fVerbose )
 {
     int fSolveAll = 0;
+    int fNotVerbose = 0;
     Aig_Man_t * pAig;
     int RetValue;
     pAig = Gia_ManToAigSimple( p );
-    RetValue = Ssw_RarSimulate( pAig, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose );
+    RetValue = Ssw_RarSimulate( pAig, nFrames, nWords, nBinSize, nRounds, nRestart, nRandSeed, TimeOut, fSolveAll, fVerbose, fNotVerbose );
     // save counter-example
     Abc_CexFree( p->pCexSeq );
     p->pCexSeq = pAig->pSeqModel; pAig->pSeqModel = NULL;
@@ -1128,7 +1143,7 @@ int Ssw_RarSignalFilter( Aig_Man_t * pAig, int nFrames, int nWords, int nBinSize
         for ( f = 0; f < nFrames; f++ )
         {
             Ssw_RarManSimulate( p, f ? NULL : p->vInits, 1, !r && !f );
-            if ( fMiter && Ssw_RarManCheckNonConstOutputs(p) )
+            if ( fMiter && Ssw_RarManCheckNonConstOutputs(p, NULL, -1, -1, 0) )
             {
                 if ( !fVerbose )
                     Abc_Print( 1, "%s", Abc_FrameIsBatchMode() ? "\n" : "\r" );
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 7cc5637b..bac4a2dd 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -54,6 +54,7 @@ struct Saig_ParBmc_t_
     int         nFfToAddMax;    // max number of flops to add during CBA
     int         fSkipRand;      // skip random decisions
     int         fVerbose;       // verbose 
+    int         fNotVerbose;    // skip line-by-line print-out 
     int         iFrame;         // explored up to this frame
     int         nFailOuts;      // the number of failed outputs
 };
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index 7ca5c7ba..cd965c06 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1305,6 +1305,7 @@ void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
     p->fSolveAll      =     0;    // stops on the first SAT instance
     p->fDropSatOuts   =     0;    // replace sat outputs by constant 0
     p->fVerbose       =     0;    // verbose 
+    p->fNotVerbose    =     0;    // skip line-by-line print-out 
     p->iFrame         =    -1;    // explored up to this frame
     p->nFailOuts      =     0;    // the number of failed outputs
 }
@@ -1425,8 +1426,9 @@ clkOther += clock() - clk2;
                     return 0;
                 }
                 pPars->nFailOuts++;
-                Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",  
-                    nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
+                if ( !pPars->fNotVerbose )
+                    Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",  
+                        nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
                 if ( p->vCexes == NULL )
                     p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
                 Vec_PtrWriteEntry( p->vCexes, i, pCex );
@@ -1498,8 +1500,9 @@ clkOther += clock() - clk2;
                     return 0;
                 }
                 pPars->nFailOuts++;
-                Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",  
-                    nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
+                if ( !pPars->fNotVerbose )
+                    Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",  
+                        nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
                 if ( p->vCexes == NULL )
                     p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
                 Vec_PtrWriteEntry( p->vCexes, i, pCex );