summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bmc/bmc.h1
-rw-r--r--src/sat/bmc/bmcBmc3.c3
-rw-r--r--src/sat/bmc/module.make1
3 files changed, 4 insertions, 1 deletions
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 65c24e93..ff1e005b 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -65,6 +65,7 @@ struct Saig_ParBmc_t_
int nLearnedPerce; // ratio of learned clause limit
int fVerbose; // verbose
int fNotVerbose; // skip line-by-line print-out
+ int fSilent; // completely silent
int iFrame; // explored up to this frame
int nFailOuts; // the number of failed outputs
int nDropOuts; // the number of dropped outputs
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index ed8f089a..ea08c1e4 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1397,7 +1397,8 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
}
if ( nTimeToStop && Abc_Clock() > nTimeToStop )
{
- Abc_Print( 1, "Reached timeout (%d seconds).\n", pPars->nTimeOut );
+ if ( !pPars->fSilent )
+ Abc_Print( 1, "Reached timeout (%d seconds).\n", pPars->nTimeOut );
goto finish;
}
// skip solved outputs
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
index e567e92b..82d18fde 100644
--- a/src/sat/bmc/module.make
+++ b/src/sat/bmc/module.make
@@ -8,4 +8,5 @@ SRC += src/sat/bmc/bmcBmc.c \
src/sat/bmc/bmcCexMin2.c \
src/sat/bmc/bmcCexTools.c \
src/sat/bmc/bmcLoad.c \
+ src/sat/bmc/bmcMulti.c \
src/sat/bmc/bmcUnroll.c