From 92da248e9a1400280d0e4674923e0f572465530d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Tue, 24 Apr 2012 15:49:40 -0700 Subject: Disallow the circiut-based solver in &scorr to run with more than 1000 conflicts. --- src/proof/cec/cecCorr.c | 3 +++ 1 file changed, 3 insertions(+) (limited to 'src/proof/cec/cecCorr.c') 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", -- cgit v1.2.3