29 files changed, 2476 insertions, 82 deletions

diff --git a/Makefile b/Makefile
index 7ddae873..a7097489 100644
--- a/Makefile
+++ b/Makefile
@@ -20,7 +20,7 @@ MODULES := src/base/abc src/base/abci src/base/cmd \
 	src/aig/mem src/aig/dar src/aig/fra src/aig/cnf \
 	src/aig/csw src/aig/ioa src/aig/aig src/aig/kit \
 	src/aig/bdc src/aig/bar src/aig/ntl src/aig/nwk src/aig/mfx \
-	src/aig/tim src/aig/saig
+	src/aig/tim src/aig/saig src/aig/bbr
 
 default: $(PROG)
 
diff --git a/abc.dsp b/abc.dsp
index 60fe207b..4fababfe 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -42,7 +42,7 @@ RSC=rc.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /GX /O2 /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /c
-# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
+# ADD CPP /nologo /W3 /GX /O2 /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "NDEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /c
 # ADD BASE RSC /l 0x409 /d "NDEBUG"
 # ADD RSC /l 0x409 /d "NDEBUG"
 BSC32=bscmake.exe
@@ -66,7 +66,7 @@ LINK32=link.exe
 # PROP Ignore_Export_Lib 0
 # PROP Target_Dir ""
 # ADD BASE CPP /nologo /W3 /Gm /GX /ZI /Od /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /YX /FD /GZ /c
-# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
+# ADD CPP /nologo /W3 /Gm /GX /ZI /Od /I "src/base/abc" /I "src/base/abci" /I "src/base/cmd" /I "src/base/io" /I "src/base/main" /I "src/base/ver" /I "src/bdd/cudd" /I "src/bdd/dsd" /I "src/bdd/epd" /I "src/bdd/mtr" /I "src/bdd/parse" /I "src/bdd/reo" /I "src/bdd/cas" /I "src/map/fpga" /I "src/map/mapper" /I "src/map/mio" /I "src/map/super" /I "src/map/if" /I "src/map/pcm" /I "src/map/ply" /I "src/misc/extra" /I "src/misc/mvc" /I "src/misc/st" /I "src/misc/util" /I "src/misc/espresso" /I "src/misc/nm" /I "src/misc/vec" /I "src/misc/hash" /I "src/opt/cut" /I "src/opt/dec" /I "src/opt/fxu" /I "src/opt/rwr" /I "src/opt/sim" /I "src/opt/ret" /I "src/opt/res" /I "src/opt/lpk" /I "src/sat/bsat" /I "src/sat/csat" /I "src/sat/msat" /I "src/sat/fraig" /I "src/aig/ivy" /I "src/aig/hop" /I "src/aig/rwt" /I "src/aig/deco" /I "src/aig/mem" /I "src/aig/dar" /I "src/aig/fra" /I "src/aig/cnf" /I "src/aig/csw" /I "src/aig/ioa" /I "src/aig/aig" /I "src/aig/kit" /I "src/aig/bdc" /I "src/aig/bar" /I "src/aig/ntl" /I "src/aig/nwk" /I "src/aig/tim" /I "src/opt/mfs" /I "src/aig/mfx" /I "src/aig/saig" /I "src/aig/bbr" /D "WIN32" /D "_DEBUG" /D "_CONSOLE" /D "_MBCS" /D "__STDC__" /FR /YX /FD /GZ /c
 # SUBTRACT CPP /X
 # ADD BASE RSC /l 0x409 /d "_DEBUG"
 # ADD RSC /l 0x409 /d "_DEBUG"
@@ -3269,6 +3269,26 @@ SOURCE=.\src\aig\saig\saigRetMin.c
 SOURCE=.\src\aig\saig\saigScl.c
 # End Source File
 # End Group
+# Begin Group "bbr"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\bbr\bbr.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\bbr\bbrImage.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\bbr\bbrNtbdd.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\bbr\bbrReach.c
+# End Source File
+# End Group
 # End Group
 # End Group
 # Begin Group "Header Files"
diff --git a/src/aig/bbr/bbr.h b/src/aig/bbr/bbr.h
new file mode 100644
index 00000000..504fc463
--- /dev/null
+++ b/src/aig/bbr/bbr.h
@@ -0,0 +1,88 @@
+/**CFile****************************************************************
+
+  FileName    [bbr.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD-based reachability analysis.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bbr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __BBR_H__
+#define __BBR_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include <stdio.h>
+#include "cuddInt.h"
+#include "aig.h"
+#include "saig.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+static inline DdNode * Aig_ObjGlobalBdd( Aig_Obj_t * pObj )  { return pObj->pData; }
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== bbrImage.c ==========================================================*/
+typedef struct Bbr_ImageTree_t_  Bbr_ImageTree_t;
+extern Bbr_ImageTree_t * Bbr_bddImageStart( 
+    DdManager * dd, DdNode * bCare,
+    int nParts, DdNode ** pbParts,
+    int nVars, DdNode ** pbVars, int fVerbose );
+extern DdNode *    Bbr_bddImageCompute( Bbr_ImageTree_t * pTree, DdNode * bCare );
+extern void        Bbr_bddImageTreeDelete( Bbr_ImageTree_t * pTree );
+extern DdNode *    Bbr_bddImageRead( Bbr_ImageTree_t * pTree );
+typedef struct Bbr_ImageTree2_t_  Bbr_ImageTree2_t;
+extern Bbr_ImageTree2_t * Bbr_bddImageStart2( 
+    DdManager * dd, DdNode * bCare,
+    int nParts, DdNode ** pbParts,
+    int nVars, DdNode ** pbVars, int fVerbose );
+extern DdNode *    Bbr_bddImageCompute2( Bbr_ImageTree2_t * pTree, DdNode * bCare );
+extern void        Bbr_bddImageTreeDelete2( Bbr_ImageTree2_t * pTree );
+extern DdNode *    Bbr_bddImageRead2( Bbr_ImageTree2_t * pTree );
+/*=== bbrNtbdd.c ==========================================================*/
+extern void        Aig_ManFreeGlobalBdds( Aig_Man_t * p, DdManager * dd );
+extern int         Aig_ManSizeOfGlobalBdds( Aig_Man_t * p );
+extern DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose );
+/*=== bbrReach.c ==========================================================*/
+extern int         Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/bbr/bbrImage.c b/src/aig/bbr/bbrImage.c
new file mode 100644
index 00000000..cfe70d15
--- /dev/null
+++ b/src/aig/bbr/bbrImage.c
@@ -0,0 +1,1286 @@
+/**CFile****************************************************************
+
+  FileName    [bbrImage.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD-based reachability analysis.]
+
+  Synopsis    [Performs image computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bbrImage.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bbr.h"
+#include "mtr.h"
+
+/* 
+    The ideas implemented in this file are inspired by the paper:
+    Pankaj Chauhan, Edmund Clarke, Somesh Jha, Jim Kukula, Tom Shiple, 
+    Helmut Veith, Dong Wang. Non-linear Quantification Scheduling in 
+    Image Computation. ICCAD, 2001.
+*/
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+typedef struct Bbr_ImageNode_t_  Bbr_ImageNode_t;
+typedef struct Bbr_ImagePart_t_  Bbr_ImagePart_t;
+typedef struct Bbr_ImageVar_t_   Bbr_ImageVar_t;
+
+struct Bbr_ImageTree_t_
+{
+    Bbr_ImageNode_t *   pRoot;      // the root of quantification tree
+    Bbr_ImageNode_t *   pCare;      // the leaf node with the care set
+    DdNode *            bCareSupp;  // the cube to quantify from the care
+    int                 fVerbose;   // the verbosity flag
+    int                 nNodesMax;  // the max number of nodes in one iter
+    int                 nNodesMaxT; // the overall max number of nodes
+    int                 nIter;      // the number of iterations with this tree
+};
+
+struct Bbr_ImageNode_t_
+{
+    DdManager *         dd;         // the manager 
+    DdNode *            bCube;      // the cube to quantify
+    DdNode *            bImage;     // the partial image
+    Bbr_ImageNode_t *   pNode1;     // the first branch
+    Bbr_ImageNode_t *   pNode2;     // the second branch
+    Bbr_ImagePart_t *   pPart;      // the partition (temporary)
+};
+
+struct Bbr_ImagePart_t_
+{
+    DdNode *            bFunc;      // the partition
+    DdNode *            bSupp;      // the support of this partition
+    int                 nNodes;     // the number of BDD nodes
+    short               nSupp;      // the number of support variables
+    short               iPart;      // the number of this partition
+};
+
+struct Bbr_ImageVar_t_
+{
+    int                 iNum;       // the BDD index of this variable
+    DdNode *            bParts;     // the partition numbers
+    int                 nParts;     // the number of partitions
+};
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+#define BDD_BLOW_UP  1000000
+
+#define     b0     Cudd_Not((dd)->one)
+#define     b1              (dd)->one
+
+#ifndef PRB
+#define PRB(dd,f)       printf("%s = ", #f); Bbr_bddPrint(dd,f); printf("\n")
+#endif
+
+/**AutomaticStart*************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+static Bbr_ImagePart_t ** Bbr_CreateParts( DdManager * dd,
+    int nParts, DdNode ** pbParts, DdNode * bCare );
+static Bbr_ImageVar_t ** Bbr_CreateVars( DdManager * dd,
+    int nParts, Bbr_ImagePart_t ** pParts,
+    int nVars, DdNode ** pbVarsNs );
+static Bbr_ImageNode_t ** Bbr_CreateNodes( DdManager * dd, 
+    int nParts, Bbr_ImagePart_t ** pParts, 
+    int nVars,  Bbr_ImageVar_t ** pVars );
+static void Bbr_DeleteParts_rec( Bbr_ImageNode_t * pNode );
+static int Bbr_BuildTreeNode( DdManager * dd, 
+    int nNodes, Bbr_ImageNode_t ** pNodes, 
+    int nVars,  Bbr_ImageVar_t ** pVars, int * pfStop );
+static Bbr_ImageNode_t * Bbr_MergeTopNodes( DdManager * dd, 
+    int nNodes, Bbr_ImageNode_t ** pNodes );
+static void Bbr_bddImageTreeDelete_rec( Bbr_ImageNode_t * pNode );
+static int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_ImageNode_t * pNode );
+static int Bbr_FindBestVariable( DdManager * dd,
+    int nNodes, Bbr_ImageNode_t ** pNodes, 
+    int nVars,  Bbr_ImageVar_t ** pVars );
+static void Bbr_FindBestPartitions( DdManager * dd, DdNode * bParts, 
+    int nNodes, Bbr_ImageNode_t ** pNodes, 
+    int * piNode1, int * piNode2 );
+static Bbr_ImageNode_t * Bbr_CombineTwoNodes( DdManager * dd, DdNode * bCube,
+    Bbr_ImageNode_t * pNode1, Bbr_ImageNode_t * pNode2 );
+
+static void Bbr_bddImagePrintLatchDependency( DdManager * dd, DdNode * bCare,
+    int nParts, DdNode ** pbParts,
+    int nVars, DdNode ** pbVars );
+static void Bbr_bddImagePrintLatchDependencyOne( DdManager * dd, DdNode * bFunc, 
+    DdNode * bVarsCs, DdNode * bVarsNs, int iPart );
+
+static void Bbr_bddImagePrintTree( Bbr_ImageTree_t * pTree );
+static void Bbr_bddImagePrintTree_rec( Bbr_ImageNode_t * pNode, int nOffset );
+
+static void Bbr_bddPrint( DdManager * dd, DdNode * F );
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the image computation using tree-based scheduling.]
+
+  Description [This procedure starts the image computation. It uses
+  the given care set to test-run the image computation and creates the 
+  quantification tree by scheduling variable quantifications. The tree can 
+  be used to compute images for other care sets without rescheduling.
+  In this case, Bbr_bddImageCompute() should be called.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbr_ImageTree_t * Bbr_bddImageStart( 
+    DdManager * dd, DdNode * bCare, // the care set
+    int nParts, DdNode ** pbParts,  // the partitions for image computation
+    int nVars, DdNode ** pbVars, int fVerbose )   // the NS and parameter variables (not quantified!)
+{
+    Bbr_ImageTree_t * pTree;
+    Bbr_ImagePart_t ** pParts;
+    Bbr_ImageVar_t ** pVars;
+    Bbr_ImageNode_t ** pNodes, * pCare;
+    int fStop, v;
+
+    if ( fVerbose && dd->size <= 80 )
+        Bbr_bddImagePrintLatchDependency( dd, bCare, nParts, pbParts, nVars, pbVars );
+
+    // create variables, partitions and leaf nodes
+    pParts = Bbr_CreateParts( dd, nParts, pbParts, bCare );
+    pVars  = Bbr_CreateVars( dd, nParts + 1, pParts, nVars, pbVars );
+    pNodes = Bbr_CreateNodes( dd, nParts + 1, pParts, dd->size, pVars );
+    pCare  = pNodes[nParts];
+
+    // process the nodes
+    while ( Bbr_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars, &fStop ) );
+
+    // consider the case of BDD node blowup
+    if ( fStop )
+    {
+        for ( v = 0; v < dd->size; v++ )
+            if ( pVars[v] )
+                free( pVars[v] );
+        free( pVars );
+        for ( v = 0; v <= nParts; v++ )
+            if ( pNodes[v] )
+            {
+                Bbr_DeleteParts_rec( pNodes[v] );
+                Bbr_bddImageTreeDelete_rec( pNodes[v] );
+            }
+        free( pNodes );
+        free( pParts );
+        return NULL;
+    }
+
+    // make sure the variables are gone
+    for ( v = 0; v < dd->size; v++ )
+        assert( pVars[v] == NULL );
+    FREE( pVars );
+    
+    // create the tree
+    pTree = ALLOC( Bbr_ImageTree_t, 1 );
+    memset( pTree, 0, sizeof(Bbr_ImageTree_t) );
+    pTree->pCare = pCare;
+    pTree->fVerbose = fVerbose;
+
+    // merge the topmost nodes
+    while ( (pTree->pRoot = Bbr_MergeTopNodes( dd, nParts + 1, pNodes )) == NULL );
+
+    // make sure the nodes are gone
+    for ( v = 0; v < nParts + 1; v++ )
+        assert( pNodes[v] == NULL );
+    FREE( pNodes );
+
+//    if ( fVerbose )
+//        Bbr_bddImagePrintTree( pTree );
+
+    // set the support of the care set
+    pTree->bCareSupp = Cudd_Support( dd, bCare );  Cudd_Ref( pTree->bCareSupp );
+
+    // clean the partitions
+    Bbr_DeleteParts_rec( pTree->pRoot );
+    FREE( pParts );
+    return pTree;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the image.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Bbr_bddImageCompute( Bbr_ImageTree_t * pTree, DdNode * bCare )
+{
+    DdManager * dd = pTree->pCare->dd;
+    DdNode * bSupp, * bRem;
+
+    pTree->nIter++;
+
+    // make sure the supports are okay
+    bSupp = Cudd_Support( dd, bCare );        Cudd_Ref( bSupp );
+    if ( bSupp != pTree->bCareSupp )
+    {
+        bRem = Cudd_bddExistAbstract( dd, bSupp, pTree->bCareSupp );  Cudd_Ref( bRem );
+        if ( bRem != b1 )
+        {
+printf( "Original care set support: " );
+PRB( dd, pTree->bCareSupp );
+printf( "Current care set support: " );
+PRB( dd, bSupp );
+            Cudd_RecursiveDeref( dd, bSupp );
+            Cudd_RecursiveDeref( dd, bRem );
+            printf( "The care set depends on some vars that were not in the care set during scheduling.\n" );
+            return NULL;
+        }
+        Cudd_RecursiveDeref( dd, bRem );
+    }
+    Cudd_RecursiveDeref( dd, bSupp );
+
+    // remove the previous image
+    Cudd_RecursiveDeref( dd, pTree->pCare->bImage );
+    pTree->pCare->bImage = bCare;   Cudd_Ref( bCare );
+
+    // compute the image
+    pTree->nNodesMax = 0;
+    if ( !Bbr_bddImageCompute_rec( pTree, pTree->pRoot ) )
+        return NULL;
+    if ( pTree->nNodesMaxT < pTree->nNodesMax )
+        pTree->nNodesMaxT = pTree->nNodesMax;
+
+//    if ( pTree->fVerbose )
+//        printf( "Iter %2d : Max nodes = %5d.\n", pTree->nIter, pTree->nNodesMax );
+    return pTree->pRoot->bImage;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Delete the tree.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_bddImageTreeDelete( Bbr_ImageTree_t * pTree )
+{
+    if ( pTree->bCareSupp )
+        Cudd_RecursiveDeref( pTree->pRoot->dd, pTree->bCareSupp );
+    Bbr_bddImageTreeDelete_rec( pTree->pRoot );
+    FREE( pTree );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the image from the tree.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Bbr_bddImageRead( Bbr_ImageTree_t * pTree )
+{
+    return pTree->pRoot->bImage;
+}
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+  Synopsis    [Outputs the BDD in a readable format.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+void Bbr_bddPrint( DdManager * dd, DdNode * F )
+{
+    DdGen * Gen;
+    int * Cube;
+    CUDD_VALUE_TYPE Value;
+    int nVars = dd->size;
+    int fFirstCube = 1;
+    int i;
+
+    if ( F == NULL )
+    {
+        printf("NULL");
+        return;
+    }
+    if ( F == b0 )
+    {
+        printf("Constant 0");
+        return;
+    }
+    if ( F == b1 )
+    {
+        printf("Constant 1");
+        return;
+    }
+
+    Cudd_ForeachCube( dd, F, Gen, Cube, Value )
+    {
+        if ( fFirstCube )
+            fFirstCube = 0;
+        else
+//          Output << " + ";
+            printf( " + " );
+
+        for ( i = 0; i < nVars; i++ )
+            if ( Cube[i] == 0 )
+                printf( "[%d]'", i );
+//              printf( "%c'", (char)('a'+i) );
+            else if ( Cube[i] == 1 )
+                printf( "[%d]", i );
+//              printf( "%c", (char)('a'+i) );
+    }
+
+//  printf("\n");
+}
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static Functions                                            */
+/*---------------------------------------------------------------------------*/
+
+/**Function*************************************************************
+
+  Synopsis    [Creates partitions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbr_ImagePart_t ** Bbr_CreateParts( DdManager * dd,
+    int nParts, DdNode ** pbParts, DdNode * bCare )
+{
+    Bbr_ImagePart_t ** pParts;
+    int i;
+
+    // start the partitions
+    pParts = ALLOC( Bbr_ImagePart_t *, nParts + 1 );
+    // create structures for each variable
+    for ( i = 0; i < nParts; i++ )
+    {
+        pParts[i] = ALLOC( Bbr_ImagePart_t, 1 );
+        pParts[i]->bFunc  = pbParts[i];                           Cudd_Ref( pParts[i]->bFunc );
+        pParts[i]->bSupp  = Cudd_Support( dd, pParts[i]->bFunc ); Cudd_Ref( pParts[i]->bSupp );
+        pParts[i]->nSupp  = Cudd_SupportSize( dd, pParts[i]->bSupp );
+        pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc );
+        pParts[i]->iPart  = i;
+    }
+    // add the care set as the last partition
+    pParts[nParts] = ALLOC( Bbr_ImagePart_t, 1 );
+    pParts[nParts]->bFunc = bCare;                                     Cudd_Ref( pParts[nParts]->bFunc );
+    pParts[nParts]->bSupp = Cudd_Support( dd, pParts[nParts]->bFunc ); Cudd_Ref( pParts[nParts]->bSupp );
+    pParts[nParts]->nSupp = Cudd_SupportSize( dd, pParts[nParts]->bSupp );
+    pParts[nParts]->nNodes = Cudd_DagSize( pParts[nParts]->bFunc );
+    pParts[nParts]->iPart  = nParts;
+    return pParts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbr_ImageVar_t ** Bbr_CreateVars( DdManager * dd,
+    int nParts, Bbr_ImagePart_t ** pParts,
+    int nVars, DdNode ** pbVars )
+{
+    Bbr_ImageVar_t ** pVars;
+    DdNode ** pbFuncs;
+    DdNode * bCubeNs, * bSupp, * bParts, * bTemp, * bSuppTemp;
+    int nVarsTotal, iVar, p, Counter;
+
+    // put all the functions into one array
+    pbFuncs = ALLOC( DdNode *, nParts );
+    for ( p = 0; p < nParts; p++ )
+        pbFuncs[p] = pParts[p]->bSupp;
+    bSupp = Cudd_VectorSupport( dd, pbFuncs, nParts );  Cudd_Ref( bSupp );
+    FREE( pbFuncs );
+
+    // remove the NS vars
+    bCubeNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars );        Cudd_Ref( bCubeNs );
+    bSupp = Cudd_bddExistAbstract( dd, bTemp = bSupp, bCubeNs );     Cudd_Ref( bSupp );
+    Cudd_RecursiveDeref( dd, bTemp );
+    Cudd_RecursiveDeref( dd, bCubeNs );
+
+    // get the number of I and CS variables to be quantified
+    nVarsTotal = Cudd_SupportSize( dd, bSupp );
+
+    // start the variables
+    pVars = ALLOC( Bbr_ImageVar_t *, dd->size );
+    memset( pVars, 0, sizeof(Bbr_ImageVar_t *) * dd->size );
+    // create structures for each variable
+    for ( bSuppTemp = bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
+    {
+        iVar = bSuppTemp->index;
+        pVars[iVar] = ALLOC( Bbr_ImageVar_t, 1 );
+        pVars[iVar]->iNum = iVar;
+        // collect all the parts this var belongs to
+        Counter = 0;
+        bParts = b1; Cudd_Ref( bParts );
+        for ( p = 0; p < nParts; p++ )
+            if ( Cudd_bddLeq( dd, pParts[p]->bSupp, dd->vars[bSuppTemp->index] ) )
+            {
+                bParts = Cudd_bddAnd( dd, bTemp = bParts, dd->vars[p] );  Cudd_Ref( bParts );
+                Cudd_RecursiveDeref( dd, bTemp );
+                Counter++;
+            }
+        pVars[iVar]->bParts = bParts; // takes ref
+        pVars[iVar]->nParts = Counter;
+    }
+    Cudd_RecursiveDeref( dd, bSupp );
+    return pVars;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbr_ImageNode_t ** Bbr_CreateNodes( DdManager * dd, 
+    int nParts, Bbr_ImagePart_t ** pParts, 
+    int nVars,  Bbr_ImageVar_t ** pVars )
+{
+    Bbr_ImageNode_t ** pNodes;
+    Bbr_ImageNode_t * pNode;
+    DdNode * bTemp;
+    int i, v, iPart;
+/*
+    DdManager *         dd;       // the manager 
+    DdNode *            bCube;    // the cube to quantify
+    DdNode *            bImage;   // the partial image
+    Bbr_ImageNode_t * pNode1;   // the first branch
+    Bbr_ImageNode_t * pNode2;   // the second branch
+    Bbr_ImagePart_t * pPart;    // the partition (temporary)
+*/
+    // start the partitions
+    pNodes = ALLOC( Bbr_ImageNode_t *, nParts );
+    // create structures for each leaf nodes
+    for ( i = 0; i < nParts; i++ )
+    {
+        pNodes[i] = ALLOC( Bbr_ImageNode_t, 1 );
+        memset( pNodes[i], 0, sizeof(Bbr_ImageNode_t) );
+        pNodes[i]->dd    = dd;
+        pNodes[i]->pPart = pParts[i];
+    }
+    // find the quantification cubes for each leaf node
+    for ( v = 0; v < nVars; v++ )
+    {
+        if ( pVars[v] == NULL )
+            continue;
+        assert( pVars[v]->nParts > 0 );
+        if ( pVars[v]->nParts > 1 )
+            continue;
+        iPart = pVars[v]->bParts->index;
+        if ( pNodes[iPart]->bCube == NULL )
+        {
+            pNodes[iPart]->bCube = dd->vars[v];   
+            Cudd_Ref( dd->vars[v] );
+        }
+        else
+        {
+            pNodes[iPart]->bCube = Cudd_bddAnd( dd, bTemp = pNodes[iPart]->bCube, dd->vars[v] );  
+            Cudd_Ref( pNodes[iPart]->bCube );
+            Cudd_RecursiveDeref( dd, bTemp );
+        }
+        // remove these  variables
+        Cudd_RecursiveDeref( dd, pVars[v]->bParts );
+        FREE( pVars[v] );
+    }
+
+    // assign the leaf node images
+    for ( i = 0; i < nParts; i++ )
+    {
+        pNode = pNodes[i];
+        if ( pNode->bCube )
+        {
+            // update the partition
+            pParts[i]->bFunc = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bFunc, pNode->bCube );
+            Cudd_Ref( pParts[i]->bFunc );
+            Cudd_RecursiveDeref( dd, bTemp );
+            // update the support the partition
+            pParts[i]->bSupp = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bSupp, pNode->bCube ); 
+            Cudd_Ref( pParts[i]->bSupp );
+            Cudd_RecursiveDeref( dd, bTemp );
+            // update the numbers
+            pParts[i]->nSupp  = Cudd_SupportSize( dd, pParts[i]->bSupp );
+            pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc );
+            // get rid of the cube
+            // save the last (care set) quantification cube
+            if ( i < nParts - 1 )
+            {
+                Cudd_RecursiveDeref( dd, pNode->bCube );
+                pNode->bCube = NULL;
+            }
+        }
+        // copy the function
+        pNode->bImage = pParts[i]->bFunc;   Cudd_Ref( pNode->bImage );
+    }
+/*
+    for ( i = 0; i < nParts; i++ )
+    {
+        pNode = pNodes[i];
+PRB( dd, pNode->bCube );
+PRB( dd, pNode->pPart->bFunc );
+PRB( dd, pNode->pPart->bSupp );
+printf( "\n" );
+    }
+*/
+    return pNodes;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Delete the partitions from the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_DeleteParts_rec( Bbr_ImageNode_t * pNode )
+{
+    Bbr_ImagePart_t * pPart;
+    if ( pNode->pNode1 )
+        Bbr_DeleteParts_rec( pNode->pNode1 );
+    if ( pNode->pNode2 )
+        Bbr_DeleteParts_rec( pNode->pNode2 );
+    pPart = pNode->pPart;
+    Cudd_RecursiveDeref( pNode->dd, pPart->bFunc );
+    Cudd_RecursiveDeref( pNode->dd, pPart->bSupp );
+    FREE( pNode->pPart );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Delete the partitions from the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_bddImageTreeDelete_rec( Bbr_ImageNode_t * pNode )
+{
+    if ( pNode->pNode1 )
+        Bbr_bddImageTreeDelete_rec( pNode->pNode1 );
+    if ( pNode->pNode2 )
+        Bbr_bddImageTreeDelete_rec( pNode->pNode2 );
+    if ( pNode->bCube )
+        Cudd_RecursiveDeref( pNode->dd, pNode->bCube );
+    if ( pNode->bImage )
+        Cudd_RecursiveDeref( pNode->dd, pNode->bImage );
+    assert( pNode->pPart == NULL );
+    FREE( pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recompute the image.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_ImageNode_t * pNode )
+{
+    DdManager * dd = pNode->dd;
+    DdNode * bTemp;
+    int nNodes;
+
+    // trivial case
+    if ( pNode->pNode1 == NULL )
+    {
+        if ( pNode->bCube )
+        {
+            pNode->bImage = Cudd_bddExistAbstract( dd, bTemp = pNode->bImage, pNode->bCube ); 
+            Cudd_Ref( pNode->bImage );
+            Cudd_RecursiveDeref( dd, bTemp );
+        }
+        return 1;
+    }
+
+    // compute the children
+    if ( pNode->pNode1 )
+        if ( !Bbr_bddImageCompute_rec( pTree, pNode->pNode1 ) )
+            return 0;
+    if ( pNode->pNode2 )
+        if ( !Bbr_bddImageCompute_rec( pTree, pNode->pNode2 ) )
+            return 0;
+
+    // clean the old image
+    if ( pNode->bImage )
+        Cudd_RecursiveDeref( dd, pNode->bImage );
+    pNode->bImage = NULL;
+
+    // compute the new image
+    if ( pNode->bCube )
+        pNode->bImage = Cudd_bddAndAbstract( dd, 
+            pNode->pNode1->bImage, pNode->pNode2->bImage, pNode->bCube );
+    else
+        pNode->bImage = Cudd_bddAnd( dd, pNode->pNode1->bImage, pNode->pNode2->bImage );
+    Cudd_Ref( pNode->bImage );
+
+    if ( pTree->fVerbose )
+    {
+        nNodes = Cudd_DagSize( pNode->bImage );
+        if ( pTree->nNodesMax < nNodes )
+            pTree->nNodesMax = nNodes;
+    }
+    if ( dd->keys > BDD_BLOW_UP )
+        return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Builds the tree.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bbr_BuildTreeNode( DdManager * dd, 
+    int nNodes, Bbr_ImageNode_t ** pNodes, 
+    int nVars,  Bbr_ImageVar_t ** pVars, int * pfStop )
+{
+    Bbr_ImageNode_t * pNode1, * pNode2;
+    Bbr_ImageVar_t * pVar;
+    Bbr_ImageNode_t * pNode;
+    DdNode * bCube, * bTemp, * bSuppTemp, * bParts;
+    int iNode1, iNode2;
+    int iVarBest, nSupp, v;
+
+    // find the best variable
+    iVarBest = Bbr_FindBestVariable( dd, nNodes, pNodes, nVars, pVars );
+    if ( iVarBest == -1 )
+        return 0;
+
+    pVar = pVars[iVarBest];
+
+    // this var cannot appear in one partition only
+    nSupp = Cudd_SupportSize( dd, pVar->bParts );
+    assert( nSupp == pVar->nParts );
+    assert( nSupp != 1 );
+
+    // if it appears in only two partitions, quantify it
+    if ( pVar->nParts == 2 )
+    {
+        // get the nodes
+        iNode1 = pVar->bParts->index;
+        iNode2 = cuddT(pVar->bParts)->index;
+        pNode1 = pNodes[iNode1];
+        pNode2 = pNodes[iNode2];
+
+        // get the quantification cube
+        bCube = dd->vars[pVar->iNum];    Cudd_Ref( bCube );
+        // add the variables that appear only in these partitions
+        for ( v = 0; v < nVars; v++ )
+            if ( pVars[v] && v != iVarBest && pVars[v]->bParts == pVars[iVarBest]->bParts )
+            {
+                // add this var
+                bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[pVars[v]->iNum] );   Cudd_Ref( bCube );
+                Cudd_RecursiveDeref( dd, bTemp );
+                // clean this var
+                Cudd_RecursiveDeref( dd, pVars[v]->bParts );
+                FREE( pVars[v] );
+            }
+        // clean the best var
+        Cudd_RecursiveDeref( dd, pVars[iVarBest]->bParts );
+        FREE( pVars[iVarBest] );
+
+        // combines two nodes
+        pNode = Bbr_CombineTwoNodes( dd, bCube, pNode1, pNode2 );
+        Cudd_RecursiveDeref( dd, bCube );
+    }
+    else // if ( pVar->nParts > 2 )
+    {
+        // find two smallest BDDs that have this var
+        Bbr_FindBestPartitions( dd, pVar->bParts, nNodes, pNodes, &iNode1, &iNode2 );
+        pNode1 = pNodes[iNode1];
+        pNode2 = pNodes[iNode2];
+
+        // it is not possible that a var appears only in these two
+        // otherwise, it would have a different cost
+        bParts = Cudd_bddAnd( dd, dd->vars[iNode1], dd->vars[iNode2] ); Cudd_Ref( bParts );
+        for ( v = 0; v < nVars; v++ )
+            if ( pVars[v] && pVars[v]->bParts == bParts )
+                assert( 0 );
+        Cudd_RecursiveDeref( dd, bParts );
+
+        // combines two nodes
+        pNode = Bbr_CombineTwoNodes( dd, b1, pNode1, pNode2 );
+    }
+
+    // clean the old nodes
+    pNodes[iNode1] = pNode;
+    pNodes[iNode2] = NULL;
+    
+    // update the variables that appear in pNode[iNode2]
+    for ( bSuppTemp = pNode2->pPart->bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
+    {
+        pVar = pVars[bSuppTemp->index];
+        if ( pVar == NULL ) // this variable is not be quantified
+            continue;
+        // quantify this var
+        assert( Cudd_bddLeq( dd, pVar->bParts, dd->vars[iNode2] ) );
+        pVar->bParts = Cudd_bddExistAbstract( dd, bTemp = pVar->bParts, dd->vars[iNode2] ); Cudd_Ref( pVar->bParts );
+        Cudd_RecursiveDeref( dd, bTemp );
+        // add the new var
+        pVar->bParts = Cudd_bddAnd( dd, bTemp = pVar->bParts, dd->vars[iNode1] ); Cudd_Ref( pVar->bParts );
+        Cudd_RecursiveDeref( dd, bTemp );
+        // update the score
+        pVar->nParts = Cudd_SupportSize( dd, pVar->bParts );
+    }
+
+    *pfStop = 0;
+    if ( dd->keys > BDD_BLOW_UP )
+    {
+        *pfStop = 1;
+        return 0;
+    }
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Merges the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbr_ImageNode_t * Bbr_MergeTopNodes(
+    DdManager * dd, int nNodes, Bbr_ImageNode_t ** pNodes )
+{
+    Bbr_ImageNode_t * pNode;
+    int n1 = -1, n2 = -1, n;
+
+    // find the first and the second non-empty spots
+    for ( n = 0; n < nNodes; n++ )
+        if ( pNodes[n] )
+        {
+            if ( n1 == -1 )
+                n1 = n;
+            else if ( n2 == -1 )
+            {
+                n2 = n;
+                break;
+            }
+        }
+    assert( n1 != -1 );
+    // check the situation when only one such node is detected
+    if ( n2 == -1 )
+    {
+        // save the node
+        pNode = pNodes[n1];
+        // clean the node
+        pNodes[n1] = NULL;
+        return pNode;
+    }
+  
+    // combines two nodes
+    pNode = Bbr_CombineTwoNodes( dd, b1, pNodes[n1], pNodes[n2] );
+
+    // clean the old nodes
+    pNodes[n1] = pNode;
+    pNodes[n2] = NULL;
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbr_ImageNode_t * Bbr_CombineTwoNodes( DdManager * dd, DdNode * bCube,
+    Bbr_ImageNode_t * pNode1, Bbr_ImageNode_t * pNode2 )
+{
+    Bbr_ImageNode_t * pNode;
+    Bbr_ImagePart_t * pPart;
+
+    // create a new partition
+    pPart = ALLOC( Bbr_ImagePart_t, 1 );
+    memset( pPart, 0, sizeof(Bbr_ImagePart_t) );
+    // create the function
+    pPart->bFunc = Cudd_bddAndAbstract( dd, pNode1->pPart->bFunc, pNode2->pPart->bFunc, bCube );
+    Cudd_Ref( pPart->bFunc );
+    // update the support the partition
+    pPart->bSupp = Cudd_bddAndAbstract( dd, pNode1->pPart->bSupp, pNode2->pPart->bSupp, bCube );
+    Cudd_Ref( pPart->bSupp );
+    // update the numbers
+    pPart->nSupp  = Cudd_SupportSize( dd, pPart->bSupp );
+    pPart->nNodes = Cudd_DagSize( pPart->bFunc );
+    pPart->iPart = -1;
+/*
+PRB( dd, pNode1->pPart->bSupp );
+PRB( dd, pNode2->pPart->bSupp );
+PRB( dd, pPart->bSupp );
+*/
+    // create a new node
+    pNode = ALLOC( Bbr_ImageNode_t, 1 );
+    memset( pNode, 0, sizeof(Bbr_ImageNode_t) );
+    pNode->dd     = dd;
+    pNode->pPart  = pPart;
+    pNode->pNode1 = pNode1;
+    pNode->pNode2 = pNode2;
+    // compute the image
+    pNode->bImage = Cudd_bddAndAbstract( dd, pNode1->bImage, pNode2->bImage, bCube ); 
+    Cudd_Ref( pNode->bImage );
+    // save the cube
+    if ( bCube != b1 )
+    {
+        pNode->bCube = bCube;   Cudd_Ref( bCube );
+    }
+    return pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the best variable.]
+
+  Description [The variables is the best if the sum of squares of the
+  BDD sizes of the partitions, in which it participates, is the minimum.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bbr_FindBestVariable( DdManager * dd,
+    int nNodes, Bbr_ImageNode_t ** pNodes, 
+    int nVars,  Bbr_ImageVar_t ** pVars )
+{
+    DdNode * bTemp;
+    int iVarBest, v;
+    double CostBest, CostCur;
+
+    CostBest = 100000000000000;
+    iVarBest = -1;
+    for ( v = 0; v < nVars; v++ )
+        if ( pVars[v] )
+        {
+            CostCur = 0;
+            for ( bTemp = pVars[v]->bParts; bTemp != b1; bTemp = cuddT(bTemp) )
+                CostCur += pNodes[bTemp->index]->pPart->nNodes * 
+                           pNodes[bTemp->index]->pPart->nNodes;
+            if ( CostBest > CostCur )
+            {
+                CostBest = CostCur;
+                iVarBest = v;
+            }
+        }
+    return iVarBest;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes two smallest partions that have this var.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_FindBestPartitions( DdManager * dd, DdNode * bParts, 
+    int nNodes, Bbr_ImageNode_t ** pNodes, 
+    int * piNode1, int * piNode2 )
+{
+    DdNode * bTemp;
+    int iPart1, iPart2;
+    int CostMin1, CostMin2, Cost;
+
+    // go through the partitions
+    iPart1 = iPart2 = -1;
+    CostMin1 = CostMin2 = 1000000;
+    for ( bTemp = bParts; bTemp != b1; bTemp = cuddT(bTemp) )
+    {
+        Cost = pNodes[bTemp->index]->pPart->nNodes;
+        if ( CostMin1 > Cost )
+        {
+            CostMin2 = CostMin1;    iPart2 = iPart1;
+            CostMin1 = Cost;        iPart1 = bTemp->index;
+        }
+        else if ( CostMin2 > Cost )
+        {
+            CostMin2 = Cost;        iPart2 = bTemp->index;
+        }
+    }
+
+    *piNode1 = iPart1;
+    *piNode2 = iPart2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the latch dependency matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_bddImagePrintLatchDependency( 
+    DdManager * dd, DdNode * bCare, // the care set
+    int nParts, DdNode ** pbParts,  // the partitions for image computation
+    int nVars, DdNode ** pbVars )   // the NS and parameter variables (not quantified!)
+{
+    int i;
+    DdNode * bVarsCs, * bVarsNs;
+
+    bVarsCs = Cudd_Support( dd, bCare );                       Cudd_Ref( bVarsCs );
+    bVarsNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars );  Cudd_Ref( bVarsNs );
+
+    printf( "The latch dependency matrix:\n" );
+    printf( "Partitions = %d   Variables: total = %d  non-quantifiable = %d\n",
+        nParts, dd->size, nVars );
+    printf( "     : " );
+    for ( i = 0; i < dd->size; i++ )
+        printf( "%d", i % 10 );
+    printf( "\n" );
+
+    for ( i = 0; i < nParts; i++ )
+        Bbr_bddImagePrintLatchDependencyOne( dd, pbParts[i], bVarsCs, bVarsNs, i );
+    Bbr_bddImagePrintLatchDependencyOne( dd, bCare, bVarsCs, bVarsNs, nParts );
+
+    Cudd_RecursiveDeref( dd, bVarsCs );
+    Cudd_RecursiveDeref( dd, bVarsNs );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints one row of the latch dependency matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_bddImagePrintLatchDependencyOne(
+    DdManager * dd, DdNode * bFunc,      // the function
+    DdNode * bVarsCs, DdNode * bVarsNs,  // the current/next state vars
+    int iPart )
+{
+    DdNode * bSupport;
+    int v;
+    bSupport = Cudd_Support( dd, bFunc );  Cudd_Ref( bSupport );
+    printf( " %3d : ", iPart );
+    for ( v = 0; v < dd->size; v++ )
+    {
+        if ( Cudd_bddLeq( dd, bSupport, dd->vars[v] ) )
+        {
+            if ( Cudd_bddLeq( dd, bVarsCs, dd->vars[v] ) )
+                printf( "c" );
+            else if ( Cudd_bddLeq( dd, bVarsNs, dd->vars[v] ) ) 
+                printf( "n" );
+            else
+                printf( "i" );
+        }
+        else
+            printf( "." );
+    }
+    printf( "\n" );
+    Cudd_RecursiveDeref( dd, bSupport );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the tree for quenstification scheduling.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_bddImagePrintTree( Bbr_ImageTree_t * pTree )
+{
+    printf( "The quantification scheduling tree:\n" );
+    Bbr_bddImagePrintTree_rec( pTree->pRoot, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the tree for quenstification scheduling.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_bddImagePrintTree_rec( Bbr_ImageNode_t * pNode, int Offset )
+{
+    DdNode * Cube;
+    int i;
+
+    Cube = pNode->bCube;
+
+    if ( pNode->pNode1 == NULL )
+    {
+        printf( "<%d> ", pNode->pPart->iPart );
+        if ( Cube != NULL )
+        {
+            PRB( pNode->dd, Cube );
+        }
+        else
+            printf( "\n" );
+        return;
+    }
+
+    printf( "<*> " );
+    if ( Cube != NULL )
+    {
+        PRB( pNode->dd, Cube );
+    }
+    else
+        printf( "\n" );
+
+    for ( i = 0; i < Offset; i++ )
+        printf( "    " );
+    Bbr_bddImagePrintTree_rec( pNode->pNode1, Offset + 1 );
+
+    for ( i = 0; i < Offset; i++ )
+        printf( "    " );
+    Bbr_bddImagePrintTree_rec( pNode->pNode2, Offset + 1 );
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Computes the positive polarty cube composed of the first vars in the array.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Bbr_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars )
+{
+    DdNode * bRes;
+    DdNode * bTemp;
+    int i;
+
+    bRes = b1; Cudd_Ref( bRes );
+    for ( i = 0; i < nVars; i++ )
+    {
+        bRes = Cudd_bddAnd( dd, bTemp = bRes, bXVars[i] );  Cudd_Ref( bRes );
+        Cudd_RecursiveDeref( dd, bTemp );
+    }
+
+    Cudd_Deref( bRes );
+    return bRes;
+}
+
+
+
+
+
+struct Bbr_ImageTree2_t_
+{
+    DdManager * dd;
+    DdNode *    bRel;
+    DdNode *    bCube;
+    DdNode *    bImage;
+};
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the monolithic image computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbr_ImageTree2_t * Bbr_bddImageStart2( 
+    DdManager * dd, DdNode * bCare,
+    int nParts, DdNode ** pbParts,
+    int nVars, DdNode ** pbVars, int fVerbose )
+{
+    Bbr_ImageTree2_t * pTree;
+    DdNode * bCubeAll, * bCubeNot, * bTemp;
+    int i;
+
+    pTree = ALLOC( Bbr_ImageTree2_t, 1 );
+    pTree->dd = dd;
+    pTree->bImage = NULL;
+
+    bCubeAll = Bbr_bddComputeCube( dd, dd->vars, dd->size );      Cudd_Ref( bCubeAll );
+    bCubeNot = Bbr_bddComputeCube( dd, pbVars,   nVars );         Cudd_Ref( bCubeNot );
+    pTree->bCube = Cudd_bddExistAbstract( dd, bCubeAll, bCubeNot ); Cudd_Ref( pTree->bCube );
+    Cudd_RecursiveDeref( dd, bCubeAll );
+    Cudd_RecursiveDeref( dd, bCubeNot );
+
+    // derive the monolithic relation
+    pTree->bRel = b1;   Cudd_Ref( pTree->bRel );
+    for ( i = 0; i < nParts; i++ )
+    {
+        pTree->bRel = Cudd_bddAnd( dd, bTemp = pTree->bRel, pbParts[i] ); Cudd_Ref( pTree->bRel );
+        Cudd_RecursiveDeref( dd, bTemp );
+    }
+    Bbr_bddImageCompute2( pTree, bCare );
+    return pTree;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Bbr_bddImageCompute2( Bbr_ImageTree2_t * pTree, DdNode * bCare )
+{
+    if ( pTree->bImage )
+        Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
+    pTree->bImage = Cudd_bddAndAbstract( pTree->dd, pTree->bRel, bCare, pTree->bCube ); 
+    Cudd_Ref( pTree->bImage );
+    return pTree->bImage;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_bddImageTreeDelete2( Bbr_ImageTree2_t * pTree )
+{
+    if ( pTree->bRel )
+        Cudd_RecursiveDeref( pTree->dd, pTree->bRel );
+    if ( pTree->bCube )
+        Cudd_RecursiveDeref( pTree->dd, pTree->bCube );
+    if ( pTree->bImage )
+        Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
+    FREE( pTree );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the previously computed image.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Bbr_bddImageRead2( Bbr_ImageTree2_t * pTree )
+{
+    return pTree->bImage;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/bbr/bbrNtbdd.c b/src/aig/bbr/bbrNtbdd.c
new file mode 100644
index 00000000..5e51a157
--- /dev/null
+++ b/src/aig/bbr/bbrNtbdd.c
@@ -0,0 +1,214 @@
+/**CFile****************************************************************
+
+  FileName    [bbrNtbdd.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD-based reachability analysis.]
+
+  Synopsis    [Procedures to construct global BDDs for the network.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bbrNtbdd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bbr.h"
+//#include "bar.h"
+
+typedef char ProgressBar;
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline void     Aig_ObjSetGlobalBdd( Aig_Obj_t * pObj, DdNode * bFunc )   { pObj->pData = bFunc; }
+static inline void     Aig_ObjCleanGlobalBdd( DdManager * dd, Aig_Obj_t * pObj ) { Cudd_RecursiveDeref( dd, pObj->pData ); pObj->pData = NULL; }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the global BDD for one AIG node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Bbr_NodeGlobalBdds_rec( DdManager * dd, Aig_Obj_t * pNode, int nBddSizeMax, int fDropInternal, ProgressBar * pProgress, int * pCounter, int fVerbose )
+{
+    DdNode * bFunc, * bFunc0, * bFunc1;
+    int fDetectMuxes = 1;
+    assert( !Aig_IsComplement(pNode) );
+    if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )
+    {
+//        Extra_ProgressBarStop( pProgress );
+        if ( fVerbose )
+        printf( "The number of live nodes reached %d.\n", nBddSizeMax );
+        fflush( stdout );
+        return NULL;
+    }
+    // if the result is available return
+    if ( Aig_ObjGlobalBdd(pNode) == NULL )
+    {
+        // compute the result for both branches
+        bFunc0 = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin0(pNode), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
+        if ( bFunc0 == NULL )
+            return NULL;
+        Cudd_Ref( bFunc0 );
+        bFunc1 = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin1(pNode), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
+        if ( bFunc1 == NULL )
+            return NULL;
+        Cudd_Ref( bFunc1 );
+        bFunc0 = Cudd_NotCond( bFunc0, Aig_ObjFaninC0(pNode) );
+        bFunc1 = Cudd_NotCond( bFunc1, Aig_ObjFaninC1(pNode) );
+        // get the final result
+        bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );
+        Cudd_RecursiveDeref( dd, bFunc0 );
+        Cudd_RecursiveDeref( dd, bFunc1 );
+        // add the number of used nodes
+        (*pCounter)++;
+        // set the result
+        assert( Aig_ObjGlobalBdd(pNode) == NULL );
+        Aig_ObjSetGlobalBdd( pNode, bFunc );
+        // increment the progress bar
+//        if ( pProgress )
+//            Extra_ProgressBarUpdate( pProgress, *pCounter, NULL );
+    }
+    // prepare the return value
+    bFunc = Aig_ObjGlobalBdd(pNode);
+    // dereference BDD at the node
+    if ( --pNode->nRefs == 0 && fDropInternal )
+    {
+        Cudd_Deref( bFunc );
+        Aig_ObjSetGlobalBdd( pNode, NULL );
+    }
+    return bFunc;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the global BDDs of the network.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManFreeGlobalBdds( Aig_Man_t * p, DdManager * dd ) 
+{ 
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManForEachObj( p, pObj, i )
+        if ( Aig_ObjGlobalBdd(pObj) )
+            Aig_ObjCleanGlobalBdd( dd, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the shared size of global BDDs of the COs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManSizeOfGlobalBdds( Aig_Man_t * p ) 
+{
+    Vec_Ptr_t * vFuncsGlob;
+    Aig_Obj_t * pObj;
+    int RetValue, i;
+    // complement the global functions
+    vFuncsGlob = Vec_PtrAlloc( Aig_ManPoNum(p) );
+    Aig_ManForEachPo( p, pObj, i )
+        Vec_PtrPush( vFuncsGlob, Aig_ObjGlobalBdd(pObj) );
+    RetValue = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncsGlob), Vec_PtrSize(vFuncsGlob) );
+    Vec_PtrFree( vFuncsGlob );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively computes global BDDs for the AIG in the manager.]
+
+  Description [On exit, BDDs are stored in the pNode->pData fields.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose )
+{
+    ProgressBar * pProgress = NULL;
+    Aig_Obj_t * pObj;
+    DdManager * dd;
+    DdNode * bFunc;
+    int i, Counter;
+    // start the manager
+    dd = Cudd_Init( Aig_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    // set reordering
+    if ( fReorder )
+        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
+    // prepare to construct global BDDs
+    Aig_ManCleanData( p );
+    // assign the constant node BDD
+    Aig_ObjSetGlobalBdd( Aig_ManConst1(p), dd->one );   Cudd_Ref( dd->one );
+    // set the elementary variables
+    Aig_ManForEachPi( p, pObj, i )
+    {
+        Aig_ObjSetGlobalBdd( pObj, dd->vars[i] );  Cudd_Ref( dd->vars[i] );
+    }
+
+    // collect the global functions of the COs
+    Counter = 0;
+    // construct the BDDs
+//    pProgress = Extra_ProgressBarStart( stdout, Aig_ManNodeNum(p) );
+    Aig_ManForEachPo( p, pObj, i )
+    {
+        bFunc = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin0(pObj), nBddSizeMax, fDropInternal, pProgress, &Counter, fVerbose );
+        if ( bFunc == NULL )
+        {
+            if ( fVerbose )
+            printf( "Constructing global BDDs is aborted.\n" );
+            Aig_ManFreeGlobalBdds( p, dd );
+            Cudd_Quit( dd ); 
+            // reset references
+            Aig_ManResetRefs( p );
+            return NULL;
+        }
+        bFunc = Cudd_NotCond( bFunc, Aig_ObjFaninC0(pObj) );  Cudd_Ref( bFunc ); 
+        Aig_ObjSetGlobalBdd( pObj, bFunc );
+    }
+//    Extra_ProgressBarStop( pProgress );
+    // reset references
+    Aig_ManResetRefs( p );
+    // reorder one more time
+    if ( fReorder )
+    {
+        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
+        Cudd_AutodynDisable( dd );
+    }
+//    Cudd_PrintInfo( dd, stdout );
+    return dd;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/bbr/bbrReach.c b/src/aig/bbr/bbrReach.c
new file mode 100644
index 00000000..95bfe1ba
--- /dev/null
+++ b/src/aig/bbr/bbrReach.c
@@ -0,0 +1,414 @@
+/**CFile****************************************************************
+
+  FileName    [bbrReach.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD-based reachability analysis.]
+
+  Synopsis    [Procedures to perform reachability analysis.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bbrReach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bbr.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function********************************************************************
+
+  Synopsis    [Performs the reordering-sensitive step of Extra_bddMove().]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Bbr_bddComputeRangeCube( DdManager * dd, int iStart, int iStop )
+{
+    DdNode * bTemp, * bProd;
+    int i;
+    assert( iStart <= iStop );
+    assert( iStart >= 0 && iStart <= dd->size );
+    assert( iStop >= 0  && iStop  <= dd->size );
+    bProd = (dd)->one;         Cudd_Ref( bProd );
+    for ( i = iStart; i < iStop; i++ )
+    {
+        bProd = Cudd_bddAnd( dd, bTemp = bProd, dd->vars[i] );      Cudd_Ref( bProd );
+        Cudd_RecursiveDeref( dd, bTemp ); 
+    }
+    Cudd_Deref( bProd );
+    return bProd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_StopManager( DdManager * dd )
+{
+    int RetValue;
+    // check for remaining references in the package
+    RetValue = Cudd_CheckZeroRef( dd );
+    if ( RetValue > 0 )
+        printf( "\nThe number of referenced nodes = %d\n\n", RetValue );
+//  Cudd_PrintInfo( dd, stdout );
+    Cudd_Quit( dd );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the initial state and sets up the variable map.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Aig_ManInitStateVarMap( DdManager * dd, Aig_Man_t * p, int fVerbose )
+{
+    DdNode ** pbVarsX, ** pbVarsY;
+    DdNode * bTemp, * bProd;
+    Aig_Obj_t * pLatch;
+    int i;
+
+    // set the variable mapping for Cudd_bddVarMap()
+    pbVarsX = ALLOC( DdNode *, dd->size );
+    pbVarsY = ALLOC( DdNode *, dd->size );
+    bProd = (dd)->one;         Cudd_Ref( bProd );
+    Saig_ManForEachLo( p, pLatch, i )
+    {
+        pbVarsX[i] = dd->vars[ Saig_ManPiNum(p) + i ];
+        pbVarsY[i] = dd->vars[ Saig_ManCiNum(p) + i ];
+        // get the initial value of the latch
+        bProd = Cudd_bddAnd( dd, bTemp = bProd, Cudd_Not(pbVarsX[i]) );      Cudd_Ref( bProd );
+        Cudd_RecursiveDeref( dd, bTemp ); 
+    }
+    Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Saig_ManRegNum(p) );
+    FREE( pbVarsX );
+    FREE( pbVarsY );
+
+    Cudd_Deref( bProd );
+    return bProd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the array of output BDDs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode ** Aig_ManCreateOutputs( DdManager * dd, Aig_Man_t * p )
+{
+    DdNode ** pbOutputs;
+    Aig_Obj_t * pNode;
+    int i;
+    // compute the transition relation
+    pbOutputs = ALLOC( DdNode *, Saig_ManPoNum(p) );
+    Saig_ManForEachPo( p, pNode, i )
+    {
+        pbOutputs[i] = Aig_ObjGlobalBdd(pNode);  Cudd_Ref( pbOutputs[i] );
+    }
+    return pbOutputs;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collects the array of partition BDDs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode ** Aig_ManCreatePartitions( DdManager * dd, Aig_Man_t * p, int fReorder, int fVerbose )
+{
+    DdNode ** pbParts;
+    DdNode * bVar;
+    Aig_Obj_t * pNode;
+    int i;
+
+    // extand the BDD manager to represent NS variables
+    assert( dd->size == Saig_ManCiNum(p) );
+    Cudd_bddIthVar( dd, Saig_ManCiNum(p) + Saig_ManRegNum(p) - 1 );
+
+    // enable reordering
+    if ( fReorder )
+        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
+    else
+        Cudd_AutodynDisable( dd );
+
+    // compute the transition relation
+    pbParts = ALLOC( DdNode *, Saig_ManRegNum(p) );
+    Saig_ManForEachLi( p, pNode, i )
+    {
+        bVar  = Cudd_bddIthVar( dd, Saig_ManCiNum(p) + i );
+        pbParts[i] = Cudd_bddXnor( dd, bVar, Aig_ObjGlobalBdd(pNode) );  Cudd_Ref( pbParts[i] );
+    }
+    // free global BDDs
+    Aig_ManFreeGlobalBdds( p, dd );
+
+    // reorder and disable reordering
+    if ( fReorder )
+    {
+        if ( fVerbose )
+            fprintf( stdout, "BDD nodes in the partitions before reordering %d.\n", Cudd_SharingSize(pbParts,Saig_ManRegNum(p)) );
+        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
+        Cudd_AutodynDisable( dd );
+        if ( fVerbose )
+            fprintf( stdout, "BDD nodes in the partitions after reordering %d.\n", Cudd_SharingSize(pbParts,Saig_ManRegNum(p)) );
+    }
+    return pbParts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the set of unreachable states.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, DdNode * bInitial, DdNode ** pbOutputs, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
+{
+    int fInternalReorder = 0;
+    Bbr_ImageTree_t * pTree;
+    Bbr_ImageTree2_t * pTree2;
+    DdNode * bReached, * bCubeCs;
+    DdNode * bCurrent, * bNext, * bTemp;
+    DdNode ** pbVarsY;
+    Aig_Obj_t * pLatch;
+    int i, nIters, nBddSize;
+    int nThreshold = 10000;
+
+    // collect the NS variables
+    // set the variable mapping for Cudd_bddVarMap()
+    pbVarsY = ALLOC( DdNode *, dd->size );
+    Saig_ManForEachLo( p, pLatch, i )
+        pbVarsY[i] = dd->vars[ Saig_ManCiNum(p) + i ];
+
+    // start the image computation
+    bCubeCs  = Bbr_bddComputeRangeCube( dd, Saig_ManPiNum(p), Saig_ManCiNum(p) );    Cudd_Ref( bCubeCs );
+    if ( fPartition )
+        pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), pbVarsY, fVerbose );
+    else
+        pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), pbVarsY, fVerbose );
+    Cudd_RecursiveDeref( dd, bCubeCs );
+    free( pbVarsY );
+    if ( pTree == NULL )
+    {
+        printf( "BDDs blew up during qualitification scheduling.  " );
+        return -1;
+    }
+
+    // perform reachability analisys
+    bCurrent = bInitial;   Cudd_Ref( bCurrent );
+    bReached = bInitial;   Cudd_Ref( bReached );
+    for ( nIters = 1; nIters <= nIterMax; nIters++ )
+    { 
+        // compute the next states
+        if ( fPartition )
+            bNext = Bbr_bddImageCompute( pTree, bCurrent );           
+        else
+            bNext = Bbr_bddImageCompute2( pTree2, bCurrent );  
+        if ( bNext == NULL )
+        {
+            printf( "BDDs blew up during image computation.  " );
+            if ( fPartition )
+                Bbr_bddImageTreeDelete( pTree );
+            else
+                Bbr_bddImageTreeDelete2( pTree2 );
+            return -1;
+        }
+        Cudd_Ref( bNext );
+        Cudd_RecursiveDeref( dd, bCurrent );
+        // remap these states into the current state vars
+        bNext = Cudd_bddVarMap( dd, bTemp = bNext );                    Cudd_Ref( bNext );
+        Cudd_RecursiveDeref( dd, bTemp );
+        // check if there are any new states
+        if ( Cudd_bddLeq( dd, bNext, bReached ) )
+            break;
+        // check the BDD size
+        nBddSize = Cudd_DagSize(bNext);
+        if ( nBddSize > nBddMax )
+            break;
+        // check the result
+        for ( i = 0; i < Saig_ManPoNum(p); i++ )
+        {
+            if ( !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) )
+            {
+                printf( "Output %d was asserted in frame %d.  ", i, nIters );
+                Cudd_RecursiveDeref( dd, bReached );
+                bReached = NULL;
+                break;
+            }
+        }
+        if ( i < Saig_ManPoNum(p) )
+            break;
+        // get the new states
+        bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) );        Cudd_Ref( bCurrent );
+        // minimize the new states with the reached states
+//        bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
+//        Cudd_RecursiveDeref( dd, bTemp );
+        // add to the reached states
+        bReached = Cudd_bddOr( dd, bTemp = bReached, bNext );           Cudd_Ref( bReached );
+        Cudd_RecursiveDeref( dd, bTemp );
+        Cudd_RecursiveDeref( dd, bNext );
+        if ( fVerbose )
+            fprintf( stdout, "Frame = %3d. BDD = %5d. ", nIters, nBddSize );
+        if ( fInternalReorder && fReorder && nBddSize > nThreshold )
+        {
+            if ( fVerbose )
+                fprintf( stdout, "Reordering... Before = %5d. ", Cudd_DagSize(bReached) );
+            Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
+            Cudd_AutodynDisable( dd );
+            if ( fVerbose )
+                fprintf( stdout, "After = %5d.\r", Cudd_DagSize(bReached) );
+            nThreshold *= 2;
+        }
+        if ( fVerbose )
+            fprintf( stdout, "\r" );
+    }
+    Cudd_RecursiveDeref( dd, bNext );
+    // undo the image tree
+    if ( fPartition )
+        Bbr_bddImageTreeDelete( pTree );
+    else
+        Bbr_bddImageTreeDelete2( pTree2 );
+    if ( bReached == NULL )
+        return 0; // proved reachable
+    // report the stats
+    if ( fVerbose )
+    {
+        double nMints = Cudd_CountMinterm(dd, bReached, Saig_ManRegNum(p) );
+        if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
+            fprintf( stdout, "Reachability analysis is stopped after %d frames.\n", nIters );
+        else
+            fprintf( stdout, "Reachability analysis completed after %d frames.\n", nIters );
+        fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p)) );
+        fflush( stdout );
+    }
+//PRB( dd, bReached );
+    Cudd_RecursiveDeref( dd, bReached );
+    if ( nIters > nIterMax || Cudd_DagSize(bReached) > nBddMax )
+    {
+         printf( "Verified only for states reachable in %d frames.  ", nIters );
+         return -1; // undecided
+    }
+    printf( "The miter is proved unreachable after %d iterations.  ", nIters );
+    return 1; // unreachable
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs reachability to see if any .]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
+{
+    DdManager * dd;
+    DdNode ** pbParts, ** pbOutputs;
+    DdNode * bInitial;
+    int RetValue, i, clk = clock();
+
+    assert( Saig_ManRegNum(p) > 0 );
+
+    // compute the global BDDs of the latches
+    dd = Aig_ManComputeGlobalBdds( p, nBddMax, 1, fReorder, fVerbose );    
+    if ( dd == NULL )
+    {
+        printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", nBddMax );
+        return -1;
+    }
+    if ( fVerbose )
+        printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+
+    // save outputs
+    pbOutputs = Aig_ManCreateOutputs( dd, p );
+
+    // create partitions
+    pbParts = Aig_ManCreatePartitions( dd, p, fReorder, fVerbose );
+
+    // create the initial state and the variable map
+    bInitial  = Aig_ManInitStateVarMap( dd, p, fVerbose );  Cudd_Ref( bInitial );
+
+    // check the result
+    RetValue = -1;
+    for ( i = 0; i < Saig_ManPoNum(p); i++ )
+    {
+        if ( !Cudd_bddLeq( dd, bInitial, Cudd_Not(pbOutputs[i]) ) )
+        {
+            printf( "The miter output %d is proved REACHABLE in the initial state.  ", i );
+            RetValue = 0;
+            break;
+        }
+    }
+    // explore reachable states
+    if ( RetValue == -1 )
+        RetValue = Aig_ManComputeReachable( dd, p, pbParts, bInitial, pbOutputs, nBddMax, nIterMax, fPartition, fReorder, fVerbose ); 
+
+    // cleanup
+    Cudd_RecursiveDeref( dd, bInitial );
+    for ( i = 0; i < Saig_ManRegNum(p); i++ )
+        Cudd_RecursiveDeref( dd, pbParts[i] );
+    free( pbParts );
+    for ( i = 0; i < Saig_ManPoNum(p); i++ )
+        Cudd_RecursiveDeref( dd, pbOutputs[i] );
+    free( pbOutputs );
+    if ( RetValue == -1 )
+        Cudd_Quit( dd );
+    else
+        Bbr_StopManager( dd );
+
+    // report the runtime
+    PRT( "Time", clock() - clk );
+    fflush( stdout );
+    return RetValue;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/bbr/bbr_.c b/src/aig/bbr/bbr_.c
new file mode 100644
index 00000000..f94c50e6
--- /dev/null
+++ b/src/aig/bbr/bbr_.c
@@ -0,0 +1,47 @@
+/**CFile****************************************************************
+
+  FileName    [.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName []
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: .c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "__Int.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/bbr/module.make b/src/aig/bbr/module.make
new file mode 100644
index 00000000..52a824b9
--- /dev/null
+++ b/src/aig/bbr/module.make
@@ -0,0 +1,3 @@
+SRC +=    src/aig/bbr/bbrImage.c \
+    src/aig/bbr/bbrNtbdd.c \
+    src/aig/bdr/bbrReach.c
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index 7c2b95db..44cfe847 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -328,7 +328,7 @@ extern int                 Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig
 extern int                 Fra_NodesAreClause( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
 extern int                 Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
 /*=== fraSec.c ========================================================*/
-extern int                 Fra_FraigSec( Aig_Man_t * p, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose );
+extern int                 Fra_FraigSec( Aig_Man_t * p, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose );
 /*=== fraSim.c ========================================================*/
 extern int                 Fra_SmlNodeHash( Aig_Obj_t * pObj, int nTableSize );
 extern int                 Fra_SmlNodeIsConst( Aig_Obj_t * pObj );
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 99d4bc89..64222a47 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -40,7 +40,7 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose )
+int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose )
 {
     Fra_Ssw_t Pars, * pPars = &Pars;
     Fra_Sml_t * pSml;
@@ -79,6 +79,23 @@ clk = clock();
 PRT( "Time", clock() - clk );
     }
 
+    // perform phase abstraction
+clk = clock();
+    if ( fPhaseAbstract )
+    {
+        extern Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose );
+        pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew = Saig_ManPhaseAbstractAuto( pTemp = pNew, 0 );
+        Aig_ManStop( pTemp );
+        if ( fVerbose )
+        {
+            printf( "Phase abstraction:    Latches = %5d. Nodes = %6d. ", 
+                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+        }
+    }
+
     // perform forward retiming
     if ( fRetimeFirst && pNew->nRegs )
     {
@@ -133,6 +150,26 @@ PRT( "Time", clock() - clk );
     }
     }
 
+    // perform min-area retiming
+    if ( fRetimeRegs && pNew->nRegs )
+    {
+    extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
+clk = clock();
+    pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
+    pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
+//        pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
+    pNew = Saig_ManRetimeMinArea( pTemp = pNew, 1000, 0, 0, 1, 0 );
+    Aig_ManStop( pTemp );
+    pNew = Aig_ManDupOrdered( pTemp = pNew );
+    Aig_ManStop( pTemp );
+    if ( fVerbose )
+    {
+    printf( "Min-reg retiming:     Latches = %5d. Nodes = %6d. ", 
+        Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+    }
+    }
+
     // perform seq sweeping while increasing the number of frames
     RetValue = Fra_FraigMiterStatus( pNew );
     if ( RetValue == -1 )
@@ -152,31 +189,22 @@ PRT( "Time", clock() - clk );
         if ( RetValue != -1 )
             break;
 
-        // perform rewriting
-clk = clock();
-        pNew = Aig_ManDupOrdered( pTemp = pNew );
-        Aig_ManStop( pTemp );
-        pNew = Dar_ManRewriteDefault( pTemp = pNew );
-        Aig_ManStop( pTemp );
-        if ( fVerbose )
-        {
-            printf( "Rewriting:            Latches = %5d. Nodes = %6d. ", 
-                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
-PRT( "Time", clock() - clk );
-        } 
-
         // perform retiming
-        if ( fRetimeFirst && pNew->nRegs )
-//        if ( pNew->nRegs )
+//        if ( fRetimeFirst && pNew->nRegs )
+        if ( pNew->nRegs )
         {
+        extern Aig_Man_t * Saig_ManRetimeMinArea( Aig_Man_t * p, int nMaxIters, int fForwardOnly, int fBackwardOnly, int fInitial, int fVerbose );
 clk = clock();
-        pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
+        pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
+//        pNew = Rtm_ManRetime( pTemp = pNew, 1, 1000, 0 );
+        pNew = Saig_ManRetimeMinArea( pTemp = pNew, 1000, 0, 0, 1, 0 );
         Aig_ManStop( pTemp );
         pNew = Aig_ManDupOrdered( pTemp = pNew );
         Aig_ManStop( pTemp );
         if ( fVerbose )
         {
-            printf( "Forward retiming:     Latches = %5d. Nodes = %6d. ", 
+            printf( "Min-reg retiming:     Latches = %5d. Nodes = %6d. ", 
                 Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
 PRT( "Time", clock() - clk );
         }
@@ -185,6 +213,20 @@ PRT( "Time", clock() - clk );
         if ( pNew->nRegs )
             pNew = Aig_ManConstReduce( pNew, 0 );
 
+        // perform rewriting
+clk = clock();
+        pNew = Aig_ManDupOrdered( pTemp = pNew );
+        Aig_ManStop( pTemp );
+//        pNew = Dar_ManRewriteDefault( pTemp = pNew );
+        pNew = Dar_ManCompress2( pTemp = pNew, 1, 0, 1, 0 ); 
+        Aig_ManStop( pTemp );
+        if ( fVerbose )
+        {
+            printf( "Rewriting:            Latches = %5d. Nodes = %6d. ", 
+                Aig_ManRegNum(pNew), Aig_ManNodeNum(pNew) );
+PRT( "Time", clock() - clk );
+        } 
+
         // perform sequential simulation
         if ( pNew->nRegs )
         {
@@ -213,6 +255,18 @@ PRT( "Time", clock() - clkTotal );
     // get the miter status
     RetValue = Fra_FraigMiterStatus( pNew );
 
+    // try reachability analysis
+    if ( RetValue == -1 && Aig_ManRegNum(pNew) < 200 )
+    {
+        extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
+        assert( Aig_ManRegNum(pNew) > 0 );
+        pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
+        pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
+clk = clock();
+        RetValue = Aig_ManVerifyUsingBdds( pNew, 100000, 1000, 1, 1, 0 );
+PRT( "Time", clock() - clk );
+    }
+
 finish:
     // report the miter
     if ( RetValue == 1 )
diff --git a/src/aig/hop/hop.h b/src/aig/hop/hop.h
index 12374a49..05e6471e 100644
--- a/src/aig/hop/hop.h
+++ b/src/aig/hop/hop.h
@@ -188,7 +188,7 @@ static inline Hop_Obj_t *  Hop_ObjChild0Copy( Hop_Obj_t * pObj ) { assert( !Hop_
 static inline Hop_Obj_t *  Hop_ObjChild1Copy( Hop_Obj_t * pObj ) { assert( !Hop_IsComplement(pObj) ); return Hop_ObjFanin1(pObj)? Hop_NotCond((Hop_Obj_t *)Hop_ObjFanin1(pObj)->pData, Hop_ObjFaninC1(pObj)) : NULL;  }
 static inline int          Hop_ObjLevel( Hop_Obj_t * pObj )       { return pObj->nRefs;                            }
 static inline int          Hop_ObjLevelNew( Hop_Obj_t * pObj )    { return 1 + Hop_ObjIsExor(pObj) + AIG_MAX(Hop_ObjFanin0(pObj)->nRefs, Hop_ObjFanin1(pObj)->nRefs);       }
-static inline int          Hop_ObjFaninPhase( Hop_Obj_t * pObj )  { return Hop_IsComplement(pObj)? !Hop_Regular(pObj)->fPhase : pObj->fPhase; }
+static inline int          Hop_ObjPhaseCompl( Hop_Obj_t * pObj )  { return Hop_IsComplement(pObj)? !Hop_Regular(pObj)->fPhase : pObj->fPhase; }
 static inline void         Hop_ObjClean( Hop_Obj_t * pObj )       { memset( pObj, 0, sizeof(Hop_Obj_t) ); }
 static inline int          Hop_ObjWhatFanin( Hop_Obj_t * pObj, Hop_Obj_t * pFanin )    
 { 
@@ -284,6 +284,7 @@ extern int             Hop_DagSize( Hop_Obj_t * pObj );
 extern void            Hop_ConeUnmark_rec( Hop_Obj_t * pObj );
 extern Hop_Obj_t *     Hop_Transfer( Hop_Man_t * pSour, Hop_Man_t * pDest, Hop_Obj_t * pObj, int nVars );
 extern Hop_Obj_t *     Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, int iVar );
+extern Hop_Obj_t *     Hop_Remap( Hop_Man_t * p, Hop_Obj_t * pRoot, unsigned uSupp, int nVars );
 /*=== hopMan.c ==========================================================*/
 extern Hop_Man_t *     Hop_ManStart();
 extern Hop_Man_t *     Hop_ManDup( Hop_Man_t * p );
diff --git a/src/aig/hop/hopDfs.c b/src/aig/hop/hopDfs.c
index 49e5f221..d798bc35 100644
--- a/src/aig/hop/hopDfs.c
+++ b/src/aig/hop/hopDfs.c
@@ -392,6 +392,74 @@ Hop_Obj_t * Hop_Compose( Hop_Man_t * p, Hop_Obj_t * pRoot, Hop_Obj_t * pFunc, in
     return Hop_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Hop_Remap_rec( Hop_Man_t * p, Hop_Obj_t * pObj )
+{
+    assert( !Hop_IsComplement(pObj) );
+    if ( !Hop_ObjIsNode(pObj) || Hop_ObjIsMarkA(pObj) )
+        return;
+    Hop_Remap_rec( p, Hop_ObjFanin0(pObj) ); 
+    Hop_Remap_rec( p, Hop_ObjFanin1(pObj) );
+    pObj->pData = Hop_And( p, Hop_ObjChild0Copy(pObj), Hop_ObjChild1Copy(pObj) );
+    assert( !Hop_ObjIsMarkA(pObj) ); // loop detection
+    Hop_ObjSetMarkA( pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Composes the AIG (pRoot) with the function (pFunc) using PI var (iVar).]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Hop_Obj_t * Hop_Remap( Hop_Man_t * p, Hop_Obj_t * pRoot, unsigned uSupp, int nVars )
+{
+    Hop_Obj_t * pObj;
+    int i, k;
+    // quit if the PI variable is not defined
+    if ( nVars > Hop_ManPiNum(p) )
+    {
+        printf( "Hop_Remap(): The number of variables (%d) is more than the manager size (%d).\n", nVars, Hop_ManPiNum(p) );
+        return NULL;
+    }
+    // return if constant
+    if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
+        return pRoot;
+    if ( uSupp == 0 )
+        return Hop_NotCond( Hop_ManConst0(p), Hop_ObjPhaseCompl(pRoot) );
+    // set the PI mapping
+    k = 0;
+    Hop_ManForEachPi( p, pObj, i )
+    {
+        if ( i == nVars )
+           break;
+        if ( uSupp & (1 << i) )
+            pObj->pData = Hop_IthVar(p, k++);
+        else
+            pObj->pData = Hop_ManConst0(p);
+    }
+    assert( k > 0 && k < nVars );
+    // recursively perform composition
+    Hop_Remap_rec( p, Hop_Regular(pRoot) );
+    // clear the markings
+    Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
+    return Hop_NotCond( Hop_Regular(pRoot)->pData, Hop_IsComplement(pRoot) );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/hop/hopObj.c b/src/aig/hop/hopObj.c
index c8e70dd3..69f63ee6 100644
--- a/src/aig/hop/hopObj.c
+++ b/src/aig/hop/hopObj.c
@@ -73,7 +73,7 @@ Hop_Obj_t * Hop_ObjCreatePo( Hop_Man_t * p, Hop_Obj_t * pDriver )
     else
         pObj->nRefs = Hop_ObjLevel( Hop_Regular(pDriver) );
     // set the phase
-    pObj->fPhase = Hop_ObjFaninPhase(pDriver);
+    pObj->fPhase = Hop_ObjPhaseCompl(pDriver);
     // update node counters of the manager
     p->nObjs[AIG_PO]++;
     return pObj;
@@ -136,7 +136,7 @@ void Hop_ObjConnect( Hop_Man_t * p, Hop_Obj_t * pObj, Hop_Obj_t * pFan0, Hop_Obj
     else
         pObj->nRefs = Hop_ObjLevelNew( pObj );
     // set the phase
-    pObj->fPhase = Hop_ObjFaninPhase(pFan0) & Hop_ObjFaninPhase(pFan1);
+    pObj->fPhase = Hop_ObjPhaseCompl(pFan0) & Hop_ObjPhaseCompl(pFan1);
     // add the node to the structural hash table
     Hop_TableInsert( p, pObj );
 }
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index 659f6c60..55581026 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -52,7 +52,7 @@ typedef enum {
     NTL_OBJ_NONE,                      // 0: non-existent object
     NTL_OBJ_PI,                        // 1: primary input
     NTL_OBJ_PO,                        // 2: primary output
-    NTL_OBJ_LATCH,                     // 3: latch node
+    NTL_OBJ_LATCH,                     // 3: latch 
     NTL_OBJ_NODE,                      // 4: logic node
     NTL_OBJ_LUT1,                      // 5: inverter/buffer
     NTL_OBJ_BOX,                       // 6: white box or black box
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index 767ea6e4..a723c981 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -76,6 +76,8 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
         if ( Aig_ObjIsPo(pObj) )
             continue;
         pObjCol = pObj->pData;
+        if ( pObjCol == NULL )
+            continue;
         if ( pMapBack[pObjCol->Id] == NULL )
             pMapBack[pObjCol->Id] = pObj;
     }
@@ -89,6 +91,8 @@ Aig_Obj_t ** Ntl_ManFraigDeriveClasses( Aig_Man_t * pAig, Ntl_Man_t * pNew, Aig_
             continue;
         // get the collapsed node
         pObjCol = pObj->pData;
+        if ( pObjCol == NULL )
+            continue;
         // get the representative of the collapsed node
         pObjColRepr = pAigCol->pReprs[pObjCol->Id];
         if ( pObjColRepr == NULL )
diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c
index 3e9f82d6..3cd9470b 100644
--- a/src/aig/ntl/ntlInsert.c
+++ b/src/aig/ntl/ntlInsert.c
@@ -82,6 +82,8 @@ Ntl_Man_t * Ntl_ManInsertMapping( Ntl_Man_t * p, Vec_Ptr_t * vMapping, Aig_Man_t
                 Ntl_ObjSetFanin( pNode, pNet, k );
             }
         }
+        else
+            pNode->nFanins = 0;
         sprintf( Buffer, "lut%0*d", nDigits, i );
         if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
         {
@@ -302,6 +304,8 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
                 Ntl_ObjSetFanin( pNode, pNet, k );
             }
         }
+        else
+            pNode->nFanins = 0;
         sprintf( Buffer, "lut%0*d", nDigits, i );
         if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
         {
@@ -341,13 +345,16 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
         if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
         {
             printf( "Ntl_ManInsertNtk(): Internal error: PO net has more than one fanin.\n" );
-            return 0;
+            return NULL;
         }
     }
     // clean CI/CO marks
     Ntl_ManUnmarkCiCoNets( p );
     if ( !Ntl_ManCheck( p ) )
+    {
         printf( "Ntl_ManInsertNtk: The check has failed for design %s.\n", p->pName );
+        return NULL;
+    }
     return p;
 }
 
diff --git a/src/aig/ntl/ntlObj.c b/src/aig/ntl/ntlObj.c
index c86ab47b..10bfbbb7 100644
--- a/src/aig/ntl/ntlObj.c
+++ b/src/aig/ntl/ntlObj.c
@@ -103,7 +103,7 @@ Ntl_Obj_t * Ntl_ModelCreateLatch( Ntl_Mod_t * pModel )
     Vec_PtrPush( pModel->vObjs, p );
     p->pModel   = pModel;
     p->Type     = NTL_OBJ_LATCH;
-    p->nFanins  = 2;
+    p->nFanins  = 1;
     p->nFanouts = 1;
     pModel->nObjs[NTL_OBJ_LATCH]++;
     return p;
diff --git a/src/aig/ntl/ntlReadBlif.c b/src/aig/ntl/ntlReadBlif.c
index cac53058..3574b61e 100644
--- a/src/aig/ntl/ntlReadBlif.c
+++ b/src/aig/ntl/ntlReadBlif.c
@@ -825,7 +825,7 @@ static int Ioa_ReadParseLineLatch( Ioa_ReadMod_t * p, char * pLine )
     {
         pToken = Vec_PtrEntry(vTokens,Vec_PtrSize(vTokens)-2);
         pNetLi = Ntl_ModelFindOrCreateNet( p->pNtk, pToken );
-        pObj->pFanio[1] = pNetLi;
+//        pObj->pFanio[1] = pNetLi;
     }
     return 1;
 }
diff --git a/src/aig/ntl/ntlWriteBlif.c b/src/aig/ntl/ntlWriteBlif.c
index 9814ed5d..51d41c26 100644
--- a/src/aig/ntl/ntlWriteBlif.c
+++ b/src/aig/ntl/ntlWriteBlif.c
@@ -28,7 +28,7 @@
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
-
+ 
 /**Function*************************************************************
 
   Synopsis    [Writes one model into the BLIF file.]
diff --git a/src/aig/nwk/nwk.h b/src/aig/nwk/nwk.h
index c36f3498..b0edd243 100644
--- a/src/aig/nwk/nwk.h
+++ b/src/aig/nwk/nwk.h
@@ -285,6 +285,7 @@ extern void            Nwk_ObjPrint( Nwk_Obj_t * pObj );
 extern void            Nwk_ManDumpBlif( Nwk_Man_t * pNtk, char * pFileName, Vec_Ptr_t * vCiNames, Vec_Ptr_t * vCoNames );
 extern void            Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk );
 extern void            Nwk_ManCleanMarks( Nwk_Man_t * pNtk );
+extern void            Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/nwk/nwkMap.c b/src/aig/nwk/nwkMap.c
index 45d56eb5..88e08413 100644
--- a/src/aig/nwk/nwkMap.c
+++ b/src/aig/nwk/nwkMap.c
@@ -146,7 +146,7 @@ If_Man_t * Nwk_ManToIf( Aig_Man_t * p, If_Par_t * pPars, Vec_Ptr_t * vAigToIf )
 
 /**Function*************************************************************
 
-  Synopsis    [Recursively derives the truth table for the cut.]
+  Synopsis    [Recursively derives the local AIG for the cut.]
 
   Description []
                
@@ -193,7 +193,7 @@ Hop_Obj_t * Nwk_NodeIfToHop2_rec( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj
 
 /**Function*************************************************************
 
-  Synopsis    [Derives the truth table for one cut.]
+  Synopsis    [Derives the local AIG for the cut.]
 
   Description []
                
@@ -309,6 +309,7 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToI
     }
     Vec_PtrFree( vIfToAig );
     pNtk->pManTime = Tim_ManDup( pIfMan->pManTim, 0 );
+    Nwk_ManMinimumBase( pNtk, 0 );
     assert( Nwk_ManCheck( pNtk ) );
     return pNtk;
 }
diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c
index 1ef0af67..14f7632f 100644
--- a/src/aig/nwk/nwkUtil.c
+++ b/src/aig/nwk/nwkUtil.c
@@ -56,7 +56,7 @@ void Nwk_ManIncrementTravId( Nwk_Man_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [Reads the maximum number of fanins.]
+  Synopsis    [Reads the maximum number of fanins of a node.]
 
   Description []
                
@@ -100,7 +100,7 @@ int Nwk_ManGetTotalFanins( Nwk_Man_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Returns the number of true PIs.]
 
   Description []
                
@@ -120,7 +120,7 @@ int Nwk_ManPiNum( Nwk_Man_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Returns the number of true POs.]
 
   Description []
                
@@ -140,7 +140,7 @@ int Nwk_ManPoNum( Nwk_Man_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    [Reads the number of BDD nodes.]
+  Synopsis    [Reads the number of AIG nodes.]
 
   Description []
                
@@ -211,7 +211,7 @@ int Nwk_NodeCompareLevelsDecrease( Nwk_Obj_t ** pp1, Nwk_Obj_t ** pp2 )
 
 /**Function*************************************************************
 
-  Synopsis    [Deletes the node.]
+  Synopsis    [Prints the objects.]
 
   Description []
                
@@ -242,7 +242,7 @@ void Nwk_ObjPrint( Nwk_Obj_t * pObj )
 
 /**Function*************************************************************
 
-  Synopsis    [Deletes the node.]
+  Synopsis    [Dumps the BLIF file for the network.]
 
   Description []
                
@@ -449,7 +449,7 @@ void Nwk_ManPrintFanioNew( Nwk_Man_t * pNtk )
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Cleans the temporary marks of the nodes.]
 
   Description []
                
@@ -466,6 +466,48 @@ void Nwk_ManCleanMarks( Nwk_Man_t * pMan )
         pObj->MarkA = pObj->MarkB = 0;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Minimizes the support of all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose )
+{
+    unsigned * pTruth;
+    Vec_Int_t * vTruth;
+    Nwk_Obj_t * pObj, * pFanin, * pObjNew;
+    int uSupp, nSuppSize, i, k, Counter = 0;
+    vTruth = Vec_IntAlloc( 1 << 16 );
+    Nwk_ManForEachNode( pNtk, pObj, i )
+    {
+        pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 );
+        nSuppSize = Kit_TruthSupportSize(pTruth, Nwk_ObjFaninNum(pObj));
+        if ( nSuppSize == Nwk_ObjFaninNum(pObj) )
+            continue;
+        Counter++;
+        uSupp = Kit_TruthSupport( pTruth, Nwk_ObjFaninNum(pObj) );
+        // create new node with the given support
+        pObjNew = Nwk_ManCreateNode( pNtk, nSuppSize, Nwk_ObjFanoutNum(pObj) );
+        Nwk_ObjForEachFanin( pObj, pFanin, k )
+            if ( uSupp & (1 << k) )
+                Nwk_ObjAddFanin( pObjNew, pFanin );
+        pObjNew->pFunc = Hop_Remap( pNtk->pManHop, pObj->pFunc, uSupp, Nwk_ObjFaninNum(pObj) );
+        if ( fVerbose )
+            printf( "Reducing node %d fanins from %d to %d.\n", 
+                pObj->Id, Nwk_ObjFaninNum(pObj), Nwk_ObjFaninNum(pObjNew) );
+        Nwk_ObjReplace( pObj, pObjNew );
+    }
+    if ( fVerbose && Counter )
+        printf( "Support minimization reduced support of %d nodes.\n", Counter );
+    Vec_IntFree( vTruth );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index e399b8bb..f9677cb0 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -45,6 +45,8 @@ extern "C" {
 
 static inline int          Saig_ManPiNum( Aig_Man_t * p )          { return p->nTruePis;                     }
 static inline int          Saig_ManPoNum( Aig_Man_t * p )          { return p->nTruePos;                     }
+static inline int          Saig_ManCiNum( Aig_Man_t * p )          { return p->nTruePis + p->nRegs;          }
+static inline int          Saig_ManCoNum( Aig_Man_t * p )          { return p->nTruePos + p->nRegs;          }
 static inline int          Saig_ManRegNum( Aig_Man_t * p )         { return p->nRegs;                        }
 static inline Aig_Obj_t *  Saig_ManLo( Aig_Man_t * p, int i )      { return (Aig_Obj_t *)Vec_PtrEntry(p->vPis, Saig_ManPiNum(p)+i);   }
 static inline Aig_Obj_t *  Saig_ManLi( Aig_Man_t * p, int i )      { return (Aig_Obj_t *)Vec_PtrEntry(p->vPos, Saig_ManPoNum(p)+i);   }
diff --git a/src/aig/saig/saigPhase.c b/src/aig/saig/saigPhase.c
index fc00ce3c..f98bb49b 100644
--- a/src/aig/saig/saigPhase.c
+++ b/src/aig/saig/saigPhase.c
@@ -800,7 +800,7 @@ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrame
         printf( "Print-out finished. Phase assignment is not performed.\n" );
     else if ( nFrames < 2 )
         printf( "The number of frames is less than 2. Phase assignment is not performed.\n" );
-    else if ( pTsi->nCycle == 0 )
+    else if ( pTsi->nCycle == 1 )
         printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" );
     else if ( pTsi->nCycle % nFrames != 0 )
         printf( "The cycle (%d) is not modulo the number of frames (%d). Phase abstraction cannot be done.\n", pTsi->nCycle, nFrames );
@@ -814,6 +814,75 @@ Aig_Man_t * Saig_ManPhaseAbstract( Aig_Man_t * p, Vec_Int_t * vInits, int nFrame
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs automated phase abstraction.]
+
+  Description [Takes the AIG manager and the array of initial states.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Saig_ManPhaseAbstractAuto( Aig_Man_t * p, int fVerbose )
+{
+    Aig_Man_t * pNew = NULL;
+    Saig_Tsim_t * pTsi;
+    int fPrint = 0;
+    int nFrames;
+    assert( Saig_ManRegNum(p) );
+    assert( Saig_ManPiNum(p) );
+    assert( Saig_ManPoNum(p) );
+    // perform terminary simulation
+    pTsi = Saig_ManReachableTernary( p, NULL );
+    if ( pTsi == NULL )
+        return NULL;
+    // derive information
+    pTsi->nPrefix = Saig_TsiComputePrefix( pTsi, Vec_PtrEntryLast(pTsi->vStates), pTsi->nWords );
+    pTsi->nCycle = Vec_PtrSize(pTsi->vStates) - 1 - pTsi->nPrefix;
+    pTsi->nNonXRegs = Saig_TsiCountNonXValuedRegisters(pTsi, pTsi->nWords);
+    // print statistics
+    if ( fVerbose )
+    {
+        printf( "Prefix = %5d. Cycle = %5d.  Total = %5d. Non-ternary = %5d.\n", 
+            pTsi->nPrefix, pTsi->nCycle, p->nRegs, pTsi->nNonXRegs );
+        if ( pTsi->nNonXRegs < 100 )
+            Saig_TsiPrintTraces( pTsi, pTsi->nWords, pTsi->nPrefix );
+    }
+    nFrames = pTsi->nCycle;
+    if ( fPrint )
+    {
+        printf( "Print-out finished. Phase assignment is not performed.\n" );
+    }
+    else if ( nFrames < 2 )
+    {
+//        printf( "The number of frames is less than 2. Phase assignment is not performed.\n" );
+    }
+    else if ( pTsi->nCycle == 1 )
+    {
+//        printf( "The cycle of ternary states is trivial. Phase abstraction cannot be done.\n" );
+    }
+    else if ( pTsi->nCycle % nFrames != 0 )
+    {
+//        printf( "The cycle (%d) is not modulo the number of frames (%d). Phase abstraction cannot be done.\n", pTsi->nCycle, nFrames );
+    }
+    else if ( pTsi->nNonXRegs == 0 )
+    {
+//        printf( "All registers have X-valued states. Phase abstraction cannot be done.\n" );
+    }
+    else if ( !Saig_ManFindRegisters( pTsi, nFrames, 0, fVerbose ) )
+    {
+//        printf( "There is no registers to abstract with %d frames.\n", nFrames );
+    }
+    else
+        pNew = Saig_ManPerformAbstraction( pTsi, nFrames, fVerbose );
+    Saig_TsiStop( pTsi );
+    if ( pNew == NULL )
+        pNew = Aig_ManDup( p );
+    return pNew;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 1e33daa6..9b3ec291 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -5618,6 +5618,7 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fVerbose;
     int c;
     extern void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
+    extern void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -5686,12 +5687,22 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Reachability analysis works only for AIGs (run \"strash\").\n" );
         return 1;
     }
+/*
+    if ( Abc_NtkLatchNum(pNtk) > 60 || Abc_NtkNodeNum(pNtk) > 3000 )
+    {
+        fprintf( stdout, "The number of latches %d and nodes %d. Skippping...\n", Abc_NtkLatchNum(pNtk), Abc_NtkNodeNum(pNtk) );
+        return 0;
+    }
+*/
+/*
     if ( Abc_NtkPoNum(pNtk) != 1 )
     {
         fprintf( stdout, "The sequential miter has more than one output (run \"orpos\").\n" );
         return 1;
     }
-    Abc_NtkVerifyUsingBdds( pNtk, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
+*/
+//    Abc_NtkVerifyUsingBdds( pNtk, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
+    Abc_NtkDarReach( pNtk, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
     return 0;
 
 usage:
@@ -13804,34 +13815,38 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fDelete1, fDelete2;
     char ** pArgvNew;
     int nArgcNew;
-    int c;
+    int nFrames;
+    int fPhaseAbstract;
     int fRetimeFirst;
+    int fRetimeRegs;
     int fFraiging;
     int fVerbose;
     int fVeryVerbose;
-    int nFrames;
+    int c;
 
-    extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose );
+    extern int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFrames      = 16;
-    fRetimeFirst =  1;
-    fFraiging    =  1;
-    fVerbose     =  0;
-    fVeryVerbose =  0;
+    nFrames        = 16;
+    fPhaseAbstract =  1;
+    fRetimeFirst   =  1;
+    fRetimeRegs    =  1;
+    fFraiging      =  1;
+    fVerbose       =  0;
+    fVeryVerbose   =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Krfwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Farmfwvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'K':
+        case 'F':
             if ( globalUtilOptind >= argc )
             {
-                fprintf( pErr, "Command line switch \"-K\" should be followed by an integer.\n" );
+                fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
                 goto usage;
             }
             nFrames = atoi(argv[globalUtilOptind]);
@@ -13839,9 +13854,15 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nFrames < 0 ) 
                 goto usage;
             break;
+        case 'a':
+            fPhaseAbstract ^= 1;
+            break;
         case 'r':
             fRetimeFirst ^= 1;
             break;
+        case 'm':
+            fRetimeRegs ^= 1;
+            break;
         case 'f':
             fFraiging ^= 1;
             break;
@@ -13868,17 +13889,19 @@ int Abc_CommandDSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // perform verification
-    Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose );
+    Abc_NtkDarSec( pNtk1, pNtk2, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose );
 
     if ( fDelete1 ) Abc_NtkDelete( pNtk1 );
     if ( fDelete2 ) Abc_NtkDelete( pNtk2 );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dsec [-K num] [-rfwvh] <file1> <file2>\n" );
+    fprintf( pErr, "usage: dsec [-F num] [-armfwvh] <file1> <file2>\n" );
     fprintf( pErr, "\t         performs inductive sequential equivalence checking\n" );
-    fprintf( pErr, "\t-K num : the limit on the depth of induction [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-a     : toggles the use of phase abstraction [default = %s]\n", fPhaseAbstract? "yes": "no" );
     fprintf( pErr, "\t-r     : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
+    fprintf( pErr, "\t-m     : toggles min-register retiming [default = %s]\n", fRetimeRegs? "yes": "no" );
     fprintf( pErr, "\t-f     : toggles the internal use of fraiging [default = %s]\n", fFraiging? "yes": "no" );
     fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w     : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
@@ -13905,27 +13928,31 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
-    int c;
+    int nFrames;
+    int fPhaseAbstract;
     int fRetimeFirst;
+    int fRetimeRegs;
     int fFraiging;
     int fVerbose;
     int fVeryVerbose;
-    int nFrames;
+    int c;
 
-    extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose );
+    extern int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nFrames      = 16; 
-    fRetimeFirst =  1;
-    fFraiging    =  1;
-    fVerbose     =  0;
-    fVeryVerbose =  0;
+    nFrames        =  8; 
+    fPhaseAbstract =  1;
+    fRetimeFirst   =  1;
+    fRetimeRegs    =  1;
+    fFraiging      =  1;
+    fVerbose       =  0;
+    fVeryVerbose   =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Frfwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Farmfwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -13940,9 +13967,15 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nFrames < 0 ) 
                 goto usage;
             break;
+        case 'a':
+            fPhaseAbstract ^= 1;
+            break;
         case 'r':
             fRetimeFirst ^= 1;
             break;
+        case 'm':
+            fRetimeRegs ^= 1;
+            break;
         case 'f':
             fFraiging ^= 1;
             break;
@@ -13959,7 +13992,8 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( Abc_NtkLatchNum(pNtk) == 0 )
     {
-        printf( "The network has no latches. Used combinational command \"iprove\".\n" );
+        printf( "The network has no latches. Running combinational command \"iprove\".\n" );
+        Cmd_CommandExecute( pAbc, "orpos; st; iprove" );
         return 0;
     }
     if ( !Abc_NtkIsStrash(pNtk) )
@@ -13969,14 +14003,16 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // perform verification
-    Abc_NtkDarProve( pNtk, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose );
+    Abc_NtkDarProve( pNtk, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dprove [-F num] [-rfwvh]\n" );
+    fprintf( pErr, "usage: dprove [-F num] [-armfwvh]\n" );
     fprintf( pErr, "\t         performs SEC on the sequential miter\n" );
     fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", nFrames );
+    fprintf( pErr, "\t-a     : toggles the use of phase abstraction [default = %s]\n", fPhaseAbstract? "yes": "no" );
     fprintf( pErr, "\t-r     : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
+    fprintf( pErr, "\t-m     : toggles min-register retiming [default = %s]\n", fRetimeRegs? "yes": "no" );
     fprintf( pErr, "\t-f     : toggles the internal use of fraiging [default = %s]\n", fFraiging? "yes": "no" );
     fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w     : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
@@ -17283,31 +17319,34 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     Aig_Man_t * pAig;
     char ** pArgvNew;
     int nArgcNew;
-    int c;
+    int nFrames;
+    int fPhaseAbstract;
     int fRetimeFirst;
+    int fRetimeRegs;
     int fFraiging;
     int fVerbose;
     int fVeryVerbose;
-    int nFrames;
+    int c;
 
-    extern int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose );
+    extern int Fra_FraigSec( Aig_Man_t * p, int nFramesMax, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose );
     extern Aig_Man_t * Ntl_ManPrepareSec( char * pFileName1, char * pFileName2 );
 
     // set defaults
     nFrames      = 16;
     fRetimeFirst =  0;
+    fRetimeRegs  =  0;
     fFraiging    =  1;
     fVerbose     =  0;
     fVeryVerbose =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Krfwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Farmfwvh" ) ) != EOF )
     {
         switch ( c )
         {
-        case 'K':
+        case 'F':
             if ( globalUtilOptind >= argc )
             {
-                fprintf( stdout, "Command line switch \"-K\" should be followed by an integer.\n" );
+                fprintf( stdout, "Command line switch \"-F\" should be followed by an integer.\n" );
                 goto usage;
             }
             nFrames = atoi(argv[globalUtilOptind]);
@@ -17315,9 +17354,15 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nFrames < 0 ) 
                 goto usage;
             break;
+        case 'a':
+            fPhaseAbstract ^= 1;
+            break;
         case 'r':
             fRetimeFirst ^= 1;
             break;
+        case 'm':
+            fRetimeRegs ^= 1;
+            break;
         case 'f':
             fFraiging ^= 1;
             break;
@@ -17343,15 +17388,17 @@ int Abc_CommandAbc8DSec( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAig = Ntl_ManPrepareSec( pArgvNew[0], pArgvNew[1] );
     if ( pAig == NULL )
         return 0;
-    Fra_FraigSec( pAig, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose );
+    Fra_FraigSec( pAig, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose );
     Aig_ManStop( pAig );
     return 0;
 
 usage:
-    fprintf( stdout, "usage: *dsec [-K num] [-rfwvh] <file1> <file2>\n" );
+    fprintf( stdout, "usage: *dsec [-F num] [-armfwvh] <file1> <file2>\n" );
     fprintf( stdout, "\t         performs sequential equivalence checking for two designs\n" );
-    fprintf( stdout, "\t-K num : the limit on the depth of induction [default = %d]\n", nFrames );
+    fprintf( stdout, "\t-F num : the limit on the depth of induction [default = %d]\n", nFrames );
+    fprintf( stdout, "\t-a     : toggles the use of phase abstraction [default = %s]\n", fPhaseAbstract? "yes": "no" );
     fprintf( stdout, "\t-r     : toggles forward retiming at the beginning [default = %s]\n", fRetimeFirst? "yes": "no" );
+    fprintf( stdout, "\t-m     : toggles min-register retiming [default = %s]\n", fRetimeRegs? "yes": "no" );
     fprintf( stdout, "\t-f     : toggles the internal use of fraiging [default = %s]\n", fFraiging? "yes": "no" );
     fprintf( stdout, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( stdout, "\t-w     : toggles additional verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 4b1a37c2..88435e3f 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -1239,7 +1239,7 @@ PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose )
+int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose )
 {
     Aig_Man_t * pMan;
     int RetValue;
@@ -1252,7 +1252,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fFraig
     }
     assert( pMan->nRegs > 0 );
     // perform verification
-    RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose );
+    RetValue = Fra_FraigSec( pMan, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose );
     pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
     if ( pNtk->pSeqModel )
     {
@@ -1274,7 +1274,7 @@ int Abc_NtkDarProve( Abc_Ntk_t * pNtk, int nFrames, int fRetimeFirst, int fFraig
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetimeFirst, int fFraiging, int fVerbose, int fVeryVerbose )
+int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fPhaseAbstract, int fRetimeFirst, int fRetimeRegs, int fFraiging, int fVerbose, int fVeryVerbose )
 {
 //    Fraig_Params_t Params;
     Aig_Man_t * pMan;
@@ -1346,7 +1346,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fRetim
     assert( pMan->nRegs > 0 );
 
     // perform verification
-    RetValue = Fra_FraigSec( pMan, nFrames, fRetimeFirst, fFraiging, fVerbose, fVeryVerbose );
+    RetValue = Fra_FraigSec( pMan, nFrames, fPhaseAbstract, fRetimeFirst, fRetimeRegs, fFraiging, fVerbose, fVeryVerbose );
     Aig_ManStop( pMan );
     return RetValue;
 }
@@ -1909,6 +1909,31 @@ Abc_Ntk_t * Abc_NtkPhaseAbstract( Abc_Ntk_t * pNtk, int nFrames, int fIgnore, in
     return pNtkAig;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs BDD-based reachability analysis.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
+{
+    extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
+    Aig_Man_t * pMan;
+    pMan = Abc_NtkToDar( pNtk, 0, 0 );
+    pMan->nRegs = Abc_NtkLatchNum(pNtk);
+    pMan->nTruePis = Aig_ManPiNum(pMan) - Aig_ManRegNum(pMan); 
+    pMan->nTruePos = Aig_ManPoNum(pMan) - Aig_ManRegNum(pMan); 
+    if ( pMan == NULL )
+        return;
+    Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
+    Aig_ManStop( pMan );
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 856f19fe..26740258 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -217,7 +217,7 @@ int main( int argc, char * argv[] )
                 break;
         }
     }
-      
+    
     // if the memory should be freed, quit packages
     if ( fStatus < 0 ) 
     {
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index bbe81cfd..7e529ef6 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -89,7 +89,7 @@ void If_ObjPerformMappingAnd( If_Man_t * p, If_Obj_t * pObj, int Mode, int fPrep
         // recompute the parameters of the best cut
         pCut->Delay = If_CutDelay( p, pCut );
 //        assert( pCut->Delay <= pObj->Required + p->fEpsilon );
-        if ( pCut->Delay > pObj->Required + p->fEpsilon )
+        if ( pCut->Delay > pObj->Required + 2*p->fEpsilon )
             printf( "If_ObjPerformMappingAnd(): Warning! Delay of node %d (%f) exceeds the required times (%f).\n", 
                 pObj->Id, pCut->Delay, pObj->Required + p->fEpsilon );
         pCut->Area = (Mode == 2)? If_CutAreaDerefed( p, pCut ) : If_CutAreaFlow( p, pCut );
diff --git a/src/misc/extra/extraBddMisc.c b/src/misc/extra/extraBddMisc.c
index 023a9841..5ebedaba 100644
--- a/src/misc/extra/extraBddMisc.c
+++ b/src/misc/extra/extraBddMisc.c
@@ -281,6 +281,7 @@ void Extra_bddPrint( DdManager * dd, DdNode * F )
 
 //  printf("\n");
 }
+
 /**Function********************************************************************
 
   Synopsis    [Returns the size of the support.]