Version abc70930

16 files changed, 0 insertions, 6314 deletions

diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
deleted file mode 100644
index 210af244..00000000
--- a/src/aig/fra/fra.h
+++ /dev/null
@@ -1,300 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fra.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [[New FRAIG package.]
-
-  Synopsis    [External declarations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fra.h,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#ifndef __FRA_H__
-#define __FRA_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif 
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-#include <stdio.h>
-#include <stdlib.h>
-#include <string.h>
-#include <assert.h>
-#include <time.h>
-
-#include "vec.h"
-#include "aig.h"
-#include "dar.h"
-#include "satSolver.h"
-#include "bar.h"
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Fra_Par_t_   Fra_Par_t;
-typedef struct Fra_Man_t_   Fra_Man_t;
-typedef struct Fra_Cla_t_   Fra_Cla_t;
-typedef struct Fra_Sml_t_   Fra_Sml_t;
-typedef struct Fra_Bmc_t_   Fra_Bmc_t;
-
-// FRAIG parameters
-struct Fra_Par_t_
-{
-    int              nSimWords;         // the number of words in the simulation info
-    double           dSimSatur;         // the ratio of refined classes when saturation is reached
-    int              fPatScores;        // enables simulation pattern scoring
-    int              MaxScore;          // max score after which resimulation is used
-    double           dActConeRatio;     // the ratio of cone to be bumped
-    double           dActConeBumpMax;   // the largest bump in activity
-    int              fChoicing;         // enables choicing
-    int              fSpeculate;        // use speculative reduction
-    int              fProve;            // prove the miter outputs
-    int              fVerbose;          // verbose output
-    int              fDoSparse;         // skip sparse functions
-    int              fConeBias;         // bias variables in the cone (good for unsat runs)
-    int              nBTLimitNode;      // conflict limit at a node
-    int              nBTLimitMiter;     // conflict limit at an output
-    int              nFramesP;          // the number of timeframes to in the prefix
-    int              nFramesK;          // the number of timeframes to unroll
-    int              nMaxImps;          // the maximum number of implications to consider
-    int              fRewrite;          // use rewriting for constraint reduction
-    int              fLatchCorr;        // computes latch correspondence only
-    int              fUseImps;          // use implications
-    int              fWriteImps;        // record implications
-};
-
-// FRAIG equivalence classes
-struct Fra_Cla_t_
-{
-    Aig_Man_t *      pAig;              // the original AIG manager
-    Aig_Obj_t **     pMemRepr;          // pointers to representatives of each node
-    Vec_Ptr_t *      vClasses;          // equivalence classes
-    Vec_Ptr_t *      vClasses1;         // equivalence class of Const1 node
-    Vec_Ptr_t *      vClassesTemp;      // temporary storage for new classes
-    Aig_Obj_t **     pMemClasses;       // memory allocated for equivalence classes
-    Aig_Obj_t **     pMemClassesFree;   // memory allocated for equivalence classes to be used
-    Vec_Ptr_t *      vClassOld;         // old equivalence class after splitting
-    Vec_Ptr_t *      vClassNew;         // new equivalence class(es) after splitting
-    int              nPairs;            // the number of pairs of nodes
-    int              fRefinement;       // set to 1 when refinement has happened
-    Vec_Int_t *      vImps;             // implications
-    // procedures used for class refinement
-    int (*pFuncNodeHash)     (Aig_Obj_t *, int);         // returns has key of the node
-    int (*pFuncNodeIsConst)  (Aig_Obj_t *);              // returns 1 if the node is a constant
-    int (*pFuncNodesAreEqual)(Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement
-};
-
-// simulation manager
-struct Fra_Sml_t_
-{
-    Aig_Man_t *      pAig;              // the original AIG manager
-    int              nPref;             // the number of times frames in the prefix
-    int              nFrames;           // the number of times frames 
-    int              nWordsFrame;       // the number of words in each time frame
-    int              nWordsTotal;       // the total number of words at a node
-    int              nWordsPref;        // the number of word in the prefix
-    int              fNonConstOut;      // have seen a non-const-0 output during simulation
-    int              nSimRounds;        // statistics
-    int              timeSim;           // statistics
-    unsigned         pData[0];          // simulation data for the nodes
-};
-
-// FRAIG manager
-struct Fra_Man_t_
-{
-    // high-level data    
-    Fra_Par_t *      pPars;             // parameters governing fraiging
-    // AIG managers
-    Aig_Man_t *      pManAig;           // the starting AIG manager
-    Aig_Man_t *      pManFraig;         // the final AIG manager
-    // mapping AIG into FRAIG
-    int              nFramesAll;        // the number of timeframes used
-    Aig_Obj_t **     pMemFraig;         // memory allocated for points to the fraig nodes
-    int              nSizeAlloc;        // allocated size of the arrays for timeframe nodes
-    // equivalence classes 
-    Fra_Cla_t *      pCla;              // representation of (candidate) equivalent nodes
-    // simulation info
-    Fra_Sml_t *      pSml;              // simulation manager
-    // bounded model checking manager
-    Fra_Bmc_t *      pBmc;
-    // counter example storage
-    int              nPatWords;         // the number of words in the counter example
-    unsigned *       pPatWords;         // the counter example
-    Vec_Int_t *      vCex;
-    // satisfiability solving
-    sat_solver *     pSat;              // SAT solver
-    int              nSatVars;          // the number of variables currently used
-    Vec_Ptr_t *      vPiVars;           // the PIs of the cone used 
-    sint64           nBTLimitGlobal;    // resource limit
-    sint64           nInsLimitGlobal;   // resource limit
-    Vec_Ptr_t **     pMemFanins;        // the arrays of fanins for some FRAIG nodes
-    int *            pMemSatNums;       // the array of SAT numbers for some FRAIG nodes
-    int              nMemAlloc;         // allocated size of the arrays for FRAIG varnums and fanins
-    Vec_Ptr_t *      vTimeouts;         // the nodes, for which equivalence checking timed out
-    // statistics
-    int              nSimRounds;
-    int              nNodesMiter;
-    int              nLitsBeg;
-    int              nLitsEnd;
-    int              nNodesBeg;
-    int              nNodesEnd;
-    int              nRegsBeg;
-    int              nRegsEnd;
-    int              nSatCalls;
-    int              nSatCallsSat;
-    int              nSatCallsUnsat;
-    int              nSatProof;
-    int              nSatFails;
-    int              nSatFailsReal;
-    int              nSpeculs;   
-    int              nChoices;
-    int              nChoicesFake;
-    int              nSatCallsRecent;
-    int              nSatCallsSkipped;
-    // runtime
-    int              timeSim;
-    int              timeTrav;
-    int              timeRwr;
-    int              timeSat;
-    int              timeSatUnsat;
-    int              timeSatSat;
-    int              timeSatFail;
-    int              timeRef;
-    int              timeTotal;
-    int              time1;
-    int              time2;
-};
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-static inline unsigned *   Fra_ObjSim( Fra_Sml_t * p, int Id )                           { return p->pData + p->nWordsTotal * Id; }
-static inline unsigned     Fra_ObjRandomSim()                                            { return (rand() << 24) ^ (rand() << 12) ^ rand();                                                   }
-
-static inline Aig_Obj_t *  Fra_ObjFraig( Aig_Obj_t * pObj, int i )                       { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i];  }
-static inline void         Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i] = pNode; }
-
-static inline Vec_Ptr_t *  Fra_ObjFaninVec( Aig_Obj_t * pObj )                           { return ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id];      }
-static inline void         Fra_ObjSetFaninVec( Aig_Obj_t * pObj, Vec_Ptr_t * vFanins )   { ((Fra_Man_t *)pObj->pData)->pMemFanins[pObj->Id] = vFanins;   }
-
-static inline int          Fra_ObjSatNum( Aig_Obj_t * pObj )                             { return ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id];     }
-static inline void         Fra_ObjSetSatNum( Aig_Obj_t * pObj, int Num )                 { ((Fra_Man_t *)pObj->pData)->pMemSatNums[pObj->Id] = Num;      }
-
-static inline Aig_Obj_t *  Fra_ClassObjRepr( Aig_Obj_t * pObj )                          { return ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id];  }
-static inline void         Fra_ClassObjSetRepr( Aig_Obj_t * pObj, Aig_Obj_t * pNode )    { ((Fra_Man_t *)pObj->pData)->pCla->pMemRepr[pObj->Id] = pNode; }
-
-static inline Aig_Obj_t *  Fra_ObjChild0Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL;  }
-static inline Aig_Obj_t *  Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Fra_ObjFraig(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL;  }
-
-static inline int          Fra_ImpLeft( int Imp )                                        { return Imp & 0xFFFF;         }
-static inline int          Fra_ImpRight( int Imp )                                       { return Imp >> 16;            }
-static inline int          Fra_ImpCreate( int Left, int Right )                          { return (Right << 16) | Left; }
-
-////////////////////////////////////////////////////////////////////////
-///                         ITERATORS                                ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                    FUNCTION DECLARATIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== fraClass.c ========================================================*/
-extern int                 Fra_BmcNodeIsConst( Aig_Obj_t * pObj );
-extern int                 Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
-extern void                Fra_BmcStop( Fra_Bmc_t * p );
-extern void                Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth );
-/*=== fraClass.c ========================================================*/
-extern Fra_Cla_t *         Fra_ClassesStart( Aig_Man_t * pAig );
-extern void                Fra_ClassesStop( Fra_Cla_t * p );
-extern void                Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
-extern void                Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose );
-extern void                Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr );
-extern int                 Fra_ClassesRefine( Fra_Cla_t * p );
-extern int                 Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped );
-extern int                 Fra_ClassesCountLits( Fra_Cla_t * p );
-extern int                 Fra_ClassesCountPairs( Fra_Cla_t * p );
-extern void                Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
-extern void                Fra_ClassesLatchCorr( Fra_Man_t * p );
-extern void                Fra_ClassesPostprocess( Fra_Cla_t * p );
-extern void                Fra_ClassesSelectRepr( Fra_Cla_t * p );
-extern Aig_Man_t *         Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK );
-/*=== fraCnf.c ========================================================*/
-extern void                Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
-/*=== fraCore.c ========================================================*/
-extern void                Fra_FraigSweep( Fra_Man_t * pManAig );
-extern int                 Fra_FraigMiterStatus( Aig_Man_t * p );
-extern Aig_Man_t *         Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
-extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax );
-extern Aig_Man_t *         Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax );
-/*=== fraImp.c ========================================================*/
-extern Vec_Int_t *         Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
-extern void                Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums );
-extern int                 Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos );
-extern int                 Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps );
-extern void                Fra_ImpCompactArray( Vec_Int_t * vImps );
-extern double              Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p );
-extern int                 Fra_ImpVerifyUsingSimulation( Fra_Man_t * p );
-extern void                Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew );
-/*=== fraInd.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter );
-/*=== fraLcr.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter );
-/*=== fraMan.c ========================================================*/
-extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
-extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
-extern Fra_Man_t *         Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pParams );
-extern void                Fra_ManClean( Fra_Man_t * p, int nNodesMax );
-extern Aig_Man_t *         Fra_ManPrepareComb( Fra_Man_t * p );
-extern void                Fra_ManFinalizeComb( Fra_Man_t * p );
-extern void                Fra_ManStop( Fra_Man_t * p );
-extern void                Fra_ManPrint( Fra_Man_t * p );
-/*=== fraSat.c ========================================================*/
-extern int                 Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
-extern int                 Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
-extern int                 Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
-/*=== fraSec.c ========================================================*/
-extern int                 Fra_FraigSec( Aig_Man_t * p, int nFrames, int fRetimeFirst, int fVerbose, int fVeryVerbose );
-/*=== fraSim.c ========================================================*/
-extern int                 Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
-extern int                 Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
-extern int                 Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
-extern int                 Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right );
-extern int                 Fra_SmlCheckOutput( Fra_Man_t * p );
-extern void                Fra_SmlSavePattern( Fra_Man_t * p );
-extern void                Fra_SmlSimulate( Fra_Man_t * p, int fInit );
-extern void                Fra_SmlResimulate( Fra_Man_t * p );
-extern Fra_Sml_t *         Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
-extern void                Fra_SmlStop( Fra_Sml_t * p );
-extern Fra_Sml_t *         Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
-extern Fra_Sml_t *         Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
-
-
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c
deleted file mode 100644
index 1140f3a4..00000000
--- a/src/aig/fra/fraBmc.c
+++ /dev/null
@@ -1,362 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraBmc.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [New FRAIG package.]
-
-  Synopsis    [Bounded model checking.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fraBmc.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-// simulation manager
-struct Fra_Bmc_t_
-{
-    // parameters
-    int              nPref;             // the size of the prefix
-    int              nDepth;            // the depth of the frames
-    int              nFramesAll;        // the total number of timeframes
-    // implications to be filtered
-    Vec_Int_t *      vImps;
-    // AIG managers
-    Aig_Man_t *      pAig;              // the original AIG manager
-    Aig_Man_t *      pAigFrames;        // initialized timeframes
-    Aig_Man_t *      pAigFraig;         // the fraiged initialized timeframes
-    // mapping of nodes
-    Aig_Obj_t **     pObjToFrames;      // mapping of the original node into frames
-    Aig_Obj_t **     pObjToFraig;       // mapping of the frames node into fraig
-};
-
-static inline Aig_Obj_t *  Bmc_ObjFrames( Aig_Obj_t * pObj, int i )                       { return ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFrames[((Fra_Man_t *)pObj->pData)->pBmc->nFramesAll*pObj->Id + i];  }
-static inline void         Bmc_ObjSetFrames( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFrames[((Fra_Man_t *)pObj->pData)->pBmc->nFramesAll*pObj->Id + i] = pNode; }
-
-static inline Aig_Obj_t *  Bmc_ObjFraig( Aig_Obj_t * pObj )                               { return ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFraig[pObj->Id];  }
-static inline void         Bmc_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode )         { ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFraig[pObj->Id] = pNode; }
-
-static inline Aig_Obj_t *  Bmc_ObjChild0Frames( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Bmc_ObjFrames(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL;  }
-static inline Aig_Obj_t *  Bmc_ObjChild1Frames( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Bmc_ObjFrames(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL;  }
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the nodes are equivalent.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
-{
-    Fra_Man_t * p = pObj0->pData;
-    Aig_Obj_t * pObjFrames0, * pObjFrames1;
-    Aig_Obj_t * pObjFraig0, * pObjFraig1;
-    int i;
-    for ( i = p->pBmc->nPref; i < p->pBmc->nFramesAll; i++ )
-    {
-        pObjFrames0 = Aig_Regular( Bmc_ObjFrames(pObj0, i) );
-        pObjFrames1 = Aig_Regular( Bmc_ObjFrames(pObj1, i) );
-        if ( pObjFrames0 == pObjFrames1 )
-            continue;
-        pObjFraig0 = Aig_Regular( Bmc_ObjFraig(pObjFrames0) );
-        pObjFraig1 = Aig_Regular( Bmc_ObjFraig(pObjFrames1) );
-        if ( pObjFraig0 != pObjFraig1 )
-            return 0;
-    }
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the node is costant.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_BmcNodeIsConst( Aig_Obj_t * pObj )
-{
-    Fra_Man_t * p = pObj->pData;
-    return Fra_BmcNodesAreEqual( pObj, Aig_ManConst1(p->pManAig) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Refines implications using BMC.]
-
-  Description [The input is the combinational FRAIG manager,
-  which is used to FRAIG the timeframes. ]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_BmcFilterImplications( Fra_Man_t * p, Fra_Bmc_t * pBmc )
-{
-    Aig_Obj_t * pLeft, * pRight;
-    Aig_Obj_t * pLeftT, * pRightT;
-    Aig_Obj_t * pLeftF, * pRightF;
-    int i, f, Imp, Left, Right;
-    int fComplL, fComplR;
-    assert( p->nFramesAll == 1 );
-    assert( p->pManAig == pBmc->pAigFrames );
-    Vec_IntForEachEntry( pBmc->vImps, Imp, i )
-    {
-        if ( Imp == 0 )
-            continue;
-        Left  = Fra_ImpLeft(Imp);
-        Right = Fra_ImpRight(Imp);
-        // get the corresponding nodes
-        pLeft  = Aig_ManObj( pBmc->pAig, Left );
-        pRight = Aig_ManObj( pBmc->pAig, Right );
-        // iterate through the timeframes
-        for ( f = pBmc->nPref; f < pBmc->nFramesAll; f++ )
-        {
-            // get timeframe nodes
-            pLeftT  = Bmc_ObjFrames( pLeft, f );
-            pRightT = Bmc_ObjFrames( pRight, f );
-            // get the corresponding FRAIG nodes
-            pLeftF  = Fra_ObjFraig( Aig_Regular(pLeftT), 0 );
-            pRightF = Fra_ObjFraig( Aig_Regular(pRightT), 0 );
-            // get the complemented attributes
-            fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF) ^ Aig_IsComplement(pLeftT);
-            fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF) ^ Aig_IsComplement(pRightT);
-            // check equality
-            if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
-            {
-                if ( fComplL == fComplR ) // x => x  - always true
-                    continue;
-                assert( fComplL != fComplR );
-                // consider 4 possibilities:
-                // NOT(1) => 1    or   0 => 1  - always true
-                // 1 => NOT(1)    or   1 => 0  - never true
-                // NOT(x) => x    or   x       - not always true
-                // x => NOT(x)    or   NOT(x)  - not always true
-                if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
-                    continue;
-                // disproved implication
-                Vec_IntWriteEntry( pBmc->vImps, i, 0 ); 
-                break;
-            }
-            // check the implication 
-            if ( Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR ) != 1 )
-            {
-                Vec_IntWriteEntry( pBmc->vImps, i, 0 );
-                break;
-            }
-        }
-    }
-    Fra_ImpCompactArray( pBmc->vImps );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the BMC manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fra_Bmc_t * Fra_BmcStart( Aig_Man_t * pAig, int nPref, int nDepth )
-{
-    Fra_Bmc_t * p;
-    p = ALLOC( Fra_Bmc_t, 1 );
-    memset( p, 0, sizeof(Fra_Bmc_t) );
-    p->pAig = pAig;
-    p->nPref = nPref;
-    p->nDepth = nDepth;
-    p->nFramesAll = nPref + nDepth;
-    p->pObjToFrames  = ALLOC( Aig_Obj_t *, p->nFramesAll * Aig_ManObjNumMax(pAig) );
-    memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * Aig_ManObjNumMax(pAig) );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the BMC manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_BmcStop( Fra_Bmc_t * p )
-{
-    Aig_ManStop( p->pAigFrames );
-    Aig_ManStop( p->pAigFraig );
-    free( p->pObjToFrames );
-    free( p->pObjToFraig );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Constructs initialized timeframes of the AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p )
-{
-    Aig_Man_t * pAigFrames;
-    Aig_Obj_t * pObj, * pObjNew;
-    Aig_Obj_t ** pLatches;
-    int i, k, f;
-
-    // start the fraig package
-    pAigFrames = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * p->nFramesAll );
-    pAigFrames->pName = Aig_UtilStrsav( p->pAig->pName );
-    // create PI nodes for the frames
-    for ( f = 0; f < p->nFramesAll; f++ )
-        Bmc_ObjSetFrames( Aig_ManConst1(p->pAig), f, Aig_ManConst1(pAigFrames) );
-    for ( f = 0; f < p->nFramesAll; f++ )
-        Aig_ManForEachPiSeq( p->pAig, pObj, i )
-            Bmc_ObjSetFrames( pObj, f, Aig_ObjCreatePi(pAigFrames) );
-    // set initial state for the latches
-    Aig_ManForEachLoSeq( p->pAig, pObj, i )
-        Bmc_ObjSetFrames( pObj, 0, Aig_ManConst0(pAigFrames) );
-
-    // add timeframes
-    pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
-    for ( f = 0; f < p->nFramesAll; f++ )
-    {
-        // add internal nodes of this frame
-        Aig_ManForEachNode( p->pAig, pObj, i )
-        {
-            pObjNew = Aig_And( pAigFrames, Bmc_ObjChild0Frames(pObj,f), Bmc_ObjChild1Frames(pObj,f) );
-            Bmc_ObjSetFrames( pObj, f, pObjNew );
-        }
-        if ( f == p->nFramesAll - 1 )
-            break;
-        // save the latch input values
-        k = 0;
-        Aig_ManForEachLiSeq( p->pAig, pObj, i )
-            pLatches[k++] = Bmc_ObjChild0Frames(pObj,f);
-        assert( k == Aig_ManRegNum(p->pAig) );
-        // insert them to the latch output values
-        k = 0;
-        Aig_ManForEachLoSeq( p->pAig, pObj, i )
-            Bmc_ObjSetFrames( pObj, f+1, pLatches[k++] );
-        assert( k == Aig_ManRegNum(p->pAig) );
-    }
-    free( pLatches );
-    // add POs to all the dangling nodes
-    Aig_ManForEachObj( pAigFrames, pObjNew, i )
-        if ( Aig_ObjIsNode(pObjNew) && pObjNew->nRefs == 0 )
-            Aig_ObjCreatePo( pAigFrames, pObjNew );
-
-    // return the new manager
-    return pAigFrames;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BMC for the given AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
-{
-    Aig_Obj_t * pObj;
-    int i, nImpsOld, clk = clock();
-    assert( p->pBmc == NULL );
-    // derive and fraig the frames
-    p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth );
-    p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc );
-    // if implications are present, configure the AIG manager to check them
-    if ( p->pCla->vImps )
-    {
-        p->pBmc->pAigFrames->pImpFunc = Fra_BmcFilterImplications;
-        p->pBmc->pAigFrames->pImpData = p->pBmc;
-        p->pBmc->vImps = p->pCla->vImps;
-        nImpsOld = Vec_IntSize(p->pCla->vImps);
-    } 
-    p->pBmc->pAigFraig = Fra_FraigEquivence( p->pBmc->pAigFrames, 1000000 );
-    p->pBmc->pObjToFraig = p->pBmc->pAigFrames->pObjCopies;
-    p->pBmc->pAigFrames->pObjCopies = NULL;
-    // annotate frames nodes with pointers to the manager
-    Aig_ManForEachObj( p->pBmc->pAigFrames, pObj, i )
-        pObj->pData = p;
-    // report the results
-    if ( p->pPars->fVerbose )
-    {
-        printf( "Original AIG = %d. Init %d frames = %d. Fraig = %d.  ", 
-            Aig_ManNodeNum(p->pBmc->pAig), p->pBmc->nFramesAll, 
-            Aig_ManNodeNum(p->pBmc->pAigFrames), Aig_ManNodeNum(p->pBmc->pAigFraig) );
-        PRT( "Time", clock() - clk );
-        printf( "Before BMC: " );  
-//        Fra_ClassesPrint( p->pCla, 0 );
-        printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
-            Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
-        if ( p->pCla->vImps )
-            printf( "Imp = %5d. ", nImpsOld );
-        printf( "\n" );
-    }
-    // refine the classes
-    p->pCla->pFuncNodeIsConst   = Fra_BmcNodeIsConst;
-    p->pCla->pFuncNodesAreEqual = Fra_BmcNodesAreEqual;
-    Fra_ClassesRefine( p->pCla );
-    Fra_ClassesRefine1( p->pCla, 1, NULL );
-    p->pCla->pFuncNodeIsConst   = Fra_SmlNodeIsConst;
-    p->pCla->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
-    // report the results
-    if ( p->pPars->fVerbose )
-    {
-        printf( "After  BMC: " );  
-//        Fra_ClassesPrint( p->pCla, 0 );
-        printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
-            Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
-        if ( p->pCla->vImps )
-            printf( "Imp = %5d. ", Vec_IntSize(p->pCla->vImps) );
-        printf( "\n" );
-    }
-    // free the BMC manager
-    Fra_BmcStop( p->pBmc );  
-    p->pBmc = NULL;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/fra/fraCec.c b/src/aig/fra/fraCec.c
deleted file mode 100644
index e705f4fc..00000000
--- a/src/aig/fra/fraCec.c
+++ /dev/null
@@ -1,48 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraCec.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [New FRAIG package.]
-
-  Synopsis    [CEC engined based on fraiging.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fraCec.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
deleted file mode 100644
index a03fa6e5..00000000
--- a/src/aig/fra/fraClass.c
+++ /dev/null
@@ -1,854 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraClass.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [New FRAIG package.]
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fraClass.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fra.h"
-
-/*
-    The candidate equivalence classes are stored as a vector of pointers 
-    to the array of pointers to the nodes in each class.
-    The first node of the class is its representative node.
-    The representative has the smallest topological order among the class nodes.
-    The nodes inside each class are ordered according to their topological order.
-    The classes are ordered according to the topological order of their representatives.
-    The array of pointers to the class nodes is terminated with a NULL pointer.
-    To enable dynamic addition of new classes (during class refinement),
-    each array has at least as many NULLs in the end, as there are nodes in the class.
-*/
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static inline Aig_Obj_t *  Fra_ObjNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj )                       { return ppNexts[pObj->Id];  }
-static inline void         Fra_ObjSetNext( Aig_Obj_t ** ppNexts, Aig_Obj_t * pObj, Aig_Obj_t * pNext ) { ppNexts[pObj->Id] = pNext; }
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Starts representation of equivalence classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
-{
-    Fra_Cla_t * p;
-    p = ALLOC( Fra_Cla_t, 1 );
-    memset( p, 0, sizeof(Fra_Cla_t) );
-    p->pAig = pAig;
-    p->pMemRepr  = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(pAig) );
-    memset( p->pMemRepr, 0, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(pAig) );
-    p->vClasses     = Vec_PtrAlloc( 100 );
-    p->vClasses1    = Vec_PtrAlloc( 100 );
-    p->vClassesTemp = Vec_PtrAlloc( 100 );
-    p->vClassOld    = Vec_PtrAlloc( 100 );
-    p->vClassNew    = Vec_PtrAlloc( 100 );
-    p->pFuncNodeHash      = Fra_SmlNodeHash;
-    p->pFuncNodeIsConst   = Fra_SmlNodeIsConst;
-    p->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Stop representation of equivalence classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClassesStop( Fra_Cla_t * p )
-{
-    FREE( p->pMemClasses );
-    FREE( p->pMemRepr );
-    if ( p->vClassesTemp ) Vec_PtrFree( p->vClassesTemp );
-    if ( p->vClassNew )    Vec_PtrFree( p->vClassNew );
-    if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
-    if ( p->vClasses1 )    Vec_PtrFree( p->vClasses1 );
-    if ( p->vClasses )     Vec_PtrFree( p->vClasses );
-    if ( p->vImps )        Vec_IntFree( p->vImps );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Starts representation of equivalence classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    Aig_ManReprStart( p->pAig, Aig_ManObjNumMax(p->pAig) );
-    memmove( p->pAig->pReprs, p->pMemRepr, sizeof(Aig_Obj_t *) * Aig_ManObjNumMax(p->pAig) );
-    if ( Vec_PtrSize(p->vClasses1) == 0 && Vec_PtrSize(p->vClasses) == 0 )
-    {
-        Aig_ManForEachObj( p->pAig, pObj, i )
-        {
-            if ( p->pAig->pReprs[i] != NULL )
-                printf( "Classes are not cleared!\n" );
-            assert( p->pAig->pReprs[i] == NULL );
-        }
-    }
-    if ( vFailed )
-        Vec_PtrForEachEntry( vFailed, pObj, i )
-            p->pAig->pReprs[pObj->Id] = NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints simulation classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ClassCount( Aig_Obj_t ** pClass )
-{
-    Aig_Obj_t * pTemp;
-    int i;
-    for ( i = 0; pTemp = pClass[i]; i++ );
-    return i;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Count the number of literals.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ClassesCountLits( Fra_Cla_t * p )
-{
-    Aig_Obj_t ** pClass;
-    int i, nNodes, nLits = 0;
-    nLits = Vec_PtrSize( p->vClasses1 );
-    Vec_PtrForEachEntry( p->vClasses, pClass, i )
-    {
-        nNodes = Fra_ClassCount( pClass );
-        assert( nNodes > 1 );
-        nLits += nNodes - 1;
-    }
-    return nLits;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Count the number of pairs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ClassesCountPairs( Fra_Cla_t * p )
-{
-    Aig_Obj_t ** pClass;
-    int i, nNodes, nPairs = 0;
-    Vec_PtrForEachEntry( p->vClasses, pClass, i )
-    {
-        nNodes = Fra_ClassCount( pClass );
-        assert( nNodes > 1 );
-        nPairs += nNodes * (nNodes - 1) / 2;
-    }
-    return nPairs;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints simulation classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_PrintClass( Aig_Obj_t ** pClass )
-{
-    Aig_Obj_t * pTemp;
-    int i;
-    for ( i = 1; pTemp = pClass[i]; i++ )
-        assert( Fra_ClassObjRepr(pTemp) == pClass[0] );
-    printf( "{ " );
-    for ( i = 0; pTemp = pClass[i]; i++ )
-        printf( "%d(%d) ", pTemp->Id, pTemp->Level );
-    printf( "}\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints simulation classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
-{
-    Aig_Obj_t ** pClass;
-    Aig_Obj_t * pObj;
-    int i;
-
-    printf( "Const = %5d. Class = %5d. Lit = %5d. ", 
-        Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) );
-    if ( p->vImps && Vec_IntSize(p->vImps) > 0 )
-        printf( "Imp = %5d. ", Vec_IntSize(p->vImps) );
-    printf( "\n" );
-
-    if ( fVeryVerbose )
-    {
-        Vec_PtrForEachEntry( p->vClasses1, pObj, i )
-            assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) );
-        printf( "Constants { " );
-        Vec_PtrForEachEntry( p->vClasses1, pObj, i )
-            printf( "%d ", pObj->Id );
-        printf( "}\n" );
-        Vec_PtrForEachEntry( p->vClasses, pClass, i )
-        {
-            printf( "%3d (%3d) : ", i, Fra_ClassCount(pClass) );
-            Fra_PrintClass( pClass );
-        }
-        printf( "\n" );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates initial simulation classes.]
-
-  Description [Assumes that simulation info is assigned.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
-{
-    Aig_Obj_t ** ppTable, ** ppNexts;
-    Aig_Obj_t * pObj, * pTemp;
-    int i, k, nTableSize, nEntries, nNodes, iEntry;
-
-    // allocate the hash table hashing simulation info into nodes
-    nTableSize = Aig_PrimeCudd( Aig_ManObjNumMax(p->pAig) );
-    ppTable = ALLOC( Aig_Obj_t *, nTableSize ); 
-    ppNexts = ALLOC( Aig_Obj_t *, nTableSize ); 
-    memset( ppTable, 0, sizeof(Aig_Obj_t *) * nTableSize );
-
-    // add all the nodes to the hash table
-    Vec_PtrClear( p->vClasses1 );
-    Aig_ManForEachObj( p->pAig, pObj, i )
-    {
-        if ( fLatchCorr )
-        {
-            if ( !Aig_ObjIsPi(pObj) )
-                continue;
-        }
-        else
-        {
-            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
-                continue;
-            // skip the node with more that the given number of levels
-//            if ( pObj->Level > 3 )
-//                continue;
-        }
-        // hash the node by its simulation info
-        iEntry = p->pFuncNodeHash( pObj, nTableSize );
-        // check if the node belongs to the class of constant 1
-        if ( p->pFuncNodeIsConst( pObj ) )
-        {
-            Vec_PtrPush( p->vClasses1, pObj );
-            Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pAig) );
-            continue;
-        }
-        // add the node to the class
-        if ( ppTable[iEntry] == NULL )
-        {
-            ppTable[iEntry] = pObj;
-            Fra_ObjSetNext( ppNexts, pObj, pObj );
-        }
-        else
-        {
-            Fra_ObjSetNext( ppNexts, pObj, Fra_ObjNext(ppNexts,ppTable[iEntry]) );
-            Fra_ObjSetNext( ppNexts, ppTable[iEntry], pObj );
-        }
-    }
-
-    // count the total number of nodes in the non-trivial classes
-    // mark the representative nodes of each equivalence class
-    nEntries = 0;
-    for ( i = 0; i < nTableSize; i++ )
-        if ( ppTable[i] && ppTable[i] != Fra_ObjNext(ppNexts, ppTable[i]) )
-        {
-            for ( pTemp = Fra_ObjNext(ppNexts, ppTable[i]), k = 1; 
-                  pTemp != ppTable[i]; 
-                  pTemp = Fra_ObjNext(ppNexts, pTemp), k++ );
-            assert( k > 1 );
-            nEntries += k;
-            // mark the node
-            assert( ppTable[i]->fMarkA == 0 );
-            ppTable[i]->fMarkA = 1;
-        }
-
-    // allocate room for classes
-    p->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->vClasses1)) );
-    p->pMemClassesFree = p->pMemClasses + 2*nEntries;
- 
-    // copy the entries into storage in the topological order
-    Vec_PtrClear( p->vClasses );
-    nEntries = 0;
-    Aig_ManForEachObj( p->pAig, pObj, i )
-    {
-        if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
-            continue;
-        // skip the nodes that are not representatives of non-trivial classes
-        if ( pObj->fMarkA == 0 )
-            continue;
-        pObj->fMarkA = 0;
-        // add the class of nodes
-        Vec_PtrPush( p->vClasses, p->pMemClasses + 2*nEntries );
-        // count the number of entries in this class
-        for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; 
-              pTemp != pObj; 
-              pTemp = Fra_ObjNext(ppNexts, pTemp), k++ );
-        nNodes = k;
-        assert( nNodes > 1 );
-        // add the nodes to the class in the topological order
-        p->pMemClasses[2*nEntries] = pObj;
-        for ( pTemp = Fra_ObjNext(ppNexts, pObj), k = 1; 
-              pTemp != pObj; 
-              pTemp = Fra_ObjNext(ppNexts, pTemp), k++ )
-        {
-            p->pMemClasses[2*nEntries+nNodes-k] = pTemp;
-            Fra_ClassObjSetRepr( pTemp, pObj );
-        }
-        // add as many empty entries
-        p->pMemClasses[2*nEntries + nNodes] = NULL;
-        // increment the number of entries
-        nEntries += k;
-    }
-    free( ppTable );
-    free( ppNexts );
-    // now it is time to refine the classes
-    Fra_ClassesRefine( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Refines one class using simulation info.]
-
-  Description [Returns the new class if refinement happened.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t ** Fra_RefineClassOne( Fra_Cla_t * p, Aig_Obj_t ** ppClass )
-{
-    Aig_Obj_t * pObj, ** ppThis;
-    int i;
-    assert( ppClass[0] != NULL && ppClass[1] != NULL );
-
-    // check if the class is going to be refined
-    for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )        
-        if ( !p->pFuncNodesAreEqual(ppClass[0], pObj) )
-            break;
-    if ( pObj == NULL )
-        return NULL;
-    // split the class
-    Vec_PtrClear( p->vClassOld );
-    Vec_PtrClear( p->vClassNew );
-    Vec_PtrPush( p->vClassOld, ppClass[0] );
-    for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )        
-        if ( p->pFuncNodesAreEqual(ppClass[0], pObj) )
-            Vec_PtrPush( p->vClassOld, pObj );
-        else
-            Vec_PtrPush( p->vClassNew, pObj );
-/*
-    printf( "Refining class (" );
-    Vec_PtrForEachEntry( p->vClassOld, pObj, i )
-        printf( "%d,", pObj->Id );
-    printf( ") + (" );
-    Vec_PtrForEachEntry( p->vClassNew, pObj, i )
-        printf( "%d,", pObj->Id );
-    printf( ")\n" );
-*/
-    // put the nodes back into the class memory
-    Vec_PtrForEachEntry( p->vClassOld, pObj, i )
-    {
-        ppClass[i] = pObj;
-        ppClass[Vec_PtrSize(p->vClassOld)+i] = NULL;
-        Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
-    }
-    ppClass += 2*Vec_PtrSize(p->vClassOld);
-    // put the new nodes into the class memory
-    Vec_PtrForEachEntry( p->vClassNew, pObj, i )
-    {
-        ppClass[i] = pObj;
-        ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
-        Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
-    }
-    return ppClass;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Iteratively refines the classes after simulation.]
-
-  Description [Returns the number of refinements performed.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_RefineClassLastIter( Fra_Cla_t * p, Vec_Ptr_t * vClasses )
-{
-    Aig_Obj_t ** pClass, ** pClass2;
-    int nRefis;
-    pClass = Vec_PtrEntryLast( vClasses );
-    for ( nRefis = 0; pClass2 = Fra_RefineClassOne( p, pClass ); nRefis++ )
-    {
-        // if the original class is trivial, remove it
-        if ( pClass[1] == NULL )
-            Vec_PtrPop( vClasses );
-        // if the new class is trivial, stop
-        if ( pClass2[1] == NULL )
-        {
-            nRefis++;
-            break;
-        }
-        // othewise, add the class and continue
-        assert( pClass2[0] != NULL );
-        Vec_PtrPush( vClasses, pClass2 );
-        pClass = pClass2;
-    }
-    return nRefis;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Refines the classes after simulation.]
-
-  Description [Assumes that simulation info is assigned. Returns the
-  number of classes refined.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ClassesRefine( Fra_Cla_t * p )
-{
-    Vec_Ptr_t * vTemp;
-    Aig_Obj_t ** pClass;
-    int i, nRefis;
-    // refine the classes
-    nRefis = 0;
-    Vec_PtrClear( p->vClassesTemp );
-    Vec_PtrForEachEntry( p->vClasses, pClass, i )
-    {
-        // add the class to the new array
-        assert( pClass[0] != NULL );
-        Vec_PtrPush( p->vClassesTemp, pClass );
-        // refine the class iteratively
-        nRefis += Fra_RefineClassLastIter( p, p->vClassesTemp );
-    }
-    // exchange the class representation
-    vTemp = p->vClassesTemp;
-    p->vClassesTemp = p->vClasses;
-    p->vClasses = vTemp;
-    return nRefis;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Refines constant 1 equivalence class.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ClassesRefine1( Fra_Cla_t * p, int fRefineNewClass, int * pSkipped )
-{
-    Aig_Obj_t * pObj, ** ppClass;
-    int i, k, nRefis = 1;
-    // check if there is anything to refine
-    if ( Vec_PtrSize(p->vClasses1) == 0 )
-        return 0;
-    // make sure constant 1 class contains only non-constant nodes
-    assert( Vec_PtrEntry(p->vClasses1,0) != Aig_ManConst1(p->pAig) );
-    // collect all the nodes to be refined
-    k = 0;
-    Vec_PtrClear( p->vClassNew );
-    Vec_PtrForEachEntry( p->vClasses1, pObj, i )
-    {
-        if ( p->pFuncNodeIsConst( pObj ) )
-            Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
-        else 
-            Vec_PtrPush( p->vClassNew, pObj );
-    }
-    Vec_PtrShrink( p->vClasses1, k );
-    if ( Vec_PtrSize(p->vClassNew) == 0 )
-        return 0;
-/*
-    printf( "Refined const-1 class: {" );
-    Vec_PtrForEachEntry( p->vClassNew, pObj, i )
-        printf( " %d", pObj->Id );
-    printf( " }\n" );
-*/
-    if ( Vec_PtrSize(p->vClassNew) == 1 )
-    {
-        Fra_ClassObjSetRepr( Vec_PtrEntry(p->vClassNew,0), NULL );
-        return 1;
-    }
-    // create a new class composed of these nodes
-    ppClass = p->pMemClassesFree;
-    p->pMemClassesFree += 2 * Vec_PtrSize(p->vClassNew);
-    Vec_PtrForEachEntry( p->vClassNew, pObj, i )
-    {
-        ppClass[i] = pObj;
-        ppClass[Vec_PtrSize(p->vClassNew)+i] = NULL;
-        Fra_ClassObjSetRepr( pObj, i? ppClass[0] : NULL );
-    }
-    assert( ppClass[0] != NULL );
-    Vec_PtrPush( p->vClasses, ppClass );
-    // iteratively refine this class
-    if ( fRefineNewClass )
-        nRefis += Fra_RefineClassLastIter( p, p->vClasses );
-    else if ( pSkipped )
-        (*pSkipped)++;
-    return nRefis;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Starts representation of equivalence classes with one class.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 )
-{
-    Aig_Obj_t ** pClass;
-    p->pMemClasses = ALLOC( Aig_Obj_t *, 4 );
-    pClass = p->pMemClasses;
-    assert( Id1 < Id2 );
-    pClass[0] = Aig_ManObj( p->pAig, Id1 );
-    pClass[1] = Aig_ManObj( p->pAig, Id2 );
-    pClass[2] = NULL;
-    pClass[3] = NULL;
-    Fra_ClassObjSetRepr( pClass[1], pClass[0] );
-    Vec_PtrPush( p->vClasses, pClass );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates latch correspondence classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClassesLatchCorr( Fra_Man_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i, nEntries = 0;
-    Vec_PtrClear( p->pCla->vClasses1 );
-    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
-    {
-        Vec_PtrPush( p->pCla->vClasses1, pObj );
-        Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pManAig) );
-    }
-    // allocate room for classes
-    p->pCla->pMemClasses = ALLOC( Aig_Obj_t *, 2*(nEntries + Vec_PtrSize(p->pCla->vClasses1)) );
-    p->pCla->pMemClassesFree = p->pCla->pMemClasses + 2*nEntries;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Postprocesses the classes by removing half of the less useful.]
-
-  Description []
-               
-  SideEffects [] 
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClassesPostprocess( Fra_Cla_t * p )
-{
-    int Ratio = 2;
-    Fra_Sml_t * pComb;
-    Aig_Obj_t * pObj, * pRepr, ** ppClass;
-    int * pWeights, WeightMax = 0, i, k, c;
-    // perform combinational simulation
-    pComb = Fra_SmlSimulateComb( p->pAig, 32 );
-    // compute the weight of each node in the classes
-    pWeights = ALLOC( int, Aig_ManObjNumMax(p->pAig) );
-    memset( pWeights, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
-    Aig_ManForEachObj( p->pAig, pObj, i )
-    { 
-        pRepr = Fra_ClassObjRepr( pObj );
-        if ( pRepr == NULL )
-            continue;
-        pWeights[i] = Fra_SmlNodeNotEquWeight( pComb, pRepr->Id, pObj->Id );
-        WeightMax = AIG_MAX( WeightMax, pWeights[i] );
-    }
-    Fra_SmlStop( pComb );
-    printf( "Before: Const = %6d. Class = %6d.  ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
-    // remove nodes from classes whose weight is less than WeightMax/Ratio
-    k = 0;
-    Vec_PtrForEachEntry( p->vClasses1, pObj, i )
-    {
-        if ( pWeights[pObj->Id] >= WeightMax/Ratio )
-            Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
-        else
-            Fra_ClassObjSetRepr( pObj, NULL );
-    }
-    Vec_PtrShrink( p->vClasses1, k );
-    // in each class, compact the nodes
-    Vec_PtrForEachEntry( p->vClasses, ppClass, i )
-    {
-        k = 1;
-        for ( c = 1; ppClass[c]; c++ )
-        {
-            if ( pWeights[ppClass[c]->Id] >= WeightMax/Ratio )
-                ppClass[k++] = ppClass[c];
-            else
-                Fra_ClassObjSetRepr( ppClass[c], NULL );
-        }
-        ppClass[k] = NULL;
-    }
-    // remove classes with only repr
-    k = 0;
-    Vec_PtrForEachEntry( p->vClasses, ppClass, i )
-        if ( ppClass[1] != NULL )
-            Vec_PtrWriteEntry( p->vClasses, k++, ppClass );
-    Vec_PtrShrink( p->vClasses, k );
-    printf( "After: Const = %6d. Class = %6d. \n", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
-    free( pWeights );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Postprocesses the classes by selecting representative lowest in top order.]
-
-  Description []
-               
-  SideEffects [] 
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClassesSelectRepr( Fra_Cla_t * p )
-{
-    Aig_Obj_t ** pClass, * pNodeMin;
-    int i, c, cMinSupp, nSuppSizeMin, nSuppSizeCur;
-    // reassign representatives in each class
-    Vec_PtrForEachEntry( p->vClasses, pClass, i )
-    {
-        // collect support sizes and find the min-support node
-        pNodeMin = NULL;
-        nSuppSizeMin = AIG_INFINITY;
-        for ( c = 0; pClass[c]; c++ )
-        {
-            nSuppSizeCur = Aig_SupportSize( p->pAig, pClass[c] );
-//            nSuppSizeCur = 1;
-            if ( nSuppSizeMin > nSuppSizeCur || 
-                (nSuppSizeMin == nSuppSizeCur && pNodeMin->Level > pClass[c]->Level) )
-            {
-                nSuppSizeMin = nSuppSizeCur;
-                pNodeMin = pClass[c];
-                cMinSupp = c; 
-            }
-        }
-        // skip the case when the repr did not change
-        if ( cMinSupp == 0 )
-            continue;
-        // make the new node the representative of the class
-        pClass[cMinSupp] = pClass[0];
-        pClass[0] = pNodeMin;
-        // set the representative
-        for ( c = 0; pClass[c]; c++ )
-            Fra_ClassObjSetRepr( pClass[c], c? pClass[0] : NULL );
-    }
-}
-
-
-
-static inline Aig_Obj_t * Fra_ObjEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj )                       { return ppEquivs[pObj->Id];  }
-static inline void        Fra_ObjSetEqu( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj, Aig_Obj_t * pNode ) { ppEquivs[pObj->Id] = pNode; }
-
-static inline Aig_Obj_t * Fra_ObjChild0Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin0(pObj)), Aig_ObjFaninC0(pObj));  }
-static inline Aig_Obj_t * Fra_ObjChild1Equ( Aig_Obj_t ** ppEquivs, Aig_Obj_t * pObj ) { return Aig_NotCond(Fra_ObjEqu(ppEquivs,Aig_ObjFanin1(pObj)), Aig_ObjFaninC1(pObj));  }
-
-/**Function*************************************************************
-
-  Synopsis    [Add the node and its constraints to the new AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Fra_ClassesDeriveNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, Aig_Obj_t ** ppEquivs )
-{
-    Aig_Obj_t * pObjNew, * pObjRepr, * pObjReprNew, * pMiter;//, * pObjNew2;
-    // skip nodes without representative
-    if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
-        return;
-    assert( pObjRepr->Id < pObj->Id );
-    // get the new node 
-    pObjNew = Fra_ObjEqu( ppEquivs, pObj );
-    // get the new node of the representative
-    pObjReprNew = Fra_ObjEqu( ppEquivs, pObjRepr );
-    // 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
-//    Fra_ObjSetEqu( ppEquivs, pObj, 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 );
-    Aig_ObjCreatePo( pManFraig, pMiter );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives AIG for the partitioned problem.]
-
-  Description []
-               
-  SideEffects [] 
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
-{
-    Aig_Man_t * pManFraig;
-    Aig_Obj_t * pObj, * pObjNew;
-    Aig_Obj_t ** pLatches, ** ppEquivs;
-    int i, k, f, nFramesAll = nFramesK + 1;
-    assert( Aig_ManRegNum(p->pAig) > 0 );
-    assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
-    assert( nFramesK > 0 );
-    // start the fraig package
-    pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pAig) * nFramesAll );
-    pManFraig->pName = Aig_UtilStrsav( p->pAig->pName );
-    // allocate place for the node mapping
-    ppEquivs = ALLOC( Aig_Obj_t *, Aig_ManObjNumMax(p->pAig) );
-    Fra_ObjSetEqu( ppEquivs, Aig_ManConst1(p->pAig), Aig_ManConst1(pManFraig) );
-    // create latches for the first frame
-    Aig_ManForEachLoSeq( p->pAig, pObj, i )
-        Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
-    // add timeframes
-    pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
-    for ( f = 0; f < nFramesAll; f++ )
-    {
-        // create PIs for this frame
-        Aig_ManForEachPiSeq( p->pAig, pObj, i )
-            Fra_ObjSetEqu( ppEquivs, pObj, Aig_ObjCreatePi(pManFraig) );
-        // set the constraints on the latch outputs
-        Aig_ManForEachLoSeq( p->pAig, pObj, i )
-            Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
-        // add internal nodes of this frame
-        Aig_ManForEachNode( p->pAig, pObj, i )
-        {
-            pObjNew = Aig_And( pManFraig, Fra_ObjChild0Equ(ppEquivs, pObj), Fra_ObjChild1Equ(ppEquivs, pObj) );
-            Fra_ObjSetEqu( ppEquivs, pObj, pObjNew );
-            Fra_ClassesDeriveNode( pManFraig, pObj, ppEquivs );
-        }
-        if ( f == nFramesAll - 1 )
-            break;
-        if ( f == nFramesAll - 2 )
-            pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
-        // save the latch input values
-        k = 0;
-        Aig_ManForEachLiSeq( p->pAig, pObj, i )
-            pLatches[k++] = Fra_ObjChild0Equ( ppEquivs, pObj );
-        // insert them to the latch output values
-        k = 0;
-        Aig_ManForEachLoSeq( p->pAig, pObj, i )
-            Fra_ObjSetEqu( ppEquivs, pObj, pLatches[k++] );
-    }
-    free( pLatches );
-    free( ppEquivs );
-    // mark the asserts
-    assert( Aig_ManPoNum(pManFraig) % nFramesAll == 0 );
-printf( "Assert miters = %6d. Output miters = %6d.\n", 
-       pManFraig->nAsserts, Aig_ManPoNum(pManFraig) - pManFraig->nAsserts );
-    // remove dangling nodes
-    Aig_ManCleanup( pManFraig );
-    return pManFraig;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/fra/fraCnf.c b/src/aig/fra/fraCnf.c
deleted file mode 100644
index d56c0254..00000000
--- a/src/aig/fra/fraCnf.c
+++ /dev/null
@@ -1,286 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraCnf.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [New FRAIG package.]
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fraCnf.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-
-/**Function*************************************************************
-
-  Synopsis    [Addes clauses to the solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_AddClausesMux( Fra_Man_t * p, Aig_Obj_t * pNode )
-{
-    Aig_Obj_t * pNodeI, * pNodeT, * pNodeE;
-    int pLits[4], RetValue, VarF, VarI, VarT, VarE, fCompT, fCompE;
-
-    assert( !Aig_IsComplement( pNode ) );
-    assert( Aig_ObjIsMuxType( pNode ) );
-    // get nodes (I = if, T = then, E = else)
-    pNodeI = Aig_ObjRecognizeMux( pNode, &pNodeT, &pNodeE );
-    // get the variable numbers
-    VarF = Fra_ObjSatNum(pNode);
-    VarI = Fra_ObjSatNum(pNodeI);
-    VarT = Fra_ObjSatNum(Aig_Regular(pNodeT));
-    VarE = Fra_ObjSatNum(Aig_Regular(pNodeE));
-    // get the complementation flags
-    fCompT = Aig_IsComplement(pNodeT);
-    fCompE = Aig_IsComplement(pNodeE);
-
-    // f = ITE(i, t, e)
-
-    // i' + t' + f
-    // i' + t  + f'
-    // i  + e' + f
-    // i  + e  + f'
-
-    // create four clauses
-    pLits[0] = toLitCond(VarI, 1);
-    pLits[1] = toLitCond(VarT, 1^fCompT);
-    pLits[2] = toLitCond(VarF, 0);
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
-    assert( RetValue );
-    pLits[0] = toLitCond(VarI, 1);
-    pLits[1] = toLitCond(VarT, 0^fCompT);
-    pLits[2] = toLitCond(VarF, 1);
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
-    assert( RetValue );
-    pLits[0] = toLitCond(VarI, 0);
-    pLits[1] = toLitCond(VarE, 1^fCompE);
-    pLits[2] = toLitCond(VarF, 0);
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
-    assert( RetValue );
-    pLits[0] = toLitCond(VarI, 0);
-    pLits[1] = toLitCond(VarE, 0^fCompE);
-    pLits[2] = toLitCond(VarF, 1);
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
-    assert( RetValue );
-
-    // two additional clauses
-    // t' & e' -> f'
-    // t  & e  -> f 
-
-    // t  + e   + f'
-    // t' + e'  + f 
-
-    if ( VarT == VarE )
-    {
-//        assert( fCompT == !fCompE );
-        return;
-    }
-
-    pLits[0] = toLitCond(VarT, 0^fCompT);
-    pLits[1] = toLitCond(VarE, 0^fCompE);
-    pLits[2] = toLitCond(VarF, 1);
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
-    assert( RetValue );
-    pLits[0] = toLitCond(VarT, 1^fCompT);
-    pLits[1] = toLitCond(VarE, 1^fCompE);
-    pLits[2] = toLitCond(VarF, 0);
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
-    assert( RetValue );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Addes clauses to the solver.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_AddClausesSuper( Fra_Man_t * p, Aig_Obj_t * pNode, Vec_Ptr_t * vSuper )
-{
-    Aig_Obj_t * pFanin;
-    int * pLits, nLits, RetValue, i;
-    assert( !Aig_IsComplement(pNode) );
-    assert( Aig_ObjIsNode( pNode ) );
-    // create storage for literals
-    nLits = Vec_PtrSize(vSuper) + 1;
-    pLits = ALLOC( int, nLits );
-    // suppose AND-gate is A & B = C
-    // add !A => !C   or   A + !C
-    Vec_PtrForEachEntry( vSuper, pFanin, i )
-    {
-        pLits[0] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), Aig_IsComplement(pFanin));
-        pLits[1] = toLitCond(Fra_ObjSatNum(pNode), 1);
-        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
-        assert( RetValue );
-    }
-    // add A & B => C   or   !A + !B + C
-    Vec_PtrForEachEntry( vSuper, pFanin, i )
-        pLits[i] = toLitCond(Fra_ObjSatNum(Aig_Regular(pFanin)), !Aig_IsComplement(pFanin));
-    pLits[nLits-1] = toLitCond(Fra_ObjSatNum(pNode), 0);
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + nLits );
-    assert( RetValue );
-    free( pLits );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_CollectSuper_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper, int fFirst, int fUseMuxes )
-{
-    // if the new node is complemented or a PI, another gate begins
-    if ( Aig_IsComplement(pObj) || Aig_ObjIsPi(pObj) || (!fFirst && Aig_ObjRefs(pObj) > 1) || 
-         (fUseMuxes && Aig_ObjIsMuxType(pObj)) )
-    {
-        Vec_PtrPushUnique( vSuper, pObj );
-        return;
-    }
-    // go through the branches
-    Fra_CollectSuper_rec( Aig_ObjChild0(pObj), vSuper, 0, fUseMuxes );
-    Fra_CollectSuper_rec( Aig_ObjChild1(pObj), vSuper, 0, fUseMuxes );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Fra_CollectSuper( Aig_Obj_t * pObj, int fUseMuxes )
-{
-    Vec_Ptr_t * vSuper;
-    assert( !Aig_IsComplement(pObj) );
-    assert( !Aig_ObjIsPi(pObj) );
-    vSuper = Vec_PtrAlloc( 4 );
-    Fra_CollectSuper_rec( pObj, vSuper, 1, fUseMuxes );
-    return vSuper;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates the solver clause database.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ObjAddToFrontier( Fra_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontier )
-{
-    Fra_Man_t * pTemp = pObj->pData;
-    assert( !Aig_IsComplement(pObj) );
-    if ( Fra_ObjSatNum(pObj) )
-        return;
-    assert( Fra_ObjSatNum(pObj) == 0 );
-    assert( Fra_ObjFaninVec(pObj) == NULL );
-    if ( Aig_ObjIsConst1(pObj) )
-        return;
-//printf( "Assigning node %d number %d\n", pObj->Id, p->nSatVars );
-    Fra_ObjSetSatNum( pObj, p->nSatVars++ );
-    if ( Aig_ObjIsNode(pObj) )
-        Vec_PtrPush( vFrontier, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates the solver clause database.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
-{ 
-    Vec_Ptr_t * vFrontier, * vFanins;
-    Aig_Obj_t * pNode, * pFanin;
-    int i, k, fUseMuxes = 1;
-    assert( pOld || pNew );
-    // quit if CNF is ready
-    if ( (!pOld || Fra_ObjFaninVec(pOld)) && (!pNew || Fra_ObjFaninVec(pNew)) )
-        return;
-    // start the frontier
-    vFrontier = Vec_PtrAlloc( 100 );
-    if ( pOld ) Fra_ObjAddToFrontier( p, pOld, vFrontier );
-    if ( pNew ) Fra_ObjAddToFrontier( p, pNew, vFrontier );
-    // explore nodes in the frontier
-    Vec_PtrForEachEntry( vFrontier, pNode, i )
-    {
-        // create the supergate
-        assert( Fra_ObjSatNum(pNode) );
-        assert( Fra_ObjFaninVec(pNode) == NULL );
-        if ( fUseMuxes && Aig_ObjIsMuxType(pNode) )
-        {
-            vFanins = Vec_PtrAlloc( 4 );
-            Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin0(pNode) ) );
-            Vec_PtrPushUnique( vFanins, Aig_ObjFanin0( Aig_ObjFanin1(pNode) ) );
-            Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin0(pNode) ) );
-            Vec_PtrPushUnique( vFanins, Aig_ObjFanin1( Aig_ObjFanin1(pNode) ) );
-            Vec_PtrForEachEntry( vFanins, pFanin, k )
-                Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
-            Fra_AddClausesMux( p, pNode );
-        }
-        else
-        {
-            vFanins = Fra_CollectSuper( pNode, fUseMuxes );
-            Vec_PtrForEachEntry( vFanins, pFanin, k )
-                Fra_ObjAddToFrontier( p, Aig_Regular(pFanin), vFrontier );
-            Fra_AddClausesSuper( p, pNode, vFanins );
-        }
-        assert( Vec_PtrSize(vFanins) > 1 );
-        Fra_ObjSetFaninVec( pNode, vFanins );
-    }
-    Vec_PtrFree( vFrontier );
-}
-
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
deleted file mode 100644
index b390edbe..00000000
--- a/src/aig/fra/fraCore.c
+++ /dev/null
@@ -1,428 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraCore.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [New FRAIG package.]
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fraCore.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-/* 
-    Speculating reduction in the sequential case leads to an interesting 
-    situation when a counter-ex may not refine any classes. This happens
-    for non-constant equivalence classes. In such cases the representative
-    of the class (proved by simulation to be non-constant) may be reduced 
-    to a constant during the speculative reduction. The fraig-representative 
-    of this representative node is a constant node, even though this is a 
-    non-constant class. Experiments have shown that this situation happens 
-    very often at the beginning of the refinement iteration when there are 
-    many spurious candidate equivalence classes (especially if heavy-duty 
-    simulatation of BMC was node used at the beginning). As a result, the 
-    SAT solver run may return a counter-ex that  distinguishes the given 
-    representative node from the constant-1 node but this counter-ex
-    does not distinguish the nodes in the non-costant class... This is why 
-    there is no check of refinment after a counter-ex in the sequential case.
-*/
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Reports the status of the miter.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_FraigMiterStatus( Aig_Man_t * p )
-{
-    Aig_Obj_t * pObj, * pObjNew;
-    int i, CountConst0 = 0, CountNonConst0 = 0, CountUndecided = 0;
-    if ( p->pData )
-        return 0;
-    Aig_ManForEachPoSeq( p, pObj, i )
-    {
-        pObjNew = Aig_ObjChild0(pObj);
-        // check if the output is constant 0
-        if ( pObjNew == Aig_ManConst0(p) )
-        {
-            CountConst0++;
-            continue;
-        }
-        // check if the output is constant 1
-        if ( pObjNew == Aig_ManConst1(p) )
-        {
-            CountNonConst0++;
-            continue;
-        }
-        // check if the output can be constant 0
-        if ( Aig_Regular(pObjNew)->fPhase != (unsigned)Aig_IsComplement(pObjNew) )
-        {
-            CountNonConst0++;
-            continue;
-        }
-        CountUndecided++;
-    }
-/*
-    if ( p->pParams->fVerbose )
-    {
-        printf( "Miter has %d outputs. ", Aig_ManPoNum(p->pManAig) );
-        printf( "Const0 = %d.  ", CountConst0 );
-        printf( "NonConst0 = %d.  ", CountNonConst0 );
-        printf( "Undecided = %d.  ", CountUndecided );
-        printf( "\n" );
-    }
-*/
-    if ( CountNonConst0 )
-        return 0;
-    if ( CountUndecided )
-        return -1;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Write speculative miter for one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Fra_FraigNodeSpeculate( Fra_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pObjFraig, Aig_Obj_t * pObjReprFraig )
-{ 
-    static int Counter = 0;
-    char FileName[20];
-    Aig_Man_t * pTemp;
-    Aig_Obj_t * pNode;
-    int i;
-    // create manager with the logic for these two nodes
-    pTemp = Aig_ManExtractMiter( p->pManFraig, pObjFraig, pObjReprFraig );
-    // dump the logic into a file
-    sprintf( FileName, "aig\\%03d.blif", ++Counter );
-    Aig_ManDumpBlif( pTemp, FileName );
-    printf( "Speculation cone with %d nodes was written into file \"%s\".\n", Aig_ManNodeNum(pTemp), FileName );
-    // clean up
-    Aig_ManStop( pTemp );
-    Aig_ManForEachObj( p->pManFraig, pNode, i )
-        pNode->pData = p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Verifies the generated counter-ex.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_FraigVerifyCounterEx( Fra_Man_t * p, Vec_Int_t * vCex )
-{
-    Aig_Obj_t * pObj, ** ppClass;
-    int i, c;
-    assert( Aig_ManPiNum(p->pManAig) == Vec_IntSize(vCex) );
-    // make sure the input pattern is not used
-    Aig_ManForEachObj( p->pManAig, pObj, i )
-        assert( !pObj->fMarkB );
-    // simulate the cex through the AIG
-    Aig_ManConst1(p->pManAig)->fMarkB = 1;
-    Aig_ManForEachPi( p->pManAig, pObj, i )
-        pObj->fMarkB = Vec_IntEntry(vCex, i);
-    Aig_ManForEachNode( p->pManAig, pObj, i )
-        pObj->fMarkB = (Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj)) & 
-                       (Aig_ObjFanin1(pObj)->fMarkB ^ Aig_ObjFaninC1(pObj));
-    Aig_ManForEachPo( p->pManAig, pObj, i )
-        pObj->fMarkB = Aig_ObjFanin0(pObj)->fMarkB ^ Aig_ObjFaninC0(pObj);
-    // check if the classes hold
-    Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
-    {
-        if ( pObj->fPhase != pObj->fMarkB )
-            printf( "The node %d is not constant under cex!\n", pObj->Id );
-    }
-    Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
-    {
-        for ( c = 1; ppClass[c]; c++ )
-            if ( (ppClass[0]->fPhase ^ ppClass[c]->fPhase) != (ppClass[0]->fMarkB ^ ppClass[c]->fMarkB) )
-                printf( "The nodes %d and %d are not equal under cex!\n", ppClass[0]->Id, ppClass[c]->Id );
-//        for ( c = 0; ppClass[c]; c++ )
-//            if ( Fra_ObjFraig(ppClass[c],p->pPars->nFramesK) == Aig_ManConst1(p->pManFraig) )
-//                printf( "A member of non-constant class has a constant repr!\n" );
-    }
-    // clean the simulation pattern
-    Aig_ManForEachObj( p->pManAig, pObj, i )
-        pObj->fMarkB = 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs fraiging for one node.]
-
-  Description [Returns the fraiged node.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
-{ 
-    Aig_Obj_t * pObjRepr, * pObjFraig, * pObjFraig2, * pObjReprFraig;
-    int RetValue;
-    assert( !Aig_IsComplement(pObj) );
-    // get representative of this class
-    pObjRepr = Fra_ClassObjRepr( pObj );
-    if ( pObjRepr == NULL || // this is a unique node
-       (!p->pPars->fDoSparse && pObjRepr == Aig_ManConst1(p->pManAig)) ) // this is a sparse node
-        return;
-    // get the fraiged node
-    pObjFraig = Fra_ObjFraig( pObj, p->pPars->nFramesK );
-    // get the fraiged representative
-    pObjReprFraig = Fra_ObjFraig( pObjRepr, p->pPars->nFramesK );
-    // if the fraiged nodes are the same, return
-    if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
-    {
-        p->nSatCallsSkipped++;
-        return;
-    }
-    assert( p->pPars->nFramesK || Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) );
-    // if they are proved different, the c-ex will be in p->pPatWords
-    RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
-    if ( RetValue == 1 )  // proved equivalent
-    {
-//        if ( p->pPars->fChoicing )
-//            Aig_ObjCreateRepr( p->pManFraig, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
-        // the nodes proved equal
-        pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
-        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjFraig2 );
-        return;
-    }
-    if ( RetValue == -1 ) // failed
-    {
-        if ( p->vTimeouts == NULL )
-            p->vTimeouts = Vec_PtrAlloc( 100 );
-        Vec_PtrPush( p->vTimeouts, pObj );
-        if ( !p->pPars->fSpeculate )
-            return;
-        assert( 0 );
-        // speculate
-        p->nSpeculs++;
-        pObjFraig2 = Aig_NotCond( pObjReprFraig, pObj->fPhase ^ pObjRepr->fPhase );
-        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjFraig2 );
-        Fra_FraigNodeSpeculate( p, pObj, Aig_Regular(pObjFraig), Aig_Regular(pObjReprFraig) );
-        return;
-    }
-    // disprove the nodes
-    p->pCla->fRefinement = 1;
-    // if we do not include the node into those disproved, we may end up 
-    // merging this node with another representative, for which proof has timed out
-    if ( p->vTimeouts )
-        Vec_PtrPush( p->vTimeouts, pObj );
-    // verify that the counter-example satisfies all the constraints
-//    if ( p->vCex )
-//        Fra_FraigVerifyCounterEx( p, p->vCex );
-    // simulate the counter-example and return the Fraig node
-    Fra_SmlResimulate( p );
-    if ( !p->pPars->nFramesK && Fra_ClassObjRepr(pObj) == pObjRepr )
-        printf( "Fra_FraigNode(): Error in class refinement!\n" );
-    assert( p->pPars->nFramesK || Fra_ClassObjRepr(pObj) != pObjRepr );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs fraiging for the internal nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_FraigSweep( Fra_Man_t * p )
-{
-    Bar_Progress_t * pProgress;
-    Aig_Obj_t * pObj, * pObjNew;
-    int i, k = 0, Pos = 0;
-    // fraig latch outputs
-    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
-    {
-        Fra_FraigNode( p, pObj );
-        if ( p->pPars->fUseImps )
-            Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
-    }
-    if ( p->pPars->fLatchCorr )
-        return;
-    // fraig internal nodes
-    pProgress = Bar_ProgressStart( stdout, Aig_ManObjNumMax(p->pManAig) );
-    Aig_ManForEachNode( p->pManAig, pObj, i )
-    {
-        Bar_ProgressUpdate( pProgress, i, NULL );
-        // derive and remember the new fraig node
-        pObjNew = Aig_And( p->pManFraig, Fra_ObjChild0Fra(pObj,p->pPars->nFramesK), Fra_ObjChild1Fra(pObj,p->pPars->nFramesK) );
-        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, pObjNew );
-        Aig_Regular(pObjNew)->pData = p;
-        // quit if simulation detected a counter-example for a PO
-        if ( p->pManFraig->pData )
-            continue;
-        // perform fraiging
-        Fra_FraigNode( p, pObj );
-        if ( p->pPars->fUseImps )
-            Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
-    }
-    Bar_ProgressStop( pProgress );
-    // try to prove the outputs of the miter
-    p->nNodesMiter = Aig_ManNodeNum(p->pManFraig);
-//    Fra_MiterStatus( p->pManFraig );
-//    if ( p->pPars->fProve && p->pManFraig->pData == NULL )
-//        Fra_MiterProve( p );
-    // compress implications after processing all of them
-    if ( p->pPars->fUseImps )
-        Fra_ImpCompactArray( p->pCla->vImps );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs fraiging of the AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars )
-{
-    Fra_Man_t * p;
-    Aig_Man_t * pManAigNew;
-    int clk;
-    if ( Aig_ManNodeNum(pManAig) == 0 )
-        return Aig_ManDup(pManAig, 1);
-clk = clock();
-    assert( Aig_ManLatchNum(pManAig) == 0 );
-    p = Fra_ManStart( pManAig, pPars );
-    p->pManFraig = Fra_ManPrepareComb( p );
-    p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords );
-    Fra_SmlSimulate( p, 0 );
-//    if ( p->pPars->fChoicing )
-//        Aig_ManReprStart( p->pManFraig, Aig_ManObjNumMax(p->pManAig) );
-    // collect initial states
-    p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
-    p->nNodesBeg = Aig_ManNodeNum(pManAig);
-    p->nRegsBeg  = Aig_ManRegNum(pManAig);
-    // perform fraig sweep
-    Fra_FraigSweep( p );
-    // call back the procedure to check implications
-    if ( pManAig->pImpFunc )
-        pManAig->pImpFunc( p, pManAig->pImpData );
-    // finalize the fraiged manager
-    Fra_ManFinalizeComb( p );
-    if ( p->pPars->fChoicing )
-    {
-int clk2 = clock();
-        Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
-        pManAigNew = Aig_ManDupRepr( p->pManAig, 1 );
-        Aig_ManReprStart( pManAigNew, Aig_ManObjNumMax(pManAigNew) );
-        Aig_ManTransferRepr( pManAigNew, p->pManAig );
-        Aig_ManMarkValidChoices( pManAigNew );
-        Aig_ManStop( p->pManFraig );
-        p->pManFraig = NULL;
-p->timeTrav += clock() - clk2;
-    }
-    else
-    {
-        Aig_ManCleanup( p->pManFraig );
-        pManAigNew = p->pManFraig;
-        p->pManFraig = NULL;
-    }
-p->timeTotal = clock() - clk;
-    // collect final stats
-    p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
-    p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
-    p->nRegsEnd  = Aig_ManRegNum(pManAigNew);
-    Fra_ManStop( p );
-    return pManAigNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs choicing of the AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax )
-{
-    Fra_Par_t Pars, * pPars = &Pars; 
-    Fra_ParamsDefault( pPars );
-    pPars->nBTLimitNode = nConfMax;
-    pPars->fChoicing    = 1;
-    pPars->fDoSparse    = 1;
-    pPars->fSpeculate   = 0;
-    pPars->fProve       = 0;
-    pPars->fVerbose     = 0;
-    return Fra_FraigPerform( pManAig, pPars );
-}
- 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Fra_FraigEquivence( Aig_Man_t * pManAig, int nConfMax )
-{
-    Aig_Man_t * pFraig;
-    Fra_Par_t Pars, * pPars = &Pars; 
-    Fra_ParamsDefault( pPars );
-    pPars->nBTLimitNode = nConfMax;
-    pPars->fChoicing    = 0;
-    pPars->fDoSparse    = 1;
-    pPars->fSpeculate   = 0;
-    pPars->fProve       = 0;
-    pPars->fVerbose     = 0;
-    pFraig = Fra_FraigPerform( pManAig, pPars );
-    return pFraig;
-} 
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
deleted file mode 100644
index a5fc7d58..00000000
--- a/src/aig/fra/fraImp.c
+++ /dev/null
@@ -1,721 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraImp.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [New FRAIG package.]
-
-  Synopsis    [Detecting and proving implications.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fraImp.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of 1s in each siminfo of each node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Fra_SmlCountOnesOne( Fra_Sml_t * p, int Node )
-{
-    unsigned * pSim;
-    int k, Counter = 0;
-    pSim = Fra_ObjSim( p, Node );
-    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
-        Counter += Aig_WordCountOnes( pSim[k] );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of 1s in each siminfo of each node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i, * pnBits; 
-    pnBits = ALLOC( int, Aig_ManObjNumMax(p->pAig) );  
-    memset( pnBits, 0, sizeof(int) * Aig_ManObjNumMax(p->pAig) );
-    Aig_ManForEachObj( p->pAig, pObj, i )
-        pnBits[i] = Fra_SmlCountOnesOne( p, i );
-    return pnBits;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if implications holds.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Sml_NodeCheckImp( Fra_Sml_t * p, int Left, int Right )
-{
-    unsigned * pSimL, * pSimR;
-    int k;
-    pSimL = Fra_ObjSim( p, Left );
-    pSimR = Fra_ObjSim( p, Right );
-    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
-        if ( pSimL[k] & ~pSimR[k] )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of 1s in the complement of the implication.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
-{
-    unsigned * pSimL, * pSimR;
-    int k, Counter = 0;
-    pSimL = Fra_ObjSim( p, Left );
-    pSimR = Fra_ObjSim( p, Right );
-    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
-        Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the complement of the implication.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Sml_NodeSaveNotImpPatterns( Fra_Sml_t * p, int Left, int Right, unsigned * pResult )
-{
-    unsigned * pSimL, * pSimR;
-    int k;
-    pSimL = Fra_ObjSim( p, Left );
-    pSimR = Fra_ObjSim( p, Right );
-    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
-        pResult[k] |= pSimL[k] & ~pSimR[k];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the array of nodes sorted by the number of 1s.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Fra_SmlSortUsingOnes( Fra_Sml_t * p, int fLatchCorr )
-{
-    Aig_Obj_t * pObj;
-    Vec_Ptr_t * vNodes;
-    int i, nNodes, nTotal, nBits, * pnNodes, * pnBits, * pMemory;
-    assert( p->nWordsTotal > 0 );
-    // count 1s in each node's siminfo
-    pnBits = Fra_SmlCountOnes( p );
-    // count number of nodes having that many 1s
-    nNodes = 0;
-    nBits = p->nWordsTotal * 32;
-    pnNodes = ALLOC( int, nBits + 1 );
-    memset( pnNodes, 0, sizeof(int) * (nBits + 1) );
-    Aig_ManForEachObj( p->pAig, pObj, i )
-    {
-        if ( i == 0 ) continue;
-        // skip non-PI and non-internal nodes
-        if ( fLatchCorr )
-        {
-            if ( !Aig_ObjIsPi(pObj) )
-                continue;
-        }
-        else
-        {
-            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
-                continue;
-        }
-        // skip nodes participating in the classes
-//        if ( Fra_ClassObjRepr(pObj) )
-//            continue;
-        assert( pnBits[i] <= nBits ); // "<" because of normalized info
-        pnNodes[pnBits[i]]++;
-        nNodes++;
-    }
-    // allocate memory for all the nodes
-    pMemory = ALLOC( int, nNodes + nBits + 1 );  
-    // markup the memory for each node
-    vNodes = Vec_PtrAlloc( nBits + 1 );
-    Vec_PtrPush( vNodes, pMemory );
-    for ( i = 1; i <= nBits; i++ )
-    {
-        pMemory += pnNodes[i-1] + 1;
-        Vec_PtrPush( vNodes, pMemory );
-    }
-    // add the nodes
-    memset( pnNodes, 0, sizeof(int) * (nBits + 1) );
-    Aig_ManForEachObj( p->pAig, pObj, i )
-    {
-        if ( i == 0 ) continue;
-        // skip non-PI and non-internal nodes
-        if ( fLatchCorr )
-        {
-            if ( !Aig_ObjIsPi(pObj) )
-                continue;
-        }
-        else
-        {
-            if ( !Aig_ObjIsNode(pObj) && !Aig_ObjIsPi(pObj) )
-                continue;
-        }
-        // skip nodes participating in the classes
-//        if ( Fra_ClassObjRepr(pObj) )
-//            continue;
-        pMemory = Vec_PtrEntry( vNodes, pnBits[i] );
-        pMemory[ pnNodes[pnBits[i]]++ ] = i;
-    }
-    // add 0s in the end
-    nTotal = 0;
-    Vec_PtrForEachEntry( vNodes, pMemory, i )
-    {
-        pMemory[ pnNodes[i]++ ] = 0;
-        nTotal += pnNodes[i];
-    }
-    assert( nTotal == nNodes + nBits + 1 );
-    free( pnNodes );
-    free( pnBits );
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the array of implications with the highest cost.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Fra_SmlSelectMaxCost( Vec_Int_t * vImps, int * pCosts, int nCostMax, int nImpLimit, int * pCostRange )
-{
-    Vec_Int_t * vImpsNew;
-    int * pCostCount, nImpCount, Imp, i, c;
-    assert( Vec_IntSize(vImps) >= nImpLimit );
-    // count how many implications have each cost
-    pCostCount = ALLOC( int, nCostMax + 1 );
-    memset( pCostCount, 0, sizeof(int) * (nCostMax + 1) );
-    for ( i = 0; i < Vec_IntSize(vImps); i++ )
-    {
-        assert( pCosts[i] <= nCostMax );
-        pCostCount[ pCosts[i] ]++;
-    }
-    assert( pCostCount[0] == 0 );
-    // select the bound on the cost (above this bound, implication will be included)
-    nImpCount = 0;
-    for ( c = nCostMax; c > 0; c-- )
-    {
-        nImpCount += pCostCount[c];
-        if ( nImpCount >= nImpLimit )
-            break;
-    }
-//    printf( "Cost range >= %d.\n", c );
-    // collect implications with the given costs
-    vImpsNew = Vec_IntAlloc( nImpLimit );
-    Vec_IntForEachEntry( vImps, Imp, i )
-    {
-        if ( pCosts[i] < c )
-            continue;
-        Vec_IntPush( vImpsNew, Imp );
-        if ( Vec_IntSize( vImpsNew ) == nImpLimit )
-            break;
-    }
-    free( pCostCount );
-    if ( pCostRange )
-        *pCostRange = c;
-    return vImpsNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Compares two implications using their largest ID.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Sml_CompareMaxId( unsigned short * pImp1, unsigned short * pImp2 )
-{
-    int Max1 = AIG_MAX( pImp1[0], pImp1[1] );
-    int Max2 = AIG_MAX( pImp2[0], pImp2[1] );
-    if ( Max1 < Max2 )
-        return -1;
-    if ( Max1 > Max2  )
-        return 1;
-    return 0; 
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives implication candidates.]
-
-  Description [Implication candidates have the property that 
-  (1) they hold using sequential simulation information
-  (2) they do not hold using combinational simulation information
-  (3) they have as high expressive power as possible (heuristically)
-      that is, they are easy to disprove combinationally
-      meaning they cover relatively larger sequential subspace.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr )
-{
-    int nSimWords = 64;
-    Fra_Sml_t * pSeq, * pComb;
-    Vec_Int_t * vImps, * vTemp;
-    Vec_Ptr_t * vNodes;
-    int * pImpCosts, * pNodesI, * pNodesK;
-    int nImpsTotal = 0, nImpsTried = 0, nImpsNonSeq = 0, nImpsComb = 0, nImpsCollected = 0;
-    int CostMin = AIG_INFINITY, CostMax = 0;
-    int i, k, Imp, CostRange, clk = clock();
-    assert( Aig_ManObjNumMax(p->pManAig) < (1 << 15) );
-    assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
-    // normalize both managers
-    pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
-    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1 );
-    // get the nodes sorted by the number of 1s
-    vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr );
-    // count the total number of implications
-    for ( k = nSimWords * 32; k > 0; k-- )
-    for ( i = k - 1; i > 0; i-- )
-    for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
-    for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
-        nImpsTotal++;
-
-    // compute implications and their costs
-    pImpCosts = ALLOC( int, nImpMaxLimit );
-    vImps = Vec_IntAlloc( nImpMaxLimit );
-    for ( k = pSeq->nWordsTotal * 32; k > 0; k-- )
-        for ( i = k - 1; i > 0; i-- )
-        {
-            for ( pNodesI = Vec_PtrEntry( vNodes, i ); *pNodesI; pNodesI++ )
-            for ( pNodesK = Vec_PtrEntry( vNodes, k ); *pNodesK; pNodesK++ )
-            {
-                nImpsTried++;
-                if ( !Sml_NodeCheckImp(pSeq, *pNodesI, *pNodesK) )
-                {
-                    nImpsNonSeq++;
-                    continue;
-                }
-                if ( Sml_NodeCheckImp(pComb, *pNodesI, *pNodesK) )
-                {
-                    nImpsComb++;
-                    continue;
-                }
-                nImpsCollected++;
-                Imp = Fra_ImpCreate( *pNodesI, *pNodesK );
-                pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK);
-                CostMin = AIG_MIN( CostMin, pImpCosts[ Vec_IntSize(vImps) ] );
-                CostMax = AIG_MAX( CostMax, pImpCosts[ Vec_IntSize(vImps) ] );
-                Vec_IntPush( vImps, Imp );
-                if ( Vec_IntSize(vImps) == nImpMaxLimit )
-                    goto finish;
-            } 
-        }
-finish:
-    Fra_SmlStop( pComb );
-    Fra_SmlStop( pSeq );
-
-    // select implications with the highest cost
-    CostRange = CostMin;
-    if ( Vec_IntSize(vImps) > nImpUseLimit )
-    {
-        vImps = Fra_SmlSelectMaxCost( vTemp = vImps, pImpCosts, nSimWords * 32, nImpUseLimit, &CostRange );
-        Vec_IntFree( vTemp );  
-    }
-
-    // dealloc
-    free( pImpCosts ); 
-    free( Vec_PtrEntry(vNodes, 0) );
-    Vec_PtrFree( vNodes );
-    // reorder implications topologically
-    qsort( (void *)Vec_IntArray(vImps), Vec_IntSize(vImps), sizeof(int), 
-            (int (*)(const void *, const void *)) Sml_CompareMaxId );
-if ( p->pPars->fVerbose )
-{
-printf( "Implications: All = %d. Try = %d. NonSeq = %d. Comb = %d. Res = %d.\n", 
-    nImpsTotal, nImpsTried, nImpsNonSeq, nImpsComb, nImpsCollected );
-printf( "Implication weight: Min = %d. Pivot = %d. Max = %d.   ", 
-       CostMin, CostRange, CostMax );
-PRT( "Time", clock() - clk );
-}
-    return vImps;
-}
-
-
-// the following three procedures are called to 
-// - add implications to the SAT solver
-// - check implications using the SAT solver
-// - refine implications using after a cex is generated
-
-/**Function*************************************************************
-
-  Synopsis    [Add implication clauses to the SAT solver.]
-
-  Description [Note that implications should be checked in the first frame!]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums )
-{
-    sat_solver * pSat = p->pSat;
-    Aig_Obj_t * pLeft, * pRight;
-    Aig_Obj_t * pLeftF, * pRightF;
-    int pLits[2], Imp, Left, Right, i, f, status;
-    int fComplL, fComplR;
-    Vec_IntForEachEntry( vImps, Imp, i )
-    {
-        // get the corresponding nodes
-        pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
-        pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
-        // check if all the nodes are present
-        for ( f = 0; f < p->pPars->nFramesK; f++ )
-        {
-            // map these info fraig
-            pLeftF = Fra_ObjFraig( pLeft, f );
-            pRightF = Fra_ObjFraig( pRight, f );
-            if ( Aig_ObjIsNone(Aig_Regular(pLeftF)) || Aig_ObjIsNone(Aig_Regular(pRightF)) )
-            {
-                Vec_IntWriteEntry( vImps, i, 0 );
-                break;
-            }
-        }
-        if ( f < p->pPars->nFramesK )
-            continue;
-        // add constraints in each timeframe
-        for ( f = 0; f < p->pPars->nFramesK; f++ )
-        {
-            // map these info fraig
-            pLeftF = Fra_ObjFraig( pLeft, f );
-            pRightF = Fra_ObjFraig( pRight, f );
-            // get the corresponding SAT numbers
-            Left = pSatVarNums[ Aig_Regular(pLeftF)->Id ];
-            Right = pSatVarNums[ Aig_Regular(pRightF)->Id ];
-            assert( Left > 0  && Left < p->nSatVars );
-            assert( Right > 0 && Right < p->nSatVars );
-            // get the complemented attributes
-            fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
-            fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
-            // get the constraint
-            // L => R      L' v R     (complement = L & R')
-            pLits[0] = 2 * Left  + !fComplL;
-            pLits[1] = 2 * Right +  fComplR;
-            // add contraint to solver
-            if ( !sat_solver_addclause( pSat, pLits, pLits + 2 ) )
-            {
-                sat_solver_delete( pSat );
-                p->pSat = NULL;
-                return;
-            }
-        }
-    }
-    status = sat_solver_simplify(pSat);
-    if ( status == 0 )
-    {
-        sat_solver_delete( pSat );
-        p->pSat = NULL;
-    }
-//    printf( "Total imps = %d. ", Vec_IntSize(vImps) );
-    Fra_ImpCompactArray( vImps );
-//    printf( "Valid imps = %d. \n", Vec_IntSize(vImps) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Check implications for the node (if they are present).]
-
-  Description [Returns the new position in the array.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos )
-{
-    Aig_Obj_t * pLeft, * pRight;
-    Aig_Obj_t * pLeftF, * pRightF;
-    int i, Imp, Left, Right, Max, RetValue;
-    int fComplL, fComplR;
-    Vec_IntForEachEntryStart( vImps, Imp, i, Pos )
-    {
-        if ( Imp == 0 )
-            continue;
-        Left = Fra_ImpLeft(Imp);
-        Right = Fra_ImpRight(Imp);
-        Max = AIG_MAX( Left, Right );
-        assert( Max >= pNode->Id );
-        if ( Max > pNode->Id )
-            return i;
-        // get the corresponding nodes
-        pLeft  = Aig_ManObj( p->pManAig, Left );
-        pRight = Aig_ManObj( p->pManAig, Right );
-        // get the corresponding FRAIG nodes
-        pLeftF  = Fra_ObjFraig( pLeft, p->pPars->nFramesK );
-        pRightF = Fra_ObjFraig( pRight, p->pPars->nFramesK );
-        // get the complemented attributes
-        fComplL = pLeft->fPhase ^ Aig_IsComplement(pLeftF);
-        fComplR = pRight->fPhase ^ Aig_IsComplement(pRightF);
-        // check equality
-        if ( Aig_Regular(pLeftF) == Aig_Regular(pRightF) )
-        {
-            if ( fComplL == fComplR ) // x => x  - always true
-                continue;
-            assert( fComplL != fComplR );
-            // consider 4 possibilities:
-            // NOT(1) => 1    or   0 => 1  - always true
-            // 1 => NOT(1)    or   1 => 0  - never true
-            // NOT(x) => x    or   x       - not always true
-            // x => NOT(x)    or   NOT(x)  - not always true
-            if ( Aig_ObjIsConst1(Aig_Regular(pLeftF)) && fComplL ) // proved implication
-                continue;
-            // disproved implication
-            p->pCla->fRefinement = 1;
-            Vec_IntWriteEntry( vImps, i, 0 );
-            continue;
-        }
-        // check the implication 
-        // - if true, a clause is added
-        // - if false, a cex is simulated
-        // make sure the implication is refined
-        RetValue = Fra_NodesAreImp( p, Aig_Regular(pLeftF), Aig_Regular(pRightF), fComplL, fComplR );
-        if ( RetValue != 1 )
-        {
-            p->pCla->fRefinement = 1;
-            if ( RetValue == 0 )
-                Fra_SmlResimulate( p );
-            if ( Vec_IntEntry(vImps, i) != 0 )
-                printf( "Fra_ImpCheckForNode(): Implication is not refined!\n" );
-            assert( Vec_IntEntry(vImps, i) == 0 );
-        }
-    }
-    return i;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Removes those implications that no longer hold.]
-
-  Description [Returns 1 if refinement has happened.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps )
-{
-    Aig_Obj_t * pLeft, * pRight;
-    int Imp, i, RetValue = 0;
-    Vec_IntForEachEntry( vImps, Imp, i )
-    {
-        if ( Imp == 0 )
-            continue;
-        // get the corresponding nodes
-        pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
-        pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
-        // check if implication holds using this simulation info
-        if ( !Sml_NodeCheckImp(p->pSml, pLeft->Id, pRight->Id) )
-        {
-            Vec_IntWriteEntry( vImps, i, 0 );
-            RetValue = 1;
-        }
-    }
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Removes empty implications.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ImpCompactArray( Vec_Int_t * vImps )
-{
-    int i, k, Imp;
-    k = 0;
-    Vec_IntForEachEntry( vImps, Imp, i )
-        if ( Imp )
-            Vec_IntWriteEntry( vImps, k++, Imp );
-    Vec_IntShrink( vImps, k );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Determines the ratio of the state space by computed implications.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-double Fra_ImpComputeStateSpaceRatio( Fra_Man_t * p )
-{
-    int nSimWords = 64;
-    Fra_Sml_t * pComb;
-    unsigned * pResult;
-    double Ratio = 0.0;
-    int Left, Right, Imp, i;
-    if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
-        return Ratio;
-    // simulate the AIG manager with combinational patterns
-    pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
-    // go through the implications and collect where they do not hold
-    pResult = Fra_ObjSim( pComb, 0 );
-    assert( pResult[0] == 0 );
-    Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
-    {
-        Left = Fra_ImpLeft(Imp);
-        Right = Fra_ImpRight(Imp);
-        Sml_NodeSaveNotImpPatterns( pComb, Left, Right, pResult );
-    }
-    // count the number of ones in this area
-    Ratio = 100.0 * Fra_SmlCountOnesOne( pComb, 0 ) / (32*(pComb->nWordsTotal-pComb->nWordsPref));
-    Fra_SmlStop( pComb );
-    return Ratio;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the number of failed implications.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_ImpVerifyUsingSimulation( Fra_Man_t * p )
-{
-    int nFrames = 2000;
-    int nSimWords = 8;
-    Fra_Sml_t * pSeq;
-    char * pfFails;
-    int Left, Right, Imp, i, Counter;
-    if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
-        return 0;
-    // simulate the AIG manager with combinational patterns
-    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nFrames, nSimWords );
-    // go through the implications and check how many of them do not hold
-    pfFails = ALLOC( char, Vec_IntSize(p->pCla->vImps) );
-    memset( pfFails, 0, sizeof(char) * Vec_IntSize(p->pCla->vImps) );
-    Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
-    {
-        Left = Fra_ImpLeft(Imp);
-        Right = Fra_ImpRight(Imp);
-        pfFails[i] = !Sml_NodeCheckImp( pSeq, Left, Right );
-    }
-    // count how many has failed
-    Counter = 0;
-    for ( i = 0; i < Vec_IntSize(p->pCla->vImps); i++ )
-        Counter += pfFails[i];
-    free( pfFails );
-    Fra_SmlStop( pSeq );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Record proven implications in the AIG manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ImpRecordInManager( Fra_Man_t * p, Aig_Man_t * pNew )
-{
-    Aig_Obj_t * pLeft, * pRight, * pMiter;
-    int nPosOld, Imp, i;
-    if ( p->pCla->vImps == NULL || Vec_IntSize(p->pCla->vImps) == 0 )
-        return;
-    // go through the implication
-    nPosOld = Aig_ManPoNum(pNew);
-    Vec_IntForEachEntry( p->pCla->vImps, Imp, i )
-    {
-        pLeft = Aig_ManObj( p->pManAig, Fra_ImpLeft(Imp) );
-        pRight = Aig_ManObj( p->pManAig, Fra_ImpRight(Imp) );
-        // record the implication: L' + R
-        pMiter = Aig_Or( pNew, 
-            Aig_NotCond(pLeft->pData, !pLeft->fPhase), 
-            Aig_NotCond(pRight->pData, pRight->fPhase) ); 
-        Aig_ObjCreatePo( pNew, pMiter );
-    }
-    pNew->nAsserts = Aig_ManPoNum(pNew) - nPosOld;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
deleted file mode 100644
index f45e8af0..00000000
--- a/src/aig/fra/fraInd.c
+++ /dev/null
@@ -1,479 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraInd.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [New FRAIG package.]
-
-  Synopsis    [Inductive prover.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fraInd.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fra.h"
-#include "cnf.h"
-#include "dar.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Performs AIG rewriting on the constaint manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_FraigInductionRewrite( Fra_Man_t * p )
-{
-    Aig_Man_t * pTemp;
-    Aig_Obj_t * pObj, * pObjPo;
-    int nTruePis, k, i, clk = clock();
-    // perform AIG rewriting on the speculated frames
-    pTemp = Aig_ManDup( p->pManFraig, 0 );
-//    pTemp = Dar_ManRwsat( pTemp, 1, 0 );
-    pTemp = Dar_ManRewriteDefault( pTemp );
-//    printf( "Before = %6d.  After = %6d.\n", Aig_ManNodeNum(p->pManFraig), Aig_ManNodeNum(pTemp) ); 
-//Aig_ManDumpBlif( p->pManFraig, "1.blif" );
-//Aig_ManDumpBlif( pTemp, "2.blif" );
-//    Fra_FramesWriteCone( pTemp );
-//    Aig_ManStop( pTemp );
-    // transfer PI/register pointers
-    assert( p->pManFraig->nRegs == pTemp->nRegs );
-    assert( p->pManFraig->nAsserts == pTemp->nAsserts );
-    nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
-    memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
-    Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), p->pPars->nFramesK, Aig_ManConst1(pTemp) );
-    Aig_ManForEachPiSeq( p->pManAig, pObj, i )
-        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ManPi(pTemp,nTruePis*p->pPars->nFramesK+i) );
-    k = 0;
-    assert( Aig_ManRegNum(p->pManAig) == Aig_ManPoNum(pTemp) - pTemp->nAsserts );
-    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
-    {
-        pObjPo = Aig_ManPo(pTemp, pTemp->nAsserts + k++);
-        Fra_ObjSetFraig( pObj, p->pPars->nFramesK, Aig_ObjChild0(pObjPo) );
-    }
-    // exchange
-    Aig_ManStop( p->pManFraig );
-    p->pManFraig = pTemp;
-p->timeRwr += clock() - clk;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs speculative reduction for one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Fra_FramesConstrainNode( Aig_Man_t * pManFraig, Aig_Obj_t * pObj, int iFrame )
-{
-    Aig_Obj_t * pObjNew, * pObjNew2, * pObjRepr, * pObjReprNew, * pMiter;
-    // skip nodes without representative
-    if ( (pObjRepr = Fra_ClassObjRepr(pObj)) == NULL )
-        return;
-    assert( pObjRepr->Id < pObj->Id );
-    // get the new node 
-    pObjNew = Fra_ObjFraig( pObj, iFrame );
-    // get the new node of the representative
-    pObjReprNew = Fra_ObjFraig( 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
-    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 );
-    Aig_ObjCreatePo( pManFraig, pMiter );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the inductive case with speculative reduction.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
-{
-    Aig_Man_t * pManFraig;
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjNew;
-    int i, k, f;
-    assert( p->pManFraig == NULL );
-    assert( Aig_ManRegNum(p->pManAig) > 0 );
-    assert( Aig_ManRegNum(p->pManAig) < Aig_ManPiNum(p->pManAig) );
-
-    // start the fraig package
-    pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) * p->nFramesAll );
-    pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName );
-    pManFraig->nRegs = p->pManAig->nRegs;
-    // create PI nodes for the frames
-    for ( f = 0; f < p->nFramesAll; f++ )
-        Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), f, Aig_ManConst1(pManFraig) );
-    for ( f = 0; f < p->nFramesAll; f++ )
-        Aig_ManForEachPiSeq( p->pManAig, pObj, i )
-            Fra_ObjSetFraig( pObj, f, Aig_ObjCreatePi(pManFraig) );
-    // create latches for the first frame
-    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
-        Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) );
-
-    // add timeframes
-//    pManFraig->fAddStrash = 1;
-    for ( f = 0; f < p->nFramesAll - 1; f++ )
-    {
-        // set the constraints on the latch outputs
-        Aig_ManForEachLoSeq( p->pManAig, pObj, i )
-            Fra_FramesConstrainNode( pManFraig, pObj, f );
-        // add internal nodes of this frame
-        Aig_ManForEachNode( p->pManAig, pObj, i )
-        {
-            pObjNew = Aig_And( pManFraig, Fra_ObjChild0Fra(pObj,f), Fra_ObjChild1Fra(pObj,f) );
-            Fra_ObjSetFraig( pObj, f, pObjNew );
-            Fra_FramesConstrainNode( pManFraig, pObj, f );
-        }
-        // transfer latch input to the latch outputs 
-        Aig_ManForEachLiLoSeq( p->pManAig, pObjLi, pObjLo, k )
-            Fra_ObjSetFraig( pObjLo, f+1, Fra_ObjChild0Fra(pObjLi,f) );
-    }
-//    pManFraig->fAddStrash = 0;
-    // mark the asserts
-    pManFraig->nAsserts = Aig_ManPoNum(pManFraig);
-    // add the POs for the latch outputs of the last frame
-    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
-        Aig_ObjCreatePo( pManFraig, Fra_ObjFraig(pObj,p->nFramesAll-1) );
-
-    // remove dangling nodes
-    Aig_ManCleanup( pManFraig );
-    // make sure the satisfying assignment is node assigned
-    assert( pManFraig->pData == NULL );
-    return pManFraig;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the inductive case with speculative reduction.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_FramesAddMore( Aig_Man_t * p, int nFrames )
-{
-    Aig_Obj_t * pObj, ** pLatches;
-    int i, k, f, nNodesOld;
-    // set copy pointer of each object to point to itself
-    Aig_ManForEachObj( p, pObj, i )
-        pObj->pData = pObj;
-    // iterate and add objects
-    nNodesOld = Aig_ManObjNumMax(p);
-    pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p) );
-    for ( f = 0; f < nFrames; f++ )
-    {
-        // clean latch inputs and outputs
-        Aig_ManForEachLiSeq( p, pObj, i )
-            pObj->pData = NULL;
-        Aig_ManForEachLoSeq( p, pObj, i )
-            pObj->pData = NULL;
-        // save the latch input values
-        k = 0;
-        Aig_ManForEachLiSeq( p, pObj, i )
-        {
-            if ( Aig_ObjFanin0(pObj)->pData )
-                pLatches[k++] = Aig_ObjChild0Copy(pObj);
-            else
-                pLatches[k++] = NULL;
-        }
-        // insert them as the latch output values
-        k = 0;
-        Aig_ManForEachLoSeq( p, pObj, i )
-            pObj->pData = pLatches[k++];
-        // create the next time frame of nodes
-        Aig_ManForEachNode( p, pObj, i )
-        {
-            if ( i > nNodesOld )
-                break;
-            if ( Aig_ObjFanin0(pObj)->pData && Aig_ObjFanin1(pObj)->pData )
-                pObj->pData = Aig_And( p, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-            else
-                pObj->pData = NULL;
-        }
-    }
-    free( pLatches );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs choicing of the AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int nMaxImps, int fRewrite, int fUseImps, int fLatchCorr, int fWriteImps, int fVerbose, int * pnIter )
-{
-    int fUseSimpleCnf = 0;
-    int fUseOldSimulation = 0;
-    // other paramaters affecting performance
-    // - presence of FRAIGing in Abc_NtkDarSeqSweep()
-    // - using distance-1 patterns in Fra_SmlAssignDist1()
-    // - the number of simulation patterns
-    // - the number of BMC frames
-
-    Fra_Man_t * p;
-    Fra_Par_t Pars, * pPars = &Pars; 
-    Aig_Obj_t * pObj;
-    Cnf_Dat_t * pCnf;
-    Aig_Man_t * pManAigNew;
-    int nNodesBeg, nRegsBeg;
-    int nIter, i, clk = clock(), clk2;
-
-    if ( Aig_ManNodeNum(pManAig) == 0 )
-    {
-        if ( pnIter ) *pnIter = 0;
-        return Aig_ManDup(pManAig, 1);
-    }
-    assert( Aig_ManLatchNum(pManAig) == 0 );
-    assert( Aig_ManRegNum(pManAig) > 0 );
-    assert( nFramesK > 0 );
-//Aig_ManShow( pManAig, 0, NULL );
- 
-    nNodesBeg = Aig_ManNodeNum(pManAig);
-    nRegsBeg  = Aig_ManRegNum(pManAig);
-
-    // enhance the AIG by adding timeframes
-//    Fra_FramesAddMore( pManAig, 3 );
-
-    // get parameters
-    Fra_ParamsDefaultSeq( pPars );
-    pPars->nFramesP   = nFramesP;
-    pPars->nFramesK   = nFramesK;
-    pPars->nMaxImps   = nMaxImps;
-    pPars->fVerbose   = fVerbose;
-    pPars->fRewrite   = fRewrite;
-    pPars->fLatchCorr = fLatchCorr;
-    pPars->fUseImps   = fUseImps;
-    pPars->fWriteImps = fWriteImps;
-
-    // start the fraig manager for this run
-    p = Fra_ManStart( pManAig, pPars );
-    // derive and refine e-classes using K initialized frames
-    if ( fUseOldSimulation )
-    {
-        if ( pPars->nFramesP > 0 )
-        {
-            pPars->nFramesP = 0;
-            printf( "Fra_FraigInduction(): Prefix cannot be used.\n" );
-        }
-        p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
-        Fra_SmlSimulate( p, 1 );
-    }
-    else
-    {
-        // bug:  r iscas/blif/s5378.blif    ; st; ssw -v
-        // bug:  r iscas/blif/s1238.blif    ; st; ssw -v
-        // refine the classes with more simulation rounds
-if ( fVerbose )
-printf( "Simulating %d AIG nodes for %d cycles ... ", Aig_ManNodeNum(pManAig), pPars->nFramesP + 32 );
-        p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 1 ); //pPars->nFramesK + 1, 1 );  
-if ( fVerbose ) 
-{
-PRT( "Time", clock() - clk );
-}
-        Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
-//        Fra_ClassesPostprocess( p->pCla );
-        // allocate new simulation manager for simulating counter-examples
-        Fra_SmlStop( p->pSml );
-        p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
-    }
-
-    // select the most expressive implications
-    if ( pPars->fUseImps )
-        p->pCla->vImps = Fra_ImpDerive( p, 5000000, pPars->nMaxImps, pPars->fLatchCorr );
-
-    // perform BMC (for the min number of frames)
-    Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK+1 ); // +1 is needed to prevent non-refinement
-//Fra_ClassesPrint( p->pCla, 1 );
-//    if ( p->vCex == NULL )
-//        p->vCex = Vec_IntAlloc( 1000 );
-
-    p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
-    p->nNodesBeg = nNodesBeg; // Aig_ManNodeNum(pManAig);
-    p->nRegsBeg  = nRegsBeg; // Aig_ManRegNum(pManAig);
-
-    // dump AIG of the timeframes
-//    pManAigNew = Fra_ClassesDeriveAig( p->pCla, pPars->nFramesK );
-//    Aig_ManDumpBlif( pManAigNew, "frame_aig.blif" );
-//    Fra_ManPartitionTest2( pManAigNew );
-//    Aig_ManStop( pManAigNew );
-
-    // iterate the inductive case
-    p->pCla->fRefinement = 1;
-    for ( nIter = 0; p->pCla->fRefinement; nIter++ )
-    {
-        int nLitsOld = Fra_ClassesCountLits(p->pCla);
-        int nImpsOld = p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0;
-        // mark the classes as non-refined
-        p->pCla->fRefinement = 0;
-        // derive non-init K-timeframes while implementing e-classes
-clk2 = clock();
-        p->pManFraig = Fra_FramesWithClasses( p );
-p->timeTrav += clock() - clk2;
-//Aig_ManDumpBlif( p->pManFraig, "testaig.blif" );
-
-        // perform AIG rewriting
-        if ( p->pPars->fRewrite )
-            Fra_FraigInductionRewrite( p );
-
-        // convert the manager to SAT solver (the last nLatches outputs are inputs)
-        if ( fUseSimpleCnf || pPars->fUseImps )
-            pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
-        else
-            pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
-//Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
-
-        p->pSat = Cnf_DataWriteIntoSolver( pCnf );
-        p->nSatVars = pCnf->nVars;
-        assert( p->pSat != NULL );
-        if ( p->pSat == NULL )
-            printf( "Fra_FraigInduction(): Computed CNF is not valid.\n" );
-        if ( pPars->fUseImps )
-        {
-            Fra_ImpAddToSolver( p, p->pCla->vImps, pCnf->pVarNums );
-            if ( p->pSat == NULL )
-                printf( "Fra_FraigInduction(): Adding implicationsn to CNF led to a conflict.\n" );
-        }
- 
-        // set the pointers to the manager
-        Aig_ManForEachObj( p->pManFraig, pObj, i )
-            pObj->pData = p;
-
-        // prepare solver for fraiging the last timeframe
-        Fra_ManClean( p, Aig_ManObjNumMax(p->pManFraig) + Aig_ManNodeNum(p->pManAig) );
-
-        // transfer PI/LO variable numbers
-        Aig_ManForEachObj( p->pManFraig, pObj, i )
-        {
-            if ( pCnf->pVarNums[pObj->Id] == -1 )
-                continue;
-            Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
-            Fra_ObjSetFaninVec( pObj, (void *)1 );
-        }
-        Cnf_DataFree( pCnf );
-
-        // report the intermediate results
-        if ( fVerbose )
-        {
-            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  ", 
-                nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
-                Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts );
-            if ( p->pCla->vImps )
-                printf( "I = %6d. ", Vec_IntSize(p->pCla->vImps) );
-            printf( "NR = %6d.\n", Aig_ManNodeNum(p->pManFraig) );
-        } 
-
-        // perform sweeping
-        p->nSatCallsRecent = 0;
-        p->nSatCallsSkipped = 0;
-        Fra_FraigSweep( p );
-
-//        Sat_SolverPrintStats( stdout, p->pSat );
-
-        // remove FRAIG and SAT solver
-        Aig_ManStop( p->pManFraig );   p->pManFraig = NULL;
-        sat_solver_delete( p->pSat );  p->pSat = NULL; 
-        memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
-//        printf( "Recent SAT called = %d. Skipped = %d.\n", p->nSatCallsRecent, p->nSatCallsSkipped );
-        assert( p->vTimeouts == NULL );
-        if ( p->vTimeouts )
-           printf( "Fra_FraigInduction(): SAT solver timed out!\n" );
-        // check if refinement has happened
-//        p->pCla->fRefinement = (int)(nLitsOld != Fra_ClassesCountLits(p->pCla));
-        if ( p->pCla->fRefinement && 
-            nLitsOld == Fra_ClassesCountLits(p->pCla) && 
-            nImpsOld == (p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0) )
-        {
-            printf( "Fra_FraigInduction(): Internal error. The result may not verify.\n" );
-            break;
-        }
-    }
-/*
-    // verify implications using simulation
-    if ( p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
-    {
-        int Temp, clk = clock();
-        if ( Temp = Fra_ImpVerifyUsingSimulation( p ) )
-            printf( "Implications failing the simulation test = %d (out of %d).  ", Temp, Vec_IntSize(p->pCla->vImps) );
-        else
-            printf( "All %d implications have passed the simulation test.  ", Vec_IntSize(p->pCla->vImps) );
-        PRT( "Time", clock() - clk );
-    }
-*/
-
-    // move the classes into representatives and reduce AIG
-clk2 = clock();
-//    Fra_ClassesPrint( p->pCla, 1 );
-    Fra_ClassesSelectRepr( p->pCla );
-    Fra_ClassesCopyReprs( p->pCla, p->vTimeouts );
-    pManAigNew = Aig_ManDupRepr( pManAig, 0 );
-    // add implications to the manager
-    if ( fWriteImps && p->pCla->vImps && Vec_IntSize(p->pCla->vImps) )
-        Fra_ImpRecordInManager( p, pManAigNew );
-    // cleanup the new manager
-    Aig_ManSeqCleanup( pManAigNew );
-//    Aig_ManCountMergeRegs( pManAigNew );
-p->timeTrav += clock() - clk2;
-p->timeTotal = clock() - clk;
-    // get the final stats
-    p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
-    p->nNodesEnd = Aig_ManNodeNum(pManAigNew);
-    p->nRegsEnd  = Aig_ManRegNum(pManAigNew);
-    // free the manager
-    Fra_ManStop( p );
-    // check the output
-//    if ( Aig_ManPoNum(pManAigNew) - Aig_ManRegNum(pManAigNew) == 1 )
-//        if ( Aig_ObjChild0( Aig_ManPo(pManAigNew,0) ) == Aig_ManConst0(pManAigNew) )
-//            printf( "Proved output constant 0.\n" );
-    if ( pnIter ) *pnIter = nIter;
-    return pManAigNew;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/fra/fraLcr.c b/src/aig/fra/fraLcr.c
deleted file mode 100644
index 50fd6687..00000000
--- a/src/aig/fra/fraLcr.c
+++ /dev/null
@@ -1,655 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraLcorr.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [New FRAIG package.]
-
-  Synopsis    [Latch correspondence computation.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fraLcorr.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Fra_Lcr_t_    Fra_Lcr_t;
-struct Fra_Lcr_t_
-{
-    // original AIG
-    Aig_Man_t *      pAig;
-    // equivalence class representation
-    Fra_Cla_t *      pCla;       
-    // partitioning information
-    Vec_Ptr_t *      vParts;        // output partitions
-    int *            pInToOutPart;  // mapping of PI num into PO partition num
-    int *            pInToOutNum;   // mapping of PI num into the num of this PO in the partition
-    // AIGs for the partitions
-    Vec_Ptr_t *      vFraigs;
-    // other variables
-    int              fRefining; 
-    // parameters
-    int              nFramesP;
-    int              fVerbose;
-    // statistics
-    int              nIters;
-    int              nLitsBeg;
-    int              nLitsEnd;
-    int              nNodesBeg;
-    int              nNodesEnd;
-    int              nRegsBeg;
-    int              nRegsEnd;
-    // runtime
-    int              timeSim;
-    int              timePart;
-    int              timeTrav;
-    int              timeFraig;
-    int              timeUpdate;
-    int              timeTotal;
-};
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates the retiming manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fra_Lcr_t * Lcr_ManAlloc( Aig_Man_t * pAig )
-{
-    Fra_Lcr_t * p;
-    p = ALLOC( Fra_Lcr_t, 1 );
-    memset( p, 0, sizeof(Fra_Lcr_t) );
-    p->pAig = pAig;
-    p->pInToOutPart = ALLOC( int, Aig_ManPiNum(pAig) );
-    memset( p->pInToOutPart, 0, sizeof(int) * Aig_ManPiNum(pAig) );
-    p->pInToOutNum = ALLOC( int, Aig_ManPiNum(pAig) );
-    memset( p->pInToOutNum, 0, sizeof(int) * Aig_ManPiNum(pAig) );
-    p->vFraigs = Vec_PtrAlloc( 1000 );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints stats for the fraiging manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lcr_ManPrint( Fra_Lcr_t * p )
-{
-    printf( "Iterations = %d.  LitBeg = %d.  LitEnd = %d. (%6.2f %%).\n", 
-        p->nIters, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg );
-    printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
-        p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg, 
-        p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg );
-    PRT( "AIG simulation  ", p->timeSim  );
-    PRT( "AIG partitioning", p->timePart );
-    PRT( "AIG rebuiding   ", p->timeTrav );
-    PRT( "FRAIGing        ", p->timeFraig );
-    PRT( "AIG updating    ", p->timeUpdate );
-    PRT( "TOTAL RUNTIME   ", p->timeTotal );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deallocates the retiming manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Lcr_ManFree( Fra_Lcr_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    if ( p->fVerbose )
-        Lcr_ManPrint( p );
-    Aig_ManForEachPi( p->pAig, pObj, i )
-        pObj->pNext = NULL;
-    Vec_PtrFree( p->vFraigs );
-    if ( p->pCla  )     Fra_ClassesStop( p->pCla );
-    if ( p->vParts  )   Vec_VecFree( (Vec_Vec_t *)p->vParts );
-    free( p->pInToOutPart );
-    free( p->pInToOutNum );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepare the AIG for class computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fra_Man_t * Fra_LcrAigPrepare( Aig_Man_t * pAig )
-{
-    Fra_Man_t * p;
-    Aig_Obj_t * pObj;
-    int i;
-    p = ALLOC( Fra_Man_t, 1 );
-    memset( p, 0, sizeof(Fra_Man_t) );
-    Aig_ManForEachPi( pAig, pObj, i )
-        pObj->pData = p;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepare the AIG for class computation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_LcrAigPrepareTwo( Aig_Man_t * pAig, Fra_Man_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    Aig_ManForEachPi( pAig, pObj, i )
-        pObj->pData = p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Compares two nodes for equivalence after partitioned fraiging.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_LcrNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
-{
-    Fra_Man_t * pTemp = pObj0->pData;
-    Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc;
-    Aig_Man_t * pFraig;
-    Aig_Obj_t * pOut0, * pOut1;
-    int nPart0, nPart1;
-    assert( Aig_ObjIsPi(pObj0) );
-    assert( Aig_ObjIsPi(pObj1) );
-    // find the partition to which these nodes belong
-    nPart0 = pLcr->pInToOutPart[(int)pObj0->pNext];
-    nPart1 = pLcr->pInToOutPart[(int)pObj1->pNext];
-    // if this is the result of refinement of the class created const-1 nodes
-    // the nodes may end up in different partions - we assume them equivalent
-    if ( nPart0 != nPart1 )
-    {
-        assert( 0 );
-        return 1;
-    }
-    assert( nPart0 == nPart1 );
-    pFraig = Vec_PtrEntry( pLcr->vFraigs, nPart0 );
-    // get the fraig outputs
-    pOut0 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(int)pObj0->pNext] );
-    pOut1 = Aig_ManPo( pFraig, pLcr->pInToOutNum[(int)pObj1->pNext] );
-    return Aig_ObjFanin0(pOut0) == Aig_ObjFanin0(pOut1);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Compares the node with a constant after partioned fraiging.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_LcrNodeIsConst( Aig_Obj_t * pObj )
-{
-    Fra_Man_t * pTemp = pObj->pData;
-    Fra_Lcr_t * pLcr = (Fra_Lcr_t *)pTemp->pBmc;
-    Aig_Man_t * pFraig;
-    Aig_Obj_t * pOut;
-    int nPart;
-    assert( Aig_ObjIsPi(pObj) );
-    // find the partition to which these nodes belong
-    nPart = pLcr->pInToOutPart[(int)pObj->pNext];
-    pFraig = Vec_PtrEntry( pLcr->vFraigs, nPart );
-    // get the fraig outputs
-    pOut = Aig_ManPo( pFraig, pLcr->pInToOutNum[(int)pObj->pNext] );
-    return Aig_ObjFanin0(pOut) == Aig_ManConst1(pFraig);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Give the AIG and classes, reduces AIG for partitioning.]
-
-  Description [Ignores registers that are not in the classes. 
-  Places candidate equivalent classes of registers into single outputs 
-  (for ease of partitioning). The resulting combinational AIG contains 
-  outputs in the same order as equivalence classes of registers, 
-  followed by constant-1 registers. Preserves the set of all inputs.
-  Complemented attributes of the outputs do not matter because we need 
-  then only for collecting the structural info.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Fra_LcrDeriveAigForPartitioning( Fra_Lcr_t * pLcr )
-{
-    Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pObjPo, * pObjNew, ** ppClass, * pMiter;
-    int i, c, Offset;
-    // remember the numbers of the inputs of the original AIG
-    Aig_ManForEachPi( pLcr->pAig, pObj, i )
-    {
-        pObj->pData = pLcr;
-        pObj->pNext = (Aig_Obj_t *)i;
-    }
-    // compute the LO/LI offset
-    Offset = Aig_ManPoNum(pLcr->pAig) - Aig_ManPiNum(pLcr->pAig);
-    // create the PIs
-    Aig_ManCleanData( pLcr->pAig );
-    pNew = Aig_ManStartFrom( pLcr->pAig );
-    // go over the equivalence classes
-    Vec_PtrForEachEntry( pLcr->pCla->vClasses, ppClass, i )
-    {
-        pMiter = Aig_ManConst0(pNew);
-        for ( c = 0; ppClass[c]; c++ )
-        {
-            assert( Aig_ObjIsPi(ppClass[c]) );
-            pObjPo  = Aig_ManPo( pLcr->pAig, Offset+(int)ppClass[c]->pNext );
-            pObjNew = Aig_ManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
-            pMiter  = Aig_Exor( pNew, pMiter, pObjNew );
-        }
-        Aig_ObjCreatePo( pNew, pMiter );
-    }
-    // go over the constant candidates
-    Vec_PtrForEachEntry( pLcr->pCla->vClasses1, pObj, i )
-    {
-        assert( Aig_ObjIsPi(pObj) );
-        pObjPo = Aig_ManPo( pLcr->pAig, Offset+(int)pObj->pNext );
-        pMiter = Aig_ManDup_rec( pNew, pLcr->pAig, Aig_ObjFanin0(pObjPo) );
-        Aig_ObjCreatePo( pNew, pMiter );
-    }
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Remaps partitions into the inputs of original AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_LcrRemapPartitions( Vec_Ptr_t * vParts, Fra_Cla_t * pCla, int * pInToOutPart, int * pInToOutNum )
-{
-    Vec_Int_t * vOne, * vOneNew;
-    Aig_Obj_t ** ppClass, * pObjPi;
-    int Out, Offset, i, k, c;
-    // compute the LO/LI offset
-    Offset = Aig_ManPoNum(pCla->pAig) - Aig_ManPiNum(pCla->pAig);
-    Vec_PtrForEachEntry( vParts, vOne, i )
-    {
-        vOneNew = Vec_IntAlloc( Vec_IntSize(vOne) );
-        Vec_IntForEachEntry( vOne, Out, k )
-        {
-            if ( Out < Vec_PtrSize(pCla->vClasses) )
-            {
-                ppClass = Vec_PtrEntry( pCla->vClasses, Out );
-                for ( c = 0; ppClass[c]; c++ )
-                {
-                    pInToOutPart[(int)ppClass[c]->pNext] = i;
-                    pInToOutNum[(int)ppClass[c]->pNext] = Vec_IntSize(vOneNew);
-                    Vec_IntPush( vOneNew, Offset+(int)ppClass[c]->pNext );
-                }
-            }
-            else
-            {
-                pObjPi = Vec_PtrEntry( pCla->vClasses1, Out - Vec_PtrSize(pCla->vClasses) );
-                pInToOutPart[(int)pObjPi->pNext] = i;
-                pInToOutNum[(int)pObjPi->pNext] = Vec_IntSize(vOneNew);
-                Vec_IntPush( vOneNew, Offset+(int)pObjPi->pNext );
-            }
-        }
-        // replace the class
-        Vec_PtrWriteEntry( vParts, i, vOneNew );
-        Vec_IntFree( vOne );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates AIG of one partition with speculative reduction.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Fra_LcrCreatePart_rec( Fra_Cla_t * pCla, Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t * pObj )
-{
-    assert( !Aig_IsComplement(pObj) );
-    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-        return pObj->pData;
-    Aig_ObjSetTravIdCurrent(p, pObj);
-    if ( Aig_ObjIsPi(pObj) )
-    {
-//        Aig_Obj_t * pRepr = Fra_ClassObjRepr(pObj);
-        Aig_Obj_t * pRepr = pCla->pMemRepr[pObj->Id];
-        if ( pRepr == NULL )
-            pObj->pData = Aig_ObjCreatePi( pNew );
-        else
-        {
-            pObj->pData = Fra_LcrCreatePart_rec( pCla, pNew, p, pRepr );
-            pObj->pData = Aig_NotCond( pObj->pData, pRepr->fPhase ^ pObj->fPhase );
-        }
-        return pObj->pData;
-    }
-    Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin0(pObj) );
-    Fra_LcrCreatePart_rec( pCla, pNew, p, Aig_ObjFanin1(pObj) );
-    return pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates AIG of one partition with speculative reduction.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Fra_LcrCreatePart( Fra_Lcr_t * p, Vec_Int_t * vPart )
-{
-    Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pObjNew;
-    int Out, i;
-    // create new AIG for this partition
-    pNew = Aig_ManStartFrom( p->pAig );
-    Aig_ManIncrementTravId( p->pAig );
-    Aig_ObjSetTravIdCurrent( p->pAig, Aig_ManConst1(p->pAig) );
-    Aig_ManConst1(p->pAig)->pData = Aig_ManConst1(pNew);
-    Vec_IntForEachEntry( vPart, Out, i )
-    {
-        pObj = Aig_ManPo( p->pAig, Out );
-        if ( pObj->fMarkA )
-        {
-            pObjNew = Fra_LcrCreatePart_rec( p->pCla, pNew, p->pAig, Aig_ObjFanin0(pObj) );
-            pObjNew = Aig_NotCond( pObjNew, Aig_ObjFaninC0(pObj) );
-        }
-        else
-            pObjNew = Aig_ManConst1( pNew );
-        Aig_ObjCreatePo( pNew, pObjNew ); 
-    }
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Marks the nodes belonging to the equivalence classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClassNodesMark( Fra_Lcr_t * p )
-{
-    Aig_Obj_t * pObj, ** ppClass;
-    int i, c, Offset;
-    // compute the LO/LI offset
-    Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig);
-    // mark the nodes remaining in the classes
-    Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
-    {
-        pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)pObj->pNext );
-        pObj->fMarkA = 1;
-    }
-    Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
-    {
-        for ( c = 0; ppClass[c]; c++ )
-        {
-            pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)ppClass[c]->pNext );
-            pObj->fMarkA = 1;
-        }
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Unmarks the nodes belonging to the equivalence classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ClassNodesUnmark( Fra_Lcr_t * p )
-{
-    Aig_Obj_t * pObj, ** ppClass;
-    int i, c, Offset;
-    // compute the LO/LI offset
-    Offset = Aig_ManPoNum(p->pCla->pAig) - Aig_ManPiNum(p->pCla->pAig);
-    // mark the nodes remaining in the classes
-    Vec_PtrForEachEntry( p->pCla->vClasses1, pObj, i )
-    {
-        pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)pObj->pNext );
-        pObj->fMarkA = 0;
-    }
-    Vec_PtrForEachEntry( p->pCla->vClasses, ppClass, i )
-    {
-        for ( c = 0; ppClass[c]; c++ )
-        {
-            pObj = Aig_ManPo( p->pCla->pAig, Offset+(int)ppClass[c]->pNext );
-            pObj->fMarkA = 0;
-        }
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs choicing of the AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Fra_FraigLatchCorrespondence( Aig_Man_t * pAig, int nFramesP, int nConfMax, int fProve, int fVerbose, int * pnIter )
-{
-    int nPartSize    = 200;
-    int fReprSelect  = 0;
-
-    Fra_Lcr_t * p;
-    Fra_Sml_t * pSml;
-    Fra_Man_t * pTemp;
-    Aig_Man_t * pAigPart, * pAigNew = NULL;
-    Vec_Int_t * vPart;
-//    Aig_Obj_t * pObj = Aig_ManObj(pAig, 2078);
-    int i, nIter, timeSim, clk = clock(), clk2, clk3;
-    if ( Aig_ManNodeNum(pAig) == 0 )
-    {
-        if ( pnIter ) *pnIter = 0;
-        return Aig_ManDup(pAig, 1);
-    }
-    assert( Aig_ManLatchNum(pAig) == 0 );
-    assert( Aig_ManRegNum(pAig) > 0 );
-
-    // simulate the AIG 
-clk2 = clock();
-if ( fVerbose )
-printf( "Simulating AIG with %d nodes for %d cycles ...  ", Aig_ManNodeNum(pAig), nFramesP + 32 );
-    pSml = Fra_SmlSimulateSeq( pAig, nFramesP, 32, 1 ); 
-if ( fVerbose ) 
-{
-PRT( "Time", clock() - clk2 );
-timeSim = clock() - clk2;
-}
-    // check if simulation discovered non-constant-0 POs
-    if ( fProve && pSml->fNonConstOut )
-    {
-        Fra_SmlStop( pSml );
-        return NULL;
-    }
-
-    // start the manager
-    p = Lcr_ManAlloc( pAig );
-    p->nFramesP = nFramesP;
-    p->fVerbose = fVerbose;
-    p->timeSim += timeSim;
-
-    pTemp = Fra_LcrAigPrepare( pAig );
-    pTemp->pBmc = (Fra_Bmc_t *)p;
-    pTemp->pSml = pSml;
-
-    // get preliminary info about equivalence classes
-    pTemp->pCla = p->pCla = Fra_ClassesStart( p->pAig );
-    Fra_ClassesPrepare( p->pCla, 1 );
-    p->pCla->pFuncNodeIsConst   = Fra_LcrNodeIsConst;
-    p->pCla->pFuncNodesAreEqual = Fra_LcrNodesAreEqual;
-    Fra_SmlStop( pTemp->pSml );
-
-    // partition the AIG for latch correspondence computation
-clk2 = clock();
-if ( fVerbose )
-printf( "Partitioning AIG ...  " );
-    pAigPart = Fra_LcrDeriveAigForPartitioning( p );
-    p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
-    Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
-    Aig_ManStop( pAigPart );
-if ( fVerbose ) 
-{
-PRT( "Time", clock() - clk2 );
-p->timePart += clock() - clk2;
-}
-
-    // get the initial stats
-    p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
-    p->nNodesBeg = Aig_ManNodeNum(p->pAig);
-    p->nRegsBeg  = Aig_ManRegNum(p->pAig);
-
-    // perforn interative reduction of the partitions
-    p->fRefining = 1;
-    for ( nIter = 0; p->fRefining; nIter++ )
-    {
-        p->fRefining = 0;
-        clk3 = clock();
-        // derive AIGs for each partition
-        Fra_ClassNodesMark( p );
-        Vec_PtrClear( p->vFraigs );
-        Vec_PtrForEachEntry( p->vParts, vPart, i )
-        {
-clk2 = clock();
-            pAigPart = Fra_LcrCreatePart( p, vPart );
-p->timeTrav += clock() - clk2;
-clk2 = clock();
-            pAigNew  = Fra_FraigEquivence( pAigPart, nConfMax );
-p->timeFraig += clock() - clk2;
-            Vec_PtrPush( p->vFraigs, pAigNew );
-            Aig_ManStop( pAigPart );
-        }
-        Fra_ClassNodesUnmark( p );
-        // report the intermediate results
-        if ( fVerbose )
-        {
-            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. Part = %3d.  ", 
-                nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
-                Fra_ClassesCountLits(p->pCla), Vec_PtrSize(p->vParts) );
-            PRT( "T", clock() - clk3 );
-        }
-        // refine the classes
-        Fra_LcrAigPrepareTwo( p->pAig, pTemp );
-        if ( Fra_ClassesRefine( p->pCla ) )
-            p->fRefining = 1;
-        if ( Fra_ClassesRefine1( p->pCla, 0, NULL ) )
-            p->fRefining = 1;
-        // clean the fraigs
-        Vec_PtrForEachEntry( p->vFraigs, pAigPart, i )
-            Aig_ManStop( pAigPart );
-
-        // repartition if needed
-        if ( 1 )
-        {
-clk2 = clock();
-            Vec_VecFree( (Vec_Vec_t *)p->vParts );
-            pAigPart = Fra_LcrDeriveAigForPartitioning( p );
-            p->vParts = (Vec_Ptr_t *)Aig_ManPartitionSmart( pAigPart, nPartSize, 0, NULL );
-            Fra_LcrRemapPartitions( p->vParts, p->pCla, p->pInToOutPart, p->pInToOutNum );
-            Aig_ManStop( pAigPart );
-p->timePart += clock() - clk2;
-        }
-    }
-    free( pTemp );
-    p->nIters = nIter;
-
-    // move the classes into representatives and reduce AIG
-clk2 = clock();
-//    Fra_ClassesPrint( p->pCla, 1 );
-    if ( fReprSelect )
-        Fra_ClassesSelectRepr( p->pCla );
-    Fra_ClassesCopyReprs( p->pCla, NULL );
-    pAigNew = Aig_ManDupRepr( p->pAig, 0 );
-    Aig_ManSeqCleanup( pAigNew );
-//    Aig_ManCountMergeRegs( pAigNew );
-p->timeUpdate += clock() - clk2;
-p->timeTotal = clock() - clk;
-    // get the final stats
-    p->nLitsEnd  = Fra_ClassesCountLits( p->pCla );
-    p->nNodesEnd = Aig_ManNodeNum(pAigNew);
-    p->nRegsEnd  = Aig_ManRegNum(pAigNew);
-    Lcr_ManFree( p );
-    if ( pnIter ) *pnIter = nIter;
-    return pAigNew;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
deleted file mode 100644
index f505b0c2..00000000
--- a/src/aig/fra/fraMan.c
+++ /dev/null
@@ -1,304 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraMan.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [New FRAIG package.]
-
-  Synopsis    [Starts the FRAIG manager.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fraMan.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the default solving parameters.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ParamsDefault( Fra_Par_t * pPars )
-{
-    memset( pPars, 0, sizeof(Fra_Par_t) );
-    pPars->nSimWords        =       32;  // the number of words in the simulation info
-    pPars->dSimSatur        =    0.005;  // the ratio of refined classes when saturation is reached
-    pPars->fPatScores       =        0;  // enables simulation pattern scoring
-    pPars->MaxScore         =       25;  // max score after which resimulation is used
-    pPars->fDoSparse        =        1;  // skips sparse functions
-//    pPars->dActConeRatio    =     0.05;  // the ratio of cone to be bumped
-//    pPars->dActConeBumpMax  =      5.0;  // the largest bump of activity
-    pPars->dActConeRatio    =      0.3;  // the ratio of cone to be bumped
-    pPars->dActConeBumpMax  =     10.0;  // the largest bump of activity
-    pPars->nBTLimitNode     =      100;  // conflict limit at a node
-    pPars->nBTLimitMiter    =   500000;  // conflict limit at an output
-    pPars->nFramesK         =        0;  // the number of timeframes to unroll
-    pPars->fConeBias        =        1;
-    pPars->fRewrite         =        0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets the default solving parameters.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
-{
-    memset( pPars, 0, sizeof(Fra_Par_t) );
-    pPars->nSimWords        =        1;  // the number of words in the simulation info
-    pPars->dSimSatur        =    0.005;  // the ratio of refined classes when saturation is reached
-    pPars->fPatScores       =        0;  // enables simulation pattern scoring
-    pPars->MaxScore         =       25;  // max score after which resimulation is used
-    pPars->fDoSparse        =        1;  // skips sparse functions
-    pPars->dActConeRatio    =      0.3;  // the ratio of cone to be bumped
-    pPars->dActConeBumpMax  =     10.0;  // the largest bump of activity
-    pPars->nBTLimitNode     = 10000000;  // conflict limit at a node
-    pPars->nBTLimitMiter    =   500000;  // conflict limit at an output
-    pPars->nFramesK         =        1;  // the number of timeframes to unroll
-    pPars->fConeBias        =        0;
-    pPars->fRewrite         =        0;
-    pPars->fLatchCorr       =        0;
-} 
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the fraiging manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
-{
-    Fra_Man_t * p;
-    Aig_Obj_t * pObj;
-    int i;
-    // allocate the fraiging manager
-    p = ALLOC( Fra_Man_t, 1 );
-    memset( p, 0, sizeof(Fra_Man_t) );
-    p->pPars      = pPars;
-    p->pManAig    = pManAig;
-    p->nSizeAlloc = Aig_ManObjNumMax( pManAig );
-    p->nFramesAll = pPars->nFramesK + 1;
-    // allocate storage for sim pattern
-    p->nPatWords  = Aig_BitWordNum( (Aig_ManPiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) );
-    p->pPatWords  = ALLOC( unsigned, p->nPatWords ); 
-    p->vPiVars    = Vec_PtrAlloc( 100 );
-    // equivalence classes
-    p->pCla       = Fra_ClassesStart( pManAig );
-    // allocate other members
-    p->pMemFraig  = ALLOC( Aig_Obj_t *, p->nSizeAlloc * p->nFramesAll );
-    memset( p->pMemFraig, 0, sizeof(Aig_Obj_t *) * p->nSizeAlloc * p->nFramesAll );
-    // set random number generator
-    srand( 0xABCABC );
-    // set the pointer to the manager
-    Aig_ManForEachObj( p->pManAig, pObj, i )
-        pObj->pData = p;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Starts the fraiging manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ManClean( Fra_Man_t * p, int nNodesMax )
-{
-    int i;
-    // remove old arrays
-    for ( i = 0; i < p->nMemAlloc; i++ )
-        if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 )
-            Vec_PtrFree( p->pMemFanins[i] );
-    // realloc for the new size
-    if ( p->nMemAlloc < nNodesMax )
-    {
-        int nMemAllocNew = nNodesMax + 5000;
-        p->pMemFanins = REALLOC( Vec_Ptr_t *, p->pMemFanins, nMemAllocNew );
-        p->pMemSatNums = REALLOC( int, p->pMemSatNums, nMemAllocNew );
-        p->nMemAlloc = nMemAllocNew;
-    }
-    // prepare for the new run
-    memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc );
-    memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prepares the new manager to begin fraiging.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Fra_ManPrepareComb( Fra_Man_t * p )
-{
-    Aig_Man_t * pManFraig;
-    Aig_Obj_t * pObj;
-    int i;
-    assert( p->pManFraig == NULL );
-    // start the fraig package
-    pManFraig = Aig_ManStart( Aig_ManObjNumMax(p->pManAig) );
-    pManFraig->pName = Aig_UtilStrsav( p->pManAig->pName );
-    pManFraig->nRegs    = p->pManAig->nRegs;
-    pManFraig->nAsserts = p->pManAig->nAsserts;
-    // set the pointers to the available fraig nodes
-    Fra_ObjSetFraig( Aig_ManConst1(p->pManAig), 0, Aig_ManConst1(pManFraig) );
-    Aig_ManForEachPi( p->pManAig, pObj, i )
-        Fra_ObjSetFraig( pObj, 0, Aig_ObjCreatePi(pManFraig) );
-    // set the pointers to the manager
-    Aig_ManForEachObj( pManFraig, pObj, i )
-        pObj->pData = p;
-    // allocate memory for mapping FRAIG nodes into SAT numbers and fanins
-    p->nMemAlloc = p->nSizeAlloc;
-    p->pMemFanins = ALLOC( Vec_Ptr_t *, p->nMemAlloc );
-    memset( p->pMemFanins, 0, sizeof(Vec_Ptr_t *) * p->nMemAlloc );
-    p->pMemSatNums = ALLOC( int, p->nMemAlloc );
-    memset( p->pMemSatNums, 0, sizeof(int) * p->nMemAlloc );
-    // make sure the satisfying assignment is node assigned
-    assert( pManFraig->pData == NULL );
-    return pManFraig;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Finalizes the combinational miter after fraiging.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ManFinalizeComb( Fra_Man_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    // add the POs
-    Aig_ManForEachPo( p->pManAig, pObj, i )
-        Aig_ObjCreatePo( p->pManFraig, Fra_ObjChild0Fra(pObj,0) );
-    // postprocess
-    Aig_ManCleanMarkB( p->pManFraig );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Stops the fraiging manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ManStop( Fra_Man_t * p )
-{
-    if ( p->pPars->fVerbose )
-        Fra_ManPrint( p );
-    // save mapping from original nodes into FRAIG nodes
-    if ( p->pManAig )
-    {
-        if ( p->pManAig->pObjCopies )
-            free( p->pManAig->pObjCopies );
-        p->pManAig->pObjCopies = p->pMemFraig;
-        p->pMemFraig = NULL;
-    }
-    Fra_ManClean( p, 0 );
-    if ( p->vTimeouts ) Vec_PtrFree( p->vTimeouts );
-    if ( p->vPiVars )   Vec_PtrFree( p->vPiVars );
-    if ( p->pSat )      sat_solver_delete( p->pSat );
-    if ( p->pCla  )     Fra_ClassesStop( p->pCla );
-    if ( p->pSml )      Fra_SmlStop( p->pSml );
-    if ( p->vCex )      Vec_IntFree( p->vCex );
-    FREE( p->pMemFraig );
-    FREE( p->pMemFanins );
-    FREE( p->pMemSatNums );
-    FREE( p->pPatWords );
-    free( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints stats for the fraiging manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ManPrint( Fra_Man_t * p )
-{
-    double nMemory = 1.0*Aig_ManObjNumMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
-    printf( "SimWord = %d. Round = %d.  Mem = %0.2f Mb.  LitBeg = %d.  LitEnd = %d. (%6.2f %%).\n", 
-        p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/(p->nLitsBeg?p->nLitsBeg:1) );
-    printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. C-lim = %d. ImpRatio = %6.2f %%\n", 
-        p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->pPars->nBTLimitNode, Fra_ImpComputeStateSpaceRatio(p) );
-    printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
-        p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/(p->nNodesBeg?p->nNodesBeg:1), 
-        p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/(p->nRegsBeg?p->nRegsBeg:1) );
-    if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
-    PRT( "AIG simulation  ", p->pSml->timeSim  );
-    PRT( "AIG traversal   ", p->timeTrav );
-    if ( p->timeRwr )
-    {
-    PRT( "AIG rewriting   ", p->timeRwr  );
-    }
-    PRT( "SAT solving     ", p->timeSat  );
-    PRT( "    Unsat       ", p->timeSatUnsat );
-    PRT( "    Sat         ", p->timeSatSat   );
-    PRT( "    Fail        ", p->timeSatFail  );
-    PRT( "Class refining  ", p->timeRef   );
-    PRT( "TOTAL RUNTIME   ", p->timeTotal );
-    if ( p->time1 ) { PRT( "time1           ", p->time1 ); }
-    if ( p->nSpeculs )
-    printf( "Speculations = %d.\n", p->nSpeculs );
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/fra/fraPart.c b/src/aig/fra/fraPart.c
deleted file mode 100644
index 691b2b3d..00000000
--- a/src/aig/fra/fraPart.c
+++ /dev/null
@@ -1,263 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraPart.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [New FRAIG package.]
-
-  Synopsis    [Partitioning for induction.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fraPart.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ManPartitionTest( Aig_Man_t * p, int nComLim )
-{
-    Bar_Progress_t * pProgress;
-    Vec_Vec_t * vSupps, * vSuppsIn;
-    Vec_Ptr_t * vSuppsNew;
-    Vec_Int_t * vSupNew, * vSup, * vSup2, * vTemp;//, * vSupIn;
-    Vec_Int_t * vOverNew, * vQuantNew;
-    Aig_Obj_t * pObj;
-    int i, k, nCommon, CountOver, CountQuant;
-    int nTotalSupp, nTotalSupp2, Entry, Largest;//, iVar;
-    double Ratio, R;
-    int clk;
-
-    nTotalSupp = 0;
-    nTotalSupp2 = 0;
-    Ratio = 0.0;
- 
-    // compute supports
-clk = clock();
-    vSupps = (Vec_Vec_t *)Aig_ManSupports( p );
-PRT( "Supports", clock() - clk );
-    // remove last entry
-    Aig_ManForEachPo( p, pObj, i )
-    {
-        vSup = Vec_VecEntry( vSupps, i );
-        Vec_IntPop( vSup );
-        // remember support
-//        pObj->pNext = (Aig_Obj_t *)vSup;
-    }
-
-    // create reverse supports
-clk = clock();
-    vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) );
-    Aig_ManForEachPo( p, pObj, i )
-    {
-        vSup = Vec_VecEntry( vSupps, i );
-        Vec_IntForEachEntry( vSup, Entry, k )
-            Vec_VecPush( vSuppsIn, Entry, (void *)i );
-    }
-PRT( "Inverse ", clock() - clk );
-
-clk = clock();
-    // compute extended supports
-    Largest = 0;
-    vSuppsNew = Vec_PtrAlloc( Aig_ManPoNum(p) );
-    vOverNew  = Vec_IntAlloc( Aig_ManPoNum(p) );
-    vQuantNew = Vec_IntAlloc( Aig_ManPoNum(p) );
-    pProgress = Bar_ProgressStart( stdout, Aig_ManPoNum(p) );
-    Aig_ManForEachPo( p, pObj, i )
-    {
-        Bar_ProgressUpdate( pProgress, i, NULL );
-        // get old supports
-        vSup = Vec_VecEntry( vSupps, i );
-        if ( Vec_IntSize(vSup) < 2 )
-            continue;
-        // compute new supports
-        CountOver = CountQuant = 0;
-        vSupNew = Vec_IntDup( vSup );
-        // go through the nodes where the first var appears
-        Aig_ManForEachPo( p, pObj, k )
-//        iVar = Vec_IntEntry( vSup, 0 );
-//        vSupIn = Vec_VecEntry( vSuppsIn, iVar );
-//        Vec_IntForEachEntry( vSupIn, Entry, k )
-        {
-//            pObj = Aig_ManObj( p, Entry );
-            // get support of this output
-//            vSup2 = (Vec_Int_t *)pObj->pNext;
-            vSup2 = Vec_VecEntry( vSupps, k );
-            // count the number of common vars
-            nCommon = Vec_IntTwoCountCommon(vSup, vSup2);
-            if ( nCommon < 2 )
-                continue;
-            if ( nCommon > nComLim )
-            {
-                vSupNew = Vec_IntTwoMerge( vTemp = vSupNew, vSup2 );
-                Vec_IntFree( vTemp );
-                CountOver++;
-            }
-            else
-                CountQuant++;
-        }
-        // save the results
-        Vec_PtrPush( vSuppsNew, vSupNew );
-        Vec_IntPush( vOverNew, CountOver );
-        Vec_IntPush( vQuantNew, CountQuant );
-
-        if ( Largest < Vec_IntSize(vSupNew) )
-            Largest = Vec_IntSize(vSupNew);
-
-        nTotalSupp  += Vec_IntSize(vSup);
-        nTotalSupp2 += Vec_IntSize(vSupNew);
-        if ( Vec_IntSize(vSup) )
-            R = Vec_IntSize(vSupNew) / Vec_IntSize(vSup);
-        else
-            R = 0;
-        Ratio += R;
-
-        if ( R < 5.0 )
-            continue;
-
-        printf( "%6d : ", i );
-        printf( "S = %5d. ", Vec_IntSize(vSup) );
-        printf( "SNew = %5d. ", Vec_IntSize(vSupNew) );
-        printf( "R = %7.2f. ", R );
-        printf( "Over = %5d. ", CountOver );
-        printf( "Quant = %5d. ", CountQuant );
-        printf( "\n" );
-/*
-        Vec_IntForEachEntry( vSupNew, Entry, k )
-            printf( "%d ", Entry );
-        printf( "\n" );
-*/
-    }
-    Bar_ProgressStop( pProgress );
-PRT( "Scanning", clock() - clk );
-
-    // print cumulative statistics
-    printf( "PIs = %6d. POs = %6d. Lim = %3d.   AveS = %3d. SN = %3d. R = %4.2f Max = %5d.\n",
-        Aig_ManPiNum(p), Aig_ManPoNum(p), nComLim,
-        nTotalSupp/Aig_ManPoNum(p), nTotalSupp2/Aig_ManPoNum(p),
-        Ratio/Aig_ManPoNum(p), Largest );
-
-    Vec_VecFree( vSupps );
-    Vec_VecFree( vSuppsIn );
-    Vec_VecFree( (Vec_Vec_t *)vSuppsNew );
-    Vec_IntFree( vOverNew );
-    Vec_IntFree( vQuantNew );
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_ManPartitionTest2( Aig_Man_t * p )
-{
-    Vec_Vec_t * vSupps, * vSuppsIn;
-    Vec_Int_t * vSup, * vSup2, * vSup3;
-    Aig_Obj_t * pObj;
-    int Entry, Entry2, Entry3, Counter;
-    int i, k, m, n, clk;
-    char * pSupp;
- 
-    // compute supports
-clk = clock();
-    vSupps = (Vec_Vec_t *)Aig_ManSupports( p );
-PRT( "Supports", clock() - clk );
-    // remove last entry
-    Aig_ManForEachPo( p, pObj, i )
-    {
-        vSup = Vec_VecEntry( vSupps, i );
-        Vec_IntPop( vSup );
-        // remember support
-//        pObj->pNext = (Aig_Obj_t *)vSup;
-    }
-
-    // create reverse supports
-clk = clock();
-    vSuppsIn = Vec_VecStart( Aig_ManPiNum(p) );
-    Aig_ManForEachPo( p, pObj, i )
-    {
-        if ( i == p->nAsserts )
-            break;
-        vSup = Vec_VecEntry( vSupps, i );
-        Vec_IntForEachEntry( vSup, Entry, k )
-            Vec_VecPush( vSuppsIn, Entry, (void *)i );
-    }
-PRT( "Inverse ", clock() - clk );
-
-    // create affective supports
-clk = clock();
-    pSupp = ALLOC( char, Aig_ManPiNum(p) );
-    Aig_ManForEachPo( p, pObj, i )
-    {
-        if ( i % 50 != 0 )
-            continue;
-        vSup = Vec_VecEntry( vSupps, i );
-        memset( pSupp, 0, sizeof(char) * Aig_ManPiNum(p) );
-        // go through each input of this output
-        Vec_IntForEachEntry( vSup, Entry, k )
-        {
-            pSupp[Entry] = 1;
-            vSup2 = Vec_VecEntry( vSuppsIn, Entry );
-            // go though each assert of this input
-            Vec_IntForEachEntry( vSup2, Entry2, m )
-            {
-                vSup3 = Vec_VecEntry( vSupps, Entry2 );
-                // go through each input of this assert
-                Vec_IntForEachEntry( vSup3, Entry3, n )
-                {
-                    pSupp[Entry3] = 1;
-                }
-            }
-        }
-        // count the entries
-        Counter = 0;
-        for ( m = 0; m < Aig_ManPiNum(p); m++ )
-            Counter += pSupp[m];
-        printf( "%d(%d) ", Vec_IntSize(vSup), Counter );
-    }
-    printf( "\n" );
-PRT( "Extension ", clock() - clk );
-
-    free( pSupp );
-    Vec_VecFree( vSupps );
-    Vec_VecFree( vSuppsIn );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c
deleted file mode 100644
index 11029b69..00000000
--- a/src/aig/fra/fraSat.c
+++ /dev/null
@@ -1,452 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraSat.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [New FRAIG package.]
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fraSat.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include <math.h>
-#include "fra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Runs equivalence test for the two nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
-{
-    int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
-    int status;
-
-    // make sure the nodes are not complemented
-    assert( !Aig_IsComplement(pNew) );
-    assert( !Aig_IsComplement(pOld) );
-    assert( pNew != pOld );
-
-    // if at least one of the nodes is a failed node, perform adjustments:
-    // if the backtrack limit is small, simply skip this node
-    // if the backtrack limit is > 10, take the quare root of the limit
-    nBTLimit = p->pPars->nBTLimitNode;
-    if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
-    {
-        p->nSatFails++;
-        // fail immediately
-//        return -1;
-        if ( nBTLimit <= 10 )
-            return -1;
-        nBTLimit = (int)pow(nBTLimit, 0.7);
-    }
-
-    p->nSatCalls++;
-    p->nSatCallsRecent++;
-
-    // make sure the solver is allocated and has enough variables
-    if ( p->pSat == NULL )
-    {
-        p->pSat = sat_solver_new();
-        p->nSatVars = 1;
-        sat_solver_setnvars( p->pSat, 1000 );
-        // var 0 is reserved for const1 node - add the clause
-        pLits[0] = toLit( 0 );
-        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
-    }
-
-    // if the nodes do not have SAT variables, allocate them
-    Fra_CnfNodeAddToSolver( p, pOld, pNew );
-
-    if ( p->pSat->qtail != p->pSat->qhead )
-    {
-        status = sat_solver_simplify(p->pSat);
-        assert( status != 0 );
-        assert( p->pSat->qtail == p->pSat->qhead );
-    }
-
-    // prepare variable activity
-    if ( p->pPars->fConeBias )
-        Fra_SetActivityFactors( p, pOld, pNew ); 
-
-    // solve under assumptions
-    // A = 1; B = 0     OR     A = 1; B = 1 
-clk = clock();
-    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
-    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
-//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
-    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
-        (sint64)nBTLimit, (sint64)0, 
-        p->nBTLimitGlobal, p->nInsLimitGlobal );
-p->timeSat += clock() - clk;
-    if ( RetValue1 == l_False )
-    {
-p->timeSatUnsat += clock() - clk;
-        pLits[0] = lit_neg( pLits[0] );
-        pLits[1] = lit_neg( pLits[1] );
-        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
-        assert( RetValue );
-        // continue solving the other implication
-        p->nSatCallsUnsat++;
-    }
-    else if ( RetValue1 == l_True )
-    {
-p->timeSatSat += clock() - clk;
-        Fra_SmlSavePattern( p );
-        p->nSatCallsSat++;
-        return 0;
-    }
-    else // if ( RetValue1 == l_Undef )
-    {
-p->timeSatFail += clock() - clk;
-        // mark the node as the failed node
-        if ( pOld != p->pManFraig->pConst1 ) 
-            pOld->fMarkB = 1;
-        pNew->fMarkB = 1;
-        p->nSatFailsReal++;
-        return -1;
-    }
-
-    // if the old node was constant 0, we already know the answer
-    if ( pOld == p->pManFraig->pConst1 )
-    {
-        p->nSatProof++;
-        return 1;
-    }
-
-    // solve under assumptions
-    // A = 0; B = 1     OR     A = 0; B = 0 
-clk = clock();
-    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 1 );
-    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase ^ pNew->fPhase );
-    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
-        (sint64)nBTLimit, (sint64)0, 
-        p->nBTLimitGlobal, p->nInsLimitGlobal );
-p->timeSat += clock() - clk;
-    if ( RetValue1 == l_False )
-    {
-p->timeSatUnsat += clock() - clk;
-        pLits[0] = lit_neg( pLits[0] );
-        pLits[1] = lit_neg( pLits[1] );
-        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
-        assert( RetValue );
-        p->nSatCallsUnsat++;
-    }
-    else if ( RetValue1 == l_True )
-    {
-p->timeSatSat += clock() - clk;
-        Fra_SmlSavePattern( p );
-        p->nSatCallsSat++;
-        return 0;
-    }
-    else // if ( RetValue1 == l_Undef )
-    {
-p->timeSatFail += clock() - clk;
-        // mark the node as the failed node
-        pOld->fMarkB = 1;
-        pNew->fMarkB = 1;
-        p->nSatFailsReal++;
-        return -1;
-    }
-/*
-    // check BDD proof
-    {
-        int RetVal;
-        PRT( "Sat", clock() - clk2 );
-        clk2 = clock();
-        RetVal = Fra_NodesAreEquivBdd( pOld, pNew );
-//        printf( "%d ", RetVal );
-        assert( RetVal );
-        PRT( "Bdd", clock() - clk2 );
-        printf( "\n" );
-    }
-*/
-    // return SAT proof
-    p->nSatProof++;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Runs the result of test for pObj => pNew.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR )
-{
-    int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
-    int status;
-
-    // make sure the nodes are not complemented
-    assert( !Aig_IsComplement(pNew) );
-    assert( !Aig_IsComplement(pOld) );
-    assert( pNew != pOld );
-
-    // if at least one of the nodes is a failed node, perform adjustments:
-    // if the backtrack limit is small, simply skip this node
-    // if the backtrack limit is > 10, take the quare root of the limit
-    nBTLimit = p->pPars->nBTLimitNode;
-/*
-    if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
-    {
-        p->nSatFails++;
-        // fail immediately
-//        return -1;
-        if ( nBTLimit <= 10 )
-            return -1;
-        nBTLimit = (int)pow(nBTLimit, 0.7);
-    }
-*/
-    p->nSatCalls++;
-
-    // make sure the solver is allocated and has enough variables
-    if ( p->pSat == NULL )
-    {
-        p->pSat = sat_solver_new();
-        p->nSatVars = 1;
-        sat_solver_setnvars( p->pSat, 1000 );
-        // var 0 is reserved for const1 node - add the clause
-        pLits[0] = toLit( 0 );
-        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
-    }
-
-    // if the nodes do not have SAT variables, allocate them
-    Fra_CnfNodeAddToSolver( p, pOld, pNew );
-
-    if ( p->pSat->qtail != p->pSat->qhead )
-    {
-        status = sat_solver_simplify(p->pSat);
-        assert( status != 0 );
-        assert( p->pSat->qtail == p->pSat->qhead );
-    }
-
-    // prepare variable activity
-    if ( p->pPars->fConeBias )
-        Fra_SetActivityFactors( p, pOld, pNew ); 
-
-    // solve under assumptions
-    // A = 1; B = 0     OR     A = 1; B = 1 
-clk = clock();
-//    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
-//    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
-    pLits[0] = toLitCond( Fra_ObjSatNum(pOld),  fComplL );
-    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), !fComplR );
-//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
-    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
-        (sint64)nBTLimit, (sint64)0, 
-        p->nBTLimitGlobal, p->nInsLimitGlobal );
-p->timeSat += clock() - clk;
-    if ( RetValue1 == l_False )
-    {
-p->timeSatUnsat += clock() - clk;
-        pLits[0] = lit_neg( pLits[0] );
-        pLits[1] = lit_neg( pLits[1] );
-        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
-        assert( RetValue );
-        // continue solving the other implication
-        p->nSatCallsUnsat++;
-    }
-    else if ( RetValue1 == l_True )
-    {
-p->timeSatSat += clock() - clk;
-        Fra_SmlSavePattern( p );
-        p->nSatCallsSat++;
-        return 0;
-    }
-    else // if ( RetValue1 == l_Undef )
-    {
-p->timeSatFail += clock() - clk;
-        // mark the node as the failed node
-        if ( pOld != p->pManFraig->pConst1 ) 
-            pOld->fMarkB = 1;
-        pNew->fMarkB = 1;
-        p->nSatFailsReal++;
-        return -1;
-    }
-    // return SAT proof
-    p->nSatProof++;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Runs equivalence test for one node.]
-
-  Description [Returns the fraiged node.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
-{
-    int pLits[2], RetValue1, RetValue, clk;
-
-    // make sure the nodes are not complemented
-    assert( !Aig_IsComplement(pNew) );
-    assert( pNew != p->pManFraig->pConst1 );
-    p->nSatCalls++;
-
-    // make sure the solver is allocated and has enough variables
-    if ( p->pSat == NULL )
-    {
-        p->pSat = sat_solver_new();
-        p->nSatVars = 1;
-        sat_solver_setnvars( p->pSat, 1000 );
-        // var 0 is reserved for const1 node - add the clause
-        pLits[0] = toLit( 0 );
-        sat_solver_addclause( p->pSat, pLits, pLits + 1 );
-    }
-
-    // if the nodes do not have SAT variables, allocate them
-    Fra_CnfNodeAddToSolver( p, NULL, pNew );
-
-    // prepare variable activity
-    if ( p->pPars->fConeBias )
-        Fra_SetActivityFactors( p, NULL, pNew ); 
-
-    // solve under assumptions
-clk = clock();
-    pLits[0] = toLitCond( Fra_ObjSatNum(pNew), pNew->fPhase );
-    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 1, 
-        (sint64)p->pPars->nBTLimitMiter, (sint64)0, 
-        p->nBTLimitGlobal, p->nInsLimitGlobal );
-p->timeSat += clock() - clk;
-    if ( RetValue1 == l_False )
-    {
-p->timeSatUnsat += clock() - clk;
-        pLits[0] = lit_neg( pLits[0] );
-        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 1 );
-        assert( RetValue );
-        // continue solving the other implication
-        p->nSatCallsUnsat++;
-    }
-    else if ( RetValue1 == l_True )
-    {
-p->timeSatSat += clock() - clk;
-        if ( p->pPatWords )
-            Fra_SmlSavePattern( p );
-        p->nSatCallsSat++;
-        return 0;
-    }
-    else // if ( RetValue1 == l_Undef )
-    {
-p->timeSatFail += clock() - clk;
-        // mark the node as the failed node
-        pNew->fMarkB = 1;
-        p->nSatFailsReal++;
-        return -1;
-    }
-
-    // return SAT proof
-    p->nSatProof++;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets variable activities in the cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_SetActivityFactors_rec( Fra_Man_t * p, Aig_Obj_t * pObj, int LevelMin, int LevelMax )
-{
-    Vec_Ptr_t * vFanins;
-    Aig_Obj_t * pFanin;
-    int i, Counter = 0;
-    assert( !Aig_IsComplement(pObj) );
-    assert( Fra_ObjSatNum(pObj) );
-    // skip visited variables
-    if ( Aig_ObjIsTravIdCurrent(p->pManFraig, pObj) )
-        return 0;
-    Aig_ObjSetTravIdCurrent(p->pManFraig, pObj);
-    // add the PI to the list
-    if ( pObj->Level <= (unsigned)LevelMin || Aig_ObjIsPi(pObj) )
-        return 0;
-    // set the factor of this variable
-    // (LevelMax-LevelMin) / (pObj->Level-LevelMin) = p->pPars->dActConeBumpMax / ThisBump
-    p->pSat->factors[Fra_ObjSatNum(pObj)] = p->pPars->dActConeBumpMax * (pObj->Level - LevelMin)/(LevelMax - LevelMin);
-    veci_push(&p->pSat->act_vars, Fra_ObjSatNum(pObj));
-    // explore the fanins
-    vFanins = Fra_ObjFaninVec( pObj );
-    Vec_PtrForEachEntry( vFanins, pFanin, i )
-        Counter += Fra_SetActivityFactors_rec( p, Aig_Regular(pFanin), LevelMin, LevelMax );
-    return 1 + Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Sets variable activities in the cone.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_SetActivityFactors( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
-{
-    int clk, LevelMin, LevelMax;
-    assert( pOld || pNew );
-clk = clock(); 
-    // reset the active variables
-    veci_resize(&p->pSat->act_vars, 0);
-    // prepare for traversal
-    Aig_ManIncrementTravId( p->pManFraig );
-    // determine the min and max level to visit
-    assert( p->pPars->dActConeRatio > 0 && p->pPars->dActConeRatio < 1 );
-    LevelMax = AIG_MAX( (pNew ? pNew->Level : 0), (pOld ? pOld->Level : 0) );
-    LevelMin = (int)(LevelMax * (1.0 - p->pPars->dActConeRatio));
-    // traverse
-    if ( pOld && !Aig_ObjIsConst1(pOld) )
-        Fra_SetActivityFactors_rec( p, pOld, LevelMin, LevelMax );
-    if ( pNew && !Aig_ObjIsConst1(pNew) )
-        Fra_SetActivityFactors_rec( p, pNew, LevelMin, LevelMax );
-//Fra_PrintActivity( p );
-p->timeTrav += clock() - clk;
-    return 1;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
deleted file mode 100644
index f9bbfe44..00000000
--- a/src/aig/fra/fraSec.c
+++ /dev/null
@@ -1,279 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraSec.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [New FRAIG package.]
-
-  Synopsis    [Performs SEC based on seq sweeping.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fraSec.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fra.h"
-#include "ioa.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_FraigSec2( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose )
-{
-    Aig_Man_t * pNew;
-    int nFrames, RetValue, nIter, clk, clkTotal = clock();
-    int fLatchCorr = 0;
-    if ( nFramesFix )
-    {
-        nFrames = nFramesFix;
-        // perform seq sweeping for one frame number
-        pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
-    }
-    else
-    {
-        // perform seq sweeping while increasing the number of frames
-        for ( nFrames = 1; ; nFrames++ )
-        {
-clk = clock();
-            pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
-            RetValue = Fra_FraigMiterStatus( pNew );
-            if ( fVerbose )
-            {
-                printf( "FRAMES %3d : Iters = %3d. ", nFrames, nIter );
-                if ( RetValue == 1 )
-                    printf( "UNSAT     " );
-                else
-                    printf( "UNDECIDED " );
-PRT( "Time", clock() - clk );
-            }
-            if ( RetValue != -1 )
-                break;
-            Aig_ManStop( pNew );
-        }
-    }
-
-    // get the miter status
-    RetValue = Fra_FraigMiterStatus( pNew );
-    Aig_ManStop( pNew );
-
-    // report the miter
-    if ( RetValue == 1 )
-        printf( "Networks are equivalent after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter );
-    else if ( RetValue == 0 )
-        printf( "Networks are NOT EQUIVALENT. " );
-    else
-        printf( "Networks are UNDECIDED after seq sweeping with K=%d frames (%d iters). ", nFrames, nIter );
-PRT( "Time", clock() - clkTotal );
-    return RetValue;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fVerbose, int fVeryVerbose )
-{
-    Fra_Sml_t * pSml;
-    Aig_Man_t * pNew, * pTemp;
-    int nFrames, RetValue, nIter, clk, clkTotal = clock();
-    int fLatchCorr = 0;
-
-    pNew = Aig_ManDup( p, 1 );
-    if ( fVerbose )
-    {
-        printf( "Original miter:       Latches = %5d. Nodes = %6d.\n", 
-            Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-    }
-//Aig_ManDumpBlif( pNew, "after.blif" );
-
-    // perform sequential cleanup
-clk = clock();
-    if ( pNew->nRegs )
-    pNew = Aig_ManReduceLaches( pNew, 0 );
-    if ( pNew->nRegs )
-    pNew = Aig_ManConstReduce( pNew, 0 );
-    if ( fVerbose )
-    {
-        printf( "Sequential cleanup:   Latches = %5d. Nodes = %6d. ", 
-            Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
-    }
-
-    // perform forward retiming
-    if ( fRetimeFirst && pNew->nRegs )
-    {
-clk = clock();
-    pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
-    Aig_ManStop( pTemp );
-    if ( fVerbose )
-    {
-        printf( "Forward retiming:     Latches = %5d. Nodes = %6d. ", 
-            Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
-    }
-    }
-    
-    // run latch correspondence
-clk = clock();
-    if ( pNew->nRegs )
-    {
-    pNew = Aig_ManDup( pTemp = pNew, 1 );
-    Aig_ManStop( pTemp );
-    pNew = Fra_FraigLatchCorrespondence( pTemp = pNew, 0, 100000, 1, fVeryVerbose, &nIter );
-    Aig_ManStop( pTemp );
-    if ( pNew == NULL )
-    {
-        RetValue = 0;
-        printf( "Networks are NOT EQUIVALENT after simulation.   " );
-PRT( "Time", clock() - clkTotal );
-        return RetValue;
-    }
-
-    if ( fVerbose )
-    {
-        printf( "Latch-corr (I=%3d):   Latches = %5d. Nodes = %6d. ", 
-            nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
-    }
-    }
-
-    // perform fraiging
-clk = clock();
-    pNew = Fra_FraigEquivence( pTemp = pNew, 100 );
-    Aig_ManStop( pTemp );
-    if ( fVerbose )
-    {
-        printf( "Fraiging:             Latches = %5d. Nodes = %6d. ", 
-            Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
-    }
-
-    // perform seq sweeping while increasing the number of frames
-    RetValue = Fra_FraigMiterStatus( pNew );
-    if ( RetValue == -1 )
-    for ( nFrames = 1; nFrames <= nFramesMax; nFrames *= 2 )
-    {
-clk = clock();
-        pNew = Fra_FraigInduction( pTemp = pNew, 0, nFrames, 0, 0, 0, fLatchCorr, 0, fVeryVerbose, &nIter );
-        Aig_ManStop( pTemp );
-        RetValue = Fra_FraigMiterStatus( pNew );
-        if ( fVerbose )
-        { 
-            printf( "K-step (K=%2d,I=%3d):  Latches = %5d. Nodes = %6d. ", 
-                nFrames, nIter, Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
-        }
-        if ( RetValue != -1 )
-            break;
-        // perform rewriting
-clk = clock();
-        pNew = Aig_ManDup( pTemp = pNew, 1 );
-        Aig_ManStop( pTemp );
-        pNew = Dar_ManRewriteDefault( pNew );
-        if ( fVerbose )
-        {
-            printf( "Rewriting:            Latches = %5d. Nodes = %6d. ", 
-                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
-        } 
-
-        // perform retiming
-clk = clock();
-        pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
-        Aig_ManStop( pTemp );
-        pNew = Aig_ManDup( pTemp = pNew, 1 );
-        Aig_ManStop( pTemp );
-        if ( fVerbose )
-        {
-            printf( "Forward retiming:     Latches = %5d. Nodes = %6d. ", 
-                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
-        }
-
-        if ( pNew->nRegs )
-        pNew = Aig_ManConstReduce( pNew, 0 );
-
-        // perform sequential simulation
-clk = clock();
-        pSml = Fra_SmlSimulateSeq( pNew, 0, 128 * nFrames, 1 + 16/(1+Aig_ManNodeNum(pNew)/1000) ); 
-        if ( fVerbose )
-        {
-            printf( "Seq simulation  :     Latches = %5d. Nodes = %6d. ", 
-                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
-        }
-        if ( pSml->fNonConstOut )
-        {
-            Fra_SmlStop( pSml );
-            Aig_ManStop( pNew );
-            RetValue = 0;
-            printf( "Networks are NOT EQUIVALENT after simulation.   " );
-PRT( "Time", clock() - clkTotal );
-            return RetValue;
-        }
-        Fra_SmlStop( pSml );
-    }
-
-    // get the miter status
-    RetValue = Fra_FraigMiterStatus( pNew );
-
-    // report the miter
-    if ( RetValue == 1 )
-    {
-        printf( "Networks are equivalent.   " );
-PRT( "Time", clock() - clkTotal );
-    }
-    else if ( RetValue == 0 )
-    {
-        printf( "Networks are NOT EQUIVALENT.   " );
-PRT( "Time", clock() - clkTotal );
-    }
-    else
-    {
-        static int Counter = 1;
-        char pFileName[1000];
-        printf( "Networks are UNDECIDED.   " );
-PRT( "Time", clock() - clkTotal );
-        sprintf( pFileName, "sm%03d.aig", Counter++ );
-        Ioa_WriteAiger( pNew, pFileName, 0 );
-        printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
-    }
-    Aig_ManStop( pNew );
-    return RetValue;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
deleted file mode 100644
index b77c775a..00000000
--- a/src/aig/fra/fraSim.c
+++ /dev/null
@@ -1,823 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fraSim.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [New FRAIG package.]
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fraSim.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Computes hash value of the node using its simulation info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize )
-{
-    Fra_Man_t * p = pObj->pData;
-    static int s_FPrimes[128] = { 
-        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
-        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
-        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
-        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
-        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
-        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
-        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
-        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
-        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
-        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
-        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
-        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
-        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
-    };
-    unsigned * pSims;
-    unsigned uHash;
-    int i;
-//    assert( p->pSml->nWordsTotal <= 128 );
-    uHash = 0;
-    pSims = Fra_ObjSim(p->pSml, pObj->Id);
-    for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
-        uHash ^= pSims[i] * s_FPrimes[i & 0x7F];
-    return uHash % nTableSize;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if simulation info is composed of all zeros.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_SmlNodeIsConst( Aig_Obj_t * pObj )
-{
-    Fra_Man_t * p = pObj->pData;
-    unsigned * pSims;
-    int i;
-    pSims = Fra_ObjSim(p->pSml, pObj->Id);
-    for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
-        if ( pSims[i] )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if simulation infos are equal.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
-{
-    Fra_Man_t * p = pObj0->pData;
-    unsigned * pSims0, * pSims1;
-    int i;
-    pSims0 = Fra_ObjSim(p->pSml, pObj0->Id);
-    pSims1 = Fra_ObjSim(p->pSml, pObj1->Id);
-    for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
-        if ( pSims0[i] != pSims1[i] )
-            return 0;
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts the number of 1s in the XOR of simulation data.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right )
-{
-    unsigned * pSimL, * pSimR;
-    int k, Counter = 0;
-    pSimL = Fra_ObjSim( p, Left );
-    pSimR = Fra_ObjSim( p, Right );
-    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
-        Counter += Aig_WordCountOnes( pSimL[k] ^ pSimR[k] );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if simulation info is composed of all zeros.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_SmlNodeIsZero( Fra_Sml_t * p, Aig_Obj_t * pObj )
-{
-    unsigned * pSims;
-    int i;
-    pSims = Fra_ObjSim(p, pObj->Id);
-    for ( i = p->nWordsPref; i < p->nWordsTotal; i++ )
-        if ( pSims[i] )
-            return 0;
-    return 1;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Generated const 0 pattern.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SmlSavePattern0( Fra_Man_t * p, int fInit )
-{
-    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [[Generated const 1 pattern.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SmlSavePattern1( Fra_Man_t * p, int fInit )
-{
-    Aig_Obj_t * pObj;
-    int i, k, nTruePis;
-    memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
-    if ( !fInit )
-        return;
-    // clear the state bits to correspond to all-0 initial state
-    nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
-    k = 0;
-    Aig_ManForEachLoSeq( p->pManAig, pObj, i )
-        Aig_InfoXorBit( p->pPatWords, nTruePis * p->nFramesAll + k++ );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Copy pattern from the solver into the internal storage.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SmlSavePattern( Fra_Man_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
-    Aig_ManForEachPi( p->pManFraig, pObj, i )
-        if ( p->pSat->model.ptr[Fra_ObjSatNum(pObj)] == l_True )
-            Aig_InfoSetBit( p->pPatWords, i );
-
-    if ( p->vCex )
-    {
-        Vec_IntClear( p->vCex );
-        for ( i = 0; i < Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig); i++ )
-            Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
-        for ( i = Aig_ManPiNum(p->pManFraig) - Aig_ManRegNum(p->pManFraig); i < Aig_ManPiNum(p->pManFraig); i++ )
-            Vec_IntPush( p->vCex, Aig_InfoHasBit( p->pPatWords, i ) );
-    }
-
-/*
-    printf( "Pattern: " );
-    Aig_ManForEachPi( p->pManFraig, pObj, i )
-        printf( "%d", Aig_InfoHasBit( p->pPatWords, i ) );
-    printf( "\n" );
-*/
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Creates the counter-example from the successful pattern.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj )
-{ 
-    unsigned * pSims;
-    int i, k, BestPat, * pModel;
-    // find the word of the pattern
-    pSims = Fra_ObjSim(p->pSml, pObj->Id);
-    for ( i = 0; i < p->pSml->nWordsTotal; i++ )
-        if ( pSims[i] )
-            break;
-    assert( i < p->pSml->nWordsTotal );
-    // find the bit of the pattern
-    for ( k = 0; k < 32; k++ )
-        if ( pSims[i] & (1 << k) )
-            break;
-    assert( k < 32 );
-    // determine the best pattern
-    BestPat = i * 32 + k;
-    // fill in the counter-example data
-    pModel = ALLOC( int, Aig_ManPiNum(p->pManFraig) );
-    Aig_ManForEachPi( p->pManAig, pObj, i )
-    {
-        pModel[i] = Aig_InfoHasBit(Fra_ObjSim(p->pSml, pObj->Id), BestPat);
-//        printf( "%d", pModel[i] );
-    }
-//    printf( "\n" );
-    // set the model
-    assert( p->pManFraig->pData == NULL );
-    p->pManFraig->pData = pModel;
-    return;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns 1 if the one of the output is already non-constant 0.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_SmlCheckOutput( Fra_Man_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    // make sure the reference simulation pattern does not detect the bug
-    pObj = Aig_ManPo( p->pManAig, 0 );
-    assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); 
-    Aig_ManForEachPo( p->pManAig, pObj, i )
-    {
-        if ( !Fra_SmlNodeIsConst( Aig_ObjFanin0(pObj) ) )
-        {
-            // create the counter-example from this pattern
-            Fra_SmlCheckOutputSavePattern( p, Aig_ObjFanin0(pObj) );
-            return 1;
-        }
-    }
-    return 0;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Assigns random patterns to the PI node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SmlAssignRandom( Fra_Sml_t * p, Aig_Obj_t * pObj )
-{
-    unsigned * pSims;
-    int i;
-    assert( Aig_ObjIsPi(pObj) );
-    pSims = Fra_ObjSim( p, pObj->Id );
-    for ( i = 0; i < p->nWordsTotal; i++ )
-        pSims[i] = Fra_ObjRandomSim();
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Assigns constant patterns to the PI node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SmlAssignConst( Fra_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame )
-{
-    unsigned * pSims;
-    int i;
-    assert( Aig_ObjIsPi(pObj) );
-    pSims = Fra_ObjSim( p, pObj->Id ) + p->nWordsFrame * iFrame;
-    for ( i = 0; i < p->nWordsFrame; i++ )
-        pSims[i] = fConst1? ~(unsigned)0 : 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Assings random simulation info for the PIs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SmlInitialize( Fra_Sml_t * p, int fInit )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    if ( fInit )
-    {
-        assert( Aig_ManRegNum(p->pAig) > 0 );
-        assert( Aig_ManRegNum(p->pAig) < Aig_ManPiNum(p->pAig) );
-        // assign random info for primary inputs
-        Aig_ManForEachPiSeq( p->pAig, pObj, i )
-            Fra_SmlAssignRandom( p, pObj );
-        // assign the initial state for the latches
-        Aig_ManForEachLoSeq( p->pAig, pObj, i )
-            Fra_SmlAssignConst( p, pObj, 0, 0 );
-    }
-    else
-    {
-        Aig_ManForEachPi( p->pAig, pObj, i )
-            Fra_SmlAssignRandom( p, pObj );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Assings distance-1 simulation info for the PIs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat )
-{
-    Aig_Obj_t * pObj;
-    int f, i, k, Limit, nTruePis;
-    assert( p->nFrames > 0 );
-    if ( p->nFrames == 1 )
-    {
-        // copy the PI info 
-        Aig_ManForEachPi( p->pAig, pObj, i )
-            Fra_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, i), 0 );
-        // flip one bit
-        Limit = AIG_MIN( Aig_ManPiNum(p->pAig), p->nWordsTotal * 32 - 1 );
-        for ( i = 0; i < Limit; i++ )
-            Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig,i)->Id ), i+1 );
-    }
-    else
-    {
-        int fUseDist1 = 0;
-
-        // copy the PI info for each frame
-        nTruePis = Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig);
-        for ( f = 0; f < p->nFrames; f++ )
-            Aig_ManForEachPiSeq( p->pAig, pObj, i )
-                Fra_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * f + i), f );
-        // copy the latch info 
-        k = 0;
-        Aig_ManForEachLoSeq( p->pAig, pObj, i )
-            Fra_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
-//        assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pManFraig) );
-
-        // flip one bit of the last frame
-        if ( fUseDist1 ) //&& p->nFrames == 2 )
-        {
-            Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 );
-            for ( i = 0; i < Limit; i++ )
-                Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ) + p->nWordsFrame*(p->nFrames-1), i+1 );
-        }
-    }
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SmlNodeSimulate( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
-{
-    unsigned * pSims, * pSims0, * pSims1;
-    int fCompl, fCompl0, fCompl1, i;
-    assert( !Aig_IsComplement(pObj) );
-    assert( Aig_ObjIsNode(pObj) );
-    assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
-    // get hold of the simulation information
-    pSims  = Fra_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame;
-    pSims0 = Fra_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + p->nWordsFrame * iFrame;
-    pSims1 = Fra_ObjSim(p, Aig_ObjFanin1(pObj)->Id) + p->nWordsFrame * iFrame;
-    // get complemented attributes of the children using their random info
-    fCompl  = pObj->fPhase;
-    fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
-    fCompl1 = Aig_ObjPhaseReal(Aig_ObjChild1(pObj));
-    // simulate
-    if ( fCompl0 && fCompl1 )
-    {
-        if ( fCompl )
-            for ( i = 0; i < p->nWordsFrame; i++ )
-                pSims[i] = (pSims0[i] | pSims1[i]);
-        else
-            for ( i = 0; i < p->nWordsFrame; i++ )
-                pSims[i] = ~(pSims0[i] | pSims1[i]);
-    }
-    else if ( fCompl0 && !fCompl1 )
-    {
-        if ( fCompl )
-            for ( i = 0; i < p->nWordsFrame; i++ )
-                pSims[i] = (pSims0[i] | ~pSims1[i]);
-        else
-            for ( i = 0; i < p->nWordsFrame; i++ )
-                pSims[i] = (~pSims0[i] & pSims1[i]);
-    }
-    else if ( !fCompl0 && fCompl1 )
-    {
-        if ( fCompl )
-            for ( i = 0; i < p->nWordsFrame; i++ )
-                pSims[i] = (~pSims0[i] | pSims1[i]);
-        else
-            for ( i = 0; i < p->nWordsFrame; i++ )
-                pSims[i] = (pSims0[i] & ~pSims1[i]);
-    }
-    else // if ( !fCompl0 && !fCompl1 )
-    {
-        if ( fCompl )
-            for ( i = 0; i < p->nWordsFrame; i++ )
-                pSims[i] = ~(pSims0[i] & pSims1[i]);
-        else
-            for ( i = 0; i < p->nWordsFrame; i++ )
-                pSims[i] = (pSims0[i] & pSims1[i]);
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SmlNodeCopyFanin( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
-{
-    unsigned * pSims, * pSims0;
-    int fCompl, fCompl0, i;
-    assert( !Aig_IsComplement(pObj) );
-    assert( Aig_ObjIsPo(pObj) );
-    assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
-    // get hold of the simulation information
-    pSims  = Fra_ObjSim(p, pObj->Id) + p->nWordsFrame * iFrame;
-    pSims0 = Fra_ObjSim(p, Aig_ObjFanin0(pObj)->Id) + p->nWordsFrame * iFrame;
-    // get complemented attributes of the children using their random info
-    fCompl  = pObj->fPhase;
-    fCompl0 = Aig_ObjPhaseReal(Aig_ObjChild0(pObj));
-    // copy information as it is
-    if ( fCompl0 )
-        for ( i = 0; i < p->nWordsFrame; i++ )
-            pSims[i] = ~pSims0[i];
-    else
-        for ( i = 0; i < p->nWordsFrame; i++ )
-            pSims[i] = pSims0[i];
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SmlNodeTransferNext( Fra_Sml_t * p, Aig_Obj_t * pOut, Aig_Obj_t * pIn, int iFrame )
-{
-    unsigned * pSims0, * pSims1;
-    int i;
-    assert( !Aig_IsComplement(pOut) );
-    assert( !Aig_IsComplement(pIn) );
-    assert( Aig_ObjIsPo(pOut) );
-    assert( Aig_ObjIsPi(pIn) );
-    assert( iFrame == 0 || p->nWordsFrame < p->nWordsTotal );
-    // get hold of the simulation information
-    pSims0 = Fra_ObjSim(p, pOut->Id) + p->nWordsFrame * iFrame;
-    pSims1 = Fra_ObjSim(p, pIn->Id) + p->nWordsFrame * (iFrame+1);
-    // copy information as it is
-    for ( i = 0; i < p->nWordsFrame; i++ )
-        pSims1[i] = pSims0[i];
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Check if any of the POs becomes non-constant.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Fra_SmlCheckNonConstOutputs( Fra_Sml_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    Aig_ManForEachPoSeq( p->pAig, pObj, i )
-        if ( !Fra_SmlNodeIsZero(p, pObj) )
-            return 1;
-    return 0;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Simulates AIG manager.]
-
-  Description [Assumes that the PI simulation info is attached.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SmlSimulateOne( Fra_Sml_t * p )
-{
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    int f, i, clk;
-clk = clock();
-    for ( f = 0; f < p->nFrames; f++ )
-    {
-        // simulate the nodes
-        Aig_ManForEachNode( p->pAig, pObj, i )
-            Fra_SmlNodeSimulate( p, pObj, f );
-        // copy simulation info into outputs
-        Aig_ManForEachPoSeq( p->pAig, pObj, i )
-            Fra_SmlNodeCopyFanin( p, pObj, f );
-        // quit if this is the last timeframe
-        if ( f == p->nFrames - 1 )
-            break;
-        // copy simulation info into outputs
-        Aig_ManForEachLiSeq( p->pAig, pObj, i )
-            Fra_SmlNodeCopyFanin( p, pObj, f );
-        // copy simulation info into the inputs
-        Aig_ManForEachLiLoSeq( p->pAig, pObjLi, pObjLo, i )
-            Fra_SmlNodeTransferNext( p, pObjLi, pObjLo, f );
-    }
-p->timeSim += clock() - clk;
-p->nSimRounds++;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Resimulates fraiging manager after finding a counter-example.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SmlResimulate( Fra_Man_t * p )
-{
-    int nChanges, clk;
-    Fra_SmlAssignDist1( p->pSml, p->pPatWords );
-    Fra_SmlSimulateOne( p->pSml );
-//    if ( p->pPars->fPatScores )
-//        Fra_CleanPatScores( p );
-    if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
-        return;
-clk = clock();
-    nChanges = Fra_ClassesRefine( p->pCla );
-    nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
-    if ( p->pCla->vImps )
-        nChanges += Fra_ImpRefineUsingCex( p, p->pCla->vImps );
-p->timeRef += clock() - clk;
-    if ( !p->pPars->nFramesK && nChanges < 1 )
-        printf( "Error: A counter-example did not refine classes!\n" );
-//    assert( nChanges >= 1 );
-//printf( "Refined classes = %5d.   Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs simulation of the manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SmlSimulate( Fra_Man_t * p, int fInit )
-{
-    int fVerbose = 0;
-    int nChanges, nClasses, clk;
-    assert( !fInit || Aig_ManRegNum(p->pManAig) );
-    // start the classes
-    Fra_SmlInitialize( p->pSml, fInit );
-    Fra_SmlSimulateOne( p->pSml );
-    Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
-//    Fra_ClassesPrint( p->pCla, 0 );
-if ( fVerbose )
-printf( "Starting classes = %5d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
-
-//return;
-
-    // refine classes by walking 0/1 patterns
-    Fra_SmlSavePattern0( p, fInit );
-    Fra_SmlAssignDist1( p->pSml, p->pPatWords );
-    Fra_SmlSimulateOne( p->pSml );
-    if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
-        return;
-clk = clock();
-    nChanges = Fra_ClassesRefine( p->pCla );
-    nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
-p->timeRef += clock() - clk;
-if ( fVerbose )
-printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
-    Fra_SmlSavePattern1( p, fInit );
-    Fra_SmlAssignDist1( p->pSml, p->pPatWords );
-    Fra_SmlSimulateOne( p->pSml );
-    if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
-        return;
-clk = clock();
-    nChanges = Fra_ClassesRefine( p->pCla );
-    nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
-p->timeRef += clock() - clk;
-
-if ( fVerbose )
-printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
-    // refine classes by random simulation
-    do {
-        Fra_SmlInitialize( p->pSml, fInit );
-        Fra_SmlSimulateOne( p->pSml );
-        nClasses = Vec_PtrSize(p->pCla->vClasses);
-        if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
-            return;
-clk = clock();
-        nChanges = Fra_ClassesRefine( p->pCla );
-        nChanges += Fra_ClassesRefine1( p->pCla, 1, NULL );
-p->timeRef += clock() - clk;
-if ( fVerbose )
-printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
-    } while ( (double)nChanges / nClasses > p->pPars->dSimSatur );
-
-//    if ( p->pPars->fVerbose )
-//    printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", 
-//        Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
-//    Fra_ClassesPrint( p->pCla, 0 );
-}
- 
-
-/**Function*************************************************************
-
-  Synopsis    [Allocates simulation manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )
-{
-    Fra_Sml_t * p;
-    p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * Aig_ManObjNumMax(pAig) * (nPref + nFrames) * nWordsFrame );
-    memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
-    p->pAig        = pAig;
-    p->nPref       = nPref;
-    p->nFrames     = nPref + nFrames;
-    p->nWordsFrame = nWordsFrame;
-    p->nWordsTotal = (nPref + nFrames) * nWordsFrame;
-    p->nWordsPref  = nPref * nWordsFrame;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Deallocates simulation manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Fra_SmlStop( Fra_Sml_t * p )
-{
-    free( p );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Performs simulation of the uninitialized circuit.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords )
-{
-    Fra_Sml_t * p;
-    p = Fra_SmlStart( pAig, 0, 1, nWords );
-    Fra_SmlInitialize( p, 0 );
-    Fra_SmlSimulateOne( p );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs simulation of the initialized circuit.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords )
-{
-    Fra_Sml_t * p;
-    p = Fra_SmlStart( pAig, nPref, nFrames, nWords );
-    Fra_SmlInitialize( p, 1 );
-    Fra_SmlSimulateOne( p );
-    p->fNonConstOut = Fra_SmlCheckNonConstOutputs( p );
-    return p;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/fra/fra_.c b/src/aig/fra/fra_.c
deleted file mode 100644
index 2b601587..00000000
--- a/src/aig/fra/fra_.c
+++ /dev/null
@@ -1,48 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [fra_.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [New FRAIG package.]
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 30, 2007.]
-
-  Revision    [$Id: fra_.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "fra.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/fra/module.make b/src/aig/fra/module.make
deleted file mode 100644
index e7264fdc..00000000
--- a/src/aig/fra/module.make
+++ /dev/null
@@ -1,12 +0,0 @@
-SRC +=    src/aig/fra/fraBmc.c \
-    src/aig/fra/fraCec.c \
-    src/aig/fra/fraClass.c \
-    src/aig/fra/fraCnf.c \
-    src/aig/fra/fraCore.c \
-    src/aig/fra/fraImp.c \
-    src/aig/fra/fraInd.c \
-    src/aig/fra/fraLcr.c \
-    src/aig/fra/fraMan.c \
-    src/aig/fra/fraSat.c \
-    src/aig/fra/fraSec.c \
-    src/aig/fra/fraSim.c