From 33001946f0e55ae4b0f93d6f2d3cd63214f17010 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 5 Dec 2025 21:14:01 -0800
Subject: [PATCH] Accidental bug.

---
 src/sat/bmc/bmcMaj8.c | 9 +++++----
 1 file changed, 5 insertions(+), 4 deletions(-)

diff --git a/src/sat/bmc/bmcMaj8.c b/src/sat/bmc/bmcMaj8.c
index 2ae25c8b5..465453d81 100644
--- a/src/sat/bmc/bmcMaj8.c
+++ b/src/sat/bmc/bmcMaj8.c
@@ -733,10 +733,10 @@ int Exa8_ManExactSynthesis( Bmc_EsPar_t * pPars )
         word * pFun = Abc_TtSymFunGenerate( pPars->pSymStr, pPars->nVars );
         pPars->pTtStr = ABC_CALLOC( char, pPars->nVars > 2 ? (1 << (pPars->nVars-2)) + 1 : 2 );
         Extra_PrintHexadecimalString( pPars->pTtStr, (unsigned *)pFun, pPars->nVars );
-        if ( !pPars->fSilent ) printf( "Generated symmetric function: %s\n", pPars->pTtStr );
+        if ( !pPars->fSilent && pPars->nVars <= 7 ) printf( "Generated symmetric function: %s\n", pPars->pTtStr );
         ABC_FREE( pFun );
     }
-    if ( pPars->pTtStr && pPars->nVars <= 7 )
+    if ( pPars->pTtStr )
         Abc_TtReadHex( pTruth, pPars->pTtStr );
     else assert( 0 );
     if ( pPars->fUseIncr && !pPars->fSilent )
@@ -822,7 +822,7 @@ int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars )
     int nNodeMax = pPars->nNodes, Result = 0;
     int fGenPerm = pPars->pPermStr == NULL;
     for ( int n = nNodeMin; n <= nNodeMax; n++ ) {
-        printf( "\nTrying M = %d:\n", n );
+        if ( !pPars->fSilent ) printf( "\nTrying M = %d:\n", n );
         pPars->nNodes = n;
         if ( !pPars->fUsePerm && fGenPerm ) {
             Vec_Str_t * vStr = Vec_StrAlloc( 100 );
@@ -905,7 +905,7 @@ int Exa8_ManExactSynthesisIter( Bmc_EsPar_t * pPars )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Ptr_t * Exa8_ManExactSynthesisPopcount( int nVars )
+Vec_Ptr_t * Exa8_ManExactSynthesisPopcount( int nVars, int fVerbose )
 {
     Bmc_EsPar_t Pars, * pPars = &Pars;
     Bmc_EsParSetDefault( pPars );
@@ -914,6 +914,7 @@ Vec_Ptr_t * Exa8_ManExactSynthesisPopcount( int nVars )
     pPars->fMinNodes   = 1;
     pPars->fUsePerm    = 1;
     pPars->fGenTruths  = 1;
+    pPars->fSilent     = !fVerbose;
     pPars->nLutSize    = 6;
     int v, o, nOuts = Abc_Base2Log(nVars+1);
     Vec_Ptr_t * vRes = Vec_PtrAlloc( nOuts );