From c30a0ca0b973faf136b309600f03b32b78d0a733 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Tue, 25 Nov 2014 21:57:34 -0800
Subject: Improvements to handling boxes and flops.

---
 src/aig/gia/giaSweep.c  | 5 +++--
 src/aig/gia/giaTim.c    | 1 +
 src/proof/int/intUtil.c | 2 +-
 3 files changed, 5 insertions(+), 3 deletions(-)

diff --git a/src/aig/gia/giaSweep.c b/src/aig/gia/giaSweep.c
index 7d383dc7..70c7a960 100644
--- a/src/aig/gia/giaSweep.c
+++ b/src/aig/gia/giaSweep.c
@@ -634,7 +634,8 @@ Gia_Man_t * Gia_ManSweepWithBoxesAndDomains( Gia_Man_t * p, void * pParsS, int f
     // iterate over domains
     for ( iDom = 1; iDom <= nDoms; iDom++ )
     {
-        if ( Vec_IntCountEntry(pNew->vRegClasses, iDom) < 2 )
+        int nFlops = Vec_IntCountEntry(pNew->vRegClasses, iDom);
+        if ( nFlops < 2 )
             continue;
         // find global equivalences
         pClp = Gia_ManDupCollapse( pNew, pNew->pAigExtra, NULL, 1 );
@@ -655,7 +656,7 @@ Gia_Man_t * Gia_ManSweepWithBoxesAndDomains( Gia_Man_t * p, void * pParsS, int f
         // report
         //if ( fVerbose )
         {
-        printf( "Domain %2d with %5d flops:  ", iDom, Vec_IntCountEntry(pNew->vRegClasses, iDom) );
+        printf( "Domain %2d : %5d -> %5d :  ", iDom, nFlops, Vec_IntCountEntry(pNew->vRegClasses, iDom) );
         Gia_ManPrintStats( pNew, NULL );
         }
     }
diff --git a/src/aig/gia/giaTim.c b/src/aig/gia/giaTim.c
index 1017308a..3704867b 100644
--- a/src/aig/gia/giaTim.c
+++ b/src/aig/gia/giaTim.c
@@ -914,6 +914,7 @@ int Gia_ManVerifyWithBoxes( Gia_Man_t * pGia, int nBTLimit, int nTimeLim, int fS
             Aig_Man_t * pMan;
             Fra_Sec_t SecPar, * pSecPar = &SecPar;
             Fra_SecSetDefaultParams( pSecPar );
+            pSecPar->fRetimeFirst = 0;
             pSecPar->nBTLimit  = nBTLimit;
             pSecPar->TimeLimit = nTimeLim;
             pSecPar->fVerbose  = fVerbose;
diff --git a/src/proof/int/intUtil.c b/src/proof/int/intUtil.c
index b7e18f09..a70656c1 100644
--- a/src/proof/int/intUtil.c
+++ b/src/proof/int/intUtil.c
@@ -58,7 +58,7 @@ int Inter_ManCheckInitialState( Aig_Man_t * p )
         return 0;
     }
     status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-    ABC_PRT( "Time", Abc_Clock() - clk );
+    //ABC_PRT( "Time", Abc_Clock() - clk );
     if ( status == l_True )
     {
         p->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), 1 );
-- 
cgit v1.2.3