Several bug fixes and silencing requests.

6 files changed, 17 insertions, 11 deletions

diff --git a/src/aig/gia/giaFx.c b/src/aig/gia/giaFx.c
index 73a8cf5c..4fff177c 100644
--- a/src/aig/gia/giaFx.c
+++ b/src/aig/gia/giaFx.c
@@ -282,7 +282,7 @@ Vec_Int_t * Gia_ManFxTopoOrder( Vec_Wec_t * vCubes, int nInputs, int nStart, Vec
     // quit if there is no new nodes
     if ( nNodeMax == nStart )
     {
-        printf( "The network is unchanged by fast extract.\n" );
+        //printf( "The network is unchanged by fast extract.\n" );
         return NULL;
     }
     // find first cube and how many cubes
@@ -459,6 +459,8 @@ Gia_Man_t * Gia_ManPerformFx( Gia_Man_t * p, int nNewNodesMax, int LitCountMax,
     Gia_Man_t * pNew = NULL;
     Vec_Wec_t * vCubes;
     Vec_Str_t * vCompl;
+    if ( Gia_ManAndNum(p) == 0 )
+        return Gia_ManDup(p);
 //    abctime clk;
     assert( Gia_ManHasMapping(p) );   
     // collect information
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index de96b546..10a6f191 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -30301,7 +30301,7 @@ int Abc_CommandAbc9Fraig( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -1, "Abc_CommandAbc9Fraig(): There is no AIG.\n" );
         return 1;
     }
-    pTemp = Cec_ManSatSweeping( pAbc->pGia, pPars );
+    pTemp = Cec_ManSatSweeping( pAbc->pGia, pPars, 0 );
     Abc_FrameUpdateGia( pAbc, pTemp );
     return 0;
 
diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c
index 8143be6c..dcf018b7 100644
--- a/src/base/wlc/wlcReadSmt.c
+++ b/src/base/wlc/wlcReadSmt.c
@@ -706,12 +706,12 @@ static inline char * Smt_PrsLoadFile( char * pFileName, char ** ppLimit )
     // move the file current reading position to the beginning
     rewind( pFile ); 
     // load the contents of the file into memory
-    pBuffer = ABC_ALLOC( char, nFileSize + 3 );
+    pBuffer = ABC_ALLOC( char, nFileSize + 16 );
     pBuffer[0] = '\n';
     RetValue = fread( pBuffer+1, nFileSize, 1, pFile );
     // terminate the string with '\0'
-    pBuffer[nFileSize + 0] = '\n';
-    pBuffer[nFileSize + 1] = '\0';
+    pBuffer[nFileSize + 1] = '\n';
+    pBuffer[nFileSize + 2] = '\0';
     *ppLimit = pBuffer + nFileSize + 2;
     return pBuffer;
 }
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;