Experiments with BMC.

src/base/abci/abc.c

@@ -39986,7 +39986,7 @@ int Abc_CommandAbc9SBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     Bmc_AndPar_t Pars, * pPars = &Pars; int c;
     memset( pPars, 0, sizeof(Bmc_AndPar_t) );
     pPars->nStart        =    0;  // starting timeframe
-    pPars->nFramesMax    =  100;  // maximum number of timeframes
+    pPars->nFramesMax    =    0;  // maximum number of timeframes
     pPars->nFramesAdd    =    0;  // the number of additional frames
     pPars->nConfLimit    =    0;  // maximum number of conflicts at a node
     pPars->nTimeOut      =    0;  // timeout in seconds

src/sat/bmc/bmcBmcS.c

@@ -473,7 +473,7 @@ Gia_Man_t * Bmcs_ManUnfold( Bmcs_Man_t * p, int f )
     // create a clean copy of the new nodes of this timeframe
     Vec_IntFillExtra( &p->vFr2Sat, Gia_ManObjNum(p->pFrames), -1 );
     Vec_IntFillExtra( &p->pFrames->vCopies, Gia_ManObjNum(p->pFrames), -1 );
-    assert( Vec_IntCountEntry(&p->pFrames->vCopies, -1) == Vec_IntSize(&p->pFrames->vCopies) );
+    //assert( Vec_IntCountEntry(&p->pFrames->vCopies, -1) == Vec_IntSize(&p->pFrames->vCopies) );
     Gia_ManStopP( &p->pClean );
     p->pClean = Gia_ManStart( Gia_ManObjNum(p->pFrames) - nFrameObjs + 1000 );
     Gia_ObjSetCopyArray( p->pFrames, 0, 0 );