Version abc70202

28 files changed, 1214 insertions, 301 deletions

diff --git a/abc.dsp b/abc.dsp
index 47e870d7..62245a6d 100644
--- a/abc.dsp
+++ b/abc.dsp
@@ -1697,6 +1697,18 @@ SOURCE=.\src\opt\res\resUpdate.c
 SOURCE=.\src\opt\res\resWin.c
 # End Source File
 # End Group
+# Begin Group "bdc"
+
+# PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\opt\bdc\bdc.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\opt\bdc\bdcInt.h
+# End Source File
+# End Group
 # End Group
 # Begin Group "map"
 
diff --git a/abc.rc b/abc.rc
index bbe7a6d4..82ef85de 100644
--- a/abc.rc
+++ b/abc.rc
@@ -102,6 +102,10 @@ alias src_rws     "st; rw -l; rs -K 6 -N 2 -l; rwz -l; rs -K 9 -N 2 -l; rwz -l;
 alias resyn2rs    "b; rs -K 6; rw; rs -K 6 -N 2; rf; rs -K 8; b; rs -K 8 -N 2; rw; rs -K 10; rwz; rs -K 10 -N 2; b; rs -K 12; rfz; rs -K 12 -N 2; rwz; b"
 alias compress2rs "b -l; rs -K 6 -l; rw -l; rs -K 6 -N 2 -l; rf -l; rs -K 8 -l; b -l; rs -K 8 -N 2 -l; rw -l; rs -K 10 -l; rwz -l; rs -K 10 -N 2 -l; b -l; rs -K 12 -l; rfz -l; rs -K 12 -N 2 -l; rwz -l; b -l"
 
+# experimental implementation of don't-cares
+alias resyn2rsdc    "b; rs -K 6 -F 2; rw; rs -K 6 -N 2 -F 2; rf; rs -K 8 -F 2; b; rs -K 8 -N 2 -F 2; rw; rs -K 10 -F 2; rwz; rs -K 10 -N 2 -F 2; b; rs -K 12 -F 2; rfz; rs -K 12 -N 2 -F 2; rwz; b"
+alias compress2rsdc "b -l; rs -K 6 -F 2 -l; rw -l; rs -K 6 -N 2 -F 2 -l; rf -l; rs -K 8 -F 2 -l; b -l; rs -K 8 -N 2 -F 2 -l; rw -l; rs -K 10 -F 2 -l; rwz -l; rs -K 10 -N 2 -F 2 -l; b -l; rs -K 12 -F 2 -l; rfz -l; rs -K 12 -N 2 -F 2 -l; rwz -l; b -l"
+
 # temporaries
 #alias t        "rvl th/lib.v; rvv th/t2.v"
 #alias t        "so c/pure_sat/test.c"
diff --git a/src/aig/ivy/ivy.h b/src/aig/ivy/ivy.h
index 9e944028..6aa7fa9f 100644
--- a/src/aig/ivy/ivy.h
+++ b/src/aig/ivy/ivy.h
@@ -152,6 +152,7 @@ struct Ivy_FraigParams_t_
 typedef struct Ivy_Cut_t_ Ivy_Cut_t;
 struct Ivy_Cut_t_
 {
+    int         nLatches;
     short       nSize;
     short       nSizeMax;
     int         pArray[IVY_CUT_INPUT];
@@ -541,6 +542,7 @@ extern Ivy_Obj_t *     Ivy_ObjRecognizeMux( Ivy_Obj_t * pObj, Ivy_Obj_t ** ppObj
 extern Ivy_Obj_t *     Ivy_ObjReal( Ivy_Obj_t * pObj );
 extern void            Ivy_ObjPrintVerbose( Ivy_Man_t * p, Ivy_Obj_t * pObj, int fHaig );
 extern void            Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig );
+extern int             Ivy_CutTruthPrint( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth );
 
 #ifdef __cplusplus
 }
diff --git a/src/aig/ivy/ivySeq.c b/src/aig/ivy/ivySeq.c
index 263a4398..0ee29fee 100644
--- a/src/aig/ivy/ivySeq.c
+++ b/src/aig/ivy/ivySeq.c
@@ -41,6 +41,11 @@ static inline int Ivy_CutHashValue( int NodeId )  { return 1 << (NodeId % 31); }
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
+//int nMoves;
+//int nMovesS;
+//int nClauses;
+//int timeInv;
+
 /**Function*************************************************************
 
   Synopsis    [Performs incremental rewriting of the AIG.]
@@ -58,6 +63,7 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
     Ivy_Obj_t * pNode;
     int i, nNodes, nGain;
     int clk, clkStart = clock();
+
     // set the DC latch values
     Ivy_ManForEachLatch( p, pNode, i )
         pNode->Init = IVY_INIT_DC;
@@ -81,7 +87,7 @@ int Ivy_ManRewriteSeq( Ivy_Man_t * p, int fUseZeroCost, int fVerbose )
 //        if ( Ivy_ObjIsBuf(pNode) )
 //            continue;
         // stop if all nodes have been tried once
-        if ( i > nNodes )
+        if ( i > nNodes ) 
             break;
         // for each cut, try to resynthesize it
         nGain = Ivy_NodeRewriteSeq( p, pManRwt, pNode, fUseZeroCost );
@@ -114,6 +120,7 @@ Rwt_ManAddTimeTotal( pManRwt, clock() - clkStart );
     return 1;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Performs rewriting for one node.]
@@ -140,11 +147,11 @@ int Ivy_NodeRewriteSeq( Ivy_Man_t * pMan, Rwt_Man_t * p, Ivy_Obj_t * pNode, int
     Ivy_Cut_t * pCut;
     Ivy_Obj_t * pFanin;//, * pFanout;
     Vec_Ptr_t * vFanout;
-    unsigned uPhase, uTruthBest, uTruth;
+    unsigned uPhase, uTruthBest, uTruth;//, nNewClauses;
     char * pPerm;
     int nNodesSaved, nNodesSaveCur;
     int i, c, GainCur, GainBest = -1;
-    int clk, clk2;
+    int clk, clk2;//, clk3;
 
     p->nNodesConsidered++;
     // get the node's cuts
@@ -201,18 +208,6 @@ clk2 = clock();
         Vec_PtrForEachEntry( p->vFaninsCur, pFanin, i )
             Ivy_ObjRefsDec( Ivy_Regular(pFanin) );
 p->timeMffc += clock() - clk2;
-/*
-if ( pNode->Id == 8648 )
-{
-    int i;
-    printf( "Trying cut : {" );
-    for ( i = 0; i < pCut->nSize; i++ )
-        printf( " %d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
-//    printf( " }\n" );
-    printf( " }   " );
-    Extra_PrintBinary( stdout, &uTruth, 16 );  printf( "\n" );
-}
-*/
 
         // evaluate the cut
 clk2 = clock();
@@ -252,6 +247,15 @@ p->timeRes += clock() - clk;
     }
 */
 
+//clk3 = clock();
+//nNewClauses = Ivy_CutTruthPrint( pMan, p->pCut, uTruth );
+//timeInv += clock() - clk;
+
+//    nClauses += nNewClauses;
+//    nMoves++;
+//    if ( nNewClauses > 0 )
+//        nMovesS++;
+
     // copy the leaves
     Ivy_GraphPrepare( p->pGraph, p->pCut, p->vFanins, p->pPerm );
 
diff --git a/src/aig/ivy/ivyUtil.c b/src/aig/ivy/ivyUtil.c
index 0e44c216..ab62a276 100644
--- a/src/aig/ivy/ivyUtil.c
+++ b/src/aig/ivy/ivyUtil.c
@@ -731,6 +731,86 @@ void Ivy_ManPrintVerbose( Ivy_Man_t * p, int fHaig )
     printf( "\n" );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Performs incremental rewriting of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_CutTruthPrint2( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth )
+{
+    int i;
+    printf( "Trying cut : {" );
+    for ( i = 0; i < pCut->nSize; i++ )
+        printf( " %6d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
+    printf( " }   " );
+    Extra_PrintBinary( stdout, &uTruth, 16 );  printf( "\n" );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs incremental rewriting of the AIG.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Ivy_CutTruthPrint( Ivy_Man_t * p, Ivy_Cut_t * pCut, unsigned uTruth )
+{
+    Vec_Ptr_t * vArray;
+    Ivy_Obj_t * pObj, * pFanout;
+    int nLatches = 0;
+    int nPresent = 0;
+    int i, k;
+    int fVerbose = 0;
+
+    if ( fVerbose )
+        printf( "Trying cut : {" );
+    for ( i = 0; i < pCut->nSize; i++ )
+    {
+        if ( fVerbose )
+            printf( " %6d(%d)", Ivy_LeafId(pCut->pArray[i]), Ivy_LeafLat(pCut->pArray[i]) );
+        nLatches += Ivy_LeafLat(pCut->pArray[i]);
+    }
+    if ( fVerbose )
+        printf( " }   " );
+    if ( fVerbose )
+        printf( "Latches = %d. ", nLatches );
+
+    // check if there are latches on the fanout edges
+    vArray = Vec_PtrAlloc( 100 );
+    for ( i = 0; i < pCut->nSize; i++ )
+    {
+        pObj = Ivy_ManObj( p, Ivy_LeafId(pCut->pArray[i]) );
+        Ivy_ObjForEachFanout( p, pObj, vArray, pFanout, k )
+        {
+            if ( Ivy_ObjIsLatch(pFanout) )
+            {
+                nPresent++;
+                break;
+            }
+        }
+    }
+    Vec_PtrSize( vArray );
+    if ( fVerbose )
+    {
+        printf( "Present = %d. ", nPresent );
+        if ( nLatches > nPresent )
+            printf( "Clauses = %d. ", 2*(nLatches - nPresent) );
+        printf( "\n" );
+    }
+    return ( nLatches > nPresent ) ? 2*(nLatches - nPresent) : 0;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index ce1947a9..3d46cdf0 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -814,6 +814,7 @@ extern int                Abc_NtkGetExorNum( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetMuxNum( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetChoiceNum( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk );
+extern int                Abc_NtkGetTotalFanins( Abc_Ntk_t * pNtk );
 extern void               Abc_NtkCleanCopy( Abc_Ntk_t * pNtk );
 extern int                Abc_NtkCountCopy( Abc_Ntk_t * pNtk );
 extern Vec_Ptr_t *        Abc_NtkSaveCopy( Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index b86dc88f..3070e01a 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -105,7 +105,7 @@ void Abc_NtkIncrementTravId( Abc_Ntk_t * pNtk )
 {
     Abc_Obj_t * pObj;
     int i;
-    if ( pNtk->nTravIds == (1<<30)-1 )
+    if ( pNtk->nTravIds >= (1<<30)-1 )
     {
         pNtk->nTravIds = 0;
         Abc_NtkForEachObj( pNtk, pObj, i )
@@ -447,6 +447,26 @@ int Abc_NtkGetFaninMax( Abc_Ntk_t * pNtk )
 
 /**Function*************************************************************
 
+  Synopsis    [Reads the total number of all fanins.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkGetTotalFanins( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i, nFanins = 0;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        nFanins += Abc_ObjFaninNum(pNode);
+    return nFanins;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Cleans the copy field of all objects.]
 
   Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c2a6214d..3a6874ca 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2569,6 +2569,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     Res_Par_t Pars, * pPars = &Pars;
     int c;
 
+//    printf( "Implementation of this command is not finished.\n" );
+//    return 1;
+
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
@@ -2641,8 +2644,8 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     fprintf( pErr, "usage: mfs [-W <NM>] [-S <num>] [-vwh]\n" );
     fprintf( pErr, "\t           performs resubstitution-based resynthesis with don't-cares\n" );
-    fprintf( pErr, "\t-W <NM>  : specifies the windowing paramters (00 < NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
-    fprintf( pErr, "\t-S <num> : specifies the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords );
+    fprintf( pErr, "\t-W <NM>  : Fanin/Fanout levels (NxM) of the window (00 <= NM <= 99) [default = %d%d]\n", pPars->nWindow/10, pPars->nWindow%10 );
+    fprintf( pErr, "\t-S <num> : the number of simulation words (1 <= n <= 256) [default = %d]\n", pPars->nSimWords );
     fprintf( pErr, "\t-v       : toggle verbose printout [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-w       : toggle printout subgraph statistics [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );
     fprintf( pErr, "\t-h       : print the command usage\n");
diff --git a/src/base/abci/abcIvy.c b/src/base/abci/abcIvy.c
index 243067ce..00f8c183 100644
--- a/src/base/abci/abcIvy.c
+++ b/src/base/abci/abcIvy.c
@@ -187,18 +187,44 @@ Abc_Ntk_t * Abc_NtkIvyHaig( Abc_Ntk_t * pNtk, int nIters, int fUseZeroCost, int
 {
     Abc_Ntk_t * pNtkAig;
     Ivy_Man_t * pMan;
+    int clk;
 //    int i;
-
+/*
+extern int nMoves;
+extern int nMovesS;
+extern int nClauses;
+extern int timeInv;
+
+nMoves = 0;
+nMovesS = 0;
+nClauses = 0;
+timeInv = 0;
+*/
     pMan = Abc_NtkIvyBefore( pNtk, 1, 1 );
     if ( pMan == NULL )
         return NULL;
 //timeRetime = clock();
 
+clk = clock();
     Ivy_ManHaigStart( pMan, fVerbose );
 //    Ivy_ManRewriteSeq( pMan, 0, 0 );
 //    for ( i = 0; i < nIters; i++ )
 //        Ivy_ManRewriteSeq( pMan, fUseZeroCost, 0 );
+
+//printf( "%d ", Ivy_ManNodeNum(pMan) );
     Ivy_ManRewriteSeq( pMan, 0, 0 );
+    Ivy_ManRewriteSeq( pMan, 0, 0 );
+    Ivy_ManRewriteSeq( pMan, 1, 0 );
+//printf( "%d ", Ivy_ManNodeNum(pMan) );
+//printf( "%d ", Ivy_ManNodeNum(pMan->pHaig) );
+//PRT( " ", clock() - clk );
+//printf( "\n" );
+/*
+    printf( "Moves = %d.  ", nMoves );
+    printf( "MovesS = %d.  ", nMovesS );
+    printf( "Clauses = %d.  ", nClauses );
+    PRT( "Time", timeInv );
+*/
 //    Ivy_ManRewriteSeq( pMan, 1, 0 );
 //printf( "Haig size = %d.\n", Ivy_ManNodeNum(pMan->pHaig) );
 //    Ivy_ManHaigPostprocess( pMan, fVerbose );
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index e66ce018..177c269b 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -77,7 +77,10 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored )
 //            fprintf( pFile, " (other = %d)", Abc_NtkNodeNum(pNtk)-3*Num2 );
     }
     else 
+    {
         fprintf( pFile, "  nd = %5d", Abc_NtkNodeNum(pNtk) );
+        fprintf( pFile, "  net = %5d", Abc_NtkGetTotalFanins(pNtk) );
+    }
 
     if ( Abc_NtkIsStrash(pNtk) || Abc_NtkIsNetlist(pNtk) )
     {
diff --git a/src/base/abci/abcSat.c b/src/base/abci/abcSat.c
index 96540269..d9cae254 100644
--- a/src/base/abci/abcSat.c
+++ b/src/base/abci/abcSat.c
@@ -65,6 +65,10 @@ int Abc_NtkMiterSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int
     pSat = Abc_NtkMiterSatCreate( pNtk, 0 );
     if ( pSat == NULL )
         return 1;
+//printf( "%d \n", pSat->clauses.size );
+//sat_solver_delete( pSat );
+//return 1;
+
 //    printf( "Created SAT problem with %d variable and %d clauses. ", sat_solver_nvars(pSat), sat_solver_nclauses(pSat) );
 //    PRT( "Time", clock() - clk );
 
@@ -619,7 +623,7 @@ void * Abc_NtkMiterSatCreate( Abc_Ntk_t * pNtk, int fAllPrimes )
 
     nMuxes = 0;
     pSat = sat_solver_new();
-sat_solver_store_alloc( pSat );
+//sat_solver_store_alloc( pSat );
     RetValue = Abc_NtkMiterSatCreateInt( pSat, pNtk );
 sat_solver_store_mark_roots( pSat );
 
diff --git a/src/opt/bdc/bdc.h b/src/opt/bdc/bdc.h
new file mode 100644
index 00000000..f0976bfe
--- /dev/null
+++ b/src/opt/bdc/bdc.h
@@ -0,0 +1,73 @@
+/**CFile****************************************************************
+
+  FileName    [bdc.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Truth-table-based bi-decomposition engine.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 30, 2007.]
+
+  Revision    [$Id: bdc.h,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __BDC_H__
+#define __BDC_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Bdc_Man_t_ Bdc_Man_t;
+typedef struct Bdc_Par_t_ Bdc_Par_t;
+struct Bdc_Par_t_
+{
+    // general parameters
+    int           nVarsMax;      // the maximum support
+    int           fVerbose;      // enable basic stats
+    int           fVeryVerbose;  // enable detailed stats
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== bdcCore.c ==========================================================*/
+extern Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars );
+extern void        Bdc_ManAlloc( Bdc_Man_t * p );
+extern int         Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodeLimit );
+
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/bdc/bdcCore.c b/src/opt/bdc/bdcCore.c
new file mode 100644
index 00000000..f120ac3f
--- /dev/null
+++ b/src/opt/bdc/bdcCore.c
@@ -0,0 +1,157 @@
+/**CFile****************************************************************
+
+  FileName    [bdcCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Truth-table-based bi-decomposition engine.]
+
+  Synopsis    [The gateway to bi-decomposition.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 30, 2007.]
+
+  Revision    [$Id: bdcCore.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "bdcInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Allocate resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bdc_Man_t * Bdc_ManAlloc( Bdc_Par_t * pPars )
+{
+    Bdc_Man_t * p;
+    int i;
+    p = ALLOC( Bdc_Man_t, 1 );
+    memset( p, 0, sizeof(Bdc_Man_t) );
+    assert( pPars->nVarsMax > 3 && pPars->nVarsMax < 16 );
+    p->pPars = pPars;
+    // memory
+    p->vMemory = Vec_IntStart( 1 << 16 );
+    // internal nodes
+    p->nNodesAlloc = 256;
+    p->pNodes = ALLOC( Bdc_Fun_t, p->nNodesAlloc );
+    // set up hash table
+    p->nTableSize = (1 << p->pPars->nVarsMax);
+    p->pTable = ALLOC( Bdc_Fun_t *, p->nTableSize );
+    memset( p->pTable, 0, sizeof(Bdc_Fun_t *) * p->nTableSize );
+    p->vSpots = Vec_IntAlloc( 256 );
+    // set up constant 1 and elementary variables
+    for ( i = 0; i < pPars->nVarsMax; i++ )
+    {
+    }
+    p->nNodes = pPars->nVarsMax + 1;
+    // remember the current place in memory
+    p->nMemStart = Vec_IntSize( p->vMemory );
+    return p;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocate resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_ManAlloc( Bdc_Man_t * p )
+{
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Sets up the divisors.]
+
+  Description [The first n+1 entries are const1 and elem variables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bdc_ManPrepare( Bdc_Man_t * p, Vec_Ptr_t * vDivs )
+{
+    Bdc_Fun_t ** pSpot, * pFunc;
+    unsigned * puTruth;
+    int i;
+    // clean hash table
+    Vec_PtrForEachEntry( p->vSpots, pSpot, i )
+        *pSpot = NULL;
+    // reset nodes
+    p->nNodes = p->pPars->nVarsMax + 1;
+    // reset memory
+    Vec_IntShrink( p->vMemory, p->nMemStart );
+    // add new nodes to the hash table
+    Vec_PtrForEachEntry( vDivs, puTruth, i )
+    {
+        pFunc = Bdc_ManNewNode( p );
+        pFunc->Type = BDC_TYPE_PI;
+        pFunc->puFunc = puTruth;
+        pFunc->uSupp = Kit_TruthSupport( puTruth, p->nVars );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs decomposition of one function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bdc_ManDecompose( Bdc_Man_t * p, unsigned * puFunc, unsigned * puCare, int nVars, Vec_Ptr_t * vDivs, int nNodeLimit )
+{
+    Bdc_Isf_t Isf, * pIsf = &Isf;
+    // set current manager parameters
+    p->nVars = nVars;
+    p->nWords = Kit_TruthWordNum( nVars );
+    p->nNodeLimit = nNodeLimit;
+    Bdc_ManPrepare( p, vDivs );
+    // copy the function
+    pIsf->uSupp = Kit_TruthSupport( puFunc, p->nVars ) | Kit_TruthSupport( puCare, p->nVars );
+    pIsf->puOn = Vec_IntFetch( p->vMemory, p->nWords );
+    pIsf->puOff = Vec_IntFetch( p->vMemory, p->nWords );
+    Kit_TruthAnd( pIsf->puOn, puCare, puFunc, p->nVars );
+    Kit_TruthSharp( pIsf->puOff, puCare, puFunc, p->nVars );
+    // call decomposition
+    p->pRoot = Bdc_ManDecompose_rec( p, pIsf );
+    if ( p->pRoot == NULL )
+        return -1;
+    return p->nNodes - (p->pPars->nVarsMax + 1);
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/bdc/bdcDec.c b/src/opt/bdc/bdcDec.c
new file mode 100644
index 00000000..1fbea911
--- /dev/null
+++ b/src/opt/bdc/bdcDec.c
@@ -0,0 +1,76 @@
+/**CFile****************************************************************
+
+  FileName    [bdc_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Truth-table-based bi-decomposition engine.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 30, 2007.]
+
+  Revision    [$Id: bdc_.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "bdcInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one step of bi-decomposition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bdc_Fun_t * Bdc_ManDecompose_rec( Bdc_Man_t * p, Bdc_Isf_t * pIsf )
+{
+    Bdc_Fun_t * pFunc;
+    Bdc_Isf_t IsfA, * pIsfA = &IsfA;
+    Bdc_Isf_t IsfB, * pIsfB = &IsfB;
+    int Type;
+    Bdc_SuppMinimize( p, pIsf );
+    if ( pFunc = Bdc_TableLookup( p, pIsf ) )
+        return pFunc;
+    pFunc = Bdc_ManNewNode( p );
+    pFunc->Type = Bdc_DecomposeStep( p, pIsf, pIsfA, pIsfB );
+    pFunc->pFan0 = Bdc_ManDecompose_rec( p, pIsfA );
+    if ( Bdc_DecomposeUpdateRight( p, pIsf, pIsfA, pIsfB, pFunc->pFan0->puFunc ) )
+    {
+        p->nNodes--;
+        return pFunc->pFan0;
+    }
+    pFunc->pFan1 = Bdc_ManDecompose_rec( p, pIsfA );
+    pFunc->puFunc = Vec_IntFetch( p->vMemory, p->nWords );
+    pFunc->puFunc = 
+
+
+
+
+
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/bdc/bdcInt.h b/src/opt/bdc/bdcInt.h
new file mode 100644
index 00000000..39d50ae9
--- /dev/null
+++ b/src/opt/bdc/bdcInt.h
@@ -0,0 +1,127 @@
+/**CFile****************************************************************
+
+  FileName    [bdcInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Truth-table-based bi-decomposition engine.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 15, 2007.]
+
+  Revision    [$Id: resInt.h,v 1.00 2007/01/15 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __BDC_INT_H__
+#define __BDC_INT_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "dec.h"
+#include "bdc.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// network types
+typedef enum { 
+    BDC_TYPE_NONE = 0,  // 0:  unknown
+    BDC_TYPE_CONST1,    // 1:  constant 1
+    BDC_TYPE_PI,        // 2:  primary input
+    BDC_TYPE_AND,       // 4:  AND-gate
+    BDC_TYPE_XOR,       // 5:  XOR-gate
+    BDC_TYPE_MUX,       // 6:  MUX-gate
+    BDC_TYPE_OTHER      // 7:  unused
+} Bdc_Type_t;
+
+typedef struct Bdc_Fun_t_ Bdc_Fun_t;
+struct Bdc_Fun_t_
+{
+    int              Type;         // Const1, PI, AND, XOR, MUX
+    Bdc_Fun_t *      pFan0;        // next function with same support
+    Bdc_Fun_t *      pFan1;        // next function with same support
+    Bdc_Fun_t *      pFan2;        // next function with same support
+    unsigned         uSupp;        // bit mask of current support
+    unsigned *       puFunc;       // the function of the node
+    Bdc_Fun_t *      pNext;        // next function with same support
+    void *           pCopy;        // the copy field
+};
+
+typedef struct Bdc_Isf_t_ Bdc_Isf_t;
+struct Bdc_Isf_t_
+{
+    unsigned         uSupp;        // bit mask of current support
+    unsigned         uUnique;      // bit mask of unique support
+    unsigned *       puOn;         // on-set
+    unsigned *       puOff;        // off-set
+    int              Cost;         // cost of this component
+};
+
+typedef struct Bdc_Man_t_ Bdc_Man_t;
+struct Bdc_Man_t_
+{
+    // external parameters
+    Bdc_Par_t *      pPars;        // parameter set
+    int              nVars;        // the number of variables
+    int              nWords;       // the number of words 
+    int              nNodeLimit;   // the limit on the number of new nodes
+    // internal nodes
+    Bdc_Fun_t *      pNodes;       // storage for decomposition nodes
+    int              nNodes;       // the number of nodes used
+    int              nNodesAlloc;  // the number of nodes allocated  
+    Bdc_Fun_t *      pRoot;        // the root node
+    // resub candidates
+    Bdc_Fun_t **     pTable;       // hash table of candidates
+    int              nTableSize;   // hash table size (1 << nVarsMax)
+    // internal memory manager
+    Vec_Int_t *      vMemory;      // memory for internal truth tables
+    int              nMemStart;    // the starting memory size
+};
+
+// working with complemented attributes of objects
+static inline bool        Bdc_IsComplement( Bdc_Fun_t * p )       { return (bool)((unsigned long)p & (unsigned long)01);             }
+static inline Bdc_Fun_t * Bdc_Regular( Bdc_Fun_t * p )            { return (Bdc_Fun_t *)((unsigned long)p & ~(unsigned long)01);     }
+static inline Bdc_Fun_t * Bdc_Not( Bdc_Fun_t * p )                { return (Bdc_Fun_t *)((unsigned long)p ^  (unsigned long)01);     }
+static inline Bdc_Fun_t * Bdc_NotCond( Bdc_Fun_t * p, int c )     { return (Bdc_Fun_t *)((unsigned long)p ^  (unsigned long)(c!=0)); }
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== bdcSupp.c ==========================================================*/
+extern int              Bdc_SuppMinimize( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
+/*=== bdcTable.c ==========================================================*/
+extern Bdc_Fun_t *      Bdc_TableLookup( Bdc_Man_t * p, Bdc_Isf_t * pIsf );
+
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/bdc/bdc_.c b/src/opt/bdc/bdc_.c
new file mode 100644
index 00000000..0fa51092
--- /dev/null
+++ b/src/opt/bdc/bdc_.c
@@ -0,0 +1,50 @@
+/**CFile****************************************************************
+
+  FileName    [bdc_.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Truth-table-based bi-decomposition engine.]
+
+  Synopsis    []
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - January 30, 2007.]
+
+  Revision    [$Id: bdc_.c,v 1.00 2007/01/30 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "abc.h"
+#include "bdcInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/opt/bdc/module.make b/src/opt/bdc/module.make
new file mode 100644
index 00000000..85936f5b
--- /dev/null
+++ b/src/opt/bdc/module.make
@@ -0,0 +1,8 @@
+SRC +=  src/opt/res/resCore.c \
+    src/opt/res/resDivs.c \
+    src/opt/res/resFilter.c \
+    src/opt/res/resSat.c \
+    src/opt/res/resSim.c \
+    src/opt/res/resStrash.c \
+    src/opt/res/resUpdate.c \
+    src/opt/res/resWin.c
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index 5f814c3a..609addf9 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -39,15 +39,19 @@ struct Res_Man_t_
     Sto_Man_t *   pCnf;          // the CNF of the SAT problem
     Int_Man_t *   pMan;          // interpolation manager;
     Vec_Int_t *   vMem;          // memory for intermediate SOPs
-    Vec_Vec_t *   vResubs;       // resubstitution candidates
+    Vec_Vec_t *   vResubs;       // resubstitution candidates of the AIG
+    Vec_Vec_t *   vResubsW;      // resubstitution candidates of the window
     Vec_Vec_t *   vLevels;       // levelized structure for updating
     // statistics
     int           nWins;         // the number of windows tried
     int           nWinNodes;     // the total number of window nodes
     int           nDivNodes;     // the total number of divisors
+    int           nWinsTriv;     // the total number of trivial windows
+    int           nWinsUsed;     // the total number of useful windows (with at least one candidate)
     int           nCandSets;     // the total number of candidates
     int           nProvedSets;   // the total number of proved groups
     int           nSimEmpty;     // the empty simulation info
+    int           nTotalNets;    // the total number of nets
     // runtime
     int           timeWin;       // windowing
     int           timeDiv;       // divisors
@@ -90,6 +94,7 @@ Res_Man_t * Res_ManAlloc( Res_Par_t * pPars )
     p->pMan = Int_ManAlloc( 512 );
     p->vMem = Vec_IntAlloc( 0 );
     p->vResubs = Vec_VecStart( pPars->nCands );
+    p->vResubsW = Vec_VecStart( pPars->nCands );
     p->vLevels = Vec_VecStart( 32 );
     return p;
 }
@@ -113,9 +118,11 @@ void Res_ManFree( Res_Man_t * p )
         printf( "Nodes = %d. (Ave = %5.1f)  ", p->nWinNodes, 1.0*p->nWinNodes/p->nWins );
         printf( "Divs = %d. (Ave = %5.1f)  ",  p->nDivNodes, 1.0*p->nDivNodes/p->nWins );
         printf( "\n" );
-        printf( "SimEmpt = %d. ", p->nSimEmpty );
+        printf( "WinsTriv = %d. ", p->nWinsTriv );
+        printf( "SimsEmpt = %d. ", p->nSimEmpty );
+        printf( "WindUsed = %d. ", p->nWinsUsed );
         printf( "Cands = %d. ", p->nCandSets );
-        printf( "Proved = %d. ", p->nProvedSets );
+        printf( "Proved = %d. (%.2f %%)", p->nProvedSets, 100.0*p->nProvedSets/p->nTotalNets );
         printf( "\n" );
 
         PRT( "Windowing  ", p->timeWin );
@@ -135,6 +142,7 @@ void Res_ManFree( Res_Man_t * p )
     Int_ManFree( p->pMan );
     Vec_IntFree( p->vMem );
     Vec_VecFree( p->vResubs );
+    Vec_VecFree( p->vResubsW );
     Vec_VecFree( p->vLevels );
     free( p );
 }
@@ -164,6 +172,7 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
 
     // start the manager
     p = Res_ManAlloc( pPars );
+    p->nTotalNets = Abc_NtkGetTotalFanins(pNtk);
     // set the number of levels
     Abc_NtkLevel( pNtk );
 
@@ -182,15 +191,32 @@ clk = clock();
 p->timeWin += clock() - clk;
         if ( !RetValue )
             continue;
+        p->nWinsTriv += Res_WinIsTrivial( p->pWin );
 
-        p->nWins++;
-        p->nWinNodes += Vec_VecSizeSize( p->pWin->vLevels );
+        if ( p->pPars->fVeryVerbose )
+        {
+            printf( "%5d (lev=%2d) : ", pObj->Id, pObj->Level );
+            printf( "Win = %3d/%3d/%4d/%3d   ", 
+                Vec_PtrSize(p->pWin->vLeaves), 
+                Vec_PtrSize(p->pWin->vBranches),
+                Vec_PtrSize(p->pWin->vNodes), 
+                Vec_PtrSize(p->pWin->vRoots) );
+        }
 
         // collect the divisors
 clk = clock();
         Res_WinDivisors( p->pWin, pObj->Level - 1 );
 p->timeDiv += clock() - clk;
-        p->nDivNodes += Vec_PtrSize( p->pWin->vDivs );
+
+        p->nWins++;
+        p->nWinNodes += Vec_PtrSize(p->pWin->vNodes);
+        p->nDivNodes += Vec_PtrSize( p->pWin->vDivs);
+
+        if ( p->pPars->fVeryVerbose )
+        {
+            printf( "D = %3d ", Vec_PtrSize(p->pWin->vDivs) );
+            printf( "D+ = %3d ", p->pWin->nDivsPlus );
+        }
 
         // create the AIG for the window
 clk = clock();
@@ -200,13 +226,6 @@ p->timeAig += clock() - clk;
 
         if ( p->pPars->fVeryVerbose )
         {
-            printf( "%5d (lev=%2d) : ", pObj->Id, pObj->Level );
-            printf( "Win = %3d/%3d/%4d/%3d   ", 
-                Vec_PtrSize(p->pWin->vLeaves) - p->pWin->nLeavesPlus, 
-                p->pWin->nLeavesPlus, Vec_VecSizeSize(p->pWin->vLevels), 
-                Vec_PtrSize(p->pWin->vRoots) );
-            printf( "D = %3d ", Vec_PtrSize(p->pWin->vDivs) );
-            printf( "D+ = %3d ", p->pWin->nDivsPlus );
             printf( "AIG = %4d ", Abc_NtkNodeNum(p->pAig) );
             printf( "\n" );
         }
@@ -223,12 +242,14 @@ p->timeSim += clock() - clk;
 
         // find resub candidates for the node
 clk = clock();
-        RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs );
+        RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs, p->vResubsW );
 p->timeCand += clock() - clk;
         p->nCandSets += RetValue;
         if ( RetValue == 0 )
             continue;
 
+        p->nWinsUsed++;
+
         // iterate through candidate resubstitutions
         Vec_VecForEachLevel( p->vResubs, vFanins, k )
         {
@@ -247,26 +268,19 @@ p->timeSat += clock() - clk;
             }
             p->nProvedSets++;
 //            printf( " Unsat\n" );
-            continue;
+//            continue;
 
             // write it into a file
 //            Sto_ManDumpClauses( p->pCnf, "trace.cnf" );
 
-
-            // interplate the problem if it was UNSAT
+            // interpolate the problem if it was UNSAT
 clk = clock();
-            RetValue = Int_ManInterpolate( p->pMan, p->pCnf, p->pPars->fVerbose, &puTruth );
+            nFanins = Int_ManInterpolate( p->pMan, p->pCnf, 0, &puTruth );
 p->timeInt += clock() - clk;
-            assert( RetValue == Vec_PtrSize(vFanins) - 2 );
-
-            if ( puTruth )
-            {
-                Extra_PrintBinary( stdout, puTruth, 1 << RetValue );
-                printf( "\n" );
-            }
-
-            continue;
-            
+            assert( nFanins == Vec_PtrSize(vFanins) - 2 );
+            assert( puTruth );
+//            Extra_PrintBinary( stdout, puTruth, 1 << nFanins );  printf( "\n" );
+           
             // transform interpolant into the AIG
             pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
 
@@ -276,10 +290,11 @@ p->timeInt += clock() - clk;
 
             // update the network
 clk = clock();
-            Res_UpdateNetwork( pObj, vFanins, pFunc, p->vLevels );
+            Res_UpdateNetwork( pObj, Vec_VecEntry(p->vResubsW, k), pFunc, p->vLevels );
 p->timeUpd += clock() - clk;
             break;
         }
+
     }
 
     // quit resubstitution manager
diff --git a/src/opt/res/resDivs.c b/src/opt/res/resDivs.c
index bff91983..af30592c 100644
--- a/src/opt/res/resDivs.c
+++ b/src/opt/res/resDivs.c
@@ -25,6 +25,9 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static void Res_WinMarkTfi( Res_Win_t * p );
+static int  Res_WinVisitMffc( Res_Win_t * p );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
@@ -43,84 +46,155 @@
 void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
 {
     Abc_Obj_t * pObj, * pFanout, * pFanin;
-    int i, k, f, m;
+    int k, f, m;
 
+    // set the maximum level of the divisors
     p->nLevDivMax = nLevDivMax;
 
-    // mark the leaves and the internal nodes
-    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
-        pObj->fMarkA = 1;
-    Vec_VecForEachEntry( p->vLevels, pObj, i, k )
-        pObj->fMarkA = 1;
+    // mark the TFI with the current trav ID
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
+    Res_WinMarkTfi( p );
 
-    // prepare the new trav ID
+    // mark with the current trav ID those nodes that should not be divisors:
+    // (1) the node and its TFO
+    // (2) the MFFC of the node
+    // (3) the node's fanins (these are treated as a special case)
     Abc_NtkIncrementTravId( p->pNode->pNtk );
-    // mark the TFO of the node (does not increment trav ID)
-    Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax, NULL );
-    // mark the MFFC of the node (does not increment trav ID)
+    Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax );
     Res_WinVisitMffc( p );
+    Abc_ObjForEachFanin( p->pNode, pObj, k )
+        Abc_NodeSetTravIdCurrent( pObj );
 
-    // what about the fanouts of the leaves!!!
+    // at this point the nodes are marked with two trav IDs:
+    // nodes to be collected as divisors are marked with previous trav ID
+    // nodes to be avoided as divisors are marked with current trav ID
 
-    // go through all the legal levels and check if their fanouts can be divisors
-    p->nDivsPlus = 0;
-    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevDivMax - 1 )
+    // start collecting the divisors
+    Vec_PtrClear( p->vDivs );
+    Vec_PtrForEachEntry( p->vLeaves, pObj, k )
+    {
+        assert( (int)pObj->Level >= p->nLevLeafMin ); 
+        if ( !Abc_NodeIsTravIdPrevious(pObj) )
+            continue;
+        if ( (int)pObj->Level > p->nLevDivMax )
+            continue;
+        Vec_PtrPush( p->vDivs, pObj );
+    }
+    // add the internal nodes to the data structure
+    Vec_PtrForEachEntry( p->vNodes, pObj, k )
     {
-        // skip nodes in the TFO or in the MFFC of node
-        if ( Abc_NodeIsTravIdCurrent(pObj) )
+        if ( !Abc_NodeIsTravIdPrevious(pObj) )
+            continue;
+        if ( (int)pObj->Level > p->nLevDivMax )
             continue;
+        Vec_PtrPush( p->vDivs, pObj );
+    }
+
+    // explore the fanouts of already collected divisors
+    p->nDivsPlus = 0;
+    Vec_PtrForEachEntry( p->vDivs, pObj, k )
+    {
         // consider fanouts of this node
         Abc_ObjForEachFanout( pObj, pFanout, f )
         {
+            // stop if there are too many fanouts
+            if ( f > 20 )
+                break;
             // skip nodes that are already added
-            if ( pFanout->fMarkA )
-                continue;
-            // skip COs
-            if ( !Abc_ObjIsNode(pFanout) ) 
+            if ( Abc_NodeIsTravIdPrevious(pFanout) )
                 continue;
             // skip nodes in the TFO or in the MFFC of node
             if ( Abc_NodeIsTravIdCurrent(pFanout) )
                 continue;
+            // skip COs
+            if ( !Abc_ObjIsNode(pFanout) ) 
+                continue;
             // skip nodes with large level
-            if ( (int)pFanout->Level > p->nLevDivMax )
+            if ( (int)pFanout->Level >= p->nLevDivMax )
                 continue;
-            // skip nodes whose fanins are not in the cone
+            // skip nodes whose fanins are not divisors
             Abc_ObjForEachFanin( pFanout, pFanin, m )
-                if ( !pFanin->fMarkA )
+                if ( !Abc_NodeIsTravIdPrevious(pFanin) )
                     break;
             if ( m < Abc_ObjFaninNum(pFanout) )
                 continue;
-            // add the node
-            Res_WinAddNode( p, pFanout );
+            // add the node to the divisors
+            Vec_PtrPush( p->vDivs, pFanout );
+            Vec_PtrPush( p->vNodes, pFanout );
+            Abc_NodeSetTravIdPrevious( pFanout );
             p->nDivsPlus++;
         }
     }
+}
 
-    // unmark the leaves and the internal nodes
-    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
-        pObj->fMarkA = 0;
-    Vec_VecForEachEntry( p->vLevels, pObj, i, k )
-        pObj->fMarkA = 0;
+/**Function*************************************************************
 
-    // collect the divisors below the line
-    Vec_PtrClear( p->vDivs );
-    // collect the node fanins first and mark the fanins
-    Abc_ObjForEachFanin( p->pNode, pFanin, m )
-    {
-        Vec_PtrPush( p->vDivs, pFanin );
-        Abc_NodeSetTravIdCurrent( pFanin );
-    }
-    // collect the remaining leaves
+  Synopsis    [Marks the TFI cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinMarkTfi_rec( Res_Win_t * p, Abc_Obj_t * pObj )
+{
+    Abc_Obj_t * pFanin;
+    int i;
+    if ( Abc_NodeIsTravIdCurrent(pObj) )
+        return;
+    Abc_NodeSetTravIdCurrent( pObj );
+    assert( Abc_ObjIsNode(pObj) );
+    // visit the fanins of the node
+    Abc_ObjForEachFanin( pObj, pFanin, i )
+        Res_WinMarkTfi_rec( p, pFanin );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFI cone of the node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinMarkTfi( Res_Win_t * p )
+{
+    Abc_Obj_t * pObj;
+    int i;
+    // mark the leaves
     Vec_PtrForEachEntry( p->vLeaves, pObj, i )
-        if ( !Abc_NodeIsTravIdCurrent(pObj) )
-            Vec_PtrPush( p->vDivs, pObj );
-    // collect remaining unvisited divisors 
-    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->nLevLeaves, p->nLevDivMax )
-        if ( !Abc_NodeIsTravIdCurrent(pObj) )
-            Vec_PtrPush( p->vDivs, pObj );
-
-    // verify the resulting window
-//    Res_WinVerify( p );
+        Abc_NodeSetTravIdCurrent( pObj );
+    // start from the node
+    Res_WinMarkTfi_rec( p, p->pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the TFO of the collected nodes up to the given level.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit )
+{
+    Abc_Obj_t * pFanout;
+    int i;
+    if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit )
+        return;
+    if ( Abc_NodeIsTravIdCurrent(pObj) )
+        return;
+    Abc_NodeSetTravIdCurrent( pObj );
+    Abc_ObjForEachFanout( pObj, pFanout, i )
+        Res_WinSweepLeafTfo_rec( pFanout, nLevelLimit );
 }
 
 /**Function*************************************************************
diff --git a/src/opt/res/resFilter.c b/src/opt/res/resFilter.c
index 4f1be833..38f64815 100644
--- a/src/opt/res/resFilter.c
+++ b/src/opt/res/resFilter.c
@@ -42,7 +42,7 @@ static unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim
   SeeAlso     []
 
 ***********************************************************************/
-int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs )
+int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW )
 {
     Abc_Obj_t * pFanin, * pFanin2;
     unsigned * pInfo;
@@ -52,18 +52,19 @@ int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim,
     pInfo = Vec_PtrEntry( pSim->vOuts, 1 );
     RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
     if ( RetValue == 0 )
-        printf( "Failed 1!" );
+        printf( "Failed 1!\n" );
 
     // collect the fanin info
     pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 );
     RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
     if ( RetValue == 0 )
-        printf( "Failed 2!" );
+        printf( "Failed 2!\n" );
 
     // try removing fanins
 //    printf( "Fanins: " );
     Counter = 0;
     Vec_VecClear( vResubs );
+    Vec_VecClear( vResubsW );
     Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
     {
         pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) );
@@ -78,7 +79,10 @@ int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim,
             Abc_ObjForEachFanin( pWin->pNode, pFanin2, k )
             {
                 if ( k != i )
+                {
                     Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
+                    Vec_VecPush( vResubsW, Counter, pFanin2 );
+                }
             }
             Counter++;
         }
diff --git a/src/opt/res/resInt.h b/src/opt/res/resInt.h
index 54251722..9d17cb1c 100644
--- a/src/opt/res/resInt.h
+++ b/src/opt/res/resInt.h
@@ -42,49 +42,48 @@ extern "C" {
 typedef struct Res_Win_t_ Res_Win_t;
 struct Res_Win_t_
 {
-    // the general data
-    int              nWinTfiMax; // the fanin levels
-    int              nWinTfoMax; // the fanout levels
-    int              nLevLeaves; // the level where leaves begin
-    int              nLevDivMax; // the maximum divisor level
-    int              nDivsPlus;  // the number of additional divisors
-    int              nLeavesPlus;// the number of additional leaves
-    Abc_Obj_t *      pNode;      // the node in the center
+    // windowing parameters
+    Abc_Obj_t *      pNode;        // the node in the center
+    int              nWinTfiMax;   // the fanin levels
+    int              nWinTfoMax;   // the fanout levels
+    int              nLevDivMax;   // the maximum divisor level
+    // internal windowing parameters
+    int              nFanoutLimit; // the limit on the fanout count of a TFO node (if more, the node is treated as a root)
+    int              nLevTfiMinus; // the number of additional levels to search from TFO below the level of leaves
+    // derived windowing parameters
+    int              nLevLeafMin;  // the minimum level of a leaf
+    int              nLevTravMin;  // the minimum level to search from TFO
+    int              nDivsPlus;    // the number of additional divisors
     // the window data
-    Vec_Vec_t *      vLevels;    // nodes by level
-    Vec_Ptr_t *      vLeaves;    // leaves of the window
-    Vec_Ptr_t *      vRoots;     // roots of the window
-    Vec_Ptr_t *      vDivs;      // the candidate divisors of the node
+    Vec_Ptr_t *      vRoots;       // outputs of the window
+    Vec_Ptr_t *      vLeaves;      // inputs of the window
+    Vec_Ptr_t *      vBranches;    // side nodes of the window
+    Vec_Ptr_t *      vNodes;       // internal nodes of the window
+    Vec_Ptr_t *      vDivs;        // candidate divisors of the node
+    // temporary data
+    Vec_Vec_t *      vMatrix;      // TFI nodes below the given node
 };
 
 typedef struct Res_Sim_t_ Res_Sim_t;
 struct Res_Sim_t_
 {
-    Abc_Ntk_t *      pAig;       // AIG for simulation
+    Abc_Ntk_t *      pAig;         // AIG for simulation
     // simulation parameters
-    int              nWords;     // the number of simulation words
-    int              nPats;      // the number of patterns
-    int              nWordsOut;  // the number of simulation words in the output patterns
-    int              nPatsOut;   // the number of patterns in the output patterns 
+    int              nWords;       // the number of simulation words
+    int              nPats;        // the number of patterns
+    int              nWordsOut;    // the number of simulation words in the output patterns
+    int              nPatsOut;     // the number of patterns in the output patterns 
     // simulation info
-    Vec_Ptr_t *      vPats;      // input simulation patterns
-    Vec_Ptr_t *      vPats0;     // input simulation patterns
-    Vec_Ptr_t *      vPats1;     // input simulation patterns
-    Vec_Ptr_t *      vOuts;      // output simulation info
-    int              nPats0;     // the number of 0-patterns accumulated
-    int              nPats1;     // the number of 1-patterns accumulated
+    Vec_Ptr_t *      vPats;        // input simulation patterns
+    Vec_Ptr_t *      vPats0;       // input simulation patterns
+    Vec_Ptr_t *      vPats1;       // input simulation patterns
+    Vec_Ptr_t *      vOuts;        // output simulation info
+    int              nPats0;       // the number of 0-patterns accumulated
+    int              nPats1;       // the number of 1-patterns accumulated
     // resub candidates
-    Vec_Vec_t *      vCands;     // resubstitution candidates
+    Vec_Vec_t *      vCands;       // resubstitution candidates
 };
 
-// adds one node to the window
-static inline void Res_WinAddNode( Res_Win_t * p, Abc_Obj_t * pObj )
-{
-    assert( !pObj->fMarkA );
-    pObj->fMarkA = 1;
-    Vec_VecPush( p->vLevels, pObj->Level, pObj );
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -95,11 +94,12 @@ static inline void Res_WinAddNode( Res_Win_t * p, Abc_Obj_t * pObj )
 
 /*=== resDivs.c ==========================================================*/
 extern void          Res_WinDivisors( Res_Win_t * p, int nLevDivMax );
-extern int           Res_WinVisitMffc( Res_Win_t * p );
+extern void          Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit );
 /*=== resFilter.c ==========================================================*/
-extern int           Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs );
+extern int           Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs, Vec_Vec_t * vResubsW );
 /*=== resSat.c ==========================================================*/
 extern void *        Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins );
+extern void *        Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins );
 /*=== resSim.c ==========================================================*/
 extern Res_Sim_t *   Res_SimAlloc( int nWords );
 extern void          Res_SimFree( Res_Sim_t * p );
@@ -111,7 +111,7 @@ extern void          Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, H
 /*=== resWnd.c ==========================================================*/
 extern Res_Win_t *   Res_WinAlloc();
 extern void          Res_WinFree( Res_Win_t * p );
-extern void          Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNode );
+extern int           Res_WinIsTrivial( Res_Win_t * p );
 extern int           Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p );
 
 
diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c
index ec609445..f9558c97 100644
--- a/src/opt/res/resSat.c
+++ b/src/opt/res/resSat.c
@@ -37,7 +37,7 @@ extern int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int
 
 /**Function*************************************************************
 
-  Synopsis    [Loads AIG into the SAT solver.]
+  Synopsis    [Loads AIG into the SAT solver for checking resubstitution.]
 
   Description []
                
@@ -126,6 +126,66 @@ void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
 
 /**Function*************************************************************
 
+  Synopsis    [Loads AIG into the SAT solver for constrained simulation.]
+
+  Description [The array of fanins contains exactly two entries: the 
+  care set and the functions.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void * Res_SatSimulateConstr( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
+{
+    sat_solver * pSat;
+    Vec_Ptr_t * vNodes;
+    Abc_Obj_t * pObj;
+    int i, nNodes;
+
+    // make sure fanins contain POs of the AIG
+    pObj = Vec_PtrEntry( vFanins, 0 );
+    assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) );
+    assert( Vec_PtrSize(vFanins) == 2 );
+
+    // collect reachable nodes
+    vNodes = Abc_NtkDfsNodes( pAig, (Abc_Obj_t **)vFanins->pArray, vFanins->nSize );
+
+    // assign unique numbers to each node
+    nNodes = 0;
+    Abc_AigConst1(pAig)->pCopy = (void *)nNodes++;
+    Abc_NtkForEachPi( pAig, pObj, i )
+        pObj->pCopy = (void *)nNodes++;
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        pObj->pCopy = (void *)nNodes++;
+    Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs
+        pObj->pCopy = (void *)nNodes++;
+
+    // start the solver
+    pSat = sat_solver_new();
+
+    // add clause for the constant node
+    Res_SatAddConst1( pSat, (int)Abc_AigConst1(pAig)->pCopy, 0 );
+    // add clauses for AND gates
+    Vec_PtrForEachEntry( vNodes, pObj, i )
+        Res_SatAddAnd( pSat, (int)pObj->pCopy, 
+            (int)Abc_ObjFanin0(pObj)->pCopy, (int)Abc_ObjFanin1(pObj)->pCopy, Abc_ObjFaninC0(pObj), Abc_ObjFaninC1(pObj) );
+    Vec_PtrFree( vNodes );
+    // add clauses for POs
+    Vec_PtrForEachEntry( vFanins, pObj, i )
+        Res_SatAddEqual( pSat, (int)pObj->pCopy, 
+            (int)Abc_ObjFanin0(pObj)->pCopy, Abc_ObjFaninC0(pObj) );
+
+    // add trivial clauses
+    pObj = Vec_PtrEntry(vFanins, 0);
+    Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // care-set
+    pObj = Vec_PtrEntry(vFanins, 1);
+    Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // on-set
+    return pSat;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Asserts equality of the variable to a constant.]
 
   Description []
diff --git a/src/opt/res/resSim.c b/src/opt/res/resSim.c
index 81267540..cc896ec0 100644
--- a/src/opt/res/resSim.c
+++ b/src/opt/res/resSim.c
@@ -484,13 +484,13 @@ int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig )
         Res_SimProcessPats( p );
         if ( !(p->nPats0 < p->nPats || p->nPats1 < p->nPats) )
             break;
-
     }
 //    printf( "%d   ", Limit );
     // report the last set of patterns
-    Res_SimReportOne( p );
-    printf( "\n" );
+//    Res_SimReportOne( p );
+//    printf( "\n" );
     // quit if there is not enough
+//    if ( p->nPats0 < 4 || p->nPats1 < 4 )
     if ( p->nPats0 < 4 || p->nPats1 < 4 )
     {
 //        Res_SimReportOne( p );
diff --git a/src/opt/res/resStrash.c b/src/opt/res/resStrash.c
index d3a8efa8..fde842a4 100644
--- a/src/opt/res/resStrash.c
+++ b/src/opt/res/resStrash.c
@@ -48,22 +48,25 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
     Vec_Ptr_t * vPairs;
     Abc_Ntk_t * pAig;
     Abc_Obj_t * pObj, * pMiter;
-    int i, k;
+    int i;
     assert( Abc_NtkHasAig(p->pNode->pNtk) );
+//    Abc_NtkCleanCopy( p->pNode->pNtk );
     // create the network
     pAig = Abc_NtkAlloc( ABC_NTK_STRASH, ABC_FUNC_AIG, 1 );
     pAig->pName = Extra_UtilStrsav( "window" );
     // create the inputs
     Vec_PtrForEachEntry( p->vLeaves, pObj, i )
         pObj->pCopy = Abc_NtkCreatePi( pAig );
+    Vec_PtrForEachEntry( p->vBranches, pObj, i )
+        pObj->pCopy = Abc_NtkCreatePi( pAig );
     // go through the nodes in the topological order
-    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->nLevLeaves + 1, (int)p->pNode->Level + p->nWinTfoMax )
+    Vec_PtrForEachEntry( p->vNodes, pObj, i )
     {
         pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj );
         if ( pObj == p->pNode )
             pObj->pCopy = Abc_ObjNot( pObj->pCopy );
     }
-    // collect the PO outputs
+    // collect the POs
     vPairs = Vec_PtrAlloc( 2 * Vec_PtrSize(p->vRoots) );
     Vec_PtrForEachEntry( p->vRoots, pObj, i )
     {
@@ -72,15 +75,17 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
     }
     // mark the TFO of the node
     Abc_NtkIncrementTravId( p->pNode->pNtk );
-    Res_WinSweepLeafTfo_rec( p->pNode, (int)p->pNode->Level + p->nWinTfoMax, NULL );
-    // redo strashing in the TFO
+    Res_WinSweepLeafTfo_rec( p->pNode, (int)p->pNode->Level + p->nWinTfoMax );
+    // update strashing of the node
     p->pNode->pCopy = Abc_ObjNot( p->pNode->pCopy );
-    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->pNode->Level + 1, (int)p->pNode->Level + p->nWinTfoMax )
+    Abc_NodeSetTravIdPrevious( p->pNode );
+    // redo strashing in the TFO
+    Vec_PtrForEachEntry( p->vNodes, pObj, i )
     {
         if ( Abc_NodeIsTravIdCurrent(pObj) )
             pObj->pCopy = Abc_ConvertAigToAig( pAig, pObj );
     }
-    // collect the PO outputs
+    // collect the POs
     Vec_PtrForEachEntry( p->vRoots, pObj, i )
         Vec_PtrWriteEntry( vPairs, 2 * i + 1, pObj->pCopy );
     // add the miter
@@ -89,6 +94,9 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
     Vec_PtrFree( vPairs );
     // add the node
     Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), p->pNode->pCopy );
+    // add the fanins
+    Abc_ObjForEachFanin( p->pNode, pObj, i )
+        Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy );
     // add the divisors
     Vec_PtrForEachEntry( p->vDivs, pObj, i )
         Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy );
diff --git a/src/opt/res/resUpdate.c b/src/opt/res/resUpdate.c
index 06704b1c..01400ead 100644
--- a/src/opt/res/resUpdate.c
+++ b/src/opt/res/resUpdate.c
@@ -45,11 +45,11 @@ static int Res_UpdateNetworkLevelNew( Abc_Obj_t * pObj );
 void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels )
 {
     Abc_Obj_t * pObjNew, * pFanin, * pFanout, * pTemp;
-    int i, k, m;
+    int Lev, k, m;
     // create the new node
     pObjNew = Abc_NtkCreateNode( pObj->pNtk );
     pObjNew->pData = pFunc;
-    Vec_PtrForEachEntry( vFanins, pFanin, i )
+    Vec_PtrForEachEntry( vFanins, pFanin, k )
         Abc_ObjAddFanin( pObjNew, pFanin );
     // replace the old node by the new node
     pObjNew->Level = pObj->Level;
@@ -62,12 +62,12 @@ void Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc
     Vec_VecPush( vLevels, pObjNew->Level, pObjNew );
     pObjNew->fMarkA = 1;
     // recursively update level
-    Vec_VecForEachEntryStart( vLevels, pTemp, i, k, pObjNew->Level )
+    Vec_VecForEachEntryStart( vLevels, pTemp, Lev, k, pObjNew->Level )
     {
         pTemp->fMarkA = 0;
         pTemp->Level = Res_UpdateNetworkLevelNew( pTemp );
         // if the level did not change, to need to check the fanout levels
-        if ( (int)pTemp->Level == i )
+        if ( (int)pTemp->Level == Lev )
             continue;
         // schedule fanout for level update
         Abc_ObjForEachFanout( pTemp, pFanout, m )
diff --git a/src/opt/res/resWin.c b/src/opt/res/resWin.c
index fa74b219..80a65ea8 100644
--- a/src/opt/res/resWin.c
+++ b/src/opt/res/resWin.c
@@ -43,12 +43,19 @@
 Res_Win_t * Res_WinAlloc()
 {
     Res_Win_t * p;
+    // start the manager
     p = ALLOC( Res_Win_t, 1 );
     memset( p, 0, sizeof(Res_Win_t) );
-    p->vLevels = Vec_VecStart( 128 );
-    p->vLeaves = Vec_PtrAlloc( 512 );
-    p->vRoots  = Vec_PtrAlloc( 512 );
-    p->vDivs   = Vec_PtrAlloc( 512 );
+    // set internal parameters
+    p->nFanoutLimit = 10;
+    p->nLevTfiMinus =  3;
+    // allocate storage
+    p->vRoots    = Vec_PtrAlloc( 256 );
+    p->vLeaves   = Vec_PtrAlloc( 256 );
+    p->vBranches = Vec_PtrAlloc( 256 );
+    p->vNodes    = Vec_PtrAlloc( 256 );
+    p->vDivs     = Vec_PtrAlloc( 256 );
+    p->vMatrix   = Vec_VecStart( 128 );
     return p;
 }
 
@@ -65,48 +72,87 @@ Res_Win_t * Res_WinAlloc()
 ***********************************************************************/
 void Res_WinFree( Res_Win_t * p )
 {
-    Vec_VecFree( p->vLevels );
-    Vec_PtrFree( p->vLeaves );
     Vec_PtrFree( p->vRoots  );
+    Vec_PtrFree( p->vLeaves );
+    Vec_PtrFree( p->vBranches );
+    Vec_PtrFree( p->vNodes  );
     Vec_PtrFree( p->vDivs   );
+    Vec_VecFree( p->vMatrix );
     free( p );
 }
 
+
+
 /**Function*************************************************************
 
-  Synopsis    [Collects nodes in the limited TFI of the node.]
+  Synopsis    [Collect the limited TFI cone of the node.]
 
-  Description [Marks the collected nodes.]
+  Description []
                
   SideEffects []
 
   SeeAlso     []
 
 ***********************************************************************/
-void Res_WinCollectNodeTfi( Res_Win_t * p )
+void Res_WinCollectLeavesAndNodes( Res_Win_t * p )
 {
     Vec_Ptr_t * vFront;
-    Abc_Obj_t * pObj, * pFanin;
+    Abc_Obj_t * pObj, * pTemp;
     int i, k, m;
-    // expand storage for levels
-    if ( Vec_VecSize( p->vLevels ) <= (int)p->pNode->Level + p->nWinTfoMax )
-        Vec_VecExpand( p->vLevels, (int)p->pNode->Level + p->nWinTfoMax );
-    // start the frontier
-    Vec_VecClear( p->vLevels );
-    Res_WinAddNode( p, p->pNode );
-    // add one level at a time
-    Vec_VecForEachLevelReverseStartStop( p->vLevels, vFront, i, p->pNode->Level, p->nLevLeaves + 1 )
+
+    assert( p->nWinTfiMax > 0 );
+    assert( Vec_VecSize(p->vMatrix) > p->nWinTfiMax );
+
+    // start matrix with the node
+    Vec_VecClear( p->vMatrix );
+    Vec_VecPush( p->vMatrix, 0, p->pNode );
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
+    Abc_NodeSetTravIdCurrent( p->pNode );
+
+    // collect the leaves (nodes pTemp such that "p->pNode->Level - pTemp->Level > p->nWinTfiMax")
+    Vec_PtrClear( p->vLeaves );
+    Vec_VecForEachLevelStartStop( p->vMatrix, vFront, i, 0, p->nWinTfiMax )
     {
         Vec_PtrForEachEntry( vFront, pObj, k )
-            Abc_ObjForEachFanin( pObj, pFanin, m )
-                if ( !pFanin->fMarkA )
-                    Res_WinAddNode( p, pFanin );
+        {
+            Abc_ObjForEachFanin( pObj, pTemp, m )
+            {
+                if ( Abc_NodeIsTravIdCurrent( pTemp ) )
+                    continue;
+                Abc_NodeSetTravIdCurrent( pTemp );
+                if ( Abc_ObjIsCi(pTemp) || (int)(p->pNode->Level - pTemp->Level) > p->nWinTfiMax )                    
+                    Vec_PtrPush( p->vLeaves, pTemp );
+                else
+                    Vec_VecPush( p->vMatrix, p->pNode->Level - pTemp->Level, pTemp );
+            }
+        }
     }
+    assert( Vec_PtrSize(p->vLeaves) > 0 );
+
+    // collect the nodes in the reverse order
+    Vec_PtrClear( p->vNodes );
+    Vec_VecForEachLevelReverseStartStop( p->vMatrix, vFront, i, p->nWinTfiMax, 0 )
+    {
+        Vec_PtrForEachEntry( vFront, pObj, k )
+            Vec_PtrPush( p->vNodes, pObj );
+        Vec_PtrClear( vFront );
+    }
+
+    // get the lowest leaf level
+    p->nLevLeafMin = ABC_INFINITY;
+    Vec_PtrForEachEntry( p->vLeaves, pObj, k )
+        p->nLevLeafMin = ABC_MIN( p->nLevLeafMin, (int)pObj->Level );
+
+    // set minimum traversal level
+    p->nLevTravMin = ABC_MAX( ((int)p->pNode->Level) - p->nWinTfiMax - p->nLevTfiMinus, p->nLevLeafMin );
+    assert( p->nLevTravMin >= 0 );
 }
 
+
+
 /**Function*************************************************************
 
-  Synopsis    [Collect all the nodes that fanin into the window nodes.]
+  Synopsis    [Returns 1 if the node should be a root.]
 
   Description []
                
@@ -115,24 +161,25 @@ void Res_WinCollectNodeTfi( Res_Win_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Res_WinCollectLeaves( Res_Win_t * p )
+static inline int Res_WinComputeRootsCheck( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit )
 {
-    Vec_Ptr_t * vLevel;
-    Abc_Obj_t * pObj;
-    int i, k;
-    // add the leaves
-    Vec_PtrClear( p->vLeaves );
-    // collect the nodes below the given level
-    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevLeaves )
-        Vec_PtrPush( p->vLeaves, pObj );
-    // remove leaves from the set
-    Vec_VecForEachLevelStartStop( p->vLevels, vLevel, i, 0, p->nLevLeaves )
-        Vec_PtrClear( vLevel );
+    Abc_Obj_t * pFanout;
+    int i;
+    // the node is the root if one of the following is true:
+    // (1) the node has more than fanouts than the limit
+    if ( Abc_ObjFanoutNum(pNode) > nFanoutLimit )
+        return 1;
+    // (2) the node has CO fanouts
+    // (3) the node has fanouts above the cutoff level
+    Abc_ObjForEachFanout( pNode, pFanout, i )
+        if ( Abc_ObjIsCo(pFanout) || (int)pFanout->Level > nLevelMax )
+            return 1;
+    return 0;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Marks the TFO of the collected nodes up to the given level.]
+  Synopsis    [Recursively collects the root candidates.]
 
   Description []
                
@@ -141,22 +188,85 @@ void Res_WinCollectLeaves( Res_Win_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNode )
+void Res_WinComputeRoots_rec( Abc_Obj_t * pNode, int nLevelMax, int nFanoutLimit, Vec_Ptr_t * vRoots )
 {
     Abc_Obj_t * pFanout;
     int i;
-    if ( Abc_ObjIsCo(pObj) || (int)pObj->Level > nLevelLimit || pObj == pNode )
-        return;
-    if ( Abc_NodeIsTravIdCurrent(pObj) )
+    assert( Abc_ObjIsNode(pNode) );
+    if ( Abc_NodeIsTravIdCurrent(pNode) )
         return;
-    Abc_NodeSetTravIdCurrent( pObj );
-    Abc_ObjForEachFanout( pObj, pFanout, i )
-        Res_WinSweepLeafTfo_rec( pFanout, nLevelLimit, pNode );
+    Abc_NodeSetTravIdCurrent( pNode );
+    // check if the node should be the root
+    if ( Res_WinComputeRootsCheck( pNode, nLevelMax, nFanoutLimit ) )
+        Vec_PtrPush( vRoots, pNode );
+    else // if not, explore its fanouts
+        Abc_ObjForEachFanout( pNode, pFanout, i )
+            Res_WinComputeRoots_rec( pFanout, nLevelMax, nFanoutLimit, vRoots );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recursively collects the root candidates.]
+
+  Description [Returns 1 if the only root is this node.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_WinComputeRoots( Res_Win_t * p )
+{
+    Vec_PtrClear( p->vRoots );
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
+    Res_WinComputeRoots_rec( p->pNode, p->pNode->Level + p->nWinTfoMax, p->nFanoutLimit, p->vRoots );
+    assert( Vec_PtrSize(p->vRoots) > 0 );
+    if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode )
+        return 0;
+    return 1;
+}
+
+
+
+/**Function*************************************************************
+
+  Synopsis    [Marks the paths from the roots to the leaves.]
+
+  Description [Returns 1 if the the node can reach a leaf.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Res_WinMarkPaths_rec( Abc_Obj_t * pNode, Abc_Obj_t * pPivot, int nLevelMin )
+{
+    Abc_Obj_t * pFanin;
+    int i, RetValue;
+    // skip visited nodes
+    if ( Abc_NodeIsTravIdCurrent(pNode) )
+        return 1;
+    if ( Abc_NodeIsTravIdPrevious(pNode) )
+        return 0;
+    // assume that the node does not have access to the leaves
+    Abc_NodeSetTravIdPrevious( pNode );
+    // skip nodes below the given level
+    if ( pNode == pPivot || (int)pNode->Level <= nLevelMin )
+        return 0;
+    assert( Abc_ObjIsNode(pNode) );
+    // check if the fanins have access to the leaves
+    RetValue = 0;
+    Abc_ObjForEachFanin( pNode, pFanin, i )
+        RetValue |= Res_WinMarkPaths_rec( pFanin, pPivot, nLevelMin );
+    // relabel the node if it has access to the leaves
+    if ( RetValue )
+        Abc_NodeSetTravIdCurrent( pNode );
+    return RetValue;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Marks the TFO of the collected nodes up to the given level.]
+  Synopsis    [Marks the paths from the roots to the leaves.]
 
   Description []
                
@@ -165,15 +275,25 @@ void Res_WinSweepLeafTfo_rec( Abc_Obj_t * pObj, int nLevelLimit, Abc_Obj_t * pNo
   SeeAlso     []
 
 ***********************************************************************/
-void Res_WinSweepLeafTfo( Res_Win_t * p )
+void Res_WinMarkPaths( Res_Win_t * p )
 {
     Abc_Obj_t * pObj;
     int i;
+    // mark the leaves
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
     Abc_NtkIncrementTravId( p->pNode->pNtk );
     Vec_PtrForEachEntry( p->vLeaves, pObj, i )
-        Res_WinSweepLeafTfo_rec( pObj, p->pNode->Level + p->nWinTfoMax, p->pNode );
+        Abc_NodeSetTravIdCurrent( pObj );
+    // traverse from the roots and mark the nodes that can reach leaves
+    // the nodes that do not reach leaves have previous trav ID
+    // the nodes that reach leaves have current trav ID
+    Vec_PtrForEachEntry( p->vRoots, pObj, i )
+        Res_WinMarkPaths_rec( pObj, p->pNode, p->nLevTravMin );
 }
 
+
+
+
 /**Function*************************************************************
 
   Synopsis    [Recursively collects the roots.]
@@ -185,29 +305,27 @@ void Res_WinSweepLeafTfo( Res_Win_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Res_WinCollectRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots )
+void Res_WinFinalizeRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots )
 {
     Abc_Obj_t * pFanout;
     int i;
     assert( Abc_ObjIsNode(pObj) );
+    assert( Abc_NodeIsTravIdCurrent(pObj) );
     // check if the node has all fanouts marked
     Abc_ObjForEachFanout( pObj, pFanout, i )
         if ( !Abc_NodeIsTravIdCurrent(pFanout) )
             break;
-    // if some of the fanouts are unmarked, add the node to the root
+    // if some of the fanouts are unmarked, add the node to the roots
     if ( i < Abc_ObjFanoutNum(pObj) ) 
-    {
         Vec_PtrPushUnique( vRoots, pObj );
-        return;
-    }
-    // otherwise, call recursively
-    Abc_ObjForEachFanout( pObj, pFanout, i )
-        Res_WinCollectRoots_rec( pFanout, vRoots );
+    else  // otherwise, call recursively
+        Abc_ObjForEachFanout( pObj, pFanout, i )
+            Res_WinFinalizeRoots_rec( pFanout, vRoots );
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Collects the roots of the window.]
+  Synopsis    [Finalizes the roots of the window.]
 
   Description [Roots of the window are the nodes that have at least
   one fanout that it not in the TFO of the leaves.]
@@ -217,13 +335,21 @@ void Res_WinCollectRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots )
   SeeAlso     []
 
 ***********************************************************************/
-void Res_WinCollectRoots( Res_Win_t * p )
+int Res_WinFinalizeRoots( Res_Win_t * p )
 {
     assert( !Abc_NodeIsTravIdCurrent(p->pNode) );
+    // mark the node with the old traversal ID
+    Abc_NodeSetTravIdCurrent( p->pNode ); 
+    // recollect the roots
     Vec_PtrClear( p->vRoots );
-    Res_WinCollectRoots_rec( p->pNode, p->vRoots );
+    Res_WinFinalizeRoots_rec( p->pNode, p->vRoots );
+    assert( Vec_PtrSize(p->vRoots) > 0 );
+    if ( Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode )
+        return 0;
+    return 1;
 }
 
+
 /**Function*************************************************************
 
   Synopsis    [Recursively adds missing nodes and leaves.]
@@ -235,23 +361,27 @@ void Res_WinCollectRoots( Res_Win_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj )
+void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj, int nLevTravMin )
 {
     Abc_Obj_t * pFanin;
     int i;
-    if ( pObj->fMarkA )
+    // skip the already collected leaves, nodes, and branches
+    if ( Abc_NodeIsTravIdCurrent(pObj) )
         return;
-    if ( !Abc_NodeIsTravIdCurrent(pObj) || (int)pObj->Level <= p->nLevLeaves )
+    // if this is not an internal node - make it a new branch
+    if ( !Abc_NodeIsTravIdPrevious(pObj) )
     {
-        p->nLeavesPlus++;
-        Vec_PtrPush( p->vLeaves, pObj );
-        pObj->fMarkA = 1;
+        Abc_NodeSetTravIdCurrent( pObj );
+        Vec_PtrPush( p->vBranches, pObj );
         return;
     }
-    Res_WinAddNode( p, pObj );
+    assert( Abc_ObjIsNode(pObj) ); // if this is a CI, then the window is incorrect!
+    Abc_NodeSetTravIdCurrent( pObj );
     // visit the fanins of the node
     Abc_ObjForEachFanin( pObj, pFanin, i )
-        Res_WinAddMissing_rec( p, pFanin );
+        Res_WinAddMissing_rec( p, pFanin, nLevTravMin );
+    // collect the node
+    Vec_PtrPush( p->vNodes, pObj );
 }
 
 /**Function*************************************************************
@@ -269,34 +399,25 @@ void Res_WinAddMissing( Res_Win_t * p )
 {
     Abc_Obj_t * pObj;
     int i;
+    // mark the leaves
+    Abc_NtkIncrementTravId( p->pNode->pNtk );
+    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
+        Abc_NodeSetTravIdCurrent( pObj );        
+    // mark the already collected nodes
+    Vec_PtrForEachEntry( p->vNodes, pObj, i )
+        Abc_NodeSetTravIdCurrent( pObj );        
+    // explore from the roots
+    Vec_PtrClear( p->vBranches );
     Vec_PtrForEachEntry( p->vRoots, pObj, i )
-        Res_WinAddMissing_rec( p, pObj );
+        Res_WinAddMissing_rec( p, pObj, p->nLevTravMin );
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Unmarks the leaves and nodes of the window.]
 
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Res_WinUnmark( Res_Win_t * p )
-{
-    Abc_Obj_t * pObj;
-    int i, k;
-    Vec_VecForEachEntry( p->vLevels, pObj, i, k )
-        pObj->fMarkA = 0;
-    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
-        pObj->fMarkA = 0;
-}
 
+ 
 /**Function*************************************************************
 
-  Synopsis    [Verifies the window.]
+  Synopsis    [Returns 1 if the window is trivial (without TFO).]
 
   Description []
                
@@ -305,30 +426,9 @@ void Res_WinUnmark( Res_Win_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Res_WinVerify( Res_Win_t * p )
+int Res_WinIsTrivial( Res_Win_t * p )
 {
-    Abc_Obj_t * pObj, * pFanin;
-    int i, k, f;
-    // make sure the nodes are not marked
-    Abc_NtkForEachObj( p->pNode->pNtk, pObj, i )
-        assert( !pObj->fMarkA );
-    // mark the leaves
-    Vec_PtrForEachEntry( p->vLeaves, pObj, i )
-        pObj->fMarkA = 1;
-    // make sure all nodes in the topological order have their fanins in the set
-    Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, p->nLevLeaves + 1, (int)p->pNode->Level + p->nWinTfoMax )
-    {
-        assert( (int)pObj->Level == i );
-        assert( !pObj->fMarkA );
-        Abc_ObjForEachFanin( pObj, pFanin, f )
-            assert( pFanin->fMarkA );
-        pObj->fMarkA = 1;
-    }
-    // make sure the roots are marked
-    Vec_PtrForEachEntry( p->vRoots, pObj, i )
-        assert( pObj->fMarkA );
-    // unmark 
-    Res_WinUnmark( p );
+    return Vec_PtrSize(p->vRoots) == 1 && Vec_PtrEntry(p->vRoots, 0) == p->pNode;
 }
 
 /**Function*************************************************************
@@ -345,31 +445,29 @@ void Res_WinVerify( Res_Win_t * p )
 int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p )
 {
     assert( Abc_ObjIsNode(pNode) );
-    assert( nWinTfiMax > 0 && nWinTfoMax > 0 );
+    assert( nWinTfiMax > 0 && nWinTfiMax < 10 );
+    assert( nWinTfoMax >= 0 && nWinTfoMax < 10 );
+
     // initialize the window
-    p->pNode = pNode;
+    p->pNode      = pNode;
     p->nWinTfiMax = nWinTfiMax;
     p->nWinTfoMax = nWinTfoMax;
-    p->nLeavesPlus = 0;
-    p->nLevLeaves = ABC_MAX( 0, ((int)p->pNode->Level) - p->nWinTfiMax - 1 );
-    // collect the nodes in TFI cone of pNode above the level of leaves (p->nLevLeaves)
-    Res_WinCollectNodeTfi( p );
-    // find the leaves of the window
-    Res_WinCollectLeaves( p );
-    // mark the TFO of the collected nodes up to the given level (p->pNode->Level + p->nWinTfoMax)
-    Res_WinSweepLeafTfo( p );
-    // find the roots of the window
-    Res_WinCollectRoots( p );
-    // add the nodes in the TFI of the roots that are not yet in the window
-    Res_WinAddMissing( p );
-    // unmark window nodes
-    Res_WinUnmark( p );
-    // clear the divisor information
-    p->nLevDivMax = 0;
-    p->nDivsPlus = 0;
-    Vec_PtrClear( p->vDivs );
-    // verify the resulting window
-//    Res_WinVerify( p );
+    Vec_PtrClear( p->vRoots );
+    Vec_PtrPush( p->vRoots, pNode );
+
+    // compute the leaves
+    Res_WinCollectLeavesAndNodes( p );
+
+    // compute the candidate roots
+    if ( p->nWinTfoMax > 0 && Res_WinComputeRoots(p) )
+    {
+        // mark the paths from the roots to the leaves
+        Res_WinMarkPaths( p );
+        // refine the roots and add branches and missing nodes
+        if ( Res_WinFinalizeRoots( p ) )
+            Res_WinAddMissing( p );
+    }
+
     return 1;
 }
 
diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c
index 32a011b9..b52cd6c7 100644
--- a/src/sat/bsat/satInter.c
+++ b/src/sat/bsat/satInter.c
@@ -771,7 +771,8 @@ int Int_ManProofRecordOne( Int_Man_t * p, Sto_Cls_t * pClause )
     {
         // construct the proof
         Int_ManProofTraceOne( p, pConflict, p->pCnf->pEmpty );
-        printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id );
+        if ( p->fVerbose )
+            printf( "Found last conflict after adding unit clause number %d!\n", pClause->Id );
         return 0;
     }
 
@@ -827,7 +828,7 @@ int Int_ManProcessRoots( Int_Man_t * p )
         if ( !Int_ManEnqueue( p, pClause->pLits[0], pClause ) )
         {
             // detected root level conflict
-            printf( "Int_ManProcessRoots(): Detected a root-level conflict\n" );
+            printf( "Error in Int_ManProcessRoots(): Detected a root-level conflict too early!\n" );
             assert( 0 );
             return 0;
         }
@@ -838,8 +839,9 @@ int Int_ManProcessRoots( Int_Man_t * p )
     if ( pClause )
     {
         // detected root level conflict
-        printf( "Int_ManProcessRoots(): Detected a root-level conflict\n" );
-//        assert( 0 );
+        Int_ManProofTraceOne( p, pClause, p->pCnf->pEmpty );
+        if ( p->fVerbose )
+            printf( "Found root level conflict!\n" );
         return 0;
     }
 
@@ -925,17 +927,12 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned
     // check that the CNF makes sense
     assert( pCnf->nVars > 0 && pCnf->nClauses > 0 );
     p->pCnf = pCnf;
+    p->fVerbose = fVerbose;
+    *ppResult = NULL;
 
     // adjust the manager
     Int_ManResize( p );
 
-    // propagate root level assignments
-    if ( !Int_ManProcessRoots( p ) )
-    {
-        *ppResult = NULL;
-        return p->nVarsAB;
-    }
-
     // prepare the interpolant computation
     Int_ManPrepareInter( p );
 
@@ -951,15 +948,19 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned
     Sto_ManForEachClauseRoot( p->pCnf, pClause )
         Int_ManProofWriteOne( p, pClause );
 
-    // consider each learned clause
-    Sto_ManForEachClause( p->pCnf, pClause )
+    // propagate root level assignments
+    if ( Int_ManProcessRoots( p ) )
     {
-        if ( pClause->fRoot )
-            continue;
-        if ( !Int_ManProofRecordOne( p, pClause ) )
+        // if there is no conflict, consider learned clauses
+        Sto_ManForEachClause( p->pCnf, pClause )
         {
-            RetValue = 0;
-            break;
+            if ( pClause->fRoot )
+                continue;
+            if ( !Int_ManProofRecordOne( p, pClause ) )
+            {
+                RetValue = 0;
+                break;
+            }
         }
     }
 
@@ -970,12 +971,15 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned
         p->pFile = NULL;    
     }
 
+    if ( fVerbose )
+    {
     printf( "Vars = %d. Roots = %d. Learned = %d. Resol steps = %d.  Ave = %.2f.  Mem = %.2f Mb\n", 
         p->pCnf->nVars, p->pCnf->nRoots, p->pCnf->nClauses-p->pCnf->nRoots, p->Counter,  
         1.0*(p->Counter-p->pCnf->nRoots)/(p->pCnf->nClauses-p->pCnf->nRoots), 
         1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
-
 p->timeTotal += clock() - clkTotal;
+    }
+
     *ppResult = Int_ManTruthRead( p, p->pCnf->pTail );
     return p->nVarsAB;
 }
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 1756b5df..c4847be4 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1264,7 +1264,7 @@ void sat_solver_store_alloc( sat_solver * s )
 void sat_solver_store_write( sat_solver * s, char * pFileName )
 {
     extern void Sto_ManDumpClauses( void * p, char * pFileName );
-    Sto_ManDumpClauses( s->pStore, pFileName );
+    if ( s->pStore ) Sto_ManDumpClauses( s->pStore, pFileName );
 }
 
 void sat_solver_store_free( sat_solver * s )
@@ -1273,7 +1273,7 @@ void sat_solver_store_free( sat_solver * s )
     if ( s->pStore ) Sto_ManFree( s->pStore );
     s->pStore = NULL;
 }
-
+ 
 void sat_solver_store_mark_roots( sat_solver * s )
 {
     extern void Sto_ManMarkRoots( void * p );