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

2 files changed, 5 insertions, 2 deletions

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 );