Version abc90714

committer: Baruch Sterin <baruchs@gmail.com>

67 files changed, 2529 insertions, 449 deletions

diff --git a/abclib.dsp b/abclib.dsp
index bef97f81..748ffeb6 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -231,6 +231,10 @@ SOURCE=.\src\base\abci\abcDelay.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\base\abci\abcDprove2.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\base\abci\abcDress.c
 # End Source File
 # Begin Source File
@@ -2269,6 +2273,14 @@ SOURCE=.\src\misc\util\abc_global.h
 
 SOURCE=.\src\misc\util\util_hack.h
 # End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\utilMem.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\misc\util\utilMem.h
+# End Source File
 # End Group
 # Begin Group "nm"
 
@@ -3107,6 +3119,10 @@ SOURCE=.\src\aig\ntl\ntlMap.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\ntl\ntlNames.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\ntl\ntlObj.c
 # End Source File
 # Begin Source File
@@ -3669,46 +3685,6 @@ SOURCE=.\src\aig\cgt\cgtSat.c
 # Begin Group "nal"
 
 # PROP Default_Filter ""
-# Begin Source File
-
-SOURCE=.\src\aig\nal090422\nal.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\nal090422\nalCore.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\nal090422\nalFlop.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\nal090422\nalFunc.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\nal090422\nalInt.h
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\nal090422\nalMan.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\nal090422\nalModels.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\nal090422\nalRead.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\nal090422\nalUtil.c
-# End Source File
-# Begin Source File
-
-SOURCE=.\src\aig\nal090422\nalWrite.c
-# End Source File
 # End Group
 # Begin Group "gia"
 
@@ -3747,6 +3723,10 @@ SOURCE=.\src\aig\gia\giaCSatOld.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaCTas.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaDfs.c
 # End Source File
 # Begin Source File
@@ -3787,6 +3767,10 @@ SOURCE=.\src\aig\gia\giaFront.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaGiarf.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaGlitch.c
 # End Source File
 # Begin Source File
@@ -3795,6 +3779,10 @@ SOURCE=.\src\aig\gia\giaHash.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\gia\giaHcd.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\gia\giaMan.c
 # End Source File
 # Begin Source File
diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 38ba167f..56e2336a 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -481,13 +481,16 @@ extern Aig_Man_t *     Aig_ManDupOrdered( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupTrim( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupExor( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupDfs( Aig_Man_t * p );
-extern Aig_Man_t *     Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide );
+extern Vec_Ptr_t *     Aig_ManOrderPios( Aig_Man_t * p, Aig_Man_t * pOrder );
+extern Aig_Man_t *     Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios );
 extern Aig_Man_t *     Aig_ManDupLevelized( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupWithoutPos( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupRepres( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupRepresDfs( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int fImpl );
+extern Aig_Man_t *     Aig_ManDupOrpos( Aig_Man_t * p, int fAddRegs );
 extern Aig_Man_t *     Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs );
+extern Aig_Man_t *     Aig_ManDupUnsolvedOutputs( Aig_Man_t * p, int fAddRegs );
 /*=== aigFanout.c ==========================================================*/
 extern void            Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
 extern void            Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index eeaf4c91..90579f59 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -602,9 +602,8 @@ Aig_Obj_t * Aig_ManDupDfsGuided_rec( Aig_Man_t * pNew, Aig_Man_t * p, Aig_Obj_t
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide )
+Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Vec_Ptr_t * vPios )
 {
-    Vec_Ptr_t * vPios;
     Aig_Man_t * pNew;
     Aig_Obj_t * pObj, * pObjNew;
     int i, nNodes;
@@ -631,7 +630,6 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide )
     // duplicate internal nodes
     Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
     Aig_ManConst1(pNew)->pHaig = Aig_ManConst1(p)->pHaig;
-    vPios = Aig_ManOrderPios( p, pGuide );
     Vec_PtrForEachEntry( vPios, pObj, i )
     {
         if ( Aig_ObjIsPi(pObj) )
@@ -650,7 +648,6 @@ Aig_Man_t * Aig_ManDupDfsGuided( Aig_Man_t * p, Aig_Man_t * pGuide )
             pObj->pData = pObjNew;
         }
     }
-    Vec_PtrFree( vPios );
 //    assert( Aig_ManBufNum(p) != 0 || Aig_ManNodeNum(p) == Aig_ManNodeNum(pNew) );
     if ( p->pEquivs == NULL && p->pReprs == NULL && (nNodes = Aig_ManCleanup( pNew )) )
         printf( "Aig_ManDupDfs(): Cleanup after AIG duplication removed %d nodes.\n", nNodes );
@@ -982,6 +979,54 @@ Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper )
   SeeAlso     []
 
 ***********************************************************************/
+Aig_Man_t * Aig_ManDupOrpos( Aig_Man_t * p, int fAddRegs )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pMiter;
+    int i;
+    assert( Aig_ManRegNum(p) > 0 );
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    // set registers
+    pNew->nRegs    = fAddRegs? p->nRegs : 0;
+    pNew->nTruePis = fAddRegs? p->nTruePis : p->nTruePis + p->nRegs;
+    pNew->nTruePos = 1;
+    // duplicate internal nodes
+    Aig_ManForEachNode( p, pObj, i )
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // create the PO
+    pMiter = Aig_ManConst0(pNew);
+    Aig_ManForEachPoSeq( p, pObj, i )
+        pMiter = Aig_Or( pNew, pMiter, Aig_ObjChild0Copy(pObj) ); 
+    Aig_ObjCreatePo( pNew, pMiter );
+    // create register inputs with MUXes
+    if ( fAddRegs )
+    {
+        Aig_ManForEachLiSeq( p, pObj, i )
+            Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    }
+    Aig_ManCleanup( pNew );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG with only one primary output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs )
 {
     Aig_Man_t * pNew;
@@ -1018,6 +1063,57 @@ Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs )
     return pNew;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG with only one primary output.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Aig_ManDupUnsolvedOutputs( Aig_Man_t * p, int fAddRegs )
+{ 
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i, nOuts = 0;
+    assert( Aig_ManRegNum(p) > 0 );
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    // create the POs
+    nOuts = 0;
+    Aig_ManForEachPoSeq( p, pObj, i )
+        nOuts += ( Aig_ObjFanin0(pObj) != Aig_ManConst1(p) );
+    // set registers
+    pNew->nRegs    = fAddRegs? p->nRegs : 0;
+    pNew->nTruePis = fAddRegs? p->nTruePis : p->nTruePis + p->nRegs;
+    pNew->nTruePos = nOuts;
+    // duplicate internal nodes
+    Aig_ManForEachNode( p, pObj, i )
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // create the PO
+    Aig_ManForEachPoSeq( p, pObj, i )
+        if ( Aig_ObjFanin0(pObj) != Aig_ManConst1(p) )
+            Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    // create register inputs with MUXes
+    if ( fAddRegs )
+    {
+        Aig_ManForEachLiSeq( p, pObj, i )
+            Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    }
+    Aig_ManCleanup( pNew );
+    return pNew;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/aig/aigMan.c b/src/aig/aig/aigMan.c
index 0b6ff6bd..11d3f3d7 100644
--- a/src/aig/aig/aigMan.c
+++ b/src/aig/aig/aigMan.c
@@ -373,8 +373,8 @@ void Aig_ManPrintStats( Aig_Man_t * p )
 {
     int nChoices = Aig_ManChoiceNum(p);
     printf( "%-15s : ",      p->pName );
-    printf( "pi = %5d  ",    Aig_ManPiNum(p) );
-    printf( "po = %5d  ",    Aig_ManPoNum(p) );
+    printf( "pi = %5d  ",    Aig_ManPiNum(p)-Aig_ManRegNum(p) );
+    printf( "po = %5d  ",    Aig_ManPoNum(p)-Aig_ManRegNum(p) );
     if ( Aig_ManRegNum(p) )
     printf( "lat = %5d  ", Aig_ManRegNum(p) );
     printf( "and = %7d  ",   Aig_ManAndNum(p) );
diff --git a/src/aig/aig/aigPart.c b/src/aig/aig/aigPart.c
index 6e0cb3e8..6849ba70 100644
--- a/src/aig/aig/aigPart.c
+++ b/src/aig/aig/aigPart.c
@@ -1223,6 +1223,7 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
 //    extern void * Abc_FrameGetGlobalFrame();
     extern Aig_Man_t * Fra_FraigChoice( Aig_Man_t * pManAig, int nConfMax, int nLevelMax );
 
+    Vec_Ptr_t * vPios;
     Vec_Ptr_t * vOutsTotal, * vOuts;
     Aig_Man_t * pAigTotal, * pAigPart, * pAig, * pTemp;
     Vec_Int_t * vPart, * vPartSupp;
@@ -1323,8 +1324,10 @@ Aig_Man_t * Aig_ManChoicePartitioned( Vec_Ptr_t * vAigs, int nPartSize, int nCon
     // create the equivalent nodes lists
     Aig_ManMarkValidChoices( pAig );
     // reconstruct the network
-    pAig = Aig_ManDupDfsGuided( pTemp = pAig, Vec_PtrEntry(vAigs,0) );
+    vPios = Aig_ManOrderPios( pAig, Vec_PtrEntry(vAigs,0) );
+    pAig = Aig_ManDupDfsGuided( pTemp = pAig, vPios );
     Aig_ManStop( pTemp );
+    Vec_PtrFree( vPios );
     // duplicate the timing manager
     pTemp = Vec_PtrEntry( vAigs, 0 );
     if ( pTemp->pManTime )
@@ -1541,6 +1544,7 @@ void Aig_ManChoiceEval( Aig_Man_t * p )
 ***********************************************************************/
 Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
 {
+    Vec_Ptr_t * vPios;
     Aig_Man_t * pNew, * pThis, * pPrev, * pTemp;
     int i;
     // start AIG with choices
@@ -1562,8 +1566,10 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
     // create the equivalent nodes lists
     Aig_ManMarkValidChoices( pNew );
     // reconstruct the network
-    pNew = Aig_ManDupDfsGuided( pTemp = pNew, Vec_PtrEntry( vAigs, 0 ) );
+    vPios = Aig_ManOrderPios( pNew, Vec_PtrEntry( vAigs, 0 ) );
+    pNew = Aig_ManDupDfsGuided( pTemp = pNew, vPios );
     Aig_ManStop( pTemp );
+    Vec_PtrFree( vPios );
     // duplicate the timing manager
     pTemp = Vec_PtrEntry( vAigs, 0 );
     if ( pTemp->pManTime )
@@ -1573,6 +1579,12 @@ Aig_Man_t * Aig_ManChoiceConstructive( Vec_Ptr_t * vAigs, int fVerbose )
     return pNew;
 }
 
+/*
+    Vec_Ptr_t * vPios;
+    vPios = Aig_ManOrderPios( pMan, pAig );
+    Vec_PtrFree( vPios );
+*/
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigUtil.c b/src/aig/aig/aigUtil.c
index d49fffd3..f51b8871 100644
--- a/src/aig/aig/aigUtil.c
+++ b/src/aig/aig/aigUtil.c
@@ -1278,6 +1278,133 @@ void Aig_NodeIntersectLists( Vec_Ptr_t * vArr1, Vec_Ptr_t * vArr2, Vec_Ptr_t * v
     assert( vArr->nSize <= vArr2->nSize );
 }
 
+#include "fra.h"
+#include "saig.h"
+
+extern void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Fra_Cex_t * pCex );
+extern void Aig_ManCounterExampleValueStop( Aig_Man_t * pAig );
+extern int Aig_ManCounterExampleValueLookup(  Aig_Man_t * pAig, int Id, int iFrame );
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the process of retuning values for internal nodes.]
+
+  Description [Should be called when pCex is available, before probing 
+  any object for its value using Aig_ManCounterExampleValueLookup().]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManCounterExampleValueStart( Aig_Man_t * pAig, Fra_Cex_t * pCex )
+{
+    Aig_Obj_t * pObj, * pObjRi, * pObjRo;
+    int Val0, Val1, nObjs, i, k, iBit = 0;
+    assert( Aig_ManRegNum(pAig) > 0 ); // makes sense only for sequential AIGs
+    assert( pAig->pData2 == NULL );    // if this fail, there may be a memory leak
+    // allocate memory to store simulation bits for internal nodes
+    pAig->pData2 = ABC_CALLOC( unsigned, Aig_BitWordNum( (pCex->iFrame + 1) * Aig_ManObjNum(pAig) ) );
+    // the register values in the counter-example should be zero
+    Saig_ManForEachLo( pAig, pObj, k )
+        assert( Aig_InfoHasBit(pCex->pData, iBit++) == 0 );
+    // iterate through the timeframes
+    nObjs = Aig_ManObjNum(pAig);
+    for ( i = 0; i <= pCex->iFrame; i++ )
+    {
+        // set constant 1 node
+        Aig_InfoSetBit( pAig->pData2, nObjs * i + 0 );
+        // set primary inputs according to the counter-example
+        Saig_ManForEachPi( pAig, pObj, k )
+            if ( Aig_InfoHasBit(pCex->pData, iBit++) )
+                Aig_InfoSetBit( pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
+        // compute values for each node
+        Aig_ManForEachNode( pAig, pObj, k )
+        {
+            Val0 = Aig_InfoHasBit( pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
+            Val1 = Aig_InfoHasBit( pAig->pData2, nObjs * i + Aig_ObjFaninId1(pObj) );
+            if ( (Val0 ^ Aig_ObjFaninC0(pObj)) & (Val1 ^ Aig_ObjFaninC1(pObj)) )
+                Aig_InfoSetBit( pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
+        }
+        // derive values for combinational outputs
+        Aig_ManForEachPo( pAig, pObj, k )
+        {
+            Val0 = Aig_InfoHasBit( pAig->pData2, nObjs * i + Aig_ObjFaninId0(pObj) );
+            if ( Val0 ^ Aig_ObjFaninC0(pObj) )
+                Aig_InfoSetBit( pAig->pData2, nObjs * i + Aig_ObjId(pObj) );
+        }
+        if ( i == pCex->iFrame )
+            continue;
+        // transfer values to the register output of the next frame
+        Saig_ManForEachLiLo( pAig, pObjRi, pObjRo, k )
+            if ( Aig_InfoHasBit( pAig->pData2, nObjs * i + Aig_ObjId(pObjRi) ) )
+                Aig_InfoSetBit( pAig->pData2, nObjs * (i+1) + Aig_ObjId(pObjRo) );
+    }
+    assert( iBit == pCex->nBits );
+    // check that the counter-example is correct, that is, the corresponding output is asserted
+    assert( Aig_InfoHasBit( pAig->pData2, nObjs * pCex->iFrame + Aig_ObjId(Aig_ManPo(pAig, pCex->iPo)) ) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops the process of retuning values for internal nodes.]
+
+  Description [Should be called when probing is no longer needed]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManCounterExampleValueStop( Aig_Man_t * pAig )
+{
+    assert( pAig->pData2 != NULL );    // if this fail, we try to call this procedure more than once
+    free( pAig->pData2 );
+    pAig->pData2 = NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the value of the given object in the given timeframe.]
+
+  Description [Should be called to probe the value of an object with 
+  the given ID (iFrame is a 0-based number of a time frame - should not 
+  exceed the number of timeframes in the original counter-example).]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManCounterExampleValueLookup(  Aig_Man_t * pAig, int Id, int iFrame )
+{
+    assert( Id >= 0 && Id < Aig_ManObjNum(pAig) );
+    return Aig_InfoHasBit( pAig->pData2, Aig_ManObjNum(pAig) * iFrame + Id );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Procedure to test the above code.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Fra_Cex_t * pCex )
+{
+    Aig_Obj_t * pObj = Aig_ManObj( pAig, Aig_ManObjNum(pAig)/2 );
+    int iFrame = ABC_MAX( 0, pCex->iFrame - 1 );
+    printf( "\nUsing counter-example, which asserts output %d in frame %d.\n", pCex->iPo, pCex->iFrame );
+    Aig_ManCounterExampleValueStart( pAig, pCex );
+    printf( "Value of object %d in frame %d is %d.\n", Aig_ObjId(pObj), iFrame,
+        Aig_ManCounterExampleValueLookup(pAig, Aig_ObjId(pObj), iFrame) );
+    Aig_ManCounterExampleValueStop( pAig );
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/bbr/bbr.h b/src/aig/bbr/bbr.h
index ee91fe8b..e5d585ce 100644
--- a/src/aig/bbr/bbr.h
+++ b/src/aig/bbr/bbr.h
@@ -57,7 +57,7 @@ typedef struct Bbr_ImageTree_t_  Bbr_ImageTree_t;
 extern Bbr_ImageTree_t * Bbr_bddImageStart( 
     DdManager * dd, DdNode * bCare,
     int nParts, DdNode ** pbParts,
-    int nVars, DdNode ** pbVars, int fVerbose );
+    int nVars, DdNode ** pbVars, int nBddMax, int fVerbose );
 extern DdNode *    Bbr_bddImageCompute( Bbr_ImageTree_t * pTree, DdNode * bCare );
 extern void        Bbr_bddImageTreeDelete( Bbr_ImageTree_t * pTree );
 extern DdNode *    Bbr_bddImageRead( Bbr_ImageTree_t * pTree );
@@ -74,7 +74,7 @@ extern void        Aig_ManFreeGlobalBdds( Aig_Man_t * p, DdManager * dd );
 extern int         Aig_ManSizeOfGlobalBdds( Aig_Man_t * p );
 extern DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose );
 /*=== bbrReach.c ==========================================================*/
-extern int         Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent );
+extern int         Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/bbr/bbrCex.c b/src/aig/bbr/bbrCex.c
index 41253dbc..4555570a 100644
--- a/src/aig/bbr/bbrCex.c
+++ b/src/aig/bbr/bbrCex.c
@@ -63,7 +63,7 @@ Ssw_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd,
 
     // create the cube of NS variables
     bCubeNs  = Bbr_bddComputeRangeCube( dd, Saig_ManCiNum(p), Saig_ManCiNum(p)+Saig_ManRegNum(p) );    Cudd_Ref( bCubeNs );
-    pTree = Bbr_bddImageStart( dd, bCubeNs, Saig_ManRegNum(p), pbParts, Saig_ManCiNum(p), dd->vars, fVerbose );
+    pTree = Bbr_bddImageStart( dd, bCubeNs, Saig_ManRegNum(p), pbParts, Saig_ManCiNum(p), dd->vars, 100000000, fVerbose );
     Cudd_RecursiveDeref( dd, bCubeNs );
     if ( pTree == NULL )
     {
diff --git a/src/aig/bbr/bbrImage.c b/src/aig/bbr/bbrImage.c
index edd344bf..aed302eb 100644
--- a/src/aig/bbr/bbrImage.c
+++ b/src/aig/bbr/bbrImage.c
@@ -27,7 +27,7 @@
     Helmut Veith, Dong Wang. Non-linear Quantification Scheduling in 
     Image Computation. ICCAD, 2001.
 */
-
+ 
 /*---------------------------------------------------------------------------*/
 /* Constant declarations                                                     */
 /*---------------------------------------------------------------------------*/
@@ -49,6 +49,7 @@ struct Bbr_ImageTree_t_
     int                 nNodesMax;  // the max number of nodes in one iter
     int                 nNodesMaxT; // the overall max number of nodes
     int                 nIter;      // the number of iterations with this tree
+    int                 nBddMax;    // the number of node to stop
 };
 
 struct Bbr_ImageNode_t_
@@ -89,8 +90,6 @@ struct Bbr_ImageVar_t_
 /* Macro declarations                                                        */
 /*---------------------------------------------------------------------------*/
 
-#define BDD_BLOW_UP  2000000
-
 #define     b0     Cudd_Not((dd)->one)
 #define     b1              (dd)->one
 
@@ -116,7 +115,7 @@ static Bbr_ImageNode_t ** Bbr_CreateNodes( DdManager * dd,
 static void Bbr_DeleteParts_rec( Bbr_ImageNode_t * pNode );
 static int Bbr_BuildTreeNode( DdManager * dd, 
     int nNodes, Bbr_ImageNode_t ** pNodes, 
-    int nVars,  Bbr_ImageVar_t ** pVars, int * pfStop );
+    int nVars,  Bbr_ImageVar_t ** pVars, int * pfStop, int nBddMax );
 static Bbr_ImageNode_t * Bbr_MergeTopNodes( DdManager * dd, 
     int nNodes, Bbr_ImageNode_t ** pNodes );
 static void Bbr_bddImageTreeDelete_rec( Bbr_ImageNode_t * pNode );
@@ -166,7 +165,7 @@ static void Bbr_bddPrint( DdManager * dd, DdNode * F );
 Bbr_ImageTree_t * Bbr_bddImageStart( 
     DdManager * dd, DdNode * bCare, // the care set
     int nParts, DdNode ** pbParts,  // the partitions for image computation
-    int nVars, DdNode ** pbVars, int fVerbose )   // the NS and parameter variables (not quantified!)
+    int nVars, DdNode ** pbVars, int nBddMax, int fVerbose )   // the NS and parameter variables (not quantified!)
 {
     Bbr_ImageTree_t * pTree;
     Bbr_ImagePart_t ** pParts;
@@ -184,7 +183,7 @@ Bbr_ImageTree_t * Bbr_bddImageStart(
     pCare  = pNodes[nParts];
 
     // process the nodes
-    while ( Bbr_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars, &fStop ) );
+    while ( Bbr_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars, &fStop, nBddMax ) );
 
     // consider the case of BDD node blowup
     if ( fStop )
@@ -213,6 +212,7 @@ Bbr_ImageTree_t * Bbr_bddImageStart(
     pTree = ABC_ALLOC( Bbr_ImageTree_t, 1 );
     memset( pTree, 0, sizeof(Bbr_ImageTree_t) );
     pTree->pCare = pCare;
+    pTree->nBddMax = nBddMax;
     pTree->fVerbose = fVerbose;
 
     // merge the topmost nodes
@@ -698,7 +698,7 @@ int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_ImageNode_t * pNode )
         if ( pTree->nNodesMax < nNodes )
             pTree->nNodesMax = nNodes;
     }
-    if ( dd->keys-dd->dead > BDD_BLOW_UP )
+    if ( dd->keys-dd->dead > (unsigned)pTree->nBddMax )
         return 0;
     return 1;
 }
@@ -716,7 +716,7 @@ int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_ImageNode_t * pNode )
 ***********************************************************************/
 int Bbr_BuildTreeNode( DdManager * dd, 
     int nNodes, Bbr_ImageNode_t ** pNodes, 
-    int nVars,  Bbr_ImageVar_t ** pVars, int * pfStop )
+    int nVars,  Bbr_ImageVar_t ** pVars, int * pfStop, int nBddMax )
 {
     Bbr_ImageNode_t * pNode1, * pNode2;
     Bbr_ImageVar_t * pVar;
@@ -808,7 +808,7 @@ int Bbr_BuildTreeNode( DdManager * dd,
     }
 
     *pfStop = 0;
-    if ( dd->keys-dd->dead > BDD_BLOW_UP )
+    if ( dd->keys-dd->dead > (unsigned)nBddMax )
     {
         *pfStop = 1;
         return 0;
diff --git a/src/aig/bbr/bbrReach.c b/src/aig/bbr/bbrReach.c
index 1d43f6fb..7d0e4bc0 100644
--- a/src/aig/bbr/bbrReach.c
+++ b/src/aig/bbr/bbrReach.c
@@ -220,11 +220,16 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
     int i, nIters, nBddSize;
     int nThreshold = 10000;
     Vec_Ptr_t * vOnionRings;
+    int status, method;
+
+    status = Cudd_ReorderingStatus( dd, &method );
+    if ( status )
+        Cudd_AutodynDisable( dd );
 
     // start the image computation
     bCubeCs  = Bbr_bddComputeRangeCube( dd, Saig_ManPiNum(p), Saig_ManCiNum(p) );    Cudd_Ref( bCubeCs );
     if ( fPartition )
-        pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), fVerbose );
+        pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), nBddMax, fVerbose );
     else
         pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), fVerbose );
     Cudd_RecursiveDeref( dd, bCubeCs );
@@ -235,6 +240,9 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
         return -1;
     }
 
+    if ( status )
+        Cudd_AutodynEnable( dd, method );
+
     // start the onion rings
     vOnionRings = Vec_PtrAlloc( 1000 );
 
@@ -360,11 +368,11 @@ int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, D
   Description []
                
   SideEffects []
-
+ 
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent )
+int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent )
 {
     DdManager * dd;
     DdNode ** pbParts, ** pbOutputs;
@@ -397,6 +405,10 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fP
     // create the initial state and the variable map
     bInitial  = Aig_ManInitStateVarMap( dd, p, fVerbose );  Cudd_Ref( bInitial );
 
+    // set reordering
+    if ( fReorderImage )
+        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
+
     // check the result
     RetValue = -1;
     for ( i = 0; i < Saig_ManPoNum(p); i++ )
@@ -456,7 +468,7 @@ int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, int nBddMax, int nIterMax, int fP
   SeeAlso     []
 
 ***********************************************************************/
-int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent )
+int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent )
 {
     Ssw_Cex_t * pCexOld, * pCexNew;
     Aig_Man_t * p;
@@ -468,12 +480,12 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, int nBddMax, int nIterMax, int fP
         if ( Aig_ObjRefs(pObj) == 0 )
             break;
     if ( i == Saig_ManPiNum(pInit) )
-        return Aig_ManVerifyUsingBdds_int( pInit, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent );
+        return Aig_ManVerifyUsingBdds_int( pInit, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, fSilent );
     // create new AIG
     p = Aig_ManDupTrim( pInit );
     assert( Aig_ManPiNum(p) < Aig_ManPiNum(pInit) );
     assert( Aig_ManRegNum(p) == Aig_ManRegNum(pInit) );
-    RetValue = Aig_ManVerifyUsingBdds_int( p, nBddMax, nIterMax, fPartition, fReorder, fVerbose, fSilent );
+    RetValue = Aig_ManVerifyUsingBdds_int( p, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, fSilent );
     if ( RetValue != 0 )
     {
         Aig_ManStop( p );
diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h
index 8e14d2ef..fcadb6ab 100644
--- a/src/aig/cec/cec.h
+++ b/src/aig/cec/cec.h
@@ -48,6 +48,7 @@ struct Cec_ParSat_t_
     int              fPolarFlip;    // flops polarity of variables
     int              fCheckMiter;   // the circuit is the miter
     int              fFirstStop;    // stop on the first sat output
+    int              fLearnCls;     // perform clause learning
     int              fVerbose;      // verbose stats
 };
 
diff --git a/src/aig/cec/cecChoice.c b/src/aig/cec/cecChoice.c
index 0662d73d..f51d138d 100644
--- a/src/aig/cec/cecChoice.c
+++ b/src/aig/cec/cecChoice.c
@@ -380,17 +380,17 @@ Gia_Man_t * Gia_ManChoiceMiter( Vec_Ptr_t * vGias )
   SeeAlso     []
 
 ***********************************************************************/
-Gia_Man_t * Cec_ManChoiceComputationVec( Vec_Ptr_t * vGias, Cec_ParChc_t * pPars )
+Gia_Man_t * Cec_ManChoiceComputationVec( Gia_Man_t * pGia, int nGias, Cec_ParChc_t * pPars )
 {
-    Gia_Man_t * pMiter, * pNew;
+    Gia_Man_t * pNew;
     int RetValue;
     // compute equivalences of the miter
-    pMiter = Gia_ManChoiceMiter( vGias );
-    RetValue = Cec_ManChoiceComputation_int( pMiter, pPars );
+//    pMiter = Gia_ManChoiceMiter( vGias );
+    RetValue = Cec_ManChoiceComputation_int( pGia, pPars );
     // derive AIG with choices
-    pNew = Gia_ManEquivToChoices( pMiter, Vec_PtrSize(vGias) );
+    pNew = Gia_ManEquivToChoices( pGia, nGias );
     Gia_ManHasChoices( pNew );
-    Gia_ManStop( pMiter );
+//    Gia_ManStop( pMiter );
     // report the results
     if ( pPars->fVerbose )
     {
@@ -422,11 +422,7 @@ Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc
     Gia_Man_t * pGia;
     if ( 0 ) 
     {
-        Vec_Ptr_t * vGias;
-        vGias = Vec_PtrAlloc( 1 );
-        Vec_PtrPush( vGias, pAig );
-        pGia = Cec_ManChoiceComputationVec( vGias, pParsChc );
-        Vec_PtrFree( vGias );
+        pGia = Cec_ManChoiceComputationVec( pAig, 3, pParsChc );
     }
     else
     {
@@ -439,7 +435,7 @@ Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc
         pManNew = Dar_ManChoiceNew( pMan, pPars );
         pGia = Gia_ManFromAig( pManNew );
         Aig_ManStop( pManNew );
-        Aig_ManStop( pMan );
+//        Aig_ManStop( pMan );
     }
     return pGia;
 }
@@ -455,13 +451,10 @@ Gia_Man_t * Cec_ManChoiceComputation( Gia_Man_t * pAig, Cec_ParChc_t * pParsChc
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
+Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars )
 {
     Cec_ParChc_t ParsChc, * pParsChc = &ParsChc;
-    Vec_Ptr_t * vGias;
-    Gia_Man_t * pGia;
     Aig_Man_t * pAig;
-    int i;
     if ( pPars->fVerbose )
         ABC_PRT( "Synthesis time", pPars->timeSynth );
     Cec_ManChcSetDefaultParams( pParsChc );
@@ -470,14 +463,8 @@ Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
     if ( pParsChc->fUseCSat && pParsChc->nBTLimit > 100 )
         pParsChc->nBTLimit = 100;
     pParsChc->fVerbose = pPars->fVerbose;
-    vGias = Vec_PtrAlloc( 10 );
-    Vec_PtrForEachEntry( vAigs, pAig, i )
-        Vec_PtrPush( vGias, Gia_ManFromAig(pAig) );
-    pGia = Cec_ManChoiceComputationVec( vGias, pParsChc );
-    Gia_ManSetRegNum( pGia, Gia_ManRegNum(Vec_PtrEntry(vGias, 0)) );
-    Vec_PtrForEachEntry( vGias, pAig, i )
-        Gia_ManStop( (Gia_Man_t *)pAig );
-    Vec_PtrFree( vGias );
+    pGia = Cec_ManChoiceComputationVec( pGia, 3, pParsChc );
+    Gia_ManSetRegNum( pGia, Gia_ManRegNum(pGia) );
     pAig = Gia_ManToAig( pGia, 1 );
     Gia_ManStop( pGia );
     return pAig;
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index dc0fc0d0..9820c05c 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -49,6 +49,7 @@ void Cec_ManSatSetDefaultParams( Cec_ParSat_t * p )
     p->fPolarFlip     =       1;  // flops polarity of variables
     p->fCheckMiter    =       0;  // the circuit is the miter
     p->fFirstStop     =       0;  // stop on the first sat output
+    p->fLearnCls      =       0;  // perform clause learning
     p->fVerbose       =       0;  // verbose stats
 }  
 
diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c
index b4076916..96af801d 100644
--- a/src/aig/cec/cecCorr.c
+++ b/src/aig/cec/cecCorr.c
@@ -797,7 +797,7 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
         } 
         pParsSat->nBTLimit *= 10;
         if ( pPars->fUseCSat )
-            vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
+            vCexStore = Tas_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 );
         else
             vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus );
         // refine classes with these counter-examples
@@ -831,8 +831,9 @@ void Cec_ManLSCorrespondenceBmc( Gia_Man_t * pAig, Cec_ParCor_t * pPars, int nPr
 ***********************************************************************/
 int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
 {  
-    int nIterMax = 100000;
-    int nAddFrames = 1; // additional timeframes to simulate
+    int nIterMax     = 100000;
+    int nAddFrames   = 1; // additional timeframes to simulate
+    int fRunBmcFirst = 0;
     Vec_Str_t * vStatus;
     Vec_Int_t * vOutputs;
     Vec_Int_t * vCexStore;
@@ -875,8 +876,8 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
         Cec_ManRefinedClassPrintStats( pAig, NULL, 0, clock() - clk );
     }
     // check the base case
-    if ( !pPars->fLatchCorr || pPars->nFrames > 1 )
-            Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
+    if ( fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
+        Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
     // perform refinement of equivalence classes
     for ( r = 0; r < nIterMax; r++ )
     { 
@@ -926,6 +927,9 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     if ( r == nIterMax )
         printf( "The refinement was not finished. The result may be incorrect.\n" );
     Cec_ManSimStop( pSim );
+    // check the base case
+    if ( !fRunBmcFirst && (!pPars->fLatchCorr || pPars->nFrames > 1) )
+        Cec_ManLSCorrespondenceBmc( pAig, pPars, 0 );
     clkTotal = clock() - clkTotal;
     // report the results
     if ( pPars->fVerbose )
diff --git a/src/aig/cec/cecInt.h b/src/aig/cec/cecInt.h
index 1fd48d55..9c012f73 100644
--- a/src/aig/cec/cecInt.h
+++ b/src/aig/cec/cecInt.h
@@ -199,6 +199,10 @@ extern int                  Cec_ObjSatVarValue( Cec_ManSat_t * p, Gia_Obj_t * pO
 extern void                 Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars );
 extern Vec_Str_t *          Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat_t * pPars, int nRegs, int * pnPats );
 extern Vec_Int_t *          Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Str_t ** pvStatus );
+extern int                  Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj );
+extern int                  Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 );
+extern void                 Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 );
+extern Vec_Int_t *          Cec_ManSatReadCex( Cec_ManSat_t * p );
 /*=== ceFraeep.c ============================================================*/
 extern Gia_Man_t *          Cec_ManFraSpecReduction( Cec_ManFra_t * p );
 extern int                  Cec_ManFraClassesUpdate( Cec_ManFra_t * p, Cec_ManSim_t * pSim, Cec_ManPat_t * pPat, Gia_Man_t * pNew );
diff --git a/src/aig/cec/cecSolve.c b/src/aig/cec/cecSolve.c
index 3a8d8588..1aaf54ff 100644
--- a/src/aig/cec/cecSolve.c
+++ b/src/aig/cec/cecSolve.c
@@ -404,9 +404,9 @@ void Cec_SetActivityFactors_rec( Cec_ManSat_t * p, Gia_Obj_t * pObj, int LevelMi
     float dActConeBumpMax = 20.0;
     int iVar;
     // skip visited variables
-    if ( Gia_ObjIsTravIdCurrent(p->pAig, pObj) )
+    if ( Gia_ObjIsTravIdCurrentArray(p->pAig, pObj) )
         return;
-    Gia_ObjSetTravIdCurrent(p->pAig, pObj);
+    Gia_ObjSetTravIdCurrentArray(p->pAig, pObj);
     // add the PI to the list
     if ( Gia_ObjLevel(p->pAig, pObj) <= LevelMin || Gia_ObjIsCi(pObj) )
         return;
@@ -440,7 +440,7 @@ int Cec_SetActivityFactors( Cec_ManSat_t * p, Gia_Obj_t * pObj )
     // reset the active variables
     veci_resize(&p->pSat->act_vars, 0);
     // prepare for traversal
-    Gia_ManIncrementTravId( p->pAig );
+    Gia_ManIncrementTravIdArray( p->pAig );
     // determine the min and max level to visit
     assert( dActConeRatio > 0 && dActConeRatio < 1 );
     LevelMax = Gia_ObjLevel(p->pAig,pObj);
@@ -465,9 +465,18 @@ int Cec_SetActivityFactors( Cec_ManSat_t * p, Gia_Obj_t * pObj )
 ***********************************************************************/
 int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj )
 {
+    Gia_Obj_t * pObjR = Gia_Regular(pObj);
     int nBTLimit = p->pPars->nBTLimit;
     int Lit, RetValue, status, clk, clk2, nConflicts;
 
+    if ( pObj == Gia_ManConst0(p->pAig) )
+        return 1;
+    if ( pObj == Gia_ManConst1(p->pAig) )
+    {
+        assert( 0 );
+        return 0;
+    }
+
     p->nCallsSince++;  // experiment with this!!!
     p->nSatTotal++;
     
@@ -480,12 +489,12 @@ int Cec_ManSatCheckNode( Cec_ManSat_t * p, Gia_Obj_t * pObj )
 
     // if the nodes do not have SAT variables, allocate them
 clk2 = clock();
-    Cec_CnfNodeAddToSolver( p, Gia_ObjFanin0(pObj) );
+    Cec_CnfNodeAddToSolver( p, pObjR );
 //ABC_PRT( "cnf", clock() - clk2 );
 //printf( "%d \n", p->pSat->size );
 
 clk2 = clock();
-//    Cec_SetActivityFactors( p, Gia_ObjFanin0(pObj) ); 
+//    Cec_SetActivityFactors( p, pObjR ); 
 //ABC_PRT( "act", clock() - clk2 );
 
     // propage unit clauses
@@ -498,10 +507,10 @@ clk2 = clock();
 
     // solve under assumptions
     // A = 1; B = 0     OR     A = 1; B = 1 
-    Lit = toLitCond( Cec_ObjSatNum(p,Gia_ObjFanin0(pObj)), Gia_ObjFaninC0(pObj) );
+    Lit = toLitCond( Cec_ObjSatNum(p,pObjR), Gia_IsComplement(pObj) );
     if ( p->pPars->fPolarFlip )
     {
-        if ( Gia_ObjFanin0(pObj)->fPhase )  Lit = lit_neg( Lit );
+        if ( pObjR->fPhase )  Lit = lit_neg( Lit );
     }
 //Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
 clk = clock();
@@ -541,6 +550,110 @@ p->timeSatUndec += clock() - clk;
     }
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Runs equivalence test for the two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Cec_ManSatCheckNodeTwo( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 )
+{
+    Gia_Obj_t * pObjR1 = Gia_Regular(pObj1);
+    Gia_Obj_t * pObjR2 = Gia_Regular(pObj2);
+    int nBTLimit = p->pPars->nBTLimit;
+    int Lits[2], RetValue, status, clk, clk2, nConflicts;
+
+    if ( pObj1 == Gia_ManConst0(p->pAig) || pObj2 == Gia_ManConst0(p->pAig) || pObj1 == Gia_Not(pObj2) )
+        return 1;
+    if ( pObj1 == Gia_ManConst1(p->pAig) && (pObj2 == NULL || pObj2 == Gia_ManConst1(p->pAig)) )
+    {
+        assert( 0 );
+        return 0;
+    }
+
+    p->nCallsSince++;  // experiment with this!!!
+    p->nSatTotal++;
+    
+    // check if SAT solver needs recycling
+    if ( p->pSat == NULL || 
+        (p->pPars->nSatVarMax && 
+         p->nSatVars > p->pPars->nSatVarMax && 
+         p->nCallsSince > p->pPars->nCallsRecycle) )
+        Cec_ManSatSolverRecycle( p );
+
+    // if the nodes do not have SAT variables, allocate them
+clk2 = clock();
+    Cec_CnfNodeAddToSolver( p, pObjR1 );
+    Cec_CnfNodeAddToSolver( p, pObjR2 );
+//ABC_PRT( "cnf", clock() - clk2 );
+//printf( "%d \n", p->pSat->size );
+
+clk2 = clock();
+//    Cec_SetActivityFactors( p, pObjR1 ); 
+//    Cec_SetActivityFactors( p, pObjR2 ); 
+//ABC_PRT( "act", clock() - clk2 );
+
+    // propage unit clauses
+    if ( p->pSat->qtail != p->pSat->qhead )
+    {
+        status = sat_solver_simplify(p->pSat);
+        assert( status != 0 );
+        assert( p->pSat->qtail == p->pSat->qhead );
+    }
+
+    // solve under assumptions
+    // A = 1; B = 0     OR     A = 1; B = 1 
+    Lits[0] = toLitCond( Cec_ObjSatNum(p,pObjR1), Gia_IsComplement(pObj1) );
+    Lits[1] = toLitCond( Cec_ObjSatNum(p,pObjR2), Gia_IsComplement(pObj2) );
+    if ( p->pPars->fPolarFlip )
+    {
+        if ( pObjR1->fPhase )  Lits[0] = lit_neg( Lits[0] );
+        if ( pObjR2->fPhase )  Lits[1] = lit_neg( Lits[1] );
+    }
+//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
+clk = clock();
+    nConflicts = p->pSat->stats.conflicts;
+
+clk2 = clock();
+    RetValue = sat_solver_solve( p->pSat, Lits, Lits + 2, 
+        (ABC_INT64_T)nBTLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
+//ABC_PRT( "sat", clock() - clk2 );
+
+    if ( RetValue == l_False )
+    {
+p->timeSatUnsat += clock() - clk;
+        Lits[0] = lit_neg( Lits[0] );
+        Lits[1] = lit_neg( Lits[1] );
+        RetValue = sat_solver_addclause( p->pSat, Lits, Lits + 2 );
+        assert( RetValue );
+        p->nSatUnsat++;
+        p->nConfUnsat += p->pSat->stats.conflicts - nConflicts;       
+//printf( "UNSAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
+        return 1;
+    }
+    else if ( RetValue == l_True )
+    {
+p->timeSatSat += clock() - clk;
+        p->nSatSat++;
+        p->nConfSat += p->pSat->stats.conflicts - nConflicts;
+//printf( "SAT after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
+        return 0;
+    }
+    else // if ( RetValue == l_Undef )
+    {
+p->timeSatUndec += clock() - clk;
+        p->nSatUndec++;
+        p->nConfUndec += p->pSat->stats.conflicts - nConflicts;
+//printf( "UNDEC after %d conflicts\n", p->pSat->stats.conflicts - nConflicts );
+        return -1;
+    }
+}
+
 
 /**Function*************************************************************
 
@@ -570,7 +683,7 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
     } 
     Gia_ManSetPhase( pAig );
     Gia_ManLevelNum( pAig );
-    Gia_ManResetTravId( pAig );
+    Gia_ManResetTravIdArray( pAig );
     p = Cec_ManSatCreate( pAig, pPars );
     pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
     Gia_ManForEachCo( pAig, pObj, i )
@@ -583,7 +696,7 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar
         }
         Bar_ProgressUpdate( pProgress, i, "SAT..." );
 clk2 = clock();
-        status = Cec_ManSatCheckNode( p, pObj );
+        status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
         pObj->fMark0 = (status == 0);
         pObj->fMark1 = (status == 1);
 /*
@@ -619,6 +732,22 @@ clk2 = clock();
 
 /**Function*************************************************************
 
+  Synopsis    [Returns the pattern stored.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Cec_ManSatReadCex( Cec_ManSat_t * pSat )
+{
+    return pSat->vCex;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Save values in the cone of influence.]
 
   Description []
@@ -630,9 +759,9 @@ clk2 = clock();
 ***********************************************************************/
 void Cec_ManSatSolveSeq_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Ptr_t * vInfo, int iPat, int nRegs )
 {
-    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+    if ( Gia_ObjIsTravIdCurrentArray(p, pObj) )
         return;
-    Gia_ObjSetTravIdCurrent(p, pObj);
+    Gia_ObjSetTravIdCurrentArray(p, pObj);
     if ( Gia_ObjIsCi(pObj) )
     {
         unsigned * pInfo = Vec_PtrEntry( vInfo, nRegs + Gia_ObjCioId(pObj) );
@@ -670,7 +799,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
     nPatsInit = nPats = 32 * Vec_PtrReadWordsSimInfo(vPatts);
     Gia_ManSetPhase( pAig );
     Gia_ManLevelNum( pAig );
-    Gia_ManResetTravId( pAig );
+    Gia_ManResetTravIdArray( pAig );
     p = Cec_ManSatCreate( pAig, pPars );
     vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
     pProgress = Bar_ProgressStart( stdout, Gia_ManPoNum(pAig) );
@@ -691,7 +820,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
             }
             continue;
         }
-        status = Cec_ManSatCheckNode( p, pObj );
+        status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
 //printf( "output %d   status = %d\n", i, status );
         Vec_StrPush( vStatus, (char)status );
         if ( status != 0 )
@@ -707,7 +836,7 @@ Vec_Str_t * Cec_ManSatSolveSeq( Vec_Ptr_t * vPatts, Gia_Man_t * pAig, Cec_ParSat
         if ( iPat % nPatsInit == 0 )
             iPat++;
         // save the pattern
-        Gia_ManIncrementTravId( pAig );
+        Gia_ManIncrementTravIdArray( pAig );
 //        Vec_IntClear( p->vCex );
         Cec_ManSatSolveSeq_rec( p, pAig, Gia_ObjFanin0(pObj), vPatts, iPat++, nRegs );
 //        Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
@@ -771,9 +900,9 @@ void Cec_ManSatAddToStore( Vec_Int_t * vCexStore, Vec_Int_t * vCex, int Out )
 ***********************************************************************/
 void Cec_ManSatSolveMiter_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * pObj )
 {
-    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+    if ( Gia_ObjIsTravIdCurrentArray(p, pObj) )
         return;
-    Gia_ObjSetTravIdCurrent(p, pObj);
+    Gia_ObjSetTravIdCurrentArray(p, pObj);
     if ( Gia_ObjIsCi(pObj) )
     {
         pSat->nCexLits++;
@@ -787,6 +916,26 @@ void Cec_ManSatSolveMiter_rec( Cec_ManSat_t * pSat, Gia_Man_t * p, Gia_Obj_t * p
 
 /**Function*************************************************************
 
+  Synopsis    [Save patterns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Cec_ManSavePattern( Cec_ManSat_t * p, Gia_Obj_t * pObj1, Gia_Obj_t * pObj2 )
+{
+    Vec_IntClear( p->vCex );
+    Gia_ManIncrementTravIdArray( p->pAig );
+    Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj1) );
+    if ( pObj2 )
+    Cec_ManSatSolveMiter_rec( p, p->pAig, Gia_Regular(pObj2) );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Performs one round of solving for the POs of the AIG.]
 
   Description [Labels the nodes that have been proved (pObj->fMark1) 
@@ -808,7 +957,7 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
     // prepare AIG
     Gia_ManSetPhase( pAig );
     Gia_ManLevelNum( pAig );
-    Gia_ManResetTravId( pAig );
+    Gia_ManResetTravIdArray( pAig );
     // create resulting data-structures
     vStatus = Vec_StrAlloc( Gia_ManPoNum(pAig) );
     vCexStore = Vec_IntAlloc( 10000 );
@@ -834,7 +983,7 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
             }
             continue;
         }
-        status = Cec_ManSatCheckNode( p, pObj );
+        status = Cec_ManSatCheckNode( p, Gia_ObjChild0(pObj) );
         Vec_StrPush( vStatus, (char)status );
         if ( status == -1 )
         {
@@ -845,8 +994,9 @@ Vec_Int_t * Cec_ManSatSolveMiter( Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_St
             continue;
         assert( status == 0 );
         // save the pattern
-        Gia_ManIncrementTravId( pAig );
-        Cec_ManSatSolveMiter_rec( p, pAig, Gia_ObjFanin0(pObj) );
+//        Gia_ManIncrementTravIdArray( pAig );
+//        Cec_ManSatSolveMiter_rec( p, pAig, Gia_ObjFanin0(pObj) );
+        Cec_ManSavePattern( p, Gia_ObjFanin0(pObj), NULL );
 //        Gia_SatVerifyPattern( pAig, pObj, p->vCex, p->vVisits );
         Cec_ManSatAddToStore( vCexStore, p->vCex, i );
     }
diff --git a/src/aig/dar/darScript.c b/src/aig/dar/darScript.c
index 66e6371d..0209165a 100644
--- a/src/aig/dar/darScript.c
+++ b/src/aig/dar/darScript.c
@@ -19,12 +19,16 @@
 ***********************************************************************/
 
 #include "darInt.h"
-//#include "ioa.h"
+#include "dch.h"
+#include "gia.h"
+#include "giaAig.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+        extern void * Tim_ManDup( void * p, int fDiscrete );     
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -419,7 +423,313 @@ ABC_PRT( "Choicing time ", clock() - clk );
 //    return NULL;
 }
 
-#include "dch.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates the AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Dar_ManChoiceMiter_rec( Gia_Man_t * pNew, Gia_Man_t * p, Gia_Obj_t * pObj )
+{
+    if ( ~pObj->Value )
+        return pObj->Value;
+    Dar_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin0(pObj) );
+    if ( Gia_ObjIsCo(pObj) )
+        return pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Dar_ManChoiceMiter_rec( pNew, p, Gia_ObjFanin1(pObj) );
+    return pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the miter of several AIGs for choice computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Dar_ManChoiceMiter( Vec_Ptr_t * vGias )
+{
+    Gia_Man_t * pNew, * pGia, * pGia0;
+    int i, k, iNode, nNodes;
+    // make sure they have equal parameters
+    assert( Vec_PtrSize(vGias) > 0 );
+    pGia0 = Vec_PtrEntry( vGias, 0 );
+    Vec_PtrForEachEntry( vGias, pGia, i )
+    {
+        assert( Gia_ManCiNum(pGia)  == Gia_ManCiNum(pGia0) );
+        assert( Gia_ManCoNum(pGia)  == Gia_ManCoNum(pGia0) );
+        assert( Gia_ManRegNum(pGia) == Gia_ManRegNum(pGia0) );
+        Gia_ManFillValue( pGia );
+        Gia_ManConst0(pGia)->Value = 0;
+    }
+    // start the new manager
+    pNew = Gia_ManStart( Vec_PtrSize(vGias) * Gia_ManObjNum(pGia0) );
+    pNew->pName = Gia_UtilStrsav( pGia0->pName );
+    // create new CIs and assign them to the old manager CIs
+    for ( k = 0; k < Gia_ManCiNum(pGia0); k++ )
+    {
+        iNode = Gia_ManAppendCi(pNew);
+        Vec_PtrForEachEntry( vGias, pGia, i )
+            Gia_ManCi( pGia, k )->Value = iNode; 
+    }
+    // create internal nodes
+    Gia_ManHashAlloc( pNew );
+    for ( k = 0; k < Gia_ManCoNum(pGia0); k++ )
+    {
+        Vec_PtrForEachEntry( vGias, pGia, i )
+            Dar_ManChoiceMiter_rec( pNew, pGia, Gia_ManCo( pGia, k ) );
+    }
+    Gia_ManHashStop( pNew );
+    // check the presence of dangling nodes
+    nNodes = Gia_ManHasDandling( pNew );
+    assert( nNodes == 0 );
+    // finalize
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(pGia0) );
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Reproduces script "compress".]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dar_NewCompress( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose )
+//alias compress2   "b -l; rw -l; rwz -l; b -l; rwz -l; b -l"
+{
+    Aig_Man_t * pTemp;
+
+    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
+    Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
+
+    Dar_ManDefaultRwrParams( pParsRwr );
+    Dar_ManDefaultRefParams( pParsRef );
+
+    pParsRwr->fUpdateLevel = fUpdateLevel;
+    pParsRef->fUpdateLevel = fUpdateLevel;
+
+    pParsRwr->fPower = fPower;
+
+    pParsRwr->fVerbose = 0;//fVerbose;
+    pParsRef->fVerbose = 0;//fVerbose;
+
+//    pAig = Aig_ManDupDfs( pAig ); 
+    if ( fVerbose ) Aig_ManPrintStats( pAig );
+
+    // rewrite
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDupDfs( pTemp = pAig ); 
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) Aig_ManPrintStats( pAig );
+    
+    // refactor
+    Dar_ManRefactor( pAig, pParsRef );
+    pAig = Aig_ManDupDfs( pTemp = pAig ); 
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) Aig_ManPrintStats( pAig );
+
+    // balance
+    if ( fBalance )
+    {
+    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) Aig_ManPrintStats( pAig );
+    }
+
+    pParsRwr->fUseZeros = 1;
+    pParsRef->fUseZeros = 1;
+    
+    // rewrite
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDupDfs( pTemp = pAig ); 
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) Aig_ManPrintStats( pAig );
+
+    return pAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reproduces script "compress2".]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dar_NewCompress2( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fFanout, int fPower, int fLightSynth, int fVerbose )
+//alias compress2   "b -l; rw -l; rf -l; b -l; rw -l; rwz -l; b -l; rfz -l; rwz -l; b -l"
+{
+    Aig_Man_t * pTemp;
+
+    Dar_RwrPar_t ParsRwr, * pParsRwr = &ParsRwr;
+    Dar_RefPar_t ParsRef, * pParsRef = &ParsRef;
+
+    Dar_ManDefaultRwrParams( pParsRwr );
+    Dar_ManDefaultRefParams( pParsRef );
+
+    pParsRwr->fUpdateLevel = fUpdateLevel;
+    pParsRef->fUpdateLevel = fUpdateLevel;
+    pParsRwr->fFanout = fFanout;
+    pParsRwr->fPower = fPower;
+
+    pParsRwr->fVerbose = 0;//fVerbose;
+    pParsRef->fVerbose = 0;//fVerbose;
+
+//    pAig = Aig_ManDupDfs( pAig ); 
+    if ( fVerbose ) Aig_ManPrintStats( pAig );
+
+    // skip if lighter synthesis is requested
+    if ( !fLightSynth )
+    {
+        // rewrite
+        Dar_ManRewrite( pAig, pParsRwr );
+        pAig = Aig_ManDupDfs( pTemp = pAig ); 
+        Aig_ManStop( pTemp );
+        if ( fVerbose ) Aig_ManPrintStats( pAig );
+    
+        // refactor
+        Dar_ManRefactor( pAig, pParsRef );
+        pAig = Aig_ManDupDfs( pTemp = pAig ); 
+        Aig_ManStop( pTemp );
+        if ( fVerbose ) Aig_ManPrintStats( pAig );
+    }
+
+    // balance
+    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) Aig_ManPrintStats( pAig );
+    
+    // skip if lighter synthesis is requested
+    if ( !fLightSynth )
+    {
+        // rewrite
+        Dar_ManRewrite( pAig, pParsRwr );
+        pAig = Aig_ManDupDfs( pTemp = pAig ); 
+        Aig_ManStop( pTemp );
+        if ( fVerbose ) Aig_ManPrintStats( pAig );
+    }
+
+    pParsRwr->fUseZeros = 1;
+    pParsRef->fUseZeros = 1;
+    
+    // rewrite
+    Dar_ManRewrite( pAig, pParsRwr );
+    pAig = Aig_ManDupDfs( pTemp = pAig ); 
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) Aig_ManPrintStats( pAig );
+
+    // skip if lighter synthesis is requested
+    if ( !fLightSynth )
+    {
+        // balance
+        if ( fBalance )
+        {
+        pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+        Aig_ManStop( pTemp );
+        if ( fVerbose ) Aig_ManPrintStats( pAig );
+        }
+    }
+    
+    // refactor
+    Dar_ManRefactor( pAig, pParsRef );
+    pAig = Aig_ManDupDfs( pTemp = pAig ); 
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) Aig_ManPrintStats( pAig );
+    
+    // skip if lighter synthesis is requested
+    if ( !fLightSynth )
+    {
+        // rewrite
+        Dar_ManRewrite( pAig, pParsRwr );
+        pAig = Aig_ManDupDfs( pTemp = pAig ); 
+        Aig_ManStop( pTemp );
+        if ( fVerbose ) Aig_ManPrintStats( pAig );
+    }
+
+    // balance
+    if ( fBalance )
+    {
+    pAig = Dar_ManBalance( pTemp = pAig, fUpdateLevel );
+    Aig_ManStop( pTemp );
+    if ( fVerbose ) Aig_ManPrintStats( pAig );
+    }
+    return pAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reproduces script "compress2".]
+
+  Description [Takes AIG manager, consumes it, and produces GIA manager.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fLightSynth, int fVerbose )
+//alias resyn    "b; rw; rwz; b; rwz; b"
+//alias resyn2   "b; rw; rf; b; rw; rwz; b; rfz; rwz; b"
+{
+    Vec_Ptr_t * vGias;
+    Gia_Man_t * pGia, * pTemp;
+    int i;
+
+    vGias = Vec_PtrAlloc( 3 );
+    pGia = Gia_ManFromAig(pAig);
+    Vec_PtrPush( vGias, pGia );
+
+    pAig = Dar_NewCompress( pAig, fBalance, fUpdateLevel, fPower, fVerbose );
+    pGia = Gia_ManFromAig(pAig);
+    Vec_PtrPush( vGias, pGia );
+//Aig_ManPrintStats( pAig );
+
+    pAig = Dar_NewCompress2( pAig, fBalance, fUpdateLevel, 1, fPower, fLightSynth, fVerbose );
+    pGia = Gia_ManFromAig(pAig);
+    Vec_PtrPush( vGias, pGia );
+//Aig_ManPrintStats( pAig );
+
+    Aig_ManStop( pAig );
+
+    // swap around the first and the last
+    pTemp = Vec_PtrPop( vGias );
+    Vec_PtrPush( vGias, Vec_PtrEntry(vGias,0) );
+    Vec_PtrWriteEntry( vGias, 0, pTemp );
+
+//    Aig_Man_t * pAig;
+//    int i;
+//    printf( "Choicing will be performed with %d AIGs:\n", Vec_PtrSize(p->vAigs) );
+//    Vec_PtrForEachEntry( p->vAigs, pAig, i )
+//        Aig_ManPrintStats( pAig );
+
+    // derive the miter
+    pGia = Dar_ManChoiceMiter( vGias );
+
+    // cleanup
+    Vec_PtrForEachEntry( vGias, pTemp, i )
+        Gia_ManStop( pTemp );
+    Vec_PtrFree( vGias );
+    return pGia;
+}
 
 /**Function*************************************************************
 
@@ -432,6 +742,7 @@ ABC_PRT( "Choicing time ", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
+/*
 Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 {
     extern Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
@@ -465,12 +776,6 @@ if ( fVerbose )
     pPars->timeSynth = clock() - clk;
 
 clk = clock();
-/*
-    if ( fConstruct )
-        pMan = Aig_ManChoiceConstructive( vAigs, fVerbose );
-    else
-        pMan = Aig_ManChoicePartitioned( vAigs, 300, nConfMax, nLevelMax, fVerbose );
-*/
     // perform choice computation
     if ( pPars->fUseGia )
         pMan = Cec_ComputeChoices( vAigs, pPars );
@@ -506,6 +811,144 @@ if ( fVerbose )
     return pMan;
 //    return NULL;
 }
+*/
+
+/**Function*************************************************************
+
+  Synopsis    [Reproduces script "compress2".]
+
+  Description [Consumes the input AIG to reduce memory usage.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManChoiceNewAig( Aig_Man_t * pAig, Dch_Pars_t * pPars )
+{
+    extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
+    extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
+    int fVerbose = pPars->fVerbose;
+    Aig_Man_t * pMan, * pTemp;
+    Vec_Ptr_t * vAigs;
+    Vec_Ptr_t * vPios;
+    void * pManTime;
+    char * pName, * pSpec;
+    int i, clk;
+
+clk = clock();
+    vAigs = Dar_ManChoiceSynthesis( pAig, 1, 1, pPars->fPower, fVerbose );
+pPars->timeSynth = clock() - clk;
+    // swap the first and last network
+    // this should lead to the primary choice being "better" because of synthesis
+    // (it is also important when constructing choices)
+    pMan = Vec_PtrPop( vAigs );
+    Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
+    Vec_PtrWriteEntry( vAigs, 0, pMan );
+
+    // derive the total AIG
+    pMan = Dch_DeriveTotalAig( vAigs );
+    // cleanup
+    Vec_PtrForEachEntry( vAigs, pTemp, i )
+        Aig_ManStop( pTemp );
+    Vec_PtrFree( vAigs );
+
+    // compute choices
+    pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
+    Aig_ManStop( pTemp );
+
+    // save useful things
+    pManTime = pAig->pManTime; pAig->pManTime = NULL;
+    pName = Aig_UtilStrsav( pAig->pName );
+    pSpec = Aig_UtilStrsav( pAig->pSpec );
+
+    // create guidence
+    vPios = Aig_ManOrderPios( pMan, pAig ); 
+    Aig_ManStop( pAig );
+
+    // reconstruct the network
+    pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios );
+    Aig_ManStop( pTemp );
+    Vec_PtrFree( vPios );
+
+    // reset levels
+    pMan->pManTime = pManTime;
+    Aig_ManChoiceLevel( pMan );
+
+    // copy names
+    ABC_FREE( pMan->pName );
+    ABC_FREE( pMan->pSpec );
+    pMan->pName = pName;
+    pMan->pSpec = pSpec;
+    return pMan;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reproduces script "compress2".]
+
+  Description [Consumes the input AIG to reduce memory usage.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Dar_ManChoiceNew( Aig_Man_t * pAig, Dch_Pars_t * pPars )
+{
+    extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
+    extern Aig_Man_t * Dch_DeriveTotalAig( Vec_Ptr_t * vAigs );
+    extern Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
+    int fVerbose = pPars->fVerbose;
+    Aig_Man_t * pMan, * pTemp;
+    Gia_Man_t * pGia;
+    Vec_Ptr_t * vPios;
+    void * pManTime;
+    char * pName, * pSpec;
+    int clk;
+
+    // save useful things
+    pManTime = pAig->pManTime; pAig->pManTime = NULL;
+    pName = Aig_UtilStrsav( pAig->pName );
+    pSpec = Aig_UtilStrsav( pAig->pSpec );
+
+    // perform synthesis
+clk = clock();
+    pGia = Dar_NewChoiceSynthesis( Aig_ManDupDfs(pAig), 1, 1, pPars->fPower, pPars->fLightSynth, 0 );
+pPars->timeSynth = clock() - clk;
+
+    // perform choice computation
+    if ( pPars->fUseGia )
+        pMan = Cec_ComputeChoices( pGia, pPars );
+    else
+    {
+        pMan = Gia_ManToAigSkip( pGia, 3 );
+        Gia_ManStop( pGia );
+        pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
+        Aig_ManStop( pTemp );
+    }
+
+    // create guidence
+    vPios = Aig_ManOrderPios( pMan, pAig ); 
+    Aig_ManStop( pAig );
+
+    // reconstruct the network
+    pMan = Aig_ManDupDfsGuided( pTemp = pMan, vPios );
+    Aig_ManStop( pTemp );
+    Vec_PtrFree( vPios );
+
+    // reset levels
+    pMan->pManTime = pManTime;
+    Aig_ManChoiceLevel( pMan );
+
+    // copy names
+    ABC_FREE( pMan->pName );
+    ABC_FREE( pMan->pSpec );
+    pMan->pName = pName;
+    pMan->pSpec = pSpec;
+    return pMan;
+}
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
diff --git a/src/aig/dch/dch.h b/src/aig/dch/dch.h
index 6157a811..38978164 100644
--- a/src/aig/dch/dch.h
+++ b/src/aig/dch/dch.h
@@ -50,6 +50,7 @@ struct Dch_Pars_t_
     int              fPower;        // uses power-aware rewriting
     int              fUseGia;       // uses GIA package 
     int              fUseCSat;      // uses circuit-based solver
+    int              fLightSynth;   // uses lighter version of synthesis
     int              fVerbose;      // verbose stats
     int              timeSynth;     // synthesis runtime
     int              nNodesAhead;   // the lookahead in terms of nodes
@@ -66,7 +67,7 @@ struct Dch_Pars_t_
 
 /*=== dchCore.c ==========================================================*/
 extern void          Dch_ManSetDefaultParams( Dch_Pars_t * p );
-extern Aig_Man_t *   Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
+extern Aig_Man_t *   Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars );
 
 
 #ifdef __cplusplus
diff --git a/src/aig/dch/dchCore.c b/src/aig/dch/dchCore.c
index 8e854355..4a8d8b53 100644
--- a/src/aig/dch/dchCore.c
+++ b/src/aig/dch/dchCore.c
@@ -49,6 +49,7 @@ void Dch_ManSetDefaultParams( Dch_Pars_t * p )
     p->fPolarFlip     =     1;  // uses polarity adjustment
     p->fSimulateTfo   =     1;  // simulate TFO
     p->fPower         =     0;  // power-aware rewriting
+    p->fLightSynth    =     0;  // uses lighter version of synthesis
     p->fVerbose       =     0;  // verbose stats
     p->nNodesAhead    =  1000;  // the lookahead in terms of nodes
     p->nCallsRecycle  =   100;  // calls to perform before recycling SAT solver
@@ -65,37 +66,35 @@ void Dch_ManSetDefaultParams( Dch_Pars_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Dch_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
+Aig_Man_t * Dch_ComputeChoices( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 {
     Dch_Man_t * p;
     Aig_Man_t * pResult;
     int clk, clkTotal = clock();
-    assert( Vec_PtrSize(vAigs) > 0 );
     // reset random numbers
     Aig_ManRandom(1);
     // start the choicing manager
-    p = Dch_ManCreate( vAigs, pPars );
+    p = Dch_ManCreate( pAig, pPars );
     // compute candidate equivalence classes
 clk = clock(); 
-    p->ppClasses = Dch_CreateCandEquivClasses( p->pAigTotal, pPars->nWords, pPars->fVerbose );
+    p->ppClasses = Dch_CreateCandEquivClasses( pAig, pPars->nWords, pPars->fVerbose );
 p->timeSimInit = clock() - clk;
 //    Dch_ClassesPrint( p->ppClasses, 0 );
     p->nLits = Dch_ClassesLitNum( p->ppClasses );
     // perform SAT sweeping
     Dch_ManSweep( p );
-    // count the number of representatives
-    p->nReprs = Dch_DeriveChoiceCountReprs( p->pAigTotal );
-    // create choices
-clk = clock();
-    pResult = Dch_DeriveChoiceAig( p->pAigTotal );
-p->timeChoice = clock() - clk;
-//    Aig_ManCleanup( p->pAigTotal );
-//    pResult = Aig_ManDupSimpleDfs( p->pAigTotal );
-    // count the number of equivalences and choices
-    p->nEquivs = Dch_DeriveChoiceCountEquivs( pResult );
-    p->nChoices = Aig_ManChoiceNum( pResult );
+    // free memory ahead of time
 p->timeTotal = clock() - clkTotal;
     Dch_ManStop( p );
+    // create choices
+    ABC_FREE( pAig->pTable );
+    pResult = Dch_DeriveChoiceAig( pAig );
+    // count the number of representatives
+    if ( pPars->fVerbose )
+        printf( "STATS:  Reprs = %6d.  Equivs = %6d.  Choices = %6d.\n", 
+               Dch_DeriveChoiceCountReprs( pAig ),
+               Dch_DeriveChoiceCountEquivs( pResult ),
+               Aig_ManChoiceNum( pResult ) );
     return pResult;
 }
 
diff --git a/src/aig/dch/dchInt.h b/src/aig/dch/dchInt.h
index 4e6315a4..a419335d 100644
--- a/src/aig/dch/dchInt.h
+++ b/src/aig/dch/dchInt.h
@@ -51,7 +51,7 @@ struct Dch_Man_t_
     // parameters
     Dch_Pars_t *     pPars;          // choicing parameters
     // AIGs used in the package
-    Vec_Ptr_t *      vAigs;          // user-given AIGs
+//    Vec_Ptr_t *      vAigs;          // user-given AIGs
     Aig_Man_t *      pAigTotal;      // intermediate AIG
     Aig_Man_t *      pAigFraig;      // final AIG
     // equivalence classes
@@ -142,7 +142,7 @@ extern int           Dch_ClassesRefineConst1Group( Dch_Cla_t * p, Vec_Ptr_t * vR
 /*=== dchCnf.c ===================================================*/
 extern void          Dch_CnfNodeAddToSolver( Dch_Man_t * p, Aig_Obj_t * pObj );
 /*=== dchMan.c ===================================================*/
-extern Dch_Man_t *   Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
+extern Dch_Man_t *   Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars );
 extern void          Dch_ManStop( Dch_Man_t * p );
 extern void          Dch_ManSatSolverRecycle( Dch_Man_t * p );
 /*=== dchSat.c ===================================================*/
diff --git a/src/aig/dch/dchMan.c b/src/aig/dch/dchMan.c
index caed0ed5..c8bd8533 100644
--- a/src/aig/dch/dchMan.c
+++ b/src/aig/dch/dchMan.c
@@ -39,15 +39,14 @@
   SeeAlso     []
 
 ***********************************************************************/
-Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
+Dch_Man_t * Dch_ManCreate( Aig_Man_t * pAig, Dch_Pars_t * pPars )
 {
     Dch_Man_t * p;
     // create interpolation manager
     p = ABC_ALLOC( Dch_Man_t, 1 );
     memset( p, 0, sizeof(Dch_Man_t) );
     p->pPars        = pPars;
-    p->vAigs        = vAigs;
-    p->pAigTotal    = Dch_DeriveTotalAig( vAigs );
+    p->pAigTotal    = pAig; //Dch_DeriveTotalAig( vAigs );
     Aig_ManFanoutStart( p->pAigTotal );
     // SAT solving
     p->nSatVars     = 1;
@@ -74,18 +73,14 @@ Dch_Man_t * Dch_ManCreate( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars )
 ***********************************************************************/
 void Dch_ManPrintStats( Dch_Man_t * p )
 {
-//    Aig_Man_t * pAig;
-//    int i;
-//    printf( "Choicing will be performed with %d AIGs:\n", Vec_PtrSize(p->vAigs) );
-//    Vec_PtrForEachEntry( p->vAigs, pAig, i )
-//        Aig_ManPrintStats( pAig );
+    int nNodeNum = Aig_ManNodeNum(p->pAigTotal) / 3;
     printf( "Parameters: Sim words = %d. Conf limit = %d. SAT var max = %d.\n", 
         p->pPars->nWords, p->pPars->nBTLimit, p->pPars->nSatVarMax );
     printf( "AIG nodes : Total = %6d. Dangling = %6d. Main = %6d. (%6.2f %%)\n", 
         Aig_ManNodeNum(p->pAigTotal), 
-        Aig_ManNodeNum(p->pAigTotal)-Aig_ManNodeNum(Vec_PtrEntry(p->vAigs,0)),
-        Aig_ManNodeNum(Vec_PtrEntry(p->vAigs,0)),
-        100.0 * Aig_ManNodeNum(Vec_PtrEntry(p->vAigs,0))/Aig_ManNodeNum(p->pAigTotal) );
+        Aig_ManNodeNum(p->pAigTotal)-nNodeNum,
+        nNodeNum,
+        100.0 * nNodeNum/Aig_ManNodeNum(p->pAigTotal) );
     printf( "SAT solver: Vars = %d. Max cone = %d. Recycles = %d.\n", 
         p->nSatVars, p->nConeMax, p->nRecycles );
     printf( "SAT calls : All = %6d. Unsat = %6d. Sat = %6d. Fail = %6d.\n", 
@@ -108,7 +103,7 @@ void Dch_ManPrintStats( Dch_Man_t * p )
     {
     ABC_PRT( "Synthesis  ", p->pPars->timeSynth );
     }
-}
+} 
 
 /**Function*************************************************************
 
@@ -123,10 +118,9 @@ void Dch_ManPrintStats( Dch_Man_t * p )
 ***********************************************************************/
 void Dch_ManStop( Dch_Man_t * p )
 {
+    Aig_ManFanoutStop( p->pAigTotal );
     if ( p->pPars->fVerbose )
         Dch_ManPrintStats( p );
-    if ( p->pAigTotal )
-        Aig_ManStop( p->pAigTotal );
     if ( p->pAigFraig )
         Aig_ManStop( p->pAigFraig );
     if ( p->ppClasses )
diff --git a/src/aig/fra/fra.h b/src/aig/fra/fra.h
index a2c10367..f661d2e5 100644
--- a/src/aig/fra/fra.h
+++ b/src/aig/fra/fra.h
@@ -128,13 +128,17 @@ struct Fra_Sec_t_
     int              fFraiging;         // enables fraiging at the beginning
     int              fInduction;        // enable the use of induction
     int              fInterpolation;    // enables interpolation
+    int              fInterSeparate;    // enables interpolation for each outputs separately
     int              fReachability;     // enables BDD based reachability
+    int              fReorderImage;     // enables BDD reordering during image computation
     int              fStopOnFirstFail;  // enables stopping after first output of a miter has failed to prove
     int              fUseNewProver;     // the new prover
     int              fSilent;           // disables all output
     int              fVerbose;          // enables verbose reporting of statistics
     int              fVeryVerbose;      // enables very verbose reporting  
     int              TimeLimit;         // enables the timeout
+    int              fReadUnsolved;     // inserts the unsolved model back
+    int              nSMnumber;         // the number of model written
     // internal parameters
     int              fRecursive;        // set to 1 when SEC is called recursively
     int              fReportSolution;   // enables report solution in a special form
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 8064d2ee..72af2466 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -61,7 +61,9 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
     p->fFraiging         =       1;  // enables fraiging at the beginning
     p->fInduction        =       1;  // enables the use of induction (signal correspondence)
     p->fInterpolation    =       1;  // enables interpolation
+    p->fInterSeparate    =       0;  // enables interpolation for each outputs separately
     p->fReachability     =       1;  // enables BDD based reachability
+    p->fReorderImage     =       0;  // enables variable reordering during image computation
     p->fStopOnFirstFail  =       1;  // enables stopping after first output of a miter has failed to prove
     p->fUseNewProver     =       0;  // enables new prover
     p->fSilent           =       0;  // disables all output
@@ -93,6 +95,7 @@ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult )
     int TimeOut = 0;
     int fLatchCorr = 0;
     float TimeLeft = 0.0;
+    pParSec->nSMnumber = -1;
 
     // try the miter before solving
     pNew = Aig_ManDupSimple( p );
@@ -466,14 +469,68 @@ clk = clock();
     {
         Inter_ManParams_t Pars, * pPars = &Pars;
         int Depth;
-
+        ABC_FREE( pNew->pSeqModel );
         Inter_ManSetDefaultParams( pPars );
+//        pPars->nBTLimit = 100;
         pPars->nBTLimit = pParSec->nBTLimitInter;
         pPars->fVerbose = pParSec->fVeryVerbose;
         if ( Saig_ManPoNum(pNew) == 1 )
         {
             RetValue = Inter_ManPerformInterpolation( pNew, pPars, &Depth );
         }
+        else if ( pParSec->fInterSeparate )
+        {
+            Aig_Man_t * pTemp, * pAux;
+            Aig_Obj_t * pObjPo;
+            int i, Counter = 0;
+            Saig_ManForEachPo( pNew, pObjPo, i )
+            { 
+                if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pNew) )
+                    continue;
+                pTemp = Aig_ManDupOneOutput( pNew, i, 1 );
+                pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0 );
+                Aig_ManStop( pAux );
+                if ( Saig_ManRegNum(pTemp) > 0 )
+                {
+                    RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &Depth );
+                    if ( pTemp->pSeqModel )
+                    {
+                        Ssw_Cex_t * pCex;
+                        pCex = pNew->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
+                        pCex->iPo = i;
+                        Aig_ManStop( pTemp );
+                        break;
+                    }
+                    // if solved, remove the output
+                    if ( RetValue == 1 )
+                    {
+                        Aig_ObjPatchFanin0( pNew, pObjPo, Aig_ManConst0(pNew) );
+    //                    printf( "Output %3d : Solved ", i );
+                    }
+                    else
+                    {
+                        Counter++;
+    //                    printf( "Output %3d : Undec  ", i );
+                    }
+                }
+                else
+                    Counter++;
+//                Aig_ManPrintStats( pTemp );
+                Aig_ManStop( pTemp );
+                printf( "Solving output %3d (out of %3d) using interpolation.\r", i, Saig_ManPoNum(pNew) );
+            }
+            Aig_ManCleanup( pNew );
+            if ( pNew->pSeqModel == NULL )
+            {
+                printf( "Interpolation left %d (out of %d) outputs unsolved              \n", Counter, Saig_ManPoNum(pNew) );
+                if ( Counter )
+                    RetValue = -1;
+            }
+            pNew = Aig_ManDupUnsolvedOutputs( pTemp = pNew, 1 );
+            Aig_ManStop( pTemp );
+            pNew = Aig_ManScl( pTemp = pNew, 1, 1, 0 );
+            Aig_ManStop( pTemp );
+        }
         else
         {
             Aig_Man_t * pNewOrpos = Said_ManDupOrpos( pNew );
@@ -481,7 +538,6 @@ clk = clock();
             if ( pNewOrpos->pSeqModel )
             {
                 Ssw_Cex_t * pCex;
-                ABC_FREE( pNew->pSeqModel );
                 pCex = pNew->pSeqModel = pNewOrpos->pSeqModel; pNewOrpos->pSeqModel = NULL;
                 pCex->iPo = Ssw_SmlFindOutputCounterExample( pNew, pNew->pSeqModel );
             }
@@ -505,10 +561,10 @@ ABC_PRT( "Time", clock() - clk );
     // try reachability analysis
     if ( pParSec->fReachability && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManRegNum(pNew) < pParSec->nBddVarsMax )
     {
-        extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent );
+        extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent );
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
         pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
-        RetValue = Aig_ManVerifyUsingBdds( pNew, pParSec->nBddMax, pParSec->nBddIterMax, 1, 1, 0, pParSec->fSilent );
+        RetValue = Aig_ManVerifyUsingBdds( pNew, pParSec->nBddMax, pParSec->nBddIterMax, 1, 1, pParSec->fReorderImage, 0, pParSec->fSilent );
     }
 
 finish:
@@ -541,6 +597,11 @@ ABC_PRT( "Time", clock() - clkTotal );
     }
     else 
     {
+        ///////////////////////////////////
+        // save intermediate result
+        extern void Abc_FrameSetSave1( void * pAig );
+        Abc_FrameSetSave1( Aig_ManDupSimple(pNew) );
+        ///////////////////////////////////
         if ( !pParSec->fSilent )
         {
             printf( "Networks are UNDECIDED.   " );
@@ -555,7 +616,8 @@ ABC_PRT( "Time", clock() - clkTotal );
         {
             static int Counter = 1;
             char pFileName[1000];
-            sprintf( pFileName, "sm%03d.aig", Counter++ );
+            pParSec->nSMnumber = Counter;
+            sprintf( pFileName, "sm%02d.aig", Counter++ );
             Ioa_WriteAiger( pNew, pFileName, 0, 0 );
             printf( "The unsolved reduced miter is written into file \"%s\".\n", pFileName );
         }
diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index 571a6ef8..af92acc9 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -82,7 +82,7 @@ struct Gia_Obj_t_
 
     unsigned       Value;         // application-specific value
 };
-// Value is currently use to store several types of information
+// Value is currently used to store several types of information
 // - pointer to the next node in the hash table during structural hashing
 // - pointer to the node copy during duplication 
 // - traversal ID of the node during traversal
@@ -135,6 +135,7 @@ struct Gia_Man_t_
     Vec_Int_t *    vFlopClasses;  // classes of flops for retiming/merging/etc
     unsigned char* pSwitching;    // switching activity for each object
     Gia_Plc_t *    pPlacement;    // placement of the objects
+    int *          pTravIds;      // separate traversal ID representation
 };
 
 
@@ -309,13 +310,22 @@ static inline void         Gia_ObjRefFanin1Inc(Gia_Man_t * p, Gia_Obj_t * pObj){
 static inline void         Gia_ObjRefFanin0Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin0(pObj));  }
 static inline void         Gia_ObjRefFanin1Dec(Gia_Man_t * p, Gia_Obj_t * pObj){ assert( p->pRefs); Gia_ObjRefDec(p, Gia_ObjFanin1(pObj));  }
 
-static inline void         Gia_ManResetTravId( Gia_Man_t * p )                             { extern void Gia_ManCleanValue( Gia_Man_t * p ); Gia_ManCleanValue( p ); p->nTravIds = 1;  }
-static inline void         Gia_ManIncrementTravId( Gia_Man_t * p )                         { p->nTravIds++;                                 }
-static inline void         Gia_ObjSetTravId( Gia_Obj_t * pObj, int TravId )                { pObj->Value = TravId;                          }
-static inline void         Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj )      { pObj->Value = p->nTravIds;                     }
-static inline void         Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj )     { pObj->Value = p->nTravIds - 1;                 }
-static inline int          Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj )       { return ((int)pObj->Value == p->nTravIds);      }
-static inline int          Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj )      { return ((int)pObj->Value == p->nTravIds - 1);  }
+static inline void         Gia_ManResetTravId( Gia_Man_t * p )                              { extern void Gia_ManCleanValue( Gia_Man_t * p ); Gia_ManCleanValue( p ); p->nTravIds = 1;  }
+static inline void         Gia_ManIncrementTravId( Gia_Man_t * p )                          { p->nTravIds++;                                 }
+static inline void         Gia_ObjSetTravId( Gia_Obj_t * pObj, int TravId )                 { pObj->Value = TravId;                          }
+static inline void         Gia_ObjSetTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj )       { pObj->Value = p->nTravIds;                     }
+static inline void         Gia_ObjSetTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj )      { pObj->Value = p->nTravIds - 1;                 }
+static inline int          Gia_ObjIsTravIdCurrent( Gia_Man_t * p, Gia_Obj_t * pObj )        { return ((int)pObj->Value == p->nTravIds);      }
+static inline int          Gia_ObjIsTravIdPrevious( Gia_Man_t * p, Gia_Obj_t * pObj )       { return ((int)pObj->Value == p->nTravIds - 1);  }
+
+static inline void         Gia_ManResetTravIdArray( Gia_Man_t * p )                         { ABC_FREE( p->pTravIds ); p->pTravIds = ABC_CALLOC( int, Gia_ManObjNum(p) ); p->nTravIds = 1;  }
+static inline void         Gia_ManIncrementTravIdArray( Gia_Man_t * p )                     { p->nTravIds++;                                                    }
+static inline void         Gia_ObjSetTravIdCurrentArray( Gia_Man_t * p, Gia_Obj_t * pObj )  { p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds;                    }
+static inline void         Gia_ObjSetTravIdPreviousArray( Gia_Man_t * p, Gia_Obj_t * pObj ) { p->pTravIds[Gia_ObjId(p, pObj)] = p->nTravIds - 1;                }
+static inline int          Gia_ObjIsTravIdCurrentArray( Gia_Man_t * p, Gia_Obj_t * pObj )   { return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds);          }
+static inline int          Gia_ObjIsTravIdPreviousArray( Gia_Man_t * p, Gia_Obj_t * pObj )  { return (p->pTravIds[Gia_ObjId(p, pObj)] == p->nTravIds - 1);      }
+static inline void         Gia_ObjSetTravIdCurrentArrayId( Gia_Man_t * p, int Id )          { p->pTravIds[Id] = p->nTravIds;                 }
+static inline int          Gia_ObjIsTravIdCurrentArrayId( Gia_Man_t * p, int Id )           { return (p->pTravIds[Id] == p->nTravIds);       }
 
 // AIG construction
 extern void Gia_ObjAddFanout( Gia_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pFanout );
@@ -402,6 +412,7 @@ static inline int Gia_XsimAndCond( int Value0, int fCompl0, int Value1, int fCom
 static inline Gia_Obj_t * Gia_ObjReprObj( Gia_Man_t * p, int Id )            { return p->pReprs[Id].iRepr == GIA_VOID ? NULL : Gia_ManObj( p, p->pReprs[Id].iRepr );                  }
 static inline int         Gia_ObjRepr( Gia_Man_t * p, int Id )               { return p->pReprs[Id].iRepr;         }
 static inline void        Gia_ObjSetRepr( Gia_Man_t * p, int Id, int Num )   { p->pReprs[Id].iRepr = Num;          }
+static inline void        Gia_ObjUnsetRepr( Gia_Man_t * p, int Id )          { p->pReprs[Id].iRepr = GIA_VOID;     }
 
 static inline int         Gia_ObjProved( Gia_Man_t * p, int Id )             { return p->pReprs[Id].fProved;       }
 static inline void        Gia_ObjSetProved( Gia_Man_t * p, int Id )          { p->pReprs[Id].fProved = 1;          }
@@ -423,12 +434,15 @@ static inline int         Gia_ObjNext( Gia_Man_t * p, int Id )               { r
 static inline void        Gia_ObjSetNext( Gia_Man_t * p, int Id, int Num )   { p->pNexts[Id] = Num;                }
 
 static inline int         Gia_ObjIsConst( Gia_Man_t * p, int Id )            { return Gia_ObjRepr(p, Id) == 0;                                   }
+static inline int         Gia_ObjIsUsed( Gia_Man_t * p, int Id )             { return Gia_ObjRepr(p, Id) != GIA_VOID && Gia_ObjNext(p, Id) > 0;  }
 static inline int         Gia_ObjIsHead( Gia_Man_t * p, int Id )             { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) > 0;  }
 static inline int         Gia_ObjIsNone( Gia_Man_t * p, int Id )             { return Gia_ObjRepr(p, Id) == GIA_VOID && Gia_ObjNext(p, Id) == 0; }
 static inline int         Gia_ObjIsTail( Gia_Man_t * p, int Id )             { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) && Gia_ObjNext(p, Id) == 0;                  }
 static inline int         Gia_ObjIsClass( Gia_Man_t * p, int Id )            { return (Gia_ObjRepr(p, Id) > 0 && Gia_ObjRepr(p, Id) != GIA_VOID) || Gia_ObjNext(p, Id) > 0;                   }
 static inline int         Gia_ObjHasSameRepr( Gia_Man_t * p, int i, int k )  { assert( k ); return i? (Gia_ObjRepr(p, i) == Gia_ObjRepr(p, k) && Gia_ObjRepr(p, i) != GIA_VOID) : Gia_ObjRepr(p, k) == 0;  }
 static inline int         Gia_ObjIsFailedPair( Gia_Man_t * p, int i, int k ) { assert( k ); return i? (Gia_ObjFailed(p, i) || Gia_ObjFailed(p, k)) : Gia_ObjFailed(p, k);                     }
+static inline int         Gia_ClassIsPair( Gia_Man_t * p, int i )            { assert( Gia_ObjIsHead(p, i) ); assert( Gia_ObjNext(p, i) ); return Gia_ObjNext(p, Gia_ObjNext(p, i)) == 0;     }
+static inline void        Gia_ClassUndoPair( Gia_Man_t * p, int i )          { assert( Gia_ClassIsPair(p,i) ); Gia_ObjSetRepr(p, Gia_ObjNext(p, i), GIA_VOID); Gia_ObjSetNext(p, i, 0);       }
 
 #define Gia_ManForEachConst( p, i )                            \
     for ( i = 1; i < Gia_ManObjNum(p); i++ ) if ( !Gia_ObjIsConst(p, i) ) {} else
@@ -466,7 +480,9 @@ static inline int *      Gia_ObjGateFanins( Gia_Man_t * p, int Id )         { re
 #define Gia_ManForEachObjReverse( p, pObj, i )                          \
     for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- )
 #define Gia_ManForEachAnd( p, pObj, i )                                 \
-    for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ )  if ( !Gia_ObjIsAnd(pObj) ) {} else
+    for ( i = 0; (i < p->nObjs) && ((pObj) = Gia_ManObj(p, i)); i++ )      if ( !Gia_ObjIsAnd(pObj) ) {} else
+#define Gia_ManForEachAndReverse( p, pObj, i )                          \
+    for ( i = p->nObjs - 1; (i > 0) && ((pObj) = Gia_ManObj(p, i)); i-- )  if ( !Gia_ObjIsAnd(pObj) ) {} else
 #define Gia_ManForEachCi( p, pObj, i )                                  \
     for ( i = 0; (i < Vec_IntSize(p->vCis)) && ((pObj) = Gia_ManCi(p, i)); i++ )
 #define Gia_ManForEachCo( p, pObj, i )                                  \
@@ -498,6 +514,8 @@ extern void                Gia_DumpAiger( Gia_Man_t * p, char * pFilePrefix, int
 extern Vec_Int_t *         Cbs_ManSolveMiter( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
 /*=== giaCsat.c ============================================================*/
 extern Vec_Int_t *         Cbs_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
+/*=== giaCTas.c ============================================================*/
+extern Vec_Int_t *         Tas_ManSolveMiterNc( Gia_Man_t * pGia, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
 /*=== giaCof.c =============================================================*/
 extern void                Gia_ManPrintFanio( Gia_Man_t * pGia, int nNodes );
 extern Gia_Man_t *         Gia_ManDupCof( Gia_Man_t * p, int iVar );
@@ -508,6 +526,7 @@ extern void                Gia_ManCollectCis( Gia_Man_t * p, int * pNodes, int n
 extern void                Gia_ManCollectAnds( Gia_Man_t * p, int * pNodes, int nNodes, Vec_Int_t * vNodes );
 extern int                 Gia_ManSuppSize( Gia_Man_t * p, int * pNodes, int nNodes );
 extern int                 Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes );
+extern Vec_Vec_t *         Gia_ManLevelize( Gia_Man_t * p );
 /*=== giaDup.c ============================================================*/
 extern Gia_Man_t *         Gia_ManDupOrderDfs( Gia_Man_t * p );
 extern Gia_Man_t *         Gia_ManDupOrderDfsReverse( Gia_Man_t * p );
@@ -620,6 +639,7 @@ extern void                Gia_ManCheckMark1( Gia_Man_t * p );
 extern void                Gia_ManCleanValue( Gia_Man_t * p );
 extern void                Gia_ManFillValue( Gia_Man_t * p );
 extern void                Gia_ManSetPhase( Gia_Man_t * p );
+extern void                Gia_ManCleanPhase( Gia_Man_t * p );
 extern int                 Gia_ManLevelNum( Gia_Man_t * p );
 extern void                Gia_ManSetRefs( Gia_Man_t * p );
 extern int *               Gia_ManCreateMuxRefs( Gia_Man_t * p );
@@ -636,6 +656,14 @@ extern void                Gia_ManPrintCounterExample( Gia_Cex_t * p );
 extern int                 Gia_NodeMffcSize( Gia_Man_t * p, Gia_Obj_t * pNode );
 extern int                 Gia_ManHasChoices( Gia_Man_t * p );
 extern int                 Gia_ManHasDandling( Gia_Man_t * p );
+/*=== giaUtil.c ===========================================================*/
+typedef struct Tas_Man_t_  Tas_Man_t;
+extern Tas_Man_t *         Tas_ManAlloc( Gia_Man_t * pAig, int nBTLimit );
+extern void                Tas_ManStop( Tas_Man_t * p );
+extern Vec_Int_t *         Tas_ReadModel( Tas_Man_t * p );
+extern void                Tas_ManSatPrintStats( Tas_Man_t * p );
+extern int                 Tas_ManSolve( Tas_Man_t * p, Gia_Obj_t * pObj, Gia_Obj_t * pObj2 );
+
  
 #ifdef __cplusplus
 }
diff --git a/src/aig/gia/giaAig.c b/src/aig/gia/giaAig.c
index 4b3692e4..07e74e34 100644
--- a/src/aig/gia/giaAig.c
+++ b/src/aig/gia/giaAig.c
@@ -271,6 +271,47 @@ Aig_Man_t * Gia_ManToAig( Gia_Man_t * p, int fChoices )
   SeeAlso     []
 
 ***********************************************************************/
+Aig_Man_t * Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t ** ppNodes;
+    Gia_Obj_t * pObj;
+    int i;
+    assert( p->pNexts == NULL && p->pReprs == NULL );
+    assert( nOutDelta > 0 && Gia_ManCoNum(p) % nOutDelta == 0 );
+    // create the new manager
+    pNew = Aig_ManStart( Gia_ManAndNum(p) );
+    pNew->pName = Gia_UtilStrsav( p->pName );
+//    pNew->pSpec = Gia_UtilStrsav( p->pName );
+    // create the PIs
+    ppNodes = ABC_CALLOC( Aig_Obj_t *, Gia_ManObjNum(p) );
+    ppNodes[0] = Aig_ManConst0(pNew);
+    Gia_ManForEachCi( p, pObj, i )
+        ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePi( pNew );
+    // add logic for the POs
+    Gia_ManForEachCo( p, pObj, i )
+    {
+        Gia_ManToAig_rec( pNew, ppNodes, p, Gia_ObjFanin0(pObj) );        
+        if ( i % nOutDelta != 0 )
+            continue;
+        ppNodes[Gia_ObjId(p, pObj)] = Aig_ObjCreatePo( pNew, Gia_ObjChild0Copy2(ppNodes, pObj, Gia_ObjId(p, pObj)) );
+    }
+    Aig_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    ABC_FREE( ppNodes );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG in the DFS order.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Aig_Man_t * Gia_ManCofactorAig( Aig_Man_t * p, int nFrames, int nCofFanLit )
 {
     Aig_Man_t * pMan;
diff --git a/src/aig/gia/giaAig.h b/src/aig/gia/giaAig.h
index 507e5143..0e29bf06 100644
--- a/src/aig/gia/giaAig.h
+++ b/src/aig/gia/giaAig.h
@@ -50,6 +50,7 @@ extern Gia_Man_t *         Gia_ManFromAig( Aig_Man_t * p );
 extern Gia_Man_t *         Gia_ManFromAigSimple( Aig_Man_t * p );
 extern Gia_Man_t *         Gia_ManFromAigSwitch( Aig_Man_t * p );
 extern Aig_Man_t *         Gia_ManToAig( Gia_Man_t * p, int fChoices );
+extern Aig_Man_t *         Gia_ManToAigSkip( Gia_Man_t * p, int nOutDelta );
 extern void                Gia_ManReprToAigRepr( Aig_Man_t * p, Gia_Man_t * pGia );
  
 #ifdef __cplusplus
diff --git a/src/aig/gia/giaCSat.c b/src/aig/gia/giaCSat.c
index e005dfc2..644ccda5 100644
--- a/src/aig/gia/giaCSat.c
+++ b/src/aig/gia/giaCSat.c
@@ -1020,6 +1020,8 @@ Vec_Int_t * Cbs_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvSt
     // solve for each output
     Gia_ManForEachCo( pAig, pRoot, i )
     {
+//        printf( "\n" );
+
         Vec_IntClear( vCex );
         if ( Gia_ObjIsConst0(Gia_ObjFanin0(pRoot)) )
         {
diff --git a/src/aig/gia/giaDfs.c b/src/aig/gia/giaDfs.c
index 8a3aef92..bcc1748f 100644
--- a/src/aig/gia/giaDfs.c
+++ b/src/aig/gia/giaDfs.c
@@ -264,6 +264,33 @@ int Gia_ManConeSize( Gia_Man_t * p, int * pNodes, int nNodes )
     return Counter;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Levelizes the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Vec_t * Gia_ManLevelize( Gia_Man_t * p )
+{
+    Gia_Obj_t * pObj;
+    Vec_Vec_t * vLevels;
+    int nLevels, Level, i;
+    nLevels = Gia_ManLevelNum( p );
+    vLevels = Vec_VecStart( nLevels + 1 );
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        Level = Gia_ObjLevel( p, pObj );
+        assert( Level <= nLevels );
+        Vec_VecPush( vLevels, Level, pObj );
+    }
+    return vLevels;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/gia/giaEquiv.c b/src/aig/gia/giaEquiv.c
index 041be0f5..8458268c 100644
--- a/src/aig/gia/giaEquiv.c
+++ b/src/aig/gia/giaEquiv.c
@@ -277,6 +277,8 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
     assert( Gia_ManEquivCheckLits( p, nLits ) );
     if ( fVerbose )
     {
+        int Ent;
+/*
         printf( "Const0 = " );
         Gia_ManForEachConst( p, i )
             printf( "%d ", i );
@@ -284,6 +286,18 @@ void Gia_ManEquivPrintClasses( Gia_Man_t * p, int fVerbose, float Mem )
         Counter = 0;
         Gia_ManForEachClass( p, i )
             Gia_ManEquivPrintOne( p, i, ++Counter );
+*/
+        Gia_ManLevelNum( p );
+        Gia_ManForEachClass( p, i )
+            if ( i % 100 == 0 )
+            {
+//                printf( "%d ", Gia_ManEquivCountOne(p, i) );
+                Gia_ClassForEachObj( p, i, Ent )
+                {
+                    printf( "%d ", Gia_ObjLevel( p, Gia_ManObj(p, Ent) ) );
+                }
+                printf( "\n" );
+            }
     }
 }
 
@@ -370,6 +384,15 @@ Gia_Man_t * Gia_ManEquivReduce( Gia_Man_t * p, int fUseAll, int fDualOut, int fV
         printf( "Gia_ManEquivReduce(): Dual-output miter should have even number of POs.\n" );
         return NULL;
     }
+    // check if there are any equivalences defined
+    Gia_ManForEachObj( p, pObj, i )
+        if ( Gia_ObjReprObj(p, i) != NULL )
+            break;
+    if ( i == Gia_ManObjNum(p) )
+    {
+        printf( "Gia_ManEquivReduce(): There are no equivalences to reduce.\n" );
+        return NULL;
+    }
 /*
     if ( !Gia_ManCheckTopoOrder( p ) )
     {
@@ -720,6 +743,16 @@ Gia_Man_t * Gia_ManSpecReduce( Gia_Man_t * p, int fDualOut, int fVerbose )
         printf( "Gia_ManSpecReduce(): Dual-output miter should have even number of POs.\n" );
         return NULL;
     }
+    // check if there are any equivalences defined
+    Gia_ManForEachObj( p, pObj, i )
+        if ( Gia_ObjReprObj(p, i) != NULL )
+            break;
+    if ( i == Gia_ManObjNum(p) )
+    {
+        printf( "Gia_ManSpecReduce(): There are no equivalences to reduce.\n" );
+        return NULL;
+    }
+
 /*
     if ( !Gia_ManCheckTopoOrder( p ) )
     {
diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c
index 7f4da081..37afde13 100644
--- a/src/aig/gia/giaMan.c
+++ b/src/aig/gia/giaMan.c
@@ -70,6 +70,7 @@ void Gia_ManStop( Gia_Man_t * p )
     Vec_IntFree( p->vFlopClasses );
     Vec_IntFree( p->vCis );
     Vec_IntFree( p->vCos );
+    ABC_FREE( p->pTravIds );
     ABC_FREE( p->pPlacement );
     ABC_FREE( p->pSwitching );
     ABC_FREE( p->pCexSeq );
@@ -203,10 +204,10 @@ void Gia_ManPrintStats( Gia_Man_t * p, int fSwitch )
 void Gia_ManPrintStatsShort( Gia_Man_t * p )
 {
     printf( "i/o =%7d/%7d  ", Gia_ManPiNum(p), Gia_ManPoNum(p) );
-//    printf( "ff =%7d  ", Gia_ManRegNum(p) );
+    printf( "ff =%7d  ", Gia_ManRegNum(p) );
     printf( "and =%8d  ", Gia_ManAndNum(p) );
     printf( "lev =%5d  ", Gia_ManLevelNum(p) );
-    printf( "mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) );
+//    printf( "mem =%5.2f Mb", 12.0*Gia_ManObjNum(p)/(1<<20) );
     printf( "\n" );
 }
  
diff --git a/src/aig/gia/giaUtil.c b/src/aig/gia/giaUtil.c
index 54bc98dd..938c6363 100644
--- a/src/aig/gia/giaUtil.c
+++ b/src/aig/gia/giaUtil.c
@@ -317,6 +317,25 @@ void Gia_ManSetPhase( Gia_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Sets phases of the internal nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Gia_ManCleanPhase( Gia_Man_t * p )  
+{
+    Gia_Obj_t * pObj;
+    int i;
+    Gia_ManForEachObj( p, pObj, i )
+        pObj->fPhase = 0;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Assigns levels.]
 
   Description []
@@ -883,17 +902,32 @@ int Gia_ManHasChoices( Gia_Man_t * p )
     Gia_ManForEachObj( p, pObj, i )
     {
         if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
+        {
+//            printf( "%d ", i );
             Counter1++;
+        }
+//        if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
+//            Counter2++;
+    }
+//    printf( "\n" );
+    Gia_ManForEachObj( p, pObj, i )
+    {
+//        if ( Gia_ObjReprObj( p, Gia_ObjId(p, pObj) ) )
+//            Counter1++;
         if ( Gia_ObjNext( p, Gia_ObjId(p, pObj) ) )
+        {
+//            printf( "%d ", i );
             Counter2++;
+        }
     }
+//    printf( "\n" );
     if ( Counter1 == 0 )
     {
         printf( "Warning: AIG has repr data-strucure but not reprs.\n" );
         return 0;
     }
-//    printf( "%d nodes have reprs.\n", Counter1 );
-//    printf( "%d nodes have nexts.\n", Counter2 );
+    printf( "%d nodes have reprs.\n", Counter1 );
+    printf( "%d nodes have nexts.\n", Counter2 );
     // check if there are any internal nodes without fanout
     // make sure all nodes without fanout have representatives
     // make sure all nodes with fanout have no representatives
diff --git a/src/aig/gia/module.make b/src/aig/gia/module.make
index 6f70f7d3..79bfa2fb 100644
--- a/src/aig/gia/module.make
+++ b/src/aig/gia/module.make
@@ -4,6 +4,7 @@ SRC +=    src/aig/gia/gia.c \
     src/aig/gia/giaCof.c \
     src/aig/gia/giaCSatOld.c \
     src/aig/gia/giaCSat.c \
+    src/aig/gia/giaCTas.c \
     src/aig/gia/giaDfs.c \
     src/aig/gia/giaDup.c \
     src/aig/gia/giaEmbed.c \
diff --git a/src/aig/int/int.h b/src/aig/int/int.h
index c9c5cd1a..1487b9bf 100644
--- a/src/aig/int/int.h
+++ b/src/aig/int/int.h
@@ -57,6 +57,7 @@ struct Inter_ManParams_t_
     int  fCheckKstep;   // check using K-step induction
     int  fUseBias;      // bias decisions to global variables
     int  fUseBackward;  // perform backward interpolation
+    int  fUseSeparate;  // solve each output separately
     int  fVerbose;      // print verbose statistics
 };
 
diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c
index cab0302f..6d29dfb9 100644
--- a/src/aig/int/intCore.c
+++ b/src/aig/int/intCore.c
@@ -53,6 +53,7 @@ void Inter_ManSetDefaultParams( Inter_ManParams_t * p )
     p->fCheckKstep  = 1;     // check using K-step induction
     p->fUseBias     = 0;     // bias decisions to global variables
     p->fUseBackward = 0;     // perform backward interpolation
+    p->fUseSeparate = 0;     // solve each output separately
     p->fVerbose     = 0;     // print verbose statistics
 }
 
diff --git a/src/aig/ntl/module.make b/src/aig/ntl/module.make
index 7f885a90..2af0f4e0 100644
--- a/src/aig/ntl/module.make
+++ b/src/aig/ntl/module.make
@@ -6,6 +6,7 @@ SRC +=    src/aig/ntl/ntlCheck.c \
     src/aig/ntl/ntlInsert.c \
     src/aig/ntl/ntlMan.c \
     src/aig/ntl/ntlMap.c \
+    src/aig/ntl/ntlNames.c \
     src/aig/ntl/ntlObj.c \
     src/aig/ntl/ntlReadBlif.c \
     src/aig/ntl/ntlSweep.c \
diff --git a/src/aig/ntl/ntl.h b/src/aig/ntl/ntl.h
index a82b4d6c..0955214e 100644
--- a/src/aig/ntl/ntl.h
+++ b/src/aig/ntl/ntl.h
@@ -76,6 +76,7 @@ struct Ntl_Man_t_
     Vec_Ptr_t *        vVisNodes;      // the nodes of the abstracted part
     Vec_Int_t *        vBox1Cios;      // the first COs of the boxes
     Vec_Int_t *        vRegClasses;    // the classes of registers in the AIG
+    Vec_Int_t *        vRstClasses;    // the classes of reset registers in the AIG
     Aig_Man_t *        pAig;           // the extracted AIG
     Tim_Man_t *        pManTime;       // the timing manager
     int                iLastCi;        // the last true CI
@@ -83,6 +84,7 @@ struct Ntl_Man_t_
     void (*pNalF)(void *);             // additional data
     void (*pNalD)(void *,void *);      // additional data
     void (*pNalW)(void *,void *);      // additional data
+    void (*pNalR)(void *);             // additional data
     // hashing names into models
     Ntl_Mod_t **       pModTable;      // the hash table of names into models
     int                nModTableSize;  // the allocated table size
@@ -112,6 +114,9 @@ struct Ntl_Mod_t_
     // clocks of the model
     Vec_Ptr_t *        vClocks;        // the clock signals
     Vec_Vec_t *        vClockFlops;    // the flops of each clock
+    // resets of the model
+    Vec_Ptr_t *        vResets;        // the reset signals
+    Vec_Vec_t *        vResetFlops;    // the ASYNC flops of each reset
     // delay information
     Vec_Int_t *        vDelays;
     Vec_Int_t *        vTimeInputs;
@@ -121,7 +126,7 @@ struct Ntl_Mod_t_
     Ntl_Mod_t *        pNext;
     void *             pCopy;
     int                nUsed, nRems;
-}; 
+};  
 
 struct Ntl_Reg_t_
 {
@@ -139,6 +144,7 @@ struct Ntl_Obj_t_
     unsigned           Id     : 28;    // object ID
     int                nFanins;        // the number of fanins
     int                nFanouts;       // the number of fanouts
+    int                Reset;          // reset of the flop
     union {                            // functionality
         Ntl_Mod_t *    pImplem;        // model (for boxes)
         char *         pSop;           // SOP (for logic nodes)
@@ -162,9 +168,10 @@ struct Ntl_Net_t_
         int            iTemp;          // other data
     };
     Ntl_Obj_t *        pDriver;        // driver of the net
-    unsigned           NetId     : 28; // unique ID of the net
+    unsigned           NetId     : 27; // unique ID of the net
     unsigned           nVisits   :  2; // the number of times the net is visted
     unsigned           fMark     :  1; // temporary mark
+    unsigned           fMark2    :  1; // temporary mark
     unsigned           fFixed    :  1; // the fixed net
     char               pName[0];       // the name of this net
 };
@@ -329,11 +336,18 @@ extern ABC_DLL void            Ntl_ManFree( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManPrintStats( Ntl_Man_t * p );
 extern ABC_DLL Tim_Man_t *     Ntl_ManReadTimeMan( Ntl_Man_t * p );
 extern ABC_DLL void            Ntl_ManPrintTypes( Ntl_Man_t * p );
+extern ABC_DLL int             Ntl_ManCompareClockClasses( Vec_Ptr_t ** pp1, Vec_Ptr_t ** pp2 );
+extern ABC_DLL void            Ntl_ManPrintClocks( Ntl_Man_t * p );
+extern ABC_DLL void            Ntl_ManPrintResets( Ntl_Man_t * p );
 extern ABC_DLL Ntl_Mod_t *     Ntl_ModelAlloc( Ntl_Man_t * pMan, char * pName );
 extern ABC_DLL Ntl_Mod_t *     Ntl_ModelStartFrom( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
 extern ABC_DLL Ntl_Mod_t *     Ntl_ModelDup( Ntl_Man_t * pManNew, Ntl_Mod_t * pModelOld );
 extern ABC_DLL void            Ntl_ModelFree( Ntl_Mod_t * p );
 extern ABC_DLL Ntl_Mod_t *     Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init );
+extern ABC_DLL int             Ntl_ModelCountLut0( Ntl_Mod_t * p );
+extern ABC_DLL int             Ntl_ModelCountLut1( Ntl_Mod_t * p );
+extern ABC_DLL int             Ntl_ModelCountBuf( Ntl_Mod_t * p );
+extern ABC_DLL int             Ntl_ModelCountInv( Ntl_Mod_t * p );
 /*=== ntlMap.c ============================================================*/
 extern ABC_DLL Vec_Ptr_t *     Ntl_MappingAlloc( int nLuts, int nVars );
 extern ABC_DLL Vec_Ptr_t *     Ntl_MappingFromAig( Aig_Man_t * p );
@@ -350,6 +364,7 @@ extern ABC_DLL Ntl_Obj_t *     Ntl_ModelCreatePiWithName( Ntl_Mod_t * pModel, ch
 extern ABC_DLL char *          Ntl_ManStoreName( Ntl_Man_t * p, char * pName );
 extern ABC_DLL char *          Ntl_ManStoreSop( Aig_MmFlex_t * pMan, char * pSop );
 extern ABC_DLL char *          Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName );
+extern ABC_DLL int             Ntl_ManObjWhichFanout( Ntl_Obj_t * pNode, Ntl_Net_t * pFanout );
 /*=== ntlSweep.c ==========================================================*/
 extern ABC_DLL int             Ntl_ManSweep( Ntl_Man_t * p, int fVerbose );
 /*=== ntlTable.c ==========================================================*/
@@ -374,7 +389,6 @@ extern ABC_DLL Ntl_Man_t *     Ioa_ReadBlif( char * pFileName, int fCheck );
 extern ABC_DLL void            Ioa_WriteBlif( Ntl_Man_t * p, char * pFileName );
 extern ABC_DLL void            Ioa_WriteBlifLogic( Nwk_Man_t * pNtk, Ntl_Man_t * p, char * pFileName );
 /*=== ntlUtil.c ==========================================================*/
-extern ABC_DLL int             Ntl_ModelCountLut1( Ntl_Mod_t * pRoot );
 extern ABC_DLL int             Ntl_ModelGetFaninMax( Ntl_Mod_t * pRoot );
 extern ABC_DLL Ntl_Net_t *     Ntl_ModelFindSimpleNet( Ntl_Net_t * pNetCo );
 extern ABC_DLL int             Ntl_ManCountSimpleCoDrivers( Ntl_Man_t * p );
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 6afeba26..55a961df 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -371,6 +371,7 @@ int Ntl_ManCollapseBoxSeq1_rec( Ntl_Man_t * p, Ntl_Obj_t * pBox, int fSeq )
         pNet->nVisits = 2;
         // remember the class of this register
         Vec_IntPush( p->vRegClasses, p->pNal ? pBox->iTemp : pObj->LatchId.regClass );
+        Vec_IntPush( p->vRstClasses, p->pNal ? pBox->Reset : -1 );
     }
     // compute AIG for the internal nodes
     Ntl_ModelForEachPo( pModel, pObj, i )
@@ -505,6 +506,7 @@ Aig_Man_t * Ntl_ManCollapse( Ntl_Man_t * p, int fSeq )
     assert( Vec_PtrSize(p->vCos) != 0 );
     Vec_IntClear( p->vBox1Cios );
     Vec_IntClear( p->vRegClasses );
+    Vec_IntClear( p->vRstClasses );
     // clear net visited flags
     pRoot = Ntl_ManRootModel(p);
     assert( Ntl_ModelLatchNum(pRoot) == 0 );
@@ -797,6 +799,7 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pMan
             {
                 pNet->pCopy2 = Ntl_ManExtractNwk_rec( p, pNet, pNtk, vCover, vMemory ); 
                 Nwk_ObjAddFanin( pNode, pNet->pCopy2 );
+                pNode->fInvert = (Nwk_ObjFanin0(pNode)->pFunc == Hop_ManConst0(pNtk->pManHop)); // fixed on June 7, 2009
             }
         }
     }
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index e98a3b46..64af98f4 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -423,6 +423,171 @@ Ntl_Man_t * Ntl_ManFraig( Ntl_Man_t * p, int nPartSize, int nConfLimit, int nLev
 
 /**Function*************************************************************
 
+  Synopsis    [Counts the number of resets.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManAigCountResets( Ntl_Man_t * pNtl )
+{
+    Ntl_Mod_t * pModel = Ntl_ManRootModel(pNtl);
+    Ntl_Obj_t * pBox;
+    int i, Counter = -1;
+    Ntl_ModelForEachObj( pModel, pBox, i )
+        Counter = ABC_MAX( Counter, pBox->Reset );
+    return Counter + 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Transforms sequential AIG to allow for async reset.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ntl_ManAigToRst( Ntl_Man_t * pNtl, Aig_Man_t * p )
+{
+    Ntl_Mod_t * pModel = Ntl_ManRootModel(pNtl);
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i, iRegNum, iRstNum, Counter = 0;
+    int nResets = Ntl_ManAigCountResets( pNtl );
+    assert( pNtl->pNal != NULL );
+    assert( Aig_ManRegNum(p) > 0 );
+    assert( Vec_IntSize(pNtl->vRstClasses) == Aig_ManRegNum(p) );
+//printf( "Number of resets before synthesis = %d.\n", nResets );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManSetPioNumbers( p );
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    // create special PIs
+    for ( i = 0; i < nResets; i++ )
+        Aig_ObjCreatePi( pNew );
+    // duplicate internal nodes
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        if ( Aig_ObjIsNode(pObj) )
+            pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        else if ( Aig_ObjIsPo(pObj) )
+            pObj->pData = Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+        else if ( Aig_ObjIsPi(pObj) )
+        {
+//            pObj->pData = Aig_ObjCreatePi( pNew );
+            iRegNum = Aig_ObjPioNum(pObj) - (Aig_ManPiNum(p) - Aig_ManRegNum(p));
+            if ( iRegNum < 0 )
+                continue;
+            iRstNum = Vec_IntEntry(pNtl->vRstClasses, iRegNum);
+            if ( iRstNum < 0 )
+                continue;
+            assert( iRstNum < nResets );
+            pObj->pData = Aig_And( pNew, pObj->pData, Aig_ManPi(pNew, iRstNum) ); // could be NOT(pi)
+            Counter++;
+        }
+        else if ( Aig_ObjIsConst1(pObj) )
+            pObj->pData = Aig_ManConst1(pNew);
+        else
+            assert( 0 );
+    }
+    assert( Aig_ManNodeNum(p) + Counter == Aig_ManNodeNum(pNew) );
+    if ( (Counter = Aig_ManCleanup( pNew )) )
+        printf( "Aig_ManDupOrdered(): Cleanup after AIG duplication removed %d nodes.\n", Counter );
+    Aig_ManSetRegNum( pNew, Aig_ManRegNum(p) );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Remaps equivalence classes from the new nodes to the old ones.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManRemapClassesLcorr( Ntl_Man_t * pNtl, Aig_Man_t * p, Aig_Man_t * pNew )
+{
+    Ntl_Mod_t * pModel = Ntl_ManRootModel(pNtl);
+    Aig_Obj_t * pObj, * pObjRepr, * pObjNew, * pObjNewRepr;
+    int i, nResets = Ntl_ManAigCountResets( pNtl );
+    int nTruePis = Aig_ManPiNum(p) - Aig_ManRegNum(p);
+    assert( pNew->pReprs != NULL );
+    assert( nResets == Aig_ManPiNum(pNew) - Aig_ManPiNum(p) );
+    Aig_ManReprStart( p, Aig_ManObjNumMax(p) );
+    Aig_ManForEachLoSeq( pNew, pObjNew, i )
+    {
+        pObj = Aig_ManPi( p, i - nResets );
+        pObjNewRepr = pNew->pReprs[pObjNew->Id];
+        if ( pObjNewRepr == NULL )
+            continue;
+        if ( pObjNewRepr == Aig_ManConst1(pNew) )
+        {
+            Aig_ObjCreateRepr( p, Aig_ManConst1(p), pObj );
+            continue;
+        }
+        assert( Aig_ObjIsPi(pObjNewRepr) );
+        // find the corresponding representative node
+        pObjRepr = Aig_ManPi( p, Aig_ObjPioNum(pObjNewRepr) - nResets );
+        // if they belong to different domains, quit
+        if ( Vec_IntEntry( pNtl->vRstClasses, Aig_ObjPioNum(pObj) - nTruePis ) != 
+             Vec_IntEntry( pNtl->vRstClasses, Aig_ObjPioNum(pObjRepr) - nTruePis ) )
+            continue;
+        Aig_ObjCreateRepr( p, pObjRepr, pObj );
+    }
+} 
+
+/**Function*************************************************************
+
+  Synopsis    [Remaps equivalence classes from the new nodes to the old ones.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManRemapClassesScorr( Ntl_Man_t * pNtl, Aig_Man_t * p, Aig_Man_t * pNew )
+{
+    Aig_Obj_t * pObj, * pObjRepr, * pObjNew, * pObjNewRepr;
+    int i;
+    // map things back
+    Aig_ManForEachObj( p, pObj, i )
+    {
+        pObjNew = pObj->pData;
+        assert( pObjNew != NULL && !Aig_IsComplement(pObjNew) );
+        pObjNew->pData = pObj;
+    }
+    // remap the classes
+    Aig_ManForEachObj( pNew, pObjNew, i )
+    {
+        pObjNewRepr = pNew->pReprs[pObjNew->Id];
+        if ( pObjNewRepr == NULL )
+            continue;
+        pObj = pObjNew->pData;
+        pObjRepr = pObjNewRepr->pData;    
+        assert( Aig_ObjId(pObjRepr) < Aig_ObjId(pObj) );
+        Aig_ObjCreateRepr( p, pObjRepr, pObj );
+    }
+}
+
+
+/**Function*************************************************************
+
   Synopsis    [Performs sequential cleanup.]
 
   Description []
@@ -451,9 +616,21 @@ Ntl_Man_t * Ntl_ManScl( Ntl_Man_t * p, int fLatchConst, int fLatchEqual, int fVe
 //Ntl_ManPrintStats( pNew );
 //Aig_ManPrintStats( pAigCol );
 
-    // perform SCL for the given design
-    pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
-    Aig_ManStop( pTemp );
+    // perform SCL
+    if ( p->pNal )
+    {
+        Aig_Man_t * pAigRst;
+        pAigRst = Ntl_ManAigToRst( pNew, pAigCol );
+        pTemp = Aig_ManScl( pAigRst, fLatchConst, fLatchEqual, fVerbose );
+        Aig_ManStop( pTemp );
+        Ntl_ManRemapClassesLcorr( pNew, pAigCol, pAigRst );
+        Aig_ManStop( pAigRst );
+    }
+    else
+    {
+        pTemp = Aig_ManScl( pAigCol, fLatchConst, fLatchEqual, fVerbose );
+        Aig_ManStop( pTemp );
+    }
 
     // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
@@ -493,11 +670,23 @@ Ntl_Man_t * Ntl_ManLcorr( Ntl_Man_t * p, int nConfMax, int fScorrGia, int fUseCS
         return pNew;
     }
 
-    // perform LCORR for the given design
+    // perform LCORR
     pPars->fScorrGia = fScorrGia;
     pPars->fUseCSat  = fUseCSat;
-    pTemp = Ssw_LatchCorrespondence( pAigCol, pPars );
-    Aig_ManStop( pTemp );
+    if ( p->pNal )
+    {
+        Aig_Man_t * pAigRst;
+        pAigRst = Ntl_ManAigToRst( pNew, pAigCol );
+        pTemp = Ssw_LatchCorrespondence( pAigRst, pPars );
+        Aig_ManStop( pTemp );
+        Ntl_ManRemapClassesLcorr( pNew, pAigCol, pAigRst );
+        Aig_ManStop( pAigRst );
+    }
+    else
+    {
+        pTemp = Ssw_LatchCorrespondence( pAigCol, pPars );
+        Aig_ManStop( pTemp );
+    }
 
     // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, fVerbose );
@@ -522,6 +711,7 @@ Ntl_Man_t * Ntl_ManSsw( Ntl_Man_t * p, Fra_Ssw_t * pPars )
 {
     Ntl_Man_t * pNew, * pAux;
     Aig_Man_t * pAig, * pAigCol, * pTemp;
+    assert( 0 ); // not updated for nal
 
     // collapse the AIG
     pAig = Ntl_ManExtract( p );
@@ -571,9 +761,21 @@ Ntl_Man_t * Ntl_ManScorr( Ntl_Man_t * p, Ssw_Pars_t * pPars )
         return pNew;
     }
 
-    // perform SCL for the given design
-    pTemp = Ssw_SignalCorrespondence( pAigCol, pPars );
-    Aig_ManStop( pTemp );
+    // perform SCL
+    if ( p->pNal )
+    {
+        Aig_Man_t * pAigRst;
+        pAigRst = Ntl_ManAigToRst( pNew, pAigCol );
+        pTemp = Ssw_SignalCorrespondence( pAigRst, pPars );
+        Aig_ManStop( pTemp );
+        Ntl_ManRemapClassesLcorr( pNew, pAigCol, pAigRst );
+        Aig_ManStop( pAigRst );
+    }
+    else
+    {
+        pTemp = Ssw_SignalCorrespondence( pAigCol, pPars );
+        Aig_ManStop( pTemp );
+    }
 
     // finalize the transformation
     pNew = Ntl_ManFinalize( pAux = pNew, pAig, pAigCol, pPars->fVerbose );
diff --git a/src/aig/ntl/ntlInsert.c b/src/aig/ntl/ntlInsert.c
index eb967bdc..750eb8f7 100644
--- a/src/aig/ntl/ntlInsert.c
+++ b/src/aig/ntl/ntlInsert.c
@@ -290,6 +290,190 @@ void Ntl_ManFindDriver( Ntl_Man_t * p, char * pName )
   SeeAlso     []
 
 ***********************************************************************/
+Ntl_Man_t * Ntl_ManInsertNtk2( Ntl_Man_t * p, Nwk_Man_t * pNtk )
+{
+    int fWriteConstants = 1;
+    char Buffer[1000]; 
+    Vec_Ptr_t * vObjs;
+    Vec_Int_t * vTruth;
+    Vec_Int_t * vCover;
+    Ntl_Mod_t * pRoot;
+    Ntl_Obj_t * pNode;
+    Ntl_Net_t * pNet, * pNetCo;
+    Nwk_Obj_t * pObj, * pFanin;
+    int i, k, nDigits;
+    unsigned * pTruth;
+    assert( Vec_PtrSize(p->vCis) == Nwk_ManCiNum(pNtk) );
+    assert( Vec_PtrSize(p->vCos) == Nwk_ManCoNum(pNtk) );
+    p = Ntl_ManStartFrom( p );
+    pRoot = Ntl_ManRootModel( p );
+    assert( Ntl_ModelNodeNum(pRoot) == 0 );
+    // set the correspondence between the PI/PO nodes
+    Ntl_ManForEachCiNet( p, pNet, i )
+        Nwk_ManCi( pNtk, i )->pCopy = pNet;
+    // create a new node for each LUT
+    vTruth  = Vec_IntAlloc( 1 << 16 );
+    vCover  = Vec_IntAlloc( 1 << 16 );
+    nDigits = Aig_Base10Log( Nwk_ManNodeNum(pNtk) );
+    // go through the nodes in the topological order
+    vObjs = Nwk_ManDfs( pNtk );
+    Vec_PtrForEachEntry( vObjs, pObj, i )
+    {
+        if ( !Nwk_ObjIsNode(pObj) )
+            continue;
+/*
+        if ( fWriteConstants && Nwk_ObjFaninNum(pObj) == 0 )
+        {
+            pObj->pCopy = NULL;
+            continue;
+        }
+*/
+        // skip constant drivers if they only drive COs
+        if ( fWriteConstants && Nwk_ObjFaninNum(pObj) == 0 )
+        {
+            Nwk_Obj_t * pFanout;
+            int i;
+            Nwk_ObjForEachFanout( pObj, pFanout, i )
+                if ( Nwk_ObjIsNode(pFanout) )
+                    break;
+            if ( i == Nwk_ObjFanoutNum(pObj) )
+            {
+                pObj->pCopy = NULL;
+                continue;
+            }
+        }
+
+        pNode = Ntl_ModelCreateNode( pRoot, Nwk_ObjFaninNum(pObj) );
+        pTruth = Hop_ManConvertAigToTruth( pNtk->pManHop, Hop_Regular(pObj->pFunc), Nwk_ObjFaninNum(pObj), vTruth, 0 );
+        if ( Hop_IsComplement(pObj->pFunc) )
+            Kit_TruthNot( pTruth, pTruth, Nwk_ObjFaninNum(pObj) );
+        if ( !Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) && !Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) )
+        {
+            Nwk_ObjForEachFanin( pObj, pFanin, k )
+            {
+                pNet = pFanin->pCopy;
+                if ( pNet == NULL )
+                {
+                    printf( "Ntl_ManInsertNtk(): Internal error: Net not found.\n" );
+                    return 0;
+                }
+                Ntl_ObjSetFanin( pNode, pNet, k );
+            }
+        }
+        else if ( Kit_TruthIsConst0(pTruth, Nwk_ObjFaninNum(pObj)) )
+        {
+            pObj->pFunc = Hop_ManConst0(pNtk->pManHop);
+            pNode->nFanins = 0;
+        }
+        else if ( Kit_TruthIsConst1(pTruth, Nwk_ObjFaninNum(pObj)) )
+        {
+            pObj->pFunc = Hop_ManConst1(pNtk->pManHop);
+            pNode->nFanins = 0;
+        }
+        pNode->pSop = Kit_PlaFromTruth( p->pMemSops, pTruth, Nwk_ObjFaninNum(pObj), vCover );
+        sprintf( Buffer, "lut%0*d", nDigits, i );
+        if ( (pNet = Ntl_ModelFindNet( pRoot, Buffer )) )
+        {
+            printf( "Ntl_ManInsertNtk(): Internal error: Intermediate net name is not unique.\n" );
+            return 0;
+        }
+        pNet = Ntl_ModelFindOrCreateNet( pRoot, Buffer );
+        if ( !Ntl_ModelSetNetDriver( pNode, pNet ) )
+        {
+            printf( "Ntl_ManInsertNtk(): Internal error: Net has more than one fanin.\n" );
+            return 0;
+        }
+        pObj->pCopy = pNet;
+    }
+    Vec_PtrFree( vObjs );
+    Vec_IntFree( vCover );
+    Vec_IntFree( vTruth );
+    // mark the nets driving special boxes
+    if ( p->pNalR )
+        p->pNalR( p );
+    // mark CIs and outputs of the registers
+    Ntl_ManForEachCiNet( p, pNetCo, i )
+        pNetCo->fMark = 1;
+    // update the CO pointers
+    Ntl_ManForEachCoNet( p, pNetCo, i )
+    {
+        if ( pNetCo->fMark )
+            continue; 
+        pNetCo->fMark = 1;
+        // get the corresponding PO and its driver
+        pObj = Nwk_ManCo( pNtk, i );
+        pFanin = Nwk_ObjFanin0( pObj );
+        // get the net driving this PO
+        pNet = pFanin->pCopy; 
+        if ( pNet == NULL ) // constant net
+        {
+            assert( fWriteConstants );
+            pNode = Ntl_ModelCreateNode( pRoot, 0 );
+            pNode->pSop = pObj->fInvert? Ntl_ManStoreSop( p->pMemSops, " 0\n" ) : Ntl_ManStoreSop( p->pMemSops, " 1\n" );
+        }
+        else 
+        if ( Nwk_ObjFanoutNum(pFanin) == 1 && Ntl_ObjIsNode(pNet->pDriver) && !pNet->fMark2 )
+        {
+            pNode = pNet->pDriver;
+            if ( !Ntl_ModelClearNetDriver( pNode, pNet ) )
+            {
+                printf( "Ntl_ManInsertNtk(): Internal error! Net already has no driver.\n" );
+                return NULL;
+            }
+            // remove this net 
+            Ntl_ModelDeleteNet( pRoot, pNet );
+            Vec_PtrWriteEntry( pRoot->vNets, pNet->NetId, NULL );
+            // update node's function
+            if ( pObj->fInvert )
+                Kit_PlaComplement( pNode->pSop );
+        }
+        else
+        {
+/*
+            if ( fWriteConstants && Ntl_ObjFaninNum(pNet->pDriver) == 0 )
+            {
+                pNode = Ntl_ModelCreateNode( pRoot, 0 );
+                pNode->pSop = pObj->fInvert? Ntl_ManStoreSop( p->pMemSops, " 0\n" ) : Ntl_ManStoreSop( p->pMemSops, " 1\n" );
+            }
+            else
+*/
+            {
+//                assert( Ntl_ObjFaninNum(pNet->pDriver) != 0 );
+                pNode = Ntl_ModelCreateNode( pRoot, 1 );
+                pNode->pSop = pObj->fInvert? Ntl_ManStoreSop( p->pMemSops, "0 1\n" ) : Ntl_ManStoreSop( p->pMemSops, "1 1\n" );
+                Ntl_ObjSetFanin( pNode, pNet, 0 );
+            }
+        }
+        // update the CO driver net
+        assert( pNetCo->pDriver == NULL );
+        if ( !Ntl_ModelSetNetDriver( pNode, pNetCo ) )
+        {
+            printf( "Ntl_ManInsertNtk(): Internal error: PO net has more than one fanin.\n" );
+            return NULL;
+        }
+    }
+    // clean CI/CO marks
+    Ntl_ManUnmarkCiCoNets( p );
+    if ( !Ntl_ManCheck( p ) )
+    {
+        printf( "Ntl_ManInsertNtk: The check has failed for design %s.\n", p->pName );
+        return NULL;
+    }
+    return p;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Inserts the given mapping into the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
 {
     char Buffer[1000]; 
@@ -418,7 +602,6 @@ Ntl_Man_t * Ntl_ManInsertNtk( Ntl_Man_t * p, Nwk_Man_t * pNtk )
     return p;
 }
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlMan.c b/src/aig/ntl/ntlMan.c
index da7e2317..a95c2352 100644
--- a/src/aig/ntl/ntlMan.c
+++ b/src/aig/ntl/ntlMan.c
@@ -51,6 +51,7 @@ Ntl_Man_t * Ntl_ManAlloc()
     p->vVisNodes = Vec_PtrAlloc( 1000 );
     p->vBox1Cios = Vec_IntAlloc( 1000 );
     p->vRegClasses = Vec_IntAlloc( 1000 );
+    p->vRstClasses = Vec_IntAlloc( 1000 );
     // start the manager
     p->pMemObjs = Aig_MmFlexStart();
     p->pMemSops = Aig_MmFlexStart();
@@ -123,6 +124,7 @@ Ntl_Man_t * Ntl_ManStartFrom( Ntl_Man_t * pOld )
         {
             ((Ntl_Obj_t *)pBox->pCopy)->pImplem = pBox->pImplem->pCopy;
             ((Ntl_Obj_t *)pBox->pCopy)->iTemp = pBox->iTemp;
+            ((Ntl_Obj_t *)pBox->pCopy)->Reset = pBox->Reset;
         }
     Ntl_ManForEachCiNet( pOld, pNet, i )
         Vec_PtrPush( pNew->vCis, pNet->pCopy );
@@ -197,6 +199,7 @@ void Ntl_ManFree( Ntl_Man_t * p )
     if ( p->vCos )       Vec_PtrFree( p->vCos );
     if ( p->vVisNodes )  Vec_PtrFree( p->vVisNodes );
     if ( p->vRegClasses) Vec_IntFree( p->vRegClasses );
+    if ( p->vRstClasses) Vec_IntFree( p->vRstClasses );
     if ( p->vBox1Cios )  Vec_IntFree( p->vBox1Cios );
     if ( p->pMemObjs )   Aig_MmFlexStop( p->pMemObjs, 0 );
     if ( p->pMemSops )   Aig_MmFlexStop( p->pMemSops, 0 );
@@ -294,14 +297,14 @@ void Nwk_ManPrintStatsShort( Ntl_Man_t * p, Aig_Man_t * pAig, Nwk_Man_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-int Nwk_ManStatsRegs( Ntl_Man_t * p )
+int Ntl_ManStatsRegs( Ntl_Man_t * p )
 {
     Ntl_Mod_t * pRoot;
     Ntl_Obj_t * pObj;
     int i, Counter = 0;
     pRoot = Ntl_ManRootModel( p );
     Ntl_ModelForEachBox( pRoot, pObj, i )
-        if ( strcmp(pObj->pImplem->pName, "dff") == 0 )
+        if ( strcmp(pObj->pImplem->pName, "m_dff") == 0 )
             Counter++;
     return Counter;
 }
@@ -317,6 +320,22 @@ int Nwk_ManStatsRegs( Ntl_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+int Ntl_ManStatsLuts( Ntl_Man_t * p )
+{
+    return Ntl_ModelLut1Num( Ntl_ManRootModel(p) ) + Ntl_ModelNodeNum( Ntl_ManRootModel(p) );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Nwk_ManStatsLuts( Nwk_Man_t * pNtk )
 {
     return pNtk ? Nwk_ManNodeNum(pNtk) : -1;
@@ -353,13 +372,13 @@ int Nwk_ManStatsLevs( Nwk_Man_t * pNtk )
 void Nwk_ManPrintStatsUpdate( Ntl_Man_t * p, Aig_Man_t * pAig, Nwk_Man_t * pNtk,
      int nRegInit, int nLutInit, int nLevInit, int Time )
 {
-    printf( "FF =%7d (%4.1f%%)  ",  Nwk_ManStatsRegs(p),    100.0*(nRegInit-Nwk_ManStatsRegs(p))/nRegInit );
+    printf( "FF =%7d (%5.1f%%)  ",  Ntl_ManStatsRegs(p),    nRegInit ? (100.0*(nRegInit-Ntl_ManStatsRegs(p))/nRegInit) : 0.0 );
     if ( pNtk == NULL )
-        printf( "Mapping is not available.                  " );
+        printf( "Mapping is not available.                    " );
     else
     {
-        printf( "Lut =%7d (%4.1f%%)  ", Nwk_ManStatsLuts(pNtk), 100.0*(nLutInit-Nwk_ManStatsLuts(pNtk))/nLutInit );
-        printf( "Lev =%4d (%4.1f%%)    ", Nwk_ManStatsLevs(pNtk), 100.0*(nLevInit-Nwk_ManStatsLevs(pNtk))/nLevInit );
+        printf( "Lut =%7d (%5.1f%%)  ", Ntl_ManStatsLuts(p), nLutInit ? (100.0*(nLutInit-Ntl_ManStatsLuts(p))/nLutInit) : 0.0 );
+        printf( "Lev =%4d (%5.1f%%)    ", Nwk_ManStatsLevs(pNtk), nLevInit ? (100.0*(nLevInit-Nwk_ManStatsLevs(pNtk))/nLevInit) : 0.0 );
     }
     ABC_PRT( "Time", clock() - Time );
 }
@@ -461,6 +480,101 @@ void Ntl_ManPrintTypes( Ntl_Man_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Procedure used for sorting the nodes in decreasing order of levels.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManCompareClockClasses( Vec_Ptr_t ** pp1, Vec_Ptr_t ** pp2 )
+{
+    int Diff = Vec_PtrSize(*pp1) - Vec_PtrSize(*pp2);
+    if ( Diff > 0 )
+        return -1;
+    if ( Diff < 0 ) 
+        return 1;
+    return 0; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Saves the model type.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManPrintClocks( Ntl_Man_t * p )
+{
+    Vec_Ptr_t * vFlops;
+    Ntl_Net_t * pNet;
+    Ntl_Mod_t * pModel;
+    int i;
+    pModel = Ntl_ManRootModel( p );
+    if ( Ntl_ModelBoxNum(pModel) == 0 )
+        return;
+    if ( pModel->vClockFlops )
+    {
+        printf( "CLOCK STATISTICS:\n" );
+        Vec_VecForEachLevel( pModel->vClockFlops, vFlops, i )
+        {
+            pNet = Vec_PtrEntry( pModel->vClocks, i );
+            printf( "Clock %2d :  Name = %30s   Flops = %6d.\n", i+1, pNet->pName, Vec_PtrSize(vFlops) );
+            if ( i == 10 )
+            {
+                printf( "Skipping... (the total is %d)\n", Vec_VecSize(pModel->vClockFlops) );
+                break;
+            }
+        }
+    }
+//    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Saves the model type.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Ntl_ManPrintResets( Ntl_Man_t * p )
+{
+    Vec_Ptr_t * vFlops;
+    Ntl_Net_t * pNet;
+    Ntl_Mod_t * pModel;
+    int i;
+    pModel = Ntl_ManRootModel( p );
+    if ( Ntl_ModelBoxNum(pModel) == 0 )
+        return;
+    if ( pModel->vResetFlops )
+    {
+        printf( "RESET STATISTICS:\n" );
+        Vec_VecForEachLevel( pModel->vResetFlops, vFlops, i )
+        {
+            pNet = Vec_PtrEntry( pModel->vResets, i );
+            printf( "Reset %2d :  Name = %30s   Flops = %6d.\n", i+1, pNet->pName, Vec_PtrSize(vFlops) );
+            if ( i == 10 )
+            {
+                printf( "Skipping... (the total is %d)\n", Vec_VecSize(pModel->vResetFlops) );
+                break;
+            }
+        }
+    }
+//    printf( "\n" );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Allocates the model.]
 
   Description []
@@ -643,6 +757,8 @@ void Ntl_ModelFree( Ntl_Mod_t * p )
     if ( p->vDelays )       Vec_IntFree( p->vDelays );
     if ( p->vClocks )       Vec_PtrFree( p->vClocks );
     if ( p->vClockFlops )   Vec_VecFree( p->vClockFlops );
+    if ( p->vResets )       Vec_PtrFree( p->vResets );
+    if ( p->vResetFlops )   Vec_VecFree( p->vResetFlops );
     Vec_PtrFree( p->vNets );
     Vec_PtrFree( p->vObjs );
     Vec_PtrFree( p->vPis );
@@ -699,6 +815,90 @@ Ntl_Mod_t * Ntl_ManCreateLatchModel( Ntl_Man_t * pMan, int Init )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Count constant nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCountLut0( Ntl_Mod_t * p )
+{
+    Ntl_Obj_t * pNode;
+    int i, Counter = 0;
+    Ntl_ModelForEachNode( p, pNode, i )
+        if ( Ntl_ObjFaninNum(pNode) == 0 )
+            Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count single-output nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCountLut1( Ntl_Mod_t * p )
+{
+    Ntl_Obj_t * pNode;
+    int i, Counter = 0;
+    Ntl_ModelForEachNode( p, pNode, i )
+        if ( Ntl_ObjFaninNum(pNode) == 1 )
+            Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count buffers]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCountBuf( Ntl_Mod_t * p )
+{
+    Ntl_Obj_t * pNode;
+    int i, Counter = 0;
+    Ntl_ModelForEachNode( p, pNode, i )
+        if ( Ntl_ObjFaninNum(pNode) == 1 && pNode->pSop[0] == '1' )
+            Counter++;
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Count inverters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ModelCountInv( Ntl_Mod_t * p )
+{
+    Ntl_Obj_t * pNode;
+    int i, Counter = 0;
+    Ntl_ModelForEachNode( p, pNode, i )
+        if ( Ntl_ObjFaninNum(pNode) == 1 && pNode->pSop[0] == '0' )
+            Counter++;
+    return Counter;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlObj.c b/src/aig/ntl/ntlObj.c
index 55924db9..4946c4e3 100644
--- a/src/aig/ntl/ntlObj.c
+++ b/src/aig/ntl/ntlObj.c
@@ -160,6 +160,7 @@ Ntl_Obj_t * Ntl_ModelCreateBox( Ntl_Mod_t * pModel, int nFanins, int nFanouts )
     p->Type     = NTL_OBJ_BOX;
     p->nFanins  = nFanins;
     p->nFanouts = nFanouts;
+    p->Reset    = -1;
     pModel->nObjs[NTL_OBJ_BOX]++;
     return p;
 }
@@ -285,6 +286,27 @@ char * Ntl_ManStoreFileName( Ntl_Man_t * p, char * pFileName )
 }
 
 
+/**Function*************************************************************
+
+  Synopsis    [Returns the index of the fanin in the fanin list of the fanout.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ntl_ManObjWhichFanout( Ntl_Obj_t * pNode, Ntl_Net_t * pFanout )
+{
+    Ntl_Net_t * pObj;
+    int i;
+    Ntl_ObjForEachFanout( pNode, pObj, i )
+        if ( pObj == pFanout )
+            return i;
+    return -1;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/ntl/ntlUtil.c b/src/aig/ntl/ntlUtil.c
index 6d1b6c83..6a4b18d5 100644
--- a/src/aig/ntl/ntlUtil.c
+++ b/src/aig/ntl/ntlUtil.c
@@ -30,27 +30,6 @@
 
 /**Function*************************************************************
 
-  Synopsis    [Counts COs that are connected to the internal nodes through invs/bufs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Ntl_ModelCountLut1( Ntl_Mod_t * pRoot )
-{
-    Ntl_Obj_t * pObj;
-    int i, Counter = 0;
-    Ntl_ModelForEachNode( pRoot, pObj, i )
-        if ( Ntl_ObjFaninNum(pObj) == 1 )
-            Counter++;
-    return Counter;
-}
-
-/**Function*************************************************************
-
   Synopsis    [Reads the maximum number of fanins.]
 
   Description []
@@ -370,6 +349,7 @@ Vec_Vec_t * Ntl_ManTransformRegClasses( Ntl_Man_t * pMan, int nSizeMax, int fVer
     if ( Vec_IntSize(pMan->vRegClasses) == 0 )
     {
         printf( "Ntl_ManReportRegClasses(): Register classes are not defined.\n" );
+//        return (Vec_Vec_t *)Vec_PtrAlloc(0);
         return NULL;
     }
     // find the largest class
diff --git a/src/aig/nwk/nwkMap.c b/src/aig/nwk/nwkMap.c
index e6865840..5812358b 100644
--- a/src/aig/nwk/nwkMap.c
+++ b/src/aig/nwk/nwkMap.c
@@ -321,6 +321,7 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToI
             pObjNew = Nwk_ManCreateCo( pNtk );
             pObjNew->fInvert = Aig_ObjFaninC0(pObj);
             Nwk_ObjAddFanin( pObjNew, Aig_ObjFanin0(pObj)->pData );
+//printf( "%d ", pObjNew->Id );
         }
         else if ( Aig_ObjIsConst1(pObj) )
         {
@@ -331,6 +332,7 @@ Nwk_Man_t * Nwk_ManFromIf( If_Man_t * pIfMan, Aig_Man_t * p, Vec_Ptr_t * vAigToI
             assert( 0 );
         pObj->pData = pObjNew;
     }
+//printf( "\n" );
     Vec_PtrFree( vIfToAig );
     pNtk->pManTime = Tim_ManDup( pIfMan->pManTim, 0 );
     Nwk_ManMinimumBase( pNtk, 0 );
diff --git a/src/aig/nwk/nwkUtil.c b/src/aig/nwk/nwkUtil.c
index 10b7b462..9fc292ea 100644
--- a/src/aig/nwk/nwkUtil.c
+++ b/src/aig/nwk/nwkUtil.c
@@ -513,6 +513,49 @@ int Nwk_ManMinimumBaseNode( Nwk_Obj_t * pObj, Vec_Int_t * vTruth, int fVerbose )
   SeeAlso     []
 
 ***********************************************************************/
+int Nwk_ManMinimumBaseInt( Nwk_Man_t * pNtk, int fVerbose )
+{
+    Vec_Int_t * vTruth;
+    Nwk_Obj_t * pObj;
+    int i, Counter = 0;
+    vTruth = Vec_IntAlloc( 1 << 16 );
+    Nwk_ManForEachNode( pNtk, pObj, i )
+        Counter += Nwk_ManMinimumBaseNode( pObj, vTruth, fVerbose );
+    if ( fVerbose && Counter )
+        printf( "Support minimization reduced support of %d nodes.\n", Counter );
+    Vec_IntFree( vTruth );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Minimizes the support of all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Nwk_ManMinimumBaseRec( Nwk_Man_t * pNtk, int fVerbose )
+{
+    int i, clk = clock();
+    for ( i = 0; Nwk_ManMinimumBaseInt( pNtk, fVerbose ); i++ );
+    ABC_PRT( "Minbase", clock() - clk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Minimizes the support of all nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Nwk_ManMinimumBase( Nwk_Man_t * pNtk, int fVerbose )
 {
     Vec_Int_t * vTruth;
@@ -585,6 +628,7 @@ void Nwk_ManRemoveDupFanins( Nwk_Man_t * pNtk, int fVerbose )
         }
     }
     Vec_IntFree( vTruth );
+//    Nwk_ManMinimumBase( pNtk, fVerbose );
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/saig/saigAbs.c b/src/aig/saig/saigAbs.c
index f6845acd..3da92fc0 100644
--- a/src/aig/saig/saigAbs.c
+++ b/src/aig/saig/saigAbs.c
@@ -24,6 +24,7 @@
 #include "satSolver.h"
 #include "satStore.h"
 #include "ssw.h"
+#include "ioa.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -681,7 +682,7 @@ Ssw_Cex_t * Saig_ManCexShrink( Aig_Man_t * p, Aig_Man_t * pAbs, Ssw_Cex_t * pCex
     }
     return pCex;
 }
-
+ 
 /**Function*************************************************************
 
   Synopsis    [Performs proof-based abstraction using BMC of the given depth.]
@@ -859,6 +860,7 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
         printf( "Refining abstraction...\n" );
         for ( Iter = 0; ; Iter++ )
         {
+            char FileName[100];
             pTemp = Saig_ManProofRefine( p, pResult, vFlops, nFramesBmc, nConfMaxBmc, fVerbose );
             if ( pTemp == NULL )
                 break;
@@ -869,9 +871,16 @@ Aig_Man_t * Saig_ManProofAbstraction( Aig_Man_t * p, int nFrames, int nConfMax,
                 Aig_ManPrintStats( pResult );
             else
                 printf( " -----------------------------------------------------\n" );
+            // output the intermediate result of abstraction
+            sprintf( FileName, "gabs%02d.aig", Iter );
+            Ioa_WriteAiger( pResult, FileName, 0, 0 );
+            printf( "Intermediate abstracted model was written into file \"%s\".\n", FileName );
+            // check if the ratio is reached
             if ( 100.0*(Aig_ManRegNum(p)-Aig_ManRegNum(pTemp))/Aig_ManRegNum(p) < 1.0*nRatio )
             {
                 printf( "Refinements is stopped because flop reduction is less than %d%%\n", nRatio );
+                Aig_ManStop( pResult );
+                pResult = NULL;
                 break;
             }
         }
diff --git a/src/aig/saig/saigBmc.c b/src/aig/saig/saigBmc.c
index d56d97a9..57759594 100644
--- a/src/aig/saig/saigBmc.c
+++ b/src/aig/saig/saigBmc.c
@@ -87,7 +87,7 @@ Saig_Bmc_t * Saig_BmcManStart( Aig_Man_t * pAig, int nFramesMax, int nNodesMax,
     Saig_Bmc_t * p;
     Aig_Obj_t * pObj;
     int i, Lit;
-    assert( Aig_ManRegNum(pAig) > 0 );
+//    assert( Aig_ManRegNum(pAig) > 0 );
     p = (Saig_Bmc_t *)ABC_ALLOC( char, sizeof(Saig_Bmc_t) );
     memset( p, 0, sizeof(Saig_Bmc_t) );
     // set parameters
@@ -589,7 +589,7 @@ void Saig_BmcPerform( Aig_Man_t * pAig, int nFramesMax, int nNodesMax, int nConf
             Aig_ManNodeNum(pAig), Aig_ManLevelNum(pAig) );
         printf( "Params: FramesMax = %d. NodesDelta = %d. ConfMaxOne = %d. ConfMaxAll = %d.\n", 
             nFramesMax, nNodesMax, nConfMaxOne, nConfMaxAll );
-    }
+    } 
     for ( Iter = 0; ; Iter++ )
     {
         clk2 = clock();
diff --git a/src/aig/saig/saigBmc2.c b/src/aig/saig/saigBmc2.c
index f8799e38..240168e6 100644
--- a/src/aig/saig/saigBmc2.c
+++ b/src/aig/saig/saigBmc2.c
@@ -162,6 +162,8 @@ Aig_Man_t * Saig_ManFramesBmcLimit( Aig_Man_t * pAig, int nFrames, int nSizeMax
     return pFrames;
 }
 
+#include "utilMem.h"
+
 /**Function*************************************************************
 
   Synopsis    [Performs BMC for the given AIG.]
@@ -228,6 +230,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
     // create the SAT solver
     clk = clock();
     pCnf = Cnf_Derive( pFrames, Aig_ManPoNum(pFrames) );  
+//if ( s_fInterrupt )
+//return -1;
     pSat = sat_solver_new();
     sat_solver_setnvars( pSat, pCnf->nVars );
     for ( i = 0; i < pCnf->nClauses; i++ )
@@ -255,6 +259,8 @@ int Saig_ManBmcSimple( Aig_Man_t * pAig, int nFrames, int nSizeMax, int nConfLim
         int clkPart = clock();
         Aig_ManForEachPo( pFrames, pObj, i )
         {
+//if ( s_fInterrupt )
+//return -1;
             Lit = toLitCond( pCnf->pVarNums[pObj->Id], 0 );
             if ( fVerbose )
             {
diff --git a/src/aig/saig/saigSimExt.c b/src/aig/saig/saigSimExt.c
index ead0ece5..97b91b1d 100644
--- a/src/aig/saig/saigSimExt.c
+++ b/src/aig/saig/saigSimExt.c
@@ -251,7 +251,7 @@ Vec_Int_t * Saig_ManExtendCounterExample( Aig_Man_t * p, int iFirstPi, Ssw_Cex_t
 {
     Vec_Int_t * vRes, * vResInv, * vUndo, * vVis, * vVis2;
     int i, f, Value;
-    assert( Aig_ManRegNum(p) > 0 );
+//    assert( Aig_ManRegNum(p) > 0 );
     assert( (unsigned *)Vec_PtrEntry(vSimInfo,1) - (unsigned *)Vec_PtrEntry(vSimInfo,0) >= Aig_BitWordNum(2*(pCex->iFrame+1)) );
     // start simulation data
     Value = Saig_ManSimDataInit( p, pCex, vSimInfo, NULL );
diff --git a/src/aig/ssw/sswSim.c b/src/aig/ssw/sswSim.c
index deb8d5d4..0e99b1e8 100644
--- a/src/aig/ssw/sswSim.c
+++ b/src/aig/ssw/sswSim.c
@@ -1280,11 +1280,11 @@ void Ssw_SmlFreeCounterExample( Ssw_Cex_t * pCex )
 
 ***********************************************************************/
 int Ssw_SmlRunCounterExample( Aig_Man_t * pAig, Ssw_Cex_t * p )
-{
+{ 
     Ssw_Sml_t * pSml;
     Aig_Obj_t * pObj;
     int RetValue, i, k, iBit;
-    assert( Aig_ManRegNum(pAig) > 0 );
+//    assert( Aig_ManRegNum(pAig) > 0 );
     assert( Aig_ManRegNum(pAig) < Aig_ManPiNum(pAig) );
     // start a new sequential simulator
     pSml = Ssw_SmlStart( pAig, 0, p->iFrame+1, 1 );
diff --git a/src/base/abc/abcNtk.c b/src/base/abc/abcNtk.c
index 6973bb64..ae345467 100644
--- a/src/base/abc/abcNtk.c
+++ b/src/base/abc/abcNtk.c
@@ -1334,7 +1334,7 @@ Abc_Ntk_t * Abc_NtkTrim( Abc_Ntk_t * pNtk )
     // filter POs
     k = m = 0;
     Abc_NtkForEachCo( pNtk, pObj, i )
-    {
+    {  
         if ( Abc_ObjIsPo(pObj) )
         {
             // remove constant nodes and PI pointers
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 660bf3e1..9d04c0bf 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -153,6 +153,7 @@ static int Abc_CommandIFraig         ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandDFraig         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCSweep         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandDProve         ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandDProve2        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbSec          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandSimSec         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMatch          ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -311,6 +312,7 @@ static int Abc_CommandAbc9Force      ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandAbc9Embed      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9If         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Era        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9Dch        ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Test       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
 static int Abc_CommandAbcTestNew     ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -543,6 +545,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Verification", "sec",           Abc_CommandSec,              0 );
     Cmd_CommandAdd( pAbc, "Verification", "dsec",          Abc_CommandDSec,             0 );
     Cmd_CommandAdd( pAbc, "Verification", "dprove",        Abc_CommandDProve,           0 );
+    Cmd_CommandAdd( pAbc, "Verification", "dprove2",       Abc_CommandDProve2,          0 );
     Cmd_CommandAdd( pAbc, "Verification", "absec",         Abc_CommandAbSec,            0 );
     Cmd_CommandAdd( pAbc, "Verification", "simsec",        Abc_CommandSimSec,           0 );
     Cmd_CommandAdd( pAbc, "Verification", "match",         Abc_CommandMatch,            0 );
@@ -631,6 +634,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "AIG",          "&embed",        Abc_CommandAbc9Embed,        0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&if",           Abc_CommandAbc9If,           0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&era",          Abc_CommandAbc9Era,          0 );
+    Cmd_CommandAdd( pAbc, "AIG",          "&dch",          Abc_CommandAbc9Dch,          0 );
     Cmd_CommandAdd( pAbc, "AIG",          "&test",         Abc_CommandAbc9Test,         0 );
 
     Cmd_CommandAdd( pAbc, "Various",      "testnew",         Abc_CommandAbcTestNew,     0 );
@@ -672,6 +676,8 @@ void Abc_Init( Abc_Frame_t * pAbc )
         void For_ManFileExperiment();
 //        For_ManFileExperiment();
     }
+    {
+    }
 
 } 
 
@@ -5437,7 +5443,7 @@ int Abc_CommandMiter( Abc_Frame_t * pAbc, int argc, char ** argv )
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Miter computation has failed.\n" );
-        return 1;
+        return 0;
     }
     // replace the current network
     Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
@@ -6539,23 +6545,24 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nIterMax;
     int fPartition;
     int fReorder;
+    int fReorderImage;
     int fVerbose;
     int c;
-    extern void Abc_NtkVerifyUsingBdds( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
-    extern void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose );
+    extern void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nBddMax    = 50000;
-    nIterMax   = 1000;
-    fPartition = 1;
-    fReorder   = 1;
-    fVerbose   = 0;
+    nBddMax       = 50000;
+    nIterMax      = 1000;
+    fPartition    = 1;
+    fReorder      = 1;
+    fReorderImage = 0;
+    fVerbose      = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "BFprvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "BFprovh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -6587,6 +6594,9 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'r':
             fReorder ^= 1;
             break;
+        case 'o':
+            fReorderImage ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -6626,16 +6636,17 @@ int Abc_CommandReach( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 */
 //    Abc_NtkVerifyUsingBdds( pNtk, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
-    Abc_NtkDarReach( pNtk, nBddMax, nIterMax, fPartition, fReorder, fVerbose );
+    Abc_NtkDarReach( pNtk, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: reach [-BF num] [-prvh]\n" );
+    fprintf( pErr, "usage: reach [-BF num] [-provh]\n" );
     fprintf( pErr, "\t         verifies sequential miter using BDD-based reachability\n" );
     fprintf( pErr, "\t-B num : max number of nodes in the intermediate BDDs [default = %d]\n", nBddMax );
     fprintf( pErr, "\t-F num : max number of reachability iterations [default = %d]\n", nIterMax );
     fprintf( pErr, "\t-p     : enable partitioned image computation [default = %s]\n", fPartition? "yes": "no" );  
     fprintf( pErr, "\t-r     : enable dynamic BDD variable reordering [default = %s]\n", fReorder? "yes": "no" );  
+    fprintf( pErr, "\t-o     : toggles BDD variable reordering during image computation [default = %s]\n", fReorderImage? "yes": "no" );
     fprintf( pErr, "\t-v     : prints verbose information [default = %s]\n", fVerbose? "yes": "no" );  
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -9554,7 +9565,6 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk, * pNtkRes;
     int c;
-
     extern Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars );
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -9564,7 +9574,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Dch_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptgcfvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -9616,6 +9626,9 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'c':
             pPars->fUseCSat ^= 1;
             break;
+        case 'f':
+            pPars->fLightSynth ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -9646,7 +9659,7 @@ int Abc_CommandDch( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dch [-WCS num] [-sptgcvh]\n" );
+    fprintf( pErr, "usage: dch [-WCS num] [-sptgcfvh]\n" );
     fprintf( pErr, "\t         computes structural choices using a new approach\n" );
     fprintf( pErr, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
     fprintf( pErr, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
@@ -9656,6 +9669,7 @@ usage:
     fprintf( pErr, "\t-t     : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" );
     fprintf( pErr, "\t-g     : toggle using GIA to prove equivalences [default = %s]\n", pPars->fUseGia? "yes": "no" );
     fprintf( pErr, "\t-c     : toggle using circuit-based SAT vs. MiniSat [default = %s]\n", pPars->fUseCSat? "yes": "no" );
+    fprintf( pErr, "\t-f     : toggle using faster logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -16581,7 +16595,7 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     Fra_SecSetDefaultParams( pSecPar );
 //    pSecPar->TimeLimit = 300;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGDVBRarmfijwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "cbFCGDVBRarmfijkouwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -16686,6 +16700,15 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'j':
             pSecPar->fInterpolation ^= 1;
             break;
+        case 'k':
+            pSecPar->fInterSeparate ^= 1;
+            break;
+        case 'o':
+            pSecPar->fReorderImage ^= 1;
+            break;
+        case 'u':
+            pSecPar->fReadUnsolved ^= 1;
+            break;
         case 'w':
             pSecPar->fVeryVerbose ^= 1;
             break;
@@ -16712,12 +16735,21 @@ int Abc_CommandDProve( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_NtkDarProve( pNtk, pSecPar );
     pAbc->pCex = pNtk->pSeqModel; // temporary ???
 
-    // Fra_SmlWriteCounterExample( stdout, Aig_Man_t * pAig, Fra_Cex_t * p )
-
+    // read back the resulting unsolved reduced sequential miter
+    if ( pSecPar->fReadUnsolved && pSecPar->nSMnumber >= 0 )
+    {
+        char FileName[100];
+        sprintf( FileName, "sm%02d.aig", pSecPar->nSMnumber );
+        pNtk = Io_Read( FileName, Io_ReadFileType(FileName), 1 );
+        if ( pNtk == NULL )
+            printf( "Cannot read back unsolved reduced sequential miter \"%s\",\n", FileName );
+        else
+            Abc_FrameReplaceCurrentNetwork( pAbc, pNtk );
+    }
     return 0;
 
 usage:
-    fprintf( pErr, "usage: dprove [-FCGDVBR num] [-cbarmfijwvh]\n" );
+    fprintf( pErr, "usage: dprove [-FCGDVBR num] [-cbarmfijouwvh]\n" );
     fprintf( pErr, "\t         performs SEC on the sequential miter\n" );
     fprintf( pErr, "\t-F num : the limit on the depth of induction [default = %d]\n", pSecPar->nFramesMax );
     fprintf( pErr, "\t-C num : the conflict limit at a node during induction [default = %d]\n", pSecPar->nBTLimit );
@@ -16734,11 +16766,105 @@ usage:
     fprintf( pErr, "\t-f     : toggles the internal use of fraiging [default = %s]\n", pSecPar->fFraiging? "yes": "no" );
     fprintf( pErr, "\t-i     : toggles the use of induction [default = %s]\n", pSecPar->fInduction? "yes": "no" );
     fprintf( pErr, "\t-j     : toggles the use of interpolation [default = %s]\n", pSecPar->fInterpolation? "yes": "no" );
-//    fprintf( pErr, "\t-n     : toggles the use of different induction prover [default = %s]\n", pSecPar->fUseNewProver? "yes": "no" );
+    fprintf( pErr, "\t-k     : toggles applying interpolation to each output [default = %s]\n", pSecPar->fInterSeparate? "yes": "no" );
+    fprintf( pErr, "\t-o     : toggles using BDD variable reordering during image computation [default = %s]\n", pSecPar->fReorderImage? "yes": "no" );
+    fprintf( pErr, "\t-u     : toggles reading back unsolved reduced sequential miter [default = %s]\n", pSecPar->fReadUnsolved? "yes": "no" );
     fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", pSecPar->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w     : toggles additional verbose output [default = %s]\n", pSecPar->fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
+} 
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandDProve2( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk;
+    int nConfLast;
+    int fSeparate;
+    int fVeryVerbose;
+    int fVerbose;
+    int c;
+
+    extern int Abc_NtkDProve2( Abc_Ntk_t * pNtk, int nConfLast, int fSeparate, int fVeryVerbose, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    nConfLast    = 75000;
+    fSeparate    = 0;
+    fVeryVerbose = 0;
+    fVerbose     = 1;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Ckwvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nConfLast = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nConfLast < 0 ) 
+                goto usage;
+            break;
+        case 'k':
+            fSeparate ^= 1;
+            break;
+        case 'w':
+            fVeryVerbose ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        default:
+            goto usage;
+        }
+    }
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        printf( "This command works only for structrally hashed networks. Run \"st\".\n" );
+        return 0;
+    }
+    if ( Abc_NtkLatchNum(pNtk) == 0 )
+    {
+        printf( "This command works only for sequential networks.\n" );
+        return 0;
+    }
+    // perform verification
+    Abc_NtkDProve2( pNtk, nConfLast, fSeparate, fVeryVerbose, fVerbose );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: dprove2 [-C num] [-kwvh]\n" );
+    fprintf( pErr, "\t         improved integrated solver of sequential miters\n" );
+    fprintf( pErr, "\t-C num : the conflict limit during final BMC [default = %d]\n", nConfLast );
+    fprintf( pErr, "\t-k     : toggles solving each output separately [default = %s]\n", fSeparate? "yes": "no" );
+    fprintf( pErr, "\t-w     : toggles very verbose output [default = %s]\n", fVeryVerbose? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggles verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-h     : print the command usage\n");
+    return 1;
 }
 
 /**Function*************************************************************
@@ -18098,7 +18224,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Inter_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CNFrtpomcgbvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CNFrtpomcgbkvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -18159,6 +18285,9 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'b':
             pPars->fUseBackward ^= 1;
             break;
+        case 'k':
+            pPars->fUseSeparate ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -18174,7 +18303,7 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         return 1;
     }
     if ( !Abc_NtkIsStrash(pNtk) )
-    {
+    { 
         fprintf( stdout, "Currently only works for structurally hashed circuits.\n" );
         return 0;
     }
@@ -18185,10 +18314,29 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( Abc_NtkPoNum(pNtk) != 1 )
     {
-        fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" );
-        return 0;
+        if ( pPars->fUseSeparate )
+        {
+            printf( "Each of %d outputs will be solved separately.\n", Abc_NtkPoNum(pNtk) );
+            Abc_NtkDarBmcInter( pNtk, pPars );
+        }
+        else
+        {
+            Abc_Ntk_t * pNtkNew = Abc_NtkDup( pNtk );
+            printf( "All %d outputs will be ORed together.\n", Abc_NtkPoNum(pNtk) );
+            if ( !Abc_NtkCombinePos( pNtkNew, 0 ) )
+            {
+                Abc_NtkDelete( pNtkNew );
+                printf( "ORing outputs has failed.\n" ); 
+                return 0;
+            }
+            Abc_NtkDarBmcInter( pNtkNew, pPars );
+            Abc_NtkDelete( pNtkNew );
+        }
+    }
+    else
+    {
+        Abc_NtkDarBmcInter( pNtk, pPars );
     }
-    Abc_NtkDarBmcInter( pNtk, pPars );
     return 0;
 
 usage:
@@ -18205,6 +18353,7 @@ usage:
     fprintf( pErr, "\t-c     : toggle using inductive containment check [default = %s]\n", pPars->fCheckKstep? "yes": "no" );
     fprintf( pErr, "\t-g     : toggle using bias for global variables using SAT [default = %s]\n", pPars->fUseBias? "yes": "no" );
     fprintf( pErr, "\t-b     : toggle using backward interpolation [default = %s]\n", pPars->fUseBackward? "yes": "no" );
+    fprintf( pErr, "\t-k     : toggle solving each output separately [default = %s]\n", pPars->fUseSeparate? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
@@ -18585,7 +18734,7 @@ int Abc_CommandInduction( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 usage:
     fprintf( pErr, "usage: ind [-FC num] [-vh]\n" );
-    fprintf( pErr, "\t         runs K-step induction for the property output\n" );
+    fprintf( pErr, "\t         runs the inductive case of the K-step induction\n" );
     fprintf( pErr, "\t-F num : the max number of timeframes [default = %d]\n", nFramesMax );
     fprintf( pErr, "\t-C num : the max number of conflicts by SAT solver [default = %d]\n", nConfMax );
     fprintf( pErr, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
@@ -19959,7 +20108,7 @@ int Abc_CommandAbc8Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Dch_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WCSsptfvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -20005,6 +20154,9 @@ int Abc_CommandAbc8Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 't':
             pPars->fSimulateTfo ^= 1;
             break;
+        case 'f':
+            pPars->fLightSynth ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -20027,12 +20179,12 @@ int Abc_CommandAbc8Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc8Dch(): Tranformation of the AIG has failed.\n" );
         return 1;
     }
-    Aig_ManStop( pAbc->pAbc8Aig );
+//    Aig_ManStop( pAbc->pAbc8Aig );
     pAbc->pAbc8Aig = pAigNew;
     return 0;
 
 usage:
-    fprintf( stdout, "usage: *dch [-WCS num] [-sptvh]\n" );
+    fprintf( stdout, "usage: *dch [-WCS num] [-sptfvh]\n" );
     fprintf( stdout, "\t         computes structural choices using a new approach\n" );
     fprintf( stdout, "\t-W num : the max number of simulation words [default = %d]\n", pPars->nWords );
     fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
@@ -20040,6 +20192,7 @@ usage:
     fprintf( stdout, "\t-s     : toggle synthesizing three snapshots [default = %s]\n", pPars->fSynthesis? "yes": "no" );
     fprintf( stdout, "\t-p     : toggle power-aware rewriting [default = %s]\n", pPars->fPower? "yes": "no" );
     fprintf( stdout, "\t-t     : toggle simulation of the TFO classes [default = %s]\n", pPars->fSimulateTfo? "yes": "no" );
+    fprintf( stdout, "\t-f     : toggle using lighter logic synthesis [default = %s]\n", pPars->fLightSynth? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
@@ -20973,7 +21126,7 @@ int Abc_CommandAbc8Scl( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
     {
-        fprintf( stdout, "Abc_CommandAbc8Scl(): The network is combinational (run \"*fraig\").\n" );
+        fprintf( stdout, "Abc_CommandAbc8Scl(): The network is combinational.\n" );
         return 0;
     }
 
@@ -21092,7 +21245,7 @@ int Abc_CommandAbc8Lcorr( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
     {
-        fprintf( stdout, "Abc_CommandAbc8Lcorr(): The network is combinational (run \"*fraig\").\n" );
+        fprintf( stdout, "Abc_CommandAbc8Lcorr(): The network is combinational.\n" );
         return 0;
     }
 
@@ -21285,7 +21438,7 @@ int Abc_CommandAbc8Ssw( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
     {
-        fprintf( stdout, "The network is combinational (run \"*fraig\").\n" );
+        fprintf( stdout, "The network is combinational.\n" );
         return 0;
     }
 
@@ -21518,7 +21671,7 @@ int Abc_CommandAbc8Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     if ( Ntl_ManIsComb(pAbc->pAbc8Ntl) )
     {
-        fprintf( stdout, "The network is combinational (run \"*fraig\").\n" );
+        fprintf( stdout, "The network is combinational.\n" );
         return 0;
     }
 
@@ -23890,7 +24043,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fCSat = 0;
     Cec_ManSatSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CSNnmfcvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CSNnmftcvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -23936,6 +24089,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'f':
             pPars->fFirstStop ^= 1;
             break;
+        case 't':
+            pPars->fLearnCls ^= 1;
+            break;
         case 'c':
             fCSat ^= 1;
             break;
@@ -23955,7 +24111,9 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
     {
         Vec_Int_t * vCounters;
         Vec_Str_t * vStatus;
-        if ( pPars->fNonChrono )
+        if ( pPars->fLearnCls )
+            vCounters = Tas_ManSolveMiterNc( pAbc->pAig, pPars->nBTLimit, &vStatus, pPars->fVerbose );
+        else if ( pPars->fNonChrono )
             vCounters = Cbs_ManSolveMiterNc( pAbc->pAig, pPars->nBTLimit, &vStatus, pPars->fVerbose );
         else
             vCounters = Cbs_ManSolveMiter( pAbc->pAig, pPars->nBTLimit, &vStatus, pPars->fVerbose );
@@ -23970,7 +24128,7 @@ int Abc_CommandAbc9Sat( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &sat [-CSN <num>] [-nmfcvh]\n" );
+    fprintf( stdout, "usage: &sat [-CSN <num>] [-nmfctvh]\n" );
     fprintf( stdout, "\t         performs SAT solving for the combinational outputs\n" );
     fprintf( stdout, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     fprintf( stdout, "\t-S num : the min number of variables to recycle the solver [default = %d]\n", pPars->nSatVarMax );
@@ -23979,6 +24137,7 @@ usage:
     fprintf( stdout, "\t-m     : toggle miter vs. any circuit [default = %s]\n", pPars->fCheckMiter? "yes": "no" );
     fprintf( stdout, "\t-f     : toggle quitting when one PO is asserted [default = %s]\n", pPars->fFirstStop? "yes": "no" );
     fprintf( stdout, "\t-c     : toggle using circuit-based SAT solver [default = %s]\n", fCSat? "yes": "no" );
+    fprintf( stdout, "\t-t     : toggle using learning in curcuit-based solver [default = %s]\n", pPars->fLearnCls? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
@@ -24139,18 +24298,23 @@ usage:
 ***********************************************************************/
 int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    char * pFileName = "gsrm.aig";
-    Gia_Man_t * pTemp;
+    char * pFileName  = "gsrm.aig";
+    char * pFileName2 = "gsyn.aig";
+    Gia_Man_t * pTemp, * pAux;
     int c, fVerbose = 0;
+    int fSynthesis = 0;
     int fDualOut = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "dvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "dsvh" ) ) != EOF )
     {
         switch ( c )
         {
         case 'd':
             fDualOut ^= 1;
             break;
+        case 's':
+            fSynthesis ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -24165,22 +24329,38 @@ int Abc_CommandAbc9Srm( Abc_Frame_t * pAbc, int argc, char ** argv )
         printf( "Abc_CommandAbc9Srm(): There is no AIG.\n" );
         return 1;
     } 
-//    pAbc->pAig = Gia_ManSpecReduce( pTemp = pAbc->pAig, fDualOut );
-//    Gia_ManStop( pTemp );
     pTemp = Gia_ManSpecReduce( pAbc->pAig, fDualOut, fVerbose );
     if ( pTemp )
     {
+        pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
+        Gia_ManStop( pAux );
+
         Gia_WriteAiger( pTemp, pFileName, 0, 0 );
         printf( "Speculatively reduced model was written into file \"%s\".\n", pFileName );
         Gia_ManPrintStatsShort( pTemp );
         Gia_ManStop( pTemp );
     }
+    if ( fSynthesis )
+    {
+        pTemp = Gia_ManEquivReduce( pAbc->pAig, 1, fDualOut, fVerbose );
+        if ( pTemp )
+        {
+            pTemp = Gia_ManSeqStructSweep( pAux = pTemp, 1, 1, 0 );
+            Gia_ManStop( pAux );
+
+            Gia_WriteAiger( pTemp, pFileName2, 0, 0 );
+            printf( "Reduced original network was written into file \"%s\".\n", pFileName2 );
+            Gia_ManPrintStatsShort( pTemp );
+            Gia_ManStop( pTemp );
+        }
+    }
     return 0;
 
 usage:
-    fprintf( stdout, "usage: &srm [-dvh]\n" );
+    fprintf( stdout, "usage: &srm [-dsvh]\n" );
     fprintf( stdout, "\t         writes speculatively reduced model into file \"%s\"\n", pFileName );
     fprintf( stdout, "\t-d     : toggle creating dual output miter [default = %s]\n", fDualOut? "yes": "no" );
+    fprintf( stdout, "\t-s     : toggle writing reduced network for synthesis [default = %s]\n", fSynthesis? "yes": "no" );
     fprintf( stdout, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     fprintf( stdout, "\t-h     : print the command usage\n");
     return 1;
@@ -24765,7 +24945,7 @@ int Abc_CommandAbc9Era( Abc_Frame_t * pAbc, int argc, char ** argv )
     Gia_Man_t * pTemp = NULL;
     int c, fVerbose = 0;
     int fMiter = 0;
-    int nStatesMax = 1000000;
+    int nStatesMax = 10000000;
     extern void Gia_ManCollectReachable( Gia_Man_t * pAig, int nStatesMax, int fMiter, int fVerbose );
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "Smvh" ) ) != EOF )
@@ -24834,6 +25014,75 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9Dch( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+//    extern void Hcd_ComputeChoicesTest( Gia_Man_t * pAig, int nBTLimit, int fSynthesis, int fUseMiniSat, int fVerbose );
+    Gia_Man_t * pTemp = NULL;
+    int nBTLimit = 100;
+    int fSynthesis = 1;
+    int fUseMiniSat = 0;
+    int c, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "Csmvh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( stdout, "Command line switch \"-C\" should be followed by a positive integer.\n" );
+                goto usage;
+            }
+            nBTLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nBTLimit < 0 ) 
+                goto usage;
+            break;
+        case 's':
+            fSynthesis ^= 1;
+            break;
+        case 'm':
+            fUseMiniSat ^= 1;
+            break;
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pAig == NULL )
+    {
+        printf( "Abc_CommandAbc9Test(): There is no AIG.\n" );
+        return 1;
+    } 
+//    Hcd_ComputeChoicesTest( pAbc->pAig, nBTLimit, fSynthesis, fUseMiniSat, fVerbose );
+    return 0;
+
+usage:
+    fprintf( stdout, "usage: &dch [-C num] [-smvh]\n" );
+    fprintf( stdout, "\t          computing choices using the latest algorithm\n" );
+    fprintf( stdout, "\t-C num  : the max number of states to traverse (num > 0) [default = %d]\n", nBTLimit );
+    fprintf( stdout, "\t-s      : toggle printing verbose information [default = %s]\n", fSynthesis? "yes": "no" );
+    fprintf( stdout, "\t-m      : toggle using MiniSat as a SAT solver [default = %s]\n", fUseMiniSat? "yes": "no" );
+    fprintf( stdout, "\t-v      : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( stdout, "\t-h      : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Gia_Man_t * pTemp = NULL;
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 873b78d1..1220cb40 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -895,45 +895,37 @@ Abc_Ntk_t * Abc_NtkDChoice( Abc_Ntk_t * pNtk, int fBalance, int fUpdateLevel, in
 ***********************************************************************/
 Abc_Ntk_t * Abc_NtkDch( Abc_Ntk_t * pNtk, Dch_Pars_t * pPars )
 {
-    extern Vec_Ptr_t * Dar_ManChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose );
-    extern Aig_Man_t * Cec_ComputeChoices( Vec_Ptr_t * vAigs, Dch_Pars_t * pPars );
+    extern Gia_Man_t * Dar_NewChoiceSynthesis( Aig_Man_t * pAig, int fBalance, int fUpdateLevel, int fPower, int fVerbose );
+    extern Aig_Man_t * Cec_ComputeChoices( Gia_Man_t * pGia, Dch_Pars_t * pPars );
 
-    Vec_Ptr_t * vAigs;
     Aig_Man_t * pMan, * pTemp;
     Abc_Ntk_t * pNtkAig;
-    int i, clk;
+    Gia_Man_t * pGia;
+    int clk;
     assert( Abc_NtkIsStrash(pNtk) );
     pMan = Abc_NtkToDar( pNtk, 0, 0 );
     if ( pMan == NULL )
         return NULL;
 clk = clock();
     if ( pPars->fSynthesis )
-    {
-//        vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, pPars->fVerbose );
-        vAigs = Dar_ManChoiceSynthesis( pMan, 1, 1, pPars->fPower, 0 );
-        Aig_ManStop( pMan );
-        // swap around the first and the last
-        pTemp = Vec_PtrPop( vAigs );
-        Vec_PtrPush( vAigs, Vec_PtrEntry(vAigs,0) );
-        Vec_PtrWriteEntry( vAigs, 0, pTemp );
-    }
+        pGia = Dar_NewChoiceSynthesis( pMan, 1, 1, pPars->fPower, 0 );
     else
     {
-        vAigs = Vec_PtrAlloc( 1 );
-        Vec_PtrPush( vAigs, pMan );
+        pGia = Gia_ManFromAig( pMan );
+        Aig_ManStop( pMan );
     }
 pPars->timeSynth = clock() - clk;
     if ( pPars->fUseGia )
-        pMan = Cec_ComputeChoices( vAigs, pPars );
+        pMan = Cec_ComputeChoices( pGia, pPars );
     else
-        pMan = Dch_ComputeChoices( vAigs, pPars );
+    {
+        pMan = Gia_ManToAigSkip( pGia, 3 );
+        Gia_ManStop( pGia );
+        pMan = Dch_ComputeChoices( pTemp = pMan, pPars );
+        Aig_ManStop( pTemp );
+    }
     pNtkAig = Abc_NtkFromDarChoices( pNtk, pMan );
-//    pNtkAig = Abc_NtkFromDar( pNtk, pMan );
     Aig_ManStop( pMan );
-    // cleanup
-    Vec_PtrForEachEntry( vAigs, pTemp, i )
-        Aig_ManStop( pTemp );
-    Vec_PtrFree( vAigs );
     return pNtkAig;
 }
 
@@ -1535,6 +1527,18 @@ Abc_Ntk_t * Abc_NtkDarLcorrNew( Abc_Ntk_t * pNtk, int nVarsMax, int nConfMax, in
     return pNtkAig;
 }
 
+/*
+#include <signal.h>
+#include "utilMem.h"
+static void sigfunc( int signo ) 
+{
+    if (signo == SIGINT) {
+        printf("SIGINT received!\n");
+        s_fInterrupt = 1;
+    }
+}
+*/
+
 /**Function*************************************************************
 
   Synopsis    [Gives the current ABC network to AIG manager for processing.]
@@ -1550,6 +1554,19 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta,
 {
     Aig_Man_t * pMan;
     int status, RetValue = -1, clk = clock();
+
+/*
+    s_fInterrupt = 0;
+    if ( signal(SIGINT,sigfunc) == SIG_ERR ) 
+    {
+        printf("Could not setup signal handler for SIGINT!\n");
+        return RetValue;
+    }
+    printf("Waiting for SIGINT. Press Ctrl+C to exit.\n");
+//    while ( !s_fInterrupt );
+//    return RetValue;
+*/
+
     // derive the AIG manager
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
@@ -1572,8 +1589,12 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nFrames, int nSizeMax, int nNodeDelta,
             printf( "No output was asserted in %d frames. Reached conflict limit (%d). ", iFrame, nBTLimit );
         else // if ( RetValue == 0 )
         {
+            extern void Aig_ManCounterExampleValueTest( Aig_Man_t * pAig, Fra_Cex_t * pCex );
+
             Fra_Cex_t * pCex = pNtk->pSeqModel;
             printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", pCex->iPo, pCex->iFrame );
+
+            Aig_ManCounterExampleValueTest( pMan, pCex );
         }
     }
     else
@@ -1639,33 +1660,105 @@ ABC_PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars )
+int Abc_NtkDarBmcInter_int( Aig_Man_t * pMan, Inter_ManParams_t * pPars )
 {
-    Aig_Man_t * pMan;
     int RetValue, iFrame, clk = clock();
-    // derive the AIG manager
-    pMan = Abc_NtkToDar( pNtk, 0, 1 );
-    if ( pMan == NULL )
+    assert( pMan->nRegs > 0 );
+    if ( pPars->fUseSeparate )
     {
-        printf( "Converting miter into AIG has failed.\n" );
-        return -1;
+        Aig_Man_t * pTemp, * pAux;
+        Aig_Obj_t * pObjPo;
+        int i, Counter = 0;
+        Saig_ManForEachPo( pMan, pObjPo, i )
+        {
+            if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pMan) )
+                continue;
+            pTemp = Aig_ManDupOneOutput( pMan, i, 1 );
+            pTemp = Aig_ManScl( pAux = pTemp, 1, 1, 0 );
+            Aig_ManStop( pAux );
+            if ( Aig_ObjFanin0(pObjPo) == Aig_ManConst1(pMan) )
+            {
+                Aig_ManStop( pTemp );
+                continue;
+            }
+            RetValue = Inter_ManPerformInterpolation( pTemp, pPars, &iFrame );
+            if ( pTemp->pSeqModel )
+            {
+                Ssw_Cex_t * pCex;
+                pCex = pMan->pSeqModel = pTemp->pSeqModel; pTemp->pSeqModel = NULL;
+                pCex->iPo = i;
+                Aig_ManStop( pTemp );
+                break;
+            }
+            // if solved, remove the output
+            if ( RetValue == 1 )
+            {
+                Aig_ObjPatchFanin0( pMan, pObjPo, Aig_ManConst0(pMan) );
+//                    printf( "Output %3d : Solved ", i );
+            }
+            else
+            {
+                Counter++;
+//                    printf( "Output %3d : Undec  ", i );
+            }
+//                Aig_ManPrintStats( pTemp );
+            Aig_ManStop( pTemp );
+            printf( "Solving output %3d (out of %3d) using interpolation.\r", i, Saig_ManPoNum(pMan) );
+        }
+        Aig_ManCleanup( pMan );
+        if ( pMan->pSeqModel == NULL )
+        {
+            printf( "Interpolation left %d (out of %d) outputs unsolved              \n", Counter, Saig_ManPoNum(pMan) );
+            if ( Counter )
+                RetValue = -1;
+        }
+/*
+        pMan = Aig_ManDupUnsolvedOutputs( pTemp = pMan, 1 );
+        Aig_ManStop( pTemp );
+        pMan = Aig_ManScl( pTemp = pMan, 1, 1, 0 );
+        Aig_ManStop( pTemp );
+*/
+    }
+    else
+    {    
+        RetValue = Inter_ManPerformInterpolation( pMan, pPars, &iFrame );
     }
-    assert( pMan->nRegs > 0 );
-    RetValue = Inter_ManPerformInterpolation( pMan, pPars, &iFrame );
     if ( RetValue == 1 )
         printf( "Property proved.  " );
     else if ( RetValue == 0 )
-    {
         printf( "Property DISPROVED in frame %d (use \"write_counter\" to dump a witness).  ", iFrame );
-        ABC_FREE( pNtk->pModel );
-        ABC_FREE( pNtk->pSeqModel );
-        pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
-    }
     else if ( RetValue == -1 )
         printf( "Property UNDECIDED.  " );
     else
         assert( 0 );
 ABC_PRT( "Time", clock() - clk );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Gives the current ABC network to AIG manager for processing.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars )
+{
+    Aig_Man_t * pMan;
+    pMan = Abc_NtkToDar( pNtk, 0, 1 );
+    if ( pMan == NULL )
+    {
+        printf( "Converting miter into AIG has failed.\n" );
+        return -1;
+    }
+    Abc_NtkDarBmcInter_int( pMan, pPars );
+    ABC_FREE( pNtk->pModel );
+    ABC_FREE( pNtk->pSeqModel );
+    pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
     Aig_ManStop( pMan );
     return 1;
 }
@@ -2411,7 +2504,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
         else
         {
             RetValue = 0;
-            printf( "Simulation of %d frames with %d words did not assert the outputs. ", 
+            printf( "Simulation of %d frames with %d words did not assert the outputs.    ", 
                 nFrames, nWords );
         }
         Gia_ManStop( pGia );
@@ -2439,7 +2532,7 @@ int Abc_NtkDarSeqSim( Abc_Ntk_t * pNtk, int nFrames, int nWords, int TimeOut, in
         else
         {
             RetValue = 0;
-            printf( "Simulation of %d frames with %d words did not assert the outputs. ", 
+            printf( "Simulation of %d frames with %d words did not assert the outputs.    ", 
                 nFrames, nWords );
         }
         Fra_SmlStop( pSml );
@@ -3187,14 +3280,14 @@ Abc_Ntk_t * Abc_NtkDarCleanupAig( Abc_Ntk_t * pNtk, int fCleanupPis, int fCleanu
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose )
+void Abc_NtkDarReach( Abc_Ntk_t * pNtk, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose )
 {
-    extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fVerbose, int fSilent );
+    extern int Aig_ManVerifyUsingBdds( Aig_Man_t * p, int nBddMax, int nIterMax, int fPartition, int fReorder, int fReorderImage, int fVerbose, int fSilent );
     Aig_Man_t * pMan;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
         return;
-    Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fVerbose, 0 );
+    Aig_ManVerifyUsingBdds( pMan, nBddMax, nIterMax, fPartition, fReorder, fReorderImage, fVerbose, 0 );
     ABC_FREE( pNtk->pModel );
     ABC_FREE( pNtk->pSeqModel );
     pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
diff --git a/src/base/abci/abcTiming.c b/src/base/abci/abcTiming.c
index 36e56e7b..95c7103a 100644
--- a/src/base/abci/abcTiming.c
+++ b/src/base/abci/abcTiming.c
@@ -157,7 +157,7 @@ void Abc_NtkTimeSetDefaultRequired( Abc_Ntk_t * pNtk, float Rise, float Fall )
     if ( pNtk->pManTime == NULL )
         pNtk->pManTime = Abc_ManTimeStart();
     pNtk->pManTime->tReqDef.Rise  = Rise;
-    pNtk->pManTime->tReqDef.Rise  = Fall;
+    pNtk->pManTime->tReqDef.Fall  = Fall;
     pNtk->pManTime->tReqDef.Worst = ABC_MAX( Rise, Fall );
 }
 
@@ -185,7 +185,7 @@ void Abc_NtkTimeSetArrival( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall
     vTimes = pNtk->pManTime->vArrs;
     pTime = vTimes->pArray[ObjId];
     pTime->Rise  = Rise;
-    pTime->Fall  = Rise;
+    pTime->Fall  = Fall;
     pTime->Worst = ABC_MAX( Rise, Fall );
 }
 
@@ -213,7 +213,7 @@ void Abc_NtkTimeSetRequired( Abc_Ntk_t * pNtk, int ObjId, float Rise, float Fall
     vTimes = pNtk->pManTime->vReqs;
     pTime = vTimes->pArray[ObjId];
     pTime->Rise  = Rise;
-    pTime->Fall  = Rise;
+    pTime->Fall  = Fall;
     pTime->Worst = ABC_MAX( Rise, Fall );
 }
 
diff --git a/src/base/abci/module.make b/src/base/abci/module.make
index 9214bb52..aaea7312 100644
--- a/src/base/abci/module.make
+++ b/src/base/abci/module.make
@@ -12,6 +12,7 @@ SRC +=    src/base/abci/abc.c \
     src/base/abci/abcDar.c \
     src/base/abci/abcDebug.c \
     src/base/abci/abcDelay.c \
+    src/base/abci/abcDprove2.c \
     src/base/abci/abcDress.c \
     src/base/abci/abcDsd.c \
     src/base/abci/abcExtract.c \
diff --git a/src/base/io/ioWriteBlif.c b/src/base/io/ioWriteBlif.c
index dae8b783..d1adaf90 100644
--- a/src/base/io/ioWriteBlif.c
+++ b/src/base/io/ioWriteBlif.c
@@ -579,7 +579,8 @@ void Io_WriteTimingInfo( FILE * pFile, Abc_Ntk_t * pNtk )
         pTime = Abc_NodeReadArrival(pNode);
         if ( pTime->Rise == pTimeDef->Rise && pTime->Fall == pTimeDef->Fall )
             continue;
-        fprintf( pFile, ".input_arrival %s %g %g\n", Abc_ObjName(pNode), pTime->Rise, pTime->Fall );
+//        fprintf( pFile, ".input_arrival %s %g %g\n", Abc_ObjName(pNode), pTime->Rise, pTime->Fall );
+        fprintf( pFile, ".input_arrival %s %g %g\n", Abc_ObjName(Abc_ObjFanout0(pNode)), pTime->Rise, pTime->Fall );
     }
 }
 
diff --git a/src/base/main/main.c b/src/base/main/main.c
index 738f217c..f74fb21a 100644
--- a/src/base/main/main.c
+++ b/src/base/main/main.c
@@ -23,10 +23,12 @@
 // this line should be included in the library project
 //#define ABC_LIB
 
+//#define ABC_USE_BINARY 1
+
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
-
+ 
 static int TypeCheck( Abc_Frame_t * pAbc, char * s);
 
 ////////////////////////////////////////////////////////////////////////
@@ -46,7 +48,11 @@ static int TypeCheck( Abc_Frame_t * pAbc, char * s);
   SeeAlso     []
 
 ***********************************************************************/
+#if defined(ABC_USE_BINARY)
+int main_( int argc, char * argv[] )
+#else
 int main( int argc, char * argv[] )
+#endif
 {
     Abc_Frame_t * pAbc;
     char sCommandUsr[500], sCommandTmp[100], sReadCmd[20], sWriteCmd[20], c;
@@ -67,7 +73,7 @@ int main( int argc, char * argv[] )
     pAbc = Abc_FrameGetGlobalFrame();
 
     // default options
-    fBatch = 0;
+    fBatch      = 0;
     fInitSource = 1;
     fInitRead   = 0;
     fFinalWrite = 0;
@@ -313,127 +319,6 @@ static int TypeCheck( Abc_Frame_t * pAbc, char * s )
 
 
 
-/**Function*************************************************************
-
-  Synopsis    [Find the file name.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-char * Abc_MainFileName( char * pFileName )
-{
-    static char Buffer[200];
-    char * pExtension;
-    assert( strlen(pFileName) < 190 );
-    pExtension = Extra_FileNameExtension( pFileName );
-    if ( pExtension == NULL )
-        sprintf( Buffer, "%s.opt", pFileName );
-    else
-    {
-        strncpy( Buffer, pFileName, pExtension-pFileName-1 );
-        sprintf( Buffer+(pExtension-pFileName-1), ".opt.%s", pExtension );
-    }
-    return Buffer;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [The main() procedure.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int main_( int argc, char * argv[] )
-{
-    extern void Nwk_ManPrintStatsUpdate( void * p, void * pAig, void * pNtk,
-         int nRegInit, int nLutInit, int nLevInit, int Time );
-    char * pComs[20] = 
-    {
-/*00*/  "*r -am ",
-/*01*/  "*w -abc 1.aig",
-/*02*/  "*lcorr -nc",//; *ps",
-/*03*/  "*scorr -nc",//; *ps",
-/*04*/  "*dch; *if -K 4 -C 16 -F 3 -A 2; *sw -m",//; *ps",
-/*05*/  "*dch; *if -K 4 -C 16 -F 3 -A 2; *sw -m",//; *ps", 
-/*06*/  "*w ",
-/*07*/  "*w -abc 2.aig",
-/*08*/  "miter -mc 1.aig 2.aig; sim -F 4 -W 4 -mv"
-    };
-    char Command[1000];
-    int i, nComs;
-    Abc_Frame_t * pAbc;
-    FILE * pFile;
-    int nRegInit, nLutInit, nLevInit;
-    int clkStart = clock();
-
-    // added to detect memory leaks:
-#if defined(_DEBUG) && defined(_MSC_VER) 
-    _CrtSetDbgFlag( _CRTDBG_ALLOC_MEM_DF | _CRTDBG_LEAK_CHECK_DF );
-#endif
-
-    // check that the file is present
-    if ( argc != 2 )
-    {
-        printf( "Expecting one command argument (file name).\n" );
-        return 0;
-    }
-    pFile = fopen( argv[1], "r" );
-    if ( pFile == NULL )
-    {
-        printf( "Cannot open file \"%s\".\n", argv[1] );
-        return 0;
-    }
-    fclose( pFile );
-
-    // count the number of commands
-    for ( nComs = 0; nComs < 20; nComs++ )
-        if ( pComs[nComs] == NULL )
-            break;
-    // perform the commands
-    printf( "Reading design \"%s\"...\n", argv[1] );
-    pAbc = Abc_FrameGetGlobalFrame();
-    for ( i = 0; i < nComs; i++ )
-    {
-
-        if ( i == 0 )
-            sprintf( Command, "%s%s", pComs[i], argv[1] );
-        else if ( i == 6 )
-            sprintf( Command, "%s%s", pComs[i], Abc_MainFileName(argv[1]) );
-        else 
-            sprintf( Command, "%s", pComs[i] );
-        if ( Cmd_CommandExecute( pAbc, Command ) )
-        {
-            printf( "Internal command %d failed.\n", i );
-            return 0;
-        }
-        if ( i == 0 )
-        {
-            extern int Nwk_ManStatsRegs( void * p );
-            extern int Nwk_ManStatsLuts( void * pNtk );
-            extern int Nwk_ManStatsLevs( void * pNtk );
-            nRegInit = Nwk_ManStatsRegs( pAbc->pAbc8Ntl );
-            nLutInit = Nwk_ManStatsLuts( pAbc->pAbc8Nwk );
-            nLevInit = Nwk_ManStatsLevs( pAbc->pAbc8Nwk );
-        }
-        if ( i >= 1 && i <= 5 )
-        Nwk_ManPrintStatsUpdate( pAbc->pAbc8Ntl, pAbc->pAbc8Aig, pAbc->pAbc8Nwk, 
-            nRegInit, nLutInit, nLevInit, clkStart );
-    }
-    Abc_Stop(); 
-    printf( "Writing optimized design \"%s\"...\n", Abc_MainFileName(argv[1]) );
-    ABC_PRT( "Total time", clock() - clkStart );
-    printf( "\n" );
-    return 0;  
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/main/mainFrame.c b/src/base/main/mainFrame.c
index 31e0afa9..81070bd8 100644
--- a/src/base/main/mainFrame.c
+++ b/src/base/main/mainFrame.c
@@ -28,6 +28,9 @@
 
 static Abc_Frame_t * s_GlobalFrame = NULL;
 
+extern void * Aig_ManDupSimple( void * p );
+extern void Aig_ManStop( void * pAig );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -148,11 +151,16 @@ void Abc_FrameDeallocate( Abc_Frame_t * p )
     if ( p->pManDec ) Dec_ManStop( p->pManDec );
     if ( p->dd )      Extra_StopManager( p->dd );
     if ( p->vStore )  Vec_PtrFree( p->vStore );
+    if ( p->pSave1 )  Aig_ManStop( p->pSave1 );
+    if ( p->pSave2 )  Aig_ManStop( p->pSave2 );
+    if ( p->pSave3 )  Aig_ManStop( p->pSave3 );
+    if ( p->pSave4 )  Aig_ManStop( p->pSave4 );
     Abc_FrameDeleteAllNetworks( p );
     ABC_FREE( p );
     s_GlobalFrame = NULL;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -513,6 +521,58 @@ Abc_Frame_t * Abc_FrameReadGlobalFrame()
     return s_GlobalFrame;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FrameSetSave1( void * pAig )
+{
+    Abc_Frame_t * pFrame = Abc_FrameGetGlobalFrame();
+    if ( pFrame->pSave1 )
+        Aig_ManStop( pFrame->pSave1 );
+    pFrame->pSave1 = pAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Abc_FrameSetSave2( void * pAig )
+{
+    Abc_Frame_t * pFrame = Abc_FrameGetGlobalFrame();
+    if ( pFrame->pSave2 )
+        Aig_ManStop( pFrame->pSave2 );
+    pFrame->pSave2 = pAig;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Abc_FrameReadSave1()  { void * pAig = Abc_FrameGetGlobalFrame()->pSave1; Abc_FrameGetGlobalFrame()->pSave1 = NULL; return pAig; }
+void * Abc_FrameReadSave2()  { void * pAig = Abc_FrameGetGlobalFrame()->pSave2; Abc_FrameGetGlobalFrame()->pSave2 = NULL; return pAig; }
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/main/mainInt.h b/src/base/main/mainInt.h
index ca8717be..01bf5eb2 100644
--- a/src/base/main/mainInt.h
+++ b/src/base/main/mainInt.h
@@ -82,6 +82,11 @@ struct Abc_Frame_t_
     void *          pAig;
     void *          pCex; 
 
+    void *          pSave1; 
+    void *          pSave2; 
+    void *          pSave3; 
+    void *          pSave4; 
+
     // the addition to keep the best Ntl that can be used to restore
     void *            pAbc8NtlBestDelay;    // the best delay, Ntl
     void *            pAbc8NtlBestArea;    // the best area
diff --git a/src/map/amap/amapRule.c b/src/map/amap/amapRule.c
index 212f7631..27de49ee 100644
--- a/src/map/amap/amapRule.c
+++ b/src/map/amap/amapRule.c
@@ -296,7 +296,7 @@ Kit_DsdPrint( stdout, pNtk );
         {
             assert( iNod > 1 );
             pNod = Amap_LibNod( pLib, Amap_Lit2Var(iNod) );
-            assert( pNod->Type == AMAP_OBJ_MUX || pNod->nSuppSize == pGate->nPins );
+//            assert( pNod->Type == AMAP_OBJ_MUX || pNod->nSuppSize == pGate->nPins );
             pSet = (Amap_Set_t *)Aig_MmFlexEntryFetch( pLib->pMemSet, sizeof(Amap_Set_t) );
             memset( pSet, 0, sizeof(Amap_Set_t) );
             pSet->iGate = pGate->Id;
diff --git a/src/map/if/ifMap.c b/src/map/if/ifMap.c
index fd1078a6..ca57868d 100644
--- a/src/map/if/ifMap.c
+++ b/src/map/if/ifMap.c
@@ -207,7 +207,9 @@ void If_ObjPerformMappingChoice( If_Man_t * p, If_Obj_t * pObj, int Mode, int fP
     for ( pTemp = pObj->pEquiv; pTemp; pTemp = pTemp->pEquiv )
     {
         assert( pTemp->nRefs == 0 );
-        assert( p->pPars->fSeqMap || pTemp->pCutSet->nCuts > 0 );
+//        assert( p->pPars->fSeqMap || pTemp->pCutSet->nCuts > 0 ); // June 9, 2009
+        if ( pTemp->pCutSet->nCuts == 0 )
+            continue;
         // go through the cuts of this node
         If_ObjForEachCut( pTemp, pCutTemp, i )
         {
diff --git a/src/map/mapper/mapperLib.c b/src/map/mapper/mapperLib.c
index 942caa8e..cc64d8b8 100644
--- a/src/map/mapper/mapperLib.c
+++ b/src/map/mapper/mapperLib.c
@@ -174,15 +174,20 @@ int Map_SuperLibDeriveFromGenlib( Mio_Library_t * pLib )
 {
     Abc_Frame_t * pAbc = Abc_FrameGetGlobalFrame();
     char * pNameGeneric;
-    char FileNameGenlib[100];
-    char FileNameSuper[100];
-    char CommandSuper[500];
-    char CommandRead[500];
+    char * FileNameGenlib;
+    char * FileNameSuper;
+    char * CommandSuper;
+    char * CommandRead;
     FILE * pFile;
 
     if ( pLib == NULL )
         return 0;
 
+    FileNameGenlib = ABC_ALLOC( char, 10000 );
+    FileNameSuper = ABC_ALLOC( char, 10000 );
+    CommandSuper = ABC_ALLOC( char, 10000 );
+    CommandRead = ABC_ALLOC( char, 10000 );
+
     // write the current library into the file
     sprintf( FileNameGenlib, "%s_temp", Mio_LibraryReadName(pLib) );
     pFile = fopen( FileNameGenlib, "w" );
@@ -197,6 +202,10 @@ int Map_SuperLibDeriveFromGenlib( Mio_Library_t * pLib )
     sprintf( CommandSuper,  "super -l 1 -i 5 -d 10000000 -a 10000000 -t 100 %s", FileNameGenlib ); 
     if ( Cmd_CommandExecute( pAbc, CommandSuper ) )
     {
+        ABC_FREE( FileNameGenlib );
+        ABC_FREE( FileNameSuper );
+        ABC_FREE( CommandSuper );
+        ABC_FREE( CommandRead );
         fprintf( stdout, "Cannot execute command \"%s\".\n", CommandSuper );
         return 0;
     }
@@ -215,6 +224,10 @@ int Map_SuperLibDeriveFromGenlib( Mio_Library_t * pLib )
         unlink( FileNameSuper );
 #endif
         fprintf( stdout, "Cannot execute command \"%s\".\n", CommandRead );
+        ABC_FREE( FileNameGenlib );
+        ABC_FREE( FileNameSuper );
+        ABC_FREE( CommandSuper );
+        ABC_FREE( CommandRead );
         return 0;
     }
 
@@ -225,6 +238,10 @@ int Map_SuperLibDeriveFromGenlib( Mio_Library_t * pLib )
     unlink( FileNameSuper );
 #endif
 */
+    ABC_FREE( FileNameGenlib );
+    ABC_FREE( FileNameSuper );
+    ABC_FREE( CommandSuper );
+    ABC_FREE( CommandRead );
      return 1;
 }
 
diff --git a/src/map/super/superGate.c b/src/map/super/superGate.c
index 7bc5e703..cb7d8d78 100644
--- a/src/map/super/superGate.c
+++ b/src/map/super/superGate.c
@@ -67,8 +67,8 @@ struct Super_ManStruct_t_
     int                 Time;         // the runtime of the generation procedure
     int                 TimeLimit;    // the runtime limit (in seconds)
     int                 TimeSec;      // the time passed (in seconds)
-    int                 TimeStop;     // the time to stop computation (in miliseconds)
-    int                 TimePrint;    // the time to print message
+    double              TimeStop;     // the time to stop computation (in miliseconds)
+    double              TimePrint;    // the time to print message
 };
 
 struct Super_GateStruct_t_
@@ -1107,10 +1107,12 @@ void Super_WriteLibrary( Super_Man_t * pMan )
 {
     Super_Gate_t * pGate, * pGateNext;
     FILE * pFile;
-    char FileName[100];
+    char * FileName;
     char * pNameGeneric;
     int i, Counter;
 
+    FileName = ABC_ALLOC( char, 10000 );
+
     // get the file name
     pNameGeneric = Extra_FileNameGeneric( pMan->pName );
     sprintf( FileName, "%s.super_old", pNameGeneric );
@@ -1152,6 +1154,8 @@ if ( pMan->fVerbose )
     printf( "The supergates are written using old format \"%s\" ", FileName );
     printf( "(%0.3f Mb).\n", ((double)Extra_FileSize(FileName))/(1<<20) );
 }
+
+    ABC_FREE( FileName );
 }
 
 /**Function*************************************************************
@@ -1251,11 +1255,13 @@ void Super_WriteLibraryTree( Super_Man_t * pMan )
 {
     Super_Gate_t * pSuper;
     FILE * pFile;
-    char FileName[100];
+    char * FileName;
     char * pNameGeneric;
     int i, Counter;
     int posStart;
 
+    FileName = ABC_ALLOC( char, 10000 );
+
     // get the file name
     pNameGeneric = Extra_FileNameGeneric( pMan->pName );
     sprintf( FileName, "%s.super", pNameGeneric );
@@ -1286,6 +1292,8 @@ if ( pMan->fVerbose )
     printf( "The supergates are written using new format \"%s\" ", FileName );
     printf( "(%0.3f Mb).\n", ((double)Extra_FileSize(FileName))/(1<<20) );
 }
+
+    ABC_FREE( FileName );
 }
 
 /**Function*************************************************************
diff --git a/src/misc/util/abc_global.h b/src/misc/util/abc_global.h
index 35a391ba..f58e3ddf 100644
--- a/src/misc/util/abc_global.h
+++ b/src/misc/util/abc_global.h
@@ -153,6 +153,15 @@ typedef unsigned __int64 ABC_UINT64_T;
 #define ABC_MIN(a,b)        ((a) < (b) ? (a) : (b))
 #define ABC_INFINITY        (100000000)
 
+#define ABC_PRT(a,t)    (printf("%s = ", (a)), printf("%7.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)))
+#define ABC_PRTn(a,t)   (printf("%s = ", (a)), printf("%6.2f sec  ", (float)(t)/(float)(CLOCKS_PER_SEC)))
+#define ABC_PRTP(a,t,T) (printf("%s = ", (a)), printf("%7.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0))
+#define ABC_PRM(a,f)    (printf("%s = ", (a)), printf("%7.2f Mb  ",    1.0*(f)/(1<<20)))
+
+
+//#define ABC_USE_MEM_REC 1
+
+#ifndef ABC_USE_MEM_REC
 #define ABC_ALLOC(type, num)     ((type *) malloc(sizeof(type) * (num)))
 #define ABC_CALLOC(type, num)     ((type *) calloc((num), sizeof(type)))
 #define ABC_FALLOC(type, num)     ((type *) memset(malloc(sizeof(type) * (num)), 0xff, sizeof(type) * (num)))
@@ -160,11 +169,16 @@ typedef unsigned __int64 ABC_UINT64_T;
 #define ABC_REALLOC(type, obj, num)    \
         ((obj) ? ((type *) realloc((char *)(obj), sizeof(type) * (num))) : \
          ((type *) malloc(sizeof(type) * (num))))
-
-#define ABC_PRT(a,t)    (printf("%s = ", (a)), printf("%7.2f sec\n", (float)(t)/(float)(CLOCKS_PER_SEC)))
-#define ABC_PRTn(a,t)   (printf("%s = ", (a)), printf("%6.2f sec  ", (float)(t)/(float)(CLOCKS_PER_SEC)))
-#define ABC_PRTP(a,t,T) (printf("%s = ", (a)), printf("%7.2f sec (%6.2f %%)\n", (float)(t)/(float)(CLOCKS_PER_SEC), (T)? 100.0*(t)/(T) : 0.0))
-#define ABC_PRM(a,f)    (printf("%s = ", (a)), printf("%7.2f Mb  ",    1.0*(f)/(1<<20)))
+#else
+#include "utilMem.h"
+#define ABC_ALLOC(type, num)     ((type *) Util_MemRecAlloc(malloc(sizeof(type) * (num))))
+#define ABC_CALLOC(type, num)     ((type *) Util_MemRecAlloc(calloc((num), sizeof(type))))
+#define ABC_FALLOC(type, num)     ((type *) memset(Util_MemRecAlloc(malloc(sizeof(type) * (num))), 0xff, sizeof(type) * (num)))
+#define ABC_FREE(obj)             ((obj) ?  (free((char *) Util_MemRecFree(obj)), (obj) = 0) : 0)
+#define ABC_REALLOC(type, obj, num)    \
+        ((obj) ? ((type *) Util_MemRecAlloc(realloc((char *)(Util_MemRecFree(obj)), sizeof(type) * (num)))) : \
+         ((type *) Util_MemRecAlloc(malloc(sizeof(type) * (num)))))
+#endif
 
 #ifdef __cplusplus
 }
diff --git a/src/misc/util/util_hack.h b/src/misc/util/util_hack.h
index 825c8bee..33fb6c6b 100644
--- a/src/misc/util/util_hack.h
+++ b/src/misc/util/util_hack.h
@@ -58,7 +58,7 @@ extern "C" {
 #     define ARGS(args)    args
 #  else
 #     define ARGS(args) ()
-# endif
+#  endif
 #endif
 
 extern long        Extra_CpuTime();
diff --git a/src/misc/vec/vec.h b/src/misc/vec/vec.h
index 915265f3..d6ed53b9 100644
--- a/src/misc/vec/vec.h
+++ b/src/misc/vec/vec.h
@@ -37,7 +37,6 @@
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/misc/vec/vecStr.h b/src/misc/vec/vecStr.h
index c77a3a17..bd10154c 100644
--- a/src/misc/vec/vecStr.h
+++ b/src/misc/vec/vecStr.h
@@ -572,6 +572,28 @@ static inline char Vec_StrPop( Vec_Str_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Reverses the order of entries.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline void Vec_StrReverseOrder( Vec_Str_t * p )
+{
+    int i, Temp;
+    for ( i = 0; i < p->nSize/2; i++ )
+    {
+        Temp = p->pArray[i];
+        p->pArray[i] = p->pArray[p->nSize-1-i];
+        p->pArray[p->nSize-1-i] = Temp;
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Comparison procedure for two clauses.]
 
   Description []
diff --git a/src/opt/mfs/mfsResub.c b/src/opt/mfs/mfsResub.c
index e49fd61d..008b6863 100644
--- a/src/opt/mfs/mfsResub.c
+++ b/src/opt/mfs/mfsResub.c
@@ -207,7 +207,7 @@ p->timeInt += clock() - clk;
         printf( "\n" );
     }
     iVar = -1;
-    while ( 1 )
+    while ( 1 ) 
     {
         if ( fVeryVerbose )
         {