Version abc81025

6 files changed, 809 insertions, 217 deletions

diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index 48d91438..7063bd2a 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -1,5 +1,6 @@
 SRC +=    src/aig/saig/saigAbs.c \
     src/aig/saig/saigBmc.c \
+    src/aig/saig/saigBmc2.c \
     src/aig/saig/saigCone.c \
     src/aig/saig/saigDup.c \
     src/aig/saig/saigHaig.c \
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index f0c8fb54..a6f5631b 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -99,6 +99,7 @@ extern Aig_Man_t *       Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, in
 extern Aig_Man_t *       Saig_ManCreateMiterComb( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
 extern Aig_Man_t *       Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFrames );
 extern int               Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 );
+extern int               Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 );
 /*=== saigPhase.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrames, int fIgnore, int fPrint, int fVerbose );
 /*=== saigRetFwd.c ==========================================================*/
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index 5776cd4a..0bbf63f9 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -26,62 +26,172 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+#define AIG_VISITED       ((Aig_Obj_t *)(PORT_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                   nConfMaxOne;    // the max number of conflicts at a target
+    int                   nConfMaxAll;    // the max number of conflicts for all targets
+    int                   nNodesMax;      // the max number of nodes to add
+    int                   fVerbose;       // enables verbose output
+    // AIG managers
+    Aig_Man_t *           pAig;           // the user's AIG manager
+    Aig_Man_t *           pFrm;           // Frames manager
+    Vec_Ptr_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
+    Vec_Int_t *           vObj2Var;       // mapping of frames objects in CNF variables
+    int                   nSatVars;       // the number of used SAT variables
+    Vec_Ptr_t *           vTargets;       // targets to be solved in this interval
+    int                   iFramelast;     // last frame  
+    int                   iOutputLast;    // last output
+};
+
+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);      }
+
+static inline Aig_Obj_t * Saig_BmcObjFrame( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )                       { return Vec_PtrGetEntry( p->vAig2Frm, p->nObjs*i+pObj->Id );     }
+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 );     }
+
+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));  }
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    [Create timeframes of the manager for BMC.]
+  Synopsis    [Create manager.]
 
-  Description [The resulting manager is combinational. POs correspond to \
-  the property outputs in each time-frame.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
+Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nNodesMax, int fVerbose )
 {
-    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_Bmc_t * p;
+    Aig_Obj_t * pObj;
+    int i, Lit;
+    assert( Aig_ManRegNum(pAig) > 0 );
+    p = (Saig_Bmc_t *)malloc( sizeof(Saig_Bmc_t) );
+    memset( p, 0, sizeof(Saig_Bmc_t) );
+    // set parameters
+    p->nFramesMax   = 1000000;
+    p->nConfMaxOne  = nConfMaxOne;
+    p->nConfMaxAll  = nConfMaxAll;
+    p->nNodesMax    = nNodesMax;
+    p->fVerbose     = fVerbose;
+    p->pAig         = pAig;
+    p->nObjs        = Aig_ManObjNumMax(pAig);
+    // create node and variable mappings
+    p->vAig2Frm     = Vec_PtrAlloc( 0 );
+    Vec_PtrFill( p->vAig2Frm, 5 * p->nObjs, NULL );
+    p->vObj2Var     = Vec_IntAlloc( 0 );
+    Vec_IntFill( p->vObj2Var, 5 * p->nObjs, 0 );
+    // start the AIG manager and map primary inputs
+    p->pFrm         = Aig_ManStart( 5 * p->nObjs );
     Saig_ManForEachLo( pAig, pObj, i )
-        pObj->pData = Aig_ManConst0( pFrames );
-    // add timeframes
-    for ( f = 0; f < nFrames; f++ )
+        Saig_BmcObjSetFrame( p, pObj, 0, Aig_ManConst0(p->pFrm) ); 
+    // create SAT solver
+    p->pSat         = sat_solver_new();
+    sat_solver_setnvars( p->pSat, 2000 );
+    p->nSatVars = 1;
+    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( 0 );
+    p->vVisited     = Vec_PtrAlloc( 0 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Delete manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_BmcManStop( Saig_Bmc_t * p )
+{
+    Aig_ManStop( p->pFrm  );
+    Vec_PtrFree( p->vAig2Frm );
+    Vec_IntFree( p->vObj2Var );
+    sat_solver_delete( p->pSat );
+    Vec_PtrFree( p->vTargets );
+    Vec_PtrFree( p->vVisited );
+    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_ObjIsPo( pObj ) )
     {
-        // create PI nodes for this frame
-        Saig_ManForEachPi( pAig, pObj, i )
-            pObj->pData = Aig_ObjCreatePi( 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_ObjCreatePo( 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;
+        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_Not(pConst1);
+        else if ( Aig_Regular(p0) == pConst1 )
+            pRes = (p0 == pConst1) ? p1 : Aig_Not(pConst1);
+        else if ( Aig_Regular(p1) == pConst1 )
+            pRes = (p1 == pConst1) ? p0 : Aig_Not(pConst1);
+        else 
+            pRes = AIG_VISITED;
+
+        if ( pRes != pConst1 && pRes != Aig_Not(pConst1) )
+            pRes = AIG_VISITED;
     }
-    Aig_ManCleanup( pFrames );
-    return pFrames;
+    Saig_BmcObjSetFrame( p, pObj, i, pRes );
+    return pRes;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns the number of internal nodes that are not counted yet.]
+  Synopsis    [Performs the actual construction of the output.]
 
   Description []
                
@@ -90,81 +200,70 @@ Aig_Man_t * Saig_ManFramesBmc( Aig_Man_t * pAig, int nFrames )
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManFramesCount_rec( Aig_Man_t * p, Aig_Obj_t * pObj )
+Aig_Obj_t * Saig_BmcIntervalConstruct_rec( Saig_Bmc_t * p, Aig_Obj_t * pObj, int i )
 {
-    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) );
+    Aig_Obj_t * pRes;
+    pRes = Saig_BmcObjFrame( p, pObj, i );
+    assert( pRes != NULL );
+    if ( pRes != AIG_VISITED )
+        return pRes;
+    if ( Saig_ObjIsPi( p->pAig, pObj ) )
+        pRes = Aig_ObjCreatePi(p->pFrm);
+    else if ( Saig_ObjIsLo( p->pAig, pObj ) )
+        pRes = Saig_BmcIntervalConstruct_rec( p, Saig_ObjLoToLi(p->pAig, pObj), i-1 );
+    else if ( Aig_ObjIsPo( pObj ) )
+    {
+        Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i );
+        pRes = Saig_BmcObjChild0( p, pObj, i );
+    }
+    else 
+    {
+        Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin0(pObj), i );
+        Saig_BmcIntervalConstruct_rec( p, Aig_ObjFanin1(pObj), i );
+        pRes = Aig_And( p->pFrm, Saig_BmcObjChild0(p, pObj, i), Saig_BmcObjChild1(p, pObj, i) );
+    }
+    Saig_BmcObjSetFrame( p, pObj, i, pRes );
+    return pRes;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Create timeframes of the manager for BMC.]
+  Synopsis    [Adds new AIG nodes to the frames.]
 
-  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.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax )
+void Saig_BmcInterval( Saig_Bmc_t * p )
 {
-    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++ )
+    Aig_Obj_t * pTarget, * pObj;
+    int i, nNodes = Aig_ManNodeNum( p->pFrm );
+    Vec_PtrClear( p->vTargets );
+    for ( ; p->iFramelast < p->nFramesMax; p->iFramelast++, p->iOutputLast = 0 )
     {
-        // create PI nodes for this frame
-        Saig_ManForEachPi( pAig, pObj, i )
-            pObj->pData = Aig_ObjCreatePi( 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 )
+        if ( p->iOutputLast == 0 )
         {
-            pObjPo = Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
-            Counter += Saig_ManFramesCount_rec( pFrames, Aig_ObjFanin0(pObjPo) );
+            Saig_BmcObjSetFrame( p, Aig_ManConst1(p->pAig), p->iFramelast, Aig_ManConst1(p->pFrm) );
+            Saig_ManForEachPi( p->pAig, pObj, i )
+                Saig_BmcObjSetFrame( p, pObj, p->iFramelast, Aig_ObjCreatePi(p->pFrm) ); 
         }
-        if ( Counter >= nSizeMax )
+        for ( ; p->iOutputLast < Saig_ManPoNum(p->pAig); p->iOutputLast++ )
         {
-            Aig_ManCleanup( pFrames );
-            return pFrames;
+            if ( Aig_ManNodeNum(p->pFrm) >= nNodes + p->nNodesMax )
+                return;
+            Saig_BmcIntervalExplore_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->nFramesMax );
+            pTarget = Saig_BmcIntervalConstruct_rec( p, Aig_ManPo(p->pAig, p->iOutputLast), p->nFramesMax );
+            Vec_PtrPush( p->vTargets, pTarget );
         }
-        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    [Performs BMC for the given AIG.]
+  Synopsis    [Performs the actual construction of the output.]
 
   Description []
                
@@ -173,140 +272,179 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax
   SeeAlso     []
 
 ***********************************************************************/
-int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLimit, int fRewrite, int fVerbose, int * piFrame )
+Aig_Obj_t * Saig_BmcIntervalToAig_rec( Saig_Bmc_t * p, Aig_Man_t * pNew, Aig_Obj_t * pObj )
 {
-    sat_solver * pSat;
-    Cnf_Dat_t * pCnf;
-    Aig_Man_t * pFrames, * pAigTemp;
-    Aig_Obj_t * pObj;
-    int status, clk, Lit, i, RetValue = 1;
-    // derive the timeframes
-    clk = clock();
-    if ( nSizeMax > 0 )
-    {
-        pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax );
-        nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0);
-    }
-    else
-        pFrames = Saig_ManFramesBmc( pAig, nFrames );
-    if ( piFrame )
-        *piFrame = nFrames;
-    if ( fVerbose )
+    if ( pObj->pData )
+        return pObj->pData;
+    Vec_PtrPush( p->vVisited, pObj );
+    if ( Saig_BmcSatNum(p, pObj) || Aig_ObjIsPi(pObj) )
+        return pObj->pData = Aig_ObjCreatePi(pNew);
+    Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin0(pObj) );
+    Saig_BmcIntervalToAig_rec( p, pNew, Aig_ObjFanin1(pObj) );
+    return 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;
+    pNew = Aig_ManStart( p->nNodesMax );
+    Aig_ManConst1(p->pFrm)->pData = Aig_ManConst1(pNew);
+    Vec_PtrClear( p->vVisited );
+    Vec_PtrPush( p->vVisited, Aig_ManConst1(p->pFrm) );
+    Vec_PtrForEachEntry( p->vTargets, pObj, i )
     {
-        printf( "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_ManPiNum(pFrames), Aig_ManPoNum(pFrames), 
-            Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
-        PRT( "Time", clock() - clk );
-        fflush( stdout );
+        pObjNew = Saig_BmcIntervalToAig_rec( p, pNew, Aig_Regular(pObj) );
+        Aig_ObjCreatePo( pNew, pObjNew );
     }
-    // rewrite the timeframes
-    if ( fRewrite )
+    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;
+    Vec_PtrForEachEntry( p->vVisited, pObj, i )
     {
-        clk = clock();
-//        pFrames = Dar_ManBalance( pAigTemp = pFrames, 0 );
-        pFrames = Dar_ManRwsat( pAigTemp = pFrames, 1, 0 );
-        Aig_ManStop( pAigTemp );
-        if ( fVerbose )
+        pObjNew   = pObj->pData;
+        pObj->pData = NULL;
+        VarNumNew = pCnf->pVarNums[ pObjNew->Id ];
+        if ( VarNumNew == -1 )
+            continue;
+        VarNumOld = Saig_BmcSatNum( p, pObj );
+        if ( VarNumOld == 0 )
         {
-            printf( "Time-frames after rewriting:  Node = %6d. Lev = %5d.  ", 
-                Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
-            PRT( "Time", clock() - clk );
-            fflush( stdout );
+            Saig_BmcSetSatNum( p, pObj, VarNumNew );
+            continue;
         }
-    }
-    // create the SAT solver
-    clk = clock();
-    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );  
-    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] ) )
+        // 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 );
     }
-    if ( fVerbose )
+    // 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     []
+
+***********************************************************************/
+int Saig_BmcSolveTargets( Saig_Bmc_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, VarNum, Lit, RetValue;
+    assert( Vec_PtrSize(p->vTargets) > 0 );
+    Vec_PtrForEachEntry( p->vTargets, pObj, i )
     {
-        printf( "CNF: Variables = %6d. Clauses = %7d. Literals = %8d. ", pCnf->nVars, pCnf->nClauses, pCnf->nLiterals );
-        PRT( "Time", clock() - clk );
-        fflush( stdout );
+        if ( 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, (sint64)p->nConfMaxOne, (sint64)0, (sint64)0, (sint64)0 );
+        if ( RetValue == l_False ) // unsat
+            continue;
+        if ( RetValue == l_Undef ) // undecided
+            return l_Undef;
+        // generate counter-example
+        return l_True;
     }
-    status = sat_solver_simplify(pSat);
-    if ( status == 0 )
+    return l_False;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs BMC with the given parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Saig_BmcPerform( Aig_Man_t * pAig, int nConfMaxOne, int nConfMaxAll, int nNodesMax, int fVerbose )
+{
+    Saig_Bmc_t * p;
+    Aig_Man_t * pNew;
+    Cnf_Dat_t * pCnf;
+    int RetValue, clk = clock();
+    p = Saig_BmcManStart( pAig, nConfMaxOne, nConfMaxAll, nNodesMax, fVerbose );
+    while ( 1 )
     {
-        if ( fVerbose )
-        {
-            printf( "The BMC problem is trivially UNSAT\n" );
-            fflush( stdout );
-        }
+        // add new logic slice to frames
+        Saig_BmcInterval( p );
+        if ( Vec_PtrSize(p->vTargets) == 0 )
+            break;
+        // convert logic slice into new AIG
+        pNew = Saig_BmcIntervalToAig( p );
+        // derive CNF for the new AIG
+        pCnf = Cnf_Derive( pNew, Aig_ManPoNum(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 );
+        if ( RetValue != l_False )
+            break;
     }
+    if ( RetValue == l_True )
+        printf( "BMC failed for output %d in frame %d.  ", p->iOutputLast, p->iFramelast );
+    else // if ( RetValue == l_False || RetValue == l_Undef )
+        printf( "BMC completed for %d timeframes.  ", p->iFramelast );
+    PRT( "Time", clock() - clk );
+    if ( p->iFramelast >= p->nFramesMax )
+        printf( "Reached limit on the number of timeframes (%d).\n", p->nFramesMax );
+    else if ( p->pSat->stats.conflicts > p->nConfMaxAll )
+        printf( "Reached global conflict limit (%d).\n", p->nConfMaxAll );
     else
-    {
-        int clkPart = clock();
-        Aig_ManForEachPo( pFrames, pObj, i )
-        {
-            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, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)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 );
-                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 )
-            {
-                extern void * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
-                Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
-                int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
-                pModel[Aig_ManPiNum(pFrames)] = pObj->Id;
-                pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel );
-                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;
+        printf( "Reached local conflict limit (%d).\n", p->nConfMaxOne );
+    Saig_BmcManStop( p );
 }
 
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
new file mode 100644
index 00000000..5776cd4a
--- /dev/null
+++ b/src/aig/saig/saigBmc2.c
@@ -0,0 +1,314 @@
+/**CFile****************************************************************
+
+  FileName    [saigBmc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Sequential AIG package.]
+
+  Synopsis    [Simple BMC package.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: saigBmc.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "saig.h"
+#include "cnf.h"
+#include "satStore.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        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_ObjCreatePi( 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_ObjCreatePo( 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_ObjCreatePi( 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_ObjCreatePo( 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;
+}
+
+/**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 )
+{
+    sat_solver * pSat;
+    Cnf_Dat_t * pCnf;
+    Aig_Man_t * pFrames, * pAigTemp;
+    Aig_Obj_t * pObj;
+    int status, clk, Lit, i, RetValue = 1;
+    // derive the timeframes
+    clk = clock();
+    if ( nSizeMax > 0 )
+    {
+        pFrames = Saig_ManFramesBmcLimit( pAig, nFrames, nSizeMax );
+        nFrames = Aig_ManPoNum(pFrames) / Saig_ManPoNum(pAig) + ((Aig_ManPoNum(pFrames) % Saig_ManPoNum(pAig)) > 0);
+    }
+    else
+        pFrames = Saig_ManFramesBmc( pAig, nFrames );
+    if ( piFrame )
+        *piFrame = nFrames;
+    if ( fVerbose )
+    {
+        printf( "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_ManPiNum(pFrames), Aig_ManPoNum(pFrames), 
+            Aig_ManNodeNum(pFrames), Aig_ManLevelNum(pFrames) );
+        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) );
+            PRT( "Time", clock() - clk );
+            fflush( stdout );
+        }
+    }
+    // create the SAT solver
+    clk = clock();
+    pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );  
+    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 );
+        PRT( "Time", clock() - clk );
+        fflush( stdout );
+    }
+    status = sat_solver_simplify(pSat);
+    if ( status == 0 )
+    {
+        if ( fVerbose )
+        {
+            printf( "The BMC problem is trivially UNSAT\n" );
+            fflush( stdout );
+        }
+    }
+    else
+    {
+        int clkPart = clock();
+        Aig_ManForEachPo( pFrames, pObj, i )
+        {
+            Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
+            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, (sint64)nConfLimit, (sint64)0, (sint64)0, (sint64)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 );
+                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 )
+            {
+                extern void * Fra_SmlCopyCounterExample( Aig_Man_t * pAig, Aig_Man_t * pFrames, int * pModel );
+                Vec_Int_t * vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
+                int * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
+                pModel[Aig_ManPiNum(pFrames)] = pObj->Id;
+                pAig->pSeqModel = Fra_SmlCopyCounterExample( pAig, pFrames, pModel );
+                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                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/saig/saigMiter.c b/src/aig/saig/saigMiter.c
index 5efcd24d..cc71f371 100644
--- a/src/aig/saig/saigMiter.c
+++ b/src/aig/saig/saigMiter.c
@@ -49,6 +49,8 @@ Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p0, Aig_Man_t * p1, int Oper )
     assert( Saig_ManPoNum(p0) == Saig_ManPoNum(p1) );
     pNew = Aig_ManStart( Aig_ManObjNumMax(p0) + Aig_ManObjNumMax(p1) );
     pNew->pName = Aig_UtilStrsav( "miter" );
+    Aig_ManCleanData( p0 );
+    Aig_ManCleanData( p1 );
     // map constant nodes
     Aig_ManConst1(p0)->pData = Aig_ManConst1(pNew);
     Aig_ManConst1(p1)->pData = Aig_ManConst1(pNew);
@@ -85,7 +87,7 @@ Aig_Man_t * Saig_ManCreateMiter( Aig_Man_t * p0, Aig_Man_t * p1, int Oper )
         pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
     // cleanup
     Aig_ManSetRegNum( pNew, Saig_ManRegNum(p0) + Saig_ManRegNum(p1) );
-    Aig_ManCleanup( pNew );
+//    Aig_ManCleanup( pNew );
     return pNew;
 }
 
@@ -184,6 +186,9 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames )
                 Aig_ObjCreatePo( p, Aig_ObjChild0Copy(pObj) );
             break;
         }
+        // create POs for this frame
+        Saig_ManForEachPo( pAig, pObj, i )
+            Aig_ObjCreatePo( p, Aig_ObjChild0Copy(pObj) );
         // save register inputs
         Saig_ManForEachLi( pAig, pObj, i )
             pObj->pData = Aig_ObjChild0Copy(pObj);
@@ -213,7 +218,7 @@ Aig_Man_t * Saig_ManUnrollTwo( Aig_Man_t * pBot, Aig_Man_t * pTop, int nFrames )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Aig_ManDupNodes_old( Aig_Man_t * p, Vec_Ptr_t * vSet )
+Aig_Man_t * Aig_ManDupNodesAll( Aig_Man_t * p, Vec_Ptr_t * vSet )
 {
     Aig_Man_t * pNew, * pCopy;
     Aig_Obj_t * pObj;
@@ -250,7 +255,7 @@ Aig_Man_t * Aig_ManDupNodes_old( Aig_Man_t * p, Vec_Ptr_t * vSet )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Aig_ManDupNodes( Aig_Man_t * p, Vec_Ptr_t * vSet, int iPart )
+Aig_Man_t * Aig_ManDupNodesHalf( Aig_Man_t * p, Vec_Ptr_t * vSet, int iPart )
 {
     Aig_Man_t * pNew, * pCopy;
     Aig_Obj_t * pObj;
@@ -337,6 +342,79 @@ int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAi
             Vec_PtrFree( vSet1 );
             return 0;
         }
+        if ( Aig_ObjFaninC0(pObj) )
+            pObj0 = Aig_Not(pObj0);
+
+//        printf( "%d %d  ", Aig_Regular(pObj0)->Id, Aig_Regular(pObj1)->Id );
+        if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id )
+        {
+            Vec_PtrPush( vSet0, pObj0 );
+            Vec_PtrPush( vSet1, pObj1 );
+        }
+        else
+        {
+            Vec_PtrPush( vSet0, pObj1 );
+            Vec_PtrPush( vSet1, pObj0 );
+        }
+    }
+//    printf( "Miter has %d constant outputs.\n", Counter );
+//    printf( "\n" );
+    if ( ppAig0 )
+    {
+        *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 );
+        FREE( (*ppAig0)->pName );
+        (*ppAig0)->pName = Aig_UtilStrsav( "part0" );
+    }
+    if ( ppAig1 )
+    {
+        *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 );
+        FREE( (*ppAig1)->pName );
+        (*ppAig1)->pName = Aig_UtilStrsav( "part1" );
+    }
+    Vec_PtrFree( vSet0 );
+    Vec_PtrFree( vSet1 );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG to have constant-0 initial state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Saig_ManDemiterSimpleDiff( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
+{
+    Vec_Ptr_t * vSet0, * vSet1;
+    Aig_Obj_t * pObj, * pFanin, * pObj0, * pObj1;
+    int i, Counter = 0;
+    assert( Saig_ManRegNum(p) % 2 == 0 );
+    vSet0 = Vec_PtrAlloc( Saig_ManPoNum(p) );
+    vSet1 = Vec_PtrAlloc( Saig_ManPoNum(p) );
+    Saig_ManForEachPo( p, pObj, i )
+    {
+        pFanin = Aig_ObjFanin0(pObj);
+        if ( Aig_ObjIsConst1( pFanin ) )
+        {
+            if ( !Aig_ObjFaninC0(pObj) )
+                printf( "The output number %d of the miter is constant 1.\n", i );
+            Counter++;
+            continue;
+        }
+        if ( !Aig_ObjIsNode(pFanin) || !Aig_ObjRecognizeExor( pFanin, &pObj0, &pObj1 ) )
+        {
+            printf( "The miter cannot be demitered.\n" );
+            Vec_PtrFree( vSet0 );
+            Vec_PtrFree( vSet1 );
+            return 0;
+        }
+        if ( Aig_ObjFaninC0(pObj) )
+            pObj0 = Aig_Not(pObj0);
+
 //        printf( "%d %d  ", Aig_Regular(pObj0)->Id, Aig_Regular(pObj1)->Id );
         if ( Aig_Regular(pObj0)->Id < Aig_Regular(pObj1)->Id )
         {
@@ -353,13 +431,13 @@ int Saig_ManDemiterSimple( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAi
 //    printf( "\n" );
     if ( ppAig0 )
     {
-        *ppAig0 = Aig_ManDupNodes( p, vSet0, 0 );
+        *ppAig0 = Aig_ManDupNodesAll( p, vSet0 );
         FREE( (*ppAig0)->pName );
         (*ppAig0)->pName = Aig_UtilStrsav( "part0" );
     }
     if ( ppAig1 )
     {
-        *ppAig1 = Aig_ManDupNodes( p, vSet1, 1 );
+        *ppAig1 = Aig_ManDupNodesAll( p, vSet1 );
         FREE( (*ppAig1)->pName );
         (*ppAig1)->pName = Aig_UtilStrsav( "part1" );
     }
@@ -525,14 +603,14 @@ int Saig_ManDemiter( Aig_Man_t * p, Aig_Man_t ** ppAig0, Aig_Man_t ** ppAig1 )
     if ( ppAig0 )
     {
         assert( 0 );
-        *ppAig0 = Aig_ManDupNodes( p, vSet0, 0 ); // not ready
+        *ppAig0 = Aig_ManDupNodesHalf( p, vSet0, 0 ); // not ready
         FREE( (*ppAig0)->pName );
         (*ppAig0)->pName = Aig_UtilStrsav( "part0" );
     }
     if ( ppAig1 )
     {
         assert( 0 );
-        *ppAig1 = Aig_ManDupNodes( p, vSet1, 1 ); // not ready
+        *ppAig1 = Aig_ManDupNodesHalf( p, vSet1, 1 ); // not ready
         FREE( (*ppAig1)->pName );
         (*ppAig1)->pName = Aig_UtilStrsav( "part1" );
     }
@@ -566,6 +644,42 @@ Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFra
     return pMiter;
 }
 
+
+/**Function*************************************************************
+
+  Synopsis    [Resimulates counter-example and returns the failed output number.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ssw_SecCexResimulate( Aig_Man_t * p, int * pModel, int * pnOutputs )
+{
+    Aig_Obj_t * pObj;
+    int i, RetValue = -1;
+    *pnOutputs = 0;
+    Aig_ManConst1(p)->fMarkA = 1;
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->fMarkA = pModel[i];
+    Aig_ManForEachNode( p, pObj, i )
+        pObj->fMarkA = ( Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj) ) & 
+                      ( Aig_ObjFanin1(pObj)->fMarkA ^ Aig_ObjFaninC1(pObj) );
+    Aig_ManForEachPo( p, pObj, i )
+        pObj->fMarkA = Aig_ObjFanin0(pObj)->fMarkA ^ Aig_ObjFaninC0(pObj);
+    Aig_ManForEachPo( p, pObj, i )
+        if ( pObj->fMarkA )
+        {
+            if ( RetValue == -1 )
+                RetValue = i;
+            (*pnOutputs)++;
+        }
+    Aig_ManCleanMarkA(p);
+    return RetValue;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Reduces SEC to CEC for the special case of seq synthesis.]
@@ -578,12 +692,16 @@ Aig_Man_t * Saig_ManCreateMiterTwo( Aig_Man_t * pOld, Aig_Man_t * pNew, int nFra
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int fVerbose )
+int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int nFrames, int fVerbose )
 {
     extern int Fra_FraigCec( Aig_Man_t ** ppAig, int nConfLimit, int fVerbose );
-    int nFrames = 2;   // modify to enable comparison over any number of frames
+    int iOut, nOuts;
     Aig_Man_t * pMiterCec;
     int RetValue, clkTotal = clock();
+    Aig_ManPrintStats( pPart0 );
+    Aig_ManPrintStats( pPart1 );
+//    Aig_ManDumpBlif( pPart0, "file0.blif", NULL, NULL );
+//    Aig_ManDumpBlif( pPart1, "file1.blif", NULL, NULL );
 //    assert( Aig_ManNodeNum(pPart0) <= Aig_ManNodeNum(pPart1) );
     if ( Aig_ManNodeNum(pPart0) >= Aig_ManNodeNum(pPart1) )
     {
@@ -605,7 +723,6 @@ int Ssw_SecSpecial( Aig_Man_t * pPart0, Aig_Man_t * pPart1, int fVerbose )
     // transfer model if given
 //    if ( pNtk2 == NULL )
 //        pNtk1->pModel = pMiterCec->pData, pMiterCec->pData = NULL;
-    Aig_ManStop( pMiterCec );
     // report the miter
     if ( RetValue == 1 )
     {
@@ -616,6 +733,24 @@ PRT( "Time", clock() - clkTotal );
     {
         printf( "Networks are NOT EQUIVALENT.   " );
 PRT( "Time", clock() - clkTotal );
+        if ( pMiterCec->pData == NULL )
+            printf( "Counter-example is not available.\n" );
+        else
+        {
+            iOut = Ssw_SecCexResimulate( pMiterCec, pMiterCec->pData, &nOuts );
+            if ( iOut == -1 )
+                printf( "Counter-example verification has failed.\n" );
+            else 
+            {
+                if ( iOut < Saig_ManPoNum(pPart0) * nFrames )
+                    printf( "Primary output %d has failed in frame %d.\n", 
+                        iOut%Saig_ManPoNum(pPart0), iOut/Saig_ManPoNum(pPart0) );
+                else
+                    printf( "Flop input %d has failed in the last frame.\n", 
+                        iOut - Saig_ManPoNum(pPart0) * nFrames );
+                printf( "The counter-example detected %d incorrect POs or flop inputs.\n", nOuts );
+            }
+        }
     }
     else
     {
@@ -623,6 +758,7 @@ PRT( "Time", clock() - clkTotal );
 PRT( "Time", clock() - clkTotal );
     }
     fflush( stdout );
+    Aig_ManStop( pMiterCec );
     return RetValue;
 }
 
@@ -639,6 +775,7 @@ PRT( "Time", clock() - clkTotal );
 ***********************************************************************/
 int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose )
 {
+    int nFrames = 2;   // modify to enable comparison over any number of frames
     Aig_Man_t * pPart0, * pPart1;
     int RetValue;
     if ( fVerbose )
@@ -657,7 +794,7 @@ int Ssw_SecSpecialMiter( Aig_Man_t * pMiter, int fVerbose )
 //        Aig_ManDumpBlif( pPart1, "part1.blif", NULL, NULL );
 //        printf( "The result of demitering is written into files \"%s\" and \"%s\".\n", "part0.blif", "part1.blif" );
     }
-    RetValue = Ssw_SecSpecial( pPart0, pPart1, fVerbose );
+    RetValue = Ssw_SecSpecial( pPart0, pPart1, nFrames, fVerbose );
     Aig_ManStop( pPart0 );
     Aig_ManStop( pPart1 );
     return RetValue;
diff --git a/src/aig/saig/saigSynch.c b/src/aig/saig/saigSynch.c
index eb0fefc9..c52f2f48 100644
--- a/src/aig/saig/saigSynch.c
+++ b/src/aig/saig/saigSynch.c
@@ -632,6 +632,7 @@ Aig_Man_t * Saig_Synchronize( Aig_Man_t * pAig1, Aig_Man_t * pAig2, int nWords,
     pAig1z = Saig_ManDupInitZero( pAig1 );
     pAig2z = Saig_ManDupInitZero( pAig2 );
     pMiter = Saig_ManCreateMiter( pAig1z, pAig2z, 0 );
+    Aig_ManCleanup( pMiter );
     Aig_ManStop( pAig1z );
     Aig_ManStop( pAig2z );