Isolating BMC code into a separate package.

7 files changed, 2 insertions, 3408 deletions

diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index a3231929..97b69363 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -1,8 +1,4 @@
-SRC +=  src/aig/saig/saigBmc.c \
-    src/aig/saig/saigBmc2.c \
-    src/aig/saig/saigBmc3.c \
-    src/aig/saig/saigCexMin.c \
-    src/aig/saig/saigCone.c \
+SRC +=  src/aig/saig/saigCone. \
     src/aig/saig/saigConstr.c \
     src/aig/saig/saigConstr2.c \
     src/aig/saig/saigDual.c \
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index 8823dcac..836a2051 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -50,26 +50,6 @@ struct Sec_MtrStatus_t_
     int         iOut;         // the satisfied output
 }; 
  
-typedef struct Saig_ParBmc_t_ Saig_ParBmc_t;
-struct Saig_ParBmc_t_
-{
-    int         nStart;         // starting timeframe
-    int         nFramesMax;     // maximum number of timeframes 
-    int         nConfLimit;     // maximum number of conflicts at a node
-    int         nConfLimitJump; // maximum number of conflicts after jumping
-    int         nFramesJump;    // the number of tiemframes to jump
-    int         nTimeOut;       // approximate timeout in seconds
-    int         nPisAbstract;   // the number of PIs to abstract
-    int         fSolveAll;      // does not stop at the first SAT output
-    int         fDropSatOuts;   // replace sat outputs by constant 0
-    int         nFfToAddMax;    // max number of flops to add during CBA
-    int         fSkipRand;      // skip random decisions
-    int         fVerbose;       // verbose 
-    int         iFrame;         // explored up to this frame
-    int         nFailOuts;      // the number of failed outputs
-};
-
- 
 typedef struct Saig_ParBbr_t_ Saig_ParBbr_t;
 struct Saig_ParBbr_t_
 {
@@ -126,14 +106,6 @@ static inline int          Saig_ObjRegId( Aig_Man_t * p, Aig_Obj_t * pObj )   {
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== saigBmc.c ==========================================================*/
-extern int               Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nBTLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit );
-extern int               Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent );
-/*=== saigBmc3.c ==========================================================*/
-extern void              Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p );
-extern int               Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars );
-/*=== saigCexMin.c ==========================================================*/
-extern Abc_Cex_t *       Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex );
 /*=== saigCone.c ==========================================================*/
 extern void              Saig_ManPrintCones( Aig_Man_t * p );
 /*=== saigConstr.c ==========================================================*/
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
deleted file mode 100644
index f88d3162..00000000
--- a/src/aig/saig/saigBmc.c
+++ /dev/null
@@ -1,338 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [saigBmc.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Sequential AIG package.]
-
-  Synopsis    [Simple BMC package.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: saigBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "saig.h"
-#include "proof/fra/fra.h"
-#include "sat/cnf/cnf.h"
-#include "sat/bsat/satStore.h"
-
-ABC_NAMESPACE_IMPL_START
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Create timeframes of the manager for BMC.]
-
-  Description [The resulting manager is combinational. POs correspond to \
-  the property outputs in each time-frame.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
-{
-    Aig_Man_t * pFrames;
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    int i, f;
-    assert( Saig_ManRegNum(pAig) > 0 );
-    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
-    // map the constant node
-    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
-    // create variables for register outputs
-    Saig_ManForEachLo( pAig, pObj, i )
-        pObj->pData = Aig_ManConst0( pFrames );
-    // add timeframes
-    for ( f = 0; f < nFrames; f++ )
-    {
-        // create PI nodes for this frame
-        Saig_ManForEachPi( pAig, pObj, i )
-            pObj->pData = Aig_ObjCreateCi( pFrames );
-        // add internal nodes of this frame
-        Aig_ManForEachNode( pAig, pObj, i )
-            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-        // create POs for this frame
-        Saig_ManForEachPo( pAig, pObj, i )
-            Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
-        if ( f == nFrames - 1 )
-            break;
-        // save register inputs
-        Saig_ManForEachLi( pAig, pObj, i )
-            pObj->pData = Aig_ObjChild0Copy(pObj);
-        // transfer to register outputs
-        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
-            pObjLo->pData = pObjLi->pData;
-    }
-    Aig_ManCleanup( pFrames );
-    return pFrames;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the number of internal nodes that are not counted yet.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
-{
-    if ( !Aig_ObjIsNode(pObj) )
-        return 0;
-    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-        return 0;
-    Aig_ObjSetTravIdCurrent(p, pObj);
-    return 1 + Saig_ManFramesCount_rec( p, Aig_ObjFanin0(pObj) ) + 
-        Saig_ManFramesCount_rec( p, Aig_ObjFanin1(pObj) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Create timeframes of the manager for BMC.]
-
-  Description [The resulting manager is combinational. POs correspond to 
-  the property outputs in each time-frame.
-  The unrolling is stopped as soon as the number of nodes in the frames
-  exceeds the given maximum size.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax )
-{
-    Aig_Man_t * pFrames;
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo, * pObjPo;
-    int i, f, Counter = 0;
-    assert( Saig_ManRegNum(pAig) > 0 );
-    pFrames = Aig_ManStart( nSizeMax );
-    Aig_ManIncrementTravId( pFrames );
-    // map the constant node
-    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
-    // create variables for register outputs
-    Saig_ManForEachLo( pAig, pObj, i )
-        pObj->pData = Aig_ManConst0( pFrames );
-    // add timeframes
-    Counter = 0;
-    for ( f = 0; f < nFrames; f++ )
-    {
-        // create PI nodes for this frame
-        Saig_ManForEachPi( pAig, pObj, i )
-            pObj->pData = Aig_ObjCreateCi( pFrames );
-        // add internal nodes of this frame
-        Aig_ManForEachNode( pAig, pObj, i )
-            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-        // create POs for this frame
-        Saig_ManForEachPo( pAig, pObj, i )
-        {
-            pObjPo = Aig_ObjCreateCo( pFrames, Aig_ObjChild0Copy(pObj) );
-            Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) );
-        }
-        if ( Counter >= nSizeMax )
-        {
-            Aig_ManCleanup( pFrames );
-            return pFrames;
-        }
-        if ( f == nFrames - 1 )
-            break;
-        // save register inputs
-        Saig_ManForEachLi( pAig, pObj, i )
-            pObj->pData = Aig_ObjChild0Copy(pObj);
-        // transfer to register outputs
-        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
-            pObjLo->pData = pObjLi->pData;
-    }
-    Aig_ManCleanup( pFrames );
-    return pFrames;
-}
-
-ABC_NAMESPACE_IMPL_END
-
-#include "misc/util/utilMem.h"
-
-ABC_NAMESPACE_IMPL_START
-
- 
-/**Function*************************************************************
-
-  Synopsis    [Performs BMC for the given AIG.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame, int nCofFanLit )
-{
-    extern Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit );
-    sat_solver * pSat;
-    Cnf_Dat_t * pCnf;
-    Aig_Man_t * pFrames, * pAigTemp;
-    Aig_Obj_t * pObj;
-    int status, Lit, i, RetValue = -1;
-    clock_t clk;
-
-    // derive the timeframes
-    clk = clock();
-    if ( nCofFanLit )
-    {
-        pFrames = Gia_ManCofactorAig( pAig, nFrames, nCofFanLit );
-        if ( pFrames == NULL )
-            return -1;
-    }
-    else if ( nSizeMax > 0 )
-    {
-        pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax );
-        nFrames = Aig_ManCoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManCoNum(pFrames) % Saig_ManPoNum(pAig)) > 0);
-    }
-    else
-        pFrames = Saig_ManFramesBmc( pAig, nFrames );
-    if ( piFrame )
-        *piFrame = nFrames;
-    if ( fVerbose )
-    {
-        printf( "Running \"bmc\". AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
-            Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
-            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
-        printf( "Time-frames (%d):  PI/PO = %d/%d.  Node = %6d. Lev = %5d.  ", 
-            nFrames, Aig_ManCiNum(pFrames), Aig_ManCoNum(pFrames), 
-            Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
-        ABC_PRT( "Time", clock() - clk );
-        fflush( stdout );
-    }
-    // rewrite the timeframes
-    if ( fRewrite )
-    {
-        clk = clock();
-//        pFrames = Dar_ManBalance( pAigTemp = pFrames, 0 );
-        pFrames = Dar_ManRwsat( pAigTemp = pFrames, 1, 0 );
-        Aig_ManStop( pAigTemp );
-        if ( fVerbose )
-        {
-            printf( "Time-frames after rewriting:  Node = %6d. Lev = %5d.  ", 
-                Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
-            ABC_PRT( "Time", clock() - clk );
-            fflush( stdout );
-        }
-    }
-    // create the SAT solver
-    clk = clock();
-    pCnf = Cnf_Derive( pFrames, Aig_ManCoNum(pFrames) );  
-//if ( s_fInterrupt )
-//return -1;
-    pSat = sat_solver_new();
-    sat_solver_setnvars( pSat, pCnf->nVars );
-    for ( i = 0; i < pCnf->nClauses; i++ )
-    {
-        if ( !sat_solver_addclause( pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
-            assert( 0 );
-    }
-    if ( fVerbose )
-    {
-        printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
-        ABC_PRT( "Time", clock() - clk );
-        fflush( stdout );
-    }
-    status = sat_solver_simplify(pSat);
-    if ( status == 0 )
-    {
-        if ( fVerbose )
-        {
-            printf( "The BMC problem is trivially UNSAT\n" );
-            fflush( stdout );
-        }
-    }
-    else
-    {
-        clock_t clkPart = clock();
-        Aig_ManForEachCo( pFrames, pObj, i )
-        {
-//if ( s_fInterrupt )
-//return -1;
-            Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
-            if ( fVerbose )
-            {
-                printf( "Solving output %2d of frame %3d ... \r", 
-                    i % Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
-            }
-            clk = clock();
-            status = sat_solver_solve( pSat, &Lit, &Lit + 1, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-            if ( fVerbose && (i % Saig_ManPoNum(pAig) == Saig_ManPoNum(pAig) - 1) )
-            {
-                printf( "Solved %2d outputs of frame %3d.  ", 
-                    Saig_ManPoNum(pAig), i / Saig_ManPoNum(pAig) );
-                printf( "Conf =%8.0f. Imp =%11.0f. ", (double)pSat->stats.conflicts, (double)pSat->stats.propagations );
-                ABC_PRT( "T", clock() - clkPart );
-                clkPart = clock();
-                fflush( stdout );
-            }
-            if ( status == l_False )
-            {
-/*
-                Lit = lit_neg( Lit );
-                RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
-                assert( RetValue );
-                if ( pSat->qtail != pSat->qhead )
-                {
-                    RetValue = sat_solver_simplify(pSat);
-                    assert( RetValue );
-                }
-*/
-            }
-            else if ( status == l_True )
-            {
-                Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
-                int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
-                pModel[Aig_ManCiNum(pFrames)] = pObj->Id;
-                pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel );
-                ABC_FREE( pModel );
-                Vec_IntFree( vCiIds );
-
-                if ( piFrame )
-                    *piFrame = i / Saig_ManPoNum(pAig);
-                RetValue = 0;
-                break;
-            }
-            else
-            {
-                if ( piFrame )
-                    *piFrame = i / Saig_ManPoNum(pAig);
-                RetValue = -1;
-                break;
-            }
-        }
-    }
-    sat_solver_delete( pSat );
-    Cnf_DataFree( pCnf );
-    Aig_ManStop( pFrames );
-    return RetValue;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
deleted file mode 100644
index 7d4bfdd2..00000000
--- a/src/aig/saig/saigBmc2.c
+++ /dev/null
@@ -1,884 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [saigBmc.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Sequential AIG package.]
-
-  Synopsis    [Simple BMC package.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: saigBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "saig.h"
-#include "sat/cnf/cnf.h"
-#include "sat/bsat/satStore.h"
-#include "proof/ssw/ssw.h"
-
-ABC_NAMESPACE_IMPL_START
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-//#define AIG_VISITED       ((Aig_Obj_t *)(ABC_PTRUINT_T)1)
-
-typedef struct Saig_Bmc_t_ Saig_Bmc_t;
-struct Saig_Bmc_t_
-{
-    // parameters
-    int                   nFramesMax;     // the max number of timeframes to consider
-    int                   nNodesMax;      // the max number of nodes to add
-    int                   nConfMaxOne;    // the max number of conflicts at a target
-    int                   nConfMaxAll;    // the max number of conflicts for all targets
-    int                   fVerbose;       // enables verbose output
-    // AIG managers
-    Aig_Man_t *           pAig;           // the user's AIG manager
-    Aig_Man_t *           pFrm;           // Frames manager
-    Vec_Int_t *           vVisited;       // nodes visited in Frames
-    // node mapping
-    int                   nObjs;          // the largest number of an AIG object
-    Vec_Ptr_t *           vAig2Frm;       // mapping of AIG nodees into Frames nodes
-    // SAT solver
-    sat_solver *          pSat;           // SAT solver
-    int                   nSatVars;       // the number of used SAT variables
-    Vec_Int_t *           vObj2Var;       // mapping of frames objects in CNF variables
-    int                   nStitchVars;
-    // subproblems
-    Vec_Ptr_t *           vTargets;       // targets to be solved in this interval
-    int                   iFramePrev;     // previous frame  
-    int                   iFrameLast;     // last frame  
-    int                   iOutputLast;    // last output
-    int                   iFrameFail;     // failed frame 
-    int                   iOutputFail;    // failed output
-};
-
-static inline Aig_Obj_t * Saig_BmcObjFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )                       
-{ 
-//    return (Aig_Obj_t *)Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id );     
-    Aig_Obj_t * pRes;
-    Vec_Int_t * vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vAig2Frm, i );
-    int iObjLit = Vec_IntEntry( vFrame, Aig_ObjId(pObj) );
-    if ( iObjLit == -1 )
-        return NULL;
-    pRes = Aig_ManObj( p->pFrm, Abc_Lit2Var(iObjLit) );
-    if ( pRes == NULL )
-        Vec_IntWriteEntry( vFrame, Aig_ObjId(pObj), -1 );
-    else
-        pRes = Aig_NotCond( pRes, Abc_LitIsCompl(iObjLit) );
-    return pRes;
-}
-static inline void        Saig_BmcObjSetFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) 
-{
-//    Vec_PtrSetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id, pNode );     
-    Vec_Int_t * vFrame;
-    int iObjLit;
-    if ( i == Vec_PtrSize(p->vAig2Frm) )
-        Vec_PtrPush( p->vAig2Frm, Vec_IntStartFull(p->nObjs) );
-    assert( i < Vec_PtrSize(p->vAig2Frm) );
-    vFrame = (Vec_Int_t *)Vec_PtrEntry( p->vAig2Frm, i );
-    if ( pNode == NULL )
-        iObjLit = -1;
-    else
-        iObjLit = Abc_Var2Lit( Aig_ObjId(Aig_Regular(pNode)), Aig_IsComplement(pNode) );
-    Vec_IntWriteEntry( vFrame, Aig_ObjId(pObj), iObjLit );
-}
-
-static inline Aig_Obj_t * Saig_BmcObjChild0( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )                   { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin0(pObj), i), Aig_ObjFaninC0(pObj));  }
-static inline Aig_Obj_t * Saig_BmcObjChild1( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )                   { assert( !Aig_IsComplement(pObj) ); return Aig_NotCond(Saig_BmcObjFrame(p, Aig_ObjFanin1(pObj), i), Aig_ObjFaninC1(pObj));  }
-
-static inline int         Saig_BmcSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj )                             { return Vec_IntGetEntry( p->vObj2Var, pObj->Id );  }
-static inline void        Saig_BmcSetSatNum( Saig_Bmc_t * p, Aig_Obj_t * pObj, int Num )                 { Vec_IntSetEntry(p->vObj2Var, pObj->Id, Num);      }
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-#define ABS_ZER 1
-#define ABS_ONE 2
-#define ABS_UND 3
-
-static inline int Abs_ManSimInfoNot( int Value )
-{
-    if ( Value == ABS_ZER )
-        return ABS_ONE;
-    if ( Value == ABS_ONE )
-        return ABS_ZER;
-    return ABS_UND;
-}
-
-static inline int Abs_ManSimInfoAnd( int Value0, int Value1 )
-{
-    if ( Value0 == ABS_ZER || Value1 == ABS_ZER )
-        return ABS_ZER;
-    if ( Value0 == ABS_ONE && Value1 == ABS_ONE )
-        return ABS_ONE;
-    return ABS_UND;
-}
-
-static inline int Abs_ManSimInfoGet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame )
-{
-    unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, iFrame );
-    return 3 & (pInfo[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1));
-}
-
-static inline void Abs_ManSimInfoSet( Vec_Ptr_t * vSimInfo, Aig_Obj_t * pObj, int iFrame, int Value )
-{
-    unsigned * pInfo = (unsigned *)Vec_PtrEntry( vSimInfo, iFrame );
-    assert( Value >= ABS_ZER && Value <= ABS_UND );
-    Value ^= Abs_ManSimInfoGet( vSimInfo, pObj, iFrame );
-    pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs ternary simulation for one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abs_ManExtendOneEval_rec( Vec_Ptr_t * vSimInfo, Aig_Man_t * p, Aig_Obj_t * pObj, int iFrame )
-{
-    int Value0, Value1, Value;
-    Value = Abs_ManSimInfoGet( vSimInfo, pObj, iFrame );
-    if ( Value )
-        return Value;
-    if ( Aig_ObjIsCi(pObj) )
-    {
-        assert( Saig_ObjIsLo(p, pObj) );
-        Value = Abs_ManExtendOneEval_rec( vSimInfo, p, Saig_ObjLoToLi(p, pObj), iFrame-1 );
-        Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
-        return Value;
-    }
-    Value0 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin0(pObj), iFrame );
-    if ( Aig_ObjFaninC0(pObj) )
-        Value0 = Abs_ManSimInfoNot( Value0 );
-    if ( Aig_ObjIsCo(pObj) )
-    {
-        Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value0 );
-        return Value0;
-    }
-    assert( Aig_ObjIsNode(pObj) );
-    if ( Value0 == ABS_ZER )
-        Value = ABS_ZER;
-    else
-    {
-        Value1 = Abs_ManExtendOneEval_rec( vSimInfo, p, Aig_ObjFanin1(pObj), iFrame );
-        if ( Aig_ObjFaninC1(pObj) )
-            Value1 = Abs_ManSimInfoNot( Value1 );
-        Value = Abs_ManSimInfoAnd( Value0, Value1 );
-    }
-    Abs_ManSimInfoSet( vSimInfo, pObj, iFrame, Value );
-    assert( Value );
-    return Value;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs ternary simulation for one design.]
-
-  Description [The returned array contains the result of ternary 
-  simulation for all the frames where the output could be proved 0.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Abs_ManTernarySimulate( Aig_Man_t * p, int nFramesMax, int fVerbose )
-{
-    Vec_Ptr_t * vSimInfo;
-    Aig_Obj_t * pObj;
-    int i, f, nFramesLimit, nFrameWords;
-    clock_t clk = clock();
-    assert( Aig_ManRegNum(p) > 0 );
-    // the maximum number of frames will be determined to use at most 200Mb of RAM
-    nFramesLimit = 1 + (200000000 * 4)/Aig_ManObjNum(p);
-    nFramesLimit = Abc_MinInt( nFramesLimit, nFramesMax );
-    nFrameWords  = Abc_BitWordNum( 2 * Aig_ManObjNum(p) );
-    // allocate simulation info
-    vSimInfo = Vec_PtrAlloc( nFramesLimit );
-    for ( f = 0; f < nFramesLimit; f++ )
-    {
-        Vec_PtrPush( vSimInfo, ABC_CALLOC(unsigned, nFrameWords) );
-        if ( f == 0 ) 
-        {
-            Saig_ManForEachLo( p, pObj, i )
-                Abs_ManSimInfoSet( vSimInfo, pObj, 0, ABS_ZER );
-        }
-        Abs_ManSimInfoSet( vSimInfo, Aig_ManConst1(p), f, ABS_ONE );
-        Saig_ManForEachPi( p, pObj, i )
-            Abs_ManSimInfoSet( vSimInfo, pObj, f, ABS_UND );
-        Saig_ManForEachPo( p, pObj, i )
-            Abs_ManExtendOneEval_rec( vSimInfo, p, pObj, f );
-        // check if simulation has derived at least one fail or unknown
-        Saig_ManForEachPo( p, pObj, i )
-            if ( Abs_ManSimInfoGet(vSimInfo, pObj, f) != ABS_ZER )
-            {
-                if ( fVerbose )
-                {
-                    printf( "Ternary sim found non-zero output in frame %d.  Used %5.2f MB.  ", 
-                        f, 0.25 * (f+1) * Aig_ManObjNum(p) / (1<<20) );
-                    ABC_PRT( "Time", clock() - clk );
-                }
-                return vSimInfo;
-            }
-    }
-    if ( fVerbose )
-    {
-        printf( "Ternary sim proved all outputs in the first %d frames.  Used %5.2f MB.  ", 
-            nFramesLimit, 0.25 * nFramesLimit * Aig_ManObjNum(p) / (1<<20) );
-        ABC_PRT( "Time", clock() - clk );
-    }
-    return vSimInfo;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Free the array of simulation info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Abs_ManFreeAray( Vec_Ptr_t * p )
-{
-    void * pTemp;
-    int i;
-    Vec_PtrForEachEntry( void *, p, pTemp, i )
-        ABC_FREE( pTemp );
-    Vec_PtrFree( p );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Create manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConfMaxOne, int nConfMaxAll, int fVerbose )
-{
-    Saig_Bmc_t * p;
-    Aig_Obj_t * pObj;
-    int i, Lit;
-//    assert( Aig_ManRegNum(pAig) > 0 );
-    p = (Saig_Bmc_t *)ABC_ALLOC( char, sizeof(Saig_Bmc_t) );
-    memset( p, 0, sizeof(Saig_Bmc_t) );
-    // set parameters
-    p->nFramesMax   = nFramesMax;
-    p->nNodesMax    = nNodesMax;
-    p->nConfMaxOne  = nConfMaxOne;
-    p->nConfMaxAll  = nConfMaxAll;
-    p->fVerbose     = fVerbose;
-    p->pAig         = pAig;
-    p->nObjs        = Aig_ManObjNumMax(pAig);
-    // create node and variable mappings
-    p->vAig2Frm     = Vec_PtrAlloc( 100 );
-    p->vObj2Var     = Vec_IntAlloc( 0 );
-    Vec_IntFill( p->vObj2Var, p->nObjs, 0 );
-    // start the AIG manager and map primary inputs
-    p->pFrm         = Aig_ManStart( p->nObjs );
-    Saig_ManForEachLo( pAig, pObj, i )
-        Saig_BmcObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrm) ); 
-    // create SAT solver
-    p->nSatVars     = 1;
-    p->pSat         = sat_solver_new();
-    sat_solver_setnvars( p->pSat, 2000 );
-    Lit = toLit( p->nSatVars );
-    sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
-    Saig_BmcSetSatNum( p, Aig_ManConst1(p->pFrm), p->nSatVars++ );
-    // other data structures
-    p->vTargets     = Vec_PtrAlloc( 1000 );
-    p->vVisited     = Vec_IntAlloc( 1000 );
-    p->iOutputFail  = -1;
-    p->iFrameFail   = -1;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Delete manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_BmcManStop( Saig_Bmc_t * p )
-{
-    Aig_ManStop( p->pFrm  );
-    Vec_VecFree( (Vec_Vec_t *)p->vAig2Frm );
-    Vec_IntFree( p->vObj2Var );
-    sat_solver_delete( p->pSat );
-    Vec_PtrFree( p->vTargets );
-    Vec_IntFree( p->vVisited );
-    ABC_FREE( p );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Explores the possibility of constructing the output.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-/*
-Aig_Obj_t * Saig_BmcIntervalExplore_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )
-{
-    Aig_Obj_t * pRes, * p0, * p1, * pConst1 = Aig_ManConst1(p->pAig);
-    pRes = Saig_BmcObjFrame( p, pObj, i );
-    if ( pRes != NULL )
-        return pRes;
-    if ( Saig_ObjIsPi( p->pAig, pObj ) )
-        pRes = AIG_VISITED;
-    else if ( Saig_ObjIsLo( p->pAig, pObj ) )
-        pRes = Saig_BmcIntervalExplore_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 );
-    else if ( Aig_ObjIsCo( pObj ) )
-    {
-        pRes = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i );
-        if ( pRes != AIG_VISITED )
-            pRes = Saig_BmcObjChild0( p, pObj, i );
-    }
-    else 
-    {
-        p0 = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin0(pObj), i );
-        if ( p0 != AIG_VISITED )
-            p0 = Saig_BmcObjChild0( p, pObj, i );
-        p1 = Saig_BmcIntervalExplore_rec( p, Aig_ObjFanin1(pObj), i );
-        if ( p1 != AIG_VISITED )
-            p1 = Saig_BmcObjChild1( p, pObj, i );
-
-        if ( p0 == Aig_Not(p1) )
-            pRes = Aig_ManConst0(p->pFrm);
-        else if ( Aig_Regular(p0) == pConst1 )
-            pRes = (p0 == pConst1) ? p1 : Aig_ManConst0(p->pFrm);
-        else if ( Aig_Regular(p1) == pConst1 )
-            pRes = (p1 == pConst1) ? p0 : Aig_ManConst0(p->pFrm);
-        else 
-            pRes = AIG_VISITED;
-
-        if ( pRes != AIG_VISITED && !Aig_ObjIsConst1(Aig_Regular(pRes)) )
-            pRes = AIG_VISITED;
-    }
-    Saig_BmcObjSetFrame( p, pObj, i, pRes );
-    return pRes;
-}
-*/
-
-/**Function*************************************************************
-
-  Synopsis    [Performs the actual construction of the output.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i, Vec_Int_t * vVisited )
-{
-    Aig_Obj_t * pRes;
-    pRes = Saig_BmcObjFrame( p, pObj, i );
-    if ( pRes != NULL )
-        return pRes;
-    if ( Saig_ObjIsPi( p->pAig, pObj ) )
-        pRes = Aig_ObjCreateCi(p->pFrm);
-    else if ( Saig_ObjIsLo( p->pAig, pObj ) )
-        pRes = Saig_BmcIntervalConstruct_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1, vVisited );
-    else if ( Aig_ObjIsCo( pObj ) )
-    {
-        Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i, vVisited );
-        pRes = Saig_BmcObjChild0( p, pObj, i );
-    }
-    else 
-    {
-        Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i, vVisited );
-        if ( Saig_BmcObjChild0(p, pObj, i) == Aig_ManConst0(p->pFrm) )
-            pRes = Aig_ManConst0(p->pFrm);
-        else
-        {
-            Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i, vVisited );
-            pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) );
-        }
-    }
-    assert( pRes != NULL );
-    Saig_BmcObjSetFrame( p, pObj, i, pRes );
-    Vec_IntPush( vVisited, Aig_ObjId(pObj) );
-    Vec_IntPush( vVisited, i );
-    return pRes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Adds new AIG nodes to the frames.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_BmcInterval( Saig_Bmc_t * p )
-{
-    Aig_Obj_t * pTarget;
-    int i, iObj, iFrame;
-    int nNodes = Aig_ManObjNum( p->pFrm );
-    Vec_PtrClear( p->vTargets );
-    p->iFramePrev = p->iFrameLast;
-    for ( ; p->iFrameLast < p->nFramesMax; p->iFrameLast++, p->iOutputLast = 0 )
-    { 
-        if ( p->iOutputLast == 0 )
-        {
-            Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFrameLast, Aig_ManConst1(p->pFrm) );
-        }
-        for ( ; p->iOutputLast < Saig_ManPoNum(p->pAig); p->iOutputLast++ )
-        {
-            if ( Aig_ManObjNum(p->pFrm) >= nNodes + p->nNodesMax )
-                return;
-//            Saig_BmcIntervalExplore_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast );
-            Vec_IntClear( p->vVisited );
-            pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManCo(p->pAig, p->iOutputLast), p->iFrameLast, p->vVisited );
-            Vec_PtrPush( p->vTargets, pTarget );
-            Aig_ObjCreateCo( p->pFrm, pTarget );
-            Aig_ManCleanup( p->pFrm ); // it is not efficient to cleanup the whole manager!!!
-            // check if the node is gone
-            Vec_IntForEachEntryDouble( p->vVisited, iObj, iFrame, i )
-                Saig_BmcObjFrame( p, Aig_ManObj(p->pAig, iObj), iFrame );
-            // it is not efficient to remove nodes, which may be used later!!!
-        }
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs the actual construction of the output.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Obj_t * Saig_BmcIntervalToAig_rec( Saig_Bmc_t * p, Aig_Man_t * pNew, Aig_Obj_t * pObj )
-{
-    if ( pObj->pData )
-        return (Aig_Obj_t *)pObj->pData;
-    Vec_IntPush( p->vVisited, Aig_ObjId(pObj) );
-    if ( Saig_BmcSatNum(p, pObj) || Aig_ObjIsCi(pObj) )
-    {
-        p->nStitchVars += !Aig_ObjIsCi(pObj);
-        return (Aig_Obj_t *)(pObj->pData = Aig_ObjCreateCi(pNew));
-    }
-    Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin0(pObj) );
-    Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin1(pObj) );
-    assert( pObj->pData == NULL );
-    return (Aig_Obj_t *)(pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) ));
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates AIG of the newly added nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_BmcIntervalToAig( Saig_Bmc_t * p )
-{
-    Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pObjNew;
-    int i;
-    Aig_ManForEachObj( p->pFrm, pObj, i )
-        assert( pObj->pData == NULL );
-
-    pNew = Aig_ManStart( p->nNodesMax );
-    Aig_ManConst1(p->pFrm)->pData = Aig_ManConst1(pNew);
-    Vec_IntClear( p->vVisited );
-    Vec_IntPush( p->vVisited, Aig_ObjId(Aig_ManConst1(p->pFrm)) );
-    Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
-    {
-//        assert( !Aig_ObjIsConst1(Aig_Regular(pObj)) );
-        pObjNew = Saig_BmcIntervalToAig_rec( p, pNew, Aig_Regular(pObj) );
-        assert( !Aig_IsComplement(pObjNew) );
-        Aig_ObjCreateCo( pNew, pObjNew );
-    } 
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives CNF for the newly added nodes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_BmcLoadCnf( Saig_Bmc_t * p, Cnf_Dat_t * pCnf )
-{
-    Aig_Obj_t * pObj, * pObjNew;
-    int i, Lits[2], VarNumOld, VarNumNew;
-    Aig_ManForEachObjVec( p->vVisited, p->pFrm, pObj, i )
-    {
-        // get the new variable of this node
-        pObjNew     = (Aig_Obj_t *)pObj->pData;
-        pObj->pData = NULL;
-        VarNumNew   = pCnf->pVarNums[ pObjNew->Id ];
-        if ( VarNumNew == -1 )
-            continue;
-        // get the old variable of this node
-        VarNumOld   = Saig_BmcSatNum( p, pObj );
-        if ( VarNumOld == 0 )
-        {
-            Saig_BmcSetSatNum( p, pObj, VarNumNew );
-            continue;
-        }
-        // add clauses connecting existing variables
-        Lits[0] = toLitCond( VarNumOld, 0 );
-        Lits[1] = toLitCond( VarNumNew, 1 );
-        if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
-            assert( 0 );
-        Lits[0] = toLitCond( VarNumOld, 1 );
-        Lits[1] = toLitCond( VarNumNew, 0 );
-        if ( !sat_solver_addclause( p->pSat, Lits, Lits+2 ) )
-            assert( 0 );
-    }
-    // add CNF to the SAT solver
-    for ( i = 0; i < pCnf->nClauses; i++ )
-        if ( !sat_solver_addclause( p->pSat, pCnf->pClauses[i], pCnf->pClauses[i+1] ) )
-            break;
-    if ( i < pCnf->nClauses )
-        printf( "SAT solver became UNSAT after adding clauses.\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Solves targets with the given resource limit.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_BmcDeriveFailed( Saig_Bmc_t * p, int iTargetFail )
-{
-    int k;
-    p->iOutputFail = p->iOutputLast;
-    p->iFrameFail  = p->iFrameLast;
-    for ( k = Vec_PtrSize(p->vTargets); k > iTargetFail; k-- )
-    {
-        if ( p->iOutputFail == 0 )
-        {
-            p->iOutputFail = Saig_ManPoNum(p->pAig);
-            p->iFrameFail--;
-        }
-        p->iOutputFail--;
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Solves targets with the given resource limit.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Saig_BmcGenerateCounterExample( Saig_Bmc_t * p )
-{
-    Abc_Cex_t * pCex;
-    Aig_Obj_t * pObj, * pObjFrm;
-    int i, f, iVarNum;
-    // start the counter-example
-    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), p->iFrameFail+1 );
-    pCex->iFrame = p->iFrameFail;
-    pCex->iPo    = p->iOutputFail;
-    // copy the bit data
-    for ( f = 0; f <= p->iFrameFail; f++ )
-    {
-        Saig_ManForEachPi( p->pAig, pObj, i )
-        {
-            pObjFrm = Saig_BmcObjFrame( p, pObj, f );
-            if ( pObjFrm == NULL )
-                continue;
-            iVarNum = Saig_BmcSatNum( p, pObjFrm );
-            if ( iVarNum == 0 )
-                continue;
-            if ( sat_solver_var_value( p->pSat, iVarNum ) )
-                Abc_InfoSetBit( pCex->pData, pCex->nRegs + Saig_ManPiNum(p->pAig) * f + i );
-        }
-    }
-    // verify the counter example
-    if ( !Saig_ManVerifyCex( p->pAig, pCex ) )
-    {
-        printf( "Saig_BmcGenerateCounterExample(): Counter-example is invalid.\n" );
-        Abc_CexFree( pCex );
-        pCex = NULL;
-    }
-    return pCex;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Solves targets with the given resource limit.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_BmcSolveTargets( Saig_Bmc_t * p, int nStart, int * pnOutsSolved )
-{
-    Aig_Obj_t * pObj;
-    int i, k, VarNum, Lit, status, RetValue;
-    assert( Vec_PtrSize(p->vTargets) > 0 );
-    if ( p->pSat->qtail != p->pSat->qhead )
-    {
-        RetValue = sat_solver_simplify(p->pSat);
-        assert( RetValue != 0 );
-    }
-    Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
-    {
-        if ( ((*pnOutsSolved)++ / Saig_ManPoNum(p->pAig)) < nStart )
-            continue;
-        if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
-            return l_Undef;
-        VarNum = Saig_BmcSatNum( p, Aig_Regular(pObj) );
-        Lit = toLitCond( VarNum, Aig_IsComplement(pObj) );
-        RetValue = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)p->nConfMaxOne, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-        if ( RetValue == l_False ) // unsat
-        {
-            // add final unit clause
-            Lit = lit_neg( Lit );
-            status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
-            assert( status );
-            // add learned units
-            for ( k = 0; k < veci_size(&p->pSat->unit_lits); k++ )
-            {
-                Lit = veci_begin(&p->pSat->unit_lits)[k];
-                status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
-                assert( status );
-            }
-            veci_resize(&p->pSat->unit_lits, 0);
-            // propagate units
-            sat_solver_compress( p->pSat );
-            continue;
-        }
-        if ( RetValue == l_Undef ) // undecided
-            return l_Undef;
-        // generate counter-example
-        Saig_BmcDeriveFailed( p, i );
-        p->pAig->pSeqModel = Saig_BmcGenerateCounterExample( p );
-
-        {
-//            extern Vec_Int_t * Saig_ManExtendCounterExampleTest( Aig_Man_t * p, int iFirstPi, void * pCex );
-//            Saig_ManExtendCounterExampleTest( p->pAig, 0, p->pAig->pSeqModel );
-        }
-        return l_True;
-    }
-    return l_False;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_BmcAddTargetsAsPos( Saig_Bmc_t * p )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    Vec_PtrForEachEntry( Aig_Obj_t *, p->vTargets, pObj, i )
-        Aig_ObjCreateCo( p->pFrm, pObj );
-    Aig_ManPrintStats( p->pFrm );
-    Aig_ManCleanup( p->pFrm );
-    Aig_ManPrintStats( p->pFrm );
-} 
-
-/**Function*************************************************************
-
-  Synopsis    [Performs BMC with the given parameters.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_BmcPerform( Aig_Man_t * pAig, int nStart, int nFramesMax, int nNodesMax, int nTimeOut, int nConfMaxOne, int nConfMaxAll, int fVerbose, int fVerbOverwrite, int * piFrames, int fSilent )
-{
-    Saig_Bmc_t * p;
-    Aig_Man_t * pNew;
-    Cnf_Dat_t * pCnf;
-    int nOutsSolved = 0;
-    int Iter, RetValue = -1;
-    clock_t nTimeToStop = nTimeOut ? nTimeOut * CLOCKS_PER_SEC + clock(): 0;
-    clock_t clk = clock(), clk2, clkTotal = clock();
-    int Status = -1;
-/*
-    Vec_Ptr_t * vSimInfo;
-    vSimInfo = Abs_ManTernarySimulate( pAig, nFramesMax, fVerbose );
-    Abs_ManFreeAray( vSimInfo );
-*/
-    if ( fVerbose )
-    {
-        printf( "Running \"bmc2\". AIG:  PI/PO/Reg = %d/%d/%d.  Node = %6d. Lev = %5d.\n", 
-            Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
-            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
-        printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n", 
-            nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll );
-    } 
-    nFramesMax = nFramesMax ? nFramesMax : ABC_INFINITY;
-    p = Saig_BmcManStart( pAig, nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll, fVerbose );
-    // set runtime limit
-    if ( nTimeOut )
-        sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
-    for ( Iter = 0; ; Iter++ )
-    {
-        clk2 = clock();
-        // add new logic interval to frames
-        Saig_BmcInterval( p );
-//        Saig_BmcAddTargetsAsPos( p );
-        if ( Vec_PtrSize(p->vTargets) == 0 )
-            break;
-        // convert logic slice into new AIG
-        pNew = Saig_BmcIntervalToAig( p );
-//printf( "StitchVars = %d.\n", p->nStitchVars );
-        // derive CNF for the new AIG
-        pCnf = Cnf_Derive( pNew, Aig_ManCoNum(pNew) );
-        Cnf_DataLift( pCnf, p->nSatVars );
-        p->nSatVars += pCnf->nVars;
-        // add this CNF to the solver
-        Saig_BmcLoadCnf( p, pCnf );
-        Cnf_DataFree( pCnf );
-        Aig_ManStop( pNew );
-        // solve the targets
-        RetValue = Saig_BmcSolveTargets( p, nStart, &nOutsSolved );
-        if ( fVerbose )
-        {
-            printf( "%4d : F =%5d. O =%4d.  And =%8d. Var =%8d. Conf =%7d. ", 
-                Iter, p->iFrameLast, p->iOutputLast, Aig_ManNodeNum(p->pFrm), p->nSatVars, (int)p->pSat->stats.conflicts );   
-            printf( "%4.0f MB",     4.0*(p->iFrameLast+1)*p->nObjs/(1<<20) );
-            printf( "%9.2f sec", (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
-            printf( "\n" );
-            fflush( stdout );
-        }
-        if ( RetValue != l_False )
-            break;
-        // check the timeout
-        if ( nTimeOut && clock() > nTimeToStop )
-        {
-            if ( !fSilent )
-                printf( "Reached timeout (%d seconds).\n",  nTimeOut );
-            if ( piFrames )
-                *piFrames = p->iFrameLast-1;
-            Saig_BmcManStop( p );
-            return Status;
-        }
-    }
-    if ( RetValue == l_True )
-    {
-        assert( p->iFrameFail * Saig_ManPoNum(p->pAig) + p->iOutputFail + 1 == nOutsSolved );
-        if ( !fSilent )
-            Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d. ", 
-                p->iOutputFail, p->pAig->pName, p->iFrameFail );
-        Status = 0;
-        if ( piFrames )
-            *piFrames = p->iFrameFail - 1;
-    }
-    else // if ( RetValue == l_False || RetValue == l_Undef )
-    {
-        if ( !fSilent )
-            Abc_Print( 1, "No output failed in %d frames.  ", Abc_MaxInt(p->iFramePrev-1, 0) );
-        if ( piFrames )
-        {
-            if ( p->iOutputLast > 0 )
-                *piFrames = p->iFramePrev - 2;
-            else
-                *piFrames = p->iFramePrev - 1;
-        }
-    }
-    if ( !fSilent )
-    {
-        if ( fVerbOverwrite )
-        {
-            ABC_PRTr( "Time", clock() - clk );
-        }
-        else
-        {
-            ABC_PRT( "Time", clock() - clk );
-        }
-        if ( RetValue != l_True )
-        {
-            if ( p->iFrameLast >= p->nFramesMax )
-                printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
-            else if ( p->nConfMaxAll && p->pSat->stats.conflicts > p->nConfMaxAll )
-                printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
-            else if ( nTimeOut && clock() > nTimeToStop )
-                printf( "Reached timeout (%d seconds).\n", nTimeOut );
-            else
-                printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
-        }
-    }
-    Saig_BmcManStop( p );
-    fflush( stdout );
-    return Status;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c
deleted file mode 100644
index c8ed7e5a..00000000
--- a/src/aig/saig/saigBmc3.c
+++ /dev/null
@@ -1,1575 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [saigBmc3.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Sequential AIG package.]
-
-  Synopsis    [Simple BMC package.]
-
-  Author      [Alan Mishchenko in collaboration with Niklas Een.]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: saigBmc3.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "saig.h"
-#include "proof/fra/fra.h"
-#include "sat/cnf/cnf.h"
-#include "sat/bsat/satStore.h"
-
-ABC_NAMESPACE_IMPL_START
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct Gia_ManBmc_t_ Gia_ManBmc_t;
-struct Gia_ManBmc_t_
-{
-    // input/output data
-    Saig_ParBmc_t *   pPars;       // parameters
-    Aig_Man_t *       pAig;        // user AIG
-    Vec_Ptr_t *       vCexes;      // counter-examples
-    // intermediate data
-    Vec_Int_t *       vMapping;    // mapping
-    Vec_Int_t *       vMapRefs;    // mapping references
-    Vec_Vec_t *       vSects;      // sections
-    Vec_Int_t *       vId2Num;     // number of each node 
-    Vec_Ptr_t *       vTerInfo;    // ternary information
-    Vec_Ptr_t *       vId2Var;     // SAT vars for each object
-    // hash table
-    int *             pTable;
-    int               nTable;
-    int               nHashHit;
-    int               nHashMiss;
-    int               nHashOver;
-    int               nBufNum;     // the number of simple nodes
-    int               nDupNum;     // the number of simple nodes
-    int               nUniProps;   // propagating learned clause values
-    int               nLitUsed;    // used literals
-    int               nLitUseless; // useless literals
-    // SAT solver
-    sat_solver *      pSat;        // SAT solver
-    int               nSatVars;    // SAT variables
-    int               nObjNums;    // SAT objects
-    int               nWordNum;    // unsigned words for ternary simulation
-    char * pSopSizes, ** pSops;    // CNF representation
-};
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-#define SAIG_TER_NON 0
-#define SAIG_TER_ZER 1
-#define SAIG_TER_ONE 2
-#define SAIG_TER_UND 3
-
-static inline int Saig_ManBmcSimInfoNot( int Value )
-{
-    if ( Value == SAIG_TER_ZER )
-        return SAIG_TER_ONE;
-    if ( Value == SAIG_TER_ONE )
-        return SAIG_TER_ZER;
-    return SAIG_TER_UND;
-}
-
-static inline int Saig_ManBmcSimInfoAnd( int Value0, int Value1 )
-{
-    if ( Value0 == SAIG_TER_ZER || Value1 == SAIG_TER_ZER )
-        return SAIG_TER_ZER;
-    if ( Value0 == SAIG_TER_ONE && Value1 == SAIG_TER_ONE )
-        return SAIG_TER_ONE;
-    return SAIG_TER_UND;
-}
-
-static inline int Saig_ManBmcSimInfoGet( unsigned * pInfo, Aig_Obj_t * pObj )
-{
-    return 3 & (pInfo[Aig_ObjId(pObj) >> 4] >> ((Aig_ObjId(pObj) & 15) << 1));
-}
-
-static inline void Saig_ManBmcSimInfoSet( unsigned * pInfo, Aig_Obj_t * pObj, int Value )
-{
-    assert( Value >= SAIG_TER_ZER && Value <= SAIG_TER_UND );
-    Value ^= Saig_ManBmcSimInfoGet( pInfo, pObj );
-    pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
-}
-
-static inline int Saig_ManBmcSimInfoClear( unsigned * pInfo, Aig_Obj_t * pObj )
-{
-    int Value = Saig_ManBmcSimInfoGet( pInfo, pObj );
-    pInfo[Aig_ObjId(pObj) >> 4] ^= (Value << ((Aig_ObjId(pObj) & 15) << 1));
-    return Value;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the number of LIs with binary ternary info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_ManBmcTerSimCount01( Aig_Man_t * p, unsigned * pInfo )
-{
-    Aig_Obj_t * pObj;
-    int i, Counter = 0;
-    if ( pInfo == NULL )
-        return Saig_ManRegNum(p);
-    Saig_ManForEachLi( p, pObj, i )
-        if ( !Aig_ObjIsConst1(Aig_ObjFanin0(pObj)) )
-            Counter += (Saig_ManBmcSimInfoGet(pInfo, pObj) != SAIG_TER_UND);
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs ternary simulation of one frame.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-unsigned * Saig_ManBmcTerSimOne( Aig_Man_t * p, unsigned * pPrev )
-{
-    Aig_Obj_t * pObj, * pObjLi;
-    unsigned * pInfo;
-    int i, Val0, Val1;
-    pInfo = ABC_CALLOC( unsigned, Abc_BitWordNum(2 * Aig_ManObjNumMax(p)) );
-    Saig_ManBmcSimInfoSet( pInfo, Aig_ManConst1(p), SAIG_TER_ONE );
-    Saig_ManForEachPi( p, pObj, i )
-        Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_UND );
-    if ( pPrev == NULL )
-    {
-        Saig_ManForEachLo( p, pObj, i )
-            Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_ZER );
-    }
-    else
-    {
-        Saig_ManForEachLiLo( p, pObjLi, pObj, i )
-            Saig_ManBmcSimInfoSet( pInfo, pObj, Saig_ManBmcSimInfoGet(pPrev, pObjLi) );
-    }
-    Aig_ManForEachNode( p, pObj, i )
-    {
-        Val0 = Saig_ManBmcSimInfoGet( pInfo, Aig_ObjFanin0(pObj) );
-        Val1 = Saig_ManBmcSimInfoGet( pInfo, Aig_ObjFanin1(pObj) );
-        if ( Aig_ObjFaninC0(pObj) )
-            Val0 = Saig_ManBmcSimInfoNot( Val0 );
-        if ( Aig_ObjFaninC1(pObj) )
-            Val1 = Saig_ManBmcSimInfoNot( Val1 );
-        Saig_ManBmcSimInfoSet( pInfo, pObj, Saig_ManBmcSimInfoAnd(Val0, Val1) );
-    }
-    Aig_ManForEachCo( p, pObj, i )
-    {
-        Val0 = Saig_ManBmcSimInfoGet( pInfo, Aig_ObjFanin0(pObj) );
-        if ( Aig_ObjFaninC0(pObj) )
-            Val0 = Saig_ManBmcSimInfoNot( Val0 );
-        Saig_ManBmcSimInfoSet( pInfo, pObj, Val0 );
-    }
-    return pInfo;    
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes and PIs in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Saig_ManBmcTerSim( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vInfos;
-    unsigned * pInfo = NULL;
-    int i, TerPrev = ABC_INFINITY, TerCur, CountIncrease = 0;
-    vInfos = Vec_PtrAlloc( 100 );
-    for ( i = 0; i < 1000 && CountIncrease < 5 && TerPrev > 0; i++ )
-    {
-        TerCur = Saig_ManBmcTerSimCount01( p, pInfo );
-        if ( TerCur >= TerPrev )
-            CountIncrease++;
-        TerPrev = TerCur;
-        pInfo = Saig_ManBmcTerSimOne( p, pInfo );
-        Vec_PtrPush( vInfos, pInfo );
-    }
-    return vInfos;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManBmcTerSimTest( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vInfos;
-    unsigned * pInfo;
-    int i;
-    vInfos = Saig_ManBmcTerSim( p );
-    Vec_PtrForEachEntry( unsigned *, vInfos, pInfo, i )
-        printf( "%d=%d ", i, Saig_ManBmcTerSimCount01(p, pInfo) );
-    printf( "\n" );
-    Vec_PtrFreeFree( vInfos );
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Count the number of non-ternary per frame.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_ManBmcCountNonternary_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vInfos, unsigned * pInfo, int f, int * pCounter )
-{ 
-    int Value = Saig_ManBmcSimInfoClear( pInfo, pObj );
-    if ( Value == SAIG_TER_NON )
-        return 0;
-    assert( f >= 0 );
-    pCounter[f] += (Value == SAIG_TER_UND);
-    if ( Saig_ObjIsPi(p, pObj) || (f == 0 && Saig_ObjIsLo(p, pObj)) || Aig_ObjIsConst1(pObj) )
-        return 0;
-    if ( Saig_ObjIsLi(p, pObj) )
-        return Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(pObj), vInfos, pInfo, f, pCounter );
-    if ( Saig_ObjIsLo(p, pObj) )
-        return Saig_ManBmcCountNonternary_rec( p, Saig_ObjLoToLi(p, pObj), vInfos, (unsigned *)Vec_PtrEntry(vInfos, f-1), f-1, pCounter );
-    assert( Aig_ObjIsNode(pObj) );
-    Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(pObj), vInfos, pInfo, f, pCounter );
-    Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin1(pObj), vInfos, pInfo, f, pCounter );
-    return 0;
-}
-void Saig_ManBmcCountNonternary( Aig_Man_t * p, Vec_Ptr_t * vInfos, int iFrame )
-{
-    int i, * pCounters = ABC_CALLOC( int, iFrame + 1 );
-    unsigned * pInfo = (unsigned *)Vec_PtrEntry(vInfos, iFrame);
-    assert( Saig_ManBmcSimInfoGet( pInfo, Aig_ManCo(p, 0) ) == SAIG_TER_UND );
-    Saig_ManBmcCountNonternary_rec( p, Aig_ObjFanin0(Aig_ManCo(p, 0)), vInfos, pInfo, iFrame, pCounters );
-    for ( i = 0; i <= iFrame; i++ )
-        printf( "%d=%d ", i, pCounters[i] );
-    printf( "\n" );
-    ABC_FREE( pCounters );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the number of POs with binary ternary info.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_ManBmcTerSimCount01Po( Aig_Man_t * p, unsigned * pInfo )
-{
-    Aig_Obj_t * pObj;
-    int i, Counter = 0;
-    Saig_ManForEachPo( p, pObj, i )
-        Counter += (Saig_ManBmcSimInfoGet(pInfo, pObj) != SAIG_TER_UND);
-    return Counter;
-}
-Vec_Ptr_t * Saig_ManBmcTerSimPo( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vInfos;
-    unsigned * pInfo = NULL;
-    int i, nPoBin;
-    vInfos = Vec_PtrAlloc( 100 );
-    for ( i = 0; ; i++ )
-    {
-        if ( i % 100 == 0 )
-            printf( "Frame %5d\n", i );
-        pInfo = Saig_ManBmcTerSimOne( p, pInfo );
-        Vec_PtrPush( vInfos, pInfo );
-        nPoBin = Saig_ManBmcTerSimCount01Po( p, pInfo );
-        if ( nPoBin < Saig_ManPoNum(p) )
-            break;
-    }
-    printf( "Detected terminary PO in frame %d.\n", i );
-    Saig_ManBmcCountNonternary( p, vInfos, i );
-    return vInfos;
-}
-void Saig_ManBmcTerSimTestPo( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vInfos;
-    vInfos = Saig_ManBmcTerSimPo( p );
-    Vec_PtrFreeFree( vInfos );
-}
-
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManBmcDfs_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
-{
-    assert( !Aig_IsComplement(pObj) );
-    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-        return;
-    Aig_ObjSetTravIdCurrent(p, pObj);
-    if ( Aig_ObjIsNode(pObj) )
-    {
-        Saig_ManBmcDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
-        Saig_ManBmcDfs_rec( p, Aig_ObjFanin1(pObj), vNodes );
-    }
-    Vec_PtrPush( vNodes, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects internal nodes and PIs in the DFS order.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Saig_ManBmcDfsNodes( Aig_Man_t * p, Vec_Ptr_t * vRoots )
-{
-    Vec_Ptr_t * vNodes;
-    Aig_Obj_t * pObj;
-    int i;
-    vNodes = Vec_PtrAlloc( 100 );
-    Vec_PtrForEachEntry( Aig_Obj_t *, vRoots, pObj, i )
-        Saig_ManBmcDfs_rec( p, Aig_ObjFanin0(pObj), vNodes );
-    return vNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Vec_t * Saig_ManBmcSections( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vSects, * vRoots, * vCone;
-    Aig_Obj_t * pObj, * pObjPo;
-    int i;
-    Aig_ManIncrementTravId( p );
-    Aig_ObjSetTravIdCurrent( p, Aig_ManConst1(p) );
-    // start the roots
-    vRoots = Vec_PtrAlloc( 1000 );
-    Saig_ManForEachPo( p, pObjPo, i )
-    {
-        Aig_ObjSetTravIdCurrent( p, pObjPo );
-        Vec_PtrPush( vRoots, pObjPo );
-    }
-    // compute the cones
-    vSects = Vec_PtrAlloc( 20 );
-    while ( Vec_PtrSize(vRoots) > 0 )
-    {
-        vCone = Saig_ManBmcDfsNodes( p, vRoots );
-        Vec_PtrPush( vSects, vCone );
-        // get the next set of roots
-        Vec_PtrClear( vRoots );
-        Vec_PtrForEachEntry( Aig_Obj_t *, vCone, pObj, i )
-        {
-            if ( !Saig_ObjIsLo(p, pObj) )
-                continue;
-            pObjPo = Saig_ObjLoToLi( p, pObj );
-            if ( Aig_ObjIsTravIdCurrent(p, pObjPo) )
-                continue;
-            Aig_ObjSetTravIdCurrent( p, pObjPo );
-            Vec_PtrPush( vRoots, pObjPo );
-        }
-    }
-    Vec_PtrFree( vRoots );
-    return (Vec_Vec_t *)vSects;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManBmcSectionsTest( Aig_Man_t * p )
-{
-    Vec_Vec_t * vSects;
-    Vec_Ptr_t * vOne;
-    int i;
-    vSects = Saig_ManBmcSections( p );
-    Vec_VecForEachLevel( vSects, vOne, i )
-        printf( "%d=%d ", i, Vec_PtrSize(vOne) );
-    printf( "\n" );
-    Vec_VecFree( vSects );
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManBmcSupergate_rec( Aig_Obj_t * pObj, Vec_Ptr_t * vSuper )
-{
-    // if the new node is complemented or a PI, another gate begins
-    if ( Aig_IsComplement(pObj) || Aig_ObjIsCi(pObj) ) // || (Aig_ObjRefs(pObj) > 1) )
-    {
-        Vec_PtrPushUnique( vSuper, Aig_Regular(pObj) );
-        return;
-    }
-    // go through the branches
-    Saig_ManBmcSupergate_rec( Aig_ObjChild0(pObj), vSuper );
-    Saig_ManBmcSupergate_rec( Aig_ObjChild1(pObj), vSuper );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collect the topmost supergate.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Ptr_t * Saig_ManBmcSupergate( Aig_Man_t * p, int iPo )
-{
-    Vec_Ptr_t * vSuper;
-    Aig_Obj_t * pObj;
-    vSuper = Vec_PtrAlloc( 10 );
-    pObj = Aig_ManCo( p, iPo );
-    pObj = Aig_ObjChild0( pObj );
-    if ( !Aig_IsComplement(pObj) )
-    {
-        Vec_PtrPush( vSuper, pObj );
-        return vSuper;
-    }
-    pObj = Aig_Regular( pObj );
-    if ( !Aig_ObjIsNode(pObj) )
-    {
-        Vec_PtrPush( vSuper, pObj );
-        return vSuper;
-    }
-    Saig_ManBmcSupergate_rec( Aig_ObjChild0(pObj), vSuper );
-    Saig_ManBmcSupergate_rec( Aig_ObjChild1(pObj), vSuper );
-    return vSuper;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the number of nodes with ref counter more than 1.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_ManBmcCountRefed( Aig_Man_t * p, Vec_Ptr_t * vSuper )
-{
-    Aig_Obj_t * pObj;
-    int i, Counter = 0;
-    Vec_PtrForEachEntry( Aig_Obj_t *, vSuper, pObj, i )
-    {
-        assert( !Aig_IsComplement(pObj) );
-        Counter += (Aig_ObjRefs(pObj) > 1);
-    }
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManBmcSupergateTest( Aig_Man_t * p )
-{
-    Vec_Ptr_t * vSuper;
-    Aig_Obj_t * pObj;
-    int i;
-    printf( "Supergates: " );
-    Saig_ManForEachPo( p, pObj, i )
-    {
-        vSuper = Saig_ManBmcSupergate( p, i );
-        printf( "%d=%d(%d) ", i, Vec_PtrSize(vSuper), Saig_ManBmcCountRefed(p, vSuper) );
-        Vec_PtrFree( vSuper );
-    }
-    printf( "\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManBmcWriteBlif( Aig_Man_t * p, Vec_Int_t * vMapping, char * pFileName )
-{
-    FILE * pFile;
-    char * pSopSizes, ** pSops;
-    Aig_Obj_t * pObj;
-    char Vals[4];
-    int i, k, b, iFan, iTruth, * pData;
-    pFile = fopen( pFileName, "w" );
-    if ( pFile == NULL )
-    {
-        printf( "Cannot open file %s\n", pFileName );
-        return;
-    }
-    fprintf( pFile, ".model test\n" );
-    fprintf( pFile, ".inputs" );
-    Aig_ManForEachCi( p, pObj, i )
-        fprintf( pFile, " n%d", Aig_ObjId(pObj) );
-    fprintf( pFile, "\n" );
-    fprintf( pFile, ".outputs" );
-    Aig_ManForEachCo( p, pObj, i )
-        fprintf( pFile, " n%d", Aig_ObjId(pObj) );
-    fprintf( pFile, "\n" );
-    fprintf( pFile, ".names" );
-    fprintf( pFile, " n%d\n", Aig_ObjId(Aig_ManConst1(p)) );
-    fprintf( pFile, " 1\n" );
-
-    Cnf_ReadMsops( &pSopSizes, &pSops );
-    Aig_ManForEachNode( p, pObj, i )
-    {
-        if ( Vec_IntEntry(vMapping, i) == 0 )
-            continue;
-        pData = Vec_IntEntryP( vMapping, Vec_IntEntry(vMapping, i) );
-        fprintf( pFile, ".names" );
-        for ( iFan = 0; iFan < 4; iFan++ )
-            if ( pData[iFan+1] >= 0 )
-                fprintf( pFile, " n%d", pData[iFan+1] );
-            else
-                break;
-        fprintf( pFile, " n%d\n", i );
-        // write SOP
-        iTruth = pData[0] & 0xffff;
-        for ( k = 0; k < pSopSizes[iTruth]; k++ )
-        {
-            int Lit = pSops[iTruth][k];
-            for ( b = 3; b >= 0; b-- )
-            {
-                if ( Lit % 3 == 0 )
-                    Vals[b] = '0';
-                else if ( Lit % 3 == 1 )
-                    Vals[b] = '1';
-                else
-                    Vals[b] = '-';
-                Lit = Lit / 3;
-            }
-            for ( b = 0; b < iFan; b++ )
-                fprintf( pFile, "%c", Vals[b] );
-            fprintf( pFile, " 1\n" );
-        }
-    }
-    free( pSopSizes );
-    free( pSops[1] );
-    free( pSops );
-
-    Aig_ManForEachCo( p, pObj, i )
-    {
-        fprintf( pFile, ".names" );
-        fprintf( pFile, " n%d", Aig_ObjId(Aig_ObjFanin0(pObj)) );
-        fprintf( pFile, " n%d\n", Aig_ObjId(pObj) );
-        fprintf( pFile, "%d 1\n", !Aig_ObjFaninC0(pObj) );
-    }
-    fprintf( pFile, ".end\n" );
-    fclose( pFile );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManBmcMappingTest( Aig_Man_t * p )
-{
-    Vec_Int_t * vMapping;
-    vMapping = Cnf_DeriveMappingArray( p );
-    Saig_ManBmcWriteBlif( p, vMapping, "test.blif" );
-    Vec_IntFree( vMapping );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Int_t * Saig_ManBmcComputeMappingRefs( Aig_Man_t * p, Vec_Int_t * vMap )
-{
-    Vec_Int_t * vRefs;
-    Aig_Obj_t * pObj;
-    int i, iFan, * pData;
-    vRefs = Vec_IntStart( Aig_ManObjNumMax(p) );
-    Aig_ManForEachCo( p, pObj, i )
-        Vec_IntAddToEntry( vRefs, Aig_ObjFaninId0(pObj), 1 );
-    Aig_ManForEachNode( p, pObj, i )
-    {
-        if ( Vec_IntEntry(vMap, i) == 0 )
-            continue;
-        pData = Vec_IntEntryP( vMap, Vec_IntEntry(vMap, i) );
-        for ( iFan = 0; iFan < 4; iFan++ )
-            if ( pData[iFan+1] >= 0 )
-                Vec_IntAddToEntry( vRefs, pData[iFan+1], 1 );
-    }
-    return vRefs;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Create manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Gia_ManBmc_t * Saig_Bmc3ManStart( Aig_Man_t * pAig )
-{
-    Gia_ManBmc_t * p;
-    Aig_Obj_t * pObj;
-    int i;
-//    assert( Aig_ManRegNum(pAig) > 0 );
-    p = ABC_CALLOC( Gia_ManBmc_t, 1 );
-    p->pAig = pAig;
-    // create mapping
-    p->vMapping = Cnf_DeriveMappingArray( pAig );
-    p->vMapRefs = Saig_ManBmcComputeMappingRefs( pAig, p->vMapping );
-    // create sections
-    p->vSects = Saig_ManBmcSections( pAig );
-    // map object IDs into their numbers and section numbers
-    p->nObjNums = 0;
-    p->vId2Num  = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
-    Vec_IntWriteEntry( p->vId2Num,  Aig_ObjId(Aig_ManConst1(pAig)), p->nObjNums++ );
-    Aig_ManForEachCi( pAig, pObj, i )
-        Vec_IntWriteEntry( p->vId2Num,  Aig_ObjId(pObj), p->nObjNums++ );
-    Aig_ManForEachNode( pAig, pObj, i )
-        if ( Vec_IntEntry(p->vMapping, Aig_ObjId(pObj)) > 0 )
-            Vec_IntWriteEntry( p->vId2Num,  Aig_ObjId(pObj), p->nObjNums++ );
-    Aig_ManForEachCo( pAig, pObj, i )
-        Vec_IntWriteEntry( p->vId2Num,  Aig_ObjId(pObj), p->nObjNums++ );
-    p->vId2Var  = Vec_PtrAlloc( 100 );
-    p->vTerInfo = Vec_PtrAlloc( 100 );
-    // create solver
-    p->nSatVars = 1;
-    p->pSat     = sat_solver_new();
-    sat_solver_setnvars( p->pSat, 1000 );
-    Cnf_ReadMsops( &p->pSopSizes, &p->pSops );
-    // terminary simulation 
-    p->nWordNum = Abc_BitWordNum( 2 * Aig_ManObjNumMax(pAig) );
-    // hash table
-    p->nTable = 1000003;
-    p->pTable = ABC_CALLOC( int, 6 * p->nTable ); // 2.4 MB
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Delete manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_Bmc3ManStop( Gia_ManBmc_t * p )
-{
-    if ( p->pPars->fVerbose )
-    printf( "Buffs = %d. Dups = %d.   Hash hits = %d.  Hash misses = %d.  Hash overs = %d.  UniProps = %d.\n", 
-        p->nBufNum, p->nDupNum, p->nHashHit, p->nHashMiss, p->nHashOver, p->nUniProps );
-//    Aig_ManCleanMarkA( p->pAig );
-    if ( p->vCexes )
-    {
-        assert( p->pAig->vSeqModelVec == NULL );
-        p->pAig->vSeqModelVec = p->vCexes;
-        p->vCexes = NULL;
-    }
-//    Vec_PtrFreeFree( p->vCexes );
-    Vec_IntFree( p->vMapping );
-    Vec_IntFree( p->vMapRefs );
-    Vec_VecFree( p->vSects );
-    Vec_IntFree( p->vId2Num );
-    Vec_VecFree( (Vec_Vec_t *)p->vId2Var );
-    Vec_PtrFreeFree( p->vTerInfo );
-    sat_solver_delete( p->pSat );
-    ABC_FREE( p->pTable );
-    ABC_FREE( p->pSopSizes );
-    ABC_FREE( p->pSops[1] );
-    ABC_FREE( p->pSops );
-    ABC_FREE( p );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int * Saig_ManBmcMapping( Gia_ManBmc_t * p, Aig_Obj_t * pObj )
-{
-    if ( Vec_IntEntry(p->vMapping, Aig_ObjId(pObj)) == 0 )
-        return NULL;
-    return Vec_IntEntryP( p->vMapping, Vec_IntEntry(p->vMapping, Aig_ObjId(pObj)) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Saig_ManBmcLiteral( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
-{
-    Vec_Int_t * vFrame;
-    int ObjNum;
-    assert( !Aig_ObjIsNode(pObj) || Saig_ManBmcMapping(p, pObj) );
-    ObjNum  = Vec_IntEntry( p->vId2Num, Aig_ObjId(pObj) );
-    assert( ObjNum >= 0 );
-    vFrame  = (Vec_Int_t *)Vec_PtrEntry( p->vId2Var, iFrame );
-    assert( vFrame != NULL );
-    return Vec_IntEntry( vFrame, ObjNum );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Saig_ManBmcSetLiteral( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, int iLit )
-{
-    Vec_Int_t * vFrame;
-    int ObjNum;
-    assert( !Aig_ObjIsNode(pObj) || Saig_ManBmcMapping(p, pObj) );
-    ObjNum  = Vec_IntEntry( p->vId2Num, Aig_ObjId(pObj) );
-    vFrame  = (Vec_Int_t *)Vec_PtrEntry( p->vId2Var, iFrame );
-    Vec_IntWriteEntry( vFrame, ObjNum, iLit );
-/*
-    if ( Vec_IntEntry( p->vMapRefs, Aig_ObjId(pObj) ) > 1 )
-        p->nLitUsed++;
-    else
-        p->nLitUseless++;
-*/
-    return iLit;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Saig_ManBmcCof0( int t, int v )
-{
-    static int s_Truth[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
-    return 0xffff & ((t & ~s_Truth[v]) | ((t & ~s_Truth[v]) << (1<<v)));
-}
-static inline int Saig_ManBmcCof1( int t, int v )
-{
-    static int s_Truth[4] = { 0xAAAA, 0xCCCC, 0xF0F0, 0xFF00 };
-    return 0xffff & ((t & s_Truth[v]) | ((t & s_Truth[v]) >> (1<<v)));
-}
-static inline int Saig_ManBmcCofEqual( int t, int v )
-{
-    assert( v >= 0 && v <= 3 );
-    if ( v == 0 )
-        return ((t & 0xAAAA) >> 1) == (t & 0x5555);
-    if ( v == 1 )
-        return ((t & 0xCCCC) >> 2) == (t & 0x3333);
-    if ( v == 2 )
-        return ((t & 0xF0F0) >> 4) == (t & 0x0F0F);
-    if ( v == 3 )
-        return ((t & 0xFF00) >> 8) == (t & 0x00FF);
-    return -1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives CNF for one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Saig_ManBmcReduceTruth( int uTruth, int Lits[] )
-{
-    int v;
-    for ( v = 0; v < 4; v++ )
-        if ( Lits[v] == 0 )
-        {
-            uTruth = Saig_ManBmcCof0(uTruth, v);
-            Lits[v] = -1;
-        }
-        else if ( Lits[v] == 1 )
-        {
-            uTruth = Saig_ManBmcCof1(uTruth, v);
-            Lits[v] = -1;
-        }
-    for ( v = 0; v < 4; v++ )
-        if ( Lits[v] == -1 )
-            assert( Saig_ManBmcCofEqual(uTruth, v) );
-        else if ( Saig_ManBmcCofEqual(uTruth, v) )
-            Lits[v] = -1;
-    return uTruth;
-}
-
-/*
-void Cnf_SopConvertToVector( char * pSop, int nCubes, Vec_Int_t * vCover )
-{
-    int Lits[4], Cube, iCube, i, b;
-    Vec_IntClear( vCover );
-    for ( i = 0; i < nCubes; i++ )
-    {
-        Cube = pSop[i];
-        for ( b = 0; b < 4; b++ )
-        {
-            if ( Cube % 3 == 0 )
-                Lits[b] = 1;
-            else if ( Cube % 3 == 1 )
-                Lits[b] = 2;
-            else
-                Lits[b] = 0;
-            Cube = Cube / 3;
-        }
-        iCube = 0;
-        for ( b = 0; b < 4; b++ )
-            iCube = (iCube << 2) | Lits[b];
-        Vec_IntPush( vCover, iCube );
-    }
-}
-
-        Vec_IntForEachEntry( vCover, Cube, k )
-        {
-            *pClas++ = pLits;
-            *pLits++ = 2 * OutVar; 
-            pLits += Cnf_IsopWriteCube( Cube, pCut->nFanins, pVars, pLits );
-        }
-
-
-int Cnf_IsopWriteCube( int Cube, int nVars, int * pVars, int * pLiterals )
-{
-    int nLits = nVars, b;
-    for ( b = 0; b < nVars; b++ )
-    {
-        if ( (Cube & 3) == 1 ) // value 0 --> write positive literal
-            *pLiterals++ = 2 * pVars[b];
-        else if ( (Cube & 3) == 2 ) // value 1 --> write negative literal
-            *pLiterals++ = 2 * pVars[b] + 1;
-        else
-            nLits--;
-        Cube >>= 2;
-    }
-    return nLits;
-}
-
-        iTruth = pData[0] & 0xffff;
-        for ( k = 0; k < pSopSizes[iTruth]; k++ )
-        {
-            int Lit = pSops[iTruth][k];
-            for ( b = 3; b >= 0; b-- )
-            {
-                if ( Lit % 3 == 0 )
-                    Vals[b] = '0';
-                else if ( Lit % 3 == 1 )
-                    Vals[b] = '1';
-                else
-                    Vals[b] = '-';
-                Lit = Lit / 3;
-            }
-            for ( b = 0; b < iFan; b++ )
-                fprintf( pFile, "%c", Vals[b] );
-            fprintf( pFile, " 1\n" );
-        }
-*/
-
-/**Function*************************************************************
-
-  Synopsis    [Derives CNF for one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits[], int iLitOut )
-{
-    int i, k, b, CutLit, nClaLits, ClaLits[5];
-    assert( uTruth > 0 && uTruth < 0xffff );
-    // write positive/negative polarity
-    for ( i = 0; i < 2; i++ )
-    {
-        if ( i )
-            uTruth = 0xffff & ~uTruth;
-//        Extra_PrintBinary( stdout, &uTruth, 16 ); printf( "\n" );
-        for ( k = 0; k < p->pSopSizes[uTruth]; k++ )
-        {
-            nClaLits = 0;
-            ClaLits[nClaLits++] = i ? lit_neg(iLitOut) : iLitOut;
-            CutLit = p->pSops[uTruth][k];
-            for ( b = 3; b >= 0; b-- )
-            {
-                if ( CutLit % 3 == 0 ) // value 0 --> write positive literal
-                {
-                    assert( Lits[b] > 1 );
-                    ClaLits[nClaLits++] = Lits[b];
-                }
-                else if ( CutLit % 3 == 1 ) // value 1 --> write negative literal
-                {
-                    assert( Lits[b] > 1 );
-                    ClaLits[nClaLits++] = lit_neg(Lits[b]);
-                }
-                CutLit = CutLit / 3;
-            }
-            if ( !sat_solver_addclause( p->pSat, ClaLits, ClaLits+nClaLits ) )
-                assert( 0 );
-        }
-    }
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline unsigned Saig_ManBmcHashKey( int * pArray )
-{
-    static int s_Primes[5] = { 12582917, 25165843, 50331653, 100663319, 201326611 };
-    unsigned i, Key = 0;
-    for ( i = 0; i < 5; i++ )
-        Key += pArray[i] * s_Primes[i];
-    return Key;
-}
-static inline int * Saig_ManBmcLookup( Gia_ManBmc_t * p, int * pArray )
-{
-    int * pTable = p->pTable + 6 * (Saig_ManBmcHashKey(pArray) % p->nTable);
-    if ( memcmp( pTable, pArray, 20 ) )
-    {
-        if ( pTable[0] == 0 )
-            p->nHashMiss++;
-        else
-            p->nHashOver++;
-        memcpy( pTable, pArray, 20 );
-        pTable[5] = 0;
-    }
-    else
-        p->nHashHit++;
-    assert( pTable + 5 < pTable + 6 * p->nTable );
-    return pTable + 5;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives CNF for one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
-{
-    extern unsigned Dar_CutSortVars( unsigned uTruth, int * pVars );
-    int * pMapping, * pLookup, i, iLit, Lits[5], uTruth;
-    iLit = Saig_ManBmcLiteral( p, pObj, iFrame );
-    if ( iLit != ~0 )
-        return iLit; 
-    assert( iFrame >= 0 );
-    if ( Aig_ObjIsCi(pObj) )
-    {
-        if ( Saig_ObjIsPi(p->pAig, pObj) )
-            iLit = toLit( p->nSatVars++ );
-        else
-            iLit = Saig_ManBmcCreateCnf_rec( p, Saig_ObjLoToLi(p->pAig, pObj), iFrame-1 );
-        return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
-    }
-    if ( Aig_ObjIsCo(pObj) )
-    {
-        iLit = Saig_ManBmcCreateCnf_rec( p, Aig_ObjFanin0(pObj), iFrame );
-        if ( Aig_ObjFaninC0(pObj) )
-            iLit = lit_neg(iLit);
-        return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
-    }
-    assert( Aig_ObjIsNode(pObj) );
-    pMapping = Saig_ManBmcMapping( p, pObj );
-    for ( i = 0; i < 4; i++ )
-        if ( pMapping[i+1] == -1 )
-            Lits[i] = -1;
-        else
-            Lits[i] = Saig_ManBmcCreateCnf_rec( p, Aig_ManObj(p->pAig, pMapping[i+1]), iFrame );
-    uTruth = 0xffff & (unsigned)pMapping[0];
-    // propagate constants
-    uTruth = Saig_ManBmcReduceTruth( uTruth, Lits );
-    if ( uTruth == 0 || uTruth == 0xffff )
-    {
-        iLit = (uTruth == 0xffff);
-        return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
-    }
-    // canonicize inputs
-    uTruth = Dar_CutSortVars( uTruth, Lits );
-    assert( uTruth != 0 && uTruth != 0xffff );
-    if ( uTruth == 0xAAAA || uTruth == 0x5555 )
-    {
-        iLit = Abc_LitNotCond( Lits[0], uTruth == 0x5555 );
-        p->nBufNum++;
-    }
-    else 
-    {
-        assert( !(uTruth == 0xAAAA || (0xffff & ~uTruth) == 0xAAAA ||
-                  uTruth == 0xCCCC || (0xffff & ~uTruth) == 0xCCCC ||
-                  uTruth == 0xF0F0 || (0xffff & ~uTruth) == 0xF0F0 ||
-                  uTruth == 0xFF00 || (0xffff & ~uTruth) == 0xFF00) );
-
-        Lits[4] = uTruth;
-        pLookup = Saig_ManBmcLookup( p, Lits );
-        if ( *pLookup == 0 )
-        {
-            *pLookup = toLit( p->nSatVars++ );
-            Saig_ManBmcAddClauses( p, uTruth, Lits, *pLookup );
-/*
-            if ( (Lits[0] > 1 && (Lits[0] == Lits[1] || Lits[0] == Lits[2] || Lits[0] == Lits[3]))   ||
-                 (Lits[1] > 1 && (Lits[1] == Lits[2] || Lits[1] == Lits[2]))                         ||
-                 (Lits[2] > 1 && (Lits[2] == Lits[3]))    )
-                       p->nDupNum++;
-*/
-        }
-        iLit = *pLookup;
-    }
-    return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively performs terminary simulation.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_ManBmcRunTerSim_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
-{
-    unsigned * pInfo = (unsigned *)Vec_PtrEntry( p->vTerInfo, iFrame );
-    int Val0, Val1, Value = Saig_ManBmcSimInfoGet( pInfo, pObj );
-    if ( Value != SAIG_TER_NON )
-    {
-/*
-        // check the value of this literal in the SAT solver
-        if ( Value == SAIG_TER_UND && Saig_ManBmcMapping(p, pObj) )
-        {
-            int Lit = Saig_ManBmcLiteral( p, pObj, iFrame );
-            if ( Lit >= 0  )
-            {
-                assert( Lit >= 2 );
-                if ( p->pSat->assigns[Abc_Lit2Var(Lit)] < 2 )
-                {
-                    p->nUniProps++;
-                    if ( Abc_LitIsCompl(Lit) ^ (p->pSat->assigns[Abc_Lit2Var(Lit)] == 0) )
-                        Value = SAIG_TER_ONE;
-                    else
-                        Value = SAIG_TER_ZER;
-
-//                    Value = SAIG_TER_UND;  // disable!
-
-                    // use the new value
-                    Saig_ManBmcSimInfoSet( pInfo, pObj, Value );
-                    // transfer to the unrolling
-                    if ( Value != SAIG_TER_UND )
-                        Saig_ManBmcSetLiteral( p, pObj, iFrame, (int)(Value == SAIG_TER_ONE) );
-                }
-            }
-        }
-*/
-        return Value;
-    }
-    if ( Aig_ObjIsCo(pObj) )
-    {
-        Value = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin0(pObj), iFrame );
-        if ( Aig_ObjFaninC0(pObj) )
-            Value = Saig_ManBmcSimInfoNot( Value );
-    }
-    else if ( Saig_ObjIsLo(p->pAig, pObj) )
-    {
-        assert( iFrame > 0 );
-        Value = Saig_ManBmcRunTerSim_rec( p, Saig_ObjLoToLi(p->pAig, pObj), iFrame - 1 );
-    }
-    else if ( Aig_ObjIsNode(pObj) )
-    {
-        Val0 = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin0(pObj), iFrame  );
-        Val1 = Saig_ManBmcRunTerSim_rec( p, Aig_ObjFanin1(pObj), iFrame  );
-        if ( Aig_ObjFaninC0(pObj) )
-            Val0 = Saig_ManBmcSimInfoNot( Val0 );
-        if ( Aig_ObjFaninC1(pObj) )
-            Val1 = Saig_ManBmcSimInfoNot( Val1 );
-        Value = Saig_ManBmcSimInfoAnd( Val0, Val1 );
-    }
-    else assert( 0 );
-    Saig_ManBmcSimInfoSet( pInfo, pObj, Value );
-    // transfer to the unrolling
-    if ( Saig_ManBmcMapping(p, pObj) && Value != SAIG_TER_UND )
-        Saig_ManBmcSetLiteral( p, pObj, iFrame, (int)(Value == SAIG_TER_ONE) );
-    return Value;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Derives CNF for one node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_ManBmcCreateCnf( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame )
-{
-    int Lit;
-    // perform terminary simulation
-    int Value = Saig_ManBmcRunTerSim_rec( p, pObj, iFrame );
-    if ( Value != SAIG_TER_UND )
-        return (int)(Value == SAIG_TER_ONE);
-    // construct CNF if value is ternary
-    Lit = Saig_ManBmcCreateCnf_rec( p, pObj, iFrame );
-    // extend the SAT solver
-    if ( p->nSatVars > sat_solver_nvars(p->pSat) )
-        sat_solver_setnvars( p->pSat, p->nSatVars );
-    return Lit;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_NodeCompareRefsIncrease( Aig_Obj_t ** pp1, Aig_Obj_t ** pp2 )
-{
-    int Diff = Aig_ObjRefs(*pp1) - Aig_ObjRefs(*pp2);
-    if ( Diff < 0 )
-        return -1;
-    if ( Diff > 0 ) 
-        return 1;
-    Diff = Aig_ObjId(*pp1) - Aig_ObjId(*pp2);
-    if ( Diff < 0 )
-        return -1;
-    if ( Diff > 0 ) 
-        return 1;
-    return 0; 
-}
-
-/**Function*************************************************************
-
-  Synopsis    [This procedure sets default parameters.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ParBmcSetDefaultParams( Saig_ParBmc_t * p )
-{
-    memset( p, 0, sizeof(Saig_ParBmc_t) );
-    p->nStart         =     0;    // maximum number of timeframes 
-    p->nFramesMax     =     0;    // maximum number of timeframes 
-    p->nConfLimit     =     0;    // maximum number of conflicts at a node
-    p->nConfLimitJump =     0;    // maximum number of conflicts after jumping
-    p->nFramesJump    =     0;    // the number of tiemframes to jump
-    p->nTimeOut       =     0;    // approximate timeout in seconds
-    p->nPisAbstract   =     0;    // the number of PIs to abstract
-    p->fSolveAll      =     0;    // stops on the first SAT instance
-    p->fDropSatOuts   =     0;    // replace sat outputs by constant 0
-    p->fVerbose       =     0;    // verbose 
-    p->iFrame         =    -1;    // explored up to this frame
-    p->nFailOuts      =     0;    // the number of failed outputs
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Bounded model checking engine.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
-{
-    Gia_ManBmc_t * p;
-    Aig_Obj_t * pObj;
-    unsigned * pInfo;
-    int RetValue = -1, fFirst = 1, nJumpFrame = 0, fUnfinished = 0;
-    int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
-    int i, f, k, Lit, status;
-    clock_t clk, clk2, clkOther = 0, clkTotal = clock();
-    clock_t nTimeToStop = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
-    p = Saig_Bmc3ManStart( pAig );
-    p->pPars = pPars;
-    if ( pPars->fVerbose )
-    {
-        printf( "Running \"bmc3\". PI/PO/Reg = %d/%d/%d. And =%7d. Lev =%6d. ObjNums =%6d. Sect =%3d.\n", 
-            Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig),
-            Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig), p->nObjNums, Vec_VecSize(p->vSects) );
-        printf( "Params: FramesMax = %d. Start = %d. ConfLimit = %d. TimeOut = %d. SolveAll = %d.\n", 
-            pPars->nFramesMax, pPars->nStart, pPars->nConfLimit, pPars->nTimeOut, pPars->fSolveAll );
-    } 
-    pPars->nFramesMax = pPars->nFramesMax ? pPars->nFramesMax : ABC_INFINITY;
-    // set runtime limit
-    if ( p->pPars->nTimeOut )
-        sat_solver_set_runtime_limit( p->pSat, nTimeToStop );
-    // perform frames
-    Aig_ManRandom( 1 );
-    for ( f = 0; f < pPars->nFramesMax; f++ )
-    {
-        // stop BMC after exploring all reachable states
-        if ( !pPars->nFramesJump && Aig_ManRegNum(pAig) < 30 && f == (1 << Aig_ManRegNum(pAig)) )
-        {
-            Saig_Bmc3ManStop( p );
-            return pPars->nFailOuts ? 0 : 1;
-        }
-        // stop BMC if all targets are solved
-        if ( pPars->fSolveAll && pPars->nFailOuts == Saig_ManPoNum(pAig) )
-        {
-            Saig_Bmc3ManStop( p );
-            return 0;
-        }
-        // consider the next timeframe
-        if ( RetValue == -1 && pPars->nStart == 0 && !nJumpFrame )
-            pPars->iFrame = f-1;
-        // map nodes of this section
-        Vec_PtrPush( p->vId2Var, Vec_IntStartFull(p->nObjNums) );
-        Vec_PtrPush( p->vTerInfo, (pInfo = ABC_CALLOC(unsigned, p->nWordNum)) );
-/*
-        // cannot remove mapping of frame values for any timeframes
-        // because with constant propagation they may be needed arbitrarily far
-        if ( f > 2*Vec_VecSize(p->vSects) )
-        {
-            int iFrameOld = f - 2*Vec_VecSize( p->vSects );
-            void * pMemory = Vec_IntReleaseArray( Vec_PtrEntry(p->vId2Var, iFrameOld) );
-            ABC_FREE( pMemory );
-        } 
-*/
-        // prepare some nodes
-        Saig_ManBmcSetLiteral( p, Aig_ManConst1(pAig), f, 1 );
-        Saig_ManBmcSimInfoSet( pInfo, Aig_ManConst1(pAig), SAIG_TER_ONE );
-        Saig_ManForEachPi( pAig, pObj, i )
-            Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_UND );
-        if ( f == 0 )
-        {
-            Saig_ManForEachLo( p->pAig, pObj, i )
-            {
-                Saig_ManBmcSetLiteral( p, pObj, 0, 0 );
-                Saig_ManBmcSimInfoSet( pInfo, pObj, SAIG_TER_ZER );
-            }
-        }
-        if ( (pPars->nStart && f < pPars->nStart) || (nJumpFrame && f < nJumpFrame) )
-            continue;
-        // solve SAT
-        clk = clock(); 
-        Saig_ManForEachPo( pAig, pObj, i )
-        {
-            if ( i >= Saig_ManPoNum(pAig) )
-                break;
-            // check for timeout
-            if ( pPars->nTimeOut && clock() > nTimeToStop )
-            {
-                printf( "Reached timeout (%d seconds).\n",  pPars->nTimeOut );
-                Saig_Bmc3ManStop( p );
-                return RetValue;
-            }
-            // skip solved outputs
-            if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
-                continue;
-            // add constraints for this output
-clk2 = clock();
-            Lit = Saig_ManBmcCreateCnf( p, pObj, f );
-clkOther += clock() - clk2;
-            if ( Lit == 0 )
-                continue;
-            if ( Lit == 1 )
-            {
-                Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i );
-                if ( !pPars->fSolveAll )
-                {
-                    printf( "Output %d is trivially SAT in frame %d.\n", i, f );
-                    ABC_FREE( pAig->pSeqModel );
-                    pAig->pSeqModel = pCex;
-                    Saig_Bmc3ManStop( p );
-                    return 0;
-                }
-                pPars->nFailOuts++;
-                Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",  
-                    nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
-                if ( p->vCexes == NULL )
-                    p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
-                Vec_PtrWriteEntry( p->vCexes, i, pCex );
-                RetValue = 0;
-                continue;
-            }
-            // solve th is output
-            fUnfinished = 0;
-            sat_solver_compress( p->pSat );
-            status = sat_solver_solve( p->pSat, &Lit, &Lit + 1, (ABC_INT64_T)pPars->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-            if ( status == l_False )
-            {
-                if ( 1 )
-                {
-                    // add final unit clause
-                    Lit = lit_neg( Lit );
-                    status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
-                    assert( status );
-                    // add learned units
-                    for ( k = 0; k < veci_size(&p->pSat->unit_lits); k++ )
-                    {
-                        Lit = veci_begin(&p->pSat->unit_lits)[k];
-                        status = sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
-                        assert( status );
-                    }
-                    veci_resize(&p->pSat->unit_lits, 0);
-                    // propagate units
-                    sat_solver_compress( p->pSat );
-                }
-            }
-            else if ( status == l_True )
-            {
-                Aig_Obj_t * pObjPi;
-                Abc_Cex_t * pCex = Abc_CexMakeTriv( Aig_ManRegNum(pAig), Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), f*Saig_ManPoNum(pAig)+i );
-                int j, iBit = Saig_ManRegNum(pAig);
-                for ( j = 0; j <= f; j++, iBit += Saig_ManPiNum(pAig) )
-                    Saig_ManForEachPi( p->pAig, pObjPi, k )
-                    {
-                        int iLit = Saig_ManBmcLiteral( p, pObjPi, j );
-                        if ( iLit != ~0 && sat_solver_var_value(p->pSat, lit_var(iLit)) )
-                            Abc_InfoSetBit( pCex->pData, iBit + k );
-                    }
-                fFirst = 0;
-                if ( !pPars->fSolveAll )
-                {
-                    if ( pPars->fVerbose )
-                    {
-                        printf( "%4d %s : ", f,  fUnfinished ? "-" : "+" );
-                        printf( "Var =%8.0f. ",  (double)p->nSatVars );
-                        printf( "Cla =%9.0f. ",  (double)p->pSat->stats.clauses );
-                        printf( "Conf =%7.0f. ", (double)p->pSat->stats.conflicts );
-//                        printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
-                        printf( "Units =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
-//                        ABC_PRT( "Time", clock() - clk );
-                        printf( "%4.0f MB",      4.25*(f+1)*p->nObjNums /(1<<20) );
-                        printf( "%4.0f MB",      1.0*sat_solver_memory(p->pSat)/(1<<20) );
-                        printf( "%9.2f sec  ",   (float)(clock() - clkTotal)/(float)(CLOCKS_PER_SEC) );
-//                        printf( "\n" );
-//                        ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
-//                        ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
-//                        printf( "S =%6d. ", p->nBufNum );
-//                        printf( "D =%6d. ", p->nDupNum );
-                        printf( "\n" );
-                        fflush( stdout );
-                    }
-                    ABC_FREE( pAig->pSeqModel );
-                    pAig->pSeqModel = pCex;
-                    Saig_Bmc3ManStop( p );
-                    return 0;
-                }
-                pPars->nFailOuts++;
-                Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",  
-                    nOutDigits, i, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
-                if ( p->vCexes == NULL )
-                    p->vCexes = Vec_PtrStart( Saig_ManPoNum(pAig) );
-                Vec_PtrWriteEntry( p->vCexes, i, pCex );
-                RetValue = 0;
-            }
-            else 
-            {
-                assert( status == l_Undef );
-                if ( pPars->nFramesJump )
-                {
-                    pPars->nConfLimit = pPars->nConfLimitJump;
-                    nJumpFrame = f + pPars->nFramesJump;
-                    fUnfinished = 1;
-                    break;
-                }
-                Saig_Bmc3ManStop( p );
-                return RetValue;
-            }
-        }
-        if ( pPars->fVerbose ) 
-        {
-            if ( fFirst == 1 && f > 0 && p->pSat->stats.conflicts > 1 )
-            {
-                fFirst = 0;
-//                printf( "Outputs of frames up to %d are trivially UNSAT.\n", f );
-            }
-            printf( "%4d %s : ", f, fUnfinished ? "-" : "+" );
-            printf( "Var =%8.0f. ", (double)p->nSatVars );
-            printf( "Cla =%9.0f. ", (double)p->pSat->stats.clauses );
-            printf( "Conf =%7.0f. ",(double)p->pSat->stats.conflicts );
-//            printf( "Imp =%10.0f. ", (double)p->pSat->stats.propagations );
-            printf( "Units =%7.0f. ",(double)sat_solver_count_assigned(p->pSat) );
-//            ABC_PRT( "Time", clock() - clk );
-//            printf( "%4.0f MB",     4.0*Vec_IntSize(p->vVisited) /(1<<20) );
-            printf( "%4.0f MB",     4.0*(f+1)*p->nObjNums /(1<<20) );
-            printf( "%4.0f MB",     1.0*sat_solver_memory(p->pSat)/(1<<20) );
-//            printf( " %6d %6d ",   p->nLitUsed, p->nLitUseless );
-            printf( "%9.2f sec ",  1.0*(clock() - clkTotal)/CLOCKS_PER_SEC );
-//            printf( "\n" );
-//            ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
-//            ABC_PRMn( "SAT", 42 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
-//            printf( "Simples = %6d. ", p->nBufNum );
-//            printf( "Dups = %6d. ", p->nDupNum );
-            printf( "\n" );
-            fflush( stdout );
-        }
-    }
-    // consider the next timeframe
-    if ( nJumpFrame && pPars->nStart == 0 )
-        pPars->iFrame = nJumpFrame - pPars->nFramesJump;
-    else if ( RetValue == -1 && pPars->nStart == 0 )
-        pPars->iFrame = f-1;
-//ABC_PRT( "CNF generation runtime", clkOther );
-    if ( pPars->fVerbose )
-    {
-//    ABC_PRMn( "Id2Var", (f+1)*p->nObjNums*4 );
-//    ABC_PRMn( "SAT", 48 * p->pSat->size + 16 * (int)p->pSat->stats.clauses + 4 * (int)p->pSat->stats.clauses_literals );
-//    printf( "Simples = %6d. ", p->nBufNum );
-//    printf( "Dups = %6d. ", p->nDupNum );
-//    printf( "\n" );
-    }
-    Saig_Bmc3ManStop( p );
-    fflush( stdout );
-    return RetValue;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/saig/saigCexMin.c b/src/aig/saig/saigCexMin.c
deleted file mode 100644
index f0fca2c4..00000000
--- a/src/aig/saig/saigCexMin.c
+++ /dev/null
@@ -1,578 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [saigCexMin.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Sequential AIG package.]
-
-  Synopsis    [CEX minimization.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: saigCexMin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "saig.h"
-#include "aig/ioa/ioa.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Find the roots to begin traversal.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManCexMinGetCos( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Int_t * vLeaves, Vec_Int_t * vRoots )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    Vec_IntClear( vRoots );
-    if ( vLeaves == NULL )
-    {
-        pObj = Aig_ManCo( pAig, pCex->iPo );
-        Vec_IntPush( vRoots, Aig_ObjId(pObj) );
-        return;
-    }
-    Aig_ManForEachObjVec( vLeaves, pAig, pObj, i )
-        if ( Saig_ObjIsLo(pAig, pObj) )
-            Vec_IntPush( vRoots, Aig_ObjId( Saig_ObjLoToLi(pAig, pObj) ) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects CI of the given timeframe.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManCexMinCollectFrameTerms_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vFrameCisOne )
-{
-    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
-        return;
-    Aig_ObjSetTravIdCurrent(pAig, pObj);
-    if ( Aig_ObjIsCo(pObj) )
-        Saig_ManCexMinCollectFrameTerms_rec( pAig, Aig_ObjFanin0(pObj), vFrameCisOne );
-    else if ( Aig_ObjIsNode(pObj) )
-    {
-        Saig_ManCexMinCollectFrameTerms_rec( pAig, Aig_ObjFanin0(pObj), vFrameCisOne );
-        Saig_ManCexMinCollectFrameTerms_rec( pAig, Aig_ObjFanin1(pObj), vFrameCisOne );
-    }
-    else if ( Aig_ObjIsCi(pObj) )
-        Vec_IntPush( vFrameCisOne, Aig_ObjId(pObj) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects CIs of all timeframes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Vec_t * Saig_ManCexMinCollectFrameTerms( Aig_Man_t * pAig, Abc_Cex_t * pCex )
-{
-    Vec_Vec_t * vFrameCis;
-    Vec_Int_t * vRoots, * vLeaves;
-    Aig_Obj_t * pObj;
-    int i, f;
-    // create terminals
-    vRoots = Vec_IntAlloc( 1000 );
-    vFrameCis = Vec_VecStart( pCex->iFrame+1 );
-    for ( f = pCex->iFrame; f >= 0; f-- )
-    {
-        // create roots
-        vLeaves = (f == pCex->iFrame) ? NULL : Vec_VecEntryInt(vFrameCis, f+1);
-        Saig_ManCexMinGetCos( pAig, pCex, vLeaves, vRoots );
-        // collect nodes starting from the roots
-        Aig_ManIncrementTravId( pAig );
-        Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
-            Saig_ManCexMinCollectFrameTerms_rec( pAig, pObj, Vec_VecEntryInt(vFrameCis, f) );
-    }
-    Vec_IntFree( vRoots );
-    return vFrameCis;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively sets phase and priority.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManCexMinDerivePhasePriority_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj )
-{
-    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
-        return;
-    Aig_ObjSetTravIdCurrent(pAig, pObj);
-    if ( Aig_ObjIsCo(pObj) )
-    {
-        Saig_ManCexMinDerivePhasePriority_rec( pAig, Aig_ObjFanin0(pObj) );
-        assert( Aig_ObjFanin0(pObj)->iData >= 0 );
-        pObj->iData = Aig_ObjFanin0(pObj)->iData ^ Aig_ObjFaninC0(pObj);
-    }
-    else if ( Aig_ObjIsNode(pObj) )
-    {
-        int fPhase0, fPhase1, iPrio0, iPrio1;
-        Saig_ManCexMinDerivePhasePriority_rec( pAig, Aig_ObjFanin0(pObj) );
-        Saig_ManCexMinDerivePhasePriority_rec( pAig, Aig_ObjFanin1(pObj) );
-        assert( Aig_ObjFanin0(pObj)->iData >= 0 );
-        assert( Aig_ObjFanin1(pObj)->iData >= 0 );
-        fPhase0 = Abc_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj);
-        fPhase1 = Abc_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj);
-        iPrio0  = Abc_Lit2Var( Aig_ObjFanin0(pObj)->iData );
-        iPrio1  = Abc_Lit2Var( Aig_ObjFanin1(pObj)->iData );
-        if ( fPhase0 && fPhase1 ) // both are one
-            pObj->iData = Abc_Var2Lit( Abc_MinInt(iPrio0, iPrio1), 1 );
-        else if ( !fPhase0 && fPhase1 ) 
-            pObj->iData = Abc_Var2Lit( iPrio0, 0 );
-        else if ( fPhase0 && !fPhase1 )
-            pObj->iData = Abc_Var2Lit( iPrio1, 0 );
-        else // both are zero
-            pObj->iData = Abc_Var2Lit( Abc_MaxInt(iPrio0, iPrio1), 0 );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Verify phase.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManCexMinVerifyPhase( Aig_Man_t * pAig, Abc_Cex_t * pCex, int f )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    Aig_ManConst1(pAig)->fPhase = 1;
-    Saig_ManForEachPi( pAig, pObj, i )
-        pObj->fPhase = Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + i);
-    if ( f == 0 )
-    {
-        Saig_ManForEachLo( pAig, pObj, i )
-            pObj->fPhase = 0;
-    }
-    else
-    {
-        Saig_ManForEachLo( pAig, pObj, i )
-            pObj->fPhase = Saig_ObjLoToLi(pAig, pObj)->fPhase;
-    }
-    Aig_ManForEachNode( pAig, pObj, i )
-        pObj->fPhase = (Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase) & 
-                       (Aig_ObjFaninC1(pObj) ^ Aig_ObjFanin1(pObj)->fPhase);
-    Aig_ManForEachCo( pAig, pObj, i )
-        pObj->fPhase = (Aig_ObjFaninC0(pObj) ^ Aig_ObjFanin0(pObj)->fPhase);
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects phase and priority of all timeframes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManCexMinDerivePhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis, Vec_Vec_t * vFramePPs, int f, Vec_Int_t * vRoots )
-{
-    Vec_Int_t * vFramePPsOne, * vFrameCisOne, * vLeaves;
-    Aig_Obj_t * pObj;
-    int i;
-    // set PP for the CIs
-    vFrameCisOne = Vec_VecEntryInt( vFrameCis, f );
-    vFramePPsOne = Vec_VecEntryInt( vFramePPs, f );
-    Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i )
-    {
-        pObj->iData = Vec_IntEntry( vFramePPsOne, i );
-        assert( pObj->iData >= 0 );
-    }
-//    if ( f == 0 )
-//        Saig_ManCexMinVerifyPhase( pAig, pCex, f );
-
-    // create roots
-    vLeaves = (f == pCex->iFrame) ? NULL : Vec_VecEntryInt(vFrameCis, f+1);
-    Saig_ManCexMinGetCos( pAig, pCex, vLeaves, vRoots );
-    // derive for the nodes starting from the roots
-    Aig_ManIncrementTravId( pAig );
-    Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
-    {
-        Saig_ManCexMinDerivePhasePriority_rec( pAig, pObj );
-//        if ( f == 0 )
-//            assert( (pObj->iData & 1) == pObj->fPhase );
-    }
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects phase and priority of all timeframes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
- 
-***********************************************************************/
-Vec_Vec_t * Saig_ManCexMinCollectPhasePriority_( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
-{
-    Vec_Vec_t * vFramePPs;
-    Vec_Int_t * vRoots, * vFramePPsOne, * vFrameCisOne;
-    Aig_Obj_t * pObj;
-    int i, f, nPrioOffset;
-
-    // initialize phase and priority
-    Aig_ManForEachObj( pAig, pObj, i )
-        pObj->iData = -1;
-
-    // set the constant node to higher priority than the flops
-    vFramePPs = Vec_VecStart( pCex->iFrame+1 );
-    nPrioOffset = (pCex->iFrame + 1) * pCex->nPis;
-    Aig_ManConst1(pAig)->iData = Abc_Var2Lit( nPrioOffset + pCex->nRegs, 1 );
-    vRoots = Vec_IntAlloc( 1000 );
-    for ( f = 0; f <= pCex->iFrame; f++ )
-    {
-        int nPiCount = 0;
-        // fill in PP for the CIs
-        vFrameCisOne = Vec_VecEntryInt( vFrameCis, f );
-        vFramePPsOne = Vec_VecEntryInt( vFramePPs, f );
-        assert( Vec_IntSize(vFramePPsOne) == 0 );
-        Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i )
-        {
-            assert( Aig_ObjIsCi(pObj) );
-            if ( Saig_ObjIsPi(pAig, pObj) )
-                Vec_IntPush( vFramePPsOne, Abc_Var2Lit( (f+1) * pCex->nPis - nPiCount++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj)) ) );
-            else if ( f == 0 )
-                Vec_IntPush( vFramePPsOne, Abc_Var2Lit( nPrioOffset + Saig_ObjRegId(pAig, pObj), 0 ) );
-            else
-                Vec_IntPush( vFramePPsOne, Saig_ObjLoToLi(pAig, pObj)->iData );
-        }
-        // compute the PP info
-        Saig_ManCexMinDerivePhasePriority( pAig, pCex, vFrameCis, vFramePPs, f, vRoots );
-    }
-    Vec_IntFree( vRoots );
-    // check the output
-    pObj = Aig_ManCo( pAig, pCex->iPo );
-    assert( Abc_LitIsCompl(pObj->iData) );
-    return vFramePPs;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects phase and priority of all timeframes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
- 
-***********************************************************************/
-Vec_Vec_t * Saig_ManCexMinCollectPhasePriority( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis )
-{
-    Vec_Vec_t * vFramePPs;
-    Vec_Int_t * vRoots, * vFramePPsOne, * vFrameCisOne;
-    Aig_Obj_t * pObj;
-    int i, f, nPrioOffset;
-
-    // initialize phase and priority
-    Aig_ManForEachObj( pAig, pObj, i )
-        pObj->iData = -1;
-
-    // set the constant node to higher priority than the flops
-    vFramePPs = Vec_VecStart( pCex->iFrame+1 );
-    nPrioOffset = pCex->nRegs;
-    Aig_ManConst1(pAig)->iData = Abc_Var2Lit( nPrioOffset + (pCex->iFrame + 1) * pCex->nPis, 1 );
-    vRoots = Vec_IntAlloc( 1000 );
-    for ( f = 0; f <= pCex->iFrame; f++ )
-    {
-        int nPiCount = 0;
-        // fill in PP for the CIs
-        vFrameCisOne = Vec_VecEntryInt( vFrameCis, f );
-        vFramePPsOne = Vec_VecEntryInt( vFramePPs, f );
-        assert( Vec_IntSize(vFramePPsOne) == 0 );
-        Aig_ManForEachObjVec( vFrameCisOne, pAig, pObj, i )
-        {
-            assert( Aig_ObjIsCi(pObj) );
-            if ( Saig_ObjIsPi(pAig, pObj) )
-                Vec_IntPush( vFramePPsOne, Abc_Var2Lit( nPrioOffset + (f+1) * pCex->nPis - 1 - nPiCount++, Abc_InfoHasBit(pCex->pData, pCex->nRegs + f * pCex->nPis + Aig_ObjCioId(pObj)) ) );
-            else if ( f == 0 )
-                Vec_IntPush( vFramePPsOne, Abc_Var2Lit( Saig_ObjRegId(pAig, pObj), 0 ) );
-            else
-                Vec_IntPush( vFramePPsOne, Saig_ObjLoToLi(pAig, pObj)->iData );
-        }
-        // compute the PP info
-        Saig_ManCexMinDerivePhasePriority( pAig, pCex, vFrameCis, vFramePPs, f, vRoots );
-    }
-    Vec_IntFree( vRoots );
-    // check the output
-    pObj = Aig_ManCo( pAig, pCex->iPo );
-    assert( Abc_LitIsCompl(pObj->iData) );
-    return vFramePPs;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Returns reasons for the property to fail.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManCexMinCollectReason_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vReason, int fPiReason )
-{
-    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
-        return;
-    Aig_ObjSetTravIdCurrent(p, pObj);
-    if ( Aig_ObjIsCi(pObj) )
-    {
-        if ( fPiReason && Saig_ObjIsPi(p, pObj) )
-            Vec_IntPush( vReason, Abc_Var2Lit( Aig_ObjCioId(pObj), !Abc_LitIsCompl(pObj->iData) ) );
-        else if ( !fPiReason && Saig_ObjIsLo(p, pObj) )
-            Vec_IntPush( vReason, Abc_Var2Lit( Saig_ObjRegId(p, pObj), !Abc_LitIsCompl(pObj->iData) ) );
-        return;
-    }
-    if ( Aig_ObjIsCo(pObj) )
-    {
-        Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
-        return;
-    }
-    if ( Aig_ObjIsConst1(pObj) )
-        return;
-    assert( Aig_ObjIsNode(pObj) );
-    if ( Abc_LitIsCompl(pObj->iData) ) // value 1
-    {
-        int fPhase0 = Abc_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj);
-        int fPhase1 = Abc_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj);
-        assert( fPhase0 && fPhase1 );
-        Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
-        Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin1(pObj), vReason, fPiReason );
-    }
-    else
-    {
-        int fPhase0 = Abc_LitIsCompl( Aig_ObjFanin0(pObj)->iData ) ^ Aig_ObjFaninC0(pObj);
-        int fPhase1 = Abc_LitIsCompl( Aig_ObjFanin1(pObj)->iData ) ^ Aig_ObjFaninC1(pObj);
-        assert( !fPhase0 || !fPhase1 );
-        if ( !fPhase0 && fPhase1 )
-            Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
-        else if ( fPhase0 && !fPhase1 )
-            Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin1(pObj), vReason, fPiReason );
-        else 
-        {
-            int iPrio0 = Abc_Lit2Var( Aig_ObjFanin0(pObj)->iData );
-            int iPrio1 = Abc_Lit2Var( Aig_ObjFanin1(pObj)->iData );
-            if ( iPrio0 >= iPrio1 )
-                Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin0(pObj), vReason, fPiReason );
-            else
-                Saig_ManCexMinCollectReason_rec( p, Aig_ObjFanin1(pObj), vReason, fPiReason );
-        }
-    }
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Collects phase and priority of all timeframes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Vec_t * Saig_ManCexMinCollectReason( Aig_Man_t * pAig, Abc_Cex_t * pCex, Vec_Vec_t * vFrameCis, Vec_Vec_t * vFramePPs, int fPiReason )
-{
-    Vec_Vec_t * vFrameReas;
-    Vec_Int_t * vRoots, * vLeaves;
-    Aig_Obj_t * pObj;
-    int i, f;
-    // select reason for the property to fail
-    vFrameReas = Vec_VecStart( pCex->iFrame+1 );
-    vRoots = Vec_IntAlloc( 1000 );
-    for ( f = pCex->iFrame; f >= 0; f-- )
-    {
-        // set phase and polarity
-        Saig_ManCexMinDerivePhasePriority( pAig, pCex, vFrameCis, vFramePPs, f, vRoots );
-        // create roots
-        vLeaves = (f == pCex->iFrame) ? NULL : Vec_VecEntryInt(vFrameCis, f+1);
-        Saig_ManCexMinGetCos( pAig, pCex, vLeaves, vRoots );
-        // collect nodes starting from the roots
-        Aig_ManIncrementTravId( pAig );
-        Aig_ManForEachObjVec( vRoots, pAig, pObj, i )
-            Saig_ManCexMinCollectReason_rec( pAig, pObj, Vec_VecEntryInt(vFrameReas, f), fPiReason );
-//printf( "%d(%d) ", Vec_VecLevelSize(vFrameCis, f), Vec_VecLevelSize(vFrameReas, f) ); 
-    }
-//printf( "\n" );
-    Vec_IntFree( vRoots );
-    return vFrameReas;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Vec_Vec_t * Saig_ManCexMinComputeReason( Aig_Man_t * pAig, Abc_Cex_t * pCex, int fPiReason )
-{
-    Vec_Vec_t * vFrameCis, * vFramePPs, * vFrameReas;
-    // sanity checks
-    assert( pCex->nPis == Saig_ManPiNum(pAig) );
-    assert( pCex->nRegs == Saig_ManRegNum(pAig) );
-    assert( pCex->iPo >= 0 && pCex->iPo < Saig_ManPoNum(pAig) );
-    // derive frame terms
-    vFrameCis = Saig_ManCexMinCollectFrameTerms( pAig, pCex );
-    // derive phase and priority
-    vFramePPs = Saig_ManCexMinCollectPhasePriority( pAig, pCex, vFrameCis );
-    // derive reasons for property failure
-    vFrameReas = Saig_ManCexMinCollectReason( pAig, pCex, vFrameCis, vFramePPs, fPiReason );
-    Vec_VecFree( vFramePPs );
-    Vec_VecFree( vFrameCis );
-    return vFrameReas;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicate with literals.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_ManCexMinDupWithCubes( Aig_Man_t * pAig, Vec_Vec_t * vReg2Value )
-{
-    Vec_Int_t * vLevel;
-    Aig_Man_t * pAigNew;
-    Aig_Obj_t * pObj, * pMiter;
-    int i, k, Lit;
-    assert( pAig->nConstrs == 0 );
-    // start the new manager
-    pAigNew = Aig_ManStart( Aig_ManNodeNum(pAig) + Vec_VecSizeSize(vReg2Value) + Vec_VecSize(vReg2Value) );
-    pAigNew->pName = Abc_UtilStrsav( pAig->pName );
-    // map the constant node
-    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pAigNew );
-    // create variables for PIs
-    Aig_ManForEachCi( pAig, pObj, i )
-        pObj->pData = Aig_ObjCreateCi( pAigNew );
-    // add internal nodes of this frame
-    Aig_ManForEachNode( pAig, pObj, i )
-        pObj->pData = Aig_And( pAigNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    // create POs for cubes
-    Vec_VecForEachLevelInt( vReg2Value, vLevel, i )
-    {
-        if ( i == 0 )
-            continue;
-        pMiter = Aig_ManConst1( pAigNew );
-        Vec_IntForEachEntry( vLevel, Lit, k )
-        {
-            assert( Lit >= 0 && Lit < 2 * Aig_ManRegNum(pAig) );
-            pObj = Saig_ManLi( pAig, Abc_Lit2Var(Lit) );
-            pMiter = Aig_And( pAigNew, pMiter, Aig_NotCond(Aig_ObjChild0Copy(pObj), Abc_LitIsCompl(Lit)) );
-        }
-        Aig_ObjCreateCo( pAigNew, pMiter );
-    }
-    // transfer to register outputs
-    Saig_ManForEachLi( pAig, pObj, i )
-        Aig_ObjCreateCo( pAigNew, Aig_ObjChild0Copy(pObj) );
-    // finalize
-    Aig_ManCleanup( pAigNew );
-    Aig_ManSetRegNum( pAigNew, Aig_ManRegNum(pAig) );
-    return pAigNew;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Saig_ManCexMinPerform( Aig_Man_t * pAig, Abc_Cex_t * pCex )
-{
-    int fReasonPi = 0;
-
-    Abc_Cex_t * pCexMin = NULL;
-    Aig_Man_t * pManNew = NULL;
-    Vec_Vec_t * vFrameReas;
-    vFrameReas = Saig_ManCexMinComputeReason( pAig, pCex, fReasonPi );
-    printf( "Reason size = %d.  Ave = %d.\n", Vec_VecSizeSize(vFrameReas), Vec_VecSizeSize(vFrameReas)/(pCex->iFrame + 1) );
-
-    // try reducing the frames
-    if ( !fReasonPi )
-    {
-        char * pFileName = "aigcube.aig";
-        pManNew = Saig_ManCexMinDupWithCubes( pAig, vFrameReas );
-        Ioa_WriteAiger( pManNew, pFileName, 0, 0 );
-        Aig_ManStop( pManNew );
-        printf( "Intermediate AIG is written into file \"%s\".\n", pFileName );
-    }
-
-    // find reduced counter-example
-    Vec_VecFree( vFrameReas );
-    return pCexMin;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/saig/saigTempor.c b/src/aig/saig/saigTempor.c
index 040df1f9..4e884140 100644
--- a/src/aig/saig/saigTempor.c
+++ b/src/aig/saig/saigTempor.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "saig.h"
+#include "sat/bmc/bmc.h"
 
 ABC_NAMESPACE_IMPL_START