Version abc70819

18 files changed, 607 insertions, 193 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index a1abd2b7..953d98ac 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -127,6 +127,7 @@ struct Aig_Man_t_
     int              nTravIds;       // the current traversal ID
     int              fCatchExor;     // enables EXOR nodes
     int              fAddStrash;     // performs additional strashing
+    Aig_Obj_t **     pObjCopies;     // mapping of AIG nodes into FRAIG nodes
     // timing statistics
     int              time1;
     int              time2;
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index d09bf41b..122daaa4 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -288,6 +288,7 @@ void Aig_ManStop( Aig_Man_t * p )
     if ( p->vBufs )    Vec_PtrFree( p->vBufs );
     if ( p->vLevelR )  Vec_IntFree( p->vLevelR );
     if ( p->vLevels )  Vec_VecFree( p->vLevels );
+    FREE( p->pObjCopies );
     FREE( p->pReprs );
     FREE( p->pEquivs );
     free( p->pTable );
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 2bb19a34..c8617d84 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -52,6 +52,7 @@ typedef struct Fra_Par_t_   Fra_Par_t;
 typedef struct Fra_Man_t_   Fra_Man_t;
 typedef struct Fra_Cla_t_   Fra_Cla_t;
 typedef struct Fra_Sml_t_   Fra_Sml_t;
+typedef struct Fra_Bmc_t_   Fra_Bmc_t;
 
 // FRAIG parameters
 struct Fra_Par_t_
@@ -70,6 +71,7 @@ struct Fra_Par_t_
     int              fConeBias;         // bias variables in the cone (good for unsat runs)
     int              nBTLimitNode;      // conflict limit at a node
     int              nBTLimitMiter;     // conflict limit at an output
+    int              nFramesP;          // the number of timeframes to in the prefix
     int              nFramesK;          // the number of timeframes to unroll
     int              fRewrite;          // use rewriting for constraint reduction
     int              fLatchCorr;        // computes latch correspondence only
@@ -91,15 +93,21 @@ struct Fra_Cla_t_
     int              nPairs;            // the number of pairs of nodes
     int              fRefinement;       // set to 1 when refinement has happened
     Vec_Int_t *      vImps;             // implications
+    // procedures used for class refinement
+    int (*pFuncNodeHash)     (Aig_Obj_t *, int);         // returns has key of the node
+    int (*pFuncNodeIsConst)  (Aig_Obj_t *);              // returns 1 if the node is a constant
+    int (*pFuncNodesAreEqual)(Aig_Obj_t *, Aig_Obj_t *); // returns 1 if nodes are equal up to a complement
 };
 
 // simulation manager
 struct Fra_Sml_t_
 {
     Aig_Man_t *      pAig;              // the original AIG manager
-    int              nFrames;           // the number of times frames
+    int              nPref;             // the number of times frames in the prefix
+    int              nFrames;           // the number of times frames 
     int              nWordsFrame;       // the number of words in each time frame
     int              nWordsTotal;       // the total number of words at a node
+    int              nWordsPref;        // the number of word in the prefix
     int              nSimRounds;        // statistics
     int              timeSim;           // statistics
     unsigned         pData[0];          // simulation data for the nodes
@@ -120,6 +128,8 @@ struct Fra_Man_t_
     Fra_Cla_t *      pCla;              // representation of (candidate) equivalent nodes
     // simulation info
     Fra_Sml_t *      pSml;              // simulation manager
+    // bounded model checking manager
+    Fra_Bmc_t *      pBmc;
     // counter example storage
     int              nPatWords;         // the number of words in the counter example
     unsigned *       pPatWords;         // the counter example
@@ -199,6 +209,11 @@ static inline Aig_Obj_t *  Fra_ObjChild1Fra( Aig_Obj_t * pObj, int i ) { assert(
 ////////////////////////////////////////////////////////////////////////
 
 /*=== fraClass.c ========================================================*/
+extern int                 Fra_BmcNodeIsConst( Aig_Obj_t * pObj );
+extern int                 Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
+extern void                Fra_BmcStop( Fra_Bmc_t * p );
+extern void                Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth );
+/*=== fraClass.c ========================================================*/
 extern Fra_Cla_t *         Fra_ClassesStart( Aig_Man_t * pAig );
 extern void                Fra_ClassesStop( Fra_Cla_t * p );
 extern void                Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed );
@@ -212,7 +227,7 @@ extern void                Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
 extern void                Fra_ClassesLatchCorr( Fra_Man_t * p );
 extern void                Fra_ClassesPostprocess( Fra_Cla_t * p );
 /*=== fraCnf.c ========================================================*/
-extern void                Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
+extern void                Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 /*=== fraCore.c ========================================================*/
 extern Aig_Man_t *         Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pPars );
 extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig );
@@ -225,7 +240,7 @@ extern int                 Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps
 extern int                 Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps );
 extern void                Fra_ImpCompactArray( Vec_Int_t * vImps );
 /*=== fraInd.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter );
+extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
 extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
@@ -242,16 +257,17 @@ extern int                 Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
 /*=== fraSec.c ========================================================*/
 extern int                 Fra_FraigSec( Aig_Man_t * p, int nFrames, int fVerbose, int fVeryVerbose );
 /*=== fraSim.c ========================================================*/
-extern int                 Fra_NodeHasZeroSim( Aig_Obj_t * pObj );
-extern int                 Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
-extern unsigned            Fra_NodeHashSims( Aig_Obj_t * pObj );
-extern int                 Fra_CheckOutputSims( Fra_Man_t * p );
-extern void                Fra_SavePattern( Fra_Man_t * p );
+extern int                 Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
+extern int                 Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
+extern int                 Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
+extern int                 Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right );
+extern int                 Fra_SmlCheckOutput( Fra_Man_t * p );
+extern void                Fra_SmlSavePattern( Fra_Man_t * p );
 extern void                Fra_SmlSimulate( Fra_Man_t * p, int fInit );
 extern void                Fra_SmlResimulate( Fra_Man_t * p );
-extern Fra_Sml_t *         Fra_SmlStart( Aig_Man_t * pAig, int nFrames, int nWordsFrame );
+extern Fra_Sml_t *         Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame );
 extern void                Fra_SmlStop( Fra_Sml_t * p );
-extern Fra_Sml_t *         Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nFrames, int nWords );
+extern Fra_Sml_t *         Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords );
 extern Fra_Sml_t *         Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
 
 
diff --git a/src/aig/fra/fraBmc.c b/src/aig/fra/fraBmc.c
new file mode 100644
index 00000000..45c162af
--- /dev/null
+++ b/src/aig/fra/fraBmc.c
@@ -0,0 +1,298 @@
+/**CFile****************************************************************
+
+  FileName    [fraBmc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [New FRAIG package.]
+
+  Synopsis    [Bounded model checking.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 30, 2007.]
+
+  Revision    [$Id: fraBmc.c,v 1.00 2007/06/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+// simulation manager
+struct Fra_Bmc_t_
+{
+    // parameters
+    int              nPref;             // the size of the prefix
+    int              nDepth;            // the depth of the frames
+    int              nFramesAll;        // the total number of timeframes
+    // AIG managers
+    Aig_Man_t *      pAig;              // the original AIG manager
+    Aig_Man_t *      pAigFrames;        // initialized timeframes
+    Aig_Man_t *      pAigFraig;         // the fraiged initialized timeframes
+    // mapping of nodes
+    Aig_Obj_t **     pObjToFrames;      // mapping of the original node into frames
+    Aig_Obj_t **     pObjToFraig;       // mapping of the frames node into fraig
+};
+
+static inline Aig_Obj_t *  Bmc_ObjFrames( Aig_Obj_t * pObj, int i )                       { return ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFrames[((Fra_Man_t *)pObj->pData)->pBmc->nFramesAll*pObj->Id + i];  }
+static inline void         Bmc_ObjSetFrames( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFrames[((Fra_Man_t *)pObj->pData)->pBmc->nFramesAll*pObj->Id + i] = pNode; }
+
+static inline Aig_Obj_t *  Bmc_ObjFraig( Aig_Obj_t * pObj )                               { return ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFraig[pObj->Id];  }
+static inline void         Bmc_ObjSetFraig( Aig_Obj_t * pObj, Aig_Obj_t * pNode )         { ((Fra_Man_t *)pObj->pData)->pBmc->pObjToFraig[pObj->Id] = pNode; }
+
+static inline Aig_Obj_t *  Bmc_ObjChild0Frames( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin0(pObj)? Aig_NotCond(Bmc_ObjFrames(Aig_ObjFanin0(pObj),i), Aig_ObjFaninC0(pObj)) : NULL;  }
+static inline Aig_Obj_t *  Bmc_ObjChild1Frames( Aig_Obj_t * pObj, int i ) { assert( !Aig_IsComplement(pObj) ); return Aig_ObjFanin1(pObj)? Aig_NotCond(Bmc_ObjFrames(Aig_ObjFanin1(pObj),i), Aig_ObjFaninC1(pObj)) : NULL;  }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the nodes are equivalent.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_BmcNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+{
+    Fra_Man_t * p = pObj0->pData;
+//    Aig_Obj_t ** ppNodes = p->pBmc->pObjToFraig;
+    Aig_Obj_t * pObjFrames0, * pObjFrames1;
+    Aig_Obj_t * pObjFraig0, * pObjFraig1;
+    int i;
+    for ( i = p->pBmc->nPref; i < p->pBmc->nFramesAll; i++ )
+    {
+        pObjFrames0 = Aig_Regular( Bmc_ObjFrames(pObj0, i) );
+        pObjFrames1 = Aig_Regular( Bmc_ObjFrames(pObj1, i) );
+        if ( pObjFrames0 == pObjFrames1 )
+            continue;
+        pObjFraig0 = Aig_Regular( Bmc_ObjFraig(pObjFrames0) );
+        pObjFraig1 = Aig_Regular( Bmc_ObjFraig(pObjFrames1) );
+        if ( pObjFraig0 != pObjFraig1 )
+            return 0;
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the node is costant.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_BmcNodeIsConst( Aig_Obj_t * pObj )
+{
+    Fra_Man_t * p = pObj->pData;
+    return Fra_BmcNodesAreEqual( pObj, Aig_ManConst1(p->pManAig) );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the BMC manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Fra_Bmc_t * Fra_BmcStart( Aig_Man_t * pAig, int nPref, int nDepth )
+{
+    Fra_Bmc_t * p;
+    p = ALLOC( Fra_Bmc_t, 1 );
+    memset( p, 0, sizeof(Fra_Bmc_t) );
+    p->pAig = pAig;
+    p->nPref = nPref;
+    p->nDepth = nDepth;
+    p->nFramesAll = nPref + nDepth;
+    p->pObjToFrames  = ALLOC( Aig_Obj_t *, p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
+    memset( p->pObjToFrames, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
+//    p->pObjToFraig  = ALLOC( Aig_Obj_t *, p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
+//    memset( p->pObjToFraig, 0, sizeof(Aig_Obj_t *) * p->nFramesAll * (Aig_ManObjIdMax(pAig) + 1) );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the BMC manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_BmcStop( Fra_Bmc_t * p )
+{
+    Aig_ManStop( p->pAigFrames );
+    Aig_ManStop( p->pAigFraig );
+    free( p->pObjToFrames );
+    free( p->pObjToFraig );
+    free( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs initialized timeframes of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Fra_BmcFrames( Fra_Bmc_t * p )
+{
+    Aig_Man_t * pAigFrames;
+    Aig_Obj_t * pObj, * pObjNew;
+    Aig_Obj_t ** pLatches;
+    int i, k, f;
+
+    // start the fraig package
+    pAigFrames = Aig_ManStart( (Aig_ManObjIdMax(p->pAig) + 1) * p->nFramesAll );
+    // create PI nodes for the frames
+    for ( f = 0; f < p->nFramesAll; f++ )
+        Bmc_ObjSetFrames( Aig_ManConst1(p->pAig), f, Aig_ManConst1(pAigFrames) );
+    for ( f = 0; f < p->nFramesAll; f++ )
+        Aig_ManForEachPiSeq( p->pAig, pObj, i )
+            Bmc_ObjSetFrames( pObj, f, Aig_ObjCreatePi(pAigFrames) );
+    // set initial state for the latches
+    Aig_ManForEachLoSeq( p->pAig, pObj, i )
+        Bmc_ObjSetFrames( pObj, 0, Aig_ManConst0(pAigFrames) );
+
+    // add timeframes
+    pLatches = ALLOC( Aig_Obj_t *, Aig_ManRegNum(p->pAig) );
+    for ( f = 0; f < p->nFramesAll; f++ )
+    {
+        // add internal nodes of this frame
+        Aig_ManForEachNode( p->pAig, pObj, i )
+        {
+            pObjNew = Aig_And( pAigFrames, Bmc_ObjChild0Frames(pObj,f), Bmc_ObjChild1Frames(pObj,f) );
+            Bmc_ObjSetFrames( pObj, f, pObjNew );
+        }
+        if ( f == p->nFramesAll - 1 )
+            break;
+        // save the latch input values
+        k = 0;
+        Aig_ManForEachLiSeq( p->pAig, pObj, i )
+            pLatches[k++] = Bmc_ObjChild0Frames(pObj,f);
+        assert( k == Aig_ManRegNum(p->pAig) );
+        // insert them to the latch output values
+        k = 0;
+        Aig_ManForEachLoSeq( p->pAig, pObj, i )
+            Bmc_ObjSetFrames( pObj, f+1, pLatches[k++] );
+        assert( k == Aig_ManRegNum(p->pAig) );
+    }
+    free( pLatches );
+    // add POs to all the dangling nodes
+    Aig_ManForEachObj( pAigFrames, pObjNew, i )
+        if ( Aig_ObjIsNode(pObjNew) && pObjNew->nRefs == 0 )
+            Aig_ObjCreatePo( pAigFrames, pObjNew );
+
+    // return the new manager
+    return pAigFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Constructs FRAIG manager for the initialized timeframes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Fra_BmcFraig( Fra_Bmc_t * p )
+{
+    Aig_Man_t * pFraig;
+    Fra_Par_t Pars, * pPars = &Pars; 
+    Fra_ParamsDefault( pPars );
+    pPars->nBTLimitNode = 100000;
+    pPars->fVerbose     = 0;
+    pPars->fProve       = 0;
+    pPars->fDoSparse    = 1;
+    pPars->fSpeculate   = 0;
+    pPars->fChoicing    = 0;
+    pFraig = Fra_FraigPerform( p->pAigFrames, pPars );
+    p->pObjToFraig = p->pAigFrames->pObjCopies;
+    p->pAigFrames->pObjCopies = NULL;
+    return pFraig;
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Performs BMC for the given AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_BmcPerform( Fra_Man_t * p, int nPref, int nDepth )
+{
+    Aig_Obj_t * pObj;
+    int i, clk = clock();
+    assert( p->pBmc == NULL );
+    // derive and fraig the frames
+    p->pBmc = Fra_BmcStart( p->pManAig, nPref, nDepth );
+    p->pBmc->pAigFrames = Fra_BmcFrames( p->pBmc );
+    p->pBmc->pAigFraig = Fra_BmcFraig( p->pBmc );
+    // annotate frames nodes with pointers to the manager
+    Aig_ManForEachObj( p->pBmc->pAigFrames, pObj, i )
+        pObj->pData = p;
+    // report the results
+    if ( p->pPars->fVerbose )
+    {
+        printf( "Original AIG = %d. Init %d frames = %d. Fraig = %d.  ", 
+            Aig_ManNodeNum(p->pBmc->pAig), p->pBmc->nFramesAll, 
+            Aig_ManNodeNum(p->pBmc->pAigFrames), Aig_ManNodeNum(p->pBmc->pAigFraig) );
+        PRT( "Time", clock() - clk );
+        printf( "Before BMC: " );  Fra_ClassesPrint( p->pCla, 0 );
+    }
+    // refine the classes
+    p->pCla->pFuncNodeIsConst   = Fra_BmcNodeIsConst;
+    p->pCla->pFuncNodesAreEqual = Fra_BmcNodesAreEqual;
+    Fra_ClassesRefine( p->pCla );
+    Fra_ClassesRefine1( p->pCla );
+    p->pCla->pFuncNodeIsConst   = Fra_SmlNodeIsConst;
+    p->pCla->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
+    // report the results
+    if ( p->pPars->fVerbose )
+    {
+        printf( "After  BMC: " );  Fra_ClassesPrint( p->pCla, 0 );
+    }
+    // free the BMC manager
+    Fra_BmcStop( p->pBmc );  
+    p->pBmc = NULL;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/fra/fraClass.c b/src/aig/fra/fraClass.c
index 9c10ae3b..a9d727da 100644
--- a/src/aig/fra/fraClass.c
+++ b/src/aig/fra/fraClass.c
@@ -67,6 +67,9 @@ Fra_Cla_t * Fra_ClassesStart( Aig_Man_t * pAig )
     p->vClassesTemp = Vec_PtrAlloc( 100 );
     p->vClassOld    = Vec_PtrAlloc( 100 );
     p->vClassNew    = Vec_PtrAlloc( 100 );
+    p->pFuncNodeHash      = Fra_SmlNodeHash;
+    p->pFuncNodeIsConst   = Fra_SmlNodeIsConst;
+    p->pFuncNodesAreEqual = Fra_SmlNodesAreEqual;
     return p;
 }
 
@@ -127,27 +130,6 @@ void Fra_ClassesCopyReprs( Fra_Cla_t * p, Vec_Ptr_t * vFailed )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_PrintClass( Aig_Obj_t ** pClass )
-{
-    Aig_Obj_t * pTemp;
-    int i;
-    printf( "{ " );
-    for ( i = 0; pTemp = pClass[i]; i++ )
-        printf( "%d ", pTemp->Id );
-    printf( "}\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints simulation classes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
 int Fra_ClassCount( Aig_Obj_t ** pClass )
 {
     Aig_Obj_t * pTemp;
@@ -216,17 +198,42 @@ int Fra_ClassesCountPairs( Fra_Cla_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Fra_PrintClass( Aig_Obj_t ** pClass )
+{
+    Aig_Obj_t * pTemp;
+    int i;
+    for ( i = 1; pTemp = pClass[i]; i++ )
+        assert( Fra_ClassObjRepr(pTemp) == pClass[0] );
+    printf( "{ " );
+    for ( i = 0; pTemp = pClass[i]; i++ )
+        printf( "%d ", pTemp->Id, Fra_ClassObjRepr(pTemp)? Fra_ClassObjRepr(pTemp)->Id : -1 );
+    printf( "}\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints simulation classes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Fra_ClassesPrint( Fra_Cla_t * p, int fVeryVerbose )
 {
     Aig_Obj_t ** pClass;
     Aig_Obj_t * pObj;
     int i;
 
-    printf( "Consts = %6d. Classes = %6d. Literals = %6d.\n", 
+    printf( "Const = %5d. Class = %5d. Lit = %5d.\n", 
         Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses), Fra_ClassesCountLits(p) );
 
     if ( fVeryVerbose )
     {
+        Vec_PtrForEachEntry( p->vClasses1, pObj, i )
+            assert( Fra_ClassObjRepr(pObj) == Aig_ManConst1(p->pAig) );
         printf( "Constants { " );
         Vec_PtrForEachEntry( p->vClasses1, pObj, i )
             printf( "%d ", pObj->Id );
@@ -281,9 +288,9 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
 //Extra_PrintBinary( stdout, Fra_ObjSim(pObj), 32 );
 //printf( "\n" );
         // hash the node by its simulation info
-        iEntry = Fra_NodeHashSims( pObj ) % nTableSize;
+        iEntry = p->pFuncNodeHash( pObj, nTableSize );
         // check if the node belongs to the class of constant 1
-        if ( iEntry == 0 && Fra_NodeHasZeroSim( pObj ) )
+        if ( p->pFuncNodeIsConst( pObj ) )
         {
             Vec_PtrPush( p->vClasses1, pObj );
             Fra_ClassObjSetRepr( pObj, Aig_ManConst1(p->pAig) );
@@ -351,7 +358,6 @@ void Fra_ClassesPrepare( Fra_Cla_t * p, int fLatchCorr )
             Fra_ClassObjSetRepr( pTemp, pObj );
         }
         // add as many empty entries
-//        memset( p->pMemClasses + 2*nEntries + nNodes, 0, sizeof(Aig_Obj_t *) * nNodes );
         p->pMemClasses[2*nEntries + nNodes] = NULL;
         // increment the number of entries
         nEntries += k;
@@ -381,7 +387,7 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Cla_t * p, Aig_Obj_t ** ppClass )
 
     // check if the class is going to be refined
     for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )        
-        if ( !Fra_NodeCompareSims(ppClass[0], pObj) )
+        if ( !p->pFuncNodesAreEqual(ppClass[0], pObj) )
             break;
     if ( pObj == NULL )
         return NULL;
@@ -390,7 +396,7 @@ Aig_Obj_t ** Fra_RefineClassOne( Fra_Cla_t * p, Aig_Obj_t ** ppClass )
     Vec_PtrClear( p->vClassNew );
     Vec_PtrPush( p->vClassOld, ppClass[0] );
     for ( ppThis = ppClass + 1; pObj = *ppThis; ppThis++ )        
-        if ( Fra_NodeCompareSims(ppClass[0], pObj) )
+        if ( p->pFuncNodesAreEqual(ppClass[0], pObj) )
             Vec_PtrPush( p->vClassOld, pObj );
         else
             Vec_PtrPush( p->vClassNew, pObj );
@@ -517,7 +523,7 @@ int Fra_ClassesRefine1( Fra_Cla_t * p )
     Vec_PtrClear( p->vClassNew );
     Vec_PtrForEachEntry( p->vClasses1, pObj, i )
     {
-        if ( Fra_NodeHasZeroSim( pObj ) )
+        if ( p->pFuncNodeIsConst( pObj ) )
             Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
         else 
             Vec_PtrPush( p->vClassNew, pObj );
@@ -526,6 +532,12 @@ int Fra_ClassesRefine1( Fra_Cla_t * p )
     if ( Vec_PtrSize(p->vClassNew) == 0 )
         return 0;
     p->fRefinement = 1;
+/*
+    printf( "Refined const-1 class: {" );
+    Vec_PtrForEachEntry( p->vClassNew, pObj, i )
+        printf( " %d", pObj->Id );
+    printf( " }\n" );
+*/
     if ( Vec_PtrSize(p->vClassNew) == 1 )
     {
         Fra_ClassObjSetRepr( Vec_PtrEntry(p->vClassNew,0), NULL );
@@ -600,28 +612,6 @@ void Fra_ClassesLatchCorr( Fra_Man_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Counts the number of 1s in the XOR of simulation data.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-static inline int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right )
-{
-    unsigned * pSimL, * pSimR;
-    int k, Counter = 0;
-    pSimL = Fra_ObjSim( p, Left );
-    pSimR = Fra_ObjSim( p, Right );
-    for ( k = 0; k < p->nWordsTotal; k++ )
-        Counter += Aig_WordCountOnes( pSimL[k] ^ pSimR[k] );
-    return Counter;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Postprocesses the classes by removing half of the less useful.]
 
   Description []
@@ -685,6 +675,22 @@ void Fra_ClassesPostprocess( Fra_Cla_t * p )
     free( pWeights );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Derives AIG for the partitioned problem.]
+
+  Description []
+               
+  SideEffects [] 
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Fra_ClassesDeriveAig( Fra_Cla_t * p, int nFramesK )
+{
+
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/fra/fraCnf.c b/src/aig/fra/fraCnf.c
index 7df55d93..d56c0254 100644
--- a/src/aig/fra/fraCnf.c
+++ b/src/aig/fra/fraCnf.c
@@ -234,7 +234,7 @@ void Fra_ObjAddToFrontier( Fra_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vFrontie
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
+void Fra_CnfNodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
 { 
     Vec_Ptr_t * vFrontier, * vFanins;
     Aig_Obj_t * pNode, * pFanin;
diff --git a/src/aig/fra/fraCore.c b/src/aig/fra/fraCore.c
index f28793aa..3c76af03 100644
--- a/src/aig/fra/fraCore.c
+++ b/src/aig/fra/fraCore.c
@@ -181,8 +181,38 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
         Vec_PtrPush( p->vTimeouts, pObj );
     // simulate the counter-example and return the Fraig node
     Fra_SmlResimulate( p );
+/*
+printf( "%d -> %d.\n", pObj->Id, pObjRepr->Id );
+Fra_ClassesPrint( p->pCla, 1 );
+printf( "%3d : ", 19 );
+Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 19), 32 * p->pSml->nWordsTotal );
+printf( "\n" );
+printf( "%3d : ", 27 );
+Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 27), 32 * p->pSml->nWordsTotal );
+printf( "\n" );
+printf( "%3d : ", 30 );
+Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, 30), 32 * p->pSml->nWordsTotal );
+printf( "\n" );
+printf( "\n\n" );
+*/
     if ( Fra_ClassObjRepr(pObj) == pObjRepr )
+    {
+/*
+//Fra_ClassesPrint( p->pCla, 1 );
+//printf( "\n\n" );
+printf( "%3d : ", pObj->Id );
+Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, pObj->Id), 32 * p->pSml->nWordsTotal );
+printf( "\n" );
+printf( "%3d : ", pObjRepr->Id );
+Extra_PrintBinary( stdout, Fra_ObjSim(p->pSml, pObjRepr->Id), 32 * p->pSml->nWordsTotal );
+printf( "\n" );
+*/
+        if ( Aig_ObjIsPi(pObj) )
+            printf( "primary input\n" );
+        else
+            printf( "NOT primary input\n" );
         printf( "Fra_FraigNode(): Error in class refinement!\n" );
+    }
     assert( Fra_ClassObjRepr(pObj) != pObjRepr );
 }
 
@@ -261,7 +291,7 @@ clk = clock();
     assert( Aig_ManLatchNum(pManAig) == 0 );
     p = Fra_ManStart( pManAig, pPars );
     p->pManFraig = Fra_ManPrepareComb( p );
-    p->pSml = Fra_SmlStart( pManAig, 1, pPars->nSimWords );
+    p->pSml = Fra_SmlStart( pManAig, 0, 1, pPars->nSimWords );
     Fra_SmlSimulate( p, 0 );
     if ( p->pPars->fChoicing )
         Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 );
diff --git a/src/aig/fra/fraImp.c b/src/aig/fra/fraImp.c
index d5761fbe..25b34e03 100644
--- a/src/aig/fra/fraImp.c
+++ b/src/aig/fra/fraImp.c
@@ -53,7 +53,7 @@ static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
     Aig_ManForEachObj( p->pAig, pObj, i )
     {
         pSim = Fra_ObjSim( p, i );
-        for ( k = 0; k < p->nWordsTotal; k++ )
+        for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
             pnBits[i] += Aig_WordCountOnes( pSim[k] );
     }
     return pnBits;
@@ -61,7 +61,7 @@ static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Counts the number of 1s in the reverse implication.]
+  Synopsis    [Returns 1 if implications holds.]
 
   Description []
                
@@ -70,20 +70,21 @@ static inline int * Fra_SmlCountOnes( Fra_Sml_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
+static inline int Sml_NodeCheckImp( Fra_Sml_t * p, int Left, int Right )
 {
     unsigned * pSimL, * pSimR;
-    int k, Counter = 0;
+    int k;
     pSimL = Fra_ObjSim( p, Left );
     pSimR = Fra_ObjSim( p, Right );
-    for ( k = 0; k < p->nWordsTotal; k++ )
-        Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] );
-    return Counter;
+    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
+        if ( pSimL[k] & ~pSimR[k] )
+            return 0;
+    return 1;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Returns 1 if implications holds.]
+  Synopsis    [Counts the number of 1s in the reverse implication.]
 
   Description []
                
@@ -92,16 +93,15 @@ static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
   SeeAlso     []
 
 ***********************************************************************/
-static inline int Sml_NodeCheckImp( Fra_Sml_t * p, int Left, int Right )
+static inline int Sml_NodeNotImpWeight( Fra_Sml_t * p, int Left, int Right )
 {
     unsigned * pSimL, * pSimR;
-    int k;
+    int k, Counter = 0;
     pSimL = Fra_ObjSim( p, Left );
     pSimR = Fra_ObjSim( p, Right );
-    for ( k = 0; k < p->nWordsTotal; k++ )
-        if ( pSimL[k] & ~pSimR[k] )
-            return 0;
-    return 1;
+    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
+        Counter += Aig_WordCountOnes( pSimL[k] & ~pSimR[k] );
+    return Counter;
 }
 
 /**Function*************************************************************
@@ -294,7 +294,7 @@ Vec_Int_t * Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, in
     assert( nImpMaxLimit > 0 && nImpUseLimit > 0 && nImpUseLimit <= nImpMaxLimit );
     // normalize both managers
     pComb = Fra_SmlSimulateComb( p->pManAig, nSimWords );
-    pSeq = Fra_SmlSimulateSeq( p->pManAig, nSimWords, 1 );
+    pSeq = Fra_SmlSimulateSeq( p->pManAig, p->pPars->nFramesP, nSimWords, 1 );
     // get the nodes sorted by the number of 1s
     vNodes = Fra_SmlSortUsingOnes( pSeq, fLatchCorr );
 /*
@@ -334,7 +334,7 @@ Aig_ManForEachObj( p->pManAig, pObj, i )
                     continue;
                 }
 //                printf( "d=%d c=%d  ", k-i, Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK) );
-
+ 
                 nImpsCollected++;
                 Imp = Sml_ImpCreate( *pNodesI, *pNodesK );
                 pImpCosts[ Vec_IntSize(vImps) ] = Sml_NodeNotImpWeight(pComb, *pNodesI, *pNodesK);
diff --git a/src/aig/fra/fraInd.c b/src/aig/fra/fraInd.c
index 76cadd0f..d754f3ae 100644
--- a/src/aig/fra/fraInd.c
+++ b/src/aig/fra/fraInd.c
@@ -198,8 +198,16 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter )
 {
+    int fUseSimpleCnf = 0;
+    int fUseOldSimulation = 0;
+    // other paramaters affecting performance
+    // - presence of FRAIGing in Abc_NtkDarSeqSweep()
+    // - using distance-1 patterns in Fra_SmlAssignDist1()
+    // - the number of simulation patterns
+    // - the number of BMC frames
+
     Fra_Man_t * p;
     Fra_Par_t Pars, * pPars = &Pars; 
     Aig_Obj_t * pObj;
@@ -207,7 +215,6 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
     Aig_Man_t * pManAigNew;
 //    Vec_Int_t * vImps;
     int nIter, i, clk = clock(), clk2;
-
     if ( Aig_ManNodeNum(pManAig) == 0 )
     {
         if ( pnIter ) *pnIter = 0;
@@ -220,6 +227,7 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
 
     // get parameters
     Fra_ParamsDefaultSeq( pPars );
+    pPars->nFramesP   = nFramesP;
     pPars->nFramesK   = nFramesK;
     pPars->fVerbose   = fVerbose;
     pPars->fRewrite   = fRewrite;
@@ -229,17 +237,31 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
     // start the fraig manager for this run
     p = Fra_ManStart( pManAig, pPars );
     // derive and refine e-classes using K initialized frames
-//    p->pSml = Fra_SmlStart( pManAig, pPars->nFramesK + 1, pPars->nSimWords );
-//    Fra_SmlSimulate( p, 1 );
-
-    // remember that strange bug: r iscas/blif/s5378.blif    ; st; ssw -F 4; sec -F 10
-    // refine the classes with more simulation rounds
-    p->pSml = Fra_SmlSimulateSeq( pManAig, 32, 2 );  
-    Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
-//    Fra_ClassesPostprocess( p->pCla );
-    // allocate new simulation manager for simulating counter-examples
-    Fra_SmlStop( p->pSml );
-    p->pSml = Fra_SmlStart( pManAig, pPars->nFramesK + 1, pPars->nSimWords );
+    if ( fUseOldSimulation )
+    {
+        if ( pPars->nFramesP > 0 )
+        {
+            pPars->nFramesP = 0;
+            printf( "Fra_FraigInduction(): Prefix cannot be used.\n" );
+        }
+        p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
+        Fra_SmlSimulate( p, 1 );
+    }
+    else
+    {
+        // bug:  r iscas/blif/s1238.blif    ; st; ssw -v
+        // refine the classes with more simulation rounds
+        p->pSml = Fra_SmlSimulateSeq( pManAig, pPars->nFramesP, 32, 2 ); //pPars->nFramesK + 1, 6 );  // 32, 2 );
+        Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
+//        Fra_ClassesPostprocess( p->pCla );
+        // allocate new simulation manager for simulating counter-examples
+        Fra_SmlStop( p->pSml );
+        p->pSml = Fra_SmlStart( pManAig, 0, pPars->nFramesK + 1, pPars->nSimWords );
+    }
+
+    // perform BMC
+    Fra_BmcPerform( p, pPars->nFramesP, pPars->nFramesK + 1 );
+//Fra_ClassesPrint( p->pCla, 1 );
 
     // select the most expressive implications
     if ( pPars->fUseImps )
@@ -264,9 +286,8 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
         if ( p->pPars->fRewrite )
             Fra_FraigInductionRewrite( p );
 
-        // bug:  r iscas/blif/s1238.blif    ; st; ssw -v
         // convert the manager to SAT solver (the last nLatches outputs are inputs)
-        if ( pPars->fUseImps )
+        if ( fUseSimpleCnf || pPars->fUseImps )
             pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
         else
             pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
@@ -289,32 +310,24 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
             pObj->pData = p;
 
         // transfer PI/LO variable numbers
-        pObj = Aig_ManConst1( p->pManFraig );
-        Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
-        Aig_ManForEachPi( p->pManFraig, pObj, i )
-            Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
-        // transfer LI variable numbers
-        Aig_ManForEachLiSeq( p->pManFraig, pObj, i )
-        {
-            Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
-            Fra_ObjSetFaninVec( pObj, (void *)1 );
-        }
-        Cnf_DataFree( pCnf );
-/* 
         Aig_ManForEachObj( p->pManFraig, pObj, i )
         {
+            if ( pCnf->pVarNums[pObj->Id] == -1 )
+                continue;
             Fra_ObjSetSatNum( pObj, pCnf->pVarNums[pObj->Id] );
             Fra_ObjSetFaninVec( pObj, (void *)1 );
         }
         Cnf_DataFree( pCnf );
-*/
+
         // report the intermediate results
         if ( fVerbose )
         {
-            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  I = %6d. NR = %6d.\n", 
+            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  %s = %6d. NR = %6d.\n", 
                 nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
                 Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts,
-                p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0, Aig_ManNodeNum(p->pManFraig) );
+                p->pCla->vImps? "I" : "N", 
+                p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : Aig_ManNodeNum(p->pManAig), 
+                Aig_ManNodeNum(p->pManFraig) );
         }
 
         // perform sweeping
diff --git a/src/aig/fra/fraMan.c b/src/aig/fra/fraMan.c
index 84621d60..2b8e0a68 100644
--- a/src/aig/fra/fraMan.c
+++ b/src/aig/fra/fraMan.c
@@ -111,7 +111,7 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
     p->nSizeAlloc = Aig_ManObjIdMax( pManAig ) + 1;
     p->nFramesAll = pPars->nFramesK + 1;
     // allocate storage for sim pattern
-    p->nPatWords  = Aig_BitWordNum( Aig_ManPiNum(pManAig) * p->nFramesAll );
+    p->nPatWords  = Aig_BitWordNum( (Aig_ManPiNum(pManAig) - Aig_ManRegNum(pManAig)) * p->nFramesAll + Aig_ManRegNum(pManAig) );
     p->pPatWords  = ALLOC( unsigned, p->nPatWords ); 
     p->vPiVars    = Vec_PtrAlloc( 100 );
     // equivalence classes
@@ -232,6 +232,14 @@ void Fra_ManStop( Fra_Man_t * p )
     int i;
     if ( p->pPars->fVerbose )
         Fra_ManPrint( p );
+    // save mapping from original nodes into FRAIG nodes
+    if ( p->pManAig )
+    {
+        if ( p->pManAig->pObjCopies )
+            free( p->pManAig->pObjCopies );
+        p->pManAig->pObjCopies = p->pMemFraig;
+        p->pMemFraig = NULL;
+    }
     for ( i = 0; i < p->nSizeAlloc; i++ )
         if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 )
             Vec_PtrFree( p->pMemFanins[i] );
diff --git a/src/aig/fra/fraSat.c b/src/aig/fra/fraSat.c
index 417163d5..bc8ef08a 100644
--- a/src/aig/fra/fraSat.c
+++ b/src/aig/fra/fraSat.c
@@ -77,7 +77,7 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     }
 
     // if the nodes do not have SAT variables, allocate them
-    Fra_NodeAddToSolver( p, pOld, pNew );
+    Fra_CnfNodeAddToSolver( p, pOld, pNew );
 
     if ( p->pSat->qtail != p->pSat->qhead )
     {
@@ -113,7 +113,7 @@ p->timeSatUnsat += clock() - clk;
     else if ( RetValue1 == l_True )
     {
 p->timeSatSat += clock() - clk;
-        Fra_SavePattern( p );
+        Fra_SmlSavePattern( p );
         p->nSatCallsSat++;
         return 0;
     }
@@ -156,7 +156,7 @@ p->timeSatUnsat += clock() - clk;
     else if ( RetValue1 == l_True )
     {
 p->timeSatSat += clock() - clk;
-        Fra_SavePattern( p );
+        Fra_SmlSavePattern( p );
         p->nSatCallsSat++;
         return 0;
     }
@@ -234,7 +234,7 @@ int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fCom
     }
 
     // if the nodes do not have SAT variables, allocate them
-    Fra_NodeAddToSolver( p, pOld, pNew );
+    Fra_CnfNodeAddToSolver( p, pOld, pNew );
 
     if ( p->pSat->qtail != p->pSat->qhead )
     {
@@ -272,7 +272,7 @@ p->timeSatUnsat += clock() - clk;
     else if ( RetValue1 == l_True )
     {
 p->timeSatSat += clock() - clk;
-        Fra_SavePattern( p );
+        Fra_SmlSavePattern( p );
         p->nSatCallsSat++;
         return 0;
     }
@@ -320,7 +320,7 @@ int Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew )
     }
 
     // if the nodes do not have SAT variables, allocate them
-    Fra_NodeAddToSolver( p, NULL, pNew );
+    Fra_CnfNodeAddToSolver( p, NULL, pNew );
 
     // prepare variable activity
     if ( p->pPars->fConeBias )
@@ -346,7 +346,7 @@ p->timeSatUnsat += clock() - clk;
     {
 p->timeSatSat += clock() - clk;
         if ( p->pPatWords )
-            Fra_SavePattern( p );
+            Fra_SmlSavePattern( p );
         p->nSatCallsSat++;
         return 0;
     }
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 814fe59e..2a0d06b5 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -47,7 +47,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
     {
         nFrames = nFramesFix;
         // perform seq sweeping for one frame number
-        pNew = Fra_FraigInduction( p, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
+        pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
     }
     else
     {
@@ -55,7 +55,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
         for ( nFrames = 1; ; nFrames++ )
         {
 clk = clock();
-            pNew = Fra_FraigInduction( p, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
+            pNew = Fra_FraigInduction( p, 0, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
             RetValue = Fra_FraigMiterStatus( pNew );
             if ( fVerbose )
             {
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index a0929f99..b31fcb7f 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -30,6 +30,46 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Computes hash value of the node using its simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize )
+{
+    Fra_Man_t * p = pObj->pData;
+    static int s_FPrimes[128] = { 
+        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
+        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
+        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
+        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
+        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
+        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
+        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
+        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
+        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
+        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
+        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
+        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
+        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
+    };
+    unsigned * pSims;
+    unsigned uHash;
+    int i;
+//    assert( p->pSml->nWordsTotal <= 128 );
+    uHash = 0;
+    pSims = Fra_ObjSim(p->pSml, pObj->Id);
+    for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
+        uHash ^= pSims[i] * s_FPrimes[i & 0x7F];
+    return uHash % nTableSize;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if simulation info is composed of all zeros.]
 
   Description []
@@ -39,13 +79,13 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_NodeHasZeroSim( Aig_Obj_t * pObj )
+int Fra_SmlNodeIsConst( Aig_Obj_t * pObj )
 {
     Fra_Man_t * p = pObj->pData;
     unsigned * pSims;
     int i;
     pSims = Fra_ObjSim(p->pSml, pObj->Id);
-    for ( i = 0; i < p->pSml->nWordsTotal; i++ )
+    for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
         if ( pSims[i] )
             return 0;
     return 1;
@@ -62,14 +102,14 @@ int Fra_NodeHasZeroSim( Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
+int Fra_SmlNodesAreEqual( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
 {
     Fra_Man_t * p = pObj0->pData;
     unsigned * pSims0, * pSims1;
     int i;
     pSims0 = Fra_ObjSim(p->pSml, pObj0->Id);
     pSims1 = Fra_ObjSim(p->pSml, pObj1->Id);
-    for ( i = 0; i < p->pSml->nWordsTotal; i++ )
+    for ( i = p->pSml->nWordsPref; i < p->pSml->nWordsTotal; i++ )
         if ( pSims0[i] != pSims1[i] )
             return 0;
     return 1;
@@ -77,7 +117,7 @@ int Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
 
 /**Function*************************************************************
 
-  Synopsis    [Computes hash value of the node using its simulation info.]
+  Synopsis    [Counts the number of 1s in the XOR of simulation data.]
 
   Description []
                
@@ -86,39 +126,19 @@ int Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 )
   SeeAlso     []
 
 ***********************************************************************/
-unsigned Fra_NodeHashSims( Aig_Obj_t * pObj )
+int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right )
 {
-    Fra_Man_t * p = pObj->pData;
-    static int s_FPrimes[128] = { 
-        1009, 1049, 1093, 1151, 1201, 1249, 1297, 1361, 1427, 1459, 
-        1499, 1559, 1607, 1657, 1709, 1759, 1823, 1877, 1933, 1997, 
-        2039, 2089, 2141, 2213, 2269, 2311, 2371, 2411, 2467, 2543, 
-        2609, 2663, 2699, 2741, 2797, 2851, 2909, 2969, 3037, 3089, 
-        3169, 3221, 3299, 3331, 3389, 3461, 3517, 3557, 3613, 3671, 
-        3719, 3779, 3847, 3907, 3943, 4013, 4073, 4129, 4201, 4243, 
-        4289, 4363, 4441, 4493, 4549, 4621, 4663, 4729, 4793, 4871, 
-        4933, 4973, 5021, 5087, 5153, 5227, 5281, 5351, 5417, 5471, 
-        5519, 5573, 5651, 5693, 5749, 5821, 5861, 5923, 6011, 6073, 
-        6131, 6199, 6257, 6301, 6353, 6397, 6481, 6563, 6619, 6689, 
-        6737, 6803, 6863, 6917, 6977, 7027, 7109, 7187, 7237, 7309, 
-        7393, 7477, 7523, 7561, 7607, 7681, 7727, 7817, 7877, 7933, 
-        8011, 8039, 8059, 8081, 8093, 8111, 8123, 8147
-    };
-    unsigned * pSims;
-    unsigned uHash;
-    int i;
-    assert( p->pSml->nWordsTotal <= 128 );
-    uHash = 0;
-    pSims = Fra_ObjSim(p->pSml, pObj->Id);
-    for ( i = 0; i < p->pSml->nWordsTotal; i++ )
-        uHash ^= pSims[i] * s_FPrimes[i];
-    return uHash;
+    unsigned * pSimL, * pSimR;
+    int k, Counter = 0;
+    pSimL = Fra_ObjSim( p, Left );
+    pSimR = Fra_ObjSim( p, Right );
+    for ( k = p->nWordsPref; k < p->nWordsTotal; k++ )
+        Counter += Aig_WordCountOnes( pSimL[k] ^ pSimR[k] );
+    return Counter;
 }
 
 
 
-
-
 /**Function*************************************************************
 
   Synopsis    [Generated const 0 pattern.]
@@ -130,7 +150,7 @@ unsigned Fra_NodeHashSims( Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_SavePattern0( Fra_Man_t * p, int fInit )
+void Fra_SmlSavePattern0( Fra_Man_t * p, int fInit )
 {
     memset( p->pPatWords, 0, sizeof(unsigned) * p->nPatWords );
 }
@@ -146,13 +166,14 @@ void Fra_SavePattern0( Fra_Man_t * p, int fInit )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_SavePattern1( Fra_Man_t * p, int fInit )
+void Fra_SmlSavePattern1( Fra_Man_t * p, int fInit )
 {
     Aig_Obj_t * pObj;
     int i, k, nTruePis;
     memset( p->pPatWords, 0xff, sizeof(unsigned) * p->nPatWords );
     if ( !fInit )
         return;
+    // clear the state bits to correspond to all-0 initial state
     nTruePis = Aig_ManPiNum(p->pManAig) - Aig_ManRegNum(p->pManAig);
     k = 0;
     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
@@ -170,7 +191,7 @@ void Fra_SavePattern1( Fra_Man_t * p, int fInit )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_SavePattern( Fra_Man_t * p )
+void Fra_SmlSavePattern( Fra_Man_t * p )
 {
     Aig_Obj_t * pObj;
     int i;
@@ -199,7 +220,7 @@ void Fra_SavePattern( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj )
+void Fra_SmlCheckOutputSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj )
 { 
     unsigned * pSims;
     int i, k, BestPat, * pModel;
@@ -241,7 +262,7 @@ void Fra_CheckOutputSimsSavePattern( Fra_Man_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_CheckOutputSims( Fra_Man_t * p )
+int Fra_SmlCheckOutput( Fra_Man_t * p )
 {
     Aig_Obj_t * pObj;
     int i;
@@ -250,10 +271,10 @@ int Fra_CheckOutputSims( Fra_Man_t * p )
     assert( Aig_ObjFanin0(pObj)->fPhase == (unsigned)Aig_ObjFaninC0(pObj) ); 
     Aig_ManForEachPo( p->pManAig, pObj, i )
     {
-        if ( !Fra_NodeHasZeroSim( Aig_ObjFanin0(pObj) ) )
+        if ( !Fra_SmlNodeIsConst( Aig_ObjFanin0(pObj) ) )
         {
             // create the counter-example from this pattern
-            Fra_CheckOutputSimsSavePattern( p, Aig_ObjFanin0(pObj) );
+            Fra_SmlCheckOutputSavePattern( p, Aig_ObjFanin0(pObj) );
             return 1;
         }
     }
@@ -365,6 +386,8 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat )
     }
     else
     {
+        int fUseDist1 = 0;
+
         // copy the PI info for each frame
         nTruePis = Aig_ManPiNum(p->pAig) - Aig_ManRegNum(p->pAig);
         for ( f = 0; f < p->nFrames; f++ )
@@ -375,16 +398,15 @@ void Fra_SmlAssignDist1( Fra_Sml_t * p, unsigned * pPat )
         Aig_ManForEachLoSeq( p->pAig, pObj, i )
             Fra_SmlAssignConst( p, pObj, Aig_InfoHasBit(pPat, nTruePis * p->nFrames + k++), 0 );
 //        assert( p->pManFraig == NULL || nTruePis * p->nFrames + k == Aig_ManPiNum(p->pManFraig) );
-/*
+
         // flip one bit of the last frame
-        if ( p->nFrames == 2 )
+        if ( fUseDist1 && p->nFrames == 2 )
         {
             Limit = AIG_MIN( nTruePis, p->nWordsFrame * 32 - 1 );
             for ( i = 0; i < Limit; i++ )
                 Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, i)->Id ), i+1 );
 //            Aig_InfoXorBit( Fra_ObjSim( p, Aig_ManPi(p->pAig, nTruePis*(p->nFrames-2) + i)->Id ), i+1 );
         }
-*/
     }
 }
 
@@ -571,7 +593,7 @@ void Fra_SmlResimulate( Fra_Man_t * p )
     Fra_SmlSimulateOne( p->pSml );
 //    if ( p->pPars->fPatScores )
 //        Fra_CleanPatScores( p );
-    if ( p->pPars->fProve && Fra_CheckOutputSims(p) )
+    if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
         return;
 clk = clock();
     nChanges = Fra_ClassesRefine( p->pCla );
@@ -581,7 +603,7 @@ clk = clock();
 p->timeRef += clock() - clk;
     if ( nChanges < 1 )
         printf( "Error: A counter-example did not refine classes!\n" );
-    assert( nChanges >= 1 );
+//    assert( nChanges >= 1 );
 //printf( "Refined classes = %5d.   Changes = %4d.\n", Vec_PtrSize(p->vClasses), nChanges );
 }
 
@@ -609,11 +631,13 @@ void Fra_SmlSimulate( Fra_Man_t * p, int fInit )
 if ( fVerbose )
 printf( "Starting classes = %5d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), Fra_ClassesCountLits(p->pCla) );
 
+//return;
+
     // refine classes by walking 0/1 patterns
-    Fra_SavePattern0( p, fInit );
+    Fra_SmlSavePattern0( p, fInit );
     Fra_SmlAssignDist1( p->pSml, p->pPatWords );
     Fra_SmlSimulateOne( p->pSml );
-    if ( p->pPars->fProve && Fra_CheckOutputSims(p) )
+    if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
         return;
 clk = clock();
     nChanges = Fra_ClassesRefine( p->pCla );
@@ -621,10 +645,10 @@ clk = clock();
 p->timeRef += clock() - clk;
 if ( fVerbose )
 printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(p->pCla->vClasses), nChanges, Fra_ClassesCountLits(p->pCla) );
-    Fra_SavePattern1( p, fInit );
+    Fra_SmlSavePattern1( p, fInit );
     Fra_SmlAssignDist1( p->pSml, p->pPatWords );
     Fra_SmlSimulateOne( p->pSml );
-    if ( p->pPars->fProve && Fra_CheckOutputSims(p) )
+    if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
         return;
 clk = clock();
     nChanges = Fra_ClassesRefine( p->pCla );
@@ -638,7 +662,7 @@ printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(
         Fra_SmlInitialize( p->pSml, fInit );
         Fra_SmlSimulateOne( p->pSml );
         nClasses = Vec_PtrSize(p->pCla->vClasses);
-        if ( p->pPars->fProve && Fra_CheckOutputSims(p) )
+        if ( p->pPars->fProve && Fra_SmlCheckOutput(p) )
             return;
 clk = clock();
         nChanges = Fra_ClassesRefine( p->pCla );
@@ -666,16 +690,18 @@ printf( "Refined classes  = %5d.   Changes = %4d.   Lits = %6d.\n", Vec_PtrSize(
   SeeAlso     []
 
 ***********************************************************************/
-Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nFrames, int nWordsFrame )
+Fra_Sml_t * Fra_SmlStart( Aig_Man_t * pAig, int nPref, int nFrames, int nWordsFrame )
 {
     Fra_Sml_t * p;
     assert( Aig_ManObjIdMax(pAig) + 1 < (1 << 16) );
-    p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * (Aig_ManObjIdMax(pAig) + 1) * nFrames * nWordsFrame );
-    memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * nFrames * nWordsFrame );
+    p = (Fra_Sml_t *)malloc( sizeof(Fra_Sml_t) + sizeof(unsigned) * (Aig_ManObjIdMax(pAig) + 1) * (nPref + nFrames) * nWordsFrame );
+    memset( p, 0, sizeof(Fra_Sml_t) + sizeof(unsigned) * (nPref + nFrames) * nWordsFrame );
     p->pAig        = pAig;
-    p->nFrames     = nFrames;
+    p->nPref       = nPref;
+    p->nFrames     = nPref + nFrames;
     p->nWordsFrame = nWordsFrame;
-    p->nWordsTotal = nFrames * nWordsFrame;
+    p->nWordsTotal = (nPref + nFrames) * nWordsFrame;
+    p->nWordsPref  = nPref * nWordsFrame;
     return p;
 }
 
@@ -710,7 +736,7 @@ void Fra_SmlStop( Fra_Sml_t * p )
 Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords )
 {
     Fra_Sml_t * p;
-    p = Fra_SmlStart( pAig, 1, nWords );
+    p = Fra_SmlStart( pAig, 0, 1, nWords );
     Fra_SmlInitialize( p, 0 );
     Fra_SmlSimulateOne( p );
     return p;
@@ -727,10 +753,10 @@ Fra_Sml_t * Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords )
   SeeAlso     []
 
 ***********************************************************************/
-Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nFrames, int nWords )
+Fra_Sml_t * Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nPref, int nFrames, int nWords )
 {
     Fra_Sml_t * p;
-    p = Fra_SmlStart( pAig, nFrames, nWords );
+    p = Fra_SmlStart( pAig, nPref, nFrames, nWords );
     Fra_SmlInitialize( p, 1 );
     Fra_SmlSimulateOne( p );
     return p;
diff --git a/src/aig/fra/module.make b/src/aig/fra/module.make
index f2a8b230..bd8a20be 100644
--- a/src/aig/fra/module.make
+++ b/src/aig/fra/module.make
@@ -1,4 +1,5 @@
-SRC +=    src/aig/fra/fraCec.c \
+SRC +=    src/aig/fra/fraBmc.c \
+    src/aig/fra/fraCec.c \
     src/aig/fra/fraClass.c \
     src/aig/fra/fraCnf.c \
     src/aig/fra/fraCore.c \
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index f2017549..16f66dc6 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -700,7 +700,7 @@ Abc_Obj_t * Abc_AigConst1( Abc_Ntk_t * pNtk )
 Abc_Obj_t * Abc_AigAnd( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
 {
     Abc_Obj_t * pAnd;
-    if ( pAnd = Abc_AigAndLookup( pMan, p0, p1 ) )
+    if ( (pAnd = Abc_AigAndLookup( pMan, p0, p1 )) )
         return pAnd;
     return Abc_AigAndCreate( pMan, p0, p1 );
 }
@@ -886,7 +886,7 @@ void Abc_AigReplace_int( Abc_Aig_t * pMan, Abc_Obj_t * pOld, Abc_Obj_t * pNew, i
         pFanin2 = Abc_ObjChild( pFanout, iFanin ^ 1 );
         assert( Abc_ObjRegular(pFanin2) != pFanout );
         // check if the node with these fanins exists
-        if ( pFanoutNew = Abc_AigAndLookup( pMan, pFanin1, pFanin2 ) )
+        if ( (pFanoutNew = Abc_AigAndLookup( pMan, pFanin1, pFanin2 )) )
         { // such node exists (it may be a constant)
             // schedule replacement of the old fanout by the new fanout
             Vec_PtrPush( pMan->vStackReplaceOld, pFanout );
@@ -1347,8 +1347,8 @@ void Abc_AigCheckFaninOrder( Abc_Aig_t * pMan )
         {
             if ( Abc_ObjRegular(Abc_ObjChild0(pEnt))->Id > Abc_ObjRegular(Abc_ObjChild1(pEnt))->Id )
             {
-                int i0 = Abc_ObjRegular(Abc_ObjChild0(pEnt))->Id;
-                int i1 = Abc_ObjRegular(Abc_ObjChild1(pEnt))->Id;
+//                int i0 = Abc_ObjRegular(Abc_ObjChild0(pEnt))->Id;
+//                int i1 = Abc_ObjRegular(Abc_ObjChild1(pEnt))->Id;
                 printf( "Node %d has incorrect ordering of fanins.\n", pEnt->Id );
             }
         }
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index cd78f218..c2eead14 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -291,7 +291,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "New AIG",      "iprove",        Abc_CommandIProve,           1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "haig",          Abc_CommandHaig,             1 );
     Cmd_CommandAdd( pAbc, "New AIG",      "mini",          Abc_CommandMini,             1 );
-    Cmd_CommandAdd( pAbc, "New AIG",      "bmc",           Abc_CommandBmc,              0 );
+    Cmd_CommandAdd( pAbc, "New AIG",      "_bmc",           Abc_CommandBmc,              0 );
     Cmd_CommandAdd( pAbc, "New AIG",      "qbf",           Abc_CommandQbf,              0 );
 
     Cmd_CommandAdd( pAbc, "Fraiging",     "fraig",         Abc_CommandFraig,            1 );
@@ -8039,7 +8039,7 @@ int Abc_CommandBmc( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: bmc [-K num] [-ivh]\n" );
+    fprintf( pErr, "usage: _bmc [-K num] [-ivh]\n" );
     fprintf( pErr, "\t         perform bounded model checking\n" );
     fprintf( pErr, "\t-K num : number of time frames [default = %d]\n", nFrames );
     fprintf( pErr, "\t-i     : toggle initialization of the first frame [default = %s]\n", fInit? "yes": "no" );
@@ -10972,19 +10972,21 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
+    int nFramesP;
     int nFramesK;
     int fExdc;
     int fUseImps;
     int fRewrite;
     int fLatchCorr;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFrames, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    nFramesP   = 0;
     nFramesK   = 1;
     fExdc      = 1;
     fUseImps   = 0;
@@ -10992,10 +10994,21 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     fLatchCorr = 0;
     fVerbose   = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Feirlvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PFeirlvh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'P':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-P\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nFramesP = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nFramesP < 0 ) 
+                goto usage;
+            break;
         case 'F':
             if ( globalUtilOptind >= argc )
             {
@@ -11048,7 +11061,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose );
+    pNtkRes = Abc_NtkDarSeqSweep( pNtk, nFramesP, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential sweeping has failed.\n" );
@@ -11059,8 +11072,9 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ssweep [-F num] [-ilrvh]\n" );
+    fprintf( pErr, "usage: ssweep [-P num] [-F num] [-ilrvh]\n" );
     fprintf( pErr, "\t         performs sequential sweep using K-step induction\n" );
+    fprintf( pErr, "\t-P num : number of time frames to use as the prefix [default = %d]\n", nFramesP );
     fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
 //    fprintf( pErr, "\t-e     : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
     fprintf( pErr, "\t-i     : toggle using implications [default = %s]\n", fUseImps? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index de527306..99217030 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -892,7 +892,7 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose )
+Abc_Ntk_t * Abc_NtkDarSeqSweep( Abc_Ntk_t * pNtk, int nFramesP, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose )
 {
     Fraig_Params_t Params;
     Abc_Ntk_t * pNtkAig, * pNtkFraig;
@@ -911,7 +911,7 @@ Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int f
     if ( pMan == NULL )
         return NULL;
 
-    pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL );
+    pMan = Fra_FraigInduction( pTemp = pMan, nFramesP, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL );
     Aig_ManStop( pTemp );
 
     if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index c4ec68f3..1ae8745b 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -335,8 +335,8 @@ void Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUs
     {
         Arrival1 = Abc_NodeReadArrival(pNodeMin)->Worst;
         Arrival2 = Abc_NodeReadArrival(pNode   )->Worst;
-        assert( Abc_ObjIsCi(pNodeMin) || Arrival1 > 0 );
-        assert( Abc_ObjIsCi(pNode)    || Arrival2 > 0 );
+//        assert( Abc_ObjIsCi(pNodeMin) || Arrival1 > 0 );
+//        assert( Abc_ObjIsCi(pNode)    || Arrival2 > 0 );
         if (  Arrival1 > Arrival2 ||
               Arrival1 == Arrival2 && pNodeMin->Level >  pNode->Level || 
               Arrival1 == Arrival2 && pNodeMin->Level == pNode->Level && 
@@ -355,8 +355,8 @@ void Abc_NtkFraigMergeClassMapped( Abc_Ntk_t * pNtk, Abc_Obj_t * pChain, int fUs
     {
         Arrival1 = Abc_NodeReadArrival(pNodeMin)->Worst;
         Arrival2 = Abc_NodeReadArrival(pNode   )->Worst;
-        assert( Abc_ObjIsCi(pNodeMin) || Arrival1 > 0 );
-        assert( Abc_ObjIsCi(pNode)    || Arrival2 > 0 );
+//        assert( Abc_ObjIsCi(pNodeMin) || Arrival1 > 0 );
+//        assert( Abc_ObjIsCi(pNode)    || Arrival2 > 0 );
         if (  Arrival1 > Arrival2 ||
               Arrival1 == Arrival2 && pNodeMin->Level >  pNode->Level || 
               Arrival1 == Arrival2 && pNodeMin->Level == pNode->Level &&