Version abc60303

95 files changed, 1789 insertions, 355 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index e36f133e..c68c74e2 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -21,6 +21,10 @@
 #ifndef __ABC_H__
 #define __ABC_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -435,7 +439,7 @@ extern bool               Abc_NtkDoCheck( Abc_Ntk_t * pNtk );
 extern bool               Abc_NtkCheckObj( Abc_Ntk_t * pNtk, Abc_Obj_t * pObj );
 extern bool               Abc_NtkCompareSignals( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int fComb );
 /*=== abcCollapse.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose );
+extern Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fVerbose );
 /*=== abcCut.c ==========================================================*/
 extern void *             Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fMulti );
 extern void *             Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fMulti );
@@ -471,7 +475,7 @@ extern void               Abc_NtkFraigStoreClean();
 extern int                Abc_NtkSopToBdd( Abc_Ntk_t * pNtk );
 extern DdNode *           Abc_ConvertSopToBdd( DdManager * dd, char * pSop );
 extern char *             Abc_ConvertBddToSop( Extra_MmFlex_t * pMan, DdManager * dd, DdNode * bFuncOn, DdNode * bFuncOnDc, int nFanins, Vec_Str_t * vCube, int fMode );
-extern int                Abc_NtkBddToSop( Abc_Ntk_t * pNtk );
+extern int                Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect );
 extern void               Abc_NodeBddToCnf( Abc_Obj_t * pNode, Extra_MmFlex_t * pMmMan, Vec_Str_t * vCube, char ** ppSop0, char ** ppSop1 );
 extern int                Abc_CountZddCubes( DdManager * dd, DdNode * zCover );
 extern void               Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk );
@@ -528,6 +532,7 @@ extern char *             Abc_NtkLogicStoreName( Abc_Obj_t * pNodeNew, char * pN
 extern char *             Abc_NtkLogicStoreNamePlus( Abc_Obj_t * pNodeNew, char * pNameOld, char * pSuffix );
 extern void               Abc_NtkCreateCioNamesTable( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
+extern void               Abc_NtkDupCioNamesTableDual( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 extern Vec_Ptr_t *        Abc_NodeGetFaninNames( Abc_Obj_t * pNode );
 extern Vec_Ptr_t *        Abc_NodeGetFakeNames( int nNames );
 extern void               Abc_NodeFreeNames( Vec_Ptr_t * vNames );
@@ -541,7 +546,7 @@ extern void               Abc_NtkShortNames( Abc_Ntk_t * pNtk );
 extern stmm_table *       Abc_NtkNamesToTable( Vec_Ptr_t * vNodes );
 /*=== abcNetlist.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk );
-extern Abc_Ntk_t *        Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk );
+extern Abc_Ntk_t *        Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk, int fDirect );
 extern Abc_Ntk_t *        Abc_NtkLogicToNetlistBench( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk );
 extern Abc_Ntk_t *        Abc_NtkAigToLogicSop( Abc_Ntk_t * pNtk );
@@ -549,12 +554,12 @@ extern Abc_Ntk_t *        Abc_NtkAigToLogicSopBench( Abc_Ntk_t * pNtk );
 /*=== abcNtbdd.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkDeriveFromBdd( DdManager * dd, DdNode * bFunc, char * pNamePo, Vec_Ptr_t * vNamesPi );
 extern Abc_Ntk_t *        Abc_NtkBddToMuxes( Abc_Ntk_t * pNtk );
-extern DdManager *        Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly );
+extern DdManager *        Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fBddSizeMax, int fLatchOnly );
 extern void               Abc_NtkFreeGlobalBdds( Abc_Ntk_t * pNtk );
 /*=== abcNtk.c ==========================================================*/
 extern Abc_Ntk_t *        Abc_NtkAlloc( Abc_NtkType_t Type, Abc_NtkFunc_t Func );
 extern Abc_Ntk_t *        Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
-extern Abc_Ntk_t *        Abc_NtkStartFromSeq( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
+extern Abc_Ntk_t *        Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func );
 extern void               Abc_NtkFinalize( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 extern void               Abc_NtkFinalizeRegular( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 extern void               Abc_NtkFinalizeLatches( Abc_Ntk_t * pNtk );
@@ -599,7 +604,7 @@ extern void               Abc_NodeMffsConeSupp( Abc_Obj_t * pNode, Vec_Ptr_t * v
 extern int                Abc_NodeDeref_rec( Abc_Obj_t * pNode );
 extern int                Abc_NodeRef_rec( Abc_Obj_t * pNode );
 /*=== abcRenode.c ==========================================================*/
-extern Abc_Ntk_t *        Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple );
+extern Abc_Ntk_t *        Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor );
 extern DdNode *           Abc_NtkRenodeDeriveBdd( DdManager * dd, Abc_Obj_t * pNodeOld, Vec_Ptr_t * vFaninsOld );
 /*=== abcSat.c ==========================================================*/
 extern int                Abc_NtkMiterSat( Abc_Ntk_t * pNtk, int nConfLimit, int nImpLimit, int fVerbose );
@@ -698,10 +703,16 @@ extern Vec_Int_t *        Abc_NtkFanoutCounts( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkCollectObjects( Abc_Ntk_t * pNtk );
 extern Vec_Int_t *        Abc_NtkGetCiIds( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkReassignIds( Abc_Ntk_t * pNtk );
+/*=== abcVerify.c ==========================================================*/
+extern int *              Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames );
+extern int *              Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel );
 
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
+#ifdef __cplusplus
+}
+#endif
 
 #endif
 
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abcAig.c b/src/base/abc/abcAig.c
index e5f39127..f2f50f77 100644
--- a/src/base/abc/abcAig.c
+++ b/src/base/abc/abcAig.c
@@ -295,6 +295,7 @@ Abc_Obj_t * Abc_AigAndCreate( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t * p1 )
     // create the cuts if defined
 //    if ( pAnd->pNtk->pManCut )
 //        Abc_NodeGetCuts( pAnd->pNtk->pManCut, pAnd );
+    pAnd->pCopy = NULL;
     return pAnd;
 }
 
@@ -331,6 +332,7 @@ Abc_Obj_t * Abc_AigAndCreateFrom( Abc_Aig_t * pMan, Abc_Obj_t * p0, Abc_Obj_t *
     // create the cuts if defined
 //    if ( pAnd->pNtk->pManCut )
 //        Abc_NodeGetCuts( pAnd->pNtk->pManCut, pAnd );
+    pAnd->pCopy = NULL;
     return pAnd;
 }
 
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 2ab3842f..cb20cec3 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -195,20 +195,25 @@ void Abc_NtkLogicMakeDirectSops( Abc_Ntk_t * pNtk )
 
   Synopsis    [Converts the network from BDD to SOP representation.]
 
-  Description []
+  Description [If the flag is set to 1, forces the direct phase of all covers.]
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkBddToSop( Abc_Ntk_t * pNtk )
+int Abc_NtkBddToSop( Abc_Ntk_t * pNtk, int fDirect )
 {
     Abc_Obj_t * pNode;
     DdManager * dd = pNtk->pManFunc;
     DdNode * bFunc;
     Vec_Str_t * vCube;
-    int i;
+    int i, fMode;
+
+    if ( fDirect )
+        fMode = 1;
+    else
+        fMode = -1;
 
     assert( Abc_NtkIsBddLogic(pNtk) ); 
     Cudd_zddVarsFromBddVars( dd, 2 );
@@ -223,7 +228,7 @@ int Abc_NtkBddToSop( Abc_Ntk_t * pNtk )
     {
         assert( pNode->pData );
         bFunc = pNode->pData;
-        pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, -1 );
+        pNode->pData = Abc_ConvertBddToSop( pNtk->pManFunc, dd, bFunc, bFunc, Abc_ObjFaninNum(pNode), vCube, fMode );
         if ( pNode->pData == NULL )
         {
             Vec_StrFree( vCube );
diff --git a/src/base/abc/abcInt.h b/src/base/abc/abcInt.h
index 967f5695..0e35e774 100644
--- a/src/base/abc/abcInt.h
+++ b/src/base/abc/abcInt.h
@@ -43,10 +43,10 @@
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
 
diff --git a/src/base/abc/abcNames.c b/src/base/abc/abcNames.c
index ccbd2c85..14f0b505 100644
--- a/src/base/abc/abcNames.c
+++ b/src/base/abc/abcNames.c
@@ -290,6 +290,39 @@ void Abc_NtkDupCioNamesTable( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
 
 /**Function*************************************************************
 
+  Synopsis    [Duplicates the name arrays.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkDupCioNamesTableDual( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    assert( Abc_NtkPiNum(pNtk) == Abc_NtkPiNum(pNtkNew) );
+    assert( Abc_NtkPoNum(pNtk) * 2 == Abc_NtkPoNum(pNtkNew) );
+    assert( Abc_NtkLatchNum(pNtk) == Abc_NtkLatchNum(pNtkNew) );
+    assert( st_count(pNtk->tObj2Name) > 0 );
+    assert( st_count(pNtkNew->tObj2Name) == 0 );
+    // copy the CI/CO names if given
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( Abc_NtkPi(pNtkNew,i),    Abc_ObjName(pObj) );
+    Abc_NtkForEachPo( pNtk, pObj, i ) 
+    {
+        Abc_NtkLogicStoreNamePlus( Abc_NtkPo(pNtkNew,2*i+0),    Abc_ObjName(pObj), "_pos" );
+        Abc_NtkLogicStoreNamePlus( Abc_NtkPo(pNtkNew,2*i+1),    Abc_ObjName(pObj), "_neg" );
+    }
+    if ( !Abc_NtkIsSeq(pNtk) )
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+        Abc_NtkLogicStoreName( Abc_NtkLatch(pNtkNew,i), Abc_ObjName(pObj) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Gets fanin node names.]
 
   Description []
diff --git a/src/base/abc/abcNetlist.c b/src/base/abc/abcNetlist.c
index 65cc6e2e..d289cd35 100644
--- a/src/base/abc/abcNetlist.c
+++ b/src/base/abc/abcNetlist.c
@@ -83,7 +83,7 @@ Abc_Ntk_t * Abc_NtkNetlistToLogic( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk )
+Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk, int fDirect )
 {
     Abc_Ntk_t * pNtkNew, * pNtkTemp; 
     assert( Abc_NtkIsLogic(pNtk) || Abc_NtkIsStrash(pNtk) || Abc_NtkIsSeq(pNtk) );
@@ -101,7 +101,7 @@ Abc_Ntk_t * Abc_NtkLogicToNetlist( Abc_Ntk_t * pNtk )
     }
     else if ( Abc_NtkIsBddLogic(pNtk) )
     {
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk, fDirect);
         pNtkNew = Abc_NtkLogicSopToNetlist( pNtk );
         Abc_NtkSopToBdd(pNtk);
     }
@@ -157,7 +157,7 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
     assert( Abc_NtkLogicHasSimpleCos(pNtk) );
 
     if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk,0);
 
     // start the netlist by creating PI/PO/Latch objects
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_NETLIST, pNtk->ntkFunc );
@@ -220,7 +220,7 @@ Abc_Ntk_t * Abc_NtkLogicSopToNetlist( Abc_Ntk_t * pNtk )
             Abc_ObjAddFanin( pObj->pCopy, pFanin->pCopy->pCopy );
     // duplicate EXDC 
     if ( pNtk->pExdc )
-        pNtkNew->pExdc = Abc_NtkLogicToNetlist( pNtk->pExdc );
+        pNtkNew->pExdc = Abc_NtkLogicToNetlist( pNtk->pExdc, 0 );
     if ( !Abc_NtkCheck( pNtkNew ) )
         fprintf( stdout, "Abc_NtkLogicSopToNetlist(): Network check has failed.\n" );
     return pNtkNew;
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 31b4c5f4..0692819b 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -148,6 +148,64 @@ Abc_Ntk_t * Abc_NtkStartFrom( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_
 
 /**Function*************************************************************
 
+  Synopsis    [Starts a new network using existing network as a model.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Ntk_t * Abc_NtkStartFromDual( Abc_Ntk_t * pNtk, Abc_NtkType_t Type, Abc_NtkFunc_t Func )
+{
+    Abc_Ntk_t * pNtkNew; 
+    Abc_Obj_t * pObj, * pObjNew;
+    int i;
+    if ( pNtk == NULL )
+        return NULL;
+    // start the network
+    pNtkNew = Abc_NtkAlloc( Type, Func );
+    // duplicate the name and the spec
+    pNtkNew->pName = Extra_UtilStrsav(pNtk->pName);
+    pNtkNew->pSpec = NULL;
+    // clean the node copy fields
+    Abc_NtkForEachNode( pNtk, pObj, i )
+        pObj->pCopy = NULL;
+    // map the constant nodes
+    if ( Abc_NtkConst1(pNtk) )
+        Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew);
+    // clone the PIs/POs/latches
+    Abc_NtkForEachPi( pNtk, pObj, i )
+        Abc_NtkDupObj(pNtkNew, pObj);
+    Abc_NtkForEachPo( pNtk, pObj, i )
+    {
+        Abc_NtkDupObj(pNtkNew, pObj);
+        pObjNew = pObj->pCopy;
+        Abc_NtkDupObj(pNtkNew, pObj);
+        // connect second to the first
+        pObjNew->pCopy = pObj->pCopy;
+        // collect first to old
+        pObj->pCopy = pObjNew;
+    }
+    Abc_NtkForEachLatch( pNtk, pObj, i )
+    {
+        pObjNew = Abc_NtkDupObj(pNtkNew, pObj);
+        Vec_PtrPush( pNtkNew->vCis, pObjNew );
+        Vec_PtrPush( pNtkNew->vCos, pObjNew );
+    }
+    // transfer the names
+    Abc_NtkDupCioNamesTableDual( pNtk, pNtkNew );
+//    Abc_ManTimeDup( pNtk, pNtkNew );
+    // check that the CI/CO/latches are copied correctly
+    assert( Abc_NtkCiNum(pNtk)    == Abc_NtkCiNum(pNtkNew) );
+    assert( Abc_NtkCoNum(pNtk)* 2 == Abc_NtkCoNum(pNtkNew) );
+    assert( Abc_NtkLatchNum(pNtk) == Abc_NtkLatchNum(pNtkNew) );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Finalizes the network using the existing network as a model.]
 
   Description []
diff --git a/src/base/abc/abcObj.c b/src/base/abc/abcObj.c
index 481b069f..d6adfeb2 100644
--- a/src/base/abc/abcObj.c
+++ b/src/base/abc/abcObj.c
@@ -227,7 +227,18 @@ void Abc_NtkDeleteObj( Abc_Obj_t * pObj )
     {
         pNtk->nLatches--;
     }
-    else 
+    else if ( Abc_ObjIsPo(pObj) )
+    {
+        assert( Abc_NtkPoNum(pObj->pNtk) == 1 );
+        Vec_PtrRemove( pObj->pNtk->vCos, pObj );
+        pObj->pNtk->nPos--;
+        // add the name to the table
+        if ( !stmm_delete( pObj->pNtk->tObj2Name, (char **)&pObj, NULL ) )
+        {
+            assert( 0 ); // the PO is not in the table
+        }
+    }
+    else
         assert( 0 );
     // recycle the net itself
     Abc_ObjRecycle( pObj );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index d2422b64..8927279f 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -71,7 +71,6 @@ static int Abc_CommandSop          ( Abc_Frame_t * pAbc, int argc, char ** argv
 static int Abc_CommandBdd          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandReorder      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMuxes        ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandSat          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandExtSeqDcs    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandOneOutput    ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandOneNode      ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -112,6 +111,7 @@ static int Abc_CommandSeqCleanup   ( Abc_Frame_t * pAbc, int argc, char ** argv
 
 static int Abc_CommandCec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandSat          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandProve        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 ////////////////////////////////////////////////////////////////////////
@@ -173,7 +173,6 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Various",      "bdd",           Abc_CommandBdd,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "reorder",       Abc_CommandReorder,          0 );
     Cmd_CommandAdd( pAbc, "Various",      "muxes",         Abc_CommandMuxes,            1 );
-    Cmd_CommandAdd( pAbc, "Various",      "sat",           Abc_CommandSat,              0 );
     Cmd_CommandAdd( pAbc, "Various",      "ext_seq_dcs",   Abc_CommandExtSeqDcs,        0 );
     Cmd_CommandAdd( pAbc, "Various",      "cone",          Abc_CommandOneOutput,        1 );
     Cmd_CommandAdd( pAbc, "Various",      "node",          Abc_CommandOneNode,          1 );
@@ -214,6 +213,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
 
     Cmd_CommandAdd( pAbc, "Verification", "cec",           Abc_CommandCec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "sec",           Abc_CommandSec,              0 );
+    Cmd_CommandAdd( pAbc, "Verification", "sat",           Abc_CommandSat,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "prove",         Abc_CommandProve,            1 );
 
 //    Rwt_Man4ExploreStart();
@@ -1594,6 +1594,8 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
+    int fBddSizeMax;
+    int fDualRail;
     int c;
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -1601,11 +1603,27 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fDualRail = 0;
+    fBddSizeMax = 1000000;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Bdh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'B':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-B\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            fBddSizeMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( fBddSizeMax < 0 ) 
+                goto usage;
+            break;
+        case 'd':
+            fDualRail ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -1627,11 +1645,11 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // get the new network
     if ( Abc_NtkIsStrash(pNtk) )
-        pNtkRes = Abc_NtkCollapse( pNtk, 1 );
+        pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, 1 );
     else
     {
         pNtk = Abc_NtkStrash( pNtk, 0, 0 );
-        pNtkRes = Abc_NtkCollapse( pNtk, 1 );
+        pNtkRes = Abc_NtkCollapse( pNtk, fBddSizeMax, fDualRail, 1 );
         Abc_NtkDelete( pNtk );
     }
     if ( pNtkRes == NULL )
@@ -1644,9 +1662,11 @@ int Abc_CommandCollapse( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: collapse [-h]\n" );
-    fprintf( pErr, "\t        collapses the network by constructing global BDDs\n" );
-    fprintf( pErr, "\t-h    : print the command usage\n");
+    fprintf( pErr, "usage: collapse [-B num] [-dh]\n" );
+    fprintf( pErr, "\t          collapses the network by constructing global BDDs\n" );
+    fprintf( pErr, "\t-B num  : limit on live BDD nodes during collapsing [default = %d]\n", fBddSizeMax );
+    fprintf( pErr, "\t-d      : toggles dual-rail collapsing mode [default = %s]\n", fDualRail? "yes": "no" );
+    fprintf( pErr, "\t-h      : print the command usage\n");
     return 1;
 }
 
@@ -1837,6 +1857,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fCnf;
     int fMulti;
     int fSimple;
+    int fFactor;
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -1848,8 +1869,9 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     fCnf      =  0;
     fMulti    =  0;
     fSimple   =  0;
+    fFactor   =  0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "TFmcsh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "TFmcsfh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -1884,6 +1906,9 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 's':
             fSimple ^= 1;
             break;
+        case 'f':
+            fFactor ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -1903,7 +1928,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkRenode( pNtk, nThresh, nFaninMax, fCnf, fMulti, fSimple );
+    pNtkRes = Abc_NtkRenode( pNtk, nThresh, nFaninMax, fCnf, fMulti, fSimple, fFactor );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Renoding has failed.\n" );
@@ -1914,7 +1939,7 @@ int Abc_CommandRenode( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: renode [-T num] [-F num] [-cmsh]\n" );
+    fprintf( pErr, "usage: renode [-T num] [-F num] [-msfch]\n" );
     fprintf( pErr, "\t          transforms an AIG into a logic network by creating larger nodes\n" );
     fprintf( pErr, "\t-F num  : the maximum fanin size after renoding [default = %d]\n", nFaninMax );
     fprintf( pErr, "\t-T num  : the threshold for AIG node duplication [default = %d]\n", nThresh );
@@ -1923,6 +1948,7 @@ usage:
     fprintf( pErr, "\t          that is, if [(numFanouts(Node)-1) * size(MFFC(Node))] <= %d)\n", nThresh );
     fprintf( pErr, "\t-m      : creates multi-input AND graph [default = %s]\n", fMulti? "yes": "no" );
     fprintf( pErr, "\t-s      : creates a simple AIG (no renoding) [default = %s]\n", fSimple? "yes": "no" );
+    fprintf( pErr, "\t-f      : creates a factor-cut network [default = %s]\n", fFactor? "yes": "no" );
     fprintf( pErr, "\t-c      : performs renoding to derive the CNF [default = %s]\n", fCnf? "yes": "no" );
     fprintf( pErr, "\t-h      : print the command usage\n");
     return 1;
@@ -2852,6 +2878,7 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
+    int fDirect;
     int c;
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -2859,11 +2886,15 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
+    fDirect = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "h" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "dh" ) ) != EOF )
     {
         switch ( c )
         {
+        case 'd':
+            fDirect ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -2883,7 +2914,7 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( pErr, "Converting to SOP is possible when node functions are BDDs.\n" );
         return 1;
     }
-    if ( !Abc_NtkBddToSop( pNtk ) )
+    if ( !Abc_NtkBddToSop( pNtk, fDirect ) )
     {
         fprintf( pErr, "Converting to SOP has failed.\n" );
         return 1;
@@ -2891,8 +2922,9 @@ int Abc_CommandSop( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: sop [-h]\n" );
+    fprintf( pErr, "usage: sop [-dh]\n" );
     fprintf( pErr, "\t         converts node functions from BDD to SOP\n" );
+    fprintf( pErr, "\t-d     : toggles using both phases or only positive [default = %s]\n", fDirect? "direct": "both" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -3084,130 +3116,6 @@ usage:
     return 1;
 }
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
-{
-    FILE * pOut, * pErr;
-    Abc_Ntk_t * pNtk;
-    int c;
-    int RetValue;
-    int fVerbose;
-    int nConfLimit;
-    int nImpLimit;
-    int clk;
-
-    pNtk = Abc_FrameReadNtk(pAbc);
-    pOut = Abc_FrameReadOut(pAbc);
-    pErr = Abc_FrameReadErr(pAbc);
-
-    // set defaults
-    fVerbose   = 0;
-    nConfLimit = 100000;   
-    nImpLimit  = 0;
-    Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CIvh" ) ) != EOF )
-    {
-        switch ( c )
-        {
-        case 'C':
-            if ( globalUtilOptind >= argc )
-            {
-                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nConfLimit = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nConfLimit < 0 ) 
-                goto usage;
-            break;
-        case 'I':
-            if ( globalUtilOptind >= argc )
-            {
-                fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
-                goto usage;
-            }
-            nImpLimit = atoi(argv[globalUtilOptind]);
-            globalUtilOptind++;
-            if ( nImpLimit < 0 ) 
-                goto usage;
-            break;
-        case 'v':
-            fVerbose ^= 1;
-            break;
-        case 'h':
-            goto usage;
-        default:
-            goto usage;
-        }
-    }
-
-    if ( pNtk == NULL )
-    {
-        fprintf( pErr, "Empty network.\n" );
-        return 1;
-    }
-    if ( Abc_NtkLatchNum(pNtk) > 0 )
-    {
-        fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
-        return 0;
-    } 
-    if ( Abc_NtkIsSeq(pNtk) )
-    {
-        fprintf( stdout, "This command cannot be applied to the sequential AIG.\n" );
-        return 0;
-    }
-
-    if ( Abc_NtkIsStrash(pNtk) )
-    {
-        clk = clock();
-        RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, fVerbose );
-        if ( RetValue == -1 )
-            printf( "UNDECIDED      " );
-        else if ( RetValue == 0 )
-            printf( "SATISFIABLE    " );
-        else
-            printf( "UNSATISFIABLE  " );
-        //printf( "\n" );
-        PRT( "Time", clock() - clk );
-    }
-    else
-    {
-        Abc_Ntk_t * pTemp;
-        pTemp = Abc_NtkStrash( pNtk, 0, 0 );
-        clk = clock();
-        RetValue = Abc_NtkMiterSat( pTemp, nConfLimit, nImpLimit, fVerbose );
-        if ( RetValue == -1 )
-            printf( "UNDECIDED      " );
-        else if ( RetValue == 0 )
-            printf( "SATISFIABLE    " );
-        else
-            printf( "UNSATISFIABLE  " );
-        //printf( "\n" );
-        PRT( "Time", clock() - clk );
-        Abc_NtkDelete( pTemp );
-    }
-    return 0;
-
-usage:
-    fprintf( pErr, "usage: sat [-C num] [-I num] [-vh]\n" );
-    fprintf( pErr, "\t         solves the combinational miter\n" );
-    fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
-    fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit );
-    fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
-    fprintf( pErr, "\t-h     : print the command usage\n");
-    return 1;
-}
-
 
 /**Function*************************************************************
 
@@ -4148,7 +4056,7 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
-    extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
+//    extern Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -4184,8 +4092,8 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     // run the command
 //    pNtkRes = Abc_NtkMiterForCofactors( pNtk, 0, 0, -1 );
 
-    pNtkRes = Abc_NtkNewAig( pNtk );
-//    pNtkRes = NULL;
+//    pNtkRes = Abc_NtkNewAig( pNtk );
+    pNtkRes = NULL;
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Command has failed.\n" );
@@ -6424,6 +6332,133 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandSat( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int c;
+    int RetValue;
+    int fVerbose;
+    int nConfLimit;
+    int nImpLimit;
+    int clk;
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fVerbose   = 0;
+    nConfLimit = 100000;   
+    nImpLimit  = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CIvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConfLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nConfLimit < 0 ) 
+                goto usage;
+            break;
+        case 'I':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-I\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nImpLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nImpLimit < 0 ) 
+                goto usage;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( Abc_NtkLatchNum(pNtk) > 0 )
+    {
+        fprintf( stdout, "Currently can only solve the miter for combinational circuits.\n" );
+        return 0;
+    } 
+    if ( Abc_NtkIsSeq(pNtk) )
+    {
+        fprintf( stdout, "This command cannot be applied to the sequential AIG.\n" );
+        return 0;
+    }
+
+    clk = clock();
+    if ( Abc_NtkIsStrash(pNtk) )
+    {
+        RetValue = Abc_NtkMiterSat( pNtk, nConfLimit, nImpLimit, fVerbose );
+    }
+    else
+    {
+        Abc_Ntk_t * pTemp;
+        pTemp = Abc_NtkStrash( pNtk, 0, 0 );
+        RetValue = Abc_NtkMiterSat( pTemp, nConfLimit, nImpLimit, fVerbose );
+        pNtk->pModel = pTemp->pModel;  pTemp->pModel = NULL;
+        Abc_NtkDelete( pTemp );
+    }
+
+    // verify that the pattern is correct
+    if ( RetValue == 0 && Abc_NtkPoNum(pNtk) == 1 )
+    {
+        int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtk->pModel );
+        if ( pSimInfo[0] != 1 )
+            printf( "ERROR in Abc_NtkMiterProve(): Generated counter example is invalid.\n" );
+        free( pSimInfo );
+    }
+
+    if ( RetValue == -1 )
+        printf( "UNDECIDED      " );
+    else if ( RetValue == 0 )
+        printf( "SATISFIABLE    " );
+    else
+        printf( "UNSATISFIABLE  " );
+    //printf( "\n" );
+    PRT( "Time", clock() - clk );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: sat [-C num] [-I num] [-vh]\n" );
+    fprintf( pErr, "\t         solves the combinational miter using SAT solver MiniSat-1.14\n" );
+    fprintf( pErr, "\t         derives CNF from the current network and leave it unchanged\n" );
+    fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
+    fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit );
+    fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -6519,6 +6554,16 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         pNtkTemp = Abc_NtkStrash( pNtk, 0, 0 );
 
     RetValue = Abc_NtkMiterProve( &pNtkTemp, nConfLimit, nImpLimit, fRewrite, fFraig, fVerbose );
+
+    // verify that the pattern is correct
+    if ( RetValue == 0 )
+    {
+        int * pSimInfo = Abc_NtkVerifySimulatePattern( pNtk, pNtkTemp->pModel );
+        if ( pSimInfo[0] != 1 )
+            printf( "ERROR in Abc_NtkMiterProve(): Generated counter-example is invalid.\n" );
+        free( pSimInfo );
+    }
+ 
     if ( RetValue == -1 ) 
         printf( "UNDECIDED      " );
     else if ( RetValue == 0 )
@@ -6535,6 +6580,7 @@ int Abc_CommandProve( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     fprintf( pErr, "usage: prove [-C num] [-I num] [-rfvh]\n" );
     fprintf( pErr, "\t         solves combinational miter by rewriting, FRAIGing, and SAT\n" );
+    fprintf( pErr, "\t         replaces the current network by the cone modified by rewriting\n" );
     fprintf( pErr, "\t-C num : limit on the number of conflicts [default = %d]\n",    nConfLimit );
     fprintf( pErr, "\t-I num : limit on the number of implications [default = %d]\n", nImpLimit );
     fprintf( pErr, "\t-r     : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );  
diff --git a/src/base/abci/abcAuto.c b/src/base/abci/abcAuto.c
index f1e1ef75..fb818ff3 100644
--- a/src/base/abci/abcAuto.c
+++ b/src/base/abci/abcAuto.c
@@ -51,7 +51,7 @@ void Abc_NtkAutoPrint( Abc_Ntk_t * pNtk, int Output, int fNaive, int fVerbose )
     int nOutputs, nInputs, i;
 
     // compute the global BDDs
-    if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL )
+    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0) == NULL )
         return;
 
     // get information about the network
diff --git a/src/base/abci/abcClpBdd.c b/src/base/abci/abcClpBdd.c
index 59c76e09..84016436 100644
--- a/src/base/abci/abcClpBdd.c
+++ b/src/base/abci/abcClpBdd.c
@@ -25,6 +25,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 static Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk );
+static Abc_Ntk_t * Abc_NtkFromGlobalBddsDual( Abc_Ntk_t * pNtk );
 static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc );
 
 ////////////////////////////////////////////////////////////////////////
@@ -42,20 +43,23 @@ static Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd,
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fVerbose )
+Abc_Ntk_t * Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fVerbose )
 {
     Abc_Ntk_t * pNtkNew;
 
     assert( Abc_NtkIsStrash(pNtk) );
 
     // compute the global BDDs
-    if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL )
+    if ( Abc_NtkGlobalBdds(pNtk, fBddSizeMax, 0) == NULL )
         return NULL;
     if ( fVerbose )
         printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
 
     // create the new network
-    pNtkNew = Abc_NtkFromGlobalBdds( pNtk );
+    if ( fDualRail )
+        pNtkNew = Abc_NtkFromGlobalBddsDual( pNtk );
+    else
+        pNtkNew = Abc_NtkFromGlobalBdds( pNtk );
     Abc_NtkFreeGlobalBdds( pNtk );
     if ( pNtkNew == NULL )
     {
@@ -127,6 +131,42 @@ Abc_Ntk_t * Abc_NtkFromGlobalBdds( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
+Abc_Ntk_t * Abc_NtkFromGlobalBddsDual( Abc_Ntk_t * pNtk )
+{
+    ProgressBar * pProgress;
+    Abc_Ntk_t * pNtkNew;
+    Abc_Obj_t * pNode, * pNodeNew;
+    DdManager * dd = pNtk->pManGlob;
+    int i;
+    // start the new network
+    pNtkNew = Abc_NtkStartFromDual( pNtk, ABC_NTK_LOGIC, ABC_FUNC_BDD );
+    // make sure the new manager has the same number of inputs
+    Cudd_bddIthVar( pNtkNew->pManFunc, dd->size-1 );
+    // process the POs
+    pProgress = Extra_ProgressBarStart( stdout, Abc_NtkCoNum(pNtk) );
+    Abc_NtkForEachCo( pNtk, pNode, i )
+    {
+        Extra_ProgressBarUpdate( pProgress, i, NULL );
+        pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Cudd_Not( Vec_PtrEntry(pNtk->vFuncsGlob, i) ) );
+        Abc_ObjAddFanin( pNode->pCopy->pCopy, pNodeNew );
+        pNodeNew = Abc_NodeFromGlobalBdds( pNtkNew, dd, Vec_PtrEntry(pNtk->vFuncsGlob, i) );
+        Abc_ObjAddFanin( pNode->pCopy, pNodeNew );
+    }
+    Extra_ProgressBarStop( pProgress );
+    return pNtkNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the network with the given global BDD.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Abc_Obj_t * Abc_NodeFromGlobalBdds( Abc_Ntk_t * pNtkNew, DdManager * dd, DdNode * bFunc )
 {
     Abc_Obj_t * pNodeNew, * pTemp;
diff --git a/src/base/abci/abcCut.c b/src/base/abci/abcCut.c
index 1ee9a712..2b1816c4 100644
--- a/src/base/abci/abcCut.c
+++ b/src/base/abci/abcCut.c
@@ -57,41 +57,6 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     extern void Abc_NtkBalanceDetach( Abc_Ntk_t * pNtk );
 
     assert( Abc_NtkIsStrash(pNtk) );
-/*
-    if ( pParams->fMulti )
-    {
-        Abc_Obj_t * pNode, * pNodeA, * pNodeB, * pNodeC;
-        int nFactors;
-        // lebel the nodes, which will be the roots of factor-cuts
-        // mark the multiple-fanout nodes
-        Abc_AigForEachAnd( pNtk, pNode, i )
-            if ( pNode->vFanouts.nSize > 1 )
-                pNode->fMarkB = 1;
-        // unmark the control inputs of MUXes and inputs of EXOR gates
-        Abc_AigForEachAnd( pNtk, pNode, i )
-        {
-            if ( !Abc_NodeIsMuxType(pNode) )
-                continue;
-
-            pNodeC = Abc_NodeRecognizeMux( pNode, &pNodeA, &pNodeB );
-            // if real children are used, skip
-            if ( Abc_ObjFanin0(pNode)->vFanouts.nSize > 1 || Abc_ObjFanin1(pNode)->vFanouts.nSize > 1 )
-                continue;
-
-            if ( pNodeC->vFanouts.nSize == 2 )
-                pNodeC->fMarkB = 0;
-            if ( Abc_ObjRegular(pNodeA) == Abc_ObjRegular(pNodeB) && Abc_ObjRegular(pNodeA)->vFanouts.nSize == 2 )
-                Abc_ObjRegular(pNodeA)->fMarkB = 0;
-       }
-        // mark the PO drivers
-//        Abc_NtkForEachCo( pNtk, pNode, i )
-//            Abc_ObjFanin0(pNode)->fMarkB = 1;
-        nFactors = 0;
-        Abc_AigForEachAnd( pNtk, pNode, i )
-            nFactors += pNode->fMarkB;
-        printf( "Total nodes = %6d.  Total factors = %6d.\n", Abc_NtkNodeNum(pNtk), nFactors );
-    }
-*/
     // start the manager
     pParams->nIdsMax = Abc_NtkObjNumMax( pNtk );
     p = Cut_ManStart( pParams );
@@ -135,13 +100,6 @@ Cut_Man_t * Abc_NtkCuts( Abc_Ntk_t * pNtk, Cut_Params_t * pParams )
     }
     Vec_PtrFree( vNodes );
     Vec_IntFree( vChoices );
-/*
-    if ( pParams->fMulti )
-    {
-        Abc_NtkForEachObj( pNtk, pNode, i )
-            pNode->fMarkB = 0;
-    }
-*/
 PRT( "Total", clock() - clk );
 //Abc_NtkPrintCuts_( p, pNtk, 0 );
 //    Cut_ManPrintStatsToFile( p, pNtk->pSpec, clock() - clk );
diff --git a/src/base/abci/abcDsd.c b/src/base/abci/abcDsd.c
index 9dd5ea3a..18a85a04 100644
--- a/src/base/abci/abcDsd.c
+++ b/src/base/abci/abcDsd.c
@@ -60,7 +60,7 @@ Abc_Ntk_t * Abc_NtkDsdGlobal( Abc_Ntk_t * pNtk, bool fVerbose, bool fPrint, bool
     assert( Abc_NtkIsStrash(pNtk) );
 
     // perform FPGA mapping
-    if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL )
+    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0) == NULL )
         return NULL;
     if ( fVerbose )
         printf( "The shared BDD size is %d nodes.\n", Cudd_ReadKeys(pNtk->pManGlob) - Cudd_ReadDead(pNtk->pManGlob) );
diff --git a/src/base/abci/abcEspresso.c b/src/base/abci/abcEspresso.c
index ee6598c9..744169b5 100644
--- a/src/base/abci/abcEspresso.c
+++ b/src/base/abci/abcEspresso.c
@@ -54,7 +54,7 @@ void Abc_NtkEspresso( Abc_Ntk_t * pNtk, int fVerbose )
     if ( Abc_NtkHasMapping(pNtk) )
         Abc_NtkUnmap(pNtk);
     else if ( Abc_NtkHasBdd(pNtk) )
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk, 0);
     // minimize SOPs of all nodes
     Abc_NtkForEachNode( pNtk, pNode, i )
         if ( i ) Abc_NodeEspresso( pNode );
diff --git a/src/base/abci/abcFxu.c b/src/base/abci/abcFxu.c
index 5c629b30..b377da1d 100644
--- a/src/base/abci/abcFxu.c
+++ b/src/base/abci/abcFxu.c
@@ -57,7 +57,7 @@ bool Abc_NtkFastExtract( Abc_Ntk_t * pNtk, Fxu_Data_t * p )
     if ( Abc_NtkIsMappedLogic(pNtk) )
         Abc_NtkUnmap(pNtk);
     else if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk, 0);
     else
     { // to make sure the SOPs are SCC-free
 //        Abc_NtkSopToBdd(pNtk);
diff --git a/src/base/abci/abcMap.c b/src/base/abci/abcMap.c
index 39bf15aa..25d9e30f 100644
--- a/src/base/abci/abcMap.c
+++ b/src/base/abci/abcMap.c
@@ -521,8 +521,8 @@ Abc_Ntk_t * Abc_NtkFromMapSuperChoice( Map_Man_t * pMan, Abc_Ntk_t * pNtk )
 
     // duplicate the network
     pNtkNew2 = Abc_NtkDup( pNtk );
-    pNtkNew  = Abc_NtkRenode( pNtkNew2, 0, 20, 0, 0, 1 );
-    Abc_NtkBddToSop( pNtkNew );
+    pNtkNew  = Abc_NtkRenode( pNtkNew2, 0, 20, 0, 0, 1, 0 );
+    Abc_NtkBddToSop( pNtkNew, 0 );
 
     // set the old network to point to the new network
     Abc_NtkForEachCi( pNtk, pNode, i )
diff --git a/src/base/abci/abcMiter.c b/src/base/abci/abcMiter.c
index 30fc3a79..c0658d5e 100644
--- a/src/base/abci/abcMiter.c
+++ b/src/base/abci/abcMiter.c
@@ -414,7 +414,7 @@ Abc_Ntk_t * Abc_NtkMiterQuantify( Abc_Ntk_t * pNtk, int In, int fExist )
 
 /**Function*************************************************************
 
-  Synopsis    [Derives the miter of two cofactors of one output.]
+  Synopsis    [Quantifies all the PIs existentially from the only PO of the network.]
 
   Description []
                
@@ -470,7 +470,7 @@ int Abc_NtkMiterIsConstant( Abc_Ntk_t * pMiter )
             if ( !Abc_ObjIsComplement(pChild) )
             {
                 // if the miter is constant 1, return immediately
-                printf( "MITER IS CONSTANT 1!\n" );
+//                printf( "MITER IS CONSTANT 1!\n" );
                 return 0;
             }
         }
diff --git a/src/base/abci/abcNewAig.c b/src/base/abci/abcNewAig.c
index ce76195a..209fc991 100644
--- a/src/base/abci/abcNewAig.c
+++ b/src/base/abci/abcNewAig.c
@@ -65,7 +65,7 @@ Abc_Ntk_t * Abc_NtkNewAig( Abc_Ntk_t * pNtk )
     assert( !Abc_NtkIsNetlist(pNtk) );
     assert( !Abc_NtkIsSeq(pNtk) );
     if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk, 0);
     // print warning about choice nodes
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
diff --git a/src/base/abci/abcNtbdd.c b/src/base/abci/abcNtbdd.c
index b961ec15..d92da31b 100644
--- a/src/base/abci/abcNtbdd.c
+++ b/src/base/abci/abcNtbdd.c
@@ -27,7 +27,7 @@
 static void        Abc_NtkBddToMuxesPerform( Abc_Ntk_t * pNtk, Abc_Ntk_t * pNtkNew );
 static Abc_Obj_t * Abc_NodeBddToMuxes( Abc_Obj_t * pNodeOld, Abc_Ntk_t * pNtkNew );
 static Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t * pNtkNew, st_table * tBdd2Node );
-static DdNode *    Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode );
+static DdNode *    Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -243,7 +243,7 @@ Abc_Obj_t * Abc_NodeBddToMuxes_rec( DdManager * dd, DdNode * bFunc, Abc_Ntk_t *
   SeeAlso     []
 
 ***********************************************************************/
-DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
+DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int nBddSizeMax, int fLatchOnly )
 {
     int fReorder = 1;
     ProgressBar * pProgress;
@@ -276,10 +276,10 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
         Abc_NtkForEachLatch( pNtk, pNode, i )
         {
             Extra_ProgressBarUpdate( pProgress, i, NULL );
-            bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode) );
+            bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax );
             if ( bFunc == NULL )
             {
-                printf( "Constructing global BDDs timed out.\n" );
+                printf( "Constructing global BDDs is aborted.\n" );
                 Extra_ProgressBarStop( pProgress );
                 Cudd_Quit( dd );
                 return NULL;
@@ -296,10 +296,10 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
         Abc_NtkForEachCo( pNtk, pNode, i )
         {
             Extra_ProgressBarUpdate( pProgress, i, NULL );
-            bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode) );
+            bFunc = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin0(pNode), nBddSizeMax );
             if ( bFunc == NULL )
             {
-                printf( "Constructing global BDDs timed out.\n" );
+                printf( "Constructing global BDDs is aborted.\n" );
                 Extra_ProgressBarStop( pProgress );
                 Cudd_Quit( dd );
                 return NULL;
@@ -339,21 +339,25 @@ DdManager * Abc_NtkGlobalBdds( Abc_Ntk_t * pNtk, int fLatchOnly )
   SeeAlso     []
 
 ***********************************************************************/
-DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode )
+DdNode * Abc_NodeGlobalBdds_rec( DdManager * dd, Abc_Obj_t * pNode, int nBddSizeMax )
 {
     DdNode * bFunc, * bFunc0, * bFunc1;
     assert( !Abc_ObjIsComplement(pNode) );
-    if ( Cudd_ReadKeys(dd) > 5000000 )
+    if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )
+    {
+        printf( "The number of live nodes reached %d.\n", nBddSizeMax );
+        fflush( stdout );
         return NULL;
+    }
     // if the result is available return
     if ( pNode->pCopy )
         return (DdNode *)pNode->pCopy;
     // compute the result for both branches
-    bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0) ); 
+    bFunc0 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,0), nBddSizeMax ); 
     if ( bFunc0 == NULL )
         return NULL;
     Cudd_Ref( bFunc0 );
-    bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1) ); 
+    bFunc1 = Abc_NodeGlobalBdds_rec( dd, Abc_ObjFanin(pNode,1), nBddSizeMax ); 
     if ( bFunc1 == NULL )
         return NULL;
     Cudd_Ref( bFunc1 );
@@ -423,7 +427,7 @@ double Abc_NtkSpacePercentage( Abc_Obj_t * pNode )
     Vec_PtrForEachEntry( vNodes, pObj, i )
         pObj->pCopy = (Abc_Obj_t *)dd->vars[i];
     // build the BDD of the cone
-    bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR );  Cudd_Ref( bFunc );
+    bFunc = Abc_NodeGlobalBdds_rec( dd, pNodeR, 10000000 );  Cudd_Ref( bFunc );
     bFunc = Cudd_NotCond( bFunc, pNode != pNodeR );
     // count minterms
     Result = Cudd_CountMinterm( dd, bFunc, dd->size );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index 6791f08c..d299a29d 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -644,7 +644,7 @@ void Abc_NtkPrintGates( Abc_Ntk_t * pNtk, int fUseLibrary )
 
     // transform logic functions from BDD to SOP
     if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk, 0);
 
     // get hold of the SOP of the node
     CountConst = CountBuf = CountInv = CountAnd = CountOr = CountOther = CounterTotal = 0;
diff --git a/src/base/abci/abcProve.c b/src/base/abci/abcProve.c
index 18ee9a3f..ae4bb250 100644
--- a/src/base/abci/abcProve.c
+++ b/src/base/abci/abcProve.c
@@ -29,7 +29,7 @@ extern int  Abc_NtkRewrite( Abc_Ntk_t * pNtk, int fUpdateLevel, int fUseZeros, i
 extern int  Abc_NtkRefactor( Abc_Ntk_t * pNtk, int nNodeSizeMax, int nConeSizeMax, bool fUpdateLevel, bool fUseZeros, bool fUseDcs, bool fVerbose );
 extern Abc_Ntk_t * Abc_NtkFromFraig( Fraig_Man_t * pMan, Abc_Ntk_t * pNtk );
 
-static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue );
+static Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue, int * pNumFails );
 static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fVerbose );
 
 ////////////////////////////////////////////////////////////////////////
@@ -53,8 +53,8 @@ static void Abc_NtkMiterPrint( Abc_Ntk_t * pNtk, char * pString, int clk, int fV
 int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fUseRewrite, int fUseFraig, int fVerbose )
 {
     Abc_Ntk_t * pNtk, * pNtkTemp;
-    int nConfsStart = 1000, nImpsStart = 0, nBTLimitStart = 2;
-    int nConfs, nImps, nBTLimit, RetValue;
+    int nConfsStart = 1000, nImpsStart = 0, nBTLimitStart = 2;  // was 5000
+    int nConfs, nImps, nBTLimit, RetValue, nSatFails;
     int nIter = 0, clk, timeStart = clock();
 
     // get the starting network
@@ -85,7 +85,10 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fU
         nIter++;
 
         if ( fVerbose )
+        {
             printf( "ITERATION %2d : Confs = %6d. FraigBTL = %3d. \n", nIter, nConfs, nBTLimit );
+            fflush( stdout );
+        }
 
         // try brute-force SAT
         clk = clock();
@@ -116,25 +119,30 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fU
         {
             // try FRAIGing
             clk = clock();
-            pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, nBTLimit, &RetValue );  Abc_NtkDelete( pNtkTemp );
+            pNtk = Abc_NtkMiterFraig( pNtkTemp = pNtk, nBTLimit, &RetValue, &nSatFails );  Abc_NtkDelete( pNtkTemp );
             Abc_NtkMiterPrint( pNtk, "FRAIGing   ", clk, fVerbose );
+//            printf( "NumFails = %d\n", nSatFails );
             if ( RetValue >= 0 )
                 break;
         }
+        else
+            nSatFails = 1000;
 
         // increase resource limits
-        nConfs   = ABC_MIN( nConfs * 3 / 2, 1000000000 );
+//        nConfs   = ABC_MIN( nConfs * 3 / 2, 1000000000 );   // was 4/2
+        nConfs   = nSatFails * nBTLimit / 2;   
         nImps    = ABC_MIN( nImps  * 3 / 2, 1000000000 );
         nBTLimit = ABC_MIN( nBTLimit * 8,   1000000000 );
 
         // timeout at 5 minutes
-        if ( clock() - timeStart >= 300 * CLOCKS_PER_SEC )
-            break;
-        if ( nIter == 4 )
+//        if ( clock() - timeStart >= 1200 * CLOCKS_PER_SEC )
+//            break;
+        if ( nIter == 7 )
             break;
     }    
-    while ( (nConfLimit == 0 || nConfs <= nConfLimit) && 
-            (nImpLimit  == 0 || nImps  <= nImpLimit ) );
+//    while ( (nConfLimit == 0 || nConfs <= nConfLimit) && 
+//            (nImpLimit  == 0 || nImps  <= nImpLimit ) );
+    while ( 1 );
 
     // try to prove it using brute force SAT
     if ( RetValue < 0 )
@@ -144,6 +152,12 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fU
         Abc_NtkMiterPrint( pNtk, "SAT solving", clk, fVerbose );
     }
 
+    // assign the model if it was proved by rewriting (const 1 miter)
+    if ( RetValue == 0 && pNtk->pModel == NULL )
+    {
+        pNtk->pModel = ALLOC( int, Abc_NtkCiNum(pNtk) );
+        memset( pNtk->pModel, 0, sizeof(int) * Abc_NtkCiNum(pNtk) );
+    }
     *ppNtk = pNtk;
     return RetValue;
 }
@@ -159,7 +173,7 @@ int Abc_NtkMiterProve( Abc_Ntk_t ** ppNtk, int nConfLimit, int nImpLimit, int fU
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue )
+Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue, int * pNumFails )
 {
     Abc_Ntk_t * pNtkNew;
     Fraig_Params_t Params, * pParams = &Params;
@@ -190,19 +204,24 @@ Abc_Ntk_t * Abc_NtkMiterFraig( Abc_Ntk_t * pNtk, int nBTLimit, int * pRetValue )
     Fraig_ManProveMiter( pMan );
     RetValue = Fraig_ManCheckMiter( pMan );
 
+    // create the network 
+    pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
+
     // save model
     if ( RetValue == 0 )
     {
         pModel = Fraig_ManReadModel( pMan );
-        FREE( pNtk->pModel );
-        pNtk->pModel = ALLOC( int, Abc_NtkCiNum(pNtk) );
-        memcpy( pNtk->pModel, pModel, sizeof(int) * Abc_NtkCiNum(pNtk) );
+        FREE( pNtkNew->pModel );
+        pNtkNew->pModel = ALLOC( int, Abc_NtkCiNum(pNtkNew) );
+        memcpy( pNtkNew->pModel, pModel, sizeof(int) * Abc_NtkCiNum(pNtkNew) );
     }
-    // create the network 
-    pNtkNew = Abc_NtkFromFraig( pMan, pNtk );
+
+    // save the return values
+    *pRetValue = RetValue;
+    *pNumFails = Fraig_ManReadSatFails( pMan );
+
     // delete the fraig manager
     Fraig_ManFree( pMan );
-    *pRetValue = RetValue;
     return pNtkNew;
 }
 
diff --git a/src/base/abci/abcReconv.c b/src/base/abci/abcReconv.c
index 2a7188f0..100551c7 100644
--- a/src/base/abci/abcReconv.c
+++ b/src/base/abci/abcReconv.c
@@ -489,18 +489,20 @@ void Abc_NodeConeMarkCollect_rec( Abc_Obj_t * pNode, Vec_Ptr_t * vVisited )
   SeeAlso     []
 
 ***********************************************************************/
-DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pNode, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited )
+DdNode * Abc_NodeConeBdd( DdManager * dd, DdNode ** pbVars, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vVisited )
 {
+    Abc_Obj_t * pNode;
     DdNode * bFunc0, * bFunc1, * bFunc;
     int i;
     // get the nodes in the cut without fanins in the DFS order
-    Abc_NodeConeCollect( &pNode, 1, vLeaves, vVisited, 0 );
+    Abc_NodeConeCollect( &pRoot, 1, vLeaves, vVisited, 0 );
     // set the elementary BDDs
     Vec_PtrForEachEntry( vLeaves, pNode, i )
         pNode->pCopy = (Abc_Obj_t *)pbVars[i];
     // compute the BDDs for the collected nodes
     Vec_PtrForEachEntry( vVisited, pNode, i )
     {
+        assert( !Abc_ObjIsPi(pNode) );
         bFunc0 = Cudd_NotCond( Abc_ObjFanin0(pNode)->pCopy, Abc_ObjFaninC0(pNode) );
         bFunc1 = Cudd_NotCond( Abc_ObjFanin1(pNode)->pCopy, Abc_ObjFaninC1(pNode) );
         bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );    Cudd_Ref( bFunc );
diff --git a/src/base/abci/abcRenode.c b/src/base/abci/abcRenode.c
index cfb05aee..ea728858 100644
--- a/src/base/abci/abcRenode.c
+++ b/src/base/abci/abcRenode.c
@@ -33,6 +33,7 @@ static void        Abc_NtkRenodeSetBounds( Abc_Ntk_t * pNtk, int nThresh, int nF
 static void        Abc_NtkRenodeSetBoundsCnf( Abc_Ntk_t * pNtk );
 static void        Abc_NtkRenodeSetBoundsMulti( Abc_Ntk_t * pNtk, int nThresh );
 static void        Abc_NtkRenodeSetBoundsSimple( Abc_Ntk_t * pNtk );
+static void        Abc_NtkRenodeSetBoundsFactor( Abc_Ntk_t * pNtk );
 static void        Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone );
 
 ////////////////////////////////////////////////////////////////////////
@@ -50,7 +51,7 @@ static void        Abc_NtkRenodeCone( Abc_Obj_t * pNode, Vec_Ptr_t * vCone );
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple )
+Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCnf, int fMulti, int fSimple, int fFactor )
 {
     Abc_Ntk_t * pNtkNew;
 
@@ -69,6 +70,8 @@ Abc_Ntk_t * Abc_NtkRenode( Abc_Ntk_t * pNtk, int nThresh, int nFaninMax, int fCn
         Abc_NtkRenodeSetBoundsMulti( pNtk, nThresh );
     else if ( fSimple )
         Abc_NtkRenodeSetBoundsSimple( pNtk );
+    else if ( fFactor )
+        Abc_NtkRenodeSetBoundsFactor( pNtk );
     else
         Abc_NtkRenodeSetBounds( pNtk, nThresh, nFaninMax );
 
@@ -564,6 +567,32 @@ void Abc_NtkRenodeSetBoundsSimple( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Sets a factor-cut boundary.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_NtkRenodeSetBoundsFactor( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    // make sure the mark is not set
+    Abc_NtkForEachObj( pNtk, pNode, i )
+        assert( pNode->fMarkA == 0 );
+    // mark the nodes where expansion stops using pNode->fMarkA
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        pNode->fMarkA = (pNode->vFanouts.nSize > 1 && !Abc_NodeIsMuxControlType(pNode));
+    // mark the PO drivers
+    Abc_NtkForEachCo( pNtk, pNode, i )
+        Abc_ObjFanin0(pNode)->fMarkA = 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Collects the fanins of a large node.]
 
   Description []
diff --git a/src/base/abci/abcRestruct.c b/src/base/abci/abcRestruct.c
index 137573a5..32e878b8 100644
--- a/src/base/abci/abcRestruct.c
+++ b/src/base/abci/abcRestruct.c
@@ -332,9 +332,15 @@ Dec_Graph_t * Abc_NodeRestructureCut( Abc_ManRst_t * p, Abc_Obj_t * pRoot, Cut_C
             return NULL;
         Vec_PtrPush( p->vLeaves, pLeaf );
     }
+
+    if ( pRoot->Id == 29 )
+    {
+        int x = 0;
+    }
+
 clk = clock();
     // collect the internal nodes of the cut
-    Abc_NodeConeCollect( &pRoot, 1, p->vLeaves, p->vVisited, 0 );
+//    Abc_NodeConeCollect( &pRoot, 1, p->vLeaves, p->vVisited, 0 );
     // derive the BDD of the cut
     bFunc = Abc_NodeConeBdd( p->dd, p->dd->vars, pRoot, p->vLeaves, p->vVisited );  Cudd_Ref( bFunc );
 p->timeBdd += clock() - clk;
diff --git a/src/base/abci/abcResub.c b/src/base/abci/abcResub.c
new file mode 100644
index 00000000..30e2eca2
--- /dev/null
+++ b/src/base/abci/abcResub.c
@@ -0,0 +1,801 @@
+/**CFile****************************************************************
+
+  FileName    [abcResub.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Network and node package.]
+
+  Synopsis    [Resubstitution manager.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: abcResub.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "dec.h"
+ 
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Abc_ResubMan_t_ Abc_ResubMan_t;
+struct Abc_ResubMan_t_
+{
+    // paramers
+    int                nLeavesMax; // the max number of leaves in the cone
+    int                nDivsMax;   // the max number of divisors in the cone
+    // representation of the cone
+    Abc_Obj_t *        pRoot;      // the root of the cone
+    int                nLeaves;    // the number of leaves
+    int                nDivs;      // the number of all divisor (including leaves)
+    int                nMffc;      // the size of MFFC
+    Vec_Ptr_t *        vDivs;      // the divisors
+    // representation of the simulation info
+    int                nBits;      // the number of simulation bits
+    int                nWords;     // the number of unsigneds for siminfo
+    Vec_Ptr_t        * vSims;      // simulation info
+    unsigned         * pInfo;      // pointer to simulation info
+    // internal divisor storage
+    Vec_Ptr_t        * vDivs1U;    // the single-node unate divisors
+    Vec_Ptr_t        * vDivs1B;    // the single-node binate divisors
+    Vec_Ptr_t        * vDivs2U0;   // the double-node unate divisors
+    Vec_Ptr_t        * vDivs2U1;   // the double-node unate divisors
+    // other data
+    Vec_Ptr_t        * vTemp;      // temporary array of nodes
+};
+
+
+// external procedures
+extern Abc_ResubMan_t * Abc_ResubManStart( int nLeavesMax, int nDivsMax );
+extern void             Abc_ResubManStop( Abc_ResubMan_t * p );
+extern Dec_Graph_t *    Abc_ResubManEval( Abc_ResubMan_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int nSteps );
+
+
+static int  Abc_ResubManCollectDivs( Abc_ResubMan_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves );
+static int  Abc_ResubManMffc( Abc_ResubMan_t * p, Vec_Ptr_t * vDivs, Abc_Obj_t * pRoot, int nLeaves );
+static void Abc_ResubManSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, int nLeavesMax, int nWords );
+
+static Dec_Graph_t * Abc_ResubManQuit( Abc_ResubMan_t * p );
+static Dec_Graph_t * Abc_ResubManDivs0( Abc_ResubMan_t * p );
+static Dec_Graph_t * Abc_ResubManDivs1( Abc_ResubMan_t * p );
+static Dec_Graph_t * Abc_ResubManDivsD( Abc_ResubMan_t * p );
+static Dec_Graph_t * Abc_ResubManDivs2( Abc_ResubMan_t * p );
+static Dec_Graph_t * Abc_ResubManDivs3( Abc_ResubMan_t * p );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_ResubMan_t * Abc_ResubManStart( int nLeavesMax, int nDivsMax )
+{
+    Abc_ResubMan_t * p;
+    unsigned * pData;
+    int i, k;
+    p = ALLOC( Abc_ResubMan_t, 1 );
+    memset( p, 0, sizeof(Abc_ResubMan_t) );
+    p->nLeavesMax = nLeavesMax;
+    p->nDivsMax   = nDivsMax;
+    p->vDivs      = Vec_PtrAlloc( p->nDivsMax );
+    // allocate simulation info
+    p->nBits      = (1 << p->nLeavesMax);
+    p->nWords     = (p->nBits <= 32)? 1 : p->nBits / sizeof(unsigned) / 8;
+    p->pInfo      = ALLOC( unsigned, p->nWords * p->nDivsMax );
+    memset( p->pInfo, 0, sizeof(unsigned) * p->nWords * p->nLeavesMax );
+    p->vSims      = Vec_PtrAlloc( p->nDivsMax );
+    for ( i = 0; i < p->nDivsMax; i++ )
+        Vec_PtrPush( p->vSims, p->pInfo + i * p->nWords );
+    // set elementary truth tables
+    for ( k = 0; k < p->nLeavesMax; k++ )
+    {
+        pData = p->vSims->pArray[k];
+        for ( i = 0; i < p->nBits; i++ )
+            if ( i & (1 << k) )
+                pData[i/32] |= (1 << (i%32));
+    }
+    // create the remaining divisors
+    p->vDivs1U  = Vec_PtrAlloc( p->nDivsMax );
+    p->vDivs1B  = Vec_PtrAlloc( p->nDivsMax );
+    p->vDivs2U0 = Vec_PtrAlloc( p->nDivsMax );
+    p->vDivs2U1 = Vec_PtrAlloc( p->nDivsMax );
+    p->vTemp    = Vec_PtrAlloc( p->nDivsMax );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ResubManStop( Abc_ResubMan_t * p )
+{
+    Vec_PtrFree( p->vDivs );
+    Vec_PtrFree( p->vSims );
+    Vec_PtrFree( p->vDivs1U );
+    Vec_PtrFree( p->vDivs1B );
+    Vec_PtrFree( p->vDivs2U0 );
+    Vec_PtrFree( p->vDivs2U1 );
+    Vec_PtrFree( p->vTemp );
+    free( p->pInfo );
+    free( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Evaluates resubstution of one cut.]
+
+  Description [Returns the graph to add if any.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Graph_t * Abc_ResubManEval( Abc_ResubMan_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves, int nSteps )
+{
+    Dec_Graph_t * pGraph;
+    assert( nSteps >= 0 );
+    assert( nSteps <= 3 );
+    // get the number of leaves
+    p->pRoot = pRoot;
+    p->nLeaves = Vec_PtrSize(vLeaves);
+    // collect the divisor nodes
+    Abc_ResubManCollectDivs( p, pRoot, vLeaves );
+    // quit if the number of divisors collected is too large
+    if ( Vec_PtrSize(p->vDivs) - p->nLeaves > p->nDivsMax - p->nLeavesMax )
+        return NULL;
+    // get the number nodes in its MFFC (and reorder the nodes)
+    p->nMffc = Abc_ResubManMffc( p, p->vDivs, pRoot, p->nLeaves );
+    assert( p->nMffc > 0 );
+    // get the number of divisors
+    p->nDivs = Vec_PtrSize(p->vDivs) - p->nMffc;
+    // simulate the nodes
+    Abc_ResubManSimulate( p->vDivs, p->nLeaves, p->vSims, p->nLeavesMax, p->nWords );
+
+    // consider constants
+    if ( pGraph = Abc_ResubManQuit( p ) )
+        return pGraph;
+
+    // consider equal nodes
+    if ( pGraph = Abc_ResubManDivs0( p ) )
+        return pGraph;
+    if ( nSteps == 0 || p->nLeavesMax == 1 )
+        return NULL;
+
+    // consider one node
+    if ( pGraph = Abc_ResubManDivs1( p ) )
+        return pGraph;
+    if ( nSteps == 1 || p->nLeavesMax == 2 )
+        return NULL;
+
+    // get the two level divisors
+    Abc_ResubManDivsD( p );
+
+    // consider two nodes
+    if ( pGraph = Abc_ResubManDivs2( p ) )
+        return pGraph;
+    if ( nSteps == 2 || p->nLeavesMax == 3 )
+        return NULL;
+
+    // consider two nodes
+    if ( pGraph = Abc_ResubManDivs3( p ) )
+        return pGraph;
+    if ( nSteps == 3 || p->nLeavesMax == 4 )
+        return NULL;
+    return NULL;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ResubManCollectDivs( Abc_ResubMan_t * p, Abc_Obj_t * pRoot, Vec_Ptr_t * vLeaves )
+{
+    Abc_Obj_t * pNode, * pFanout;
+    int i, k;
+    // collect the leaves of the cut
+    Vec_PtrClear( p->vDivs );
+    Abc_NtkIncrementTravId( pRoot->pNtk );
+    Vec_PtrForEachEntry( vLeaves, pNode, i )
+    {
+        Vec_PtrPush( p->vDivs, pNode );
+        Abc_NodeSetTravIdCurrent( pNode );        
+    }
+    // explore the fanouts
+    Vec_PtrForEachEntry( p->vDivs, pNode, i )
+    {
+        // if the fanout has both fanins in the set, add it
+        Abc_ObjForEachFanout( pNode, pFanout, k )
+        {
+            if ( Abc_NodeIsTravIdCurrent(pFanout) || Abc_ObjIsPo(pFanout) )
+                continue;
+            if ( Abc_NodeIsTravIdCurrent(Abc_ObjFanin0(pFanout)) && Abc_NodeIsTravIdCurrent(Abc_ObjFanin1(pFanout)) )
+            {
+                Vec_PtrPush( p->vDivs, pFanout );
+                Abc_NodeSetTravIdCurrent( pFanout );     
+            }
+        }
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ResubManMffc_rec( Abc_Obj_t * pNode )
+{
+    if ( Abc_NodeIsTravIdCurrent(pNode) )
+        return 0;
+    Abc_NodeSetTravIdCurrent( pNode ); 
+    return 1 + Abc_ResubManMffc_rec( Abc_ObjFanin0(pNode) ) +
+        Abc_ResubManMffc_rec( Abc_ObjFanin1(pNode) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_ResubManMffc( Abc_ResubMan_t * p, Vec_Ptr_t * vDivs, Abc_Obj_t * pRoot, int nLeaves )
+{
+    Abc_Obj_t * pObj;
+    int Counter, i, k;
+    // increment the traversal ID for the leaves
+    Abc_NtkIncrementTravId( pRoot->pNtk );
+    // label the leaves
+    Vec_PtrForEachEntryStop( vDivs, pObj, i, nLeaves )
+        Abc_NodeSetTravIdCurrent( pObj ); 
+    // make sure the node is in the cone and is no one of the leaves
+    assert( Abc_NodeIsTravIdPrevious(pRoot) );
+    Counter = Abc_ResubManMffc_rec( pRoot );
+    // move the labeled nodes to the end 
+    Vec_PtrClear( p->vTemp );
+    k = 0;
+    Vec_PtrForEachEntryStart( vDivs, pObj, i, nLeaves )
+        if ( Abc_NodeIsTravIdCurrent(pObj) )
+            Vec_PtrPush( p->vTemp, pObj );
+        else
+            Vec_PtrWriteEntry( vDivs, k++, pObj );
+    // add the labeled nodes
+    Vec_PtrForEachEntry( p->vTemp, pObj, i )
+        Vec_PtrWriteEntry( vDivs, k++, pObj );
+    assert( k == Vec_PtrSize(p->vDivs) );
+    assert( pRoot == Vec_PtrEntryLast(p->vDivs) );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs simulation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_ResubManSimulate( Vec_Ptr_t * vDivs, int nLeaves, Vec_Ptr_t * vSims, int nLeavesMax, int nWords )
+{
+    Abc_Obj_t * pObj;
+    unsigned * puData0, * puData1, * puData;
+    int i, k;
+    // initialize random simulation data
+    Vec_PtrForEachEntryStop( vDivs, pObj, i, nLeaves )
+        pObj->pData = Vec_PtrEntry( vSims, i );
+    // simulate
+    Vec_PtrForEachEntryStart( vDivs, pObj, i, nLeaves )
+    {
+        pObj->pData = Vec_PtrEntry( vSims, i + nLeavesMax );
+        puData0 = Abc_ObjFanin0(pObj)->pData;
+        puData1 = Abc_ObjFanin1(pObj)->pData;
+        puData  = pObj->pData;
+        // simulate
+        if ( Abc_ObjFaninC0(pObj) && Abc_ObjFaninC1(pObj) )
+            for ( k = 0; k < nWords; k++ )
+                puData[k] = ~puData0[k] & ~puData1[k];
+        else if ( Abc_ObjFaninC0(pObj) )
+            for ( k = 0; k < nWords; k++ )
+                puData[k] = ~puData0[k] & puData1[k];
+        else if ( Abc_ObjFaninC1(pObj) )
+            for ( k = 0; k < nWords; k++ )
+                puData[k] = puData0[k] & ~puData1[k];
+        else 
+            for ( k = 0; k < nWords; k++ )
+                puData[k] = puData0[k] & puData1[k];
+    }
+    // complement if needed
+    Vec_PtrForEachEntry( vDivs, pObj, i )
+    {
+        puData = pObj->pData;
+        pObj->fPhase = (puData[0] & 1);
+        if ( pObj->fPhase )
+            for ( k = 0; k < nWords; k++ )
+                puData[k] = ~puData[k];
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Graph_t * Abc_ResubManQuit( Abc_ResubMan_t * p )
+{
+    Dec_Graph_t * pGraph;
+    unsigned * upData;
+    int w;
+    upData = p->pRoot->pData;
+    for ( w = 0; w < p->nWords; w++ )
+        if ( upData[0] == 0 )
+            break;
+    if ( w != p->nWords )
+        return NULL;
+    // get the graph if the node looks constant
+    if ( p->pRoot->fPhase )
+        pGraph = Dec_GraphCreateConst1();
+    else 
+        pGraph = Dec_GraphCreateConst0();
+    return pGraph;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Graph_t * Abc_ResubManQuit0( Abc_Obj_t * pRoot, Abc_Obj_t * pObj )
+{
+    Dec_Graph_t * pGraph;
+    Dec_Edge_t eRoot;
+    pGraph = Dec_GraphCreate( 1 );
+    Dec_GraphNode( pGraph, 0 )->pFunc = pObj;
+    eRoot = Dec_EdgeCreate( 0, pObj->fPhase );
+    Dec_GraphSetRoot( pGraph, eRoot );
+    if ( pRoot->fPhase )
+        Dec_GraphComplement( pGraph );
+    return pGraph;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Graph_t * Abc_ResubManQuit1( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1 )
+{
+    Dec_Graph_t * pGraph;
+    Dec_Edge_t eRoot, eNode0, eNode1;
+    assert( !Abc_ObjIsComplement(pObj0) );
+    assert( !Abc_ObjIsComplement(pObj1) );
+    pGraph = Dec_GraphCreate( 2 );
+    Dec_GraphNode( pGraph, 0 )->pFunc = pObj0;
+    Dec_GraphNode( pGraph, 1 )->pFunc = pObj1;
+    eNode0 = Dec_EdgeCreate( 0, pObj0->fPhase );
+    eNode1 = Dec_EdgeCreate( 1, pObj1->fPhase );
+    eRoot  = Dec_GraphAddNodeOr( pGraph, eNode0, eNode1 );
+    Dec_GraphSetRoot( pGraph, eRoot );
+    if ( pRoot->fPhase )
+        Dec_GraphComplement( pGraph );
+    return pGraph;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Graph_t * Abc_ResubManQuit2( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1, Abc_Obj_t * pObj2 )
+{
+    Dec_Graph_t * pGraph;
+    Dec_Edge_t eRoot, eAnd, eNode0, eNode1, eNode2;
+    assert( !Abc_ObjIsComplement(pObj0) );
+    pGraph = Dec_GraphCreate( 3 );
+    Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0);
+    Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1);
+    Dec_GraphNode( pGraph, 2 )->pFunc = Abc_ObjRegular(pObj2);
+    eNode0 = Dec_EdgeCreate( 0, Abc_ObjIsComplement(pObj0) ^ pObj0->fPhase );
+    eNode1 = Dec_EdgeCreate( 1, Abc_ObjIsComplement(pObj1) ^ pObj1->fPhase );
+    eNode2 = Dec_EdgeCreate( 2, Abc_ObjIsComplement(pObj2) ^ pObj2->fPhase );
+    eAnd   = Dec_GraphAddNodeAnd( pGraph, eNode1, eNode2 );
+    eRoot  = Dec_GraphAddNodeOr( pGraph, eNode0, eAnd );
+    Dec_GraphSetRoot( pGraph, eRoot );
+    if ( pRoot->fPhase )
+        Dec_GraphComplement( pGraph );
+    return pGraph;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Graph_t * Abc_ResubManQuit3( Abc_Obj_t * pRoot, Abc_Obj_t * pObj0, Abc_Obj_t * pObj1, Abc_Obj_t * pObj2, Abc_Obj_t * pObj3 )
+{
+    Dec_Graph_t * pGraph;
+    Dec_Edge_t eRoot, eAnd0, eAnd1, eNode0, eNode1, eNode2, eNode3;
+    pGraph = Dec_GraphCreate( 4 );
+    Dec_GraphNode( pGraph, 0 )->pFunc = Abc_ObjRegular(pObj0);
+    Dec_GraphNode( pGraph, 1 )->pFunc = Abc_ObjRegular(pObj1);
+    Dec_GraphNode( pGraph, 2 )->pFunc = Abc_ObjRegular(pObj2);
+    Dec_GraphNode( pGraph, 3 )->pFunc = Abc_ObjRegular(pObj3);
+    eNode0 = Dec_EdgeCreate( 0, Abc_ObjIsComplement(pObj0) ^ pObj0->fPhase );
+    eNode1 = Dec_EdgeCreate( 1, Abc_ObjIsComplement(pObj1) ^ pObj1->fPhase );
+    eNode2 = Dec_EdgeCreate( 2, Abc_ObjIsComplement(pObj2) ^ pObj2->fPhase );
+    eNode3 = Dec_EdgeCreate( 3, Abc_ObjIsComplement(pObj3) ^ pObj3->fPhase );
+    eAnd0  = Dec_GraphAddNodeAnd( pGraph, eNode0, eNode1 );
+    eAnd1  = Dec_GraphAddNodeAnd( pGraph, eNode2, eNode3 );
+    eRoot  = Dec_GraphAddNodeOr( pGraph, eAnd0, eAnd1 );
+    Dec_GraphSetRoot( pGraph, eRoot );
+    if ( pRoot->fPhase )
+        Dec_GraphComplement( pGraph );
+    return pGraph;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives unate/binate divisors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Graph_t * Abc_ResubManDivs0( Abc_ResubMan_t * p )
+{
+    Abc_Obj_t * pObj;
+    unsigned * puData, * puDataR;
+    int i, w;
+    Vec_PtrClear( p->vDivs1U );
+    Vec_PtrClear( p->vDivs1B );
+    puDataR = p->pRoot->pData;
+    Vec_PtrForEachEntryStop( p->vDivs, pObj, i, p->nDivs )
+    {
+        puData = pObj->pData;
+        for ( w = 0; w < p->nWords; w++ )
+            if ( puData[w] != puDataR[w] )
+                break;
+        if ( w == p->nWords )
+            return Abc_ResubManQuit0( p->pRoot, pObj );
+        for ( w = 0; w < p->nWords; w++ )
+            if ( puData[w] & ~puDataR[w] )
+                break;
+        if ( w == p->nWords )
+            Vec_PtrPush( p->vDivs1U, pObj );
+        else
+            Vec_PtrPush( p->vDivs1B, pObj );
+    }
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives unate/binate divisors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Graph_t * Abc_ResubManDivs1( Abc_ResubMan_t * p )
+{
+    Abc_Obj_t * pObj0, * pObj1;
+    unsigned * puData0, * puData1, * puDataR;
+    int i, k, w;
+    puDataR = p->pRoot->pData;
+    Vec_PtrForEachEntry( p->vDivs1U, pObj0, i )
+    {
+        puData0 = pObj0->pData;
+        Vec_PtrForEachEntryStart( p->vDivs1U, pObj1, k, i + 1 )
+        {
+            puData1 = pObj1->pData;
+            for ( w = 0; w < p->nWords; w++ )
+                if ( (puData0[w] | puData1[w]) != puDataR[w] )
+                    break;
+            if ( w == p->nWords )
+                return Abc_ResubManQuit1( p->pRoot, pObj0, pObj1 );
+        }
+    }
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives unate/binate divisors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Graph_t * Abc_ResubManDivsD( Abc_ResubMan_t * p )
+{
+    Abc_Obj_t * pObj0, * pObj1;
+    unsigned * puData0, * puData1, * puDataR;
+    int i, k, w;
+    Vec_PtrClear( p->vDivs2U0 );
+    Vec_PtrClear( p->vDivs2U1 );
+    puDataR = p->pRoot->pData;
+    Vec_PtrForEachEntry( p->vDivs1U, pObj0, i )
+    {
+        puData0 = pObj0->pData;
+        Vec_PtrForEachEntryStart( p->vDivs1U, pObj1, k, i + 1 )
+        {
+            puData1 = pObj1->pData;
+
+            for ( w = 0; w < p->nWords; w++ )
+                if ( (puData0[w] & puData1[w]) & ~puDataR[w] )
+                    break;
+            if ( w == p->nWords )
+            {
+                Vec_PtrPush( p->vDivs2U0, pObj0 );
+                Vec_PtrPush( p->vDivs2U1, pObj1 );
+            }
+
+            for ( w = 0; w < p->nWords; w++ )
+                if ( (~puData0[w] & puData1[w]) & ~puDataR[w] )
+                    break;
+            if ( w == p->nWords )
+            {
+                Vec_PtrPush( p->vDivs2U0, Abc_ObjNot(pObj0) );
+                Vec_PtrPush( p->vDivs2U1, pObj1 );
+            }
+
+            for ( w = 0; w < p->nWords; w++ )
+                if ( (puData0[w] & ~puData1[w]) & ~puDataR[w] )
+                    break;
+            if ( w == p->nWords )
+            {
+                Vec_PtrPush( p->vDivs2U0, pObj0 );
+                Vec_PtrPush( p->vDivs2U1, Abc_ObjNot(pObj1) );
+            }
+        }
+    }
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives unate/binate divisors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Graph_t * Abc_ResubManDivs2( Abc_ResubMan_t * p )
+{
+    Abc_Obj_t * pObj0, * pObj1, * pObj2;
+    unsigned * puData0, * puData1, * puData2, * puDataR;
+    int i, k, w;
+    puDataR = p->pRoot->pData;
+    Vec_PtrForEachEntry( p->vDivs1U, pObj0, i )
+    {
+        puData0 = pObj0->pData;
+        Vec_PtrForEachEntryStart( p->vDivs2U0, pObj1, k, i + 1 )
+        {
+            pObj2 = Vec_PtrEntry( p->vDivs2U1, k );
+            puData1 = Abc_ObjRegular(pObj1)->pData;
+            puData2 = Abc_ObjRegular(pObj2)->pData;
+
+            if ( !Abc_ObjFaninC0(pObj1) && !Abc_ObjFaninC1(pObj2) )
+            {
+                for ( w = 0; w < p->nWords; w++ )
+                    if ( (puData0[w] | (puData1[w] & puData2[w])) != puDataR[w] )
+                        break;
+            }
+            else if ( Abc_ObjFaninC0(pObj1) )
+            {
+                for ( w = 0; w < p->nWords; w++ )
+                    if ( (puData0[w] | (~puData1[w] & puData2[w])) != puDataR[w] )
+                        break;
+            }
+            else if ( Abc_ObjFaninC1(pObj2) )
+            {
+                for ( w = 0; w < p->nWords; w++ )
+                    if ( (puData0[w] | (puData1[w] & ~puData2[w])) != puDataR[w] )
+                        break;
+            }
+            else assert( 0 );
+            if ( w == p->nWords )
+                return Abc_ResubManQuit2( p->pRoot, pObj0, pObj1, pObj2 );
+        }
+    }
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives unate/binate divisors.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Dec_Graph_t * Abc_ResubManDivs3( Abc_ResubMan_t * p )
+{
+    Abc_Obj_t * pObj0, * pObj1, * pObj2, * pObj3;
+    unsigned * puData0, * puData1, * puData2, * puData3, * puDataR;
+    int i, k, w;
+    puDataR = p->pRoot->pData;
+    Vec_PtrForEachEntry( p->vDivs2U0, pObj0, i )
+    {
+        pObj1 = Vec_PtrEntry( p->vDivs2U1, i );
+        puData0 = Abc_ObjRegular(pObj0)->pData;
+        puData1 = Abc_ObjRegular(pObj1)->pData;
+
+        Vec_PtrForEachEntryStart( p->vDivs2U0, pObj2, k, i + 1 )
+        {
+            pObj3 = Vec_PtrEntry( p->vDivs2U1, k );
+            puData2 = Abc_ObjRegular(pObj2)->pData;
+            puData3 = Abc_ObjRegular(pObj3)->pData;
+
+            if ( !Abc_ObjFaninC0(pObj0) && !Abc_ObjFaninC1(pObj1) )
+            {
+                if ( !Abc_ObjFaninC0(pObj2) && !Abc_ObjFaninC1(pObj3) )
+                {
+                    for ( w = 0; w < p->nWords; w++ )
+                        if ( ((puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
+                            break;
+                }
+                else if ( Abc_ObjFaninC0(pObj2) )
+                {
+                    for ( w = 0; w < p->nWords; w++ )
+                        if ( ((puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
+                            break;
+                }
+                else if ( Abc_ObjFaninC0(pObj3) )
+                {
+                    for ( w = 0; w < p->nWords; w++ )
+                        if ( ((puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
+                            break;
+                }
+                else assert( 0 );
+            }
+            else if ( Abc_ObjFaninC0(pObj0) )
+            {
+                if ( !Abc_ObjFaninC0(pObj2) && !Abc_ObjFaninC1(pObj3) )
+                {
+                    for ( w = 0; w < p->nWords; w++ )
+                        if ( ((~puData0[w] & puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
+                            break;
+                }
+                else if ( Abc_ObjFaninC0(pObj2) )
+                {
+                    for ( w = 0; w < p->nWords; w++ )
+                        if ( ((~puData0[w] & puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
+                            break;
+                }
+                else if ( Abc_ObjFaninC0(pObj3) )
+                {
+                    for ( w = 0; w < p->nWords; w++ )
+                        if ( ((~puData0[w] & puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
+                            break;
+                }
+                else assert( 0 );
+            }
+            else if ( Abc_ObjFaninC1(pObj1) )
+            {
+                if ( !Abc_ObjFaninC0(pObj2) && !Abc_ObjFaninC1(pObj3) )
+                {
+                    for ( w = 0; w < p->nWords; w++ )
+                        if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & puData3[w])) != puDataR[w] )
+                            break;
+                }
+                else if ( Abc_ObjFaninC0(pObj2) )
+                {
+                    for ( w = 0; w < p->nWords; w++ )
+                        if ( ((puData0[w] & ~puData1[w]) | (~puData2[w] & puData3[w])) != puDataR[w] )
+                            break;
+                }
+                else if ( Abc_ObjFaninC0(pObj3) )
+                {
+                    for ( w = 0; w < p->nWords; w++ )
+                        if ( ((puData0[w] & ~puData1[w]) | (puData2[w] & ~puData3[w])) != puDataR[w] )
+                            break;
+                }
+                else assert( 0 );
+            }
+            else assert( 0 );
+            if ( w == p->nWords )
+                return Abc_ResubManQuit3( p->pRoot, pObj0, pObj1, pObj2, pObj3 );
+        }
+    }
+    return NULL;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 5376444b..f7400313 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -400,6 +400,10 @@ int Abc_NtkMiterSatCreateInt( solver * pSat, Abc_Ntk_t * pNtk )
 
     assert( Abc_NtkIsStrash(pNtk) );
 
+    // clean the CI node pointers
+    Abc_NtkForEachCi( pNtk, pNode, i )
+        pNode->pCopy = NULL;
+
     // start the data structures
     vNodes = Vec_PtrAlloc( 1000 );   // the nodes corresponding to vars in the solver
     vSuper = Vec_PtrAlloc( 100 );    // the nodes belonging to the given implication supergate
diff --git a/src/base/abci/abcStrash.c b/src/base/abci/abcStrash.c
index 72f4215b..fbaca324 100644
--- a/src/base/abci/abcStrash.c
+++ b/src/base/abci/abcStrash.c
@@ -58,7 +58,7 @@ Abc_Ntk_t * Abc_NtkStrash( Abc_Ntk_t * pNtk, bool fAllNodes, bool fCleanup )
     assert( !Abc_NtkIsNetlist(pNtk) );
     assert( !Abc_NtkIsSeq(pNtk) );
     if ( Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk, 0);
     // print warning about choice nodes
     if ( Abc_NtkGetChoiceNum( pNtk ) )
         printf( "Warning: The choice nodes in the initial AIG are removed by strashing.\n" );
@@ -108,7 +108,7 @@ int Abc_NtkAppend( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2 )
     assert( Abc_NtkIsStrash(pNtk1) );
     assert( Abc_NtkIsLogic(pNtk2) || Abc_NtkIsStrash(pNtk2) ); 
     if ( Abc_NtkIsBddLogic(pNtk2) )
-        Abc_NtkBddToSop(pNtk2);
+        Abc_NtkBddToSop(pNtk2, 0);
     // check that the networks have the same PIs
     // reorder PIs of pNtk2 according to pNtk1
     if ( !Abc_NtkCompareSignals( pNtk1, pNtk2, 1 ) )
diff --git a/src/base/abci/abcSweep.c b/src/base/abci/abcSweep.c
index 228e27eb..08236edc 100644
--- a/src/base/abci/abcSweep.c
+++ b/src/base/abci/abcSweep.c
@@ -545,7 +545,7 @@ int Abc_NtkSweep( Abc_Ntk_t * pNtk, int fVerbose )
     while ( nSweptNew );
     // conver back to BDD
     if ( fConvert )
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk, 0);
     // report
     if ( fVerbose )
         printf( "Sweep removed %d nodes.\n", nSwept );
diff --git a/src/base/abci/abcSymm.c b/src/base/abci/abcSymm.c
index 12cdab85..35cf896f 100644
--- a/src/base/abci/abcSymm.c
+++ b/src/base/abci/abcSymm.c
@@ -88,7 +88,7 @@ void Abc_NtkSymmetriesUsingBdds( Abc_Ntk_t * pNtk, int fNaive, int fVerbose )
 
     // compute the global functions
 clk = clock();
-    dd = Abc_NtkGlobalBdds( pNtk, 0 );
+    dd = Abc_NtkGlobalBdds( pNtk, 10000000, 0 );
     Cudd_AutodynDisable( dd );
     Cudd_zddVarsFromBddVars( dd, 2 );
 clkBdd = clock() - clk;
diff --git a/src/base/abci/abcUnate.c b/src/base/abci/abcUnate.c
index 08a42623..88188655 100644
--- a/src/base/abci/abcUnate.c
+++ b/src/base/abci/abcUnate.c
@@ -73,7 +73,7 @@ void Abc_NtkPrintUnateBdd( Abc_Ntk_t * pNtk, int fUseNaive, int fVerbose )
     int clkBdd, clkUnate;
 
     // compute the global BDDs
-    if ( Abc_NtkGlobalBdds(pNtk, 0) == NULL )
+    if ( Abc_NtkGlobalBdds(pNtk, 10000000, 0) == NULL )
         return;
 clkBdd = clock() - clk;
 
diff --git a/src/base/abci/abcUnreach.c b/src/base/abci/abcUnreach.c
index 34757145..5690013b 100644
--- a/src/base/abci/abcUnreach.c
+++ b/src/base/abci/abcUnreach.c
@@ -58,7 +58,7 @@ int Abc_NtkExtractSequentialDcs( Abc_Ntk_t * pNtk, bool fVerbose )
     }
 
     // compute the global BDDs of the latches
-    dd = Abc_NtkGlobalBdds( pNtk, 1 );    
+    dd = Abc_NtkGlobalBdds( pNtk, 10000000, 1 );    
     if ( dd == NULL )
         return 0;
     if ( fVerbose )
@@ -331,7 +331,7 @@ Abc_Ntk_t * Abc_NtkConstructExdc( DdManager * dd, Abc_Ntk_t * pNtk, DdNode * bUn
     Abc_NtkLogicMakeSimpleCos( pNtkNew, 0 );
 
     // transform the network to the SOP representation
-    Abc_NtkBddToSop( pNtkNew );
+    Abc_NtkBddToSop( pNtkNew, 0 );
     return pNtkNew;
 }
 
diff --git a/src/base/abci/abcVanEijk.c b/src/base/abci/abcVanEijk.c
index d719df4f..c178c013 100644
--- a/src/base/abci/abcVanEijk.c
+++ b/src/base/abci/abcVanEijk.c
@@ -713,7 +713,7 @@ Fraig_Man_t * Abc_NtkVanEijkFraig( Abc_Ntk_t * pMulti, int fInit )
 Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses )
 {
     Abc_Ntk_t * pNtkNew; 
-    Abc_Obj_t * pClass, * pNode, * pRepr, * pObj;
+    Abc_Obj_t * pClass, * pNode, * pRepr, * pObj, *pObjNew;
     Abc_Obj_t * pMiter, * pTotal;
     Vec_Ptr_t * vCone;
     int i, k;
@@ -766,6 +766,30 @@ Abc_Ntk_t * Abc_NtkVanEijkDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vClasses )
         pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pMiter );
     }
 
+/*
+    // create the only PO
+    pObjNew = Abc_NtkCreatePo( pNtkNew );
+    // add the PO name
+    Abc_NtkLogicStoreName( pObjNew, "DC" );
+    // add the PO
+    Abc_ObjAddFanin( pObjNew, pTotal );
+
+    // quontify the PIs existentially
+    pNtkNew = Abc_NtkMiterQuantifyPis( pNtkNew );
+
+    // get the new PO
+    pObjNew = Abc_NtkPo( pNtkNew, 0 );
+    // remember the miter output
+    pTotal = Abc_ObjChild0( pObjNew );
+    // remove the PO
+    Abc_NtkDeleteObj( pObjNew );
+
+    // make the old network point to the new things
+    Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew);
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->pCopy = Abc_NtkPi( pNtkNew, i );
+*/
+
     // for each CO, create PO (skip POs equal to CIs because of name conflict)
     Abc_NtkForEachPo( pNtk, pObj, i )
         if ( !Abc_ObjIsCi(Abc_ObjFanin0(pObj)) )
diff --git a/src/base/abci/abcVanImp.c b/src/base/abci/abcVanImp.c
index 1805378c..c92667a3 100644
--- a/src/base/abci/abcVanImp.c
+++ b/src/base/abci/abcVanImp.c
@@ -870,7 +870,7 @@ Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_I
 {
     Abc_Ntk_t * pNtkNew; 
     Vec_Ptr_t * vCone;
-    Abc_Obj_t * pObj, * pMiter, * pTotal, * pNode, * pNode1, * pNode2;
+    Abc_Obj_t * pObj, * pMiter, * pTotal, * pNode, * pNode1, * pNode2, * pObjNew;
     unsigned Imp;
     int i, k;
 
@@ -942,6 +942,29 @@ Abc_Ntk_t * Abc_NtkVanImpDeriveExdc( Abc_Ntk_t * pNtk, Vec_Ptr_t * vZeros, Vec_I
         pMiter = Abc_AigAnd( pNtkNew->pManFunc, pNode1->pCopy, Abc_ObjNot(pNode2->pCopy) );
         pTotal = Abc_AigOr( pNtkNew->pManFunc, pTotal, pMiter );
     }
+/*
+    // create the only PO
+    pObjNew = Abc_NtkCreatePo( pNtkNew );
+    // add the PO name
+    Abc_NtkLogicStoreName( pObjNew, "DC" );
+    // add the PO
+    Abc_ObjAddFanin( pObjNew, pTotal );
+
+    // quontify the PIs existentially
+    pNtkNew = Abc_NtkMiterQuantifyPis( pNtkNew );
+
+    // get the new PO
+    pObjNew = Abc_NtkPo( pNtkNew, 0 );
+    // remember the miter output
+    pTotal = Abc_ObjChild0( pObjNew );
+    // remove the PO
+    Abc_NtkDeleteObj( pObjNew );
+
+    // make the old network point to the new things
+    Abc_NtkConst1(pNtk)->pCopy = Abc_NtkConst1(pNtkNew);
+    Abc_NtkForEachCi( pNtk, pObj, i )
+        pObj->pCopy = Abc_NtkPi( pNtkNew, i );
+*/
 
     // for each CO, create PO (skip POs equal to CIs because of name conflict)
     Abc_NtkForEachPo( pNtk, pObj, i )
diff --git a/src/base/abci/abcVerify.c b/src/base/abci/abcVerify.c
index 5c7b525e..718ad657 100644
--- a/src/base/abci/abcVerify.c
+++ b/src/base/abci/abcVerify.c
@@ -26,8 +26,6 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
  
-static int * Abc_NtkVerifyGetCleanModel( Abc_Ntk_t * pNtk, int nFrames );
-static int * Abc_NtkVerifySimulatePattern( Abc_Ntk_t * pNtk, int * pModel );
 static void  Abc_NtkVerifyReportError( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel );
 static void  Abc_NtkVerifyReportErrorSeq( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int * pModel, int nFrames );
 
@@ -78,7 +76,7 @@ void Abc_NtkCecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // convert the miter into a CNF
-    pCnf = Abc_NtkRenode( pMiter, 0, 100, 1, 0, 0 );
+    pCnf = Abc_NtkRenode( pMiter, 0, 100, 1, 0, 0, 0 );
     Abc_NtkDelete( pMiter );
     if ( pCnf == NULL )
     {
@@ -235,7 +233,7 @@ void Abc_NtkSecSat( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nConfLimit, int nI
     }
 
     // convert the miter into a CNF
-    pCnf = Abc_NtkRenode( pFrames, 0, 100, 1, 0, 0 );
+    pCnf = Abc_NtkRenode( pFrames, 0, 100, 1, 0, 0, 0 );
     Abc_NtkDelete( pFrames );
     if ( pCnf == NULL )
     {
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 3ca188b7..4339b520 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -19,6 +19,8 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcReconv.c \
     src/base/abci/abcRefactor.c \
     src/base/abci/abcRenode.c \
+    src/base/abci/abcRestruct.c \
+    src/base/abci/abcResub.c \
     src/base/abci/abcRewrite.c \
     src/base/abci/abcSat.c \
     src/base/abci/abcStrash.c \
diff --git a/src/base/cmd/cmd.c b/src/base/cmd/cmd.c
index 21dba247..c2c09697 100644
--- a/src/base/cmd/cmd.c
+++ b/src/base/cmd/cmd.c
@@ -1252,7 +1252,7 @@ int CmdCommandSis( Abc_Frame_t * pAbc, int argc, char **argv )
     }
 
     // write out the current network
-    pNetlist = Abc_NtkLogicToNetlist(pNtk);
+    pNetlist = Abc_NtkLogicToNetlist(pNtk,0);
     Io_WriteBlif( pNetlist, "_sis_in.blif", 1 );
     Abc_NtkDelete( pNetlist );
 
@@ -1388,7 +1388,7 @@ int CmdCommandMvsis( Abc_Frame_t * pAbc, int argc, char **argv )
     }
 
     // write out the current network
-    pNetlist = Abc_NtkLogicToNetlist(pNtk);
+    pNetlist = Abc_NtkLogicToNetlist(pNtk,0);
     Io_WriteBlif( pNetlist, "_mvsis_in.blif", 1 );
     Abc_NtkDelete( pNetlist );
 
diff --git a/src/base/cmd/cmd.h b/src/base/cmd/cmd.h
index 4e54df21..030b77e8 100644
--- a/src/base/cmd/cmd.h
+++ b/src/base/cmd/cmd.h
@@ -21,6 +21,10 @@
 #ifndef __CMD_H__
 #define __CMD_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -57,9 +61,13 @@ extern void        Cmd_FlagUpdateValue( Abc_Frame_t * pAbc, char * key, char * v
 /*=== cmdHist.c ========================================================*/
 extern void          Cmd_HistoryAddCommand( Abc_Frame_t * pAbc, char * command );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/base/io/io.c b/src/base/io/io.c
index 2725eb8a..0aa5e415 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -45,6 +45,7 @@ static int IoCommandWriteGml    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteList   ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWritePla    ( Abc_Frame_t * pAbc, int argc, char **argv );
 static int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv );
+static int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv );
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -83,6 +84,7 @@ void Io_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "I/O", "write_list",    IoCommandWriteList,    0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_pla",     IoCommandWritePla,     0 );
     Cmd_CommandAdd( pAbc, "I/O", "write_verilog", IoCommandWriteVerilog, 0 );
+    Cmd_CommandAdd( pAbc, "I/O", "write_counter", IoCommandWriteCounter, 0 );
 }
 
 /**Function*************************************************************
@@ -1174,7 +1176,7 @@ int IoCommandWriteEqn( Abc_Frame_t * pAbc, int argc, char **argv )
     if ( Abc_NtkIsSopLogic(pNtk) )
         Abc_NtkLogicMakeDirectSops(pNtk);
     // derive the netlist
-    pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
+    pNtkTemp = Abc_NtkLogicToNetlist(pNtk,1);
     if ( pNtkTemp == NULL )
     {
         fprintf( pAbc->Out, "Writing BENCH has failed.\n" );
@@ -1358,6 +1360,12 @@ int IoCommandWritePla( Abc_Frame_t * pAbc, int argc, char **argv )
         return 0;
     }
 
+    if ( Abc_NtkGetLevelNum(pNtk) > 1 )
+    {
+        fprintf( pAbc->Out, "PLA writing is available for collapsed networks.\n" );
+        return 0;
+    }
+
     if ( Abc_NtkLatchNum(pNtk) > 0 )
     {
         fprintf( pAbc->Out, "Latches are writed at PI/PO pairs in the PLA file.\n" );
@@ -1368,11 +1376,12 @@ int IoCommandWritePla( Abc_Frame_t * pAbc, int argc, char **argv )
     {
         goto usage;
     }
+
     // get the input file name
     FileName = argv[globalUtilOptind];
 
     // derive the netlist
-    pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
+    pNtkTemp = Abc_NtkLogicToNetlist(pNtk,1);
     if ( pNtkTemp == NULL )
     {
         fprintf( pAbc->Out, "Writing PLA has failed.\n" );
@@ -1434,7 +1443,7 @@ int IoCommandWriteVerilog( Abc_Frame_t * pAbc, int argc, char **argv )
     FileName = argv[globalUtilOptind];
 
     // derive the netlist
-    pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
+    pNtkTemp = Abc_NtkLogicToNetlist(pNtk,0);
     if ( pNtkTemp == NULL )
     {
         fprintf( pAbc->Out, "Writing PLA has failed.\n" );
@@ -1452,6 +1461,96 @@ usage:
     return 1;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int IoCommandWriteCounter( Abc_Frame_t * pAbc, int argc, char **argv )
+{
+    Abc_Ntk_t * pNtk;
+    char * FileName;
+    int c;
+    int fNames;
+
+    fNames = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "nh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+            case 'n':
+                fNames ^= 1;
+                break;
+            case 'h':
+                goto usage;
+            default:
+                goto usage;
+        }
+    }
+
+    pNtk = pAbc->pNtkCur;
+    if ( pNtk == NULL )
+    {
+        fprintf( pAbc->Out, "Empty network.\n" );
+        return 0;
+    }
+
+    if ( argc != globalUtilOptind + 1 )
+    {
+        goto usage;
+    }
+    // get the input file name
+    FileName = argv[globalUtilOptind];
+
+    if ( pNtk->pModel == NULL )
+    {
+        fprintf( pAbc->Out, "Counter-example is not available.\n" );
+        return 0;
+    }
+
+    // write the counter-example into the file
+    {
+        Abc_Obj_t * pObj;
+        FILE * pFile = fopen( FileName, "w" );
+        int i;
+        if ( pFile == NULL )
+        {
+            fprintf( stdout, "Io_WriteVerilog(): Cannot open the output file \"%s\".\n", FileName );
+            return 1;
+        }
+        if ( fNames )
+        {
+            Abc_NtkForEachPi( pNtk, pObj, i )
+                fprintf( pFile, "%s=%c ", Abc_ObjName(pObj), '0'+(pNtk->pModel[i]==1) );
+        }
+        else
+        {
+            Abc_NtkForEachPi( pNtk, pObj, i )
+                fprintf( pFile, "%c", '0'+(pNtk->pModel[i]==1) );
+        }
+        fprintf( pFile, "\n" );
+        fclose( pFile );
+    }
+
+    return 0;
+
+usage:
+    fprintf( pAbc->Err, "usage: write_counter [-nh] <file>\n" );
+    fprintf( pAbc->Err, "\t         writes the counter-example derived by \"prove\" or \"sat\"\n" );
+    fprintf( pAbc->Err, "\t         the file contains values for each PI in the natural order\n" );
+    fprintf( pAbc->Err, "\t-n     : write input names into the file [default = %s]\n", fNames? "yes": "no" );
+    fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
+    fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
+    return 1;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/base/io/io.h b/src/base/io/io.h
index fe5c237f..a9a61040 100644
--- a/src/base/io/io.h
+++ b/src/base/io/io.h
@@ -21,6 +21,10 @@
 #ifndef __IO_H__
 #define __IO_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -94,9 +98,13 @@ extern int                Io_WritePla( Abc_Ntk_t * pNtk, char * FileName );
 /*=== abcWriteVerilog.c ==========================================================*/
 extern void               Io_WriteVerilog( Abc_Ntk_t * pNtk, char * FileName );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/base/io/ioInt.h b/src/base/io/ioInt.h
index 7f4e200e..3daf3c75 100644
--- a/src/base/io/ioInt.h
+++ b/src/base/io/ioInt.h
@@ -41,9 +41,9 @@
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index 6b6c4a92..1b515a1e 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -53,7 +53,7 @@ void Io_WriteBlifLogic( Abc_Ntk_t * pNtk, char * FileName, int fWriteLatches )
 {
     Abc_Ntk_t * pNtkTemp;
     // derive the netlist
-    pNtkTemp = Abc_NtkLogicToNetlist(pNtk);
+    pNtkTemp = Abc_NtkLogicToNetlist(pNtk,0);
     if ( pNtkTemp == NULL )
     {
         fprintf( stdout, "Writing BLIF has failed.\n" );
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index 373c4636..dbf157bf 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -412,7 +412,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
 
     // transform logic functions from BDD to SOP
     if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk, 0);
 
     // mark the nodes from the set
     Vec_PtrForEachEntry( vNodes, pNode, i )
diff --git a/src/base/io/ioWritePla.c b/src/base/io/ioWritePla.c
index 12ac9ef7..4da8aca8 100644
--- a/src/base/io/ioWritePla.c
+++ b/src/base/io/ioWritePla.c
@@ -88,7 +88,7 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
     nProducts = 0;
     Abc_NtkForEachCo( pNtk, pNode, i )
     {
-        pDriver = Abc_ObjFanin0Ntk(pNode);
+        pDriver = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pNode) );
         if ( !Abc_ObjIsNode(pDriver) )
         {
             nProducts++;
@@ -138,9 +138,10 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
         pCubeOut[i] = '1';
 
         // consider special cases of nodes
-        pDriver = Abc_ObjFanin0Ntk(pNode);
+        pDriver = Abc_ObjFanin0Ntk( Abc_ObjFanin0(pNode) );
         if ( !Abc_ObjIsNode(pDriver) )
         {
+            assert( Abc_ObjIsCi(pDriver) );
             pCubeIn[(int)pDriver->pCopy] = '1' - Abc_ObjFaninC0(pNode);
             fprintf( pFile, "%s %s\n", pCubeIn, pCubeOut );
             pCubeIn[(int)pDriver->pCopy] = '-';
@@ -152,17 +153,29 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
                 fprintf( pFile, "%s %s\n", pCubeIn, pCubeOut );
             continue;
         }
+
+        // make sure the cover is not complemented
+        assert( !Abc_SopIsComplement( pDriver->pData ) );
+
         // write the cubes
         nFanins = Abc_ObjFaninNum(pDriver);
         Abc_SopForEachCube( pDriver->pData, nFanins, pCube )
         {
             Abc_ObjForEachFanin( pDriver, pFanin, k )
+            {
+                pFanin = Abc_ObjFanin0Ntk(pFanin);
+                assert( (int)pFanin->pCopy < nInputs );
                 pCubeIn[(int)pFanin->pCopy] = pCube[k];
+            }
             fprintf( pFile, "%s %s\n", pCubeIn, pCubeOut );
         }
         // clean the cube for future writing
         Abc_ObjForEachFanin( pDriver, pFanin, k )
+        {
+            pFanin = Abc_ObjFanin0Ntk(pFanin);
+            assert( Abc_ObjIsCi(pFanin) );
             pCubeIn[(int)pFanin->pCopy] = '-';
+        }
         Extra_ProgressBarUpdate( pProgress, i, NULL );
     }
     Extra_ProgressBarStop( pProgress );
@@ -171,6 +184,8 @@ int Io_WritePlaOne( FILE * pFile, Abc_Ntk_t * pNtk )
     // clean the CI nodes
     Abc_NtkForEachCi( pNtk, pNode, i )
         pNode->pCopy = NULL;
+    free( pCubeIn );
+    free( pCubeOut );
     return 1;
 }
 
diff --git a/src/base/main/main.h b/src/base/main/main.h
index d5a463f5..9b483904 100644
--- a/src/base/main/main.h
+++ b/src/base/main/main.h
@@ -21,6 +21,10 @@
 #ifndef __MAIN_H__
 #define __MAIN_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         TYPEDEFS                                 ///
 ////////////////////////////////////////////////////////////////////////
@@ -104,8 +108,12 @@ extern void            Abc_FrameSetLibGen( void * pLib );
 extern void            Abc_FrameSetLibSuper( void * pLib );      
 extern void            Abc_FrameSetFlag( char * pFlag, char * pValue );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index ec932838..d2bca1ab 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -102,8 +102,8 @@ extern void            Abc_UtilsPrintHello( Abc_Frame_t * pAbc );
 extern void            Abc_UtilsPrintUsage( Abc_Frame_t * pAbc, char * ProgName );
 extern void            Abc_UtilsSource( Abc_Frame_t * pAbc );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif
diff --git a/src/base/seq/seq.h b/src/base/seq/seq.h
index cba15e47..b66799b5 100644
--- a/src/base/seq/seq.h
+++ b/src/base/seq/seq.h
@@ -21,6 +21,10 @@
 #ifndef __SEQ_H__
 #define __SEQ_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -82,9 +86,13 @@ extern int             Seq_MapComputeAreaFlows( Abc_Ntk_t * pNtk, int fVerbose )
 extern Vec_Ptr_t *     Seq_NtkReachNodes( Abc_Ntk_t * pNtk, int fFromPos );
 extern int             Seq_NtkCleanup( Abc_Ntk_t * pNtk, int fVerbose );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/base/seq/seqInt.h b/src/base/seq/seqInt.h
index 3d3d0804..221efc91 100644
--- a/src/base/seq/seqInt.h
+++ b/src/base/seq/seqInt.h
@@ -21,6 +21,10 @@
 #ifndef __SEQ_INT_H__
 #define __SEQ_INT_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -240,9 +244,13 @@ extern int                   Seq_ObjFanoutLMin( Abc_Obj_t * pObj );
 extern int                   Seq_ObjFanoutLSum( Abc_Obj_t * pObj );
 extern int                   Seq_ObjFaninLSum( Abc_Obj_t * pObj );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/base/seq/seqRetCore.c b/src/base/seq/seqRetCore.c
index 4aba069d..0805a838 100644
--- a/src/base/seq/seqRetCore.c
+++ b/src/base/seq/seqRetCore.c
@@ -107,7 +107,7 @@ Abc_Ntk_t * Seq_NtkRetimeDerive( Abc_Ntk_t * pNtk, int fVerbose )
 
     // transform logic functions from BDD to SOP
     if ( fHasBdds = Abc_NtkIsBddLogic(pNtk) )
-        Abc_NtkBddToSop(pNtk);
+        Abc_NtkBddToSop(pNtk, 0);
 
     // start the network
     pNtkNew = Abc_NtkAlloc( ABC_NTK_SEQ, ABC_FUNC_AIG );
diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h
index 04385933..a3fc4948 100644
--- a/src/bdd/dsd/dsd.h
+++ b/src/bdd/dsd/dsd.h
@@ -28,6 +28,10 @@
 #ifndef __DSD_H__
 #define __DSD_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                      TYPEDEF DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -114,8 +118,12 @@ extern void            Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode );
 /*=== dsdLocal.c =======================================================*/
 extern DdNode *        Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                           END OF FILE                            ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif
\ No newline at end of file
diff --git a/src/bdd/dsd/dsdInt.h b/src/bdd/dsd/dsdInt.h
index 5569c443..62ce7e99 100644
--- a/src/bdd/dsd/dsdInt.h
+++ b/src/bdd/dsd/dsdInt.h
@@ -83,9 +83,9 @@ extern void         Dsd_TreeNodeDelete( DdManager * dd, Dsd_Node_t * pNode );
 extern void         Dsd_TreeUnmark( Dsd_Manager_t * dMan );
 extern DdNode *     Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fRemap );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                           END OF FILE                            ///
 ////////////////////////////////////////////////////////////////////////
 
-
-#endif
\ No newline at end of file
diff --git a/src/bdd/parse/parse.h b/src/bdd/parse/parse.h
index c16c8991..4923fbdd 100644
--- a/src/bdd/parse/parse.h
+++ b/src/bdd/parse/parse.h
@@ -47,7 +47,8 @@
 extern DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormula, int nVars, int nRanks, 
       char * ppVarNames[], DdManager * dd, DdNode * pbVars[] );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-#endif
diff --git a/src/bdd/parse/parseInt.h b/src/bdd/parse/parseInt.h
index 14623681..a1730f2c 100644
--- a/src/bdd/parse/parseInt.h
+++ b/src/bdd/parse/parseInt.h
@@ -67,7 +67,8 @@ extern void               Parse_StackOpPush   ( Parse_StackOp_t * p, int Oper );
 extern int                Parse_StackOpPop    ( Parse_StackOp_t * p );
 extern void               Parse_StackOpFree   ( Parse_StackOp_t * p );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-#endif
diff --git a/src/bdd/reo/reo.h b/src/bdd/reo/reo.h
index 7e4be855..45667768 100644
--- a/src/bdd/reo/reo.h
+++ b/src/bdd/reo/reo.h
@@ -19,6 +19,10 @@
 #ifndef __REO_H__
 #define __REO_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 #include <stdio.h>
 #include <stdlib.h>
 #include "extra.h"
@@ -215,8 +219,12 @@ extern DdNode *   Extra_ReorderCudd( DdManager * dd, DdNode * aFunc, int pPermut
 extern int        Extra_bddReorderTest( DdManager * dd, DdNode * bF ); 
 extern int        Extra_addReorderTest( DdManager * dd, DdNode * aF ); 
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         END OF FILE                              ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif
diff --git a/src/generic.h b/src/generic.h
index f634ea1c..e17d2edf 100644
--- a/src/generic.h
+++ b/src/generic.h
@@ -21,6 +21,10 @@
 #ifndef __zzz_H__
 #define __zzz_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -42,10 +46,14 @@
 ////////////////////////////////////////////////////////////////////////
 
 /*=== zzz.c ==========================================================*/
+ 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/map/fpga/fpga.h b/src/map/fpga/fpga.h
index 51868188..bbb95984 100644
--- a/src/map/fpga/fpga.h
+++ b/src/map/fpga/fpga.h
@@ -19,6 +19,10 @@
 #ifndef __FPGA_H__
 #define __FPGA_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -153,8 +157,12 @@ extern int             Fpga_ManCheckConsistency( Fpga_Man_t * p );
 extern void            Fpga_ManCleanData0( Fpga_Man_t * pMan );
 extern Fpga_NodeVec_t * Fpga_CollectNodeTfo( Fpga_Man_t * pMan, Fpga_Node_t * pNode );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-#endif
diff --git a/src/map/fpga/fpgaInt.h b/src/map/fpga/fpgaInt.h
index b6ac71d4..3a35d6dc 100644
--- a/src/map/fpga/fpgaInt.h
+++ b/src/map/fpga/fpgaInt.h
@@ -376,8 +376,8 @@ extern void              Fpga_MappingSetChoiceLevels( Fpga_Man_t * pMan );
 /*=== CUDD package.c ===============================================================*/
 extern unsigned int      Cudd_Prime( unsigned int p );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif
diff --git a/src/map/fpga/fpgaTruth.c b/src/map/fpga/fpgaTruth.c
index 11660731..e3eb487f 100644
--- a/src/map/fpga/fpgaTruth.c
+++ b/src/map/fpga/fpgaTruth.c
@@ -94,8 +94,7 @@ void * Fpga_TruthsCutBdd( void * dd, Fpga_Cut_t * pCut )
         Cudd_RecursiveDeref( dd, (DdNode*)pCut->uSign );
         pCut->uSign = 0;
     }
-    printf( "%d ", vVisited->nSize );
-
+//    printf( "%d ", vVisited->nSize );
     Fpga_NodeVecFree( vVisited );
     Cudd_Deref( bFunc );
     return bFunc;
diff --git a/src/map/mapper/mapper.h b/src/map/mapper/mapper.h
index 9b059fd0..10839382 100644
--- a/src/map/mapper/mapper.h
+++ b/src/map/mapper/mapper.h
@@ -19,6 +19,10 @@
 #ifndef __MAPPER_H__
 #define __MAPPER_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -180,7 +184,12 @@ extern void            Map_ManCleanData( Map_Man_t * p );
 extern void            Map_MappingSetupTruthTables( unsigned uTruths[][2] );
 extern void            Map_MappingSetupTruthTablesLarge( unsigned uTruths[][32] );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-#endif
diff --git a/src/map/mapper/mapperInt.h b/src/map/mapper/mapperInt.h
index fd7ac946..a3a2cf40 100644
--- a/src/map/mapper/mapperInt.h
+++ b/src/map/mapper/mapperInt.h
@@ -470,8 +470,8 @@ extern void              Map_NodeVecWriteEntry( Map_NodeVec_t * p, int i, Map_No
 extern Map_Node_t *      Map_NodeVecReadEntry( Map_NodeVec_t * p, int i );
 extern void              Map_NodeVecSortByLevel( Map_NodeVec_t * p );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif
diff --git a/src/map/mio/mio.h b/src/map/mio/mio.h
index 0e2c085d..dabc05dd 100644
--- a/src/map/mio/mio.h
+++ b/src/map/mio/mio.h
@@ -19,6 +19,10 @@
 #ifndef __MIO_H__
 #define __MIO_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -133,7 +137,13 @@ extern void              Mio_DeriveGateDelays( Mio_Gate_t * pGate,
                             float * ptDelaysRes, float * ptPinDelayMax );
 extern Mio_Gate_t *      Mio_GateCreatePseudo( int nInputs );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-#endif
+
diff --git a/src/map/mio/mioInt.h b/src/map/mio/mioInt.h
index a25ca026..3f90b625 100644
--- a/src/map/mio/mioInt.h
+++ b/src/map/mio/mioInt.h
@@ -118,8 +118,8 @@ struct  Mio_PinStruct_t_
 /*=== mioRead.c =============================================================*/
 /*=== mioUtils.c =============================================================*/
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif
diff --git a/src/map/pga/pga.h b/src/map/pga/pga.h
index ac129c7f..4b2a9df4 100644
--- a/src/map/pga/pga.h
+++ b/src/map/pga/pga.h
@@ -21,6 +21,10 @@
 #ifndef __PGA_H__
 #define __PGA_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -64,9 +68,13 @@ extern Vec_Ptr_t *   Pga_DoMapping( Pga_Man_t * p );
 extern Pga_Man_t *   Pga_ManStart( Pga_Params_t * pParams );
 extern void          Pga_ManStop( Pga_Man_t * p );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/map/pga/pgaInt.h b/src/map/pga/pgaInt.h
index 65832c8d..da9aa9a9 100644
--- a/src/map/pga/pgaInt.h
+++ b/src/map/pga/pgaInt.h
@@ -124,9 +124,9 @@ extern float       Pga_MappingSetRefsAndArea( Pga_Man_t * p );
 extern float       Pga_MappingGetSwitching( Pga_Man_t * p );
 extern void        Pga_MappingPrintOutputArrivals( Pga_Man_t * p );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/map/super/super.h b/src/map/super/super.h
index 9d475116..a7169924 100644
--- a/src/map/super/super.h
+++ b/src/map/super/super.h
@@ -19,6 +19,10 @@
 #ifndef __SUPER_H__
 #define __SUPER_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -44,8 +48,13 @@
 ////////////////////////////////////////////////////////////////////////
 
 /*=== superCore.c =============================================================*/
+    
+#ifdef __cplusplus
+}
+#endif
+
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-#endif
diff --git a/src/map/super/superInt.h b/src/map/super/superInt.h
index 97ed4c5a..ec6d0a38 100644
--- a/src/map/super/superInt.h
+++ b/src/map/super/superInt.h
@@ -55,8 +55,8 @@ extern void       Super2_Precompute( int nInputs, int nLevels, int fVerbose );
 /*=== superGate.c =============================================================*/
 extern void       Super_Precompute( Mio_Library_t * pLibGen, int nInputs, int nLevels, float tDelayMax, float tAreaMax, int TimeLimit, bool fSkipInv, bool fWriteOldFormat, int fVerbose );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif
diff --git a/src/misc/extra/extra.h b/src/misc/extra/extra.h
index 666d7388..1b6abaa6 100644
--- a/src/misc/extra/extra.h
+++ b/src/misc/extra/extra.h
@@ -29,6 +29,10 @@
 #ifndef __EXTRA_H__
 #define __EXTRA_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 #ifdef _WIN32
 #define inline __inline // compatible with MS VS 6.0
 #endif
@@ -434,4 +438,8 @@ extern int         globalUtilOptind;
 
 /**AutomaticEnd***************************************************************/
 
+#ifdef __cplusplus
+}
+#endif
+
 #endif /* __EXTRA_H__ */
diff --git a/src/misc/mvc/mvc.h b/src/misc/mvc/mvc.h
index 363b1e57..650f698d 100644
--- a/src/misc/mvc/mvc.h
+++ b/src/misc/mvc/mvc.h
@@ -724,9 +724,9 @@ extern Mvc_Manager_t *  Mvc_ManagerAllocCube( int nWords );
 extern Mvc_Manager_t *  Mvc_ManagerFreeCover( Mvc_Cover_t * pCover );
 extern Mvc_Manager_t *  Mvc_ManagerFreeCube( Mvc_Cover_t * pCube, int nWords );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/misc/st/st.h b/src/misc/st/st.h
index 1802cf9b..b15f3c83 100644
--- a/src/misc/st/st.h
+++ b/src/misc/st/st.h
@@ -14,6 +14,10 @@
 #ifndef ST_INCLUDED
 #define ST_INCLUDED
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 typedef struct st_table_entry st_table_entry;
 struct st_table_entry {
     char *key;
@@ -85,4 +89,8 @@ extern void st_free_gen (st_generator *);
 
 #define ST_OUT_OF_MEM -10000
 
+#ifdef __cplusplus
+}
+#endif
+
 #endif /* ST_INCLUDED */
diff --git a/src/misc/st/stmm.h b/src/misc/st/stmm.h
index d7b8a3f3..4330416e 100644
--- a/src/misc/st/stmm.h
+++ b/src/misc/st/stmm.h
@@ -14,6 +14,10 @@
 #ifndef STMM_INCLUDED
 #define STMM_INCLUDED
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 #include "extra.h"
 
 typedef struct stmm_table_entry stmm_table_entry;
@@ -116,4 +120,8 @@ EXTERN void stmm_clean ARGS ((stmm_table *));
 
 */
 
+#ifdef __cplusplus
+}
+#endif
+
 #endif /* STMM_INCLUDED */
diff --git a/src/misc/util/util_hack.h b/src/misc/util/util_hack.h
index 57914c47..a9b90e61 100644
--- a/src/misc/util/util_hack.h
+++ b/src/misc/util/util_hack.h
@@ -21,6 +21,10 @@
 #ifndef __UTIL_HACK_H__
 #define __UTIL_HACK_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 #include <stdio.h>
 #include <stdlib.h>
 #include <string.h>
@@ -84,4 +88,8 @@ extern char *      Extra_UtilFileSearch( char *file, char *path, char *mode );
 extern char *      globalUtilOptarg;
 extern int         globalUtilOptind;
 
+#ifdef __cplusplus
+}
+#endif
+
 #endif
diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h
index f5ecf9bd..6ab23298 100644
--- a/src/misc/vec/vec.h
+++ b/src/misc/vec/vec.h
@@ -21,6 +21,10 @@
 #ifndef __VEC_H__
 #define __VEC_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -50,9 +54,13 @@
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/misc/vec/vecInt.h b/src/misc/vec/vecInt.h
index 06526332..ee848df7 100644
--- a/src/misc/vec/vecInt.h
+++ b/src/misc/vec/vecInt.h
@@ -696,9 +696,9 @@ static inline void Vec_IntSortUnsigned( Vec_Int_t * p )
             (int (*)(const void *, const void *)) Vec_IntSortCompareUnsigned );
 }
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h
index 66198eb0..65314af6 100644
--- a/src/misc/vec/vecPtr.h
+++ b/src/misc/vec/vecPtr.h
@@ -529,10 +529,10 @@ static inline void Vec_PtrSort( Vec_Ptr_t * p, int (*Vec_PtrSortCompare)() )
             (int (*)(const void *, const void *)) Vec_PtrSortCompare );
 }
 
+#endif
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index 86a5046a..5549d374 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -501,9 +501,9 @@ static inline void Vec_StrSort( Vec_Str_t * p, int fReverse )
                 (int (*)(const void *, const void *)) Vec_StrSortCompare1 );
 }
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/misc/vec/vecVec.h b/src/misc/vec/vecVec.h
index f95b334c..8518184a 100644
--- a/src/misc/vec/vecVec.h
+++ b/src/misc/vec/vecVec.h
@@ -256,9 +256,9 @@ static inline void Vec_VecPushUnique( Vec_Vec_t * p, int Level, void * Entry )
         Vec_PtrPushUnique( (Vec_Ptr_t*)p->pArray[Level], Entry );
 }
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/opt/cut/cut.h b/src/opt/cut/cut.h
index b724c976..0a1cd41a 100644
--- a/src/opt/cut/cut.h
+++ b/src/opt/cut/cut.h
@@ -21,6 +21,10 @@
 #ifndef __CUT_H__
 #define __CUT_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -133,9 +137,13 @@ extern void             Cut_OracleTryDroppingCuts( Cut_Oracle_t * p, int Node );
 /*=== cutTruth.c ==========================================================*/
 extern void             Cut_TruthCanonicize( Cut_Cut_t * pCut );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/opt/cut/cutInt.h b/src/opt/cut/cutInt.h
index eca2fcd5..375d2213 100644
--- a/src/opt/cut/cutInt.h
+++ b/src/opt/cut/cutInt.h
@@ -141,9 +141,9 @@ extern int                 Cut_TableReadTime( Cut_HashTable_t * pTable );
 /*=== cutTruth.c ==========================================================*/
 extern void                Cut_TruthCompute( Cut_Cut_t * pCut, Cut_Cut_t * pCut0, Cut_Cut_t * pCut1, int fCompl0, int fCompl1 );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/opt/cut/cutList.h b/src/opt/cut/cutList.h
index 12db2207..a03ec9d5 100644
--- a/src/opt/cut/cutList.h
+++ b/src/opt/cut/cutList.h
@@ -199,9 +199,9 @@ static inline Cut_Cut_t * Cut_ListFinish( Cut_List_t * p )
     return pHead;
 }
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/opt/dec/dec.h b/src/opt/dec/dec.h
index 7b8b2e94..2987723f 100644
--- a/src/opt/dec/dec.h
+++ b/src/opt/dec/dec.h
@@ -21,6 +21,10 @@
 #ifndef __DEC_H__
 #define __DEC_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -699,9 +703,13 @@ static inline Dec_Edge_t Dec_GraphAddNodeMux( Dec_Graph_t * pGraph, Dec_Edge_t e
     return eNode;
 }
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/opt/dec/decAbc.c b/src/opt/dec/decAbc.c
index 066b3bb2..af76cd84 100644
--- a/src/opt/dec/decAbc.c
+++ b/src/opt/dec/decAbc.c
@@ -18,7 +18,7 @@
 
 #include "abc.h"
 #include "dec.h"
-#include "aig.h"
+//#include "aig.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -214,6 +214,7 @@ void Dec_GraphUpdateNetwork( Abc_Obj_t * pRoot, Dec_Graph_t * pGraph, bool fUpda
   SeeAlso     []
 
 ***********************************************************************/
+/*
 Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph )
 {
     Dec_Node_t * pNode;
@@ -235,7 +236,7 @@ Aig_Node_t * Dec_GraphToNetworkAig( Aig_Man_t * pMan, Dec_Graph_t * pGraph )
     // complement the result if necessary
     return Aig_NotCond( pNode->pFunc, Dec_GraphIsComplement(pGraph) );
 }
-
+*/
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/opt/fxu/fxu.h b/src/opt/fxu/fxu.h
index df43b6b3..6a1bb5e3 100644
--- a/src/opt/fxu/fxu.h
+++ b/src/opt/fxu/fxu.h
@@ -19,6 +19,10 @@
 #ifndef __FXU_H__
 #define __FXU_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -74,9 +78,13 @@ struct FxuDataStruct
 /*===== fxu.c ==========================================================*/
 extern int          Fxu_FastExtract( Fxu_Data_t * pData );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/opt/fxu/fxuInt.h b/src/opt/fxu/fxuInt.h
index d82a68db..0ae1d79e 100644
--- a/src/opt/fxu/fxuInt.h
+++ b/src/opt/fxu/fxuInt.h
@@ -529,8 +529,9 @@ extern int          Fxu_HeapSingleReadMaxWeight( Fxu_HeapSingle * p );
 extern Fxu_Single * Fxu_HeapSingleReadMax( Fxu_HeapSingle * p );
 extern Fxu_Single * Fxu_HeapSingleGetMax( Fxu_HeapSingle * p );  
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                         END OF FILE                              ///
 ////////////////////////////////////////////////////////////////////////
-#endif
 
diff --git a/src/opt/rwr/rwr.h b/src/opt/rwr/rwr.h
index 70e1070b..8de225e8 100644
--- a/src/opt/rwr/rwr.h
+++ b/src/opt/rwr/rwr.h
@@ -21,6 +21,10 @@
 #ifndef __RWR_H__
 #define __RWR_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -145,9 +149,13 @@ extern void              Rwr_ManLoadFromFile( Rwr_Man_t * p, char * pFileName );
 extern void              Rwr_ListAddToTail( Rwr_Node_t ** ppList, Rwr_Node_t * pNode );
 extern char *            Rwr_ManGetPractical( Rwr_Man_t * p );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/opt/sim/sim.h b/src/opt/sim/sim.h
index 963f0ad6..7f32fc34 100644
--- a/src/opt/sim/sim.h
+++ b/src/opt/sim/sim.h
@@ -21,6 +21,10 @@
 #ifndef __SIM_H__
 #define __SIM_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 /*
     The ideas realized in this package are described in the paper:
     "Detecting Symmetries in Boolean Functions using Circuit Representation, 
@@ -217,9 +221,13 @@ extern int             Sim_UtilCountAllPairs( Vec_Ptr_t * vSuppFun, int nSimWord
 extern void            Sim_UtilCountPairsAll( Sym_Man_t * p );
 extern int             Sim_UtilMatrsAreDisjoint( Sym_Man_t * p );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/opt/xyz/xyz.h b/src/opt/xyz/xyz.h
index ea488068..4fec2150 100644
--- a/src/opt/xyz/xyz.h
+++ b/src/opt/xyz/xyz.h
@@ -18,6 +18,13 @@
 
 ***********************************************************************/
 
+#ifndef __XYZ_H__
+#define __XYZ_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 #include "abc.h"
 #include "xyzInt.h"
 
@@ -89,8 +96,15 @@ extern void        Abc_NodeXyzDropData( Xyz_Man_t * p, Abc_Obj_t * pObj );
 /*=== xyzTest.c ===========================================================*/
 extern Abc_Ntk_t * Abc_NtkXyzTestSop( Abc_Ntk_t * pNtk );
 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
 
+
diff --git a/src/sat/aig/aig.h b/src/sat/aig/aig.h
index c83af527..5d2547ea 100644
--- a/src/sat/aig/aig.h
+++ b/src/sat/aig/aig.h
@@ -21,6 +21,10 @@
 #ifndef __AIG_H__
 #define __AIG_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 /*
     AIG is an And-Inv Graph with structural hashing.
     It is always structurally hashed. It means that at any time:
@@ -358,10 +362,14 @@ extern void                Aig_PatternFill( Aig_Pattern_t * pPat );
 extern int                 Aig_PatternCount( Aig_Pattern_t * pPat );
 extern void                Aig_PatternRandom( Aig_Pattern_t * pPat );
 extern void                Aig_PatternFree( Aig_Pattern_t * pPat );
+ 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
 
-#endif
-
diff --git a/src/sat/asat/asatmem.h b/src/sat/asat/asatmem.h
index 56115e7d..7351d77b 100644
--- a/src/sat/asat/asatmem.h
+++ b/src/sat/asat/asatmem.h
@@ -70,7 +70,9 @@ extern char *              Asat_MmStepEntryFetch( Asat_MmStep_t * p, int nBytes
 extern void                Asat_MmStepEntryRecycle( Asat_MmStep_t * p, char * pEntry, int nBytes );
 extern int                 Asat_MmStepReadMemUsage( Asat_MmStep_t * p );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-#endif
+
diff --git a/src/sat/asat/solver.h b/src/sat/asat/solver.h
index d798a7a9..62815656 100644
--- a/src/sat/asat/solver.h
+++ b/src/sat/asat/solver.h
@@ -22,6 +22,10 @@ OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWA
 #ifndef solver_h
 #define solver_h
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 #ifdef _WIN32
 #define inline __inline // compatible with MS VS 6.0
 #endif
@@ -141,5 +145,9 @@ struct solver_t
 
     stats    solver_stats;
 };
+ 
+#ifdef __cplusplus
+}
+#endif
 
 #endif
diff --git a/src/sat/csat/csat_apis.h b/src/sat/csat/csat_apis.h
index e187845c..d2fa770e 100644
--- a/src/sat/csat/csat_apis.h
+++ b/src/sat/csat/csat_apis.h
@@ -206,12 +206,12 @@ extern void                  ABC_TargetResFree( CSAT_Target_ResultT * p );
 
 extern void CSAT_SetCaller(ABC_Manager mng, enum CSAT_CallerT caller);
 
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
 #ifdef __cplusplus
 }
 #endif
 
 #endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
diff --git a/src/sat/fraig/fraig.h b/src/sat/fraig/fraig.h
index 4637c030..4e2a295e 100644
--- a/src/sat/fraig/fraig.h
+++ b/src/sat/fraig/fraig.h
@@ -18,7 +18,11 @@
 
 #ifndef __FRAIG_H__
 #define __FRAIG_H__
- 
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -106,6 +110,7 @@ extern int *               Fraig_ManReadModel( Fraig_Man_t * p );
 extern int                 Fraig_ManReadPatternNumRandom( Fraig_Man_t * p );
 extern int                 Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p );
 extern int                 Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p );
+extern int                 Fraig_ManReadSatFails( Fraig_Man_t * p );      
 
 extern void                Fraig_ManSetFuncRed( Fraig_Man_t * p, int fFuncRed );        
 extern void                Fraig_ManSetFeedBack( Fraig_Man_t * p, int fFeedBack );      
@@ -208,4 +213,9 @@ extern Fraig_NodeVec_t *   Fraig_CollectSupergate( Fraig_Node_t * pNode, int fSt
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
+ 
+#ifdef __cplusplus
+}
+#endif
+
 #endif
diff --git a/src/sat/fraig/fraigApi.c b/src/sat/fraig/fraigApi.c
index aeea01f1..3b8da17f 100644
--- a/src/sat/fraig/fraigApi.c
+++ b/src/sat/fraig/fraigApi.c
@@ -64,6 +64,8 @@ int               Fraig_ManReadPatternNumRandom( Fraig_Man_t * p )            {
 int               Fraig_ManReadPatternNumDynamic( Fraig_Man_t * p )           { return p->iWordStart * 32;  }
 // returns the number of dynamic patterns proved useful to distinquish some FRAIG nodes (this number is more than 0 after the first garbage collection of patterns)
 int               Fraig_ManReadPatternNumDynamicFiltered( Fraig_Man_t * p )   { return p->iPatsPerm;        }
+// returns the number of times FRAIG package timed out
+int               Fraig_ManReadSatFails( Fraig_Man_t * p )                    { return p->nSatFails;        }      
 
 /**Function*************************************************************
 
diff --git a/src/sat/fraig/fraigInt.h b/src/sat/fraig/fraigInt.h
index f5e792eb..890af13c 100644
--- a/src/sat/fraig/fraigInt.h
+++ b/src/sat/fraig/fraigInt.h
@@ -441,8 +441,8 @@ extern int                 Fraig_NodeIsTravIdPrevious( Fraig_Man_t * pMan, Fraig
 /*=== fraigVec.c ===============================================================*/
 extern void                Fraig_NodeVecSortByRefCount( Fraig_NodeVec_t * p );
 
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-
-#endif
diff --git a/src/sat/msat/msat.h b/src/sat/msat/msat.h
index 40028784..94416a5d 100644
--- a/src/sat/msat/msat.h
+++ b/src/sat/msat/msat.h
@@ -21,6 +21,10 @@
 #ifndef __MSAT_H__
 #define __MSAT_H__
 
+#ifdef __cplusplus
+extern "C" {
+#endif
+
 ////////////////////////////////////////////////////////////////////////
 ///                          INCLUDES                                ///
 ////////////////////////////////////////////////////////////////////////
@@ -154,8 +158,13 @@ extern double           Msat_VarHeapReadMaxWeight( Msat_VarHeap_t * p );
 extern int              Msat_VarHeapCountNodes( Msat_VarHeap_t * p, double WeightLimit );  
 extern int              Msat_VarHeapReadMax( Msat_VarHeap_t * p );  
 extern int              Msat_VarHeapGetMax( Msat_VarHeap_t * p );  
+ 
+#ifdef __cplusplus
+}
+#endif
+
+#endif
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
-#endif
diff --git a/src/sat/msat/msatSolverCore.c b/src/sat/msat/msatSolverCore.c
index 091a0c55..397dbcdc 100644
--- a/src/sat/msat/msatSolverCore.c
+++ b/src/sat/msat/msatSolverCore.c
@@ -176,7 +176,7 @@ bool Msat_SolverSolve( Msat_Solver_t * p, Msat_IntVec_t * vAssumps, int nBackTra
         nConflictsLimit *= 1.5;
         nLearnedLimit   *= 1.1;
         // if the limit on the number of backtracks is given, quit the restart loop
-        if ( nBackTrackLimit > 0 )
+        if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit )
             break;
         // if the runtime limit is exceeded, quit the restart loop
         if ( nTimeLimit > 0 && clock() - timeStart >= nTimeLimit * CLOCKS_PER_SEC )
diff --git a/src/sat/msat/msatSolverSearch.c b/src/sat/msat/msatSolverSearch.c
index e594d9c3..4b73d6b3 100644
--- a/src/sat/msat/msatSolverSearch.c
+++ b/src/sat/msat/msatSolverSearch.c
@@ -599,7 +599,7 @@ Msat_Type_t Msat_SolverSearch( Msat_Solver_t * p, int nConfLimit, int nLearnedLi
                 Msat_SolverCancelUntil( p, p->nLevelRoot );
                 return MSAT_UNKNOWN; 
             }
-            else if ( nBackTrackLimit > 0 && nConfs > nBackTrackLimit ) {
+            else if ( nBackTrackLimit > 0 && (int)p->Stats.nConflicts - p->nBackTracks > nBackTrackLimit ) {
                 // Reached bound on number of conflicts:
                 Msat_QueueClear( p->pQueue );
                 Msat_SolverCancelUntil( p, p->nLevelRoot );