Isolating BMC code into a separate package.

9 files changed, 3941 insertions, 0 deletions

diff --git a/src/sat/bmc/bmc.c b/src/sat/bmc/bmc.c
new file mode 100644
index 00000000..2dde80ab
--- /dev/null
+++ b/src/sat/bmc/bmc.c
@@ -0,0 +1,52 @@
+/**CFile****************************************************************
+
+  FileName    [bmc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bmc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
new file mode 100644
index 00000000..633dc205
--- /dev/null
+++ b/src/sat/bmc/bmc.h
@@ -0,0 +1,88 @@
+/**CFile****************************************************************
+
+  FileName    [bmc.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmc.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC___sat_bmc_BMC_h
+#define ABC___sat_bmc_BMC_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "aig/saig/saig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+ 
+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
+};
+
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    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 );
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/sat/bmc/bmcBmc.c b/src/sat/bmc/bmcBmc.c
new file mode 100644
index 00000000..56bb7ca6
--- /dev/null
+++ b/src/sat/bmc/bmcBmc.c
@@ -0,0 +1,339 @@
+/**CFile****************************************************************
+
+  FileName    [bmcBmc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    [Simple BMC package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmcBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig/saig/saig.h"
+#include "proof/fra/fra.h"
+#include "sat/cnf/cnf.h"
+#include "sat/bsat/satStore.h"
+#include "bmc.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/sat/bmc/bmcBmc2.c b/src/sat/bmc/bmcBmc2.c
new file mode 100644
index 00000000..778fe8e0
--- /dev/null
+++ b/src/sat/bmc/bmcBmc2.c
@@ -0,0 +1,885 @@
+/**CFile****************************************************************
+
+  FileName    [bmcBmc2.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    [Simple BMC package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmcBmc2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig/saig/saig.h"
+#include "sat/cnf/cnf.h"
+#include "sat/bsat/satStore.h"
+#include "proof/ssw/ssw.h"
+#include "bmc.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/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
new file mode 100644
index 00000000..a29be146
--- /dev/null
+++ b/src/sat/bmc/bmcBmc3.c
@@ -0,0 +1,1576 @@
+/**CFile****************************************************************
+
+  FileName    [bmcBmc3.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  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: bmcBmc3.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig/saig/saig.h"
+#include "proof/fra/fra.h"
+#include "sat/cnf/cnf.h"
+#include "sat/bsat/satStore.h"
+#include "bmc.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/sat/bmc/bmcCexCut.c b/src/sat/bmc/bmcCexCut.c
new file mode 100644
index 00000000..3cc81d97
--- /dev/null
+++ b/src/sat/bmc/bmcCexCut.c
@@ -0,0 +1,52 @@
+/**CFile****************************************************************
+
+  FileName    [bmcCexCut.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmcCexCut.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bmc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bmc/bmcCexMin1.c b/src/sat/bmc/bmcCexMin1.c
new file mode 100644
index 00000000..3b0a0274
--- /dev/null
+++ b/src/sat/bmc/bmcCexMin1.c
@@ -0,0 +1,579 @@
+/**CFile****************************************************************
+
+  FileName    [bmcCexMin1.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    [CEX minimization.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmcCexMin1.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig/saig/saig.h"
+#include "aig/ioa/ioa.h"
+#include "bmc.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/sat/bmc/bmcCexMin2.c b/src/sat/bmc/bmcCexMin2.c
new file mode 100644
index 00000000..076d744c
--- /dev/null
+++ b/src/sat/bmc/bmcCexMin2.c
@@ -0,0 +1,363 @@
+/**CFile****************************************************************
+
+  FileName    [bmcCexMin2.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [SAT-based bounded model checking.]
+
+  Synopsis    [CEX minimization.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bmcCexMin2.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "aig/gia/gia.h"
+#include "bmc.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int  Abc_InfoGet2Bits( Vec_Int_t * vData, int nWords, int iFrame, int iObj )
+{
+    unsigned * pInfo = (unsigned *)Vec_IntEntryP( vData, nWords * iFrame );
+    return 3 & (pInfo[iObj >> 4] >> ((iObj & 15) << 1));
+}
+static inline void Abc_InfoSet2Bits( Vec_Int_t * vData, int nWords, int iFrame, int iObj, int Value )
+{
+    unsigned * pInfo = (unsigned *)Vec_IntEntryP( vData, nWords * iFrame );
+    Value ^= (3 & (pInfo[iObj >> 4] >> ((iObj & 15) << 1)));
+    pInfo[iObj >> 4] ^= (Value << ((iObj & 15) << 1));
+}
+static inline void Abc_InfoAdd2Bits( Vec_Int_t * vData, int nWords, int iFrame, int iObj, int Value )
+{
+    unsigned * pInfo = (unsigned *)Vec_IntEntryP( vData, nWords * iFrame );
+    pInfo[iObj >> 4] |= (Value << ((iObj & 15) << 1));
+}
+
+static inline int  Gia_ManGetTwo( Gia_Man_t * p, int iFrame, Gia_Obj_t * pObj )              { return Abc_InfoGet2Bits( p->vTruths, p->nTtWords, iFrame, Gia_ObjId(p, pObj) ); }
+static inline void Gia_ManSetTwo( Gia_Man_t * p, int iFrame, Gia_Obj_t * pObj, int Value )   { Abc_InfoSet2Bits( p->vTruths, p->nTtWords, iFrame, Gia_ObjId(p, pObj), Value ); }
+static inline void Gia_ManAddTwo( Gia_Man_t * p, int iFrame, Gia_Obj_t * pObj, int Value )   { Abc_InfoAdd2Bits( p->vTruths, p->nTtWords, iFrame, Gia_ObjId(p, pObj), Value ); }
+
+/*
+    For CEX minimization, all terminals (const0, PI, RO in frame0) have equal priority.
+    For abstraction refinement, all terminals, except PPis, have higher priority.
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Annotates the unrolling with CEX value/priority.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Gia_ManAnnotateUnrolling( Gia_Man_t * p, Abc_Cex_t * pCex, int fJustMax )
+{
+    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+    int RetValue, f, k, Value, Value0, Value1, iBit;
+    // start storage for internal info
+    assert( p->vTruths == NULL );
+    p->nTtWords = Abc_BitWordNum( 2 * Gia_ManObjNum(p) );
+    p->vTruths  = Vec_IntStart( (pCex->iFrame + 1) * p->nTtWords );
+    // assign values to all objects (const0 and RO in frame0 are assigned 0)
+    Gia_ManCleanMark0(p);
+    for ( f = 0, iBit = pCex->nRegs; f <= pCex->iFrame; f++ )
+    {
+        Gia_ManForEachPi( p, pObj, k )
+            if ( (pObj->fMark0 = Abc_InfoHasBit(pCex->pData, iBit++)) )
+                Gia_ManAddTwo( p, f, pObj, 1 );
+        Gia_ManForEachAnd( p, pObj, k )
+            if ( (pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj))) )
+                Gia_ManAddTwo( p, f, pObj, 1 );
+        Gia_ManForEachCo( p, pObj, k )
+            if ( (pObj->fMark0 = Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) )
+                Gia_ManAddTwo( p, f, pObj, 1 );
+        if ( f == pCex->iFrame )
+            break;
+        Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
+            if ( (pObjRo->fMark0 = pObjRi->fMark0) )
+                Gia_ManAddTwo( p, f+1, pObjRo, 1 );
+    }
+    assert( iBit == pCex->nBits );
+    // check the output value
+    RetValue = Gia_ManPo(p, pCex->iPo)->fMark0;
+    if ( RetValue != 1 )
+        printf( "Counter-example is invalid.\n" );
+    // assign justification to nodes
+    Gia_ManCleanMark0(p);
+    pObj = Gia_ManPo(p, pCex->iPo);
+    pObj->fMark0 = 1;
+    Gia_ManAddTwo( p, pCex->iFrame, pObj, 2 );
+    for ( f = pCex->iFrame; f >= 0; f-- )
+    {
+        // transfer to CO drivers
+        Gia_ManForEachCo( p, pObj, k )
+            if ( (Gia_ObjFanin0(pObj)->fMark0 = pObj->fMark0) )
+            {
+                pObj->fMark0 = 0;
+                Gia_ManAddTwo( p, f, Gia_ObjFanin0(pObj), 2 );
+            }
+        // compute justification
+        Gia_ManForEachAndReverse( p, pObj, k )
+        {
+            if ( !pObj->fMark0 ) 
+                continue;
+            pObj->fMark0 = 0;
+            Value = (1 & Gia_ManGetTwo(p, f, pObj));
+            Value0 = (1 & Gia_ManGetTwo(p, f, Gia_ObjFanin0(pObj))) ^ Gia_ObjFaninC0(pObj);
+            Value1 = (1 & Gia_ManGetTwo(p, f, Gia_ObjFanin1(pObj))) ^ Gia_ObjFaninC1(pObj);
+            if ( Value0 == Value1 )
+            {
+                assert( Value == (Value0 & Value1) );
+                if ( fJustMax || Value == 1 )
+                {
+                    Gia_ObjFanin0(pObj)->fMark0 = Gia_ObjFanin1(pObj)->fMark0 = 1;
+                    Gia_ManAddTwo( p, f, Gia_ObjFanin0(pObj), 2 );
+                    Gia_ManAddTwo( p, f, Gia_ObjFanin1(pObj), 2 );
+                }
+                else
+                {
+                    Gia_ObjFanin0(pObj)->fMark0 = 1;
+                    Gia_ManAddTwo( p, f, Gia_ObjFanin0(pObj), 2 );
+                }
+            }
+            else if ( Value0 == 0 )
+            {
+                assert( Value == 0 );
+                Gia_ObjFanin0(pObj)->fMark0 = 1;
+                Gia_ManAddTwo( p, f, Gia_ObjFanin0(pObj), 2 );
+            }
+            else if ( Value1 == 0 )
+            {
+                assert( Value == 0 );
+                Gia_ObjFanin1(pObj)->fMark0 = 1;
+                Gia_ManAddTwo( p, f, Gia_ObjFanin1(pObj), 2 );
+            }
+            else assert( 0 );
+        }
+        if ( f == 0 )
+            break;
+        // transfer to RIs
+        Gia_ManForEachPi( p, pObj, k )
+            pObj->fMark0 = 0;
+        Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
+            if ( (pObjRi->fMark0 = pObjRo->fMark0) )
+            {
+                pObjRo->fMark0 = 0;
+                Gia_ManAddTwo( p, f-1, pObjRi, 2 );
+            }
+    }
+    Gia_ManCleanMark0(p);
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computing AIG characterizing all justifying assignments.]
+
+  Description [Used in CEX minimization.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Gia_ManCreateUnate( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrame, int nRealPis, int fUseAllObjects )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pObjRo, * pObjRi;
+    int f, k, Value;
+    assert( iFrame >= 0 && iFrame <= pCex->iFrame );
+    pNew = Gia_ManStart( 1000 );
+    pNew->pName = Abc_UtilStrsav( "unate" );
+    Gia_ManCleanValue( p );
+    // set flop outputs
+    if ( nRealPis < 0 ) // CEX min
+    {
+        Gia_ManForEachRo( p, pObj, k )
+        {
+            if ( fUseAllObjects )
+            {
+                int Value = Gia_ManAppendCi(pNew);
+                if ( (Gia_ManGetTwo(p, iFrame, pObj) >> 1) ) // in the path
+                    pObj->Value = Value;
+            }
+            else if ( (Gia_ManGetTwo(p, iFrame, pObj) >> 1) ) // in the path
+                pObj->Value = Gia_ManAppendCi(pNew);
+        }
+    }
+    else
+    {
+        Gia_ManForEachRo( p, pObj, k )
+            pObj->Value = (Gia_ManGetTwo(p, iFrame, pObj) >> 1);
+    }
+    Gia_ManHashAlloc( pNew );
+    for ( f = iFrame; f <= pCex->iFrame; f++ )
+    {
+/*
+        printf( "  F%03d ", f );
+        Gia_ManForEachRo( p, pObj, k )
+            printf( "%d", pObj->Value > 0 );
+        printf( "\n" );
+*/
+        // set const0 to const1 if present
+        pObj = Gia_ManConst0(p);
+        pObj->Value = (Gia_ManGetTwo(p, f, pObj) >> 1);
+        // set primary inputs 
+        if ( nRealPis < 0 ) // CEX min
+        {
+            Gia_ManForEachPi( p, pObj, k )
+                pObj->Value = (Gia_ManGetTwo(p, f, pObj) >> 1);
+        }
+        else
+        {
+            Gia_ManForEachPi( p, pObj, k )
+            {
+                pObj->Value = (Gia_ManGetTwo(p, f, pObj) >> 1);
+                if ( k >= nRealPis )
+                {
+                    if ( fUseAllObjects )
+                    {
+                        int Value = Gia_ManAppendCi(pNew);
+                        if ( (Gia_ManGetTwo(p, f, pObj) >> 1) ) // in the path
+                            pObj->Value = Value;
+                    }
+                    else if ( (Gia_ManGetTwo(p, f, pObj) >> 1) ) // in the path
+                        pObj->Value = Gia_ManAppendCi(pNew);
+                }
+            }
+        }
+        // traverse internal nodes
+        Gia_ManForEachAnd( p, pObj, k )
+        { 
+            pObj->Value = 0;
+            Value = Gia_ManGetTwo(p, f, pObj);
+            if ( !(Value >> 1) ) // not in the path
+                continue;
+            if ( Gia_ObjFanin0(pObj)->Value && Gia_ObjFanin1(pObj)->Value )
+            {
+                if ( 1 & Gia_ManGetTwo(p, f, pObj) ) // value 1
+                {
+                    if ( Gia_ObjFanin0(pObj)->Value > 1 && Gia_ObjFanin1(pObj)->Value > 1 )
+                        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
+                    else if ( Gia_ObjFanin0(pObj)->Value > 1 )
+                        pObj->Value = Gia_ObjFanin0(pObj)->Value;
+                    else if ( Gia_ObjFanin1(pObj)->Value > 1 )
+                        pObj->Value = Gia_ObjFanin1(pObj)->Value;
+                    else 
+                        pObj->Value = 1;
+                }
+                else // value 0
+                {
+                    if ( Gia_ObjFanin0(pObj)->Value > 1 && Gia_ObjFanin1(pObj)->Value > 1 )
+                        pObj->Value = Gia_ManHashOr( pNew, Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
+                    else if ( Gia_ObjFanin0(pObj)->Value > 1 )
+                        pObj->Value = Gia_ObjFanin0(pObj)->Value;
+                    else if ( Gia_ObjFanin1(pObj)->Value > 1 )
+                        pObj->Value = Gia_ObjFanin1(pObj)->Value;
+                    else 
+                        pObj->Value = 1;
+                }
+            }
+            else if ( Gia_ObjFanin0(pObj)->Value )
+                pObj->Value = Gia_ObjFanin0(pObj)->Value;
+            else if ( Gia_ObjFanin1(pObj)->Value )
+                pObj->Value = Gia_ObjFanin1(pObj)->Value;
+            else assert( 0 );
+        }
+        Gia_ManForEachCo( p, pObj, k )
+            pObj->Value = Gia_ObjFanin0(pObj)->Value;
+        if ( f == pCex->iFrame )
+            break;
+        Gia_ManForEachRiRo( p, pObjRi, pObjRo, k )
+            pObjRo->Value = pObjRi->Value;
+    }
+    Gia_ManHashStop( pNew );
+    // create primary output
+    pObj = Gia_ManPo(p, pCex->iPo);
+    assert( (Gia_ManGetTwo(p, pCex->iFrame, pObj) >> 1) );
+    assert( pObj->Value );
+    Gia_ManAppendCo( pNew, pObj->Value );
+    // cleanup
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Gia_ManCexMin( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrameStart, int nRealPis, int fJustMax, int fUseAll, int fVerbose )
+{
+    Gia_Man_t * pNew;
+    int f, RetValue;
+    // check CEX
+    assert( pCex->nPis == Gia_ManPiNum(p) );
+//    assert( pCex->nRegs == Gia_ManRegNum(p) );
+    assert( pCex->iPo < Gia_ManPoNum(p) );
+    // check frames
+    assert( iFrameStart >= 0 && iFrameStart <= pCex->iFrame );
+    // check primary inputs
+    assert( nRealPis < Gia_ManPiNum(p) );
+    // prepare
+    RetValue = Gia_ManAnnotateUnrolling( p, pCex, fJustMax );
+    if ( nRealPis >= 0 ) // refinement
+    {
+        pNew = Gia_ManCreateUnate( p, pCex, iFrameStart, nRealPis, fUseAll );
+        printf( "%3d : ", iFrameStart );
+        Gia_ManPrintStats( pNew, 0, 0, 0 );
+        if ( fVerbose )
+            Gia_WriteAiger( pNew, "temp.aig", 0, 0 );
+        Gia_ManStop( pNew );
+    }
+    else // CEX min
+    {
+        for ( f = pCex->iFrame; f >= iFrameStart; f-- )
+        {
+            pNew = Gia_ManCreateUnate( p, pCex, f, -1, fUseAll );
+            printf( "%3d : ", f );
+            Gia_ManPrintStats( pNew, 0, 0, 0 );
+            if ( fVerbose )
+                Gia_WriteAiger( pNew, "temp.aig", 0, 0 );
+            Gia_ManStop( pNew );
+        }
+    }
+    Vec_IntFreeP( &p->vTruths );
+    p->nTtWords = 0;
+    return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/sat/bmc/module.make b/src/sat/bmc/module.make
new file mode 100644
index 00000000..071834d8
--- /dev/null
+++ b/src/sat/bmc/module.make
@@ -0,0 +1,7 @@
+SRC +=    src/sat/bmc/bmc.c \
+    src/sat/bmc/bmcBmc.c \
+    src/sat/bmc/bmcBmc2.c \
+    src/sat/bmc/bmcBmc3.c \
+    src/sat/bmc/bmcCexCut.c \
+    src/sat/bmc/bmcCexMin1.c \
+    src/sat/bmc/bmcCexMin2.c