summaryrefslogtreecommitdiffstats
path: root/src/aig/saig/saigBmc2.c
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2012-02-19 09:55:52 -0800
committerAlan Mishchenko <alanmi@berkeley.edu>2012-02-19 09:55:52 -0800
commitc9147d76cc6fe6b9add5a84e02c0fce2a399cc9f (patch)
tree603c14d04cfddae2dbe7137fcf9d6b31308cbeaf /src/aig/saig/saigBmc2.c
parent7ca9c116df0475d567d6fbc616b454f40a44003c (diff)
downloadabc-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.c3
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 );