Cleaing AIG manager by removing pointers to HAIG.

18 files changed, 2 insertions, 1137 deletions

diff --git a/abclib.dsp b/abclib.dsp
index 5bb5a374..69f5dc3c 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -3283,10 +3283,6 @@ SOURCE=.\src\aig\saig\saigDup.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\saig\saigHaig.c
-# End Source File
-# Begin Source File
-
 SOURCE=.\src\aig\saig\saigInd.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 3e682391..9953cf6a 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -66,7 +66,7 @@ typedef enum {
 } Aig_Type_t;
 
 // the AIG node
-struct Aig_Obj_t_  // 9 words
+struct Aig_Obj_t_  // 8 words
 {
     union {                         
         Aig_Obj_t *  pNext;          // strashing table
@@ -74,7 +74,6 @@ struct Aig_Obj_t_  // 9 words
     };
     Aig_Obj_t *      pFanin0;        // fanin
     Aig_Obj_t *      pFanin1;        // fanin
-    Aig_Obj_t *      pHaig;          // pointer to the HAIG node
     unsigned int     Type    :  3;   // object type
     unsigned int     fPhase  :  1;   // value under 000...0 pattern
     unsigned int     fMarkA  :  1;   // multipurpose mask
@@ -156,7 +155,6 @@ struct Aig_Man_t_
     Vec_Ptr_t *      vSeqModelVec;   // vector of counter-examples (for sequential miters)
     Aig_Man_t *      pManExdc;
     Vec_Ptr_t *      vOnehots;
-    Aig_Man_t *      pManHaig;
     int              fCreatePios;
     Vec_Int_t *      vEquPairs;   
     Vec_Vec_t *      vClockDoms; 
@@ -326,7 +324,6 @@ static inline Aig_Obj_t *  Aig_ObjEquiv( Aig_Man_t * p, Aig_Obj_t * pObj )    {
 static inline void         Aig_ObjSetEquiv( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pEqu ) { assert(p->pEquivs); p->pEquivs[pObj->Id] = pEqu;                  }
 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 void         Aig_ObjSetRepr( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pRepr )     { assert(p->pReprs); p->pReprs[pObj->Id] = pRepr;                                } 
-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_ObjWhatFanin( Aig_Obj_t * pObj, Aig_Obj_t * pFanin )    
 { 
     if ( Aig_ObjFanin0(pObj) == pFanin ) return 0; 
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index 9d87db92..67b71d61 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -49,7 +49,6 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
     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 = Abc_UtilStrsav( p->pName );
@@ -61,11 +60,9 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
     Aig_ManForEachCi( p, pObj, i )
     {
         pObjNew = Aig_ObjCreateCi( pNew );
-        pObjNew->pHaig = pObj->pHaig;
         pObjNew->Level = pObj->Level;
         pObj->pData = pObjNew;
     }
@@ -74,30 +71,21 @@ Aig_Man_t * Aig_ManDupSimple( Aig_Man_t * p )
         if ( Aig_ObjIsBuf(pObj) )
         {
             pObjNew = Aig_ObjChild0Copy(pObj);
-            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
             pObj->pData = pObjNew;
         }
         else if ( Aig_ObjIsNode(pObj) )
         {
             pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
             pObj->pData = pObjNew;
         }
     // add the POs
     Aig_ManForEachCo( p, pObj, i )
     {
         pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
-        pObjNew->pHaig = pObj->pHaig;
         pObj->pData = pObjNew;
     }
     assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
     Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
-    // 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" );
@@ -120,7 +108,6 @@ Aig_Man_t * Aig_ManDupSimpleWithHints( Aig_Man_t * p, Vec_Int_t * vHints )
     Aig_Man_t * pNew;
     Aig_Obj_t * pObj;
     int i, Entry;
-    assert( p->pManHaig == NULL || Aig_ManBufNum(p) == 0 );
     assert( p->nAsserts == 0 || p->nConstrs == 0 );
     // create the new manager
     pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
@@ -175,7 +162,6 @@ Aig_Obj_t * Aig_ManDupSimpleDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t
         return (Aig_Obj_t *)(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((Aig_Obj_t *)pObj->pData)->pHaig = pObj->pHaig;
     return (Aig_Obj_t *)pObj->pData;
 }
 
@@ -200,7 +186,6 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
     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 = Abc_UtilStrsav( p->pName );
@@ -212,11 +197,9 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
     Aig_ManForEachCi( p, pObj, i )
     {
         pObjNew = Aig_ObjCreateCi( pNew );
-        pObjNew->pHaig = pObj->pHaig;
         pObjNew->Level = pObj->Level;
         pObj->pData = pObjNew;
     }
@@ -231,17 +214,10 @@ Aig_Man_t * Aig_ManDupSimpleDfs( Aig_Man_t * p )
     Aig_ManForEachCo( p, pObj, i )
     {
         pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
-        pObjNew->pHaig = pObj->pHaig;
         pObj->pData = pObjNew;
     }
     assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
     Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
-    // 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" );
@@ -337,7 +313,6 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
         }
         else
             assert( 0 );
-        Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
         pObj->pData = pObjNew;
     }
     assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
@@ -347,12 +322,6 @@ Aig_Man_t * Aig_ManDupOrdered( Aig_Man_t * p )
     // duplicate the timing manager
     if ( p->pManTime )
         pNew->pManTime = Tim_ManDup( (Tim_Man_t *)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" );
@@ -376,7 +345,6 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
     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 = Abc_UtilStrsav( p->pName );
@@ -388,7 +356,6 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
     // create the PIs
     Aig_ManCleanData( p );
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
     Aig_ManForEachCi( p, pObj, i )
     {
         if ( i == iInput )
@@ -396,7 +363,6 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
         else
         {
             pObjNew = Aig_ObjCreateCi( pNew );
-            pObjNew->pHaig = pObj->pHaig;
             pObjNew->Level = pObj->Level;
         }
         pObj->pData = pObjNew;
@@ -406,31 +372,22 @@ Aig_Man_t * Aig_ManDupCof( Aig_Man_t * p, int iInput, int Value )
         if ( Aig_ObjIsBuf(pObj) )
         {
             pObjNew = Aig_ObjChild0Copy(pObj);
-            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
             pObj->pData = pObjNew;
         }
         else if ( Aig_ObjIsNode(pObj) )
         {
             pObjNew = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
             pObj->pData = pObjNew;
         }
     // add the POs
     Aig_ManForEachCo( p, pObj, i )
     {
         pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
-        pObjNew->pHaig = pObj->pHaig;
         pObj->pData = pObjNew;
     }
 //    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
     Aig_ManCleanup( pNew );
     Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
-    // 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" );
@@ -539,7 +496,6 @@ Aig_Man_t * Aig_ManDupExor( Aig_Man_t * p )
         }
         else
             assert( 0 );
-        Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
         pObj->pData = pObjNew;
     }
     Aig_ManCleanup( pNew );
@@ -576,10 +532,6 @@ Aig_Obj_t * Aig_ManDupDfs_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj
         return (Aig_Obj_t *)(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 ( 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 )
     {
         assert( Aig_Regular(pEquivNew)->Id < Aig_Regular(pObjNew)->Id );
@@ -624,14 +576,12 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
     Aig_ManCleanData( p );
     // duplicate internal nodes
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
     Aig_ManForEachObj( p, pObj, i )
     {
         if ( Aig_ObjIsCi(pObj) )
         {
             pObjNew = Aig_ObjCreateCi( pNew );
             pObjNew->Level = pObj->Level;
-            pObjNew->pHaig = pObj->pHaig;
             pObj->pData = pObjNew;
         }
         else if ( Aig_ObjIsCo(pObj) )
@@ -639,7 +589,6 @@ 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_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
-            pObjNew->pHaig = pObj->pHaig;
             pObj->pData = pObjNew;
         }
     }
@@ -650,12 +599,6 @@ Aig_Man_t * Aig_ManDupDfs( Aig_Man_t * p )
     // duplicate the timing manager
     if ( p->pManTime )
         pNew->pManTime = Tim_ManDup( (Tim_Man_t *)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" );
@@ -720,8 +663,6 @@ Aig_Obj_t * Aig_ManDupDfsGuided_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t
     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 )
-        Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
     if ( pEquivNew )
     {
         if ( pNew->pEquivs )
@@ -771,14 +712,12 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios )
     Aig_ManCleanData( p );
     // duplicate internal nodes
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
     Vec_PtrForEachEntry( Aig_Obj_t *, vPios, pObj, i )
     {
         if ( Aig_ObjIsCi(pObj) )
         {
             pObjNew = Aig_ObjCreateCi( pNew );
             pObjNew->Level = pObj->Level;
-            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
             pObj->pData = pObjNew;
         }
         else if ( Aig_ObjIsCo(pObj) )
@@ -786,7 +725,6 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios )
             Aig_ManDupDfsGuided_rec( pNew, p, Aig_ObjFanin0(pObj) );        
 //            assert( pObj->Level == ((Aig_Obj_t*)pObj->pData)->Level );
             pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
-            Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
             pObj->pData = pObjNew;
         }
     }
@@ -841,11 +779,9 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
     }
     // create the PIs
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
     Aig_ManForEachCi( p, pObj, i )
     {
         pObjNew = Aig_ObjCreateCi( pNew );
-        pObjNew->pHaig = pObj->pHaig;
         pObjNew->Level = pObj->Level;
         pObj->pData = pObjNew;
     }
@@ -854,7 +790,6 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
     Vec_VecForEachEntry( Aig_Obj_t *, vLevels, pObj, i, k )
     {
         pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
-        Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
         pObj->pData = pObjNew;
     }
     Vec_VecFree( vLevels );
@@ -862,7 +797,6 @@ Aig_Man_t * Aig_ManDupLevelized( Aig_Man_t * p )
     Aig_ManForEachCo( p, pObj, i )
     {
         pObjNew = Aig_ObjCreateCo( pNew, Aig_ObjChild0Copy(pObj) );
-        pObjNew->pHaig = pObj->pHaig;
         pObj->pData = pObjNew;
     }
     assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 6a0555a0..230a2b18 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -100,7 +100,6 @@ Aig_Man_t * Aig_ManStartFrom( Aig_Man_t * p )
     {
         pObjNew = Aig_ObjCreateCi( pNew );
         pObjNew->Level = pObj->Level;
-        pObjNew->pHaig = pObj->pHaig;
         pObj->pData = pObjNew;
     }
     return pNew;
@@ -127,7 +126,6 @@ Aig_Obj_t * Aig_ManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
         return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
     Aig_ManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
     pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
-    Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
     return (Aig_Obj_t *)(pObj->pData = pObjNew);
 }
 
@@ -361,27 +359,6 @@ int Aig_ManCoCleanup( Aig_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Performs one iteration of AIG rewriting.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManHaigCounter( Aig_Man_t * pAig )
-{
-    Aig_Obj_t * pObj;
-    int Counter, i;
-    Counter = 0;
-    Aig_ManForEachNode( pAig, pObj, i )
-        Counter += (pObj->pHaig != NULL);
-    return Counter;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Stops the AIG manager.]
 
   Description []
diff --git a/src/aig/aig/aigObj.c b/src/aig/aig/aigObj.c
index 41a07823..e1eab364 100644
--- a/src/aig/aig/aigObj.c
+++ b/src/aig/aig/aigObj.c
@@ -49,12 +49,6 @@ Aig_Obj_t * Aig_ObjCreateCi( Aig_Man_t * p )
     pObj->Type = AIG_OBJ_CI;
     Vec_PtrPush( p->vCis, pObj );
     p->nObjs[AIG_OBJ_CI]++;
-    if ( p->pManHaig && p->fCreatePios )
-    {
-        p->pManHaig->nRegs++;
-        pObj->pHaig = Aig_ObjCreateCi( p->pManHaig );
-//        printf( "Creating PI HAIG node %d equivalent to PI %d.\n", pObj->pHaig->Id, pObj->Id );
-    }
     return pObj;
 }
 
@@ -77,11 +71,6 @@ Aig_Obj_t * Aig_ObjCreateCo( Aig_Man_t * p, Aig_Obj_t * pDriver )
     Vec_PtrPush( p->vCos, pObj );
     Aig_ObjConnect( p, pObj, pDriver, NULL );
     p->nObjs[AIG_OBJ_CO]++;
-    if ( p->pManHaig && p->fCreatePios )
-    {
-        pObj->pHaig = Aig_ObjCreateCo( p->pManHaig, Aig_ObjHaig( pDriver ) );
-//        printf( "Creating PO HAIG node %d equivalent to PO %d.\n", pObj->pHaig->Id, pObj->Id );
-    }
     return pObj;
 }
 
@@ -111,14 +100,6 @@ 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 );
-    }
     // create the power counter
     if ( p->vProbs )
     {
@@ -384,14 +365,6 @@ void Aig_ObjPrint( Aig_Man_t * p, Aig_Obj_t * pObj )
         }
         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] )
     {
@@ -511,19 +484,6 @@ 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( !Aig_IsComplement(pObjNewR->pHaig) );
-        assert( p->pManHaig->vEquPairs != NULL );
-        Vec_IntPush( p->pManHaig->vEquPairs, pObjNewR->pHaig->Id );
-        Vec_IntPush( p->pManHaig->vEquPairs, pObjOld->pHaig->Id );
-    }
-    else
-        pObjOld->pHaig = pObjNewR->pHaig? pObjNewR->pHaig : pObjOld->pHaig;
     // recursively delete the old node - but leave the object there
     pObjNewR->nRefs++;
     Aig_ObjDelete_rec( p, pObjOld, 0 );
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index d2d92b82..717f3192 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -1493,8 +1493,6 @@ void Aig_ManChoiceConstructiveOne( Aig_Man_t * pNew, Aig_Man_t * pPrev, Aig_Man_
     // make sure the nodes of pThis point to pPrev
     Aig_ManForEachObj( pPrev, pObj, i )
         pObj->fMarkB = 1;
-    Aig_ManForEachObj( pThis, pObj, i )
-        assert( pObj->pHaig == NULL || (!Aig_IsComplement(pObj->pHaig) && pObj->pHaig->fMarkB) );
     Aig_ManForEachObj( pPrev, pObj, i )
         pObj->fMarkB = 0;
     // remap nodes of pThis on top of pNew using pPrev
@@ -1506,13 +1504,7 @@ void Aig_ManChoiceConstructiveOne( Aig_Man_t * pNew, Aig_Man_t * pPrev, Aig_Man_
         pObj->pData = Aig_ManCo(pNew, i);
     // go through the nodes in the topological order
     Aig_ManForEachNode( pThis, pObj, i )
-    {
         pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-        if ( pObj->pHaig == NULL )
-            continue;
-        // pObj->pData and pObj->pHaig->pData are equivalent
-        Aig_ObjSetRepr_( pNew, Aig_Regular((Aig_Obj_t *)pObj->pData), Aig_Regular((Aig_Obj_t *)pObj->pHaig->pData) );
-    }
     // set the inputs of POs as equivalent
     Aig_ManForEachCo( pThis, pObj, i )
     {
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index edf5798e..a3231929 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -7,7 +7,6 @@ SRC +=  src/aig/saig/saigBmc.c \
     src/aig/saig/saigConstr2.c \
     src/aig/saig/saigDual.c \
     src/aig/saig/saigDup.c \
-    src/aig/saig/saigHaig.c \
     src/aig/saig/saigInd.c \
     src/aig/saig/saigIoa.c \
     src/aig/saig/saigIso.c \
diff --git a/src/aig/saig/saigHaig.c b/src/aig/saig/saigHaig.c
deleted file mode 100644
index 7cb34c5d..00000000
--- a/src/aig/saig/saigHaig.c
+++ /dev/null
@@ -1,733 +0,0 @@
-/**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 "sat/bsat/satSolver.h"
-#include "sat/cnf/cnf.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        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;
-    Aig_Obj_t * pPo;
-    // skip nodes without representative
-    pObjRepr = pObj->pHaig;
-    if ( pObjRepr == NULL )
-        return;
-//    assert( pObjRepr->Id < pObj->Id );
-    // get the new node 
-    pObjNew = (Aig_Obj_t *)pObj->pData;
-    // get the new node of the representative
-    pObjReprNew = (Aig_Obj_t *)pObjRepr->pData;
-    // if this is the same node, no need to add constraints
-    assert( pObjNew != NULL && pObjReprNew != NULL );
-    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
-    if ( pObj->fMarkA )
-        return;
-//    pMiter = Aig_Exor( pFrames, pObjNew, pObjReprNew );
-//    pMiter = Aig_NotCond( pMiter, !Aig_ObjPhaseReal(pMiter) );
-//    assert( Aig_ObjPhaseReal(pMiter) == 1 );
-//    Aig_ObjCreateCo( pFrames, pMiter );
-    if ( Aig_ObjPhaseReal(pObjNew) != Aig_ObjPhaseReal(pObjReprNew) )
-        pObjReprNew = Aig_Not(pObjReprNew);
-    pPo = Aig_ObjCreateCo( pFrames, pObjNew );
-    Aig_ObjCreateCo( pFrames, pObjReprNew );
-
-    // remember the node corresponding to this PO
-    pPo->pData = pObj;
-}
-
-/**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 = Abc_UtilStrsav( pHaig->pName );
-    pFrames->pSpec = Abc_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_ObjCreateCi( pFrames );
-    // add timeframes
-    Aig_ManSetCioIds( pHaig );
-    for ( f = 0; f < nFrames; f++ )
-    {
-        // create primary inputs
-        Saig_ManForEachPi( pHaig, pObj, i )
-            pObj->pData = Aig_ObjCreateCi( pFrames );
-        // create internal nodes
-        Aig_ManForEachNode( pHaig, pObj, i )
-        {        
-            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-            Aig_ManHaigSpeculate( pFrames, pObj );
-        }
-        if ( f == nFrames - 2 )
-            nAssumptions = Aig_ManCoNum(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_ManCoNum(pFrames) - nAssumptions;
-    Aig_ManSetRegNum( pFrames, 0 );
-    return pFrames;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManMapHaigNodes( Aig_Man_t * pHaig )
-{
-    Aig_Obj_t * pObj1, * pObj2;
-    int Id1, Id2, i, Counter = 0;
-    Aig_ManForEachObj( pHaig, pObj1, i )
-        pObj1->pHaig = NULL;
-    Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
-    {
-        Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
-        pObj1 = Aig_ManObj( pHaig, Id1 );
-        pObj2 = Aig_ManObj( pHaig, Id2 );
-        assert( pObj1 != pObj2 );
-        assert( !Aig_ObjIsCi(pObj1) || !Aig_ObjIsCi(pObj2) );
-        if ( Aig_ObjIsCi(pObj1) )
-        {
-            Counter += (int)(pObj2->pHaig != NULL);
-            pObj2->pHaig = pObj1;
-        }
-        else if ( Aig_ObjIsCi(pObj2) )
-        {
-            Counter += (int)(pObj1->pHaig != NULL);
-            pObj1->pHaig = pObj2;
-        }
-        else if ( pObj1->Id < pObj2->Id )
-        {
-            Counter += (int)(pObj2->pHaig != NULL);
-            pObj2->pHaig = pObj1;
-        }
-        else 
-        {
-            Counter += (int)(pObj1->pHaig != NULL);
-            pObj1->pHaig = pObj2;
-        }
-    }
-//    printf( "Overwrites %d out of %d.\n", Counter, Vec_IntSize(pHaig->vEquPairs)/2 );
-    return Counter;
-}
- 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManHaigVerify( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames, clock_t clkSynth )
-{
-    int nBTLimit = 0;
-    Aig_Man_t * pFrames, * pTemp;
-    Cnf_Dat_t * pCnf;
-    sat_solver * pSat;
-    Aig_Obj_t * pObj1, * pObj2;
-    int i, RetValue1, RetValue2, Counter, Lits[2], nOvers;
-    clock_t clk = clock(), clkVerif;
-
-    nOvers = Aig_ManMapHaigNodes( pHaig );
-
-    // create time frames with speculative reduction and convert them into CNF
-clk = clock();
-    pFrames = Aig_ManHaigFrames( pHaig, nFrames );
-    Aig_ManCleanMarkA( pHaig );
-
-    printf( "Frames:     " );
-    Aig_ManPrintStats( pFrames );
-
-    pFrames = Dar_ManRwsat( pTemp = pFrames, 1, 0 );
-    Aig_ManStop( pTemp );
-
-    printf( "Frames synt:" );
-    Aig_ManPrintStats( pFrames );
-
-    printf( "Additional frames stats: Assumptions = %d. Assertions = %d. Pairs = %d. Over = %d.\n", 
-        Aig_ManCoNum(pFrames)/2 - pFrames->nAsserts/2, pFrames->nAsserts/2, Vec_IntSize(pHaig->vEquPairs)/2, nOvers );
-//    pCnf = Cnf_DeriveSimple( pFrames, Aig_ManCoNum(pFrames) );
-    pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) );
-
-
-
-//    pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(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 = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
-    if ( pSat == NULL )
-    {
-        printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
-        return 0;
-    }
-
-    if ( nFrames == 2 )
-    {
-        // add clauses for the first frame
-        Aig_ManForEachCo( pFrames, pObj1, i )
-        {
-            if ( i >= Aig_ManCoNum(pFrames) - pFrames->nAsserts )
-                break;
-
-            pObj2 = Aig_ManCo( pFrames, ++i );
-            assert( pObj1->fPhase == pObj2->fPhase );
-
-            Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
-            Lits[1] = toLitCond( pCnf->pVarNums[pObj2->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;
-            }
-        }
-
-        if ( !sat_solver_simplify(pSat) )
-        {
-            sat_solver_delete( pSat );
-            return 0;
-        }
-    }
-ABC_PRT( "Preparation", clock() - clk );
-
-
-    // check in the second timeframe
-clk = clock();
-    Counter = 0;
-    printf( "Started solving ...\r" );
-    Aig_ManForEachCo( pFrames, pObj1, i )
-    {
-        if ( i < Aig_ManCoNum(pFrames) - pFrames->nAsserts )
-            continue;
-
-        pObj2 = Aig_ManCo( pFrames, ++i );
-        assert( pObj1->fPhase == pObj2->fPhase );
-
-        Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
-        Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id], 1 );
-
-        RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-        if ( RetValue1 == l_False )
-        {
-            Lits[0] = lit_neg( Lits[0] );
-            Lits[1] = lit_neg( Lits[1] );
-//            RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
-//            assert( RetValue );
-        }
-
-        Lits[0]++;
-        Lits[1]--;
-
-        RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-        if ( RetValue2 == l_False )
-        {
-            Lits[0] = lit_neg( Lits[0] );
-            Lits[1] = lit_neg( Lits[1] );
-//            RetValue = sat_solver_addclause( pSat, Lits, Lits + 2 );
-//            assert( RetValue );
-        }
-
-        if ( RetValue1 != l_False || RetValue2 != l_False )
-            Counter++;
-
-        if ( i % 50 == 1 )
-            printf( "Solving assertion %6d out of %6d.\r", 
-                (i - (Aig_ManCoNum(pFrames) - pFrames->nAsserts))/2, 
-                pFrames->nAsserts/2 );
-//        if ( nClasses == 1000 )
-//            break;
-    }
-    printf( "                                                          \r" );
-ABC_PRT( "Solving    ", clock() - clk );
-clkVerif = clock() - clk;
-    if ( Counter )
-        printf( "Verification failed for %d out of %d assertions.\n", Counter, pFrames->nAsserts/2 );
-    else
-        printf( "Verification is successful for all %d assertions.\n", pFrames->nAsserts/2 );
-
-    // print the statistic into a file
-    {
-        FILE * pTable;
-        Aig_Man_t * pTemp, * pHaig2;
-
-        pHaig2 = pAig->pManHaig; 
-        pAig->pManHaig = NULL;
-        pTemp = Aig_ManDupDfs( pAig );
-        pAig->pManHaig = pHaig2;
-
-        Aig_ManSeqCleanup( pTemp );
-
-        pTable = fopen( "stats.txt", "a+" );
-        fprintf( pTable, "%s ",  p->pName );
-        fprintf( pTable, "%d ", Saig_ManPiNum(p) );
-        fprintf( pTable, "%d ", Saig_ManPoNum(p) );
-
-        fprintf( pTable, "%d ", Saig_ManRegNum(p) );
-        fprintf( pTable, "%d ", Aig_ManNodeNum(p) );
-        fprintf( pTable, "%d ", Aig_ManLevelNum(p) );
-
-        fprintf( pTable, "%d ", Saig_ManRegNum(pTemp) );
-        fprintf( pTable, "%d ", Aig_ManNodeNum(pTemp) );
-        fprintf( pTable, "%d ", Aig_ManLevelNum(pTemp) );
-
-        fprintf( pTable, "%d ", Saig_ManRegNum(pHaig) );
-        fprintf( pTable, "%d ", Aig_ManNodeNum(pHaig) );
-        fprintf( pTable, "%d ", Aig_ManLevelNum(pHaig) );
-
-        fprintf( pTable, "%.2f", (float)(clkSynth)/(float)(CLOCKS_PER_SEC) );
-        fprintf( pTable, "\n" );
-        fclose( pTable );
-
-
-        pTable = fopen( "stats2.txt", "a+" );
-        fprintf( pTable, "%s ",  p->pName );
-        fprintf( pTable, "%d ", Aig_ManNodeNum(pFrames) );
-        fprintf( pTable, "%d ", Aig_ManLevelNum(pFrames) );
-
-        fprintf( pTable, "%d ", pCnf->nVars );
-        fprintf( pTable, "%d ", pCnf->nClauses );
-        fprintf( pTable, "%d ", pCnf->nLiterals );
-
-        fprintf( pTable, "%d ", Aig_ManCoNum(pFrames)/2 - pFrames->nAsserts/2 );
-        fprintf( pTable, "%d ", pFrames->nAsserts/2 );
-        fprintf( pTable, "%d ", Vec_IntSize(pHaig->vEquPairs)/2 );
-
-        fprintf( pTable, "%.2f", (float)(clkVerif)/(float)(CLOCKS_PER_SEC) );
-        fprintf( pTable, "\n" );
-        fclose( pTable );
-
-        Aig_ManStop( pTemp );
-    }
-
-    // clean up
-    Aig_ManStop( pFrames );
-    Cnf_DataFree( pCnf );
-    sat_solver_delete( pSat );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManHaigVerify2( Aig_Man_t * p, Aig_Man_t * pAig, Aig_Man_t * pHaig, int nFrames )
-{
-    int nBTLimit = 0;
-    Cnf_Dat_t * pCnf;
-    sat_solver * pSat;
-    Aig_Obj_t * pObj1, * pObj2;
-    int i, RetValue1, RetValue2, Counter, Lits[2];
-    clock_t clk = clock();
-    int Delta;
-    int Id1, Id2;
-
-    assert( nFrames == 1 || nFrames == 2 );
-
-clk = clock();
-    pCnf = Cnf_DeriveSimple( pHaig, Aig_ManCoNum(pHaig) );
-//    Aig_ManForEachObj( pHaig, pObj, i )
-//        printf( "%d=%d  ", pObj->Id, pCnf->pVarNums[pObj->Id] );
-//    printf( "\n" );
-
-    // create the SAT solver to be used for this problem
-    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, nFrames, 0 );
-//Sat_SolverWriteDimacs( pSat, "1.cnf", NULL, NULL, 0 );
-    if ( pSat == NULL )
-    {
-        printf( "Aig_ManHaigVerify(): Computed CNF is not valid.\n" );
-        return -1;
-    }
-
-    if ( nFrames == 2 )
-    {
-        Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
-        {
-            Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
-            pObj1 = Aig_ManObj( pHaig, Id1 );
-            pObj2 = Aig_ManObj( pHaig, Id2 );
-            if ( pObj1->fPhase ^ pObj2->fPhase )
-            {
-                Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id], 0 );
-                Lits[1] = toLitCond( pCnf->pVarNums[pObj2->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[pObj1->Id], 0 );
-                Lits[1] = toLitCond( pCnf->pVarNums[pObj2->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;
-                }
-            }
-        }
-
-        if ( !sat_solver_simplify(pSat) )
-        {
-            sat_solver_delete( pSat );
-            return 0;
-        }
-    }
-ABC_PRT( "Preparation", clock() - clk );
-
-
-    // check in the second timeframe
-clk = clock();
-    Counter = 0;
-    Delta = (nFrames == 2)? pCnf->nVars : 0;
-    Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
-    {
-        Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
-        pObj1 = Aig_ManObj( pHaig, Id1 );
-        pObj2 = Aig_ManObj( pHaig, Id2 );
-        if ( pObj1->fPhase ^ pObj2->fPhase )
-        {
-            Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 );
-            Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 0 );
-
-            RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-
-            Lits[0]++;
-            Lits[1]++;
-
-            RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-
-            if ( RetValue1 != l_False || RetValue2 != l_False )
-                Counter++;
-        }
-        else
-        {
-            Lits[0] = toLitCond( pCnf->pVarNums[pObj1->Id]+Delta, 0 );
-            Lits[1] = toLitCond( pCnf->pVarNums[pObj2->Id]+Delta, 1 );
-
-            RetValue1 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-
-            Lits[0]++;
-            Lits[1]--;
-
-            RetValue2 = sat_solver_solve( pSat, Lits, Lits + 2, (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-
-            if ( RetValue1 != l_False || RetValue2 != l_False )
-                Counter++;
-        }
-        if ( i % 50 == 1 )
-            printf( "Solving assertion %6d out of %6d.\r", i/2, Vec_IntSize(pHaig->vEquPairs)/2 );
-
-//        if ( i / 2 > 1000 )
-//            break;
-    }
-ABC_PRT( "Solving    ", clock() - clk );
-    if ( Counter )
-        printf( "Verification failed for %d out of %d classes.\n", Counter, Vec_IntSize(pHaig->vEquPairs)/2 );
-    else
-        printf( "Verification is successful for all %d classes.\n", Vec_IntSize(pHaig->vEquPairs)/2 );
-
-    Cnf_DataFree( pCnf );
-    sat_solver_delete( pSat );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_ManHaigDump( Aig_Man_t * pHaig )
-{
-    Vec_Ptr_t * vTemp;
-    Aig_Obj_t * pObj, * pObj1, * pObj2, * pMiter;
-    int Id1, Id2, i;
-    // remove regular POs
-    Aig_ManSetCioIds( pHaig );
-    vTemp = Vec_PtrAlloc( Saig_ManRegNum(pHaig) );
-    Aig_ManForEachCo( pHaig, pObj, i )
-    {
-        if ( Saig_ObjIsPo(pHaig, pObj) )
-        {
-            Aig_ObjDisconnect( pHaig, pObj );
-            Vec_PtrWriteEntry( pHaig->vObjs, pObj->Id, NULL );
-        }
-        else
-        {
-            Vec_PtrPush( vTemp, pObj );
-        }
-    }
-    Vec_PtrShrink( pHaig->vCos, 0 ); 
-    pHaig->nObjs[AIG_OBJ_CO] = Vec_PtrSize( vTemp );
-    // add new POs
-    Vec_IntForEachEntry( pHaig->vEquPairs, Id1, i )
-    {
-        Id2 = Vec_IntEntry( pHaig->vEquPairs, ++i );
-        pObj1 = Aig_ManObj( pHaig, Id1 );
-        pObj2 = Aig_ManObj( pHaig, Id2 );
-        assert( pObj1 != pObj2 );
-        assert( !Aig_ObjIsCi(pObj1) || !Aig_ObjIsCi(pObj2) );
-        pMiter = Aig_Exor( pHaig, pObj1, pObj2 );
-        pMiter = Aig_NotCond( pMiter, Aig_ObjPhaseReal(pMiter) );
-        assert( Aig_ObjPhaseReal(pMiter) == 0 );
-        Aig_ObjCreateCo( pHaig, pMiter );
-    }
-    printf( "Added %d property outputs.\n", Vec_IntSize(pHaig->vEquPairs)/2 );
-    // add the registers
-    Vec_PtrForEachEntry( Aig_Obj_t *, vTemp, pObj, i )
-        Vec_PtrPush( pHaig->vCos, pObj );
-    Vec_PtrFree( vTemp );
-    assert( pHaig->nObjs[AIG_OBJ_CO] ==  Vec_PtrSize(pHaig->vCos) ); 
-    Aig_ManCleanup( pHaig );
-    Aig_ManSetRegNum( pHaig, pHaig->nRegs );
-//    return pHaig;
-
-    printf( "HAIG:       " );
-    Aig_ManPrintStats( pHaig );
-    printf( "HAIG is written into file \"haig.blif\".\n" );
-    Saig_ManDumpBlif( pHaig, "haig.blif" );
-
-    Vec_IntFree( pHaig->vEquPairs );
-    Aig_ManStop( pHaig );
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSteps, int fRetimingOnly, int fAddBugs, int fUseCnf, int fVerbose )
-{
-    int fSeqHaig = (int)( Aig_ManRegNum(p) > 0 );
-    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
-    Aig_Man_t * pNew, * pTemp;
-    Aig_Obj_t * pObj;
-    int i, k, nStepsReal;
-    clock_t clk = clock(), clkSynth;
-    Dar_ManDefaultRwrParams( pParsRwr );
-
-clk = clock();
-    // duplicate this manager
-    pNew = Aig_ManDupSimple( p );
-    // create its history AIG
-    pNew->pManHaig = Aig_ManDupSimple( pNew );
-    Aig_ManForEachObj( pNew, pObj, i )
-        pObj->pHaig = (Aig_Obj_t *)pObj->pData;
-    // remove structural hashing table
-    Aig_TableClear( pNew->pManHaig );
-    pNew->pManHaig->vEquPairs = Vec_IntAlloc( 10000 );
-ABC_PRT( "HAIG setup time", clock() - clk );
-
-clk = clock();
-    if ( fSeqHaig )
-    {
-        if ( fRetimingOnly )
-        {
-            // perform retiming
-            nStepsReal = Saig_ManRetimeSteps( pNew, nSteps, 1, fAddBugs ); 
-            pNew = Aig_ManDupSimpleDfs( pTemp = pNew ); 
-            Aig_ManStop( pTemp );
-            printf( "Performed %d retiming moves.\n", nStepsReal );
-        }
-        else
-        {
-            for ( k = 0; k < nIters; k++ )
-            {
-                // perform balancing
-                pNew = Dar_ManBalance( pTemp = pNew, 0 );
-                Aig_ManStop( pTemp );
-
-                // perform rewriting
-                Dar_ManRewrite( pNew, pParsRwr );
-                pNew = Aig_ManDupDfs( pTemp = pNew ); 
-                Aig_ManStop( pTemp );
-
-                // perform retiming
-                nStepsReal = Saig_ManRetimeSteps( pNew, nSteps, 1, fAddBugs ); 
-                pNew = Aig_ManDupSimpleDfs( pTemp = pNew ); 
-                Aig_ManStop( pTemp );
-                printf( "Performed %d retiming moves.\n", nStepsReal );
-            }
-        }
-    }
-    else
-    {
-        for ( k = 0; k < nIters; k++ )
-        {
-            // perform balancing
-            pNew = Dar_ManBalance( pTemp = pNew, 0 );
-            Aig_ManStop( pTemp );
-
-            // perform rewriting
-            Dar_ManRewrite( pNew, pParsRwr );
-            pNew = Aig_ManDupDfs( pTemp = pNew ); 
-            Aig_ManStop( pTemp );
-        }
-    } 
-ABC_PRT( "Synthesis time ", clock() - clk );
-clkSynth = clock() - clk;
-
-    // use the haig for verification
-//    Aig_ManAntiCleanup( pNew->pManHaig );
-    Aig_ManSetRegNum( pNew->pManHaig, pNew->pManHaig->nRegs );
-//Aig_ManShow( pNew->pManHaig, 0, NULL ); 
-
-    printf( "AIG before: " );
-    Aig_ManPrintStats( p );
-    printf( "AIG after:  " );
-    Aig_ManPrintStats( pNew );
-    printf( "HAIG:       " );
-    Aig_ManPrintStats( pNew->pManHaig );
-
-    if ( fUseCnf )
-    {
-        if ( !Aig_ManHaigVerify2( p, pNew, pNew->pManHaig, 1+fSeqHaig ) )
-            printf( "Constructing SAT solver has failed.\n" );         
-    }
-    else
-    {
-        if ( !Aig_ManHaigVerify( p, pNew, pNew->pManHaig, 1+fSeqHaig, clkSynth ) )
-            printf( "Constructing SAT solver has failed.\n" );         
-    }
-
-    Saig_ManHaigDump( pNew->pManHaig );
-    pNew->pManHaig = NULL;
-    return pNew;
-/*
-    // cleanup
-    Vec_IntFree( pNew->pManHaig->vEquPairs );
-    Aig_ManStop( pNew->pManHaig );
-    pNew->pManHaig = NULL;
-    return pNew;
-*/
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 91f10590..fd93ccec 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -215,7 +215,6 @@ struct Abc_Ntk_t_
     void *            pExcare;       // the EXDC network (if given)
     void *            pData;         // misc
     Abc_Ntk_t *       pCopy;         // copy of this network
-    void *            pHaig;         // history AIG
     float *           pLutTimes;     // arrivals/requireds/slacks using LUT-delay model
     Vec_Ptr_t *       vOnehots;      // names of one-hot-encoded registers
     Vec_Int_t *       vObjPerm;      // permutation saved
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index 4e725a01..5fc3ffd3 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -344,9 +344,6 @@ Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
     // add the node to the list of updated nodes
     if ( pMan->vAddedCells )
         Vec_PtrPush( pMan->vAddedCells, pAnd );
-    // create HAIG
-//    if ( pAnd->pNtk->pHaig )
-//        pAnd->pEquiv = Hop_And( pAnd->pNtk->pHaig, Abc_ObjChild0Equiv(pAnd), Abc_ObjChild1Equiv(pAnd) );
     return pAnd;
 }
 
@@ -387,9 +384,6 @@ Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t *
     // add the node to the list of updated nodes
 //    if ( pMan->vAddedCells )
 //        Vec_PtrPush( pMan->vAddedCells, pAnd );
-    // create HAIG
-//    if ( pAnd->pNtk->pHaig )
-//        pAnd->pEquiv = Hop_And( pAnd->pNtk->pHaig, Abc_ObjChild0Equiv(pAnd), Abc_ObjChild1Equiv(pAnd) );
     return pAnd;
 }
 
@@ -858,9 +852,6 @@ void Abc_AigReplace( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, int f
     Vec_PtrPush( pMan->vStackReplaceOld, pOld );
     Vec_PtrPush( pMan->vStackReplaceNew, pNew );
     assert( !Abc_ObjIsComplement(pOld) );
-    // create HAIG
-//    if ( pOld->pNtk->pHaig )
-//        Hop_ObjCreateChoice( pOld->pEquiv, Abc_ObjRegular(pNew)->pEquiv );
     // process the replacements
     while ( Vec_PtrSize(pMan->vStackReplaceOld) )
     {
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 5f9c0f0d..db54643d 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -1070,9 +1070,6 @@ void Abc_NtkDelete( Abc_Ntk_t * pNtk )
 //    int LargePiece = (4 << ABC_NUM_STEPS);
     if ( pNtk == NULL )
         return;
-    // free the HAIG
-//    if ( pNtk->pHaig )
-//        Abc_NtkHaigStop( pNtk );
     // free EXDC Ntk
     if ( pNtk->pExdc )
         Abc_NtkDelete( pNtk->pExdc );
diff --git a/src/base/abci/abcBalance.c b/src/base/abci/abcBalance.c
index 2c391e89..9807997c 100644
--- a/src/base/abci/abcBalance.c
+++ b/src/base/abci/abcBalance.c
@@ -277,9 +277,6 @@ Abc_Obj_t * Abc_NodeBalance_rec( Abc_Ntk_t * pNtkNew, Abc_Obj_t * pNodeOld, Vec_
 //    if ( Abc_ObjRegular(pNodeOld->pCopy) == Abc_AigConst1(pNtkNew) )
 //        printf( "Constant node\n" );
 //    assert( pNodeOld->Level >= Abc_ObjRegular(pNodeOld->pCopy)->Level );
-    // update HAIG
-//    if ( Abc_ObjRegular(pNodeOld->pCopy)->pNtk->pHaig )
-//        Hop_ObjCreateChoice( pNodeOld->pEquiv, Abc_ObjRegular(pNodeOld->pCopy)->pEquiv );
     return pNodeOld->pCopy;
 }
 
diff --git a/src/base/abci/abcHaig.c b/src/base/abci/abcHaig.c
index d6c0ddad..02547de1 100644
--- a/src/base/abci/abcHaig.c
+++ b/src/base/abci/abcHaig.c
@@ -31,129 +31,6 @@ ABC_NAMESPACE_IMPL_START
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-#if 0
-
-/**Function*************************************************************
-
-  Synopsis    [Start history AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkHaigStart( Abc_Ntk_t * pNtk )
-{
-    Hop_Man_t * p;
-    Abc_Obj_t * pObj, * pTemp;
-    int i;
-    assert( Abc_NtkIsStrash(pNtk) );
-    // check if the package is already started
-    if ( pNtk->pHaig )
-    {
-        Abc_NtkHaigStop( pNtk );
-        assert( pNtk->pHaig == NULL );
-        printf( "Warning: Previous history AIG was removed.\n" );
-    }
-    // make sure the data is clean
-    Abc_NtkForEachObj( pNtk, pObj, i )
-        assert( pObj->pEquiv == NULL );
-    // start the HOP package
-    p = Hop_ManStart();
-    p->vObjs = Vec_PtrAlloc( 4096 );
-    Vec_PtrPush( p->vObjs, Hop_ManConst1(p) );
-    // map the constant node
-    Abc_AigConst1(pNtk)->pEquiv = Hop_ManConst1(p);
-    // map the CIs
-    Abc_NtkForEachCi( pNtk, pObj, i )
-        pObj->pEquiv = Hop_ObjCreatePi(p);
-    // map the internal nodes
-    Abc_NtkForEachNode( pNtk, pObj, i )
-        pObj->pEquiv = Hop_And( p, Abc_ObjChild0Equiv(pObj), Abc_ObjChild1Equiv(pObj) );
-    // map the choice nodes
-    if ( Abc_NtkGetChoiceNum( pNtk ) )
-    {
-        // print warning about choice nodes
-        printf( "Warning: The choice nodes in the original AIG are converted into HAIG.\n" );
-        Abc_NtkForEachNode( pNtk, pObj, i )
-        {
-            if ( !Abc_AigNodeIsChoice( pObj ) )
-                continue;
-            for ( pTemp = pObj->pData; pTemp; pTemp = pTemp->pData )
-                Hop_ObjCreateChoice( pObj->pEquiv, pTemp->pEquiv );
-        }
-    }
-    // make sure everything is okay
-    if ( !Hop_ManCheck(p) )
-    {
-        printf( "Abc_NtkHaigStart: Check for History AIG has failed.\n" );
-        Hop_ManStop(p);
-        return 0;
-    }
-    pNtk->pHaig = p;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops history AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_NtkHaigStop( Abc_Ntk_t * pNtk )
-{
-    Abc_Obj_t * pObj;
-    int i;
-    assert( Abc_NtkIsStrash(pNtk) );
-    if ( pNtk->pHaig == NULL )
-    {
-        printf( "Warning: History AIG is not allocated.\n" );
-        return 1;
-    }
-    Abc_NtkForEachObj( pNtk, pObj, i )
-        pObj->pEquiv = NULL;
-    Hop_ManStop( pNtk->pHaig );
-    pNtk->pHaig = NULL;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Transfers the HAIG to the new network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abc_NtkHaigTranfer( Abc_Ntk_t * pNtkOld, Abc_Ntk_t * pNtkNew )
-{
-    Abc_Obj_t * pObj;
-    int i;
-    if ( pNtkOld->pHaig == NULL )
-        return;
-    // transfer the package
-    assert( pNtkNew->pHaig == NULL );
-    pNtkNew->pHaig = pNtkOld->pHaig;
-    pNtkOld->pHaig = NULL;
-    // transfer constant pointer
-    Abc_AigConst1(pNtkOld)->pCopy->pEquiv = Abc_AigConst1(pNtkOld)->pEquiv;
-    // transfer the CI pointers
-    Abc_NtkForEachCi( pNtkOld, pObj, i )
-        pObj->pCopy->pEquiv = pObj->pEquiv;
-}
-
-
-#endif
 
 /**Function*************************************************************
 
@@ -642,64 +519,6 @@ int Abc_NtkHaigResetReprs( Hop_Man_t * p )
     return nFanouts;
 }
 
-#if 0
-
-/**Function*************************************************************
-
-  Synopsis    [Stops history AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Ntk_t * Abc_NtkHaigUse( Abc_Ntk_t * pNtk )
-{
-    Hop_Man_t * pMan, * pManTemp;
-    Abc_Ntk_t * pNtkAig;
-    Abc_Obj_t * pObj;
-    int i;
-
-    // check if HAIG is available
-    assert( Abc_NtkIsStrash(pNtk) );
-    if ( pNtk->pHaig == NULL )
-    {
-        printf( "Warning: History AIG is not available.\n" );
-        return NULL;
-    }
-    // convert HOP package into AIG with choices
-    // print HAIG stats
-//    Hop_ManPrintStats( pMan ); // USES DATA!!!
-
-    // add the POs
-    Abc_NtkForEachCo( pNtk, pObj, i )
-        Hop_ObjCreatePo( pNtk->pHaig, Abc_ObjChild0Equiv(pObj) );
-
-    // clean the old network
-    Abc_NtkForEachObj( pNtk, pObj, i )
-        pObj->pEquiv = NULL;
-    pMan = pNtk->pHaig; 
-    pNtk->pHaig = 0;
-
-    // iteratively reconstruct the HOP manager to create choice nodes
-    while ( Abc_NtkHaigResetReprs( pMan ) )
-    {
-        pMan = Abc_NtkHaigReconstruct( pManTemp = pMan );
-        Hop_ManStop( pManTemp );
-    }
-
-    // traverse in the topological order and create new AIG
-    pNtkAig = Abc_NtkHaigRecreateAig( pNtk, pMan );
-    Hop_ManStop( pMan );
-
-    // free HAIG
-    return pNtkAig;
-}
-
-#endif
-
 /**Function*************************************************************
 
   Synopsis    [Transform HOP manager into the one without loops.]
diff --git a/src/base/abci/abcPart.c b/src/base/abci/abcPart.c
index 779c5c7e..c68e0729 100644
--- a/src/base/abci/abcPart.c
+++ b/src/base/abci/abcPart.c
@@ -1000,7 +1000,6 @@ Hop_Man_t * Abc_NtkPartStartHop( Abc_Ntk_t * pNtk )
 Abc_Ntk_t * Abc_NtkPartStitchChoices( Abc_Ntk_t * pNtk, Vec_Ptr_t * vParts )
 {
     extern Abc_Ntk_t * Abc_NtkHopRemoveLoops( Abc_Ntk_t * pNtk, Hop_Man_t * pMan );
-
     Hop_Man_t * pMan;
     Vec_Ptr_t * vNodes;
     Abc_Ntk_t * pNtkNew, * pNtkTemp;
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index e25e497d..cb57acaa 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -21,7 +21,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcFraig.c \
         src/base/abci/abcFxu.c \
         src/base/abci/abcGen.c \
-        src/base/abci/abcHaig.c \
+    src/base/abci/abcHaig.c \
     src/base/abci/abcIf.c \
     src/base/abci/abcIfif.c \
     src/base/abci/abcIfMux.c \
diff --git a/src/opt/dar/darBalance.c b/src/opt/dar/darBalance.c
index 75f0eaf4..f31c6fc7 100644
--- a/src/opt/dar/darBalance.c
+++ b/src/opt/dar/darBalance.c
@@ -532,19 +532,6 @@ 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 );
-    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( !Aig_IsComplement(pObjNewR->pHaig) );
-        assert( pNew->pManHaig->vEquPairs != NULL );
-        Vec_IntPush( pNew->pManHaig->vEquPairs, pObjNewR->pHaig->Id );
-        Vec_IntPush( pNew->pManHaig->vEquPairs, pObjOld->pHaig->Id );
-    }
-    else
-        Aig_Regular(pObjNew)->pHaig = pObjOld->pHaig;
     return (Aig_Obj_t *)(pObjOld->pData = pObjNew);
 }
 
@@ -574,12 +561,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
     pNew->nConstrs = p->nConstrs;
     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);
@@ -598,7 +579,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
                 // copy the PI
                 pObjNew = Aig_ObjCreateCi(pNew); 
                 pObj->pData = pObjNew;
-                pObjNew->pHaig = pObj->pHaig;
                 // set the arrival time of the new PI
                 arrTime = Tim_ManGetCiArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj) );
                 pObjNew->Level = (int)arrTime;
@@ -614,7 +594,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
                 Tim_ManSetCoArrival( (Tim_Man_t *)p->pManTime, Aig_ObjCioId(pObj), arrTime );
                 // create PO
                 pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
-                pObjNew->pHaig = pObj->pHaig;
             }
             else
                 assert( 0 );
@@ -629,7 +608,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
             pObjNew = Aig_ObjCreateCi(pNew); 
             pObjNew->Level = pObj->Level;
             pObj->pData = pObjNew;
-            pObjNew->pHaig = pObj->pHaig;
         }
         Aig_ManForEachCo( p, pObj, i )
         {
@@ -637,7 +615,6 @@ Aig_Man_t * Dar_ManBalance( Aig_Man_t * p, int fUpdateLevel )
             pObjNew = Dar_Balance_rec( pNew, Aig_Regular(pDriver), vStore, 0, fUpdateLevel );
             pObjNew = Aig_NotCond( pObjNew, Aig_IsComplement(pDriver) );
             pObjNew = Aig_ObjCreateCo( pNew, pObjNew );
-            pObjNew->pHaig = pObj->pHaig;
         }
     }
     Vec_VecFree( vStore );
diff --git a/src/opt/dar/darScript.c b/src/opt/dar/darScript.c
index b3830cc3..583ca563 100644
--- a/src/opt/dar/darScript.c
+++ b/src/opt/dar/darScript.c
@@ -134,27 +134,6 @@ Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose )
 
 /**Function*************************************************************
 
-  Synopsis    [Performs one iteration of AIG rewriting.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Dar_ManHaigPrintStats( Aig_Man_t * pAig )
-{
-    Aig_Obj_t * pObj;
-    int Counter, i;
-    Counter = 0;
-    Aig_ManForEachNode( pAig, pObj, i )
-        Counter += (pObj->pHaig != NULL);
-    printf( "Total nodes = %6d. Equiv nodes = %6d.\n", Aig_ManNodeNum(pAig), Counter );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Reproduces script "compress".]
 
   Description []
@@ -352,34 +331,20 @@ Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateL
 //alias resyn2   "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
 {
     Vec_Ptr_t * vAigs;
-    Aig_Obj_t * pObj;
-    int i;
 
     vAigs = Vec_PtrAlloc( 3 );
     pAig = Aig_ManDupDfs(pAig);
     Vec_PtrPush( vAigs, pAig );
 
-    Aig_ManForEachObj( pAig, pObj, i )
-        pObj->pHaig = pObj;
-
     pAig = Dar_ManCompress(pAig, fBalance, fUpdateLevel, fPower, fVerbose);
     Vec_PtrPush( vAigs, pAig );
 //Aig_ManPrintStats( pAig );
 
-    Aig_ManForEachObj( pAig, pObj, i )
-    {
-        pObj->pNext = pObj->pHaig;
-        pObj->pHaig = pObj;
-    }
-
     pAig = Dar_ManCompress2(pAig, fBalance, fUpdateLevel, 1, fPower, fVerbose);
     Vec_PtrPush( vAigs, pAig );
 //Aig_ManPrintStats( pAig );
 
     pAig = (Aig_Man_t *)Vec_PtrEntry( vAigs, 1 );
-    Aig_ManForEachObj( pAig, pObj, i )
-        pObj->pHaig = pObj->pNext;
-
     return vAigs;
 }
 
diff --git a/src/proof/fra/fraLcr.c b/src/proof/fra/fraLcr.c
index 2941f24f..9d573bee 100644
--- a/src/proof/fra/fraLcr.c
+++ b/src/proof/fra/fraLcr.c
@@ -273,7 +273,6 @@ Aig_Obj_t * Fra_LcrManDup_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj
         return (Aig_Obj_t *)(pObj->pData = Aig_ObjChild0Copy(pObj));
     Fra_LcrManDup_rec( pNew, p, Aig_ObjFanin1(pObj) );
     pObjNew = Aig_Oper( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj), Aig_ObjType(pObj) );
-    Aig_Regular(pObjNew)->pHaig = pObj->pHaig;
     return (Aig_Obj_t *)(pObj->pData = pObjNew);
 }