Several bug fixes and silencing requests.

3 files changed, 10 insertions, 6 deletions

diff --git a/src/proof/cec/cec.h b/src/proof/cec/cec.h
index 3fb5d0b0..805a5d73 100644
--- a/src/proof/cec/cec.h
+++ b/src/proof/cec/cec.h
@@ -210,7 +210,7 @@ extern void          Cec_ManFraSetDefaultParams( Cec_ParFra_t * p );
 extern void          Cec_ManCecSetDefaultParams( Cec_ParCec_t * p );
 extern void          Cec_ManCorSetDefaultParams( Cec_ParCor_t * p );
 extern void          Cec_ManChcSetDefaultParams( Cec_ParChc_t * p );
-extern Gia_Man_t *   Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars );
+extern Gia_Man_t *   Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSilent );
 extern Gia_Man_t *   Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars );
 extern void          Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars );
 /*=== cecSeq.c ==========================================================*/
diff --git a/src/proof/cec/cecCec.c b/src/proof/cec/cecCec.c
index d6e8456d..1465a721 100644
--- a/src/proof/cec/cecCec.c
+++ b/src/proof/cec/cecCec.c
@@ -358,7 +358,7 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
     pParsFra->fVerbose     = pPars->fVerbose;
     pParsFra->fCheckMiter  = 1;
     pParsFra->fDualOut     = 1;
-    pNew = Cec_ManSatSweeping( p, pParsFra );
+    pNew = Cec_ManSatSweeping( p, pParsFra, pPars->fSilent );
     pPars->iOutFail = pParsFra->iOutFail;
     // update
     pInit->pCexComb = p->pCexComb; p->pCexComb = NULL;
@@ -371,8 +371,11 @@ int Cec_ManVerify( Gia_Man_t * pInit, Cec_ParCec_t * pPars )
         {
             if ( p->pCexComb && !Gia_ManVerifyCex( p, p->pCexComb, 1 ) )
                 Abc_Print( 1, "Counter-example simulation has failed.\n" );
+            if ( !pPars->fSilent )
+            {
             Abc_Print( 1, "Networks are NOT EQUIVALENT.  " );
             Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+            }
             return 0;
         }
         p = Gia_ManDup( pInit );
@@ -542,7 +545,7 @@ Aig_Man_t * Cec_FraigCombinational( Aig_Man_t * pAig, int nConfs, int fVerbose )
     pFraPars->nItersMax = 20;
     pFraPars->fVerbose  = fVerbose;
     pGia = Gia_ManFromAigSimple( pAig );
-    Cec_ManSatSweeping( pGia, pFraPars );
+    Cec_ManSatSweeping( pGia, pFraPars, 0 );
     Gia_ManReprToAigRepr( pAig, pGia );
     Gia_ManStop( pGia );
     return Aig_ManDupSimple( pAig );
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c
index 71335e85..c9e9f67a 100644
--- a/src/proof/cec/cecCore.c
+++ b/src/proof/cec/cecCore.c
@@ -334,7 +334,7 @@ void Cec_ManSimulation( Gia_Man_t * pAig, Cec_ParSim_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
+Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars, int fSilent )
 {
     int fOutputResult = 0;
     Cec_ParSat_t ParsSat, * pParsSat = &ParsSat;
@@ -521,12 +521,13 @@ finalize:
     pTemp = p->pAig; p->pAig = NULL;
     if ( pTemp == NULL && pSim->iOut >= 0 )
     {
+        if ( !fSilent )
         Abc_Print( 1, "Disproved at least one output of the miter (zero-based number %d).\n", pSim->iOut );
         pPars->iOutFail = pSim->iOut;
     }
-    else if ( pSim->pCexes )
+    else if ( pSim->pCexes && !fSilent )
         Abc_Print( 1, "Disproved %d outputs of the miter.\n", pSim->nOuts );
-    if ( fTimeOut )
+    if ( fTimeOut && !fSilent )
         Abc_Print( 1, "Timed out after %d seconds.\n", (int)((double)Abc_Clock() - clkTotal)/CLOCKS_PER_SEC );
 
     pAig->pCexComb = pSim->pCexComb; pSim->pCexComb = NULL;