Version abc80517

31 files changed, 995 insertions, 493 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 6987412d..5861bc36 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -150,6 +150,8 @@ struct Aig_Man_t_
     void *           pSeqModel;
     Aig_Man_t *      pManExdc;
     Vec_Ptr_t *      vOnehots;
+    Aig_Man_t *      pManHaig;
+    int              fCreatePios;
     // timing statistics
     int              time1;
     int              time2;
@@ -322,7 +324,8 @@ static inline void         Aig_ObjClean( Aig_Obj_t * pObj )       { memset( pObj
 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 Aig_Obj_t *  Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj )    { return p->pEquivs? p->pEquivs[pObj->Id] : NULL;           } 
 static inline Aig_Obj_t *  Aig_ObjRepr( Aig_Man_t * p, Aig_Obj_t * pObj )     { return p->pReprs? p->pReprs[pObj->Id] : NULL;             } 
-static inline int          Aig_ObjPioNum( Aig_Obj_t * pObj )      { assert( !Aig_ObjIsNode(pObj) ); return (int)(long)pObj->pNext;                                                    }
+static inline Aig_Obj_t *  Aig_ObjHaig( Aig_Obj_t * pObj )        { assert( Aig_Regular(pObj)->pHaig ); return Aig_NotCond( Aig_Regular(pObj)->pHaig, Aig_IsComplement(pObj) );      } 
+static inline int          Aig_ObjPioNum( Aig_Obj_t * pObj )      { assert( !Aig_ObjIsNode(pObj) ); return (int)(long)pObj->pNext;                                                   }
 static inline int          Aig_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )    
 { 
     if ( Aig_ObjFanin0(pObj) == pFanin ) return 0; 
@@ -469,11 +472,12 @@ extern Aig_Obj_t *     Aig_Compose( Aig_Man_t * p, Aig_Obj_t * pRoot, Aig_Obj_t
 extern void            Aig_ObjCollectCut( Aig_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vNodes );
 extern int             Aig_ObjCollectSuper( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper );
 /*=== aigDup.c ==========================================================*/
-extern Aig_Man_t *     Aig_ManDup( Aig_Man_t * p );
+extern Aig_Man_t *     Aig_ManDupSimple( Aig_Man_t * p );
+extern Aig_Man_t *     Aig_ManDupSimpleDfs( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupOrdered( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupExor( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupDfs( Aig_Man_t * p );
-extern Aig_Man_t *     Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder );
+extern Aig_Man_t *     Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide );
 extern Aig_Man_t *     Aig_ManDupLevelized( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupWithoutPos( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupRepres( Aig_Man_t * p );
@@ -487,15 +491,15 @@ extern void            Aig_ManFanoutStart( Aig_Man_t * p );
 extern void            Aig_ManFanoutStop( Aig_Man_t * p );
 /*=== aigFrames.c ==========================================================*/
 extern Aig_Man_t *     Aig_ManFrames( Aig_Man_t * pAig, int nFs, int fInit, int fOuts, int fRegs, int fEnlarge, Aig_Obj_t *** ppObjMap );
-/*=== aigHaig.c ==========================================================*/
-extern void            Aig_ManHaigRecord( Aig_Man_t * p );
 /*=== aigMan.c ==========================================================*/
 extern Aig_Man_t *     Aig_ManStart( int nNodesMax );
 extern Aig_Man_t *     Aig_ManStartFrom( Aig_Man_t * p );
 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 int             Aig_ManAntiCleanup( Aig_Man_t * p );
 extern int             Aig_ManPiCleanup( Aig_Man_t * p );
+extern int             Aig_ManPoCleanup( Aig_Man_t * p );
 extern void            Aig_ManPrintStats( Aig_Man_t * p );
 extern void            Aig_ManReportImprovement( Aig_Man_t * p, Aig_Man_t * pNew );
 extern void            Aig_ManSetRegNum( Aig_Man_t * p, int nRegs );
@@ -517,9 +521,9 @@ extern void            Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_
 extern void            Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern void            Aig_ObjDelete( Aig_Man_t * p, Aig_Obj_t * pObj );
 extern void            Aig_ObjDelete_rec( Aig_Man_t * p, Aig_Obj_t * pObj, int fFreeTop );
-extern void            Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew );
-extern void            Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel );
 extern void            Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj );
+extern void            Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew );
+extern void            Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fUpdateLevel );
 /*=== aigOper.c =========================================================*/
 extern Aig_Obj_t *     Aig_IthVar( Aig_Man_t * p, int i );
 extern Aig_Obj_t *     Aig_Oper( Aig_Man_t * p, Aig_Obj_t * p0, Aig_Obj_t * p1, Aig_Type_t Type );
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index fc01e7f0..1ec92968 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -40,11 +40,13 @@
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Aig_ManDup( Aig_Man_t * p )
+Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
 {
     Aig_Man_t * pNew;
     Aig_Obj_t * pObj, * pObjNew;
     int i;
+    assert( p->pManTime == NULL );
+    assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
     pNew->pName = Aig_UtilStrsav( p->pName );
@@ -88,12 +90,109 @@ Aig_Man_t * Aig_ManDup( Aig_Man_t * p )
         pObj->pData = pObjNew;
     }
     assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
-    // duplicate the timing manager
-    if ( p->pManTime )
-        pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+    // pass the HAIG manager
+    if ( p->pManHaig != NULL )
+    {
+        pNew->pManHaig = p->pManHaig;  
+        p->pManHaig = NULL;
+    }
     // check the resulting network
     if ( !Aig_ManCheck(pNew) )
-        printf( "Aig_ManDup(): The check has failed.\n" );
+        printf( "Aig_ManDupSimple(): The check has failed.\n" );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager recursively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Obj_t * Aig_ManDupSimpleDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    if ( pObj->pData )
+        return pObj->pData;
+    Aig_ManDupSimpleDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );
+    if ( Aig_ObjIsBuf(pObj) )
+        return pObj->pData = Aig_ObjChild0Copy(pObj);
+    Aig_ManDupSimpleDfs_rec( pNew, p, Aig_ObjFanin1(pObj) );
+    pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    Aig_Regular(pObj->pData)->pHaig = pObj->pHaig;
+    return pObj->pData;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG manager.]
+
+  Description [Orders nodes as follows: PIs, ANDs, POs.]
+               
+  SideEffects [This procedure assumes that buffers are not used during
+  HAIG recording. This way, each HAIG node is in one-to-one correspondence 
+  with old HAIG node. There is no need to create new nodes, just reassign 
+  the pointers. If it were not the case, we would need to create HAIG nodes 
+  for each new node duplicated. ]
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjNew;
+    int i;
+    assert( p->pManTime == NULL );
+    assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    pNew->nRegs = p->nRegs;
+    pNew->nTruePis = p->nTruePis;
+    pNew->nTruePos = p->nTruePos;
+    pNew->nAsserts = p->nAsserts;
+    if ( p->vFlopNums )
+        pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
+    Aig_ManForEachPi( p, pObj, i )
+    {
+        pObjNew = Aig_ObjCreatePi( pNew );
+        pObjNew->pHaig = pObj->pHaig;
+        pObjNew->Level = pObj->Level;
+        pObj->pData = pObjNew;
+    }
+    // duplicate internal nodes
+    Aig_ManForEachObj( p, pObj, i )
+        if ( !Aig_ObjIsPo(pObj) )
+        {
+            Aig_ManDupSimpleDfs_rec( pNew, p, pObj );        
+            assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
+        }
+    // add the POs
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+        pObjNew->pHaig = pObj->pHaig;
+        pObj->pData = pObjNew;
+    }
+    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
+    // pass the HAIG manager
+    if ( p->pManHaig != NULL )
+    {
+        pNew->pManHaig = p->pManHaig;  
+        p->pManHaig = NULL;
+    }
+    // check the resulting network
+    if ( !Aig_ManCheck(pNew) )
+        printf( "Aig_ManDupSimple(): The check has failed.\n" );
     return pNew;
 }
 
@@ -160,6 +259,12 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
     // duplicate the timing manager
     if ( p->pManTime )
         pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+    // pass the HAIG manager
+    if ( p->pManHaig != NULL )
+    {
+        pNew->pManHaig = p->pManHaig;  
+        p->pManHaig = NULL;
+    }
     // check the resulting network
     if ( !Aig_ManCheck(pNew) )
         printf( "Aig_ManDupOrdered(): The check has failed.\n" );
@@ -255,7 +360,9 @@ Aig_Obj_t * Aig_ManDupDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj
         return pObj->pData = Aig_ObjChild0Copy(pObj);
     Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin1(pObj) );
     pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
-    if ( pObj->pHaig )
+    if ( p->pManHaig != NULL )
+        Aig_Regular(pObjNew)->pHaig = Aig_NotCond( pObj->pHaig, Aig_IsComplement(pObjNew) );
+    else if ( pObj->pHaig )
         Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
     if ( pEquivNew )
     {
@@ -313,7 +420,7 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
         {
             pObjNew = Aig_ObjCreatePi( pNew );
             pObjNew->Level = pObj->Level;
-            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+            pObjNew->pHaig = pObj->pHaig;
             pObj->pData = pObjNew;
         }
         else if ( Aig_ObjIsPo(pObj) )
@@ -321,7 +428,7 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
             Aig_ManDupDfs_rec( pNew, p, Aig_ObjFanin0(pObj) );        
 //            assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
             pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
+            pObjNew->pHaig = pObj->pHaig;
             pObj->pData = pObjNew;
         }
     }
@@ -331,6 +438,12 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
     // duplicate the timing manager
     if ( p->pManTime )
         pNew->pManTime = Tim_ManDup( p->pManTime, 0 );
+    // pass the HAIG manager
+    if ( p->pManHaig != NULL )
+    {
+        pNew->pManHaig = p->pManHaig;  
+        p->pManHaig = NULL;
+    }
     // check the resulting network
     if ( !Aig_ManCheck(pNew) )
         printf( "Aig_ManDupDfs(): The check has failed.\n" );
@@ -379,7 +492,7 @@ Vec_Ptr_t * Aig_ManOrderPios( Aig_Man_t * p, Aig_Man_t * pOrder )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Obj_t * Aig_ManDupDfsOrder_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
+Aig_Obj_t * Aig_ManDupDfsGuided_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
 {
     Aig_Obj_t * pObjNew, * pEquivNew = NULL;
     if ( pObj->pData )
@@ -387,12 +500,12 @@ Aig_Obj_t * Aig_ManDupDfsOrder_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t *
     if ( Aig_ObjIsPi(pObj) )
         return NULL;
     if ( p->pEquivs && Aig_ObjEquiv(p, pObj) )
-        pEquivNew = Aig_ManDupDfsOrder_rec( pNew, p, Aig_ObjEquiv(p, pObj) );
-    if ( !Aig_ManDupDfsOrder_rec( pNew, p, Aig_ObjFanin0(pObj) ) )
+        pEquivNew = Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjEquiv(p, pObj) );
+    if ( !Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjFanin0(pObj) ) )
         return NULL;
     if ( Aig_ObjIsBuf(pObj) )
         return pObj->pData = Aig_ObjChild0Copy(pObj);
-    if ( !Aig_ManDupDfsOrder_rec( pNew, p, Aig_ObjFanin1(pObj) ) )
+    if ( !Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjFanin1(pObj) ) )
         return NULL;
     pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
     if ( pObj->pHaig )
@@ -418,7 +531,7 @@ Aig_Obj_t * Aig_ManDupDfsOrder_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t *
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder )
+Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide )
 {
     Vec_Ptr_t * vPios;
     Aig_Man_t * pNew;
@@ -448,7 +561,7 @@ Aig_Man_t * Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder )
     // duplicate internal nodes
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
     Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
-    vPios = Aig_ManOrderPios( p, pOrder );
+    vPios = Aig_ManOrderPios( p, pGuide );
     Vec_PtrForEachEntry( vPios, pObj, i )
     {
         if ( Aig_ObjIsPi(pObj) )
@@ -460,7 +573,7 @@ Aig_Man_t * Aig_ManDupDfsOrder( Aig_Man_t * p, Aig_Man_t * pOrder )
         }
         else if ( Aig_ObjIsPo(pObj) )
         {
-            Aig_ManDupDfsOrder_rec( pNew, p, Aig_ObjFanin0(pObj) );        
+            Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjFanin0(pObj) );        
 //            assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
             pObjNew = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
             Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
diff --git a/src/aig/aig/aigHaig.c b/src/aig/aig/aigHaig.c
deleted file mode 100644
index 491a09a3..00000000
--- a/src/aig/aig/aigHaig.c
+++ /dev/null
@@ -1,271 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [aigHaig.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [AIG package.]
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - April 28, 2007.]
-
-  Revision    [$Id: aigHaig.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "aig.h"
-#include "satSolver.h"
-#include "cnf.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static inline Aig_Obj_t *  Aig_HaigObjFrames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int f )                       { return ppMap[nFrames*pObj->Id + f];  }
-static inline void         Aig_HaigObjSetFrames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int f, Aig_Obj_t * pNode ) { ppMap[nFrames*pObj->Id + f] = pNode; }
-static inline Aig_Obj_t *  Aig_HaigObjChild0Frames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i )                 { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Aig_HaigObjFrames(ppMap,nFrames,Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL;  }
-static inline Aig_Obj_t *  Aig_HaigObjChild1Frames( Aig_Obj_t ** ppMap, int nFrames, Aig_Obj_t * pObj, int i )                 { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Aig_HaigObjFrames(ppMap,nFrames,Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL;  }
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Performs speculative reduction for one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Aig_ManHaigFramesNode( Aig_Obj_t ** ppMap, int nFrames, Aig_Man_t * pFrames, Aig_Obj_t * pObj, int iFrame )
-{
-    Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
-    // skip nodes without representative
-    pObjRepr = pObj->pHaig;
-    if ( pObjRepr == NULL )
-        return;
-    assert( !Aig_IsComplement(pObjRepr) );
-    assert( pObjRepr->Id < pObj->Id );
-    // get the new node 
-    pObjNew = Aig_HaigObjFrames( ppMap, nFrames, pObj, iFrame );
-    // get the new node of the representative
-    pObjReprNew = Aig_HaigObjFrames( ppMap, nFrames, pObjRepr, iFrame );
-    // if this is the same node, no need to add constraints
-    if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
-        return;
-    // these are different nodes - perform speculative reduction
-    pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
-    // set the new node
-    Aig_HaigObjSetFrames( ppMap, nFrames, pObj, iFrame, pObjNew2 );
-    // add the constraint
-    pMiter = Aig_Exor( pFrames, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) );
-    pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
-    pMiter = Aig_Not( pMiter );
-    Aig_ObjCreatePo( pFrames, pMiter );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the inductive case with speculative reduction.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames )
-{
-    Aig_Man_t * pFrames;
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
-    Aig_Obj_t ** ppMap;
-    int i, k, f;
-    assert( nFrames >= 2 );
-    assert( Aig_ManRegNum(pHaig) > 0 );
-    assert( Aig_ManRegNum(pHaig) < Aig_ManPiNum(pHaig) );
-
-    // create node mapping
-    ppMap = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pHaig) * nFrames );
-    memset( ppMap, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pHaig) * nFrames );
-
-    // start the frames
-    pFrames = Aig_ManStart( Aig_ManObjNumMax(pHaig) * nFrames );
-    pFrames->pName = Aig_UtilStrsav( pHaig->pName );
-    pFrames->pSpec = Aig_UtilStrsav( pHaig->pSpec );
-    pFrames->nRegs = pHaig->nRegs;
-
-    // create PI nodes for the frames
-    for ( f = 0; f < nFrames; f++ )
-        Aig_HaigObjSetFrames( ppMap, nFrames, Aig_ManConst1(pHaig), f, Aig_ManConst1(pFrames) );
-    for ( f = 0; f < nFrames; f++ )
-        Aig_ManForEachPiSeq( pHaig, pObj, i )
-            Aig_HaigObjSetFrames( ppMap, nFrames, pObj, f, Aig_ObjCreatePi(pFrames) );
-    // create latches for the first frame
-    Aig_ManForEachLoSeq( pHaig, pObj, i )
-        Aig_HaigObjSetFrames( ppMap, nFrames, pObj, 0, Aig_ObjCreatePi(pFrames) );
-
-    // add timeframes
-    for ( f = 0; f < nFrames; f++ )
-    {
-        // mark the asserts
-        if ( f == nFrames - 1 )
-            pFrames->nAsserts = Aig_ManPoNum(pFrames);
-        // constrain latch outputs and internal nodes
-        Aig_ManForEachObj( pHaig, pObj, i )
-        {
-            if ( Aig_ObjIsPi(pObj) && Aig_HaigObjFrames(ppMap, nFrames, pObj, f) == NULL )
-            {
-                Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f );
-            }
-            else if ( Aig_ObjIsNode(pObj) )
-            {
-                pObjNew = Aig_And( pFrames, 
-                    Aig_HaigObjChild0Frames(ppMap,nFrames,pObj,f), 
-                    Aig_HaigObjChild1Frames(ppMap,nFrames,pObj,f) );
-                Aig_HaigObjSetFrames( ppMap, nFrames, pObj, f, pObjNew );
-                Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f );
-            }
-        }
-
-/*
-        // set the constraints on the latch outputs
-        Aig_ManForEachLoSeq( pHaig, pObj, i )
-            Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f );
-        // add internal nodes of this frame
-        Aig_ManForEachNode( pHaig, pObj, i )
-        {
-            pObjNew = Aig_And( pFrames, 
-                Aig_HaigObjChild0Frames(ppMap,nFrames,pObj,f), 
-                Aig_HaigObjChild1Frames(ppMap,nFrames,pObj,f) );
-            Aig_HaigObjSetFrames( ppMap, nFrames, pObj, f, pObjNew );
-            Aig_ManHaigFramesNode( ppMap, nFrames, pFrames, pObj, f );
-        }
-*/
-        // transfer latch inputs to the latch outputs 
-        Aig_ManForEachLiLoSeq( pHaig, pObjLi, pObjLo, k )
-        {
-            pObjNew = Aig_HaigObjChild0Frames(ppMap,nFrames,pObjLi,f);
-            Aig_HaigObjSetFrames( ppMap, nFrames, pObjLo, f+1, pObjNew );
-        }
-    }
-
-    // remove dangling nodes
-    Aig_ManCleanup( pFrames );
-    free( ppMap );
-    return pFrames;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManHaigVerify( Aig_Man_t * pHaig )
-{
-    int nBTLimit = 0;
-    Aig_Man_t * pFrames;
-    Cnf_Dat_t * pCnf;
-    sat_solver * pSat;
-    Aig_Obj_t * pObj;
-    int i, Lit, RetValue, Counter;
-    int clk = clock();
-
-    // create time frames with speculative reduction and convert them into CNF
-clk = clock();
-    pFrames = Aig_ManHaigFrames( pHaig, 2 );
-    pCnf = Cnf_DeriveSimple( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
-//    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
-//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
-    // create the SAT solver to be used for this problem
-    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
-
-    printf( "HAIG regs = %d. HAIG nodes = %d. Outputs = %d.\n", 
-        Aig_ManRegNum(pHaig), Aig_ManNodeNum(pHaig), Aig_ManPoNum(pHaig) );
-    printf( "Frames regs = %d. Frames nodes = %d. Outputs = %d. Assumptions = %d. Asserts = %d.\n", 
-        Aig_ManRegNum(pFrames), Aig_ManNodeNum(pFrames), Aig_ManPoNum(pFrames), 
-        pFrames->nAsserts, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
-
-PRT( "Preparation", clock() - clk );
-    if ( pSat == NULL )
-    {
-        printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
-        return -1;
-    }
-    
-    // solve each output
-clk = clock();
-    Counter = 0;
-    Aig_ManForEachPo( pFrames, pObj, i )
-    {
-        if ( i < pFrames->nAsserts )
-            continue;
-        Lit = toLitCond( pCnf->pVarNums[pObj->Id], pObj->fPhase );
-        RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
-        if ( RetValue != l_False )
-            Counter++;
-    }
-PRT( "Solving    ", clock() - clk );
-    if ( Counter )
-        printf( "Verification failed for %d classes.\n", Counter );
-    else
-        printf( "Verification is successful.\n" );
-
-    // clean up
-    Aig_ManStop( pFrames );
-    Cnf_DataFree( pCnf );
-    sat_solver_delete( pSat );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManHaigRecord( Aig_Man_t * p )
-{
-    Aig_Man_t * pNew;
-    Aig_Obj_t * pObj;
-    int i;
-    // start the HAIG
-    p->pManHaig = Aig_ManDupOrdered( p );
-    // set the pointers to the HAIG nodes
-    Aig_ManForEachObj( p, pObj, i )
-        pObj->pHaig = pObj->pData;
-    // remove structural hashing table
-    Aig_TableClear( p->pManHaig );
-    // perform a sequence of synthesis steps
-    pNew = Aig_ManRetimeFrontier( p, 10000 );
-    // use the haig for verification
-    Aig_ManDumpBlif( pNew->pManHaig, "haig_temp.blif", NULL, NULL );
-    Aig_ManHaigVerify( pNew->pManHaig );
-    Aig_ManStop( pNew );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 669691f4..9877fdae 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -163,7 +163,7 @@ Aig_Man_t * Aig_ManExtractMiter( Aig_Man_t * p, Aig_Obj_t * pNode1, Aig_Obj_t *
     Aig_ObjCreatePo( pNew, pObj );
     // check the resulting network
     if ( !Aig_ManCheck(pNew) )
-        printf( "Aig_ManDup(): The check has failed.\n" );
+        printf( "Aig_ManExtractMiter(): The check has failed.\n" );
     return pNew;
 }
 
@@ -235,8 +235,7 @@ int Aig_ManCleanup( Aig_Man_t * p )
 {
     Vec_Ptr_t * vObjs;
     Aig_Obj_t * pNode;
-    int i, nNodesOld;
-    nNodesOld = Aig_ManNodeNum(p);
+    int i, nNodesOld = Aig_ManNodeNum(p);
     // collect roots of dangling nodes
     vObjs = Vec_PtrAlloc( 100 );
     Aig_ManForEachObj( p, pNode, i )
@@ -251,6 +250,27 @@ int Aig_ManCleanup( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Adds POs for the nodes that otherwise would be dangling.]
+
+  Description [Returns the number of POs added.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManAntiCleanup( Aig_Man_t * p )
+{
+    Aig_Obj_t * pNode;
+    int i, nNodesOld = Aig_ManPoNum(p);
+    Aig_ManForEachObj( p, pNode, i )
+        if ( Aig_ObjIsNode(pNode) && Aig_ObjRefs(pNode) == 0 )
+            Aig_ObjCreatePo( p, pNode );
+    return nNodesOld - Aig_ManPoNum(p);
+}
+
+/**Function*************************************************************
+
   Synopsis    [Removes PIs without fanouts.]
 
   Description [Returns the number of PIs removed.]
@@ -282,6 +302,40 @@ int Aig_ManPiCleanup( Aig_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Removes POs with constant input.]
+
+  Description [Returns the number of POs removed.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManPoCleanup( Aig_Man_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, k = 0, nPosOld = Aig_ManPoNum(p);
+    Vec_PtrForEachEntry( p->vPos, pObj, i )
+    {
+        if ( i >= Aig_ManPoNum(p) - Aig_ManRegNum(p) )
+            Vec_PtrWriteEntry( p->vPos, k++, pObj );
+        else if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) || !Aig_ObjFaninC0(pObj) ) // non-const or const1
+            Vec_PtrWriteEntry( p->vPos, k++, pObj );
+        else
+        {
+            Aig_ObjDisconnect( p, pObj );
+            Vec_PtrWriteEntry( p->vObjs, pObj->Id, NULL );
+        }
+    }
+    Vec_PtrShrink( p->vPos, k );
+    p->nObjs[AIG_OBJ_PO] = Vec_PtrSize( p->vPos );
+    if ( Aig_ManRegNum(p) )
+        p->nTruePos = Aig_ManPoNum(p) - Aig_ManRegNum(p);
+    return nPosOld - Aig_ManPoNum(p);
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs one iteration of AIG rewriting.]
 
   Description []
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index 73b15caf..b5a404ab 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -46,6 +46,12 @@ Aig_Obj_t * Aig_ObjCreatePi( Aig_Man_t * p )
     pObj->Type = AIG_OBJ_PI;
     Vec_PtrPush( p->vPis, pObj );
     p->nObjs[AIG_OBJ_PI]++;
+    if ( p->pManHaig && p->fCreatePios )
+    {
+        p->pManHaig->nRegs++;
+        pObj->pHaig = Aig_ObjCreatePi( p->pManHaig );
+//        printf( "Creating PI HAIG node %d equivalent to PI %d.\n", pObj->pHaig->Id, pObj->Id );
+    }
     return pObj;
 }
 
@@ -68,6 +74,11 @@ Aig_Obj_t * Aig_ObjCreatePo( Aig_Man_t * p, Aig_Obj_t * pDriver )
     Vec_PtrPush( p->vPos, pObj );
     Aig_ObjConnect( p, pObj, pDriver, NULL );
     p->nObjs[AIG_OBJ_PO]++;
+    if ( p->pManHaig && p->fCreatePios )
+    {
+        pObj->pHaig = Aig_ObjCreatePo( p->pManHaig, Aig_ObjHaig( pDriver ) );
+//        printf( "Creating PO HAIG node %d equivalent to PO %d.\n", pObj->pHaig->Id, pObj->Id );
+    }
     return pObj;
 }
 
@@ -88,7 +99,7 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
     Aig_Obj_t * pObj;
     assert( !Aig_IsComplement(pGhost) );
     assert( Aig_ObjIsHash(pGhost) );
-    assert( pGhost == &p->Ghost );
+//    assert( pGhost == &p->Ghost );
     // get memory for the new object
     pObj = Aig_ManFetchMemory( p );
     pObj->Type = pGhost->Type;
@@ -97,6 +108,14 @@ Aig_Obj_t * Aig_ObjCreate( Aig_Man_t * p, Aig_Obj_t * pGhost )
     // update node counters of the manager
     p->nObjs[Aig_ObjType(pObj)]++;
     assert( pObj->pData == NULL );
+    if ( p->pManHaig )
+    {
+        pGhost->pFanin0 = Aig_ObjHaig( pGhost->pFanin0 );
+        pGhost->pFanin1 = Aig_ObjHaig( pGhost->pFanin1 );
+        pObj->pHaig = Aig_ObjCreate( p->pManHaig, pGhost );
+        assert( !Aig_IsComplement(pObj->pHaig) );
+//        printf( "Creating  HAIG node %d equivalent to node %d.\n", pObj->pHaig->Id, pObj->Id );
+    }
     return pObj;
 }
 
@@ -137,7 +156,7 @@ void Aig_ObjConnect( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFan0, Aig_Obj
     pObj->Level = Aig_ObjLevelNew( pObj );
     pObj->fPhase = Aig_ObjPhaseReal(pFan0) & Aig_ObjPhaseReal(pFan1);
     // add the node to the structural hash table
-    if ( Aig_ObjIsHash(pObj) )
+    if ( p->pTable && Aig_ObjIsHash(pObj) )
         Aig_TableInsert( p, pObj );
     // add the node to the dynamically updated topological order
 //    if ( p->pOrderData && Aig_ObjIsNode(pObj) )
@@ -173,7 +192,7 @@ void Aig_ObjDisconnect( Aig_Man_t * p, Aig_Obj_t * pObj )
         Aig_ObjDeref(Aig_ObjFanin1(pObj));
     }
     // remove the node from the structural hash table
-    if ( Aig_ObjIsHash(pObj) )
+    if ( p->pTable && Aig_ObjIsHash(pObj) )
         Aig_TableDelete( p, pObj );
     // add the first fanin
     pObj->pFanin0 = NULL;
@@ -271,6 +290,81 @@ void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew
 
 /**Function*************************************************************
 
+  Synopsis    [Verbose printing of the AIG node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj )
+{
+    int fHaig = 0;
+    int fShowFanouts = 0;
+    Aig_Obj_t * pTemp;
+    assert( !Aig_IsComplement(pObj) );
+    printf( "Node %4d : ", Aig_ObjId(pObj) );
+    if ( Aig_ObjIsConst1(pObj) )
+        printf( "constant 1" );
+    else if ( Aig_ObjIsPi(pObj) )
+        printf( "PI" );
+    else if ( Aig_ObjIsPo(pObj) )
+        printf( "PO( %4d%s )", Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " ") );
+    else if ( Aig_ObjIsBuf(pObj) )
+        printf( "BUF( %d%s )", Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " ") );
+    else
+        printf( "AND( %4d%s, %4d%s )", 
+            Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " "), 
+            Aig_ObjFanin1(pObj)->Id, (Aig_ObjFaninC1(pObj)? "\'" : " ") );
+    printf( " (refs = %3d)", Aig_ObjRefs(pObj) );
+    if ( fShowFanouts && p->pFanData )
+    {
+        Aig_Obj_t * pFanout;
+        int i, iFan;
+        printf( "\nFanouts:\n" );
+        Aig_ObjForEachFanout( p, pObj, pFanout, iFan, i )
+        {
+            printf( "    " );
+            printf( "Node %4d : ", Aig_ObjId(pFanout) );
+            if ( Aig_ObjIsPo(pFanout) )
+                printf( "PO( %4d%s )", Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " ") );
+            else if ( Aig_ObjIsBuf(pFanout) )
+                printf( "BUF( %d%s )", Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " ") );
+            else
+                printf( "AND( %4d%s, %4d%s )", 
+                    Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " "), 
+                    Aig_ObjFanin1(pFanout)->Id, (Aig_ObjFaninC1(pFanout)? "\'" : " ") );
+            printf( "\n" );
+        }
+        return;
+    }
+    if ( fHaig )
+    {
+        if ( pObj->pHaig == NULL )
+            printf( " HAIG node not given" );
+        else
+            printf( " HAIG node = %d%s", Aig_Regular(pObj->pHaig)->Id, (Aig_IsComplement(pObj->pHaig)? "\'" : " ") );
+        return;
+    }
+    // there are choices
+    if ( p->pEquivs && p->pEquivs[pObj->Id] )
+    {
+        // print equivalence class
+        printf( "  { %4d ", pObj->Id );
+        for ( pTemp = p->pEquivs[pObj->Id]; pTemp; pTemp = p->pEquivs[pTemp->Id] )
+            printf( " %4d%s", pTemp->Id, (pTemp->fPhase != pObj->fPhase)? "\'" : " " );
+        printf( " }" );
+        return;
+    }
+    // this is a secondary node
+    if ( p->pReprs && p->pReprs[pObj->Id] )
+        printf( "  class of %d", pObj->Id );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Replaces node with a buffer fanin by a node without them.]
 
   Description []
@@ -280,7 +374,7 @@ void Aig_ObjPatchFanin0( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFaninNew
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_NodeFixBufferFanins( Aig_Man_t * p, Aig_Obj_t * pObj, int fNodesOnly, int fUpdateLevel )
+void Aig_NodeFixBufferFanins( Aig_Man_t * p, Aig_Obj_t * pObj, int fUpdateLevel )
 {
     Aig_Obj_t * pFanReal0, * pFanReal1, * pResult;
     p->nBufFixes++;
@@ -305,7 +399,7 @@ void Aig_NodeFixBufferFanins( Aig_Man_t * p, Aig_Obj_t * pObj, int fNodesOnly, i
     else 
         assert( 0 );
     // replace the node with buffer by the node without buffer
-    Aig_ObjReplace( p, pObj, pResult, fNodesOnly, fUpdateLevel );
+    Aig_ObjReplace( p, pObj, pResult, fUpdateLevel );
 }
 
 /**Function*************************************************************
@@ -319,7 +413,7 @@ void Aig_NodeFixBufferFanins( Aig_Man_t * p, Aig_Obj_t * pObj, int fNodesOnly, i
   SeeAlso     [] 
 
 ***********************************************************************/
-int Aig_ManPropagateBuffers( Aig_Man_t * p, int fNodesOnly, int fUpdateLevel )
+int Aig_ManPropagateBuffers( Aig_Man_t * p, int fUpdateLevel )
 {
     Aig_Obj_t * pObj;
     int nSteps;
@@ -329,7 +423,7 @@ int Aig_ManPropagateBuffers( Aig_Man_t * p, int fNodesOnly, int fUpdateLevel )
         // get the node with a buffer fanin
         for ( pObj = Vec_PtrEntryLast(p->vBufs); Aig_ObjIsBuf(pObj); pObj = Aig_ObjFanout0(p, pObj) );
         // replace this node by a node without buffer
-        Aig_NodeFixBufferFanins( p, pObj, fNodesOnly, fUpdateLevel );
+        Aig_NodeFixBufferFanins( p, pObj, fUpdateLevel );
         // stop if a cycle occured
         if ( nSteps > 1000000 )
         {
@@ -354,15 +448,13 @@ int Aig_ManPropagateBuffers( Aig_Man_t * p, int fNodesOnly, int fUpdateLevel )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fNodesOnly, int fUpdateLevel )
+void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, int fUpdateLevel )
 {
     Aig_Obj_t * pObjNewR = Aig_Regular(pObjNew);
-    Aig_Obj_t * pHaig = pObjNewR->pHaig? pObjNewR->pHaig : pObjOld->pHaig;
     // the object to be replaced cannot be complemented
     assert( !Aig_IsComplement(pObjOld) );
     // the object to be replaced cannot be a terminal
-//    assert( !Aig_ObjIsPi(pObjOld) && !Aig_ObjIsPo(pObjOld) );
-    assert( !Aig_ObjIsPo(pObjOld) );
+    assert( !Aig_ObjIsPi(pObjOld) && !Aig_ObjIsPo(pObjOld) );
     // the object to be used cannot be a buffer or a PO
     assert( !Aig_ObjIsBuf(pObjNewR) && !Aig_ObjIsPo(pObjNewR) );
     // the object cannot be the same
@@ -375,14 +467,25 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
         printf( "Aig_ObjReplace(): Internal error!\n" );
         exit(1);
     }
+    // map the HAIG nodes
+    if ( p->pManHaig != NULL )
+    {
+//        printf( "Setting HAIG node %d equivalent to HAIG node %d (over = %d).\n", 
+//            pObjNewR->pHaig->Id, pObjOld->pHaig->Id, pObjNewR->pHaig->pHaig != NULL );
+        assert( pObjNewR->pHaig != NULL );
+//        assert( pObjNewR->pHaig->pHaig == NULL );
+        assert( !Aig_IsComplement(pObjNewR->pHaig) );
+        pObjNewR->pHaig->pHaig = pObjOld->pHaig;
+    }
+    else
+        pObjOld->pHaig = pObjNewR->pHaig? pObjNewR->pHaig : pObjOld->pHaig;
     // recursively delete the old node - but leave the object there
     pObjNewR->nRefs++;
-    if ( !Aig_ObjIsPi(pObjOld) )
-        Aig_ObjDelete_rec( p, pObjOld, 0 );
+    Aig_ObjDelete_rec( p, pObjOld, 0 );
     pObjNewR->nRefs--;
     // if the new object is complemented or already used, create a buffer
     p->nObjs[pObjOld->Type]--;
-    if ( Aig_IsComplement(pObjNew) || Aig_ObjRefs(pObjNew) > 0 || (fNodesOnly && !Aig_ObjIsNode(pObjNew)) )
+    if ( Aig_IsComplement(pObjNew) || Aig_ObjRefs(pObjNew) > 0 || !Aig_ObjIsNode(pObjNew) )
     {
         pObjOld->Type = AIG_OBJ_BUF;
         Aig_ObjConnect( p, pObjOld, pObjNew, NULL );
@@ -396,8 +499,6 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
         pObjOld->Type = pObjNew->Type;
         Aig_ObjDisconnect( p, pObjNew );
         Aig_ObjConnect( p, pObjOld, pFanin0, pFanin1 );
-        // update the haig node
-        pObjOld->pHaig = pObjNew->pHaig;
         // delete the new object
         Aig_ObjDelete( p, pObjNew );
         // update levels
@@ -418,84 +519,8 @@ void Aig_ObjReplace( Aig_Man_t * p, Aig_Obj_t * pObjOld, Aig_Obj_t * pObjNew, in
     {
         Vec_PtrPush( p->vBufs, pObjOld );
         p->nBufMax = AIG_MAX( p->nBufMax, Vec_PtrSize(p->vBufs) );
-        Aig_ManPropagateBuffers( p, fNodesOnly, fUpdateLevel );
+        Aig_ManPropagateBuffers( p, fUpdateLevel );
     }
-    pObjOld->pHaig = pHaig;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Verbose printing of the AIG node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
-    int fHaig = 0;
-    int fShowFanouts = 0;
-    Aig_Obj_t * pTemp;
-    assert( !Aig_IsComplement(pObj) );
-    printf( "Node %4d : ", Aig_ObjId(pObj) );
-    if ( Aig_ObjIsConst1(pObj) )
-        printf( "constant 1" );
-    else if ( Aig_ObjIsPi(pObj) )
-        printf( "PI" );
-    else if ( Aig_ObjIsPo(pObj) )
-        printf( "PO( %4d%s )", Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " ") );
-    else if ( Aig_ObjIsBuf(pObj) )
-        printf( "BUF( %d%s )", Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " ") );
-    else
-        printf( "AND( %4d%s, %4d%s )", 
-            Aig_ObjFanin0(pObj)->Id, (Aig_ObjFaninC0(pObj)? "\'" : " "), 
-            Aig_ObjFanin1(pObj)->Id, (Aig_ObjFaninC1(pObj)? "\'" : " ") );
-    printf( " (refs = %3d)", Aig_ObjRefs(pObj) );
-    if ( fShowFanouts && p->pFanData )
-    {
-        Aig_Obj_t * pFanout;
-        int i, iFan;
-        printf( "\nFanouts:\n" );
-        Aig_ObjForEachFanout( p, pObj, pFanout, iFan, i )
-        {
-            printf( "    " );
-            printf( "Node %4d : ", Aig_ObjId(pFanout) );
-            if ( Aig_ObjIsPo(pFanout) )
-                printf( "PO( %4d%s )", Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " ") );
-            else if ( Aig_ObjIsBuf(pFanout) )
-                printf( "BUF( %d%s )", Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " ") );
-            else
-                printf( "AND( %4d%s, %4d%s )", 
-                    Aig_ObjFanin0(pFanout)->Id, (Aig_ObjFaninC0(pFanout)? "\'" : " "), 
-                    Aig_ObjFanin1(pFanout)->Id, (Aig_ObjFaninC1(pFanout)? "\'" : " ") );
-            printf( "\n" );
-        }
-        return;
-    }
-    if ( fHaig )
-    {
-        if ( pObj->pHaig == NULL )
-            printf( " HAIG node not given" );
-        else
-            printf( " HAIG node = %d%s", Aig_Regular(pObj->pHaig)->Id, (Aig_IsComplement(pObj->pHaig)? "\'" : " ") );
-        return;
-    }
-    // there are choices
-    if ( p->pEquivs && p->pEquivs[pObj->Id] )
-    {
-        // print equivalence class
-        printf( "  { %4d ", pObj->Id );
-        for ( pTemp = p->pEquivs[pObj->Id]; pTemp; pTemp = p->pEquivs[pTemp->Id] )
-            printf( " %4d%s", pTemp->Id, (pTemp->fPhase != pObj->fPhase)? "\'" : " " );
-        printf( " }" );
-        return;
-    }
-    // this is a secondary node
-    if ( p->pReprs && p->pReprs[pObj->Id] )
-        printf( "  class of %d", pObj->Id );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index cec92c11..392de03e 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -1323,7 +1323,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
     // create the equivalent nodes lists
     Aig_ManMarkValidChoices( pAig );
     // reconstruct the network
-    pAig = Aig_ManDupDfsOrder( pTemp = pAig, Vec_PtrEntry(vAigs,0) );
+    pAig = Aig_ManDupDfsGuided( pTemp = pAig, Vec_PtrEntry(vAigs,0) );
     Aig_ManStop( pTemp );
     // duplicate the timing manager
     pTemp = Vec_PtrEntry( vAigs, 0 );
@@ -1566,7 +1566,7 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
     // create the equivalent nodes lists
     Aig_ManMarkValidChoices( pNew );
     // reconstruct the network
-    pNew = Aig_ManDupDfsOrder( pTemp = pNew, Vec_PtrEntry( vAigs, 0 ) );
+    pNew = Aig_ManDupDfsGuided( pTemp = pNew, Vec_PtrEntry( vAigs, 0 ) );
     Aig_ManStop( pTemp );
     // duplicate the timing manager
     pTemp = Vec_PtrEntry( vAigs, 0 );
diff --git a/src/aig/aig/aigScl.c b/src/aig/aig/aigScl.c
index c2d08350..1474fcd5 100644
--- a/src/aig/aig/aigScl.c
+++ b/src/aig/aig/aigScl.c
@@ -103,7 +103,7 @@ Aig_Man_t * Aig_ManRemap( Aig_Man_t * p, Vec_Ptr_t * vMap )
     assert( Aig_ManNodeNum(p) >= Aig_ManNodeNum(pNew) );
     // check the resulting network
     if ( !Aig_ManCheck(pNew) )
-        printf( "Aig_ManDup(): The check has failed.\n" );
+        printf( "Aig_ManRemap(): The check has failed.\n" );
     return pNew;
 }
 
@@ -598,7 +598,7 @@ Aig_Man_t * Aig_ManScl( Aig_Man_t * pAig, int fLatchConst, int fLatchEqual, int
     // store the original AIG
     assert( pAig->vFlopNums == NULL );
     pAigInit = pAig;
-    pAig = Aig_ManDup( pAig );
+    pAig = Aig_ManDupSimple( pAig );
     // create storage for latch numbers
     pAig->vFlopNums = Vec_IntStartNatural( pAig->nRegs );
     pAig->vFlopReprs = Vec_IntAlloc( 100 );
diff --git a/src/aig/aig/aigTable.c b/src/aig/aig/aigTable.c
index 9cfbf5f2..68efbba6 100644
--- a/src/aig/aig/aigTable.c
+++ b/src/aig/aig/aigTable.c
@@ -68,6 +68,7 @@ void Aig_TableResize( Aig_Man_t * p )
     Aig_Obj_t * pEntry, * pNext;
     Aig_Obj_t ** pTableOld, ** ppPlace;
     int nTableSizeOld, Counter, i, clk;
+    assert( p->pTable != NULL );
 clk = clock();
     // save the old table
     pTableOld = p->pTable;
@@ -115,7 +116,7 @@ Aig_Obj_t * Aig_TableLookup( Aig_Man_t * p, Aig_Obj_t * pGhost )
     assert( Aig_ObjIsNode(pGhost) );
     assert( Aig_ObjChild0(pGhost) && Aig_ObjChild1(pGhost) );
     assert( Aig_ObjFanin0(pGhost)->Id < Aig_ObjFanin1(pGhost)->Id );
-    if ( !Aig_ObjRefs(Aig_ObjFanin0(pGhost)) || !Aig_ObjRefs(Aig_ObjFanin1(pGhost)) )
+    if ( p->pTable == NULL || !Aig_ObjRefs(Aig_ObjFanin0(pGhost)) || !Aig_ObjRefs(Aig_ObjFanin1(pGhost)) )
         return NULL;
     for ( pEntry = p->pTable[Aig_Hash(pGhost, p->nTableSize)]; pEntry; pEntry = pEntry->pNext )
     {
diff --git a/src/aig/cnf/cnfWrite.c b/src/aig/cnf/cnfWrite.c
index 5556ac2e..3656aae3 100644
--- a/src/aig/cnf/cnfWrite.c
+++ b/src/aig/cnf/cnfWrite.c
@@ -333,7 +333,7 @@ Cnf_Dat_t * Cnf_ManWriteCnf( Cnf_Man_t * p, Vec_Ptr_t * vMapped, int nOutputs )
 
   Synopsis    [Derives a simple CNF for the AIG.]
 
-  Description [The last argument shows the number of last outputs
+  Description [The last argument lists the number of last outputs
   of the manager, which will not be converted into clauses. 
   New variables will be introduced for these outputs.]
                
diff --git a/src/aig/dar/darBalance.c b/src/aig/dar/darBalance.c
index 6dd308f9..49ca963b 100644
--- a/src/aig/dar/darBalance.c
+++ b/src/aig/dar/darBalance.c
@@ -353,7 +353,18 @@ Aig_Obj_t * Dar_Balance_rec( Aig_Man_t * pNew, Aig_Obj_t * pObjOld, Vec_Vec_t *
     // make sure the balanced node is not assigned
 //    assert( pObjOld->Level >= Aig_Regular(pObjNew)->Level );
     assert( pObjOld->pData == NULL );
-    Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
+    if ( pNew->pManHaig != NULL )
+    {
+        Aig_Obj_t * pObjNewR = Aig_Regular(pObjNew);
+//        printf( "Balancing HAIG node %d equivalent to HAIG node %d (over = %d).\n", 
+//            pObjNewR->pHaig->Id, pObjOld->pHaig->Id, pObjNewR->pHaig->pHaig != NULL );
+        assert( pObjNewR->pHaig != NULL );
+//        assert( pObjNewR->pHaig->pHaig == NULL );
+        assert( !Aig_IsComplement(pObjNewR->pHaig) );
+        pObjNewR->pHaig->pHaig = pObjOld->pHaig;
+    }
+    else
+        Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
     return pObjOld->pData = pObjNew;
 }
 
@@ -383,6 +394,12 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
     pNew->nAsserts = p->nAsserts;
     if ( p->vFlopNums )
         pNew->vFlopNums = Vec_IntDup( p->vFlopNums );
+    // pass the HAIG manager
+    if ( p->pManHaig != NULL )
+    {
+        pNew->pManHaig = p->pManHaig;  p->pManHaig = NULL;
+        Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(pNew->pManHaig);
+    }
     // map the PI nodes
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
@@ -401,6 +418,7 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
                 // copy the PI
                 pObjNew = Aig_ObjCreatePi(pNew); 
                 pObj->pData = pObjNew;
+                pObjNew->pHaig = pObj->pHaig;
                 // set the arrival time of the new PI
                 arrTime = Tim_ManGetCiArrival( p->pManTime, Aig_ObjPioNum(pObj) );
                 pObjNew->Level = (int)arrTime;
@@ -411,10 +429,12 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
                 pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
                 pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
                 pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
-                Aig_ObjCreatePo( pNew, pObjNew );
                 // save arrival time of the output
                 arrTime = (float)Aig_Regular(pObjNew)->Level;
                 Tim_ManSetCoArrival( p->pManTime, Aig_ObjPioNum(pObj), arrTime );
+                // create PO
+                pObjNew = Aig_ObjCreatePo( pNew, pObjNew );
+                pObjNew->pHaig = pObj->pHaig;
             }
             else
                 assert( 0 );
@@ -429,13 +449,15 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
             pObjNew = Aig_ObjCreatePi(pNew); 
             pObjNew->Level = pObj->Level;
             pObj->pData = pObjNew;
+            pObjNew->pHaig = pObj->pHaig;
         }
         Aig_ManForEachPo( p, pObj, i )
         {
             pDriver = Aig_ObjReal_rec( Aig_ObjChild0(pObj) );
             pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
             pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
-            Aig_ObjCreatePo( pNew, pObjNew );
+            pObjNew = Aig_ObjCreatePo( pNew, pObjNew );
+            pObjNew->pHaig = pObj->pHaig;
         }
     }
     Vec_VecFree( vStore );
diff --git a/src/aig/dar/darCore.c b/src/aig/dar/darCore.c
index b13c7313..e82cce22 100644
--- a/src/aig/dar/darCore.c
+++ b/src/aig/dar/darCore.c
@@ -133,7 +133,7 @@ p->timeCuts += clock() - clk;
             // remove the old cuts
             Dar_ObjSetCuts( pObj, NULL );
             // replace the node
-            Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
+            Aig_ObjReplace( pAig, pObj, pObjNew, p->pPars->fUpdateLevel );
             continue;
         }
 
@@ -156,7 +156,7 @@ p->timeCuts += clock() - clk;
         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 );
+        Aig_ObjReplace( pAig, pObj, pObjNew, p->pPars->fUpdateLevel );
         // compare the gains
         nNodeAfter = Aig_ManNodeNum( pAig );
         assert( p->GainBest <= nNodeBefore - nNodeAfter );
diff --git a/src/aig/dar/darRefact.c b/src/aig/dar/darRefact.c
index 09b9b3a4..d19d48e4 100644
--- a/src/aig/dar/darRefact.c
+++ b/src/aig/dar/darRefact.c
@@ -582,7 +582,7 @@ p->timeEval += clock() - clk;
         pObjNew = Dar_RefactBuildGraph( pAig, p->vLeavesBest, p->pGraphBest );
         assert( (int)Aig_Regular(pObjNew)->Level <= Required );
         // replace the node
-        Aig_ObjReplace( pAig, pObj, pObjNew, 1, p->pPars->fUpdateLevel );
+        Aig_ObjReplace( pAig, pObj, pObjNew, p->pPars->fUpdateLevel );
         // compare the gains
         nNodeAfter = Aig_ManNodeNum( pAig );
         assert( p->GainBest <= nNodeBefore - nNodeAfter );
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 3be0e3f6..df92792a 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -105,9 +105,9 @@ static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * p
     // set the new node
     Fra_ObjSetFraig( pObj, iFrame, pObjNew2 );
     // add the constraint
-    pMiter = Aig_Exor( pManFraig, Aig_Regular(pObjNew), Aig_Regular(pObjReprNew) );
-    pMiter = Aig_NotCond( pMiter, Aig_Regular(pMiter)->fPhase ^ Aig_IsComplement(pMiter) );
-    pMiter = Aig_Not( pMiter );
+    pMiter = Aig_Exor( pManFraig, pObjNew, pObjReprNew );
+    pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
+    assert( Aig_ObjPhaseReal(pMiter) == 1 );
     Aig_ObjCreatePo( pManFraig, pMiter );
 }
 
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index b8f93f57..ec6b7795 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -82,7 +82,7 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec )
     float TimeLeft = 0.0;
 
     // try the miter before solving
-    pNew = Aig_ManDup( p );
+    pNew = Aig_ManDupSimple( p );
     RetValue = Fra_FraigMiterStatus( pNew );
     if ( RetValue >= 0 )
         goto finish;
@@ -144,7 +144,7 @@ clk = clock();
 PRT( "Time", clock() - clk );
     }
     }
-    
+     
     // run latch correspondence
 clk = clock();
     if ( pNew->nRegs )
@@ -165,22 +165,27 @@ clk = clock();
         }
     }
     pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 1000, 1, pParSec->fVeryVerbose, &nIter, TimeLeft );
+    p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
+    Aig_ManStop( pTemp );
     if ( pNew == NULL )
     {
+        if ( p->pSeqModel )
+        {
+            RetValue = 0;
+            printf( "Networks are NOT EQUIVALENT after simulation.   " );
+PRT( "Time", clock() - clkTotal );
+            if ( pParSec->fReportSolution && !pParSec->fRecursive )
+            {
+            printf( "SOLUTION: FAIL       " );
+PRT( "Time", clock() - clkTotal );
+            }
+            return RetValue;
+        }
         pNew = pTemp;
         RetValue = -1;
         TimeOut = 1;
         goto finish;
     }
-    p->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
-    Aig_ManStop( pTemp );
-    if ( pNew == NULL )
-    {
-        RetValue = 0;
-        printf( "Networks are NOT EQUIVALENT after simulation.   " );
-PRT( "Time", clock() - clkTotal );
-        return RetValue;
-    }
 
     if ( pParSec->fVerbose )
     {
@@ -354,6 +359,11 @@ PRT( "Time", clock() - clk );
             RetValue = 0;
             printf( "Networks are NOT EQUIVALENT after simulation.   " );
 PRT( "Time", clock() - clkTotal );
+            if ( pParSec->fReportSolution && !pParSec->fRecursive )
+            {
+            printf( "SOLUTION: FAIL       " );
+PRT( "Time", clock() - clkTotal );
+            }
             return RetValue;
         }
         Fra_SmlStop( pSml );
diff --git a/src/aig/fra/fraSec80516.zip b/src/aig/fra/fraSec80516.zip
new file mode 100644
index 00000000..0adf10df
--- /dev/null
+++ b/src/aig/fra/fraSec80516.zip
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index b14dd5bd..a8de5e37 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -994,7 +994,7 @@ Fra_Cex_t * Fra_SmlGetCounterExample( Fra_Sml_t * p )
     }
     return pCex;
 }
-
+ 
 /**Function*************************************************************
 
   Synopsis    [Generates seq counter-example from the combinational one.]
diff --git a/src/aig/ntl/ntlMap.c b/src/aig/ntl/ntlMap.c
index faae32d2..c6e80e75 100644
--- a/src/aig/ntl/ntlMap.c
+++ b/src/aig/ntl/ntlMap.c
@@ -129,7 +129,7 @@ void Ntl_ManSetIfParsDefault( If_Par_t * pPars )
     pPars->nFlowIters  =  1;
     pPars->nAreaIters  =  2;
     pPars->DelayTarget = -1;
-    pPars->Epsilon     =  (float)0.001;
+    pPars->Epsilon     =  (float)0.005;
     pPars->fPreprocess =  1;
     pPars->fArea       =  0;
     pPars->fFancy      =  0;
diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h
index 6c78ca87..f74f44f3 100644
--- a/src/aig/nwk/nwk.h
+++ b/src/aig/nwk/nwk.h
@@ -29,8 +29,6 @@ extern "C" {
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#pragma warning( disable : 4273 )
-
 #include "aig.h"
 #include "hop.h"
 #include "tim.h"
@@ -119,6 +117,9 @@ struct Nwk_Obj_t_
 ////////////////////////////////////////////////////////////////////////
 ///                      INLINED FUNCTIONS                           ///
 ////////////////////////////////////////////////////////////////////////
+
+//#pragma warning( disable : 4273 )
+
 #ifdef WIN32
 #define DLLEXPORT __declspec(dllexport)
 #define DLLIMPORT __declspec(dllimport)
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index ea122bbf..50d6db49 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -1,5 +1,6 @@
 SRC +=    src/aig/saig/saigBmc.c \
     src/aig/saig/saigCone.c \
+    src/aig/saig/saigHaig.c \
     src/aig/saig/saigInter.c \
     src/aig/saig/saigIoa.c \
     src/aig/saig/saigPhase.c \
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index c8efab40..8ec680b8 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -79,6 +79,8 @@ static inline int          Saig_ObjIsLi( Aig_Man_t * p, Aig_Obj_t * pObj )    {
 extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame );
 /*=== saigCone.c ==========================================================*/
 extern void              Saig_ManPrintCones( Aig_Man_t * p );
+/*=== saigHaig.c ==========================================================*/
+extern void              Saig_ManHaigRecord( Aig_Man_t * p );
 /*=== saigIoa.c ==========================================================*/
 extern void              Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
 extern Aig_Man_t *       Saig_ManReadBlif( char * pFileName );
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index 952094ce..2d5af2d3 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -145,11 +145,11 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax
         {
             pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
             Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) );
-            if ( Counter >= nSizeMax )
-            {
-                Aig_ManCleanup( pFrames );
-                return pFrames;
-            }
+        }
+        if ( Counter >= nSizeMax )
+        {
+            Aig_ManCleanup( pFrames );
+            return pFrames;
         }
         if ( f == nFrames - 1 )
             break;
@@ -201,6 +201,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
             nFrames, Aig_ManPiNum(pFrames), Aig_ManPoNum(pFrames), 
             Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
         PRT( "Time", clock() - clk );
+        fflush( stdout );
     }
     // rewrite the timeframes
     if ( fRewrite )
@@ -214,6 +215,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
             printf( "Time-frames after rewriting:  Node = %6d. Lev = %5d.  ", 
                 Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
             PRT( "Time", clock() - clk );
+            fflush( stdout );
         }
     }
     // create the SAT solver
@@ -230,15 +232,20 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
     {
         printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
         PRT( "Time", clock() - clk );
+        fflush( stdout );
     }
     status = sat_solver_simplify(pSat);
     if ( status == 0 )
     {
         if ( fVerbose )
+        {
             printf( "The BMC problem is trivially UNSAT\n" );
+            fflush( stdout );
+        }
     }
     else
     {
+        int clkPart = clock();
         Aig_ManForEachPo( pFrames, pObj, i )
         {
             Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
@@ -247,12 +254,14 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
                     i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
             clk = clock();
             status = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
-            if ( fVerbose )
+            if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) )
             {
-                printf( "Solved  output %2d of frame %3d.  ", 
-                    i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
+                printf( "Solved %2d outputs of frame %3d.  ", 
+                    Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
                 printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations );
-                PRT( "Time", clock() - clk );
+                PRT( "Time", clock() - clkPart );
+                clkPart = clock();
+                fflush( stdout );
             }
             if ( status == l_False )
             {
@@ -272,7 +281,7 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
             }
             else
             {
-                *piFrame = i;
+                *piFrame = i / Saig_ManPoNum(pAig);
                 RetValue = -1;
                 break;
             }
diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c
new file mode 100644
index 00000000..64f4e943
--- /dev/null
+++ b/src/aig/saig/saigHaig.c
@@ -0,0 +1,472 @@
+/**CFile****************************************************************
+
+  FileName    [saigHaig.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Experiments with history AIG recording.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - April 28, 2007.]
+
+  Revision    [$Id: saigHaig.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+#include "satSolver.h"
+#include "cnf.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the inductive case with speculative reduction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManHaigSpeculate( Aig_Man_t * pFrames, Aig_Obj_t * pObj )
+{
+    Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
+    // skip nodes without representative
+    pObjRepr = pObj->pHaig;
+    if ( pObjRepr == NULL )
+        return;
+    assert( pObjRepr->Id < pObj->Id );
+    // get the new node 
+    pObjNew = pObj->pData;
+    // get the new node of the representative
+    pObjReprNew = pObjRepr->pData;
+    // if this is the same node, no need to add constraints
+    if ( Aig_Regular(pObjNew) == Aig_Regular(pObjReprNew) )
+        return;
+    // these are different nodes - perform speculative reduction
+    pObjNew2 = Aig_NotCond( pObjReprNew, pObj->fPhase ^ pObjRepr->fPhase );
+    // set the new node
+    pObj->pData = pObjNew2;
+    // add the constraint
+    pMiter = Aig_Exor( pFrames, pObjNew, pObjReprNew );
+    pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
+    assert( Aig_ObjPhaseReal(pMiter) == 1 );
+    Aig_ObjCreatePo( pFrames, pMiter );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prepares the inductive case with speculative reduction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManHaigFrames( Aig_Man_t * pHaig, int nFrames )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, f, nAssumptions = 0;
+    assert( nFrames == 1 || nFrames == 2 );
+    assert( nFrames == 1 || Saig_ManRegNum(pHaig) > 0 );
+    // start AIG manager for timeframes
+    pFrames = Aig_ManStart( Aig_ManNodeNum(pHaig) * nFrames );
+    pFrames->pName = Aig_UtilStrsav( pHaig->pName );
+    pFrames->pSpec = Aig_UtilStrsav( pHaig->pSpec );
+    // map the constant node
+    Aig_ManConst1(pHaig)->pData = Aig_ManConst1( pFrames );
+    // create variables for register outputs
+    Saig_ManForEachLo( pHaig, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pFrames );
+    // add timeframes
+    Aig_ManSetPioNumbers( pHaig );
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Aig_ManForEachObj( pHaig, pObj, i )
+        {
+            if ( Aig_ObjIsConst1(pObj) || Aig_ObjIsPo(pObj) )
+                continue;
+            if ( Saig_ObjIsPi(pHaig, pObj) )
+            {
+                pObj->pData = Aig_ObjCreatePi( pFrames );
+                continue;
+            }
+            if ( Saig_ObjIsLo(pHaig, pObj) )
+            {
+                Aig_ManHaigSpeculate( pFrames, pObj );
+                continue;
+            }
+            if ( Aig_ObjIsNode(pObj) )
+            {
+                pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+                Aig_ManHaigSpeculate( pFrames, pObj );
+                continue;
+            }
+            assert( 0 );
+        }
+        if ( f == nFrames - 2 )
+            nAssumptions = Aig_ManPoNum(pFrames);
+        if ( f == nFrames - 1 )
+            break;
+        // save register inputs
+        Saig_ManForEachLi( pHaig, pObj, i )
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+        // transfer to register outputs
+        Saig_ManForEachLiLo(  pHaig, pObjLi, pObjLo, i )
+            pObjLo->pData = pObjLi->pData;
+    }
+    Aig_ManCleanup( pFrames );
+    pFrames->nAsserts = Aig_ManPoNum(pFrames) - nAssumptions;
+    Aig_ManSetRegNum( pFrames, 0 );
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManHaigVerify2( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
+{
+    int nBTLimit = 0;
+    Aig_Man_t * pFrames;
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    Aig_Obj_t * pObj;
+    int i, Lit, RetValue, Counter;
+    int clk = clock();
+
+    // create time frames with speculative reduction and convert them into CNF
+clk = clock();
+    pFrames = Aig_ManHaigFrames( pHaig, nFrames );
+Aig_ManShow( pFrames, 0, NULL ); 
+
+    printf( "AIG:    " );
+    Aig_ManPrintStats( pAig );
+    printf( "HAIG:   " );
+    Aig_ManPrintStats( pHaig );
+    printf( "Frames: " );
+    Aig_ManPrintStats( pFrames );
+    printf( "Additional frames stats: Assumptions = %d. Asserts = %d.\n", 
+        Aig_ManPoNum(pFrames) - pFrames->nAsserts, pFrames->nAsserts );
+    pCnf = Cnf_DeriveSimple( pFrames, pFrames->nAsserts );
+PRT( "Preparation", clock() - clk );
+
+//    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) - pFrames->nAsserts );
+//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
+    Saig_ManDumpBlif( pHaig, "haig_temp.blif" );
+    Saig_ManDumpBlif( pFrames, "haig_temp_frames.blif" );
+    // create the SAT solver to be used for this problem
+    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    if ( pSat == NULL )
+    {
+        printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
+        return -1;
+    }
+    
+    // solve each output
+clk = clock();
+    if ( pFrames->nAsserts == 0 )
+    {
+        RetValue = sat_solver_solve( pSat, NULL, NULL, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+        if ( RetValue != l_False )
+            printf( "SAT solver is wrong\n" );
+    }
+    else
+    {
+        Counter = 0;
+        Aig_ManForEachPo( pFrames, pObj, i )
+        {
+            if ( i < Aig_ManPoNum(pFrames) - pFrames->nAsserts )
+                continue;
+            Lit = toLitCond( pCnf->pVarNums[pObj->Id], 1 );
+            RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            if ( RetValue != l_False )
+                Counter++;
+        }
+PRT( "Solving    ", clock() - clk );
+        if ( Counter )
+            printf( "Verification failed for %d classes.\n", Counter );
+        else
+            printf( "Verification is successful.\n" );
+    }
+
+    // clean up
+    Aig_ManStop( pFrames );
+    Cnf_DataFree( pCnf );
+    sat_solver_delete( pSat );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManHaigVerify( Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
+{
+    int nBTLimit = 0;
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    Aig_Obj_t * pObj, * pRepr;
+    int i, RetValue, Counter, Lits[2];
+    int nClasses = 0;
+    int clk = clock();
+
+    assert( nFrames == 1 || nFrames == 2 );
+
+clk = clock();
+    pCnf = Cnf_DeriveSimple( pHaig, Aig_ManPoNum(pHaig) );
+    // create the SAT solver to be used for this problem
+    pSat = Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 );
+    if ( pSat == NULL )
+    {
+        printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
+        return -1;
+    }
+
+    if ( nFrames == 2 )
+    {
+        // add clauses for the first frame
+        Aig_ManForEachObj( pHaig, pObj, i )
+        {
+            pRepr = pObj->pHaig;
+            if ( pRepr == NULL )
+                continue;
+            if ( pRepr->fPhase ^ pObj->fPhase )
+            {
+                Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+                Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 0 );
+                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+                {
+                    sat_solver_delete( pSat );
+                    return 0;
+                }
+                Lits[0]++;
+                Lits[1]++;
+                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+                {
+                    sat_solver_delete( pSat );
+                    return 0;
+                }
+            }
+            else
+            {
+                Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+                Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 1 );
+                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+                {
+                    sat_solver_delete( pSat );
+                    return 0;
+                }
+                Lits[0]++;
+                Lits[1]--;
+                if ( !sat_solver_addclause( pSat, Lits, Lits + 2 ) )
+                {
+                    sat_solver_delete( pSat );
+                    return 0;
+                }
+            }
+        }
+
+        // add clauses for the next timeframe
+        { 
+            int nLitsAll = 2 * pCnf->nVars;
+            int * pLits = pCnf->pClauses[0];
+            for ( i = 0; i < pCnf->nLiterals; i++ )
+                pLits[i] += nLitsAll;
+        }
+    }
+PRT( "Preparation", clock() - clk );
+
+
+    // check in the second timeframe
+clk = clock();
+    Counter = 0;
+    nClasses = 0;
+    Aig_ManForEachObj( pHaig, pObj, i )
+    {
+        pRepr = pObj->pHaig;
+        if ( pRepr == NULL )
+            continue;
+        nClasses++;
+        if ( pRepr->fPhase ^ pObj->fPhase )
+        {
+            Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+            Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 0 );
+
+            RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            if ( RetValue != l_False )
+                Counter++;
+
+            Lits[0]++;
+            Lits[1]++;
+
+            RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            if ( RetValue != l_False )
+                Counter++;
+        }
+        else
+        {
+            Lits[0] = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+            Lits[1] = toLitCond( pCnf->pVarNums[pRepr->Id], 1 );
+
+            RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            if ( RetValue != l_False )
+                Counter++;
+
+            Lits[0]++;
+            Lits[1]--;
+
+            RetValue = sat_solver_solve( pSat, Lits, Lits + 2, (sint64)nBTLimit, (sint64)0, (sint64)0, (sint64)0 );
+            if ( RetValue != l_False )
+                Counter++;
+        }
+    }
+PRT( "Solving    ", clock() - clk );
+    if ( Counter )
+        printf( "Verification failed for %d out of %d classes.\n", Counter, nClasses );
+    else
+        printf( "Verification is successful for all %d classes.\n", nClasses );
+
+    Cnf_DataFree( pCnf );
+    sat_solver_delete( pSat );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_ManHaigRecord( Aig_Man_t * p )
+{
+    extern void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward );
+    int fUseRetiming = (int)( Aig_ManRegNum(p) > 0 );
+    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
+    Aig_Man_t * pNew, * pTemp;
+    Aig_Obj_t * pObj;
+    int i;
+    Dar_ManDefaultRwrParams( pParsRwr );
+    // duplicate this manager
+    pNew = Aig_ManDupSimple( p );
+
+    // create its history AIG
+    pNew->pManHaig = Aig_ManDupSimple( pNew );
+    Aig_ManForEachObj( pNew, pObj, i )
+        pObj->pHaig = pObj->pData;
+    // remove structural hashing table
+    Aig_TableClear( pNew->pManHaig );
+
+    // perform retiming
+    if ( fUseRetiming )
+    {
+/*
+        // perform balancing
+        pNew = Dar_ManBalance( pTemp = pNew, 0 );
+        assert( pNew->pManHaig != NULL );
+        assert( pTemp->pManHaig == NULL );
+        Aig_ManStop( pTemp );
+
+        // perform rewriting
+        Dar_ManRewrite( pNew, pParsRwr );
+        pNew = Aig_ManDupDfs( pTemp = pNew ); 
+        assert( pNew->pManHaig != NULL );
+        assert( pTemp->pManHaig == NULL );
+        Aig_ManStop( pTemp );
+*/
+        // perform retiming
+        Saig_ManRetimeSteps( pNew, 1000, 1 ); 
+        pNew = Aig_ManDupSimpleDfs( pTemp = pNew ); 
+        assert( pNew->pManHaig != NULL );
+        assert( pTemp->pManHaig == NULL );
+        Aig_ManStop( pTemp );
+
+        // perform balancing
+        pNew = Dar_ManBalance( pTemp = pNew, 0 );
+        assert( pNew->pManHaig != NULL );
+        assert( pTemp->pManHaig == NULL );
+        Aig_ManStop( pTemp );
+
+        // perform rewriting
+        Dar_ManRewrite( pNew, pParsRwr );
+        pNew = Aig_ManDupDfs( pTemp = pNew ); 
+        assert( pNew->pManHaig != NULL );
+        assert( pTemp->pManHaig == NULL );
+        Aig_ManStop( pTemp );
+    }
+    else
+    {
+        // perform balancing
+        pNew = Dar_ManBalance( pTemp = pNew, 0 );
+        assert( pNew->pManHaig != NULL );
+        assert( pTemp->pManHaig == NULL );
+        Aig_ManStop( pTemp );
+/*
+        // perform rewriting
+        Dar_ManRewrite( pNew, pParsRwr );
+        pNew = Aig_ManDupDfs( pTemp = pNew ); 
+        assert( pNew->pManHaig != NULL );
+        assert( pTemp->pManHaig == NULL );
+        Aig_ManStop( pTemp );
+*/
+    } 
+
+    // use the haig for verification
+    Aig_ManAntiCleanup( pNew->pManHaig );
+    Aig_ManSetRegNum( pNew->pManHaig, pNew->pManHaig->nRegs );
+//Aig_ManShow( pNew->pManHaig, 0, NULL ); 
+
+    printf( "AIG:    " );
+    Aig_ManPrintStats( pNew );
+    printf( "HAIG:   " );
+    Aig_ManPrintStats( pNew->pManHaig );
+
+    if ( !Aig_ManHaigVerify( pNew, pNew->pManHaig, 1+fUseRetiming ) )
+        printf( "Constructing SAT solver has failed.\n" );         
+
+    // cleanup
+    Aig_ManStop( pNew->pManHaig );
+    pNew->pManHaig = NULL;
+    Aig_ManStop( pNew );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c
index f19a27b6..323a230f 100644
--- a/src/aig/saig/saigPhase.c
+++ b/src/aig/saig/saigPhase.c
@@ -885,7 +885,7 @@ Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose )
         pNew = Saig_ManPerformAbstraction( pTsi, nFrames, fVerbose );
     Saig_TsiStop( pTsi );
     if ( pNew == NULL )
-        pNew = Aig_ManDup( p );
+        pNew = Aig_ManDupSimple( p );
     return pNew;
 }
 
diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c
index 3935db6c..0ad6c314 100644
--- a/src/aig/saig/saigRetMin.c
+++ b/src/aig/saig/saigRetMin.c
@@ -622,7 +622,7 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl
     Vec_Ptr_t * vCut;
     Aig_Man_t * pNew, * pTemp, * pCopy;
     int i, fChanges;
-    pNew = Aig_ManDup( p );
+    pNew = Aig_ManDupSimple( p );
     // perform several iterations of forward retiming
     fChanges = 0;
     if ( !fBackwardOnly )
@@ -672,7 +672,7 @@ Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnl
     {
         if ( Saig_ManRegNum(pNew) == 0 )
             break;
-        pCopy = Aig_ManDup( pNew );
+        pCopy = Aig_ManDupSimple( pNew );
         pTemp = Saig_ManRetimeMinAreaBackward( pCopy, fVerbose );
         Aig_ManStop( pCopy );
         if ( pTemp == NULL )
diff --git a/src/aig/saig/saigRetStep.c b/src/aig/saig/saigRetStep.c
index e7ec3c08..f7c27a93 100644
--- a/src/aig/saig/saigRetStep.c
+++ b/src/aig/saig/saigRetStep.c
@@ -44,6 +44,7 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj )
     Aig_Obj_t * pFanin0, * pFanin1;
     Aig_Obj_t * pInput0, * pInput1;
     Aig_Obj_t * pObjNew, * pObjLi, * pObjLo;
+    int fCompl;
 
     assert( Saig_ManRegNum(p) > 0 );
     assert( Aig_ObjIsNode(pObj) );
@@ -68,22 +69,26 @@ Aig_Obj_t * Saig_ManRetimeNodeFwd( Aig_Man_t * p, Aig_Obj_t * pObj )
     pInput1 = Aig_ObjChild0( pInput1 );
     pInput0 = Aig_NotCond( pInput0, Aig_ObjFaninC0(pObj) );
     pInput1 = Aig_NotCond( pInput1, Aig_ObjFaninC1(pObj) );
+    // get the condition when the register should be complemetned
+    fCompl = Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj);
 
     // create new node
     pObjNew = Aig_And( p, pInput0, pInput1 );
 
     // create new register input
-    pObjLi = Aig_ObjCreatePo( p, Aig_NotCond(pObjNew, pObjNew->fPhase) );
+    pObjLi = Aig_ObjCreatePo( p, Aig_NotCond(pObjNew, fCompl) );
     pObjLi->PioNum = Aig_ManPoNum(p) - 1;
-    assert( pObjLi->fPhase == 0 );
 
     // create new register output
     pObjLo = Aig_ObjCreatePi( p );
     pObjLo->PioNum = Aig_ManPiNum(p) - 1;
     p->nRegs++;
 
+//printf( "Reg = %4d. Reg = %4d. Compl = %d. Phase = %d.\n", 
+//       pFanin0->PioNum, pFanin1->PioNum, Aig_IsComplement(pObjNew), fCompl );
+
     // return register output
-    return Aig_NotCond( pObjLo, pObjNew->fPhase );
+    return Aig_NotCond( pObjLo, fCompl );
 }
 
 /**Function*************************************************************
@@ -163,6 +168,7 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
     int RetValue, s, i;
     Aig_ManSetPioNumbers( p );
     Aig_ManFanoutStart( p );
+    p->fCreatePios = 1;
     if ( fForward )
     {
         for ( s = 0; s < nSteps; s++ )
@@ -172,7 +178,7 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
                 pObjNew = Saig_ManRetimeNodeFwd( p, pObj );
                 if ( pObjNew == NULL )
                     continue;
-                Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
+                Aig_ObjReplace( p, pObj, pObjNew, 0 );
                 break;
             }
         }
@@ -186,13 +192,16 @@ void Saig_ManRetimeSteps( Aig_Man_t * p, int nSteps, int fForward )
                 pObjNew = Saig_ManRetimeNodeBwd( p, pObj );
                 if ( pObjNew == NULL )
                     continue;
-                Aig_ObjReplace( p, pObj, pObjNew, 0, 0 );
+                Aig_ObjReplace( p, pObj, pObjNew, 0 );
                 break;
             }
         }
     }
+    p->fCreatePios = 0;
+    Aig_ManFanoutStop( p );
     RetValue = Aig_ManCleanup( p );
     assert( RetValue == 0 );
+    Aig_ManSetRegNum( p, p->nRegs ); 
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 0cafa314..8f0c7210 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -29,8 +29,6 @@ extern "C" {
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#pragma warning( disable : 4273 )
-
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
@@ -226,6 +224,8 @@ struct Abc_Lib_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
+//#pragma warning( disable : 4273 )
+
 #ifdef WIN32
 #define DLLEXPORT __declspec(dllexport)
 #define DLLIMPORT __declspec(dllimport)
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 9b5ebddb..8d27c0d2 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2762,19 +2762,36 @@ usage:
 int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk;
+    Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
+    int fCleanupPis;
+    int fCleanupPos;
+    int fVerbose;
+
+    extern Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanupPos, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fCleanupPis = 1;
+    fCleanupPos = 1;
+    fVerbose    = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "iovh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'i':
+            fCleanupPis ^= 1;
+            break;
+        case 'o':
+            fCleanupPos ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -2789,16 +2806,35 @@ int Abc_CommandCleanup( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( Abc_NtkIsStrash(pNtk) )
     {
-        fprintf( pErr, "Cleanup cannot be performed on the AIG.\n" );
+        if ( !fCleanupPos && !fCleanupPos )
+        {
+            printf( "Cleanup for PIs and POs is not enabled.\n" );
+            pNtkRes = Abc_NtkDup( pNtk );
+        }
+        else
+            pNtkRes = Abc_NtkDarCleanupAig( pNtk, fCleanupPis, fCleanupPos, fVerbose );
+    }
+    else
+    {
+        Abc_NtkCleanup( pNtk, fVerbose );
+        pNtkRes = Abc_NtkDup( pNtk );
+    }
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "Cleanup has failed.\n" );
         return 1;
     }
-    // modify the current network
-    Abc_NtkCleanup( pNtk, 1 );
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: cleanup [-h]\n" );
-    fprintf( pErr, "\t        removes dangling nodes\n" );
+    fprintf( pErr, "usage: cleanup [-iovh]\n" );
+    fprintf( pErr, "\t        for logic networks, removes dangling combinatinal logic\n" );
+    fprintf( pErr, "\t        for AIGs, removes PIs w/o fanout and POs driven by const-0\n" );
+    fprintf( pErr, "\t-i    : toggles removing PIs without fanout [default = %s]\n", fCleanupPis? "yes": "no" );
+    fprintf( pErr, "\t-o    : toggles removing POs with const-0 drivers [default = %s]\n", fCleanupPos? "yes": "no" );
+    fprintf( pErr, "\t-v    : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); 
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -7469,7 +7505,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     extern Abc_Ntk_t * Abc_NtkFilter( Abc_Ntk_t * pNtk );
 //    extern Abc_Ntk_t * Abc_NtkDarRetime( Abc_Ntk_t * pNtk, int nStepsMax, int fVerbose );
 //    extern Abc_Ntk_t * Abc_NtkPcmTest( Abc_Ntk_t * pNtk, int fVerbose );
-//    extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
+    extern Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk );
 //    extern void Abc_NtkDarTestBlif( char * pFileName );
 //    extern Abc_Ntk_t * Abc_NtkDarPartition( Abc_Ntk_t * pNtk );
 //    extern Abc_Ntk_t * Abc_NtkTestExor( Abc_Ntk_t * pNtk, int fVerbose );
@@ -7661,7 +7697,10 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 */
 
 //    Abc_NtkDarPartition( pNtk );
-Abc_NtkDarTest( pNtk );
+//Abc_NtkDarTest( pNtk );
+
+
+Abc_NtkDarHaigRecord( pNtk );
 return 0;
 
     pNtkRes = Abc_NtkDarRetimeStep( pNtk, 0 );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index ca54e4e1..f369918e 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -94,16 +94,6 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters )
     pMan->fCatchExor = fExors;
 
     pMan->pName = Extra_UtilStrsav( pNtk->pName );
-    // save the number of registers
-    if ( fRegisters )
-    {
-        pMan->nRegs = Abc_NtkLatchNum(pNtk);
-        pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
-//        pMan->vFlopNums = NULL;
-//        pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk );
-        if ( pNtk->vOnehots )
-            pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
-    }
     // transfer the pointers to the basic nodes
     Abc_AigConst1(pNtk)->pCopy = (Abc_Obj_t *)Aig_ManConst1(pMan);
     Abc_NtkForEachCi( pNtk, pObj, i )
@@ -134,6 +124,16 @@ Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters )
     if ( !fExors && nNodes )
         printf( "Abc_NtkToDar(): Unexpected %d dangling nodes when converting to AIG!\n", nNodes );
 //Aig_ManDumpVerilog( pMan, "test.v" );
+    // save the number of registers
+    if ( fRegisters )
+    {
+        Aig_ManSetRegNum( pMan, Abc_NtkLatchNum(pNtk) );
+        pMan->vFlopNums = Vec_IntStartNatural( pMan->nRegs );
+//        pMan->vFlopNums = NULL;
+//        pMan->vOnehots = Abc_NtkConverLatchNamesIntoNumbers( pNtk );
+        if ( pNtk->vOnehots )
+            pMan->vOnehots = (Vec_Ptr_t *)Vec_VecDupInt( (Vec_Vec_t *)pNtk->vOnehots );
+    }
     if ( !Aig_ManCheck( pMan ) )
     {
         printf( "Abc_NtkToDar: AIG check has failed.\n" );
@@ -1220,8 +1220,6 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nBTLimit, in
         return RetValue;
     }
     assert( pMan->nRegs > 0 );
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
     // perform verification
     if ( fNewAlgo )
     {
@@ -1282,8 +1280,6 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int fRewrite, int fTra
         return -1;
     }
     assert( pMan->nRegs > 0 );
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan);
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan);
     RetValue = Saig_Interpolate( pMan, nConfLimit, fRewrite, fTransLoop, fVerbose, &Depth );
     if ( RetValue == 1 )
         printf( "Property proved.  " );
@@ -1593,9 +1589,6 @@ Abc_Ntk_t * Abc_NtkDarRetimeMostFwd( Abc_Ntk_t * pNtk, int nMaxIters, int fVerbo
         Vec_IntFree( pMan->vFlopNums ); 
     pMan->vFlopNums = NULL;
 
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
-
     pMan = Saig_ManRetimeForward( pTemp = pMan, nMaxIters, fVerbose );
     Aig_ManStop( pTemp );
 
@@ -1630,9 +1623,6 @@ Abc_Ntk_t * Abc_NtkDarRetimeMinArea( Abc_Ntk_t * pNtk, int nMaxIters, int fForwa
         Vec_IntFree( pMan->vFlopNums ); 
     pMan->vFlopNums = NULL;
 
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
-
     pMan = Saig_ManRetimeMinArea( pTemp = pMan, nMaxIters, fForwardOnly, fBackwardOnly, fInitial, fVerbose );
     Aig_ManStop( pTemp );
 
@@ -1664,11 +1654,8 @@ Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose )
         Vec_IntFree( pMan->vFlopNums ); 
     pMan->vFlopNums = NULL;
 
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
-
     Aig_ManPrintStats(pMan);
-    Saig_ManRetimeSteps( pMan, 1, 0 );
+    Saig_ManRetimeSteps( pMan, 1000, 1 );
     Aig_ManPrintStats(pMan);
 
     pNtkAig = Abc_NtkFromDarSeqSweep( pNtk, pMan );
@@ -1689,18 +1676,16 @@ Abc_Ntk_t * Abc_NtkDarRetimeStep( Abc_Ntk_t * pNtk, int fVerbose )
 ***********************************************************************/
 void Abc_NtkDarHaigRecord( Abc_Ntk_t * pNtk )
 {
-/*
     Aig_Man_t * pMan;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return;
-//    Aig_ManReduceLachesCount( pMan );
     if ( pMan->vFlopNums )
         Vec_IntFree( pMan->vFlopNums ); 
     pMan->vFlopNums = NULL;
-    Aig_ManHaigRecord( pMan );
+
+    Saig_ManHaigRecord( pMan );
     Aig_ManStop( pMan );
-*/
 }
 
 /**Function*************************************************************
@@ -2006,8 +1991,6 @@ void Abc_NtkDarPrintCone( Abc_Ntk_t * pNtk )
     if ( pMan == NULL )
         return;
     assert( Aig_ManRegNum(pMan) > 0 );
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
     Saig_ManPrintCones( pMan );
     Aig_ManStop( pMan );
 }
@@ -2063,10 +2046,7 @@ Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, in
     Vec_Int_t * vInits;
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk, 0, 0 );
-    pMan->nRegs = Abc_NtkLatchNum(pNtk);
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return NULL;
     vInits = Abc_NtkGetLatchValues(pNtk);
@@ -2097,10 +2077,7 @@ Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fI
 {
     Abc_Ntk_t * pNtkAig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk, 0, 0 );
-    pMan->nRegs = Abc_NtkLatchNum(pNtk);
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return NULL;
     pMan = Saig_ManTimeframeSimplify( pTemp = pMan, nPrefix, nFrames, fInit, fVerbose );
@@ -2116,6 +2093,43 @@ Abc_Ntk_t * Abc_NtkDarFrames( Abc_Ntk_t * pNtk, int nPrefix, int nFrames, int fI
 
 /**Function*************************************************************
 
+  Synopsis    [Performs phase abstraction.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanupPos, int fVerbose )
+{
+    Abc_Ntk_t * pNtkAig;
+    Aig_Man_t * pMan;
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+        return NULL;
+    if ( fCleanupPis )
+    {
+        int Temp = Aig_ManPiCleanup( pMan );
+        if ( fVerbose )
+            printf( "Cleanup removed %d primary inputs without fanout.\n", Temp );                                                                     
+    }
+    if ( fCleanupPos )
+    {
+        int Temp = Aig_ManPoCleanup( pMan );
+        if ( fVerbose )
+            printf( "Cleanup removed %d primary outputs driven by const-0.\n", Temp );                                                                     
+    }
+    pNtkAig = Abc_NtkFromAigPhase( pMan );
+    pNtkAig->pName = Extra_UtilStrsav(pNtk->pName);
+    pNtkAig->pSpec = Extra_UtilStrsav(pNtk->pSpec);
+    Aig_ManStop( pMan );
+    return pNtkAig;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs BDD-based reachability analysis.]
 
   Description []
@@ -2129,10 +2143,7 @@ void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartitio
 {
     extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
     Aig_Man_t * pMan;
-    pMan = Abc_NtkToDar( pNtk, 0, 0 );
-    pMan->nRegs = Abc_NtkLatchNum(pNtk);
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return;
     Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
@@ -2156,9 +2167,6 @@ void Abc_NtkDarTest( Abc_Ntk_t * pNtk )
     Aig_Man_t * pMan;
     assert( Abc_NtkIsStrash(pNtk) );
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
-    pMan->nRegs = Abc_NtkLatchNum(pNtk);
-    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
-    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
     if ( pMan == NULL )
         return;
 
diff --git a/src/base/abci/abcRec.c b/src/base/abci/abcRec.c
index a6ec6981..f74cbee8 100644
--- a/src/base/abci/abcRec.c
+++ b/src/base/abci/abcRec.c
@@ -523,6 +523,7 @@ void Abc_NtkRecAdd( Abc_Ntk_t * pNtk )
     pPars->nFlowIters  =  0;
     pPars->nAreaIters  =  0;
     pPars->DelayTarget = -1;
+    pPars->Epsilon     =  (float)0.005;
     pPars->fPreprocess =  0;
     pPars->fArea       =  1;
     pPars->fFancy      =  0;
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index 8e8e8719..f2861204 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -74,6 +74,7 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nFaninMax, int nCubeMax, int nF
     pPars->nFlowIters  =  nFlowIters;
     pPars->nAreaIters  =  nAreaIters;
     pPars->DelayTarget = -1;
+    pPars->Epsilon     =  (float)0.005;
     pPars->fPreprocess =  1;
     pPars->fArea       =  fArea;
     pPars->fFancy      =  0;
diff --git a/src/opt/lpk/lpkCore.c b/src/opt/lpk/lpkCore.c
index 80080d50..4eb64aa2 100644
--- a/src/opt/lpk/lpkCore.c
+++ b/src/opt/lpk/lpkCore.c
@@ -53,6 +53,7 @@ void Lpk_IfManStart( Lpk_Man_t * p )
     pPars->nFlowIters  =  0; // 1
     pPars->nAreaIters  =  0; // 1 
     pPars->DelayTarget = -1;
+    pPars->Epsilon     =  (float)0.005;
     pPars->fPreprocess =  0;
     pPars->fArea       =  1;
     pPars->fFancy      =  0;