Version abc70124

19 files changed, 677 insertions, 282 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index d843bca6..39360034 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -241,9 +241,9 @@ static inline unsigned    Abc_InfoRandom()                           { return ((
 static inline void        Abc_InfoClear( unsigned * p, int nWords )  { memset( p, 0, sizeof(unsigned) * nWords );   } 
 static inline void        Abc_InfoFill( unsigned * p, int nWords )   { memset( p, 0xff, sizeof(unsigned) * nWords );} 
 static inline void        Abc_InfoNot( unsigned * p, int nWords )    { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = ~p[i];   } 
-static inline int         Abc_InfoIsZero( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) if ( p[i] ) return 0; return 1;  } 
-static inline int         Abc_InfoIsOne( unsigned * p, int nWords )  { int i; for ( i = nWords - 1; i >= 0; i-- ) if ( !p[i] ) return 0; return 1; } 
-static inline void        Abc_InfoCopy( unsigned * p, unsigned * q, int nWords )  { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = q[i];   } 
+static inline int         Abc_InfoIsZero( unsigned * p, int nWords ) { int i; for ( i = nWords - 1; i >= 0; i-- ) if ( p[i] )  return 0; return 1; } 
+static inline int         Abc_InfoIsOne( unsigned * p, int nWords )  { int i; for ( i = nWords - 1; i >= 0; i-- ) if ( ~p[i] ) return 0; return 1; } 
+static inline void        Abc_InfoCopy( unsigned * p, unsigned * q, int nWords )  { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i]  = q[i];  } 
 static inline void        Abc_InfoAnd( unsigned * p, unsigned * q, int nWords )   { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &= q[i];  } 
 static inline void        Abc_InfoOr( unsigned * p, unsigned * q, int nWords )    { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= q[i];  } 
 static inline void        Abc_InfoXor( unsigned * p, unsigned * q, int nWords )   { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] ^= q[i];  } 
diff --git a/src/base/abc/abcFunc.c b/src/base/abc/abcFunc.c
index 421a64cf..5e13807a 100644
--- a/src/base/abc/abcFunc.c
+++ b/src/base/abc/abcFunc.c
@@ -830,10 +830,13 @@ Abc_Obj_t * Abc_ConvertAigToAig( Abc_Ntk_t * pNtkAig, Abc_Obj_t * pObjOld )
     pRoot = pObjOld->pData;
     // check the case of a constant
     if ( Hop_ObjIsConst1( Hop_Regular(pRoot) ) )
-        return Abc_ObjNotCond( Abc_AigConst1(pNtkAig->pManFunc), Hop_IsComplement(pRoot) );
+        return Abc_ObjNotCond( Abc_AigConst1(pNtkAig), Hop_IsComplement(pRoot) );
     // assign the fanin nodes
     Abc_ObjForEachFanin( pObjOld, pFanin, i )
+    {
+        assert( pFanin->pCopy != NULL );
         Hop_ManPi(pHopMan, i)->pData = pFanin->pCopy;
+    }
     // construct the AIG
     Abc_ConvertAigToAig_rec( pNtkAig, Hop_Regular(pRoot) );
     Hop_ConeUnmark_rec( Hop_Regular(pRoot) );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index a6552951..b20d2c8c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -25,6 +25,7 @@
 #include "cut.h"
 #include "fpga.h"
 #include "if.h"
+#include "res.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -2565,23 +2566,19 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
+    Res_Par_t Pars, * pPars = &Pars;
     int c;
-    int nWindow;
-    int nSimWords;
-    int fVerbose;
-    int fVeryVerbose;
-    // external functions
-    extern int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, int nWindow, int nSimWords, int fVerbose, int fVeryVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nWindow      = 33;
-    nSimWords    =  8;
-    fVerbose     =  1;
-    fVeryVerbose =  0;
+    pPars->nWindow      = 33;
+    pPars->nCands       =  3;
+    pPars->nSimWords    =  8;
+    pPars->fVerbose     =  1;
+    pPars->fVeryVerbose =  0;
     Extra_UtilGetoptReset();
     while ( ( c = Extra_UtilGetopt( argc, argv, "WSvwh" ) ) != EOF )
     {
@@ -2593,9 +2590,9 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-W\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nWindow = atoi(argv[globalUtilOptind]);
+            pPars->nWindow = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nWindow < 1 || nWindow > 99 ) 
+            if ( pPars->nWindow < 1 || pPars->nWindow > 99 ) 
                 goto usage;
             break;
         case 'S':
@@ -2604,16 +2601,16 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-S\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nSimWords = atoi(argv[globalUtilOptind]);
+            pPars->nSimWords = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nSimWords < 2 || nSimWords > 256 ) 
+            if ( pPars->nSimWords < 1 || pPars->nSimWords > 256 ) 
                 goto usage;
             break;
         case 'v':
-            fVerbose ^= 1;
+            pPars->fVerbose ^= 1;
             break;
         case 'w':
-            fVeryVerbose ^= 1;
+            pPars->fVeryVerbose ^= 1;
             break;
         case 'h':
             goto usage;
@@ -2634,7 +2631,7 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // modify the current network
-    if ( !Abc_NtkResynthesize( pNtk, nWindow, nSimWords, fVerbose, fVeryVerbose ) )
+    if ( !Abc_NtkResynthesize( pNtk, pPars ) )
     {
         fprintf( pErr, "Resynthesis has failed.\n" );
         return 1;
@@ -2642,13 +2639,13 @@ int Abc_CommandMfs( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: mfs [-W <NM>] [-S <n>] [-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", nWindow/10, nWindow%10 );
-    fprintf( pErr, "\t-S <n>  : specifies the number of simulation words (2 <= n <= 256) [default = %d]\n", nSimWords );
-    fprintf( pErr, "\t-v      : toggle verbose printout [default = %s]\n", fVerbose? "yes": "no" );
-    fprintf( pErr, "\t-w      : toggle printout subgraph statistics [default = %s]\n", fVeryVerbose? "yes": "no" );
-    fprintf( pErr, "\t-h      : print the command usage\n");
+    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-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");
     return 1;
 } 
 
diff --git a/src/opt/res/res.h b/src/opt/res/res.h
index 4a887741..fda35b89 100644
--- a/src/opt/res/res.h
+++ b/src/opt/res/res.h
@@ -37,50 +37,17 @@ extern "C" {
 ///                         BASIC TYPES                              ///
 ////////////////////////////////////////////////////////////////////////
 
-typedef struct Res_Win_t_ Res_Win_t;
-struct Res_Win_t_
+typedef struct Res_Par_t_ Res_Par_t;
+struct Res_Par_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
-    Abc_Obj_t *      pNode;      // the node in the center
-    // 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
+    // general parameters
+    int           nWindow;       // window size
+    int           nSimWords;     // the number of simulation words 
+    int           nCands;        // the number of candidates to try
+    int           fVerbose;      // enable basic stats
+    int           fVeryVerbose;  // enable detailed stats
 };
 
-typedef struct Res_Sim_t_ Res_Sim_t;
-struct Res_Sim_t_
-{
-    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 
-    // 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
-    // resub 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                           ///
 ////////////////////////////////////////////////////////////////////////
@@ -89,26 +56,8 @@ static inline void Res_WinAddNode( Res_Win_t * p, Abc_Obj_t * pObj )
 ///                    FUNCTION DECLARATIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
-/*=== resDivs.c ==========================================================*/
-extern void          Res_WinDivisors( Res_Win_t * p, int nLevDivMax );
-extern int           Res_WinVisitMffc( Res_Win_t * p );
-/*=== resFilter.c ==========================================================*/
-extern Vec_Vec_t *   Res_FilterCandidates( Res_Win_t * pWin, Res_Sim_t * pSim );
-/*=== resSat.c ==========================================================*/
-extern void *        Res_SatProveUnsat( 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 );
-extern int           Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig );
-/*=== resStrash.c ==========================================================*/
-extern Abc_Ntk_t *   Res_WndStrash( Res_Win_t * p );
-/*=== resWnd.c ==========================================================*/
-extern void          Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels );
-/*=== resWnd.c ==========================================================*/
-extern Res_Win_t *   Res_WinAlloc();
-extern void          Res_WinFree( Res_Win_t * p );
-extern int           Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p );
-extern void          Res_WinVisitNodeTfo( Res_Win_t * p );
+/*=== resCore.c ==========================================================*/
+extern int        Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars );
 
 
 #ifdef __cplusplus
diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index 17d1c62e..6340b175 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
-#include "res.h"
+#include "resInt.h"
 #include "kit.h"
 #include "satStore.h"
 
@@ -27,12 +27,120 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+typedef struct Res_Man_t_ Res_Man_t;
+struct Res_Man_t_
+{
+    // general parameters
+    Res_Par_t *   pPars;
+    // specialized manager
+    Res_Win_t *   pWin;          // windowing manager
+    Abc_Ntk_t *   pAig;          // the strashed window
+    Res_Sim_t *   pSim;          // simulation manager
+    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 *   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           nCandSets;     // the total number of candidates
+    int           nProvedSets;   // the total number of proved groups
+    int           nSimEmpty;     // the empty simulation info
+    // runtime
+    int           timeWin;       // windowing
+    int           timeDiv;       // divisors
+    int           timeAig;       // strashing
+    int           timeSim;       // simulation
+    int           timeCand;      // resubstitution candidates
+    int           timeSat;       // SAT solving
+    int           timeInt;       // interpolation 
+    int           timeUpd;       // updating  
+    int           timeTotal;     // total runtime
+};
+
+extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
+  Synopsis    [Allocate resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Res_Man_t * Res_ManAlloc( Res_Par_t * pPars )
+{
+    Res_Man_t * p;
+    p = ALLOC( Res_Man_t, 1 );
+    memset( p, 0, sizeof(Res_Man_t) );
+    assert( pPars->nWindow > 0 && pPars->nWindow < 100 );
+    assert( pPars->nCands > 0 && pPars->nCands < 100 );
+    p->pPars = pPars;
+    p->pWin = Res_WinAlloc();
+    p->pSim = Res_SimAlloc( pPars->nSimWords );
+    p->pMan = Int_ManAlloc( 512 );
+    p->vMem = Vec_IntAlloc( 0 );
+    p->vResubs = Vec_VecStart( pPars->nCands );
+    p->vLevels = Vec_VecStart( 32 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Deallocate resynthesis manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_ManFree( Res_Man_t * p )
+{
+    if ( p->pPars->fVerbose )
+    {
+        printf( "Winds = %d. ", p->nWins );
+        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( "Cands = %d. ", p->nCandSets );
+        printf( "Proved = %d. ", p->nProvedSets );
+        printf( "\n" );
+
+        PRT( "Windowing  ", p->timeWin );
+        PRT( "Divisors   ", p->timeDiv );
+        PRT( "Strashing  ", p->timeAig );
+        PRT( "Simulation ", p->timeSim );
+        PRT( "Candidates ", p->timeCand );
+        PRT( "SAT solver ", p->timeSat );
+        PRT( "Interpol   ", p->timeInt );
+        PRT( "Undating   ", p->timeUpd );
+        PRT( "TOTAL      ", p->timeTotal );
+    }
+    Res_WinFree( p->pWin );
+    if ( p->pAig ) Abc_NtkDelete( p->pAig );
+    Res_SimFree( p->pSim );
+    if ( p->pCnf ) Sto_ManFree( p->pCnf );
+    Int_ManFree( p->pMan );
+    Vec_IntFree( p->vMem );
+    Vec_VecFree( p->vResubs );
+    Vec_VecFree( p->vLevels );
+    free( p );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Entrace into the resynthesis package.]
 
   Description []
@@ -42,31 +150,23 @@
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, int nWindow, int nSimWords, int fVerbose, int fVeryVerbose )
+int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, Res_Par_t * pPars )
 {
-    Int_Man_t * pMan;
-    Sto_Man_t * pCnf;
-    Res_Win_t * pWin;
-    Res_Sim_t * pSim;
-    Abc_Ntk_t * pAig;
+    Res_Man_t * p;
     Abc_Obj_t * pObj;
     Hop_Obj_t * pFunc;
     Kit_Graph_t * pGraph;
-    Vec_Vec_t * vResubs;
     Vec_Ptr_t * vFanins;
-    Vec_Int_t * vMemory;
     unsigned * puTruth;
-    int i, k, nNodesOld, nFanins;
+    int i, k, RetValue, nNodesOld, nFanins;
+    int clk, clkTotal = clock();
     assert( Abc_NtkHasAig(pNtk) );
-    assert( nWindow > 0 && nWindow < 100 );
-    vMemory = Vec_IntAlloc(0);
-    // start the interpolation manager
-    pMan = Int_ManAlloc( 512 );
-    // start the window
-    pWin = Res_WinAlloc();
-    pSim = Res_SimAlloc( nSimWords );
+
+    // start the manager
+    p = Res_ManAlloc( pPars );
     // set the number of levels
     Abc_NtkLevel( pNtk );
+
     // try resynthesizing nodes in the topological order
     nNodesOld = Abc_NtkObjNumMax(pNtk);
     Abc_NtkForEachObj( pNtk, pObj, i )
@@ -75,52 +175,113 @@ int Abc_NtkResynthesize( Abc_Ntk_t * pNtk, int nWindow, int nSimWords, int fVerb
             continue;
         if ( pObj->Id > nNodesOld )
             break;
+
         // create the window for this node
-        if ( !Res_WinCompute(pObj, nWindow/10, nWindow%10, pWin) )
+clk = clock();
+        RetValue = Res_WinCompute( pObj, p->pPars->nWindow/10, p->pPars->nWindow%10, p->pWin );
+p->timeWin += clock() - clk;
+        if ( !RetValue )
             continue;
+
+        p->nWins++;
+        p->nWinNodes += Vec_VecSizeSize( p->pWin->vLevels );
+
         // collect the divisors
-        Res_WinDivisors( pWin, pObj->Level - 1 );
+clk = clock();
+        Res_WinDivisors( p->pWin, pObj->Level - 1 );
+p->timeDiv += clock() - clk;
+        p->nDivNodes += Vec_PtrSize( p->pWin->vDivs );
+
         // create the AIG for the window
-        pAig = Res_WndStrash( pWin );
+clk = clock();
+        if ( p->pAig ) Abc_NtkDelete( p->pAig );
+        p->pAig = Res_WndStrash( p->pWin );
+p->timeAig += clock() - clk;
+
+        if ( p->pPars->fVeryVerbose )
+        {
+            printf( "%5d : ", pObj->Id );
+            printf( "Win = %3d/%4d/%3d ", Vec_PtrSize(p->pWin->vLeaves), 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" );
+        }
+
         // prepare simulation info
-        if ( !Res_SimPrepare( pSim, pAig ) )
+clk = clock();
+        RetValue = Res_SimPrepare( p->pSim, p->pAig );
+p->timeSim += clock() - clk;
+        if ( !RetValue )
         {
-            Abc_NtkDelete( pAig );
+            p->nSimEmpty++;
             continue;
         }
+
         // find resub candidates for the node
-        vResubs = Res_FilterCandidates( pWin, pSim );
-        if ( vResubs )
+clk = clock();
+        RetValue = Res_FilterCandidates( p->pWin, p->pAig, p->pSim, p->vResubs );
+p->timeCand += clock() - clk;
+        p->nCandSets += RetValue;
+        if ( RetValue == 0 )
+            continue;
+
+        // iterate through candidate resubstitutions
+        Vec_VecForEachLevel( p->vResubs, vFanins, k )
         {
-            // iterate through the resubstitutions
-            Vec_VecForEachLevel( vResubs, vFanins, k )
-            {
-                extern Hop_Obj_t * Kit_GraphToHop( Hop_Man_t * pMan, Kit_Graph_t * pGraph );
-                pCnf = Res_SatProveUnsat( pAig, vFanins );
-                if ( pCnf == NULL )
-                    continue;
-                // interplate this proof
-                nFanins = Int_ManInterpolate( pMan, pCnf, fVerbose, &puTruth );
-                assert( nFanins == Vec_PtrSize(vFanins) - 2 );
-                Sto_ManFree( pCnf );
-                // transform interpolant into the AIG
-                pGraph = Kit_TruthToGraph( puTruth, nFanins, vMemory );
-                // derive the AIG for the decomposition tree
-                pFunc = Kit_GraphToHop( pNtk->pManFunc, pGraph );
-                Kit_GraphFree( pGraph );
-                // update the network
-                if ( pFunc == NULL )
-                    Res_UpdateNetwork( pObj, vFanins, pFunc, pWin->vLevels );
+            if ( Vec_PtrSize(vFanins) == 0 )
                 break;
+
+            // solve the SAT problem and get clauses
+clk = clock();
+            if ( p->pCnf ) Sto_ManFree( p->pCnf );
+            p->pCnf = Res_SatProveUnsat( p->pAig, vFanins );
+p->timeSat += clock() - clk;
+            if ( p->pCnf == NULL )
+            {
+//                printf( " Sat\n" );
+                continue;
+            }
+//            printf( " Unsat\n" );
+
+            // write it into a file
+//            Sto_ManDumpClauses( p->pCnf, "trace.cnf" );
+
+            p->nProvedSets++;
+
+            // interplate the problem if it was UNSAT
+clk = clock();
+            RetValue = Int_ManInterpolate( p->pMan, p->pCnf, p->pPars->fVerbose, &puTruth );
+p->timeInt += clock() - clk;
+            assert( RetValue == Vec_PtrSize(vFanins) - 2 );
+
+            if ( puTruth )
+            {
+                Extra_PrintBinary( stdout, puTruth, 1 << RetValue );
+                printf( "\n" );
             }
-            Vec_VecFree( vResubs );
+
+            continue;
+            
+            // transform interpolant into the AIG
+            pGraph = Kit_TruthToGraph( puTruth, nFanins, p->vMem );
+
+            // derive the AIG for the decomposition tree
+            pFunc = Kit_GraphToHop( pNtk->pManFunc, pGraph );
+            Kit_GraphFree( pGraph );
+
+            // update the network
+clk = clock();
+            Res_UpdateNetwork( pObj, vFanins, pFunc, p->vLevels );
+p->timeUpd += clock() - clk;
+            break;
         }
-        Abc_NtkDelete( pAig );
     }
-    Res_WinFree( pWin );
-    Res_SimFree( pSim );
-    Int_ManFree( pMan );
-    Vec_IntFree( vMemory );
+
+    // quit resubstitution manager
+p->timeTotal = clock() - clkTotal;
+    Res_ManFree( p );
+
     // check the resulting network
     if ( !Abc_NtkCheck( pNtk ) )
     {
diff --git a/src/opt/res/resDivs.c b/src/opt/res/resDivs.c
index 0739b81b..a18764ed 100644
--- a/src/opt/res/resDivs.c
+++ b/src/opt/res/resDivs.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
-#include "res.h"
+#include "resInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -56,11 +56,12 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
     // prepare the new trav ID
     Abc_NtkIncrementTravId( p->pNode->pNtk );
     // mark the TFO of the node (does not increment trav ID)
-    Res_WinVisitNodeTfo( p );
+    Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax, NULL );
     // mark the MFFC of the node (does not increment trav ID)
     Res_WinVisitMffc( p );
 
     // 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 )
     {
         // skip nodes in the TFO or in the MFFC of node
@@ -69,15 +70,15 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
         // consider fanouts of this node
         Abc_ObjForEachFanout( pObj, pFanout, f )
         {
+            // skip nodes that are already added
+            if ( pFanout->fMarkA )
+                continue;
             // skip COs
             if ( !Abc_ObjIsNode(pFanout) ) 
                 continue;
             // skip nodes in the TFO or in the MFFC of node
             if ( Abc_NodeIsTravIdCurrent(pFanout) )
                 continue;
-            // skip nodes that are already added
-            if ( pFanout->fMarkA )
-                continue;
             // skip nodes with large level
             if ( (int)pFanout->Level > p->nLevDivMax )
                 continue;
@@ -85,10 +86,11 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
             Abc_ObjForEachFanin( pFanout, pFanin, m )
                 if ( !pFanin->fMarkA )
                     break;
-            if ( m < Abc_ObjFaninNum(pFanin) )
+            if ( m < Abc_ObjFaninNum(pFanout) )
                 continue;
             // add the node
             Res_WinAddNode( p, pFanout );
+            p->nDivsPlus++;
         }
     }
 
@@ -100,8 +102,8 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
 
     // collect the divisors below the line
     Vec_PtrClear( p->vDivs );
-    // collect the node fanins first
-    Abc_ObjForEachFanin( pObj, pFanin, m )
+    // collect the node fanins first and mark the fanins
+    Abc_ObjForEachFanin( p->pNode, pFanin, m )
     {
         Vec_PtrPush( p->vDivs, pFanin );
         Abc_NodeSetTravIdCurrent( pFanin );
@@ -114,6 +116,9 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
     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 );
 }
 
 /**Function*************************************************************
diff --git a/src/opt/res/resFilter.c b/src/opt/res/resFilter.c
index 65e9953f..4f1be833 100644
--- a/src/opt/res/resFilter.c
+++ b/src/opt/res/resFilter.c
@@ -19,19 +19,21 @@
 ***********************************************************************/
 
 #include "abc.h"
-#include "res.h"
+#include "resInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+static unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim, unsigned uMask );
+
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
 
-  Synopsis    []
+  Synopsis    [Finds sets of feasible candidates.]
 
   Description []
                
@@ -40,26 +42,78 @@
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Vec_t * Res_FilterCandidates( Res_Win_t * pWin, Res_Sim_t * pSim )
+int Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs )
 {
+    Abc_Obj_t * pFanin, * pFanin2;
     unsigned * pInfo;
-    Abc_Obj_t * pFanin;
-    int i, RetValue;
+    int Counter, RetValue, i, k;
+
     // check that the info the node is one
     pInfo = Vec_PtrEntry( pSim->vOuts, 1 );
     RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
     if ( RetValue == 0 )
         printf( "Failed 1!" );
+
     // collect the fanin info
-    pInfo = Vec_PtrEntry( pSim->vOuts, 0 );
-    Abc_InfoClear( pInfo, pSim->nWordsOut );
-    Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
-        Abc_InfoOr( pInfo, Vec_PtrEntry( pSim->vOuts, 2+i ), pSim->nWordsOut );
-    // check that the simulation info is constant 1
+    pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~0 );
     RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
     if ( RetValue == 0 )
         printf( "Failed 2!" );
-    return NULL;
+
+    // try removing fanins
+//    printf( "Fanins: " );
+    Counter = 0;
+    Vec_VecClear( vResubs );
+    Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
+    {
+        pInfo = Res_FilterCollectFaninInfo( pWin, pSim, ~(1 << i) );
+        RetValue = Abc_InfoIsOne( pInfo, pSim->nWordsOut );
+        if ( RetValue )
+        {
+//            printf( "Node %4d. Removing fanin %4d.\n", pWin->pNode->Id, Abc_ObjFaninId(pWin->pNode, i) );
+
+            // collect the nodes
+            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,0) );
+            Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,1) );
+            Abc_ObjForEachFanin( pWin->pNode, pFanin2, k )
+            {
+                if ( k != i )
+                    Vec_VecPush( vResubs, Counter, Abc_NtkPo(pAig,2+k) );
+            }
+            Counter++;
+        }
+        if ( Counter == Vec_VecSize(vResubs) )
+            break;            
+//        printf( "%d", RetValue );
+    }
+//    printf( "\n\n" );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds sets of feasible candidates.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned * Res_FilterCollectFaninInfo( Res_Win_t * pWin, Res_Sim_t * pSim, unsigned uMask )
+{
+    Abc_Obj_t * pFanin;
+    unsigned * pInfo;
+    int i;
+    pInfo = Vec_PtrEntry( pSim->vOuts, 0 );
+    Abc_InfoClear( pInfo, pSim->nWordsOut );
+    Abc_ObjForEachFanin( pWin->pNode, pFanin, i )
+    {
+        if ( uMask & (1 << i) )
+            Abc_InfoOr( pInfo, Vec_PtrEntry(pSim->vOuts, 2+i), pSim->nWordsOut );
+    }
+    return pInfo;
 }
 
 
diff --git a/src/opt/res/resInt.h b/src/opt/res/resInt.h
new file mode 100644
index 00000000..f5c64f8e
--- /dev/null
+++ b/src/opt/res/resInt.h
@@ -0,0 +1,126 @@
+/**CFile****************************************************************
+
+  FileName    [resInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Resynthesis package.]
+
+  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 __RES_INT_H__
+#define __RES_INT_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "res.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+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
+    Abc_Obj_t *      pNode;      // the node in the center
+    // 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
+};
+
+typedef struct Res_Sim_t_ Res_Sim_t;
+struct Res_Sim_t_
+{
+    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 
+    // 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
+    // resub 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                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== resDivs.c ==========================================================*/
+extern void          Res_WinDivisors( Res_Win_t * p, int nLevDivMax );
+extern int           Res_WinVisitMffc( Res_Win_t * p );
+/*=== resFilter.c ==========================================================*/
+extern int           Res_FilterCandidates( Res_Win_t * pWin, Abc_Ntk_t * pAig, Res_Sim_t * pSim, Vec_Vec_t * vResubs );
+/*=== resSat.c ==========================================================*/
+extern void *        Res_SatProveUnsat( 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 );
+extern int           Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig );
+/*=== resStrash.c ==========================================================*/
+extern Abc_Ntk_t *   Res_WndStrash( Res_Win_t * p );
+/*=== resWnd.c ==========================================================*/
+extern void          Res_UpdateNetwork( Abc_Obj_t * pObj, Vec_Ptr_t * vFanins, Hop_Obj_t * pFunc, Vec_Vec_t * vLevels );
+/*=== 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_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t * p );
+
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/opt/res/resSat.c b/src/opt/res/resSat.c
index 770152cf..ec609445 100644
--- a/src/opt/res/resSat.c
+++ b/src/opt/res/resSat.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
-#include "res.h"
+#include "resInt.h"
 #include "hop.h"
 #include "satSolver.h"
 
@@ -27,7 +27,7 @@
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-extern int Res_SatAddConst1( sat_solver * pSat, int iVar );
+extern int Res_SatAddConst1( sat_solver * pSat, int iVar, int fCompl );
 extern int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl );
 extern int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int fCompl0, int fCompl1 );
 
@@ -48,70 +48,85 @@ extern int Res_SatAddAnd( sat_solver * pSat, int iVar, int iVar0, int iVar1, int
 ***********************************************************************/
 void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
 {
-    void * pCnf;
+    void * pCnf = NULL;
     sat_solver * pSat;
     Vec_Ptr_t * vNodes;
     Abc_Obj_t * pObj;
     int i, nNodes, status;
 
-    // make sure the constant node is not involved
-    assert( Abc_ObjFanoutNum(Abc_AigConst1(pAig)) == 0 );
+    // make sure fanins contain POs of the AIG
+    pObj = Vec_PtrEntry( vFanins, 0 );
+    assert( pObj->pNtk == pAig && Abc_ObjIsPo(pObj) );
 
     // 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 )
+    Vec_PtrForEachEntry( vFanins, pObj, i ) // useful POs
         pObj->pCopy = (void *)nNodes++;
 
     // start the solver
     pSat = sat_solver_new();
     sat_solver_store_alloc( pSat );
 
-    // add clause for AND gates
+    // 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) );
-    // add clauses for the POs
+    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 );
+    Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // care-set
     pObj = Vec_PtrEntry(vFanins, 1);
-    Res_SatAddConst1( pSat, (int)pObj->pCopy );
+    Res_SatAddConst1( pSat, (int)pObj->pCopy, 0 ); // on-set
+
     // bookmark the clauses of A
     sat_solver_store_mark_clauses_a( pSat );
+
     // duplicate the clauses
     pObj = Vec_PtrEntry(vFanins, 1);
     Sat_SolverDoubleClauses( pSat, (int)pObj->pCopy );
-    // add the equality clauses
+    // add the equality constraints
     Vec_PtrForEachEntryStart( vFanins, pObj, i, 2 )
         Res_SatAddEqual( pSat, (int)pObj->pCopy, ((int)pObj->pCopy) + nNodes, 0 );
+
     // bookmark the roots
     sat_solver_store_mark_roots( pSat );
-    Vec_PtrFree( vNodes );
 
     // solve the problem
     status = sat_solver_solve( pSat, NULL, NULL, (sint64)10000, (sint64)0, (sint64)0, (sint64)0 );
     if ( status == l_False )
+    {
         pCnf = sat_solver_store_release( pSat );
+//        printf( "unsat\n" );
+    }
     else if ( status == l_True )
-        pCnf = NULL;
+    {
+//        printf( "sat\n" );
+    }
     else
-        pCnf = NULL;
+    {
+//        printf( "undef\n" );
+    }
     sat_solver_delete( pSat );
     return pCnf;
 }
 
 /**Function*************************************************************
 
-  Synopsis    [Loads two-input AND-gate.]
+  Synopsis    [Asserts equality of the variable to a constant.]
 
   Description []
                
@@ -120,9 +135,9 @@ void * Res_SatProveUnsat( Abc_Ntk_t * pAig, Vec_Ptr_t * vFanins )
   SeeAlso     []
 
 ***********************************************************************/
-int Res_SatAddConst1( sat_solver * pSat, int iVar )
+int Res_SatAddConst1( sat_solver * pSat, int iVar, int fCompl )
 {
-    lit Lit = lit_var(iVar);
+    lit Lit = toLitCond( iVar, fCompl );
     if ( !sat_solver_addclause( pSat, &Lit, &Lit + 1 ) )
         return 0;
     return 1;
@@ -130,7 +145,7 @@ int Res_SatAddConst1( sat_solver * pSat, int iVar )
 
 /**Function*************************************************************
 
-  Synopsis    [Loads two-input AND-gate.]
+  Synopsis    [Asserts equality of two variables.]
 
   Description []
                
@@ -158,7 +173,7 @@ int Res_SatAddEqual( sat_solver * pSat, int iVar0, int iVar1, int fCompl )
 
 /**Function*************************************************************
 
-  Synopsis    [Loads two-input AND-gate.]
+  Synopsis    [Adds constraints for the two-input AND-gate.]
 
   Description []
                
diff --git a/src/opt/res/resSim.c b/src/opt/res/resSim.c
index 27ce7b6c..27a6c1f0 100644
--- a/src/opt/res/resSim.c
+++ b/src/opt/res/resSim.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
-#include "res.h"
+#include "resInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -38,7 +38,7 @@
   SideEffects []
 
   SeeAlso     []
-
+ 
 ***********************************************************************/
 Res_Sim_t * Res_SimAlloc( int nWords )
 {
@@ -57,8 +57,6 @@ Res_Sim_t * Res_SimAlloc( int nWords )
     p->vOuts     = Vec_PtrAllocSimInfo( 128,  p->nWordsOut );
     // resub candidates
     p->vCands    = Vec_VecStart( 16 );
-    // set siminfo for the constant node
-    Abc_InfoFill( Vec_PtrEntry(p->vPats,0), p->nWords );
     return p;
 }
 
@@ -75,6 +73,8 @@ Res_Sim_t * Res_SimAlloc( int nWords )
 ***********************************************************************/
 void Res_SimAdjust( Res_Sim_t * p, Abc_Ntk_t * pAig )
 {
+    srand( 0xABC );
+
     assert( Abc_NtkIsStrash(pAig) );
     p->pAig = pAig;
     if ( Vec_PtrSize(p->vPats) < Abc_NtkObjNumMax(pAig)+1 )
@@ -125,44 +125,6 @@ void Res_SimFree( Res_Sim_t * p )
     free( p );
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Free simulation engine.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Res_SimReportOne( Res_Sim_t * p )
-{
-    unsigned * pInfoCare, * pInfoNode;
-    int i, nDcs, nOnes, nZeros;
-    pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
-    pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
-    nDcs = nOnes = nZeros = 0;
-    for ( i = 0; i < p->nPats; i++ )
-    {
-        // skip don't-care patterns
-        if ( !Abc_InfoHasBit(pInfoCare, i) )
-        {
-            nDcs++;
-            continue;
-        }
-        // separate offset and onset patterns
-        if ( !Abc_InfoHasBit(pInfoNode, i) )
-            nZeros++;
-        else
-            nOnes++;
-    }
-    printf( "Onset = %3d (%6.2f %%)  ",  nOnes,  100.0*nOnes/p->nPats );
-    printf( "Offset = %3d (%6.2f %%)  ", nZeros, 100.0*nZeros/p->nPats );
-    printf( "Dcset = %3d (%6.2f %%)  ",  nDcs,   100.0*nDcs/p->nPats );
-    printf( "\n" );
-}
-
 
 /**Function*************************************************************
 
@@ -292,6 +254,7 @@ void Res_SimPerformRound( Res_Sim_t * p )
 {
     Abc_Obj_t * pObj;
     int i;
+    Abc_InfoFill( Vec_PtrEntry(p->vPats,0), p->nWords );
     Abc_AigForEachAnd( p->pAig, pObj, i )
         Res_SimPerformOne( pObj, p->vPats, p->nWords );
     Abc_NtkForEachPo( p->pAig, pObj, i )
@@ -313,14 +276,17 @@ void Res_SimProcessPats( Res_Sim_t * p )
 {
     Abc_Obj_t * pObj;
     unsigned * pInfoCare, * pInfoNode;
-    int i, j;
+    int i, j, nDcs = 0;
     pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
     pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
     for ( i = 0; i < p->nPats; i++ )
     {
         // skip don't-care patterns
         if ( !Abc_InfoHasBit(pInfoCare, i) )
+        {
+            nDcs++;
             continue;
+        }
         // separate offset and onset patterns
         if ( !Abc_InfoHasBit(pInfoNode, i) )
         {
@@ -357,14 +323,21 @@ void Res_SimProcessPats( Res_Sim_t * p )
 void Res_SimPadSimInfo( Vec_Ptr_t * vPats, int nPats, int nWords )
 {
     unsigned * pInfo;
-    int i, w, iWords, nBits;
+    int i, w, iWords;
+    assert( nPats > 0 && nPats < nWords * 8 * (int) sizeof(unsigned) );
+    // pad the first word
+    if ( nPats < 8 * sizeof(unsigned) )
+    {
+        Vec_PtrForEachEntry( vPats, pInfo, i )
+            if ( pInfo[0] & 1 )
+                pInfo[0] |= ((~0) << nPats);
+        nPats = 8 * sizeof(unsigned);
+    }
+    // pad the empty words
     iWords = nPats / (8 * sizeof(unsigned));
-    nBits = nPats % (8 * sizeof(unsigned));
-    if ( iWords == nWords )
-        return;
     Vec_PtrForEachEntry( vPats, pInfo, i )
     {
-        for ( w = iWords; w < nWords; i++ )
+        for ( w = iWords; w < nWords; w++ )
             pInfo[w] = pInfo[0];
     }
 }
@@ -424,6 +397,72 @@ void Res_SimDeriveInfoComplement( Res_Sim_t * p )
 
 /**Function*************************************************************
 
+  Synopsis    [Free simulation engine.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimReportOne( Res_Sim_t * p )
+{
+    unsigned * pInfoCare, * pInfoNode;
+    int i, nDcs, nOnes, nZeros;
+    pInfoCare = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 0)->Id );
+    pInfoNode = Vec_PtrEntry( p->vPats, Abc_NtkPo(p->pAig, 1)->Id );
+    nDcs = nOnes = nZeros = 0;
+    for ( i = 0; i < p->nPats; i++ )
+    {
+        // skip don't-care patterns
+        if ( !Abc_InfoHasBit(pInfoCare, i) )
+        {
+            nDcs++;
+            continue;
+        }
+        // separate offset and onset patterns
+        if ( !Abc_InfoHasBit(pInfoNode, i) )
+            nZeros++;
+        else
+            nOnes++;
+    }
+    printf( "On = %3d (%7.2f %%)  ",  nOnes,  100.0*nOnes/p->nPats );
+    printf( "Off = %3d (%7.2f %%)  ", nZeros, 100.0*nZeros/p->nPats );
+    printf( "Dc = %3d (%7.2f %%)  ",  nDcs,   100.0*nDcs/p->nPats );
+    printf( "P0 = %3d ", p->nPats0 );
+    printf( "P1 = %3d ", p->nPats1 );
+    if ( p->nPats0 < 4 || p->nPats1 < 4 )
+        printf( "*" );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints output patterns.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Res_SimPrintOutPatterns( Res_Sim_t * p, Abc_Ntk_t * pAig )
+{
+    Abc_Obj_t * pObj;
+    unsigned * pInfo2;
+    int i;
+    Abc_NtkForEachPo( pAig, pObj, i )
+    {
+        pInfo2 = Vec_PtrEntry( p->vOuts, i );
+        Extra_PrintBinary( stdout, pInfo2, p->nPatsOut );
+        printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
   Synopsis    [Prepares simulation info for candidate filtering.]
 
   Description []
@@ -435,19 +474,24 @@ void Res_SimDeriveInfoComplement( Res_Sim_t * p )
 ***********************************************************************/
 int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig )
 {
-    int Limit = 20;
+    int Limit;
     // prepare the manager
     Res_SimAdjust( p, pAig );
     // collect 0/1 simulation info
-    while ( p->nPats0 < p->nPats || p->nPats1 < p->nPats || Limit-- == 0 )
+    for ( Limit = 0; Limit < 100; Limit++ )
     {
         Res_SimSetRandom( p );
         Res_SimPerformRound( p );
         Res_SimProcessPats( p );
-        if ( Limit == 19 )
-            Res_SimReportOne( p );
+        if ( !(p->nPats0 < p->nPats || p->nPats1 < p->nPats) )
+            break;
+
     }
-    if ( p->nPats0 < 32 || p->nPats1 < 32 )
+//    printf( "%d   ", Limit );
+    // report the last set of patterns
+//    Res_SimReportOne( p );
+    // quit if there is not enough
+    if ( p->nPats0 < 4 || p->nPats1 < 4 )
         return 0;
     // create bit-matrix info
     if ( p->nPats0 < p->nPats )
@@ -462,6 +506,8 @@ int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig )
     Res_SimSetGiven( p, p->vPats1 );
     Res_SimPerformRound( p );
     Res_SimDeriveInfoComplement( p );
+    // print output patterns
+//    Res_SimPrintOutPatterns( p, pAig );
     return 1;
 }
 
diff --git a/src/opt/res/resStrash.c b/src/opt/res/resStrash.c
index 2c112642..d3a8efa8 100644
--- a/src/opt/res/resStrash.c
+++ b/src/opt/res/resStrash.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
-#include "res.h"
+#include "resInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -72,7 +72,7 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
     }
     // mark the TFO of the node
     Abc_NtkIncrementTravId( p->pNode->pNtk );
-    Res_WinVisitNodeTfo( p );
+    Res_WinSweepLeafTfo_rec( p->pNode, (int)p->pNode->Level + p->nWinTfoMax, NULL );
     // redo strashing in the TFO
     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 )
@@ -92,6 +92,9 @@ Abc_Ntk_t * Res_WndStrash( Res_Win_t * p )
     // add the divisors
     Vec_PtrForEachEntry( p->vDivs, pObj, i )
         Abc_ObjAddFanin( Abc_NtkCreatePo(pAig), pObj->pCopy );
+    // add the names
+    Abc_NtkAddDummyPiNames( pAig );
+    Abc_NtkAddDummyPoNames( pAig );
     // check the resulting network
     if ( !Abc_NtkCheck( pAig ) )
         fprintf( stdout, "Res_WndStrash(): Network check has failed.\n" );
diff --git a/src/opt/res/resUpdate.c b/src/opt/res/resUpdate.c
index f79176bc..06704b1c 100644
--- a/src/opt/res/resUpdate.c
+++ b/src/opt/res/resUpdate.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
-#include "res.h"
+#include "resInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
diff --git a/src/opt/res/resWin.c b/src/opt/res/resWin.c
index a2504d50..b5fe0641 100644
--- a/src/opt/res/resWin.c
+++ b/src/opt/res/resWin.c
@@ -19,7 +19,7 @@
 ***********************************************************************/
 
 #include "abc.h"
-#include "res.h"
+#include "resInt.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -95,7 +95,7 @@ void Res_WinCollectNodeTfi( Res_Win_t * p )
     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 )
+    Vec_VecForEachLevelReverseStartStop( p->vLevels, vFront, i, p->pNode->Level, p->nLevLeaves + 1 )
     {
         Vec_PtrForEachEntry( vFront, pObj, k )
             Abc_ObjForEachFanin( pObj, pFanin, m )
@@ -190,15 +190,14 @@ void Res_WinCollectRoots_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(pObj) )
+        if ( !Abc_NodeIsTravIdCurrent(pFanout) )
             break;
     // if some of the fanouts are unmarked, add the node to the root
     if ( i < Abc_ObjFanoutNum(pObj) ) 
     {
-        Vec_PtrPush( vRoots, pObj );
+        Vec_PtrPushUnique( vRoots, pObj );
         return;
     }
     // otherwise, call recursively
@@ -220,6 +219,7 @@ void Res_WinCollectRoots_rec( Abc_Obj_t * pObj, Vec_Ptr_t * vRoots )
 ***********************************************************************/
 void Res_WinCollectRoots( Res_Win_t * p )
 {
+    assert( !Abc_NodeIsTravIdCurrent(p->pNode) );
     Vec_PtrClear( p->vRoots );
     Res_WinCollectRoots_rec( p->pNode, p->vRoots );
 }
@@ -241,7 +241,7 @@ void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj )
     int i;
     if ( pObj->fMarkA )
         return;
-    if ( !Abc_NodeIsTravIdCurrent(pObj) )
+    if ( !Abc_NodeIsTravIdCurrent(pObj) || (int)pObj->Level <= p->nLevLeaves )
     {
         Vec_PtrPush( p->vLeaves, pObj );
         pObj->fMarkA = 1;
@@ -250,7 +250,7 @@ void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj )
     Res_WinAddNode( p, pObj );
     // visit the fanins of the node
     Abc_ObjForEachFanin( pObj, pFanin, i )
-        Res_WinAddMissing_rec( p, pObj );
+        Res_WinAddMissing_rec( p, pFanin );
 }
 
 /**Function*************************************************************
@@ -295,7 +295,7 @@ void Res_WinUnmark( Res_Win_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Labels the TFO of the node with the current trav ID.]
+  Synopsis    [Verifies the window.]
 
   Description []
                
@@ -304,10 +304,30 @@ void Res_WinUnmark( Res_Win_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Res_WinVisitNodeTfo( Res_Win_t * p )
+void Res_WinVerify( Res_Win_t * p )
 {
-    // mark the TFO of the node
-    Res_WinSweepLeafTfo_rec( p->pNode, p->nLevDivMax, NULL );
+    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 );
 }
 
 /**Function*************************************************************
@@ -329,9 +349,7 @@ int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t
     p->pNode = pNode;
     p->nWinTfiMax = nWinTfiMax;
     p->nWinTfoMax = nWinTfoMax;
-    p->nLevLeaves = ABC_MAX( 0, p->pNode->Level - p->nWinTfiMax - 1 );
-    p->nLevDivMax = 0;
-    Vec_PtrClear( p->vDivs );
+    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
@@ -344,6 +362,12 @@ int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t
     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 );
     return 1;
 }
 
diff --git a/src/sat/bsat/module.make b/src/sat/bsat/module.make
index c8ec65dd..563c8dfc 100644
--- a/src/sat/bsat/module.make
+++ b/src/sat/bsat/module.make
@@ -1,3 +1,6 @@
 SRC +=  src/sat/bsat/satMem.c \
+    src/sat/bsat/satInter.c \
     src/sat/bsat/satSolver.c \
+    src/sat/bsat/satStore.c \
+    src/sat/bsat/satTrace.c \
     src/sat/bsat/satUtil.c
diff --git a/src/sat/bsat/satInter.c b/src/sat/bsat/satInter.c
index e22b309c..32a011b9 100644
--- a/src/sat/bsat/satInter.c
+++ b/src/sat/bsat/satInter.c
@@ -71,18 +71,18 @@ struct Int_Man_t_
     int             timeTotal;    // the total runtime of interpolation
 };
 
-// procedure to get hold of the clauses' truth table
+// procedure to get hold of the clauses' truth table 
 static inline unsigned * Int_ManTruthRead( Int_Man_t * p, Sto_Cls_t * pCls )          { return p->pInters + pCls->Id * p->nWords;                 }
-static inline void       Int_ManTruthClear( unsigned * p, int nWords )                { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = 0;      }
-static inline void       Int_ManTruthFill( unsigned * p, int nWords )                 { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = ~0;     }
-static inline void       Int_ManTruthCopy( unsigned * p, unsigned * q, int nWords )   { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] = q[i];   }
-static inline void       Int_ManTruthAnd( unsigned * p, unsigned * q, int nWords )    { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &= q[i];  }
-static inline void       Int_ManTruthOr( unsigned * p, unsigned * q, int nWords )     { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= q[i];  }
+static inline void       Int_ManTruthClear( unsigned * p, int nWords )                { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i]  =  0;    }
+static inline void       Int_ManTruthFill( unsigned * p, int nWords )                 { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i]  = ~0;    }
+static inline void       Int_ManTruthCopy( unsigned * p, unsigned * q, int nWords )   { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i]  =  q[i]; }
+static inline void       Int_ManTruthAnd( unsigned * p, unsigned * q, int nWords )    { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] &=  q[i]; }
+static inline void       Int_ManTruthOr( unsigned * p, unsigned * q, int nWords )     { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |=  q[i]; }
 static inline void       Int_ManTruthOrNot( unsigned * p, unsigned * q, int nWords )  { int i; for ( i = nWords - 1; i >= 0; i-- ) p[i] |= ~q[i]; }
 
 // reading/writing the proof for a clause
-static inline int        Int_ManProofRead( Int_Man_t * p, Sto_Cls_t * pCls )          { return p->pProofNums[pCls->Id];  }
-static inline void       Int_ManProofWrite( Int_Man_t * p, Sto_Cls_t * pCls, int n )  { p->pProofNums[pCls->Id] = n;     }
+static inline int        Int_ManProofGet( Int_Man_t * p, Sto_Cls_t * pCls )           { return p->pProofNums[pCls->Id];  }
+static inline void       Int_ManProofSet( Int_Man_t * p, Sto_Cls_t * pCls, int n )    { p->pProofNums[pCls->Id] = n;     }
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -110,7 +110,7 @@ Int_Man_t * Int_ManAlloc( int nVarsAlloc )
     p->pResLits = malloc( sizeof(lit) * p->nResLitsAlloc );
     // parameters
     p->fProofWrite = 0;
-    p->fProofVerif = 0;
+    p->fProofVerif = 1;
     return p;    
 }
 
@@ -125,7 +125,7 @@ Int_Man_t * Int_ManAlloc( int nVarsAlloc )
   SeeAlso     []
 
 ***********************************************************************/
-int Int_ManCommonVars( Int_Man_t * p )
+int Int_ManGlobalVars( Int_Man_t * p )
 {
     Sto_Cls_t * pClause;
     int Var, nVarsAB, v;
@@ -161,8 +161,8 @@ int Int_ManCommonVars( Int_Man_t * p )
     nVarsAB = 0;
     for ( v = 0; v < p->pCnf->nVars; v++ )
         if ( p->pVarTypes[v] == -1 )
-            p->pVarTypes[v] -= p->nVarsAB++;
-printf( "There are %d global variables.\n", nVarsAB );
+            p->pVarTypes[v] -= nVarsAB++;
+//printf( "There are %d global variables.\n", nVarsAB );
     return nVarsAB;
 }
 
@@ -182,7 +182,6 @@ void Int_ManResize( Int_Man_t * p )
     // check if resizing is needed
     if ( p->nVarsAlloc < p->pCnf->nVars )
     {
-        int nVarsAllocOld = p->nVarsAlloc;
         // find the new size
         if ( p->nVarsAlloc == 0 )
             p->nVarsAlloc = 1;
@@ -205,7 +204,7 @@ void Int_ManResize( Int_Man_t * p )
     memset( p->pWatches , 0,    sizeof(Sto_Cls_t *) * p->pCnf->nVars*2 );
 
     // compute the number of common variables
-    p->nVarsAB = Int_ManCommonVars( p );
+    p->nVarsAB = Int_ManGlobalVars( p );
     // compute the number of words in the truth table
     p->nWords = (p->nVarsAB <= 5 ? 1 : (1 << (p->nVarsAB - 5)));
 
@@ -228,7 +227,7 @@ void Int_ManResize( Int_Man_t * p )
         p->nIntersAlloc = p->nWords * p->pCnf->nClauses;
         p->pInters = (unsigned *) realloc( p->pInters, sizeof(unsigned) * p->nIntersAlloc );
     }
-    memset( p->pInters, 0, sizeof(unsigned) * p->nIntersAlloc );
+//    memset( p->pInters, 0, sizeof(unsigned) * p->nWords * p->pCnf->nClauses );
 }
 
 /**Function*************************************************************
@@ -244,11 +243,12 @@ void Int_ManResize( Int_Man_t * p )
 ***********************************************************************/
 void Int_ManFree( Int_Man_t * p )
 {
+/*
     printf( "Runtime stats:\n" );
 PRT( "BCP     ", p->timeBcp   );
 PRT( "Trace   ", p->timeTrace );
 PRT( "TOTAL   ", p->timeTotal );
-
+*/
     free( p->pInters );
     free( p->pProofNums );
     free( p->pTrail );
@@ -278,7 +278,7 @@ PRT( "TOTAL   ", p->timeTotal );
 void Int_ManPrintClause( Int_Man_t * p, Sto_Cls_t * pClause )
 {
     int i;
-    printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Int_ManProofRead(p, pClause) );
+    printf( "Clause ID = %d. Proof = %d. {", pClause->Id, Int_ManProofGet(p, pClause) );
     for ( i = 0; i < (int)pClause->nLits; i++ )
         printf( " %d", pClause->pLits[i] );
     printf( " }\n" );
@@ -534,12 +534,12 @@ p->timeBcp += clock() - clk;
 ***********************************************************************/
 void Int_ManProofWriteOne( Int_Man_t * p, Sto_Cls_t * pClause )
 {
-    Int_ManProofWrite( p, pClause, ++p->Counter );
+    Int_ManProofSet( p, pClause, ++p->Counter );
 
     if ( p->fProofWrite )
     {
         int v;
-        fprintf( p->pFile, "%d", Int_ManProofRead(p, pClause) );
+        fprintf( p->pFile, "%d", Int_ManProofGet(p, pClause) );
         for ( v = 0; v < (int)pClause->nLits; v++ )
             fprintf( p->pFile, " %d", lit_print(pClause->pLits[v]) );
         fprintf( p->pFile, " 0 0\n" );
@@ -584,7 +584,7 @@ int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFin
         Int_ManTruthCopy( Int_ManTruthRead(p, pFinal), Int_ManTruthRead(p, pConflict), p->nWords );
 
     // follow the trail backwards
-    PrevId = Int_ManProofRead(p, pConflict);
+    PrevId = Int_ManProofGet(p, pConflict);
     for ( i = p->nTrailSize - 1; i >= 0; i-- )
     {
         // skip literals that are not involved
@@ -605,10 +605,10 @@ int Int_ManProofTraceOne( Int_Man_t * p, Sto_Cls_t * pConflict, Sto_Cls_t * pFin
 
 
         // record the reason clause
-        assert( Int_ManProofRead(p, pReason) > 0 );
+        assert( Int_ManProofGet(p, pReason) > 0 );
         p->Counter++;
         if ( p->fProofWrite )
-            fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Int_ManProofRead(p, pReason) );
+            fprintf( p->pFile, "%d * %d %d 0\n", p->Counter, PrevId, Int_ManProofGet(p, pReason) );
         PrevId = p->Counter;
 
         if ( p->pCnf->nClausesA )
@@ -700,7 +700,7 @@ p->timeTrace += clock() - clk;
     {
 //        Int_ManPrintInterOne( p, pFinal );
     }
-    Int_ManProofWrite( p, pFinal, p->Counter );
+    Int_ManProofSet( p, pFinal, p->Counter );
     return p->Counter;
 }
 
@@ -839,7 +839,7 @@ int Int_ManProcessRoots( Int_Man_t * p )
     {
         // detected root level conflict
         printf( "Int_ManProcessRoots(): Detected a root-level conflict\n" );
-        assert( 0 );
+//        assert( 0 );
         return 0;
     }
 
@@ -873,7 +873,7 @@ void Int_ManPrepareInter( Int_Man_t * p )
         { 0x00000000,0x00000000,0x00000000,0x00000000,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF,0xFFFFFFFF } 
     };
     Sto_Cls_t * pClause;
-    int Var, v;
+    int Var, VarAB, v;
     assert( p->nVarsAB <= 8 );
 
     // set interpolants for root clauses
@@ -892,10 +892,12 @@ void Int_ManPrepareInter( Int_Man_t * p )
             Var = lit_var(pClause->pLits[v]);
             if ( p->pVarTypes[Var] < 0 ) // global var
             {
+                VarAB = -p->pVarTypes[Var]-1;
+                assert( VarAB >= 0 && VarAB < p->nVarsAB );
                 if ( lit_sign(pClause->pLits[v]) ) // negative var
-                    Int_ManTruthOrNot( Int_ManTruthRead(p, pClause), uTruths[ -p->pVarTypes[Var]-1 ], p->nWords );
+                    Int_ManTruthOrNot( Int_ManTruthRead(p, pClause), uTruths[VarAB], p->nWords );
                 else
-                    Int_ManTruthOr( Int_ManTruthRead(p, pClause), uTruths[ -p->pVarTypes[Var]-1 ], p->nWords );
+                    Int_ManTruthOr( Int_ManTruthRead(p, pClause), uTruths[VarAB], p->nWords );
             }
         }
 //        Int_ManPrintInterOne( p, pClause );
@@ -922,12 +924,17 @@ 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;
 
     // adjust the manager
     Int_ManResize( p );
 
     // propagate root level assignments
-    Int_ManProcessRoots( p );
+    if ( !Int_ManProcessRoots( p ) )
+    {
+        *ppResult = NULL;
+        return p->nVarsAB;
+    }
 
     // prepare the interpolant computation
     Int_ManPrepareInter( p );
@@ -969,8 +976,8 @@ int Int_ManInterpolate( Int_Man_t * p, Sto_Man_t * pCnf, int fVerbose, unsigned
         1.0*Sto_ManMemoryReport(p->pCnf)/(1<<20) );
 
 p->timeTotal += clock() - clkTotal;
-    Int_ManFree( p );
-    return 1;
+    *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 6aafc187..1756b5df 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -1223,7 +1223,7 @@ int sat_solver_solve(sat_solver* s, lit* begin, lit* end, sint64 nConfLimit, sin
     sat_solver_canceluntil(s,0);
 
     ////////////////////////////////////////////////
-    if ( status == l_Undef && s->pStore )
+    if ( status == l_False && s->pStore )
     {
         extern int Sto_ManAddClause( void * p, lit * pBeg, lit * pEnd );
         int RetValue = Sto_ManAddClause( s->pStore, NULL, NULL );
diff --git a/src/sat/bsat/satStore.c b/src/sat/bsat/satStore.c
index 33cba6a7..7c1d7132 100644
--- a/src/sat/bsat/satStore.c
+++ b/src/sat/bsat/satStore.c
@@ -292,7 +292,7 @@ void Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName )
             fprintf( pFile, " %d", lit_print(pClause->pLits[i]) );
         fprintf( pFile, "\n" );
     }
-    fprintf( pFile, "\n" );
+    fprintf( pFile, " 0\n" );
     fclose( pFile );
 }
 
diff --git a/src/sat/bsat/satStore.h b/src/sat/bsat/satStore.h
index 3db52ada..346b59df 100644
--- a/src/sat/bsat/satStore.h
+++ b/src/sat/bsat/satStore.h
@@ -116,6 +116,8 @@ extern int          Sto_ManAddClause( Sto_Man_t * p, lit * pBeg, lit * pEnd );
 extern int          Sto_ManMemoryReport( Sto_Man_t * p );
 extern void         Sto_ManMarkRoots( Sto_Man_t * p );
 extern void         Sto_ManMarkClausesA( Sto_Man_t * p );
+extern void         Sto_ManDumpClauses( Sto_Man_t * p, char * pFileName );
+extern Sto_Man_t *  Sto_ManLoadClauses( char * pFileName );
 
 /*=== satInter.c ==========================================================*/
 typedef struct Int_Man_t_ Int_Man_t;
diff --git a/src/sat/bsat/satUtil.c b/src/sat/bsat/satUtil.c
index 76cb2dc2..3001957f 100644
--- a/src/sat/bsat/satUtil.c
+++ b/src/sat/bsat/satUtil.c
@@ -190,7 +190,7 @@ int * Sat_SolverGetModel( sat_solver * p, int * pVars, int nVars )
 ***********************************************************************/
 void Sat_SolverDoubleClauses( sat_solver * p, int iVar )
 {
-    clause ** pClauses;
+    clause * pClause;
     lit Lit, * pLits;
     int RetValue, nClauses, nVarsOld, nLitsOld, nLits, c, v;
     // get the number of variables
@@ -210,11 +210,11 @@ void Sat_SolverDoubleClauses( sat_solver * p, int iVar )
         }
     // duplicate clauses
     nClauses = vecp_size(&p->clauses);
-    pClauses = (clause**)vecp_begin(&p->clauses);
     for ( c = 0; c < nClauses; c++ )
     {
-        nLits = clause_size(pClauses[c]);
-        pLits = clause_begin(pClauses[c]);
+        pClause = p->clauses.ptr[c];
+        nLits = clause_size(pClause);
+        pLits = clause_begin(pClause);
         for ( v = 0; v < nLits; v++ )
             pLits[v] += nLitsOld;
         RetValue = sat_solver_addclause( p, pLits, pLits + nLits );