diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2007-01-23 08:01:00 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2007-01-23 08:01:00 -0800 |
| commit | b1a913fb5e85ba04646632f3d771ad79bfd8a720 (patch) | |
| tree | 672fd9d1e3f52bf9be192cb91355e2eee6b14302 /src/base/abci/abcProve.c | |
| parent | 2167d6c148191f7aa65381bb0618b64050bf4de3 (diff) | |
| download | abc-b1a913fb5e85ba04646632f3d771ad79bfd8a720.tar.gz abc-b1a913fb5e85ba04646632f3d771ad79bfd8a720.tar.bz2 abc-b1a913fb5e85ba04646632f3d771ad79bfd8a720.zip | |
Version abc70123
Diffstat (limited to 'src/base/abci/abcProve.c')
| -rw-r--r-- | src/base/abci/abcProve.c | 6 |
1 files changed, 3 insertions, 3 deletions
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c index d206ae6e..6d1ed161 100644 --- a/src/base/abci/abcProve.c +++ b/src/base/abci/abcProve.c @@ -79,7 +79,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars ) if ( !pParams->fUseRewriting && !pParams->fUseFraiging ) { clk = clock(); - RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, 0, NULL, NULL ); + RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)0, 0, NULL, NULL ); Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose ); *ppNtk = pNtk; return RetValue; @@ -99,7 +99,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars ) // try brute-force SAT clk = clock(); nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0; - RetValue = Abc_NtkMiterSat( pNtk, (sint64)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), (sint64)nInspectLimit, 0, 0, &nSatConfs, &nSatInspects ); + RetValue = Abc_NtkMiterSat( pNtk, (sint64)(pParams->nMiteringLimitStart * pow(pParams->nMiteringLimitMulti,nIter)), (sint64)nInspectLimit, 0, &nSatConfs, &nSatInspects ); Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose ); if ( RetValue >= 0 ) break; @@ -213,7 +213,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, void * pPars ) } clk = clock(); nInspectLimit = pParams->nTotalInspectLimit? pParams->nTotalInspectLimit - pParams->nTotalInspectsMade : 0; - RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)nInspectLimit, 0, 0, NULL, NULL ); + RetValue = Abc_NtkMiterSat( pNtk, (sint64)pParams->nMiteringLimitLast, (sint64)nInspectLimit, 0, NULL, NULL ); Abc_NtkMiterPrint( pNtk, "SAT solving", clk, pParams->fVerbose ); } |