diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-02-19 09:55:52 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-02-19 09:55:52 -0800 |
commit | c9147d76cc6fe6b9add5a84e02c0fce2a399cc9f (patch) | |
tree | 603c14d04cfddae2dbe7137fcf9d6b31308cbeaf /src/aig/saig/saigBmc2.c | |
parent | 7ca9c116df0475d567d6fbc616b454f40a44003c (diff) | |
download | abc-c9147d76cc6fe6b9add5a84e02c0fce2a399cc9f.tar.gz abc-c9147d76cc6fe6b9add5a84e02c0fce2a399cc9f.tar.bz2 abc-c9147d76cc6fe6b9add5a84e02c0fce2a399cc9f.zip |
Setting the default limit on the number of timeframe in bmc2/bmc3 to 0 (infinity).
Diffstat (limited to 'src/aig/saig/saigBmc2.c')
-rw-r--r-- | src/aig/saig/saigBmc2.c | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c index d172c4c2..40d3bc66 100644 --- a/src/aig/saig/saigBmc2.c +++ b/src/aig/saig/saigBmc2.c @@ -759,7 +759,6 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax vSimInfo = Abs_ManTernarySimulate( pAig, nFramesMax, fVerbose ); Abs_ManFreeAray( vSimInfo ); */ - p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose ); if ( fVerbose ) { printf( "Running \"bmc2\". AIG: PI/PO/Reg = %d/%d/%d. Node = %6d. Lev = %5d.\n", @@ -768,6 +767,8 @@ int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n", nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll ); } + nFramesMax = nFramesMax ? nFramesMax : ABC_INFINITY; + p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose ); // set runtime limit if ( nTimeOut ) sat_solver_set_runtime_limit( p->pSat, nTimeToStop ); |