diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-04-24 15:49:40 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-04-24 15:49:40 -0700 |
| commit | 92da248e9a1400280d0e4674923e0f572465530d (patch) | |
| tree | f268ae830780fd6e1237e3d1ba819f8be960cc89 | |
| parent | b8088b901dac6531b5fa2550f0508262b961a3fe (diff) | |
| download | abc-92da248e9a1400280d0e4674923e0f572465530d.tar.gz abc-92da248e9a1400280d0e4674923e0f572465530d.tar.bz2 abc-92da248e9a1400280d0e4674923e0f572465530d.zip | |
Disallow the circiut-based solver in &scorr to run with more than 1000 conflicts.
| -rw-r--r-- | src/proof/cec/cecCorr.c | 3 |
1 files changed, 3 insertions, 0 deletions
diff --git a/src/proof/cec/cecCorr.c b/src/proof/cec/cecCorr.c index 618d43d4..d080dfea 100644 --- a/src/proof/cec/cecCorr.c +++ b/src/proof/cec/cecCorr.c @@ -872,6 +872,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars ) Cec_ManSatSetDefaultParams( pParsSat ); pParsSat->nBTLimit = pPars->nBTLimit; 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 ) { Abc_Print( 1, "Obj = %7d. And = %7d. Conf = %5d. Fr = %d. Lcorr = %d. Ring = %d. CSat = %d.\n", |