From 272089221a530f61bceee07378cb747c88471b70 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 27 Mar 2013 12:51:57 -0700 Subject: Removing hard-coded limit on the number of solving iterations in command 'qbf'. --- src/base/abci/abcQbf.c | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) (limited to 'src/base/abci/abcQbf.c') diff --git a/src/base/abci/abcQbf.c b/src/base/abci/abcQbf.c index 86755433..abbcc172 100644 --- a/src/base/abci/abcQbf.c +++ b/src/base/abci/abcQbf.c @@ -65,7 +65,7 @@ void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fVerbose ) Abc_Ntk_t * pNtkVer, * pNtkSyn, * pNtkSyn2, * pNtkTemp; Vec_Int_t * vPiValues; clock_t clkTotal = clock(), clkS, clkV; - int nIters, nIterMax = 500, nInputs, RetValue, fFound = 0; + int nIters, nInputs, RetValue, fFound = 0; assert( Abc_NtkIsStrash(pNtk) ); assert( Abc_NtkIsComb(pNtk) ); @@ -96,7 +96,7 @@ void Abc_NtkQbf( Abc_Ntk_t * pNtk, int nPars, int nItersMax, int fVerbose ) } // iteratively solve - for ( nIters = 0; nIters < nIterMax; nIters++ ) + for ( nIters = 0; nIters < nItersMax; nIters++ ) { // solve the synthesis instance clkS = clock(); @@ -170,7 +170,7 @@ clkV = clock() - clkV; printf( "\n" ); printf( "Solved after %d interations. ", nIters ); } - else if ( nIters == nIterMax ) + else if ( nIters == nItersMax ) printf( "Unsolved after %d interations. ", nIters ); else if ( nIters == nItersMax ) printf( "Quit after %d interatios. ", nItersMax ); -- cgit v1.2.3