Skip to content

A
abc
Commit 92da248e by Alan Mishchenko
Options

Disallow the circiut-based solver in &scorr to run with more than 1000 conflicts.

parent b8088b90
Showing with 3 additions and 0 deletions
src/proof/cec/cecCorr.c
...@@ -872,6 +872,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) ...@@ -872,6 +872,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
Cec_ManSatSetDefaultParams( pParsSat ); Cec_ManSatSetDefaultParams( pParsSat );
pParsSat->nBTLimit = pPars->nBTLimit; pParsSat->nBTLimit = pPars->nBTLimit;
pParsSat->fVerbose = pPars->fVerbose; pParsSat->fVerbose = pPars->fVerbose;
// limit the number of conflicts in the circuit-based solver
if ( pPars->fUseCSat )
pParsSat->nBTLimit = Abc_MinInt( pParsSat->nBTLimit, 1000 );
if ( pPars->fVerbose ) if ( pPars->fVerbose )
{ {
Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n", Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n",
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment