Misc changes.

src/aig/gia/gia.h

@@ -439,6 +439,8 @@ static inline int Gia_ManAppendCi( Gia_Man_t * p )
 static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 )  
 { 
     Gia_Obj_t * pObj = Gia_ManAppendObj( p );
+    assert( iLit0 >= 0 && Abc_Lit2Var(iLit0) < Gia_ManObjNum(p) );
+    assert( iLit1 >= 0 && Abc_Lit2Var(iLit1) < Gia_ManObjNum(p) );
     assert( iLit0 != iLit1 );
     if ( iLit0 < iLit1 )
     {
@@ -463,7 +465,9 @@ static inline int Gia_ManAppendAnd( Gia_Man_t * p, int iLit0, int iLit1 )
 }
 static inline int Gia_ManAppendCo( Gia_Man_t * p, int iLit0 )  
 { 
-    Gia_Obj_t * pObj = Gia_ManAppendObj( p );
+    Gia_Obj_t * pObj;
+    assert( iLit0 >= 0 && Abc_Lit2Var(iLit0) < Gia_ManObjNum(p) );
+    pObj = Gia_ManAppendObj( p );    
     pObj->fTerm = 1;
     pObj->iDiff0  = Gia_ObjId(p, pObj) - Abc_Lit2Var(iLit0);
     pObj->fCompl0 = Abc_LitIsCompl(iLit0);

src/misc/tim/tim.c

@@ -582,6 +582,7 @@ void Tim_ManCreateBoxFirst( Tim_Man_t * p, int firstIn, int nIns, int firstOut,
 {
     Tim_Box_t * pBox;
     int i;
+//    printf( "Creating %d x %d box with first inputs (%d and %d).\n", nIns, nOuts, firstIn, firstOut );
 
     pBox = (Tim_Box_t *)Mem_FlexEntryFetch( p->pMemObj, sizeof(Tim_Box_t) + sizeof(int) * (nIns+nOuts) );
     memset( pBox, 0, sizeof(Tim_Box_t) );
@@ -847,7 +848,7 @@ float Tim_ManGetCoRequired( Tim_Man_t * p, int iCo )
     if ( p->fUseTravId )
     Tim_ManBoxForEachOutput( p, pBox, pObj, i )
         if ( pObj->TravId != p->nTravIds )
-            printf( "Tim_ManGetCoRequired(): Output required times of the box are not up to date!\n" );
+            printf( "Tim_ManGetCoRequired(): Output required times of output %d the box %d are not up to date!\n", i, pBox->iBox );
     // compute the required times for each input of the box (POs)
     Tim_ManBoxForEachInput( p, pBox, pObjRes, i )
     {
@@ -855,7 +856,7 @@ float Tim_ManGetCoRequired( Tim_Man_t * p, int iCo )
         Tim_ManBoxForEachOutput( p, pBox, pObj, k )
         {
             pDelays = pBox->pDelayTable + k * pBox->nInputs;
-            DelayBest = Abc_MinInt( DelayBest, pObj->timeReq - pDelays[i] );
+            DelayBest = Abc_MinFloat( DelayBest, pObj->timeReq - pDelays[i] );
         }
         pObjRes->timeReq = DelayBest;
         pObjRes->TravId = p->nTravIds;

src/proof/cec/cecCec.c

@@ -143,7 +143,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
         // (for example, when they have the same driver but complemented)
         if ( Gia_ObjPhase(pObj1) != Gia_ObjPhase(pObj2) )
         {
-            Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ.  ", i/2 );
+            Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ (different phase).  ", i/2 );
             Abc_PrintTime( 1, "Time", clock() - clk );
             pPars->iOutFail = i/2;
             Cec_ManTransformPattern( p, i/2, NULL );
@@ -155,7 +155,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
         // drivers are different PIs
         if ( Gia_ObjIsPi(p, pDri1) && Gia_ObjIsPi(p, pDri2) && pDri1 != pDri2 )
         {
-            Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ.  ", i/2 );
+            Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ (different PIs).  ", i/2 );
             Abc_PrintTime( 1, "Time", clock() - clk );
             pPars->iOutFail = i/2;
             Cec_ManTransformPattern( p, i/2, NULL );
@@ -168,7 +168,7 @@ int Cec_ManHandleSpecialCases( Gia_Man_t * p, Cec_ParCec_t * pPars )
         if ( (Gia_ObjIsPi(p, pDri1) && Gia_ObjIsConst0(pDri2)) || 
              (Gia_ObjIsPi(p, pDri2) && Gia_ObjIsConst0(pDri1)) )
         {
-            Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ.  ", i/2 );
+            Abc_Print( 1, "Networks are NOT EQUIVALENT. Outputs %d trivially differ (PI vs. constant).  ", i/2 );
             Abc_PrintTime( 1, "Time", clock() - clk );
             pPars->iOutFail = i/2;
             Cec_ManTransformPattern( p, i/2, NULL );