Version abc70731

24 files changed, 532 insertions, 112 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 4d23e029..d6a97257 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -92,7 +92,7 @@ struct Aig_Man_t_
     Vec_Ptr_t *      vBufs;          // the array of buffers
     Aig_Obj_t *      pConst1;        // the constant 1 node
     Aig_Obj_t        Ghost;          // the ghost node
-    int              nRegs;          // the number of registers
+    int              nRegs;          // the number of registers (registers are last POs)
     int              nAsserts;       // the number of asserts among POs (asserts are first POs)
     // AIG node counters
     int              nObjs[AIG_OBJ_VOID];// the number of objects by type
@@ -202,6 +202,7 @@ static inline int          Aig_ObjIsTravIdPrevious( Aig_Man_t * p, Aig_Obj_t * p
 
 static inline int          Aig_ObjTravId( Aig_Obj_t * pObj )      { return (int)pObj->pData;                       }
 static inline int          Aig_ObjPhase( Aig_Obj_t * pObj )       { return pObj->fPhase;                           }
+static inline int          Aig_ObjPhaseReal( Aig_Obj_t * pObj )   { return pObj? Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) : 1;                              }
 static inline int          Aig_ObjRefs( Aig_Obj_t * pObj )        { return pObj->nRefs;                            }
 static inline void         Aig_ObjRef( Aig_Obj_t * pObj )         { pObj->nRefs++;                                 }
 static inline void         Aig_ObjDeref( Aig_Obj_t * pObj )       { assert( pObj->nRefs > 0 ); pObj->nRefs--;      }
@@ -218,7 +219,6 @@ static inline Aig_Obj_t *  Aig_ObjChild0Copy( Aig_Obj_t * pObj )  { assert( !Aig
 static inline Aig_Obj_t *  Aig_ObjChild1Copy( Aig_Obj_t * pObj )  { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond((Aig_Obj_t *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj)) : NULL;  }
 static inline int          Aig_ObjLevel( Aig_Obj_t * pObj )       { return pObj->Level;                            }
 static inline int          Aig_ObjLevelNew( Aig_Obj_t * pObj )    { return Aig_ObjFanin1(pObj)? 1 + Aig_ObjIsExor(pObj) + AIG_MAX(Aig_ObjFanin0(pObj)->Level, Aig_ObjFanin1(pObj)->Level) : Aig_ObjFanin0(pObj)->Level; }
-static inline int          Aig_ObjFaninPhase( Aig_Obj_t * pObj )  { return pObj? Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) : 0;                              }
 static inline void         Aig_ObjClean( Aig_Obj_t * pObj )       { memset( pObj, 0, sizeof(Aig_Obj_t) );                                                             }
 static inline Aig_Obj_t *  Aig_ObjFanout0( Aig_Man_t * p, Aig_Obj_t * pObj )  { assert(p->pFanData && pObj->Id < p->nFansAlloc); return Aig_ManObj(p, p->pFanData[5*pObj->Id] >> 1); } 
 static inline int          Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )    
@@ -335,6 +335,8 @@ static inline int     Aig_ObjFanoutNext( Aig_Man_t * p, int iFan )   { assert(iF
 
 /*=== aigCheck.c ========================================================*/
 extern int             Aig_ManCheck( Aig_Man_t * p );
+extern void            Aig_ManCheckMarkA( Aig_Man_t * p );
+extern void            Aig_ManCheckPhase( Aig_Man_t * p );
 /*=== aigDfs.c ==========================================================*/
 extern Vec_Ptr_t *     Aig_ManDfs( Aig_Man_t * p );
 extern Vec_Ptr_t *     Aig_ManDfsNodes( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes );
@@ -356,7 +358,7 @@ extern void            Aig_ManFanoutStop( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManStart( int nNodesMax );
 extern Aig_Man_t *     Aig_ManStartFrom( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDup( Aig_Man_t * p, int fOrdered );
-extern Aig_Man_t *     Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes );
+extern Aig_Man_t *     Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 );
 extern void            Aig_ManStop( Aig_Man_t * p );
 extern int             Aig_ManCleanup( Aig_Man_t * p );
 extern void            Aig_ManPrintStats( Aig_Man_t * p );
@@ -438,7 +440,7 @@ extern unsigned *      Aig_ManCutTruth( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves,
 extern unsigned        Aig_PrimeCudd( unsigned p );
 extern void            Aig_ManIncrementTravId( Aig_Man_t * p );
 extern int             Aig_ManLevels( Aig_Man_t * p );
-extern void            Aig_ManCheckMarkA( Aig_Man_t * p );
+extern void            Aig_ManResetRefs( Aig_Man_t * p );
 extern void            Aig_ManCleanMarkA( Aig_Man_t * p );
 extern void            Aig_ManCleanMarkB( Aig_Man_t * p );
 extern void            Aig_ManCleanData( Aig_Man_t * p );
@@ -452,6 +454,7 @@ extern void            Aig_ObjPrintEqn( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_
 extern void            Aig_ObjPrintVerilog( FILE * pFile, Aig_Obj_t * pObj, Vec_Vec_t * vLevels, int Level );
 extern void            Aig_ObjPrintVerbose( Aig_Obj_t * pObj, int fHaig );
 extern void            Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig );
+extern void            Aig_ManDump( Aig_Man_t * p );
 extern void            Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
 /*=== aigWin.c =========================================================*/
 extern void            Aig_ManFindCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vFront, Vec_Ptr_t * vVisited, int nSizeLimit, int nFanoutLimit );
diff --git a/src/aig/aig/aigCheck.c b/src/aig/aig/aigCheck.c
index 1a8f108e..dc01f779 100644
--- a/src/aig/aig/aigCheck.c
+++ b/src/aig/aig/aigCheck.c
@@ -114,6 +114,47 @@ int Aig_ManCheck( Aig_Man_t * p )
     return 1; 
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Checks if the markA is reset.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManCheckMarkA( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManForEachObj( p, pObj, i )
+        assert( pObj->fMarkA == 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks the consistency of phase assignment.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManCheckPhase( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManForEachObj( p, pObj, i )
+        if ( Aig_ObjIsPi(pObj) )
+            assert( (int)pObj->fPhase == 0 );
+        else
+            assert( (int)pObj->fPhase == (Aig_ObjPhaseReal(Aig_ObjChild0(pObj)) & Aig_ObjPhaseReal(Aig_ObjChild1(pObj))) );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 50093195..818b75fe 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -135,6 +135,8 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
     int i;
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
+    pNew->nRegs = p->nRegs;
+    pNew->nAsserts = p->nAsserts;
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@@ -179,12 +181,11 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p, int fOrdered )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes )
+Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t * pNode2 )
 {
     Aig_Man_t * pNew;
     Aig_Obj_t * pObj;
     int i;
-    assert( nNodes == 2 );
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
     // create the PIs
@@ -193,10 +194,10 @@ Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t ** ppNodes, int nNodes
     Aig_ManForEachPi( p, pObj, i )
         pObj->pData = Aig_ObjCreatePi(pNew);
     // dump the nodes
-    for ( i = 0; i < nNodes; i++ )
-        Aig_ManDup_rec( pNew, p, ppNodes[i] );   
+    Aig_ManDup_rec( pNew, p, pNode1 );   
+    Aig_ManDup_rec( pNew, p, pNode2 );   
     // construct the EXOR
-    pObj = Aig_Exor( pNew, ppNodes[0]->pData, ppNodes[1]->pData ); 
+    pObj = Aig_Exor( pNew, pNode1->pData, pNode2->pData ); 
     pObj = Aig_NotCond( pObj, Aig_Regular(pObj)->fPhase ^ Aig_IsComplement(pObj) );
     // add the PO
     Aig_ObjCreatePo( pNew, pObj );
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index a017ff2d..34c07dce 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -135,7 +135,7 @@ void Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFan0, Aig_Obj
     }
     // set level and phase
     pObj->Level = Aig_ObjLevelNew( pObj );
-    pObj->fPhase = Aig_ObjFaninPhase(pFan0) & Aig_ObjFaninPhase(pFan1);
+    pObj->fPhase = Aig_ObjPhaseReal(pFan0) & Aig_ObjPhaseReal(pFan1);
     // add the node to the structural hash table
     if ( Aig_ObjIsHash(pObj) )
         Aig_TableInsert( p, pObj );
@@ -285,6 +285,7 @@ void Aig_NodeFixBufferFanins( Aig_Man_t * p, Aig_Obj_t * pObj, int fNodesOnly, i
     {
         assert( Aig_ObjIsBuf(Aig_ObjFanin0(pObj)) );
         pFanReal0 = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
+        assert( Aig_ObjPhaseReal(Aig_ObjChild0(pObj)) == Aig_ObjPhaseReal(pFanReal0) );
         Aig_ObjPatchFanin0( p, pObj, pFanReal0 );
         return;
     }
diff --git a/src/aig/aig/aigRepr.c b/src/aig/aig/aigRepr.c
index 47df7982..a862bf97 100644
--- a/src/aig/aig/aigRepr.c
+++ b/src/aig/aig/aigRepr.c
@@ -232,6 +232,7 @@ Aig_Man_t * Aig_ManDupRepr( Aig_Man_t * p )
     int i;
     // start the HOP package
     pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
+    pNew->nRegs = p->nRegs;
     Aig_ManReprStart( pNew, Aig_ManObjIdMax(p)+1 );
     // map the const and primary inputs
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c
index 0d4ffd1f..ba359c09 100644
--- a/src/aig/aig/aigTable.c
+++ b/src/aig/aig/aigTable.c
@@ -99,7 +99,7 @@ clk = clock();
     }
     nEntries = Aig_ManNodeNum(p);
     assert( Counter == nEntries );
-//    printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
+    printf( "Increasing the structural table size from %6d to %6d. ", nTableSizeOld, p->nTableSize );
     PRT( "Time", clock() - clk );
     // replace the table and the parameters
     free( pTableOld );
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index 364c32a3..cdf1fdf7 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -104,7 +104,7 @@ int Aig_ManLevels( Aig_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Checks if the markA is reset.]
+  Synopsis    [Reset reference counters.]
 
   Description []
                
@@ -113,17 +113,24 @@ int Aig_ManLevels( Aig_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_ManCheckMarkA( Aig_Man_t * p )
+void Aig_ManResetRefs( Aig_Man_t * p )
 {
     Aig_Obj_t * pObj;
     int i;
     Aig_ManForEachObj( p, pObj, i )
-        assert( pObj->fMarkA == 0 );
+        pObj->nRefs = 0;
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjFanin0(pObj) )
+            Aig_ObjFanin0(pObj)->nRefs++;
+        if ( Aig_ObjFanin1(pObj) )
+            Aig_ObjFanin1(pObj)->nRefs++;
+    }
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Checks if the markA is reset.]
+  Synopsis    [Cleans MarkB.]
 
   Description []
                
@@ -142,7 +149,7 @@ void Aig_ManCleanMarkA( Aig_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Checks if the markA is reset.]
+  Synopsis    [Cleans MarkB.]
 
   Description []
                
@@ -621,6 +628,27 @@ void Aig_ManPrintVerbose( Aig_Man_t * p, int fHaig )
 
 /**Function*************************************************************
 
+  Synopsis    [Write speculative miter for one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManDump( Aig_Man_t * p )
+{ 
+    static int Counter = 0;
+    char FileName[20];
+    // dump the logic into a file
+    sprintf( FileName, "aigbug\\%03d.blif", ++Counter );
+    Aig_ManDumpBlif( p, FileName );
+    printf( "Intermediate AIG with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(p), FileName );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Writes the AIG into the BLIF file.]
 
   Description []
@@ -679,6 +707,10 @@ void Aig_ManDumpBlif( Aig_Man_t * p, char * pFileName )
     // write POs
     Aig_ManForEachPo( p, pObj, i )
     {
+        if ( (int)pObj->pData == 1359 )
+        {
+            int x = 0;
+        }
         fprintf( pFile, ".names n%0*d n%0*d\n", 
             nDigits, (int)Aig_ObjFanin0(pObj)->pData, 
             nDigits, (int)pObj->pData );
diff --git a/src/aig/cnf/cnfCore.c b/src/aig/cnf/cnfCore.c
index 13de745b..06731451 100644
--- a/src/aig/cnf/cnfCore.c
+++ b/src/aig/cnf/cnfCore.c
@@ -75,6 +75,8 @@ clk = clock();
     Aig_MmFixedStop( pMemCuts, 0 );
 p->timeSave = clock() - clk;
 
+   // reset reference counters
+    Aig_ManResetRefs( pAig );
 //PRT( "Cuts   ", p->timeCuts );
 //PRT( "Map    ", p->timeMap  );
 //PRT( "Saving ", p->timeSave );
diff --git a/src/aig/dar/dar.h b/src/aig/dar/dar.h
index 44dd2788..923ffc12 100644
--- a/src/aig/dar/dar.h
+++ b/src/aig/dar/dar.h
@@ -85,6 +85,7 @@ extern Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax );
 extern void            Dar_ManDefaultRefParams( Dar_RefPar_t * pPars );
 extern int             Dar_ManRefactor( Aig_Man_t * pAig, Dar_RefPar_t * pPars );
 /*=== darScript.c ========================================================*/
+extern Aig_Man_t *     Dar_ManRewriteDefault( Aig_Man_t * pAig );
 extern Aig_Man_t *     Dar_ManCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fVerbose );
 extern Aig_Man_t *     Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose );
 
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 097f1a4d..9c0997b8 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -54,6 +54,8 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
     int i;
     // create the new manager 
     pNew = Aig_ManStart( Aig_ManObjIdMax(p) + 1 );
+    pNew->nRegs = p->nRegs;
+    pNew->nAsserts = p->nAsserts;
     // map the PI nodes
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index b74f570c..dec9bff7 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -42,7 +42,7 @@
 void Dar_ManDefaultRwrParams( Dar_RwrPar_t * pPars )
 {
     memset( pPars, 0, sizeof(Dar_RwrPar_t) );
-    pPars->nCutsMax     =  8;
+    pPars->nCutsMax     =  8; // 8
     pPars->nSubgMax     =  5; // 5 is a "magic number"
     pPars->fFanout      =  1;
     pPars->fUpdateLevel =  0;
@@ -151,8 +151,8 @@ p->timeCuts += clock() - clk;
         Dar_ObjSetCuts( pObj, NULL );
         // if we end up here, a rewriting step is accepted
         nNodeBefore = Aig_ManNodeNum( pAig );
-        pObjNew = Dar_LibBuildBest( p );
-        pObjNew = Aig_NotCond( pObjNew, pObjNew->fPhase ^ pObj->fPhase );
+        pObjNew = Dar_LibBuildBest( p ); // pObjNew can be complemented!
+        pObjNew = Aig_NotCond( pObjNew, Aig_ObjPhaseReal(pObjNew) ^ pObj->fPhase );
         assert( (int)Aig_Regular(pObjNew)->Level <= Required );
         // replace the node
         Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
@@ -183,6 +183,7 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
     }
     // stop the rewriting manager
     Dar_ManStop( p );
+    Aig_ManCheckPhase( pAig );
     // check
     if ( !Aig_ManCheck( pAig ) )
     {
@@ -209,9 +210,12 @@ Aig_MmFixed_t * Dar_ManComputeCuts( Aig_Man_t * pAig, int nCutsMax )
     Dar_RwrPar_t Pars, * pPars = &Pars; 
     Aig_Obj_t * pObj;
     Aig_MmFixed_t * pMemCuts;
-    int i, clk = 0, clkStart = clock();
+    int i, nNodes, clk = 0, clkStart = clock();
     // remove dangling nodes
-    Aig_ManCleanup( pAig );
+    if ( nNodes = Aig_ManCleanup( pAig ) )
+    {
+//        printf( "Removing %d nodes.\n", nNodes );
+    }
     // create default parameters
     Dar_ManDefaultRwrParams( pPars );
     pPars->nCutsMax = nCutsMax;
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
index fbd12cae..b304fe34 100644
--- a/src/aig/dar/darRefact.c
+++ b/src/aig/dar/darRefact.c
@@ -361,6 +361,21 @@ int Dar_ManRefactorTryCuts( Ref_Man_t * p, Aig_Obj_t * pObj, int nNodesSaved, in
         Aig_ObjCollectCut( pObj, vCut, p->vCutNodes );
         // get the truth table
         pTruth = Aig_ManCutTruth( pObj, vCut, p->vCutNodes, p->vTruthElem, p->vTruthStore );
+        if ( Kit_TruthIsConst0(pTruth, Vec_PtrSize(vCut)) )
+        {
+            p->GainBest = Vec_PtrSize(p->vCutNodes);
+            p->pGraphBest = Kit_GraphCreateConst0();
+            Vec_PtrCopy( p->vLeavesBest, vCut );
+            return p->GainBest;
+        }
+        if ( Kit_TruthIsConst1(pTruth, Vec_PtrSize(vCut)) )
+        {
+            p->GainBest = Vec_PtrSize(p->vCutNodes);
+            p->pGraphBest = Kit_GraphCreateConst1();
+            Vec_PtrCopy( p->vLeavesBest, vCut );
+            return p->GainBest;
+        }
+
         // try the positive phase
         RetValue = Kit_TruthIsop( pTruth, Vec_PtrSize(vCut), p->vMemory, 0 );
         if ( RetValue > -1 )
@@ -559,6 +574,7 @@ p->timeOther = p->timeTotal - p->timeCuts - p->timeEval;
 
     // stop the rewriting manager
     Dar_ManRefStop( p );
+    Aig_ManCheckPhase( pAig );
     if ( !Aig_ManCheck( pAig ) )
     {
         printf( "Dar_ManRefactor: The network check has failed.\n" );
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index 75076981..2fe39860 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -30,6 +30,30 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Performs one iteration of AIG rewriting.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManRewriteDefault( Aig_Man_t * pAig )
+{
+    Aig_Man_t * pTemp;
+    Dar_RwrPar_t Pars, * pPars = &Pars;
+    Dar_ManDefaultRwrParams( pPars );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+    Dar_ManRewrite( pAig, pPars );
+    pAig = Aig_ManDup( pTemp = pAig, 0 ); 
+    Aig_ManStop( pTemp );
+    return pAig;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Reproduces script "compress2".]
 
   Description []
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 91a1f8b1..5d357290 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -70,6 +70,7 @@ struct Fra_Par_t_
     int              nBTLimitNode;      // conflict limit at a node
     int              nBTLimitMiter;     // conflict limit at an output
     int              nFramesK;          // the number of timeframes to unroll
+    int              fRewrite;          // use rewriting for constraint reduction
 };
 
 // FRAIG equivalence classes
@@ -121,11 +122,13 @@ struct Fra_Man_t_
     // statistics
     int              nSimRounds;
     int              nNodesMiter;
-    int              nClassesZero;
-    int              nClassesBeg;
-    int              nClassesEnd;
-    int              nPairsBeg;
-    int              nPairsEnd;
+    int              nLitsZero;
+    int              nLitsBeg;
+    int              nLitsEnd;
+    int              nNodesBeg;
+    int              nNodesEnd;
+    int              nRegsBeg;
+    int              nRegsEnd;
     int              nSatCalls;
     int              nSatCallsSat;
     int              nSatCallsUnsat;
@@ -138,6 +141,7 @@ struct Fra_Man_t_
     // runtime
     int              timeSim;
     int              timeTrav;
+    int              timeRwr;
     int              timeSat;
     int              timeSatUnsat;
     int              timeSatSat;
@@ -182,7 +186,7 @@ static inline Aig_Obj_t *  Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert(
 extern Fra_Cla_t *         Fra_ClassesStart( Aig_Man_t * pAig );
 extern void                Fra_ClassesStop( Fra_Cla_t * p );
 extern void                Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
-extern void                Fra_ClassesPrint( Fra_Cla_t * p );
+extern void                Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose );
 extern void                Fra_ClassesPrepare( Fra_Cla_t * p );
 extern int                 Fra_ClassesRefine( Fra_Cla_t * p );
 extern int                 Fra_ClassesRefine1( Fra_Cla_t * p );
@@ -197,7 +201,7 @@ extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig );
 extern void                Fra_FraigSweep( Fra_Man_t * pManAig );
 /*=== fraDfs.c ========================================================*/
 /*=== fraInd.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fVerbose );
+extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fVerbose );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
 extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 05c07889..31d6270a 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -215,25 +215,28 @@ int Fra_ClassesCountPairs( Fra_Cla_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_ClassesPrint( Fra_Cla_t * p )
+void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
 {
     Aig_Obj_t ** pClass;
     Aig_Obj_t * pObj;
     int i;
+
     printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", 
         Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) );
-/*
-    printf( "Constants { " );
-    Vec_PtrForEachEntry( p->vClasses1, pObj, i )
-        printf( "%d ", pObj->Id );
-    printf( "}\n" );
-    Vec_PtrForEachEntry( p->vClasses, pClass, i )
+
+    if ( fVeryVerbose )
     {
-        printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
-        Fra_PrintClass( pClass );
+        printf( "Constants { " );
+        Vec_PtrForEachEntry( p->vClasses1, pObj, i )
+            printf( "%d ", pObj->Id );
+        printf( "}\n" );
+        Vec_PtrForEachEntry( p->vClasses, pClass, i )
+        {
+            printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
+            Fra_PrintClass( pClass );
+        }
+        printf( "\n" );
     }
-    printf( "\n" );
-*/
 }
 
 /**Function*************************************************************
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index 9f2b8ca7..71e12a75 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -39,7 +39,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFraig, Aig_Obj_t * pObjReprFraig )
+static inline void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFraig, Aig_Obj_t * pObjReprFraig )
 { 
     static int Counter = 0;
     char FileName[20];
@@ -47,8 +47,7 @@ void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFr
     Aig_Obj_t * pNode;
     int i;
     // create manager with the logic for these two nodes
-    Aig_Obj_t * ppNodes[2] = { pObjFraig, pObjReprFraig };
-    pTemp = Aig_ManExtractMiter( p->pManFraig, ppNodes, 2 );
+    pTemp = Aig_ManExtractMiter( p->pManFraig, pObjFraig, pObjReprFraig );
     // dump the logic into a file
     sprintf( FileName, "aig\\%03d.blif", ++Counter );
     Aig_ManDumpBlif( pTemp, FileName );
@@ -70,7 +69,7 @@ void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFr
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
+static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
 { 
     Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
     int RetValue;
@@ -123,6 +122,8 @@ void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
     // simulate the counter-example and return the Fraig node
     Fra_Resimulate( p );
     assert( Fra_ClassObjRepr(pObj) != pObjRepr );
+    if ( Fra_ClassObjRepr(pObj) == pObjRepr )
+        printf( "Fra_FraigNode(): Error in class refinement!\n" );
 }
 
 /**Function*************************************************************
@@ -141,8 +142,6 @@ void Fra_FraigSweep( Fra_Man_t * p )
     ProgressBar * pProgress;
     Aig_Obj_t * pObj, * pObjNew;
     int i, k = 0;
-p->nClassesZero = Vec_PtrSize(p->pCla->vClasses1);
-p->nClassesBeg  = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0);
     // duplicate internal nodes
     pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) );
     // fraig latch outputs
@@ -163,7 +162,6 @@ p->nClassesBeg  = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vC
         Fra_FraigNode( p, pObj );
     }
     Extra_ProgressBarStop( pProgress );
-p->nClassesEnd = Vec_PtrSize(p->pCla->vClasses) + (int)(Vec_PtrSize(p->pCla->vClasses1) > 0);
     // try to prove the outputs of the miter
     p->nNodesMiter = Aig_ManNodeNum(p->pManFraig);
 //    Fra_MiterStatus( p->pManFraig );
@@ -196,15 +194,23 @@ clk = clock();
     Fra_Simulate( p, 0 );
     if ( p->pPars->fChoicing )
         Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 );
+    // collect initial states
+    p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
+    p->nLitsBeg = Fra_ClassesCountLits( p->pCla );
+    p->nNodesBeg = Aig_ManNodeNum(pManAig);
+    p->nRegsBeg  = Aig_ManRegNum(pManAig);
+    // perform fraig sweep
     Fra_FraigSweep( p );
     Fra_ManFinalizeComb( p );
     if ( p->pPars->fChoicing )
     {
+        int clk2 = clock();
         Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
         pManAigNew = Aig_ManDupRepr( p->pManAig );
         Aig_ManCreateChoices( pManAigNew );
         Aig_ManStop( p->pManFraig );
         p->pManFraig = NULL;
+p->timeTrav += clock() - clk2;
     }
     else
     {
@@ -221,6 +227,10 @@ clk = clock();
 */
     }
 p->timeTotal = clock() - clk;
+    // collect final stats
+    p->nLitsEnd = Fra_ClassesCountLits( p->pCla );
+    p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
+    p->nRegsEnd  = Aig_ManRegNum(pManAigNew);
     Fra_ManStop( p );
     return pManAigNew;
 }
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 71e535f7..bb4c4287 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -20,6 +20,7 @@
 
 #include "fra.h"
 #include "cnf.h"
+#include "dar.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -31,6 +32,54 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Performs AIG rewriting on the constaint manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_FraigInductionRewrite( Fra_Man_t * p )
+{
+    Aig_Man_t * pTemp;
+    Aig_Obj_t * pObj, * pObjPo;
+    int nTruePis, k, i, clk = clock();
+    // perform AIG rewriting on the speculated frames
+    pTemp = Aig_ManDup( p->pManFraig, 0 );
+//    pTemp = Dar_ManRwsat( pTemp, 1, 0 );
+    pTemp = Dar_ManRewriteDefault( pTemp );
+
+//    printf( "Before = %6d.  After = %6d.\n", Aig_ManNodeNum(p->pManFraig), Aig_ManNodeNum(pTemp) ); 
+//Aig_ManDumpBlif( p->pManFraig, "1.blif" );
+//Aig_ManDumpBlif( pTemp, "2.blif" );
+
+//    Fra_FramesWriteCone( pTemp );
+//    Aig_ManStop( pTemp );
+    // transfer PI/register pointers
+    assert( p->pManFraig->nRegs == pTemp->nRegs );
+    assert( p->pManFraig->nAsserts == pTemp->nAsserts );
+    nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
+    memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
+    Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), p->pPars->nFramesK, Aig_ManConst1(pTemp) );
+    Aig_ManForEachPiSeq( p->pManAig, pObj, i )
+        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ManPi(pTemp,nTruePis*p->pPars->nFramesK+i) );
+    k = 0;
+    assert( Aig_ManRegNum(p->pManAig) == Aig_ManPoNum(pTemp) - pTemp->nAsserts );
+    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
+    {
+        pObjPo = Aig_ManPo(pTemp, pTemp->nAsserts + k++);
+        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ObjChild0(pObjPo) );
+    }
+    // exchange
+    Aig_ManStop( p->pManFraig );
+    p->pManFraig = pTemp;
+p->timeRwr += clock() - clk;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs speculative reduction for one node.]
 
   Description []
@@ -131,6 +180,8 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
     Aig_ManForEachLiSeq( p->pManAig, pObj, i )
         Aig_ObjCreatePo( pManFraig, Fra_ObjChild0Fra(pObj,f-1) );
 
+    // remove dangling nodes
+    Aig_ManCleanup( pManFraig );
     // make sure the satisfying assignment is node assigned
     assert( pManFraig->pData == NULL );
     return pManFraig;
@@ -147,35 +198,39 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fVerbose )
 {
     Fra_Man_t * p;
     Fra_Par_t Pars, * pPars = &Pars; 
     Aig_Obj_t * pObj;
     Cnf_Dat_t * pCnf;
     Aig_Man_t * pManAigNew;
-    int nIter, i;
+    int nIter, i, clk = clock(), clk2;
 
     if ( Aig_ManNodeNum(pManAig) == 0 )
         return Aig_ManDup(pManAig, 1);
     assert( Aig_ManLatchNum(pManAig) == 0 );
     assert( Aig_ManRegNum(pManAig) > 0 );
     assert( nFramesK > 0 );
+//Aig_ManShow( pManAig, 0, NULL );
 
     // get parameters
     Fra_ParamsDefaultSeq( pPars );
     pPars->nFramesK = nFramesK;
     pPars->fVerbose = fVerbose;
+    pPars->fRewrite = fRewrite;
 
     // start the fraig manager for this run
     p = Fra_ManStart( pManAig, pPars );
-    // derive and refine e-classes using the 1st init frame
+    // derive and refine e-classes using K initialized frames
     Fra_Simulate( p, 1 );
-//    Fra_ClassesTest( p->pCla, 2, 3 );
-//Aig_ManShow( pManAig, 0, NULL );
-
-    // refine e-classes using sequential simulation
+    // refine e-classes using sequential simulation?
  
+    p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
+    p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
+    p->nNodesBeg = Aig_ManNodeNum(pManAig);
+    p->nRegsBeg  = Aig_ManRegNum(pManAig);
+
     // iterate the inductive case
     p->pCla->fRefinement = 1;
     for ( nIter = 0; p->pCla->fRefinement; nIter++ )
@@ -184,6 +239,10 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose
         p->pCla->fRefinement = 0;
         // derive non-init K-timeframes while implementing e-classes
         p->pManFraig = Fra_FramesWithClasses( p );
+        // perform AIG rewriting
+        if ( p->pPars->fRewrite )
+            Fra_FraigInductionRewrite( p );
+        // report the intermediate results
         if ( fVerbose )
         {
             printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  N = %6d. NR = %6d.\n", 
@@ -191,19 +250,22 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose
                 Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts,
                 Aig_ManNodeNum(p->pManAig), Aig_ManNodeNum(p->pManFraig) );
         }
-        // perform AIG rewriting on the speculated frames
 
         // convert the manager to SAT solver (the last nLatches outputs are inputs)
-//        pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
-        pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
+        pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
+//        pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
 //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
 
         p->pSat = Cnf_DataWriteIntoSolver( pCnf );
         p->nSatVars = pCnf->nVars;
+        assert( p->pSat != NULL );
+        if ( p->pSat == NULL )
+            printf( "Fra_FraigInduction(): Computed CNF is not valid.\n" );
 
         // set the pointers to the manager
         Aig_ManForEachObj( p->pManFraig, pObj, i )
             pObj->pData = p;
+
         // transfer PI/LO variable numbers
         pObj = Aig_ManConst1( p->pManFraig );
         Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
@@ -216,20 +278,40 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fVerbose
             Fra_ObjSetFaninVec( pObj, (void *)1 );
         }
         Cnf_DataFree( pCnf );
+/*
+        Aig_ManForEachObj( p->pManFraig, pObj, i )
+        {
+            Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
+            Fra_ObjSetFaninVec( pObj, (void *)1 );
+        }
+        Cnf_DataFree( pCnf );
+*/
 
         // perform sweeping
         Fra_FraigSweep( p );
         assert( p->vTimeouts == NULL );
+        if ( p->vTimeouts )
+           printf( "Fra_FraigInduction(): SAT solver timed out!\n" );
 
         // cleanup
         Fra_ManClean( p );
     }
-
-    // move the classes into representatives
+    // move the classes into representatives and reduce AIG
+clk2 = clock();
     Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
-    // implement the classes
     pManAigNew = Aig_ManDupRepr( pManAig );
+p->timeTrav += clock() - clk2;
+p->timeTotal = clock() - clk;
+    // get the final stats
+    p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
+    p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
+    p->nRegsEnd  = Aig_ManRegNum(pManAigNew);
+    // free the manager
     Fra_ManStop( p );
+    // check the output
+    if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
+        if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
+            printf( "Proved output constant 0.\n" );
     return pManAigNew;
 }
 
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index fdd1ccc5..95cf28d8 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -55,6 +55,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars )
     pPars->nBTLimitMiter    =  500000;  // conflict limit at an output
     pPars->nFramesK         =       0;  // the number of timeframes to unroll
     pPars->fConeBias        =       1;
+    pPars->fRewrite         =       0;
 }
 
 /**Function*************************************************************
@@ -71,7 +72,7 @@ void Fra_ParamsDefault( Fra_Par_t * pPars )
 void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
 {
     memset( pPars, 0, sizeof(Fra_Par_t) );
-    pPars->nSimWords        =       4;  // the number of words in the simulation info
+    pPars->nSimWords        =       1;  // the number of words in the simulation info
     pPars->dSimSatur        =   0.005;  // the ratio of refined classes when saturation is reached
     pPars->fPatScores       =       0;  // enables simulation pattern scoring
     pPars->MaxScore         =      25;  // max score after which resimulation is used
@@ -80,10 +81,11 @@ void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
 //    pPars->dActConeBumpMax  =     5.0;  // the largest bump of activity
     pPars->dActConeRatio    =     0.3;  // the ratio of cone to be bumped
     pPars->dActConeBumpMax  =    10.0;  // the largest bump of activity
-    pPars->nBTLimitNode     = 1000000;  // conflict limit at a node
+    pPars->nBTLimitNode     =10000000;  // conflict limit at a node
     pPars->nBTLimitMiter    =  500000;  // conflict limit at an output
     pPars->nFramesK         =       1;  // the number of timeframes to unroll
     pPars->fConeBias        =       0;
+    pPars->fRewrite         =       0;
 }
 
 /**Function*************************************************************
@@ -165,7 +167,6 @@ void Fra_ManClean( Fra_Man_t * p )
 
     sat_solver_delete( p->pSat );  
     p->pSat = NULL; 
-    p->nSatVars = 0;
 }
 
 /**Function*************************************************************
@@ -268,23 +269,28 @@ void Fra_ManStop( Fra_Man_t * p )
 void Fra_ManPrint( Fra_Man_t * p )
 {
     double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*((p->nSimWords+2)*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
-    printf( "SimWords = %d. Rounds = %d. Mem = %0.2f Mb.  ", p->nSimWords, p->nSimRounds, nMemory );
-    printf( "Classes: Beg = %d. End = %d.\n", p->nClassesBeg, p->nClassesEnd );
-    printf( "Limits: BTNode = %d. BTMiter = %d.\n", p->pPars->nBTLimitNode, p->pPars->nBTLimitMiter );
-    printf( "Proof = %d. Counter-example = %d. Fail = %d. FailReal = %d. Zero = %d.\n", 
-        p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nClassesZero );
-    printf( "Final = %d. Miter = %d. Total = %d. Mux = %d. (Exor = %d.) SatVars = %d.\n", 
-        p->pManFraig? Aig_ManNodeNum(p->pManFraig) : -1, p->nNodesMiter, Aig_ManNodeNum(p->pManAig), 0, 0, p->nSatVars );
+    printf( "SimWord = %d. Round = %d.  Mem = %0.2f Mb.  LitBeg = %d.  LitEnd = %d. (%6.2f %%).\n", 
+        p->nSimWords, p->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg );
+    printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. Zero = %d. C-lim = %d. Vars = %d.\n", 
+        p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nLitsZero, p->pPars->nBTLimitNode, p->nSatVars );
+    printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
+        p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg, 
+        p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg );
     if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
     PRT( "AIG simulation  ", p->timeSim  );
-    PRT( "AIG traversal   ", p->timeTrav  );
-    PRT( "SAT solving     ", p->timeSat   );
+    PRT( "AIG traversal   ", p->timeTrav );
+    if ( p->timeRwr )
+    {
+    PRT( "AIG rewriting   ", p->timeRwr  );
+    }
+    PRT( "SAT solving     ", p->timeSat  );
     PRT( "    Unsat       ", p->timeSatUnsat );
     PRT( "    Sat         ", p->timeSatSat   );
     PRT( "    Fail        ", p->timeSatFail  );
     PRT( "Class refining  ", p->timeRef   );
     PRT( "TOTAL RUNTIME   ", p->timeTotal );
     if ( p->time1 ) { PRT( "time1           ", p->time1 ); }
+    if ( p->nSpeculs )
     printf( "Speculations = %d.\n", p->nSpeculs );
 }
 
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 4ae8a686..4a6e0251 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -142,10 +142,14 @@ void Fra_AssignDist1( Fra_Man_t * p, unsigned * pPat )
             Fra_NodeAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFramesAll + k++), 0 );
         assert( p->pManFraig == NULL || nTruePis * p->nFramesAll + k == Aig_ManPiNum(p->pManFraig) );
 
-        // flip one bit of the first frame
-        Limit = AIG_MIN( nTruePis, p->pPars->nSimWords * 32 - 1 );
-        for ( i = 0; i < Limit; i++ )
-            Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig,i) ), i+1 );
+        // flip one bit of the last frame
+        if ( p->nFramesAll == 2 )
+        {
+            Limit = AIG_MIN( nTruePis, p->pPars->nSimWords * 32 - 1 );
+            for ( i = 0; i < Limit; i++ )
+                Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig, i) ), i+1 );
+//            Aig_InfoXorBit( Fra_ObjSim( Aig_ManPi(p->pManAig, nTruePis*(p->nFramesAll-2) + i) ), i+1 );
+        }
     }
 }
 
@@ -261,8 +265,8 @@ void Fra_NodeSimulate( Fra_Man_t * p, Aig_Obj_t * pObj, int iFrame )
     pSims1 = Fra_ObjSim(Aig_ObjFanin1(pObj)) + nSimWords * iFrame;
     // get complemented attributes of the children using their random info
     fCompl  = pObj->fPhase;
-    fCompl0 = Aig_ObjFaninPhase(Aig_ObjChild0(pObj));
-    fCompl1 = Aig_ObjFaninPhase(Aig_ObjChild1(pObj));
+    fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
+    fCompl1 = Aig_ObjPhaseReal(Aig_ObjChild1(pObj));
     // simulate
     if ( fCompl0 && fCompl1 )
     {
@@ -326,7 +330,7 @@ void Fra_NodeCopyFanin( Fra_Man_t * p, Aig_Obj_t * pObj, int iFrame )
     pSims0 = Fra_ObjSim(Aig_ObjFanin0(pObj)) + nSimWords * iFrame;
     // get complemented attributes of the children using their random info
     fCompl  = pObj->fPhase;
-    fCompl0 = Aig_ObjFaninPhase(Aig_ObjChild0(pObj));
+    fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
     // copy information as it is
     if ( fCompl0 )
         for ( i = 0; i < nSimWords; i++ )
@@ -624,7 +628,7 @@ void Fra_Simulate( Fra_Man_t * p, int fInit )
     Fra_AssignRandom( p, fInit );
     Fra_SimulateOne( p );
     Fra_ClassesPrepare( p->pCla );
-//    Fra_ClassesPrint( p->pCla );
+//    Fra_ClassesPrint( p->pCla, 0 );
 //printf( "Starting classes = %5d.   Pairs = %6d.\n", p->lClasses.nItems, Fra_CountPairsClasses(p) );
 
     // refine classes by walking 0/1 patterns
@@ -667,7 +671,7 @@ p->timeRef += clock() - clk;
 //    printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", 
 //        Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
 
-//    Fra_ClassesPrint( p->pCla );
+//    Fra_ClassesPrint( p->pCla, 0 );
 }
  
 /**Function*************************************************************
@@ -729,7 +733,7 @@ int Fra_CheckOutputSims( Fra_Man_t * p )
     int i;
     // make sure the reference simulation pattern does not detect the bug
     pObj = Aig_ManPo( p->pManAig, 0 );
-    assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); // Aig_ObjFaninPhase(Aig_ObjChild0(pObj)) == 0
+    assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); 
     Aig_ManForEachPo( p->pManAig, pObj, i )
     {
         if ( !Fra_NodeHasZeroSim( Aig_ObjFanin0(pObj) ) )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 8ae5bb9e..3a916fdc 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -157,6 +157,7 @@ static int Abc_CommandIf             ( Abc_Frame_t * pAbc, int argc, char ** arg
 
 static int Abc_CommandScut           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandInit           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandZero           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandPipe           ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSeq            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandUnseq          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -320,6 +321,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 
 //    Cmd_CommandAdd( pAbc, "Sequential",   "scut",          Abc_CommandScut,             0 );
     Cmd_CommandAdd( pAbc, "Sequential",   "init",          Abc_CommandInit,             1 );
+    Cmd_CommandAdd( pAbc, "Sequential",   "zero",          Abc_CommandZero,             1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "pipe",          Abc_CommandPipe,             1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "seq",           Abc_CommandSeq,              1 );
 //    Cmd_CommandAdd( pAbc, "Sequential",   "unseq",         Abc_CommandUnseq,            1 );
@@ -371,6 +373,10 @@ void Abc_End()
 //    Dar_LibDumpPriorities();
 
     {
+        extern void Cnf_ClearMemory();
+        Cnf_ClearMemory();
+    }
+    {
         extern void Dar_LibStop();
         Dar_LibStop();
     }
@@ -4080,19 +4086,20 @@ int Abc_CommandOrPos( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "The network is not strashed.\n" );
         return 1;
     }
-
+/*
     if ( Abc_NtkPoNum(pNtk) == 1 )
     {
         fprintf( pErr, "The network already has one PO.\n" );
         return 1;
     }
-
+*/
+/*
     if ( Abc_NtkLatchNum(pNtk) )
     {
         fprintf( pErr, "The miter has latches. ORing is not performed.\n" );
         return 1;
     }
-
+*/
     // get the new network
     if ( !Abc_NtkCombinePos( pNtk, 0 ) )
     {
@@ -10113,6 +10120,78 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandZero( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+
+    extern Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+
+    if ( Abc_NtkIsComb(pNtk) )
+    {
+        fprintf( pErr, "The current network is combinational.\n" );
+        return 0;
+    }
+
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "This command works only for AIGs.\n" );
+        return 0;
+    }
+
+    // get the new network
+    pNtkRes = Abc_NtkRestrashZero( pNtk, 0 );
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Converting to sequential AIG has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: zero [-h]\n" );
+    fprintf( pErr, "\t        converts latches to have const-0 initial value\n" );
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandPipe( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -10736,8 +10815,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nFramesK;
     int fExdc;
     int fImp;
+    int fRewrite;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -10747,9 +10827,10 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     nFramesK = 1;
     fExdc    = 1;
     fImp     = 0;
+    fRewrite = 0;
     fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Feivh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Feirvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -10770,6 +10851,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'i':
             fImp ^= 1;
             break;
+        case 'r':
+            fRewrite ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -10799,7 +10883,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fVerbose );
+    pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential sweeping has failed.\n" );
@@ -10810,11 +10894,12 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ssweep [-F num] [-eivh]\n" );
-    fprintf( pErr, "\t         performs sequential sweep using van Eijk's method\n" );
+    fprintf( pErr, "usage: ssweep [-F num] [-rvh]\n" );
+    fprintf( pErr, "\t         performs sequential sweep using K-step induction\n" );
     fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
 //    fprintf( pErr, "\t-e     : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
 //    fprintf( pErr, "\t-i     : toggle computing implications [default = %s]\n", fImp? "yes": "no" );
+    fprintf( pErr, "\t-r     : toggle AIG rewriting [default = %s]\n", fRewrite? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 035daeff..ca80fec8 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -36,24 +36,48 @@
 
   Synopsis    [Converts the network from the AIG manager into ABC.]
 
-  Description []
+  Description [Assumes that registers are ordered after PIs/POs.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk )
+Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fRegisters )
 {
     Aig_Man_t * pMan;
+    Aig_Obj_t * pObjNew;
     Abc_Obj_t * pObj;
-    int i;
+    int i, nNodes;
+    // make sure the latches follow PIs/POs
+    if ( fRegisters )
+    {
+        assert( Abc_NtkBoxNum(pNtk) == Abc_NtkLatchNum(pNtk) );
+        Abc_NtkForEachCi( pNtk, pObj, i )
+            if ( i < Abc_NtkPiNum(pNtk) )
+                assert( Abc_ObjIsPi(pObj) );
+            else
+                assert( Abc_ObjIsBo(pObj) );
+        Abc_NtkForEachCo( pNtk, pObj, i )
+            if ( i < Abc_NtkPoNum(pNtk) )
+                assert( Abc_ObjIsPo(pObj) );
+            else
+                assert( Abc_ObjIsBi(pObj) );
+    }
     // create the manager
     pMan = Aig_ManStart( Abc_NtkNodeNum(pNtk) + 100 );
+    // save the number of registers
+    if ( fRegisters )
+        pMan->nRegs = Abc_NtkLatchNum(pNtk);
     // transfer the pointers to the basic nodes
     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
     Abc_NtkForEachCi( pNtk, pObj, i )
         pObj->pCopy = (Abc_Obj_t *)Aig_ObjCreatePi(pMan);
+    // complement the 1-values registers
+    if ( fRegisters )
+        Abc_NtkForEachLatch( pNtk, pObj, i )
+            if ( Abc_LatchIsInit1(pObj) )
+                Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy);
     // perform the conversion of the internal nodes (assumes DFS ordering)
     Abc_NtkForEachNode( pNtk, pObj, i )
     {
@@ -63,7 +87,14 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk )
     // create the POs
     Abc_NtkForEachCo( pNtk, pObj, i )
         Aig_ObjCreatePo( pMan, (Aig_Obj_t *)Abc_ObjChild0Copy(pObj) );
-    Aig_ManCleanup( pMan );
+    // complement the 1-valued registers
+    if ( fRegisters )
+        Aig_ManForEachLiSeq( pMan, pObjNew, i )
+            if ( Abc_LatchIsInit1(Abc_ObjFanout0(Abc_NtkCo(pNtk,i))) )
+                pObjNew->pFanin0 = Aig_Not(pObjNew->pFanin0);
+    // remove dangling nodes
+    if ( nNodes = Aig_ManCleanup( pMan ) )
+        printf( "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
     if ( !Aig_ManCheck( pMan ) )
     {
         printf( "Abc_NtkToDar: AIG check has failed.\n" );
@@ -296,8 +327,8 @@ void Abc_NtkSecRetime( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     fRemove2 = (!Abc_NtkIsStrash(pNtk2)) && (pNtk2 = Abc_NtkStrash(pNtk2, 0, 0, 0));
 
 
-    pMan1 = Abc_NtkToDar( pNtk1 );
-    pMan2 = Abc_NtkToDar( pNtk2 );
+    pMan1 = Abc_NtkToDar( pNtk1, 0 );
+    pMan2 = Abc_NtkToDar( pNtk2, 0 );
 
     Aig_ManPrintStats( pMan1 );
     Aig_ManPrintStats( pMan2 );
@@ -342,7 +373,7 @@ Abc_Ntk_t * Abc_NtkDar( Abc_Ntk_t * pNtk )
 
     assert( Abc_NtkIsStrash(pNtk) );
     // convert to the AIG manager
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
     if ( !Aig_ManCheck( pMan ) )
@@ -410,7 +441,7 @@ Abc_Ntk_t * Abc_NtkDarFraig( Abc_Ntk_t * pNtk, int nConfLimit, int fDoSparse, in
     Fra_Par_t Pars, * pPars = &Pars; 
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
     Fra_ParamsDefault( pPars );
@@ -446,7 +477,7 @@ Abc_Ntk_t * Abc_NtkCSweep( Abc_Ntk_t * pNtk, int nCutsMax, int nLeafMax, int fVe
     extern Aig_Man_t * Csw_Sweep( Aig_Man_t * pAig, int nCutsMax, int nLeafMax, int fVerbose );
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
     pMan = Csw_Sweep( pTemp = pMan, nCutsMax, nLeafMax, fVerbose );
@@ -473,7 +504,7 @@ Abc_Ntk_t * Abc_NtkDRewrite( Abc_Ntk_t * pNtk, Dar_RwrPar_t * pPars )
     Abc_Ntk_t * pNtkAig;
     int clk;
     assert( Abc_NtkIsStrash(pNtk) );
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
 //    Aig_ManPrintStats( pMan );
@@ -517,7 +548,7 @@ Abc_Ntk_t * Abc_NtkDRefactor( Abc_Ntk_t * pNtk, Dar_RefPar_t * pPars )
     Abc_Ntk_t * pNtkAig;
     int clk;
     assert( Abc_NtkIsStrash(pNtk) );
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
 //    Aig_ManPrintStats( pMan );
@@ -554,7 +585,7 @@ Abc_Ntk_t * Abc_NtkDCompress2( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel,
     Abc_Ntk_t * pNtkAig;
     int clk;
     assert( Abc_NtkIsStrash(pNtk) );
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
 //    Aig_ManPrintStats( pMan );
@@ -587,7 +618,7 @@ Abc_Ntk_t * Abc_NtkDrwsat( Abc_Ntk_t * pNtk, int fBalance, int fVerbose )
     Abc_Ntk_t * pNtkAig;
     int clk;
     assert( Abc_NtkIsStrash(pNtk) );
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
 //    Aig_ManPrintStats( pMan );
@@ -696,7 +727,7 @@ Abc_Ntk_t * Abc_NtkDarToCnf( Abc_Ntk_t * pNtk, char * pFileName )
     assert( Abc_NtkIsStrash(pNtk) );
 
     // convert to the AIG manager
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
     if ( !Aig_ManCheck( pMan ) )
@@ -751,7 +782,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
     assert( Abc_NtkPoNum(pNtk) == 1 );
 
     // conver to the manager
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     // derive CNF
 //    pCnf = Cnf_Derive( pMan, 0 );
     pCnf = Cnf_DeriveSimple( pMan, 0 );
@@ -809,7 +840,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
         assert( 0 );
 //    PRT( "SAT sat_solver time", clock() - clk );
 //    printf( "The number of conflicts = %d.\n", (int)pSat->sat_solver_stats.conflicts );
-
+ 
     // if the problem is SAT, get the counterexample
     if ( status == l_True )
     {
@@ -836,16 +867,16 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fVerbose )
+Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fVerbose )
 {
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk );
+    pMan = Abc_NtkToDar( pNtk, 0 );
     if ( pMan == NULL )
         return NULL;
     pMan->nRegs = Abc_NtkLatchNum(pNtk);
 
-    pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fVerbose );
+    pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fVerbose );
     Aig_ManStop( pTemp );
 
     pNtkAig = Abc_NtkFromDar( pNtk, pMan );
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 445c73c1..a33b9875 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -1099,7 +1099,9 @@ int Abc_NtkCombinePos( Abc_Ntk_t * pNtk, int fAnd )
     Abc_Obj_t * pNode, * pMiter;
     int i;
     assert( Abc_NtkIsStrash(pNtk) );
-    assert( Abc_NtkLatchNum(pNtk) == 0 );
+//    assert( Abc_NtkLatchNum(pNtk) == 0 );
+    if ( Abc_NtkPoNum(pNtk) == 1 )
+        return 1;
     // start the result
     if ( fAnd )
         pMiter = Abc_AigConst1(pNtk);
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 978b7cdb..4fdb7cbc 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -87,6 +87,71 @@ Abc_Ntk_t * Abc_NtkRestrash( Abc_Ntk_t * pNtk, bool fCleanup )
 
 /**Function*************************************************************
 
+  Synopsis    [Reapplies structural hashing to the AIG.]
+
+  Description [Because of the structural hashing, this procedure should not 
+  change the number of nodes. It is useful to detect the bugs in the original AIG.]
+               
+  SideEffects []
+ 
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkRestrashZero( Abc_Ntk_t * pNtk, bool fCleanup )
+{
+    extern int timeRetime;
+    Abc_Ntk_t * pNtkAig;
+    Abc_Obj_t * pObj;
+    int i, nNodes;//, RetValue;
+    assert( Abc_NtkIsStrash(pNtk) );
+//timeRetime = clock();
+    // print warning about choice nodes
+    if ( Abc_NtkGetChoiceNum( pNtk ) )
+        printf( "Warning: The choice nodes in the original AIG are removed by strashing.\n" );
+    // start the new network (constants and CIs of the old network will point to the their counterparts in the new network)
+    pNtkAig = Abc_NtkStartFrom( pNtk, ABC_NTK_STRASH, ABC_FUNC_AIG );
+    // complement the 1-values registers
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        if ( Abc_LatchIsInit1(pObj) )
+            Abc_ObjFanout0(pObj)->pCopy = Abc_ObjNot(Abc_ObjFanout0(pObj)->pCopy);
+    // restrash the nodes (assuming a topological order of the old network)
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        pObj->pCopy = Abc_AigAnd( pNtkAig->pManFunc, Abc_ObjChild0Copy(pObj), Abc_ObjChild1Copy(pObj) );
+    // finalize the network
+    Abc_NtkFinalize( pNtk, pNtkAig );
+    // complement the 1-valued registers
+    Abc_NtkForEachLatch( pNtkAig, pObj, i )
+        if ( Abc_LatchIsInit1(pObj) )
+            Abc_ObjXorFaninC( Abc_ObjFanin0(pObj), 0 );
+    // set all constant-0 values
+    Abc_NtkForEachLatch( pNtkAig, pObj, i )
+        Abc_LatchSetInit0( pObj );
+
+    // print warning about self-feed latches
+//    if ( Abc_NtkCountSelfFeedLatches(pNtkAig) )
+//        printf( "Warning: The network has %d self-feeding latches.\n", Abc_NtkCountSelfFeedLatches(pNtkAig) );
+    // perform cleanup if requested
+    if ( fCleanup && (nNodes = Abc_AigCleanup(pNtkAig->pManFunc)) ) 
+        printf( "Abc_NtkRestrash(): AIG cleanup removed %d nodes (this is a bug).\n", nNodes );
+    // duplicate EXDC 
+    if ( pNtk->pExdc )
+        pNtkAig->pExdc = Abc_NtkDup( pNtk->pExdc );
+    // make sure everything is okay
+    if ( !Abc_NtkCheck( pNtkAig ) )
+    {
+        printf( "Abc_NtkStrash: The network check has failed.\n" );
+        Abc_NtkDelete( pNtkAig );
+        return NULL;
+    }
+//timeRetime = clock() - timeRetime;
+//    if ( RetValue = Abc_NtkRemoveSelfFeedLatches(pNtkAig) )
+//        printf( "Modified %d self-feeding latches. The result will not verify.\n", RetValue );
+    return pNtkAig;
+
+}
+
+/**Function*************************************************************
+
   Synopsis    [Transforms logic network into structurally hashed AIG.]
 
   Description []
diff --git a/src/base/io/ioReadAiger.c b/src/base/io/ioReadAiger.c
index fe519476..23b5b350 100644
--- a/src/base/io/ioReadAiger.c
+++ b/src/base/io/ioReadAiger.c
@@ -123,7 +123,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
         // assign names to latch and its input
         Abc_ObjAssignName( pObj, Abc_ObjNameDummy("_L", i, nDigits), NULL );
 
-        printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id );
+//        printf( "Creating latch %s with input %d and output %d.\n", Abc_ObjName(pObj), pNode0->Id, pNode1->Id );
     } 
     
     // remember the beginning of latch/PO literals
@@ -161,7 +161,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
         pNode0 = Abc_ObjNotCond( Vec_PtrEntry(vNodes, uLit0 >> 1), (uLit0 & 1) );//^ (uLit0 < 2) );
         Abc_ObjAddFanin( pObj, pNode0 );
 
-        printf( "Adding input %d to latch input %d.\n", pNode0->Id, pObj->Id );
+//        printf( "Adding input %d to latch input %d.\n", pNode0->Id, pObj->Id );
 
     }
     // read the PO driver literals
@@ -233,7 +233,7 @@ Abc_Ntk_t * Io_ReadAiger( char * pFileName, int fCheck )
     }
 
     // remove the extra nodes
-//    Abc_AigCleanup( pNtkNew->pManFunc );
+    Abc_AigCleanup( pNtkNew->pManFunc );
 
     // check the result
     if ( fCheck && !Abc_NtkCheckRead( pNtkNew ) )