Experiments with recent ideas.

src/sat/bmc/bmcLilac.c

@@ -219,13 +219,11 @@ int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int
             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;
+                printf( "Reached a fixed point after %d frames.  \n", f+1 );
+            break;
         }
         // create new part
         pPart = Bmc_LilacPart( pNew, vSatMap, vMiters, vPartMap, vCopies );
@@ -288,6 +286,7 @@ int Bmc_LilacPerform( Gia_Man_t * p, Vec_Int_t * vInit0, Vec_Int_t * vInit1, int
         }
         if ( fVerbose )
         {
+            printf( "Frame %4d : ",     f+1 );
             printf( "Vars =%7d  ",      nSatVars );
             printf( "Clause =%10d  ",   sat_solver_nclauses(pSat) );
             printf( "Conflict =%10d  ", sat_solver_nconflicts(pSat) );

src/sat/bmc/bmcTulip.c

@@ -239,7 +239,7 @@ Vec_Int_t * Gia_ManTulipPerform( Gia_Man_t * p, Vec_Int_t * vInit, int nFrames,
     Gia_ManForEachPi( pM, pObj, i )
         if ( i == Gia_ManRegNum(p) )
             break;
-        else if ( (Vec_IntEntry(vLits, i) & 2) && !Vec_IntEntry( vMap, pCnf->pVarNums[Gia_ObjId(pM, pObj)] ) )
+        else if ( (Vec_IntEntry(vLits, i) & 2) && Vec_IntEntry( vMap, pCnf->pVarNums[Gia_ObjId(pM, pObj)] ) )
             Vec_IntWriteEntry( vLits, i, (Vec_IntEntry(vLits, i) & 1) );
     Vec_IntFree( vMap );