Experiments with recent ideas.

5 files changed, 202 insertions, 187 deletions

diff --git a/abclib.dsp b/abclib.dsp
index b4dc5dd6..cfdfb1be 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -729,162 +729,10 @@ SOURCE=.\src\base\test\test.c
 # Begin Group "abc2"
 
 # PROP Default_Filter ""
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2_.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2_power.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Blifi.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Blifo.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Core.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Dup.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Equiv.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Extract.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Flatten.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Func.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Fx.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Gia.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Hash.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Insert.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Logic.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Map.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Merge.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Mfs.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Multi.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Ntk.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Part.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Print.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Rec.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Slack.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Strash.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Time.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Truth.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Util.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Veri.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Verify.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2\abc2Vero.c
-# End Source File
 # End Group
 # Begin Group "abc2d"
 
 # PROP Default_Filter ""
-# Begin Source File
-
-SOURCE=.\src\base\abc2d\abc2d.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2d\ast2.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2d\magic.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2d\magic.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\base\abc2d\util.c
-# End Source File
 # End Group
 # End Group
 # Begin Group "bdd"
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index e78cb849..d3ee3f48 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -293,6 +293,43 @@ void Gia_ManPrintTents( Gia_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManPrintInitClasses( Vec_Int_t * vInits )
+{
+    int i, Value;
+    int Counts[4] = {0};
+    Vec_IntForEachEntry( vInits, Value, i )
+        Counts[Value]++;
+    for ( i = 0; i < 4; i++ )
+        printf( "%d = %d  ", i, Counts[i] );
+    printf( "X = %d\n", Counts[2] + Counts[3] );
+    Vec_IntForEachEntry( vInits, Value, i )
+    {
+        Counts[Value]++;
+        if ( Value == 0 )
+            printf( "0" );
+        else if ( Value == 1 )
+            printf( "1" );
+        else if ( Value == 2 )
+            printf( "x" );
+        else if ( Value == 3 )
+            printf( "X" );
+        else assert( 0 );
+    }
+    printf( "\n" );
+    
+}
+
+/**Function*************************************************************
+
   Synopsis    [Prints stats for the AIG.]
 
   Description []
@@ -385,6 +422,8 @@ void Gia_ManPrintStats( Gia_Man_t * p, Gps_Par_t * pPars )
     Gia_ManPrintFlopClasses( p );
     Gia_ManPrintGateClasses( p );
     Gia_ManPrintObjClasses( p );
+    if ( p->vInitClasses )
+        Gia_ManPrintInitClasses( p->vInitClasses );
     if ( pPars && pPars->fTents )
     {
 /*
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d3fcb137..e54a62e9 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -400,6 +400,7 @@ static int Abc_CommandAbc9ICheck             ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9SatTest            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9FunFaTest          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Tulip              ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Lilac              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9PoPart2            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexCut             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 //static int Abc_CommandAbc9CexMerge           ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -964,6 +965,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&sattest",      Abc_CommandAbc9SatTest,      0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&funfatest",    Abc_CommandAbc9FunFaTest,    0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&tulip",        Abc_CommandAbc9Tulip,        0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&lilac",        Abc_CommandAbc9Lilac,        0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&popart2",      Abc_CommandAbc9PoPart2,      0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexcut",       Abc_CommandAbc9CexCut,       0 );
 //    Cmd_CommandAdd( pAbc, "ABC9",         "&cexmerge",     Abc_CommandAbc9CexMerge,     0 );
@@ -32820,7 +32822,99 @@ int Abc_CommandAbc9Tulip( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 usage:
     Abc_Print( -2, "usage: &tulip [-FWT num] [-svh]\n" );
-    Abc_Print( -2, "\t         experimental prcedure for testing new ideas\n" );
+    Abc_Print( -2, "\t         experimental procedure\n" );
+    Abc_Print( -2, "\t-F num : the number of timeframes [default = %d]\n",                    nFrames );
+    Abc_Print( -2, "\t-W num : the number of machine words [default = %d]\n",                 nWords );
+    Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", nTimeOut );
+    Abc_Print( -2, "\t-s     : toggles using ternary simulation [default = %s]\n",            fSim?     "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n",        fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9Lilac( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern Vec_Int_t * Gia_ManLilacTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose );
+    Vec_Int_t * vTemp;
+    int c, nFrames = 1000, nWords = 1000, nTimeOut = 0, fSim = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FWTsvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFrames = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFrames < 0 )
+                goto usage;
+            break;
+        case 'W':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-W\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nWords = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nWords < 0 )
+                goto usage;
+            break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nTimeOut = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nTimeOut < 0 )
+                goto usage;
+            break;
+        case 's':
+            fSim ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Lilac(): There is no AIG.\n" );
+        return 0;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9Lilac(): AIG is combinational.\n" );
+        return 0;
+    }
+    pAbc->pGia->vInitClasses = Gia_ManLilacTest( pAbc->pGia, vTemp = pAbc->pGia->vInitClasses, nFrames, nWords, nTimeOut, fSim, fVerbose );
+    Vec_IntFreeP( &vTemp );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &lilac [-FWT num] [-svh]\n" );
+    Abc_Print( -2, "\t         experimental procedure\n" );
     Abc_Print( -2, "\t-F num : the number of timeframes [default = %d]\n",                    nFrames );
     Abc_Print( -2, "\t-W num : the number of machine words [default = %d]\n",                 nWords );
     Abc_Print( -2, "\t-T num : approximate global runtime limit in seconds [default = %d]\n", nTimeOut );
diff --git a/src/sat/bmc/bmcLilac.c b/src/sat/bmc/bmcLilac.c
index e1386061..1d41312b 100644
--- a/src/sat/bmc/bmcLilac.c
+++ b/src/sat/bmc/bmcLilac.c
@@ -115,40 +115,47 @@ void Bmc_LilacUnfold( Gia_Man_t * pNew, Gia_Man_t * p, Vec_Int_t * vFFLits, int
   SeeAlso     []
 
 ***********************************************************************/
-int Bmc_LilacPart_rec( Gia_Man_t * pNew, Vec_Int_t * vSatMap, int iIdNew, Gia_Man_t * pPart, Vec_Int_t * vPartMap )
+int Bmc_LilacPart_rec( Gia_Man_t * pNew, Vec_Int_t * vSatMap, int iIdNew, Gia_Man_t * pPart, Vec_Int_t * vPartMap, Vec_Int_t * vCopies )
 {
     Gia_Obj_t * pObj = Gia_ManObj( pNew, iIdNew ); 
-    int iLitPart0, iLitPart1;
-    if ( pObj->Value )
-        return pObj->Value;
-    if ( Vec_IntEntry(vSatMap, iIdNew) )
+    int iLitPart0, iLitPart1, iRes;
+    if ( Vec_IntEntry(vCopies, iIdNew) )
+        return Vec_IntEntry(vCopies, iIdNew);
+    if ( Vec_IntEntry(vSatMap, iIdNew) >= 0 || Gia_ObjIsCi(pObj) )
     {
         Vec_IntPush( vPartMap, iIdNew );
-        return (pObj->Value = Gia_ManAppendCi(pPart));
+        iRes = Gia_ManAppendCi(pPart);
+        Vec_IntWriteEntry( vCopies, iIdNew, iRes );
+        return iRes;
     }
-    iLitPart0 = Bmc_LilacPart_rec( pNew, vSatMap, Gia_ObjFaninId0(pObj, iIdNew), pPart, vPartMap );
-    iLitPart1 = Bmc_LilacPart_rec( pNew, vSatMap, Gia_ObjFaninId1(pObj, iIdNew), pPart, vPartMap );
+    assert( Gia_ObjIsAnd(pObj) );
+    iLitPart0 = Bmc_LilacPart_rec( pNew, vSatMap, Gia_ObjFaninId0(pObj, iIdNew), pPart, vPartMap, vCopies );
+    iLitPart1 = Bmc_LilacPart_rec( pNew, vSatMap, Gia_ObjFaninId1(pObj, iIdNew), pPart, vPartMap, vCopies );
     iLitPart0 = Abc_LitNotCond( iLitPart0, Gia_ObjFaninC0(pObj) );
     iLitPart1 = Abc_LitNotCond( iLitPart1, Gia_ObjFaninC1(pObj) );
     Vec_IntPush( vPartMap, iIdNew );
-    return (pObj->Value = Gia_ManAppendAnd( pPart, iLitPart0, iLitPart1 ));
+    iRes = Gia_ManAppendAnd( pPart, iLitPart0, iLitPart1 );
+    Vec_IntWriteEntry( vCopies, iIdNew, iRes );
+    return iRes;
 }
-Gia_Man_t * Bmc_LilacPart( Gia_Man_t * pNew, Vec_Int_t * vSatMap, Vec_Int_t * vMiters, Vec_Int_t * vPartMap )
+Gia_Man_t * Bmc_LilacPart( Gia_Man_t * pNew, Vec_Int_t * vSatMap, Vec_Int_t * vMiters, Vec_Int_t * vPartMap, Vec_Int_t * vCopies )
 {
     Gia_Man_t * pPart;
     int i, iLit, iLitPart;
-    Gia_ManCleanValue( pNew );
+    Vec_IntFill( vCopies, Gia_ManObjNum(pNew), 0 );
     Vec_IntFillExtra( vSatMap, Gia_ManObjNum(pNew), -1 );
     pPart = Gia_ManStart( 1000 );
     pPart->pName = Abc_UtilStrsav( pNew->pName );
-    Gia_ManConst0(pNew)->Value = 0;
     Vec_IntClear( vPartMap );
+    Vec_IntPush( vPartMap, 0 );
     Vec_IntForEachEntry( vMiters, iLit, i )
     {
         if ( iLit == -1 )
             continue;
-        iLitPart = Bmc_LilacPart_rec( pNew, vSatMap, Abc_Lit2Var(iLit), pPart, vPartMap );
+        assert( iLit >= 2 );
+        iLitPart = Bmc_LilacPart_rec( pNew, vSatMap, Abc_Lit2Var(iLit), pPart, vPartMap, vCopies );
         Gia_ManAppendCo( pPart, Abc_LitNotCond(iLitPart, Abc_LitIsCompl(iLit)) );
+        Vec_IntPush( vPartMap, -1 );
     }
     assert( Gia_ManPoNum(pPart) > 0 );
     assert( Vec_IntSize(vPartMap) == Gia_ManObjNum(pPart) );
@@ -166,17 +173,16 @@ Gia_Man_t * Bmc_LilacPart( Gia_Man_t * pNew, Vec_Int_t * vSatMap, Vec_Int_t * vM
   SeeAlso     []
 
 ***********************************************************************/
-int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int nFrames, int fVerbose )
+int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int nFrames, int nWords, int nTimeOut, int fVerbose )
 {
     int nSatVars = 1;
-    int nTimeOut = 0;
-    Vec_Int_t * vLits0, * vLits1, * vMiters, * vSatMap, * vPartMap;
+    Vec_Int_t * vLits0, * vLits1, * vMiters, * vSatMap, * vPartMap, * vCopies;
     Gia_Man_t * pNew, * pPart;
     Gia_Obj_t * pObj;
     Cnf_Dat_t * pCnf;
     sat_solver * pSat;
-    int i, f, status, iVar0, iVar1, iLit, iLit0, iLit1;
-    int fChanges, RetValue = 1;
+    int iVar0, iVar1, iLit, iLit0, iLit1;
+    int i, f, status, nChanges, nMiters, RetValue = 1;
 
     // start the SAT solver
     pSat = sat_solver_new();
@@ -198,21 +204,31 @@ int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int
     vMiters  = Vec_IntAlloc( 1000 );
     vSatMap  = Vec_IntAlloc( 1000 );
     vPartMap = Vec_IntAlloc( 1000 );
+    vCopies  = Vec_IntAlloc( 1000 );
     for ( f = 0; f < nFrames; f++ )
     {
+        abctime clk = Abc_Clock();
         Bmc_LilacUnfold( pNew, p, vLits0, 0 );
         Bmc_LilacUnfold( pNew, p, vLits1, 1 );
         assert( Vec_IntSize(vLits0) == Vec_IntSize(vLits1) );
+        nMiters  = 0;
         Vec_IntClear( vMiters );
         Vec_IntForEachEntryTwo( vLits0, vLits1, iLit0, iLit1, i )
-            if ( (iLit0 > 2 || iLit1 > 2) && iLit0 != iLit1 )
-                Vec_IntPush( vMiters, Gia_ManHashXor(pNew, iLit0, iLit1) );
+            if ( (iLit0 >= 2 || iLit1 >= 2) && iLit0 != iLit1 )
+                Vec_IntPush( vMiters, Gia_ManHashXor(pNew, iLit0, iLit1) ), nMiters++;
             else
                 Vec_IntPush( vMiters, -1 );
+        assert( Vec_IntSize(vMiters) == Gia_ManRegNum(p) );
+        if ( fVerbose )
+            printf( "Frame %4d : ", f );
         if ( Vec_IntSum(vMiters) + Vec_IntSize(vLits1) == 0 )
+        {
+            if ( fVerbose )
+                printf( "Trivial\n" );
             continue;
+        }
         // create new part
-        pPart = Bmc_LilacPart( pNew, vSatMap, vMiters, vPartMap );
+        pPart = Bmc_LilacPart( pNew, vSatMap, vMiters, vPartMap, vCopies );
         pCnf = Cnf_DeriveGiaRemapped( pPart );
         Cnf_DataLiftGia( pCnf, pPart, nSatVars );
         nSatVars += pCnf->nVars;
@@ -223,28 +239,35 @@ int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int
         // stitch the clauses
         Gia_ManForEachPi( pPart, pObj, i )
         {
-            int iIdPart = Gia_ObjId(pPart, pObj);
-            iVar0 = pCnf->pVarNums[iIdPart];
-            iVar1 = Vec_IntEntry( vSatMap, Vec_IntEntry(vPartMap, iIdPart) );
+            iVar0 = pCnf->pVarNums[Gia_ObjId(pPart, pObj)];
+            iVar1 = Vec_IntEntry( vSatMap, Vec_IntEntry(vPartMap, Gia_ObjId(pPart, pObj)) );
             if ( iVar1 == -1 )
                 continue;
             sat_solver_add_buffer( pSat, iVar0, iVar1, 0 );
         }
         // transfer variables
-        Gia_ManForEachAnd( pPart, pObj, i )
+        Gia_ManForEachCand( pPart, pObj, i )
             if ( pCnf->pVarNums[i] >= 0 )
+            {
+                assert( Gia_ObjIsCi(pObj) || Vec_IntEntry( vSatMap, Vec_IntEntry(vPartMap, i) ) == -1 );
                 Vec_IntWriteEntry( vSatMap, Vec_IntEntry(vPartMap, i), pCnf->pVarNums[i] );
+            }
         Cnf_DataFree( pCnf );
         Gia_ManStop( pPart );
         // perform runs
-        fChanges = 0;
+        nChanges = 0;
         Vec_IntForEachEntry( vMiters, iLit, i )
         {
             if ( iLit == -1 )
                 continue;
+            assert( Vec_IntEntry(vSatMap, Abc_Lit2Var(iLit)) > 0 );
+            iLit = Abc_Lit2LitV( Vec_IntArray(vSatMap), iLit );
             status = sat_solver_solve( pSat, &iLit, &iLit + 1, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
             if ( status == l_True )
+            {
+                nChanges++;
                 continue;
+            }
             if ( status == l_Undef )
             {
                 printf( "Timeout reached after %d seconds.  \n", nTimeOut );
@@ -254,17 +277,26 @@ int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int
             assert( status == l_False );
             iLit0 = Vec_IntEntry( vLits0, i );
             iLit1 = Vec_IntEntry( vLits1, i );
-            assert( (iLit0 > 2 || iLit1 > 2) && iLit0 != iLit1 );
-            if ( iLit1 > 2 )
+            assert( (iLit0 >= 2 || iLit1 >= 2) && iLit0 != iLit1 );
+            if ( iLit1 >= 2 )
                 Vec_IntWriteEntry( vLits1, i, iLit0 );
             else
                 Vec_IntWriteEntry( vLits0, i, iLit1 );
             iLit0 = Vec_IntEntry( vLits0, i );
             iLit1 = Vec_IntEntry( vLits1, i );
             assert( iLit0 == iLit1 );
-            fChanges = 1;
         }
-        if ( !fChanges )
+        if ( fVerbose )
+        {
+            printf( "Vars =%7d  ",      nSatVars );
+            printf( "Clause =%10d  ",   sat_solver_nclauses(pSat) );
+            printf( "Conflict =%10d  ", sat_solver_nconflicts(pSat) );
+            printf( "AIG =%7d  ",       Gia_ManAndNum(pNew) );
+            printf( "Miters =%5d  ",    nMiters );
+            printf( "SAT =%5d  ",       nChanges );
+            Abc_PrintTime( 1, "Time",   Abc_Clock() - clk );
+        }
+        if ( nChanges == 0 )
         {
             printf( "Reached a fixed point after %d frames.  \n", f+1 );
             break;
@@ -279,6 +311,7 @@ cleanup:
     Vec_IntFree( vMiters );
     Vec_IntFree( vSatMap );
     Vec_IntFree( vPartMap );
+    Vec_IntFree( vCopies );
     return RetValue;
 }
 
@@ -293,9 +326,11 @@ cleanup:
   SeeAlso     []
 
 ***********************************************************************/
-void Bmc_LilacTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int fVerbose )
+void Gia_ManLilacTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int nWords, int nTimeOut, int fSim, int fVerbose )
 {
-    Bmc_LilacPerform( p, vInit, vInit, nFrames, fVerbose );
+    Vec_Int_t * vInit0 = Vec_IntStart( Gia_ManRegNum(p) );
+    Bmc_LilacPerform( p, vInit, vInit0, nFrames, nWords, nTimeOut, fVerbose );
+    Vec_IntFree( vInit0 );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/bmc/bmcTulip.c b/src/sat/bmc/bmcTulip.c
index 29e8781f..8c32d699 100644
--- a/src/sat/bmc/bmcTulip.c
+++ b/src/sat/bmc/bmcTulip.c
@@ -481,9 +481,9 @@ Vec_Int_t * Gia_ManRosePerform( Gia_Man_t * p, Vec_Int_t * vInit0, int nFrames,
     Gia_ParTestFree( p );
     printf( "After %d frames, found a sequence to produce %d x-values (out of %d).  ", f, Cost, Gia_ManRegNum(p) );
     Abc_PrintTime( 1, "Total runtime", Abc_Clock() - clkTotal );
-//    Vec_IntFreeP( &vInit );
     Vec_IntFill(vInit, Vec_IntSize(vInit), 2);
 //    printf( "The resulting init state is invalid.\n" );
+    Vec_IntFreeP( &vInit );
     return vInit;
 }
 
@@ -505,7 +505,6 @@ Vec_Int_t * Gia_ManTulipTest( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames, int
         vRes = Gia_ManRosePerform( p, vInit, nFrames, nWords, fVerbose );
     else
         vRes = Gia_ManTulipPerform( p, vInit, nFrames, nTimeOut, fVerbose );
-    Vec_IntFreeP( &vRes );
     return vRes;
 }