Version abc80725

34 files changed, 3305 insertions, 1996 deletions

diff --git a/src/aig/aig/aig.h b/src/aig/aig/aig.h
index 84c1e0b5..ef821d12 100644
--- a/src/aig/aig/aig.h
+++ b/src/aig/aig/aig.h
@@ -486,7 +486,7 @@ extern Aig_Man_t *     Aig_ManDupWithoutPos( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupRepres( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManDupRepresDfs( Aig_Man_t * p );
 extern Aig_Man_t *     Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int fImpl );
-extern Aig_Man_t *     Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum );
+extern Aig_Man_t *     Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs );
 /*=== aigFanout.c ==========================================================*/
 extern void            Aig_ObjAddFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
 extern void            Aig_ObjRemoveFanout( Aig_Man_t * p, Aig_Obj_t * pObj, Aig_Obj_t * pFanout );
diff --git a/src/aig/aig/aigCheck.c b/src/aig/aig/aigCheck.c
index bddc9288..4cfdaaf1 100644
--- a/src/aig/aig/aigCheck.c
+++ b/src/aig/aig/aigCheck.c
@@ -17,7 +17,7 @@
   Revision    [$Id: aigCheck.c,v 1.00 2007/04/28 00:00:00 alanmi Exp $]
 
 ***********************************************************************/
-
+ 
 #include "aig.h"
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/aig/aigDup.c b/src/aig/aig/aigDup.c
index db9e7288..c6a4d19a 100644
--- a/src/aig/aig/aigDup.c
+++ b/src/aig/aig/aigDup.c
@@ -905,7 +905,7 @@ Aig_Man_t * Aig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum )
+Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum, int fAddRegs )
 {
     Aig_Man_t * pNew;
     Aig_Obj_t * pObj;
@@ -922,8 +922,8 @@ Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum )
     Aig_ManForEachPi( p, pObj, i )
         pObj->pData = Aig_ObjCreatePi( pNew );
     // set registers
-    pNew->nRegs    = p->nRegs;
-    pNew->nTruePis = p->nTruePis;
+    pNew->nRegs    = fAddRegs? p->nRegs : 0;
+    pNew->nTruePis = fAddRegs? p->nTruePis : p->nTruePis + p->nRegs;
     pNew->nTruePos = 1;
     // duplicate internal nodes
     Aig_ManForEachNode( p, pObj, i )
@@ -932,8 +932,11 @@ Aig_Man_t * Aig_ManDupOneOutput( Aig_Man_t * p, int iPoNum )
     pObj = Aig_ManPo( p, iPoNum );
     Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
     // create register inputs with MUXes
-    Aig_ManForEachLiSeq( p, pObj, i )
-        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    if ( fAddRegs )
+    {
+        Aig_ManForEachLiSeq( p, pObj, i )
+            Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    }
     Aig_ManCleanup( pNew );
     return pNew;
 }
diff --git a/src/aig/bar/bar.c b/src/aig/bar/bar.c
index 8c215b48..13bd9fe7 100644
--- a/src/aig/bar/bar.c
+++ b/src/aig/bar/bar.c
@@ -60,9 +60,9 @@ static void Bar_ProgressClean( Bar_Progress_t * p );
 Bar_Progress_t * Bar_ProgressStart( FILE * pFile, int nItemsTotal )
 {
     Bar_Progress_t * p;
-//    extern int Abc_FrameShowProgress( void * p );
-//    extern void * Abc_FrameGetGlobalFrame();
-//    if ( !Abc_FrameShowProgress(Abc_FrameGetGlobalFrame()) ) return NULL;
+    extern int Abc_FrameShowProgress( void * p );
+    extern void * Abc_FrameGetGlobalFrame();
+    if ( !Abc_FrameShowProgress(Abc_FrameGetGlobalFrame()) ) return NULL;
     p = (Bar_Progress_t *) malloc(sizeof(Bar_Progress_t));
     memset( p, 0, sizeof(Bar_Progress_t) );
     p->pFile       = pFile;
diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 04adb7e3..5944cf56 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -20,6 +20,7 @@
 
 #include "fra.h"
 #include "ioa.h"
+#include "int.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -389,11 +390,15 @@ PRT( "Time", clock() - clkTotal );
 clk = clock();
     if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 )
     {
-        extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth );
+        Inter_ManParams_t Pars, * pPars = &Pars;
         int Depth;
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
         pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
-        RetValue = Saig_Interpolate( pNew, 5000, 40, 0, 1, 0, 0, 0, 1, 1, pParSec->fVeryVerbose, &Depth );
+
+        Inter_ManSetDefaultParams( pPars );
+        pPars->fVerbose = pParSec->fVeryVerbose;
+        RetValue = Inter_ManPerformInterpolation( pNew, pPars, &Depth );
+
         if ( pParSec->fVerbose )
         {
         if ( RetValue == 1 )
@@ -454,7 +459,7 @@ PRT( "Time", clock() - clk );
             iCount++;
             if ( !pParSec->fSilent )
                 printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter );
-            pNew2 = Aig_ManDupOneOutput( pNew, i );
+            pNew2 = Aig_ManDupOneOutput( pNew, i, 1 );
             
             TimeLimitCopy = pParSec->TimeLimit;
             pParSec->TimeLimit = TimeLimit2;
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 53493201..d1d73a03 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -542,6 +542,35 @@ void Fra_SmlNodeSimulate( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
   SeeAlso     []
 
 ***********************************************************************/
+int Fra_SmlNodesCompareInFrame( Fra_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1, int iFrame0, int iFrame1 )
+{
+    unsigned * pSims0, * pSims1;
+    int i;
+    assert( !Aig_IsComplement(pObj0) );
+    assert( !Aig_IsComplement(pObj1) );
+    assert( iFrame0 == 0 || p->nWordsFrame < p->nWordsTotal );
+    assert( iFrame1 == 0 || p->nWordsFrame < p->nWordsTotal );
+    // get hold of the simulation information
+    pSims0  = Fra_ObjSim(p, pObj0->Id) + p->nWordsFrame * iFrame0;
+    pSims1  = Fra_ObjSim(p, pObj1->Id) + p->nWordsFrame * iFrame1;
+    // compare
+    for ( i = 0; i < p->nWordsFrame; i++ )
+        if ( pSims0[i] != pSims1[i] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Fra_SmlNodeCopyFanin( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
 {
     unsigned * pSims, * pSims0;
diff --git a/src/aig/int/int.h b/src/aig/int/int.h
new file mode 100644
index 00000000..bc9c1237
--- /dev/null
+++ b/src/aig/int/int.h
@@ -0,0 +1,85 @@
+/**CFile****************************************************************
+
+  FileName    [int.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Interpolation engine.]
+
+  Synopsis    [External declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 24, 2008.]
+
+  Revision    [$Id: int.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __INT_H__
+#define __INT_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+/* 
+    The interpolation algorithm implemented here was introduced in the paper:
+    K. L. McMillan. Interpolation and SAT-based model checking. CAV’03, pp. 1-13.
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// simulation manager
+typedef struct Inter_ManParams_t_ Inter_ManParams_t;
+struct Inter_ManParams_t_
+{
+    int  nBTLimit;      // limit on the number of conflicts
+    int  nFramesMax;    // the max number timeframes to unroll
+    int  nFramesK;      // the number of timeframes to use in induction
+    int  fRewrite;      // use additional rewriting to simplify timeframes
+    int  fTransLoop;    // add transition into the init state under new PI var
+    int  fUsePudlak;    // use Pudluk interpolation procedure
+    int  fUseOther;     // use other undisclosed option
+    int  fUseMiniSat;   // use MiniSat-1.14p instead of internal proof engine
+    int  fCheckKstep;   // check using K-step induction
+    int  fUseBias;      // bias decisions to global variables
+    int  fUseBackward;  // perform backward interpolation
+    int  fVerbose;      // print verbose statistics
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== intCore.c ==========================================================*/
+extern void       Inter_ManSetDefaultParams( Inter_ManParams_t * p );
+extern int        Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * pDepth );
+
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/int/intContain.c b/src/aig/int/intContain.c
new file mode 100644
index 00000000..fa52e2b6
--- /dev/null
+++ b/src/aig/int/intContain.c
@@ -0,0 +1,328 @@
+/**CFile****************************************************************
+
+  FileName    [intContain.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Interpolation engine.]
+
+  Synopsis    [Interpolant containment checking.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 24, 2008.]
+
+  Revision    [$Id: intContain.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "intInt.h"
+#include "fra.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+extern int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf, int nFrames );
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Checks constainment of two interpolants.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld )
+{
+    Aig_Man_t * pMiter, * pAigTemp;
+    int RetValue;
+    pMiter = Aig_ManCreateMiter( pNew, pOld, 1 );
+//    pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 );
+//    Aig_ManStop( pAigTemp );
+    RetValue = Fra_FraigMiterStatus( pMiter );
+    if ( RetValue == -1 )
+    {
+        pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
+        RetValue = Fra_FraigMiterStatus( pAigTemp );
+        Aig_ManStop( pAigTemp );
+//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 );
+    }
+    assert( RetValue != -1 );
+    Aig_ManStop( pMiter );
+    return RetValue;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks constainment of two interpolants.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld )
+{
+    Aig_Man_t * pMiter, * pAigTemp;
+    int RetValue;
+    pMiter = Aig_ManCreateMiter( pNew, pOld, 0 );
+//    pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 );
+//    Aig_ManStop( pAigTemp );
+    RetValue = Fra_FraigMiterStatus( pMiter );
+    if ( RetValue == -1 )
+    {
+        pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
+        RetValue = Fra_FraigMiterStatus( pAigTemp );
+        Aig_ManStop( pAigTemp );
+//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 );
+    }
+    assert( RetValue != -1 );
+    Aig_ManStop( pMiter );
+    return RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Create timeframes of the manager for interpolation.]
+
+  Description [The resulting manager is combinational. The primary inputs
+  corresponding to register outputs are ordered first.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Inter_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t ** pvMapReg )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, f;
+    assert( Saig_ManRegNum(pAig) > 0 );
+    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
+    // create variables for register outputs
+    *pvMapReg = Vec_PtrAlloc( (nFrames+1) * Saig_ManRegNum(pAig) );
+    Saig_ManForEachLo( pAig, pObj, i )
+    {
+        pObj->pData = Aig_ObjCreatePi( pFrames );
+        Vec_PtrPush( *pvMapReg, pObj->pData );
+    }
+    // add timeframes
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // create PI nodes for this frame
+        Saig_ManForEachPi( pAig, pObj, i )
+            pObj->pData = Aig_ObjCreatePi( pFrames );
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        // save register inputs
+        Saig_ManForEachLi( pAig, pObj, i )
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+        // transfer to register outputs
+        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
+        {
+            pObjLo->pData = pObjLi->pData;
+            Vec_PtrPush( *pvMapReg, pObjLo->pData );
+        }
+    }
+    return pFrames;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicates AIG while mapping PIs into the given array.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Inter_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNewPis, int fCompl )
+{
+    Aig_Obj_t * pObj;
+    int i;
+    assert( Aig_ManPoNum(pOld) == 1 );
+    // create the PIs
+    Aig_ManCleanData( pOld );
+    Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( pOld, pObj, i )
+        pObj->pData = ppNewPis[i];
+    // duplicate internal nodes
+    Aig_ManForEachNode( pOld, pObj, i )
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // add one PO to new
+    pObj = Aig_ManPo( pOld, 0 );
+    Aig_ObjCreatePo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Checks constainment of two interpolants inductively.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t ** ppNodes;
+    Vec_Ptr_t * vMapRegs;
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    int f, nRegs, status;
+    nRegs = Saig_ManRegNum(pTrans);
+    assert( nRegs > 0 );
+    // generate the timeframes 
+    pFrames = Inter_ManFramesLatches( pTrans, nSteps, &vMapRegs );
+    assert( Vec_PtrSize(vMapRegs) == (nSteps + 1) * nRegs );
+    // add main constraints to the timeframes
+    ppNodes = (Aig_Obj_t **)Vec_PtrArray(vMapRegs);
+    if ( fBackward )
+    {
+        // p -> !p -> ... -> !p
+        Inter_ManAppendCone( pInter, pFrames, ppNodes + 0 * nRegs, 1 );
+        for ( f = 1; f <= nSteps; f++ )
+            Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 );
+    }
+    else
+    {
+        // !p -> p -> ... -> p
+        for ( f = 0; f < nSteps; f++ )
+            Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 0 );
+        Inter_ManAppendCone( pInter, pFrames, ppNodes + f * nRegs, 1 );
+    }
+    Vec_PtrFree( vMapRegs );
+    Aig_ManCleanup( pFrames );
+
+    // convert to CNF
+    pCnf = Cnf_Derive( pFrames, 0 ); 
+    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+//    Cnf_DataFree( pCnf );
+//    Aig_ManStop( pFrames );
+
+    if ( pSat == NULL )
+    {
+        Cnf_DataFree( pCnf );
+        Aig_ManStop( pFrames );
+        return 1;
+    }
+
+     // solve the problem
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+
+//    Inter_ManCheckUniqueness( pTrans, pSat, pCnf, nSteps );
+
+    Cnf_DataFree( pCnf );
+    Aig_ManStop( pFrames );
+
+    sat_solver_delete( pSat );
+    return status == l_False;
+}
+
+#include "fra.h"
+
+/**Function*************************************************************
+
+  Synopsis    [Check if cex satisfies uniqueness constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Inter_ManCheckUniqueness( Aig_Man_t * p, sat_solver * pSat, Cnf_Dat_t * pCnf, int nFrames )
+{
+    extern int Fra_SmlNodesCompareInFrame( Fra_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1, int iFrame0, int iFrame1 );
+    extern void Fra_SmlAssignConst( Fra_Sml_t * p, Aig_Obj_t * pObj, int fConst1, int iFrame );
+    extern void Fra_SmlSimulateOne( Fra_Sml_t * p );
+
+    Fra_Sml_t * pSml;
+    Vec_Int_t * vPis;
+    Aig_Obj_t * pObj, * pObj0;
+    int i, k, v, iBit, * pCounterEx;
+    int Counter;
+    if ( nFrames == 1 )
+        return 1;
+    if ( pSat->model.size == 0 )
+        return 1;
+//    assert( Saig_ManPoNum(p) == 1 );
+    assert( Aig_ManRegNum(p) > 0 );
+    assert( Aig_ManRegNum(p) < Aig_ManPiNum(p) );
+
+    // get the counter-example
+    vPis = Vec_IntAlloc( 100 );
+    Aig_ManForEachPi( pCnf->pMan, pObj, k )
+        Vec_IntPush( vPis, pCnf->pVarNums[Aig_ObjId(pObj)] );
+    assert( Vec_IntSize(vPis) == Aig_ManRegNum(p) + nFrames * Saig_ManPiNum(p) );
+    pCounterEx = Sat_SolverGetModel( pSat, vPis->pArray, vPis->nSize );
+    Vec_IntFree( vPis );
+
+    // start a new sequential simulator
+    pSml = Fra_SmlStart( p, 0, nFrames, 1 );
+    // assign simulation info for the registers
+    iBit = 0;
+    Aig_ManForEachLoSeq( p, pObj, i )
+        Fra_SmlAssignConst( pSml, pObj, pCounterEx[iBit++], 0 );
+    // assign simulation info for the primary inputs
+    for ( i = 0; i < nFrames; i++ )
+        Aig_ManForEachPiSeq( p, pObj, k )
+            Fra_SmlAssignConst( pSml, pObj, pCounterEx[iBit++], i );
+    assert( iBit == Aig_ManPiNum(pCnf->pMan) );
+    // run simulation
+    Fra_SmlSimulateOne( pSml );
+
+    // check if the given output has failed
+//    RetValue = !Fra_SmlNodeIsZero( pSml, Aig_ManPo(pAig, 0) );
+//    assert( RetValue );
+
+    // check values at the internal nodes
+    Counter = 0;
+    for ( i = 0; i < nFrames; i++ )
+    for ( k = i+1; k < nFrames; k++ )
+    {
+        for ( v = 0; v < Aig_ManRegNum(p); v++ )
+        {
+            pObj0 = Aig_ManLo(p, v);
+            if ( !Fra_SmlNodesCompareInFrame( pSml, pObj0, pObj0, i, k ) )
+                break;
+        }
+        if ( v == Aig_ManRegNum(p) )
+            Counter++;
+    }
+    printf( "Uniquness does not hold in %d frames.\n", Counter );
+
+    Fra_SmlStop( pSml );
+    free( pCounterEx );
+    return 1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c
new file mode 100644
index 00000000..d959ff07
--- /dev/null
+++ b/src/aig/int/intCore.c
@@ -0,0 +1,286 @@
+/**CFile****************************************************************
+
+  FileName    [intCore.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Interpolation engine.]
+
+  Synopsis    [Core procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 24, 2008.]
+
+  Revision    [$Id: intCore.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "intInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure sets default values of interpolation parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Inter_ManSetDefaultParams( Inter_ManParams_t * p )
+{
+    memset( p, 0, sizeof(Inter_ManParams_t) );
+    p->nBTLimit     = 10000; // limit on the number of conflicts
+    p->nFramesMax   = 40;    // the max number timeframes to unroll
+    p->nFramesK     = 1;     // the number of timeframes to use in induction
+    p->fRewrite     = 0;     // use additional rewriting to simplify timeframes
+    p->fTransLoop   = 1;     // add transition into the init state under new PI var
+    p->fUsePudlak   = 0;     // use Pudluk interpolation procedure
+    p->fUseOther    = 0;     // use other undisclosed option
+    p->fUseMiniSat  = 0;     // use MiniSat-1.14p instead of internal proof engine
+    p->fCheckKstep  = 1;     // check using K-step induction
+    p->fUseBias     = 0;     // bias decisions to global variables
+    p->fUseBackward = 0;     // perform backward interpolation
+    p->fVerbose     = 0;     // print verbose statistics
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Interplates while the number of conflicts is not exceeded.]
+
+  Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
+               
+  SideEffects [Does not check the property in 0-th frame.]
+
+  SeeAlso     []
+
+***********************************************************************/
+int Inter_ManPerformInterpolation( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * pDepth )
+{
+    extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
+    Inter_Man_t * p;
+    Aig_Man_t * pAigTemp;
+    int s, i, RetValue, Status, clk, clk2, clkTotal = clock();
+    // sanity checks
+    assert( Saig_ManRegNum(pAig) > 0 );
+    assert( Saig_ManPiNum(pAig) > 0 );
+    assert( Saig_ManPoNum(pAig) == 1 );
+/*
+    if ( Inter_ManCheckInitialState(pAig) )
+    {
+        printf( "Property trivially fails in the initial state.\n" );
+        return 0;
+    }
+    if ( Inter_ManCheckAllStates(pAig) )
+    {
+        printf( "Property trivially holds in all states.\n" );
+        return 1;
+    }
+*/
+    // create interpolation manager
+    // can perform SAT sweeping and/or rewriting of this AIG...
+    p = Inter_ManCreate( pAig, pPars );
+    if ( pPars->fTransLoop )
+        p->pAigTrans = Inter_ManStartOneOutput( pAig, 0 );
+    else
+        p->pAigTrans = Inter_ManStartDuplicated( pAig );
+    // derive CNF for the transformed AIG
+clk = clock();
+    p->pCnfAig = Cnf_Derive( p->pAigTrans, Aig_ManRegNum(p->pAigTrans) ); 
+p->timeCnf += clock() - clk;    
+    if ( pPars->fVerbose )
+    { 
+        printf( "AIG: PI/PO/Reg = %d/%d/%d. And = %d. Lev = %d.  CNF: Var/Cla = %d/%d.\n",
+            Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig), 
+            Aig_ManAndNum(pAig), Aig_ManLevelNum(pAig),
+            p->pCnfAig->nVars, p->pCnfAig->nClauses );
+    }
+
+    // derive interpolant
+    *pDepth = -1;
+    p->nFrames = 1;
+    for ( s = 0; ; s++ )
+    {
+clk2 = clock();
+        // initial state
+        if ( pPars->fUseBackward )
+            p->pInter = Inter_ManStartOneOutput( pAig, 1 );
+        else
+            p->pInter = Inter_ManStartInitState( Aig_ManRegNum(pAig) );
+        assert( Aig_ManPoNum(p->pInter) == 1 );
+clk = clock();
+        p->pCnfInter = Cnf_Derive( p->pInter, 0 );  
+p->timeCnf += clock() - clk;    
+        // timeframes
+        p->pFrames = Inter_ManFramesInter( pAig, p->nFrames, pPars->fUseBackward );
+clk = clock();
+        if ( pPars->fRewrite )
+        {
+            p->pFrames = Dar_ManRwsat( pAigTemp = p->pFrames, 1, 0 );
+            Aig_ManStop( pAigTemp );
+//        p->pFrames = Fra_FraigEquivence( pAigTemp = p->pFrames, 100, 0 );
+//        Aig_ManStop( pAigTemp );
+        }
+p->timeRwr += clock() - clk;
+        // can also do SAT sweeping on the timeframes...
+clk = clock();
+        if ( pPars->fUseBackward )
+            p->pCnfFrames = Cnf_Derive( p->pFrames, Aig_ManPoNum(p->pFrames) );  
+        else
+            p->pCnfFrames = Cnf_Derive( p->pFrames, 0 );  
+p->timeCnf += clock() - clk;    
+        // report statistics
+        if ( pPars->fVerbose )
+        {
+            printf( "Step = %2d. Frames = 1 + %d. And = %5d. Lev = %5d.  ", 
+                s+1, p->nFrames, Aig_ManNodeNum(p->pFrames), Aig_ManLevelNum(p->pFrames) );
+            PRT( "Time", clock() - clk2 );
+        }
+        // iterate the interpolation procedure
+        for ( i = 0; ; i++ )
+        {
+            if ( p->nFrames + i >= pPars->nFramesMax )
+            { 
+                if ( pPars->fVerbose )
+                    printf( "Reached limit (%d) on the number of timeframes.\n", pPars->nFramesMax );
+                p->timeTotal = clock() - clkTotal;
+                Inter_ManStop( p );
+                return -1;
+            }
+
+            // perform interpolation
+            clk = clock();
+#ifdef ABC_USE_LIBRARIES
+            if ( pPars->fUseMiniSat )
+            {
+                assert( !pPars->fUseBackward );
+                RetValue = Inter_ManPerformOneStepM114p( p, pPars->fUsePudlak, pPars->fUseOther );
+            }
+            else 
+#endif
+                RetValue = Inter_ManPerformOneStep( p, pPars->fUseBias, pPars->fUseBackward );
+
+            if ( pPars->fVerbose )
+            {
+                printf( "   I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d.  ", 
+                    i+1, i + 1 + p->nFrames, Aig_ManNodeNum(p->pInter), Aig_ManLevelNum(p->pInter), p->nConfCur );
+                PRT( "Time", clock() - clk );
+            }
+            if ( RetValue == 0 ) // found a (spurious?) counter-example
+            {
+                if ( i == 0 ) // real counterexample
+                {
+                    if ( pPars->fVerbose )
+                        printf( "Found a real counterexample in the first frame.\n" );
+                    p->timeTotal = clock() - clkTotal;
+                    *pDepth = p->nFrames + 1;
+                    Inter_ManStop( p );
+                    return 0;
+                }
+                // likely spurious counter-example
+                p->nFrames += i;
+                Inter_ManClean( p );
+                break;
+            }
+            else if ( RetValue == -1 ) // timed out
+            {
+                if ( pPars->fVerbose )
+                    printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit );
+                assert( p->nConfCur >= p->nConfLimit );
+                p->timeTotal = clock() - clkTotal;
+                Inter_ManStop( p );
+                return -1;
+            }
+            assert( RetValue == 1 ); // found new interpolant
+            // compress the interpolant
+clk = clock();
+            if ( p->pInterNew )
+            {
+                p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 1, 0 );
+                Aig_ManStop( pAigTemp );
+            }
+p->timeRwr += clock() - clk;
+
+            // check if interpolant is trivial
+            if ( p->pInterNew == NULL || Aig_ObjChild0(Aig_ManPo(p->pInterNew,0)) == Aig_ManConst0(p->pInterNew) )
+            { 
+//                printf( "interpolant is constant 0\n" );
+                if ( pPars->fVerbose )
+                    printf( "The problem is trivially true for all states.\n" );
+                p->timeTotal = clock() - clkTotal;
+                Inter_ManStop( p );
+                return 1;
+            }
+
+            // check containment of interpolants
+clk = clock();
+            if ( pPars->fCheckKstep ) // k-step unique-state induction
+            {
+                if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) )
+                    Status = Inter_ManCheckInductiveContainment( p->pAigTrans, p->pInterNew, pPars->nFramesK, pPars->fUseBackward );
+                else
+                    Status = 0;
+            }
+            else // combinational containment
+            {
+                if ( Aig_ManPiNum(p->pInterNew) == Aig_ManPiNum(p->pInter) )
+                    Status = Inter_ManCheckContainment( p->pInterNew, p->pInter );
+                else
+                    Status = 0;
+            }
+p->timeEqu += clock() - clk;
+            if ( Status ) // contained
+            {
+                if ( pPars->fVerbose )
+                    printf( "Proved containment of interpolants.\n" );
+                p->timeTotal = clock() - clkTotal;
+                Inter_ManStop( p );
+                return 1;
+            }
+            // save interpolant and convert it into CNF
+            if ( pPars->fTransLoop )
+            {
+                Aig_ManStop( p->pInter );
+                p->pInter = p->pInterNew; 
+            }
+            else
+            {
+                p->pInter = Aig_ManCreateMiter( pAigTemp = p->pInter, p->pInterNew, 2 );
+                Aig_ManStop( pAigTemp );
+                Aig_ManStop( p->pInterNew );
+                // compress the interpolant
+clk = clock();
+                p->pInter = Dar_ManRwsat( pAigTemp = p->pInter, 1, 0 );
+                Aig_ManStop( pAigTemp );
+p->timeRwr += clock() - clk;
+            }
+            p->pInterNew = NULL;
+            Cnf_DataFree( p->pCnfInter );
+clk = clock();
+            p->pCnfInter = Cnf_Derive( p->pInter, 0 );  
+p->timeCnf += clock() - clk;
+        }
+    }
+    assert( 0 );
+    return RetValue;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/int/intDup.c b/src/aig/int/intDup.c
new file mode 100644
index 00000000..3e5aaa7e
--- /dev/null
+++ b/src/aig/int/intDup.c
@@ -0,0 +1,161 @@
+/**CFile****************************************************************
+
+  FileName    [intDup.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Interpolation engine.]
+
+  Synopsis    [Specialized AIG duplication procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 24, 2008.]
+
+  Revision    [$Id: intDup.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "intInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Create trivial AIG manager for the init state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Inter_ManStartInitState( int nRegs )
+{
+    Aig_Man_t * p;
+    Aig_Obj_t * pRes;
+    Aig_Obj_t ** ppInputs;
+    int i;
+    assert( nRegs > 0 );
+    ppInputs = ALLOC( Aig_Obj_t *, nRegs );
+    p = Aig_ManStart( nRegs );
+    for ( i = 0; i < nRegs; i++ )
+        ppInputs[i] = Aig_Not( Aig_ObjCreatePi(p) );
+    pRes = Aig_Multi( p, ppInputs, nRegs, AIG_OBJ_AND );
+    Aig_ObjCreatePo( p, pRes );
+    free( ppInputs );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicate the AIG w/o POs.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Inter_ManStartDuplicated( Aig_Man_t * p )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj;
+    int i;
+    assert( Aig_ManRegNum(p) > 0 );
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p, pObj, i )
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    // set registers
+    pNew->nRegs    = p->nRegs;
+    pNew->nTruePis = p->nTruePis;
+    pNew->nTruePos = 0;
+    // duplicate internal nodes
+    Aig_ManForEachNode( p, pObj, i )
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // create register inputs with MUXes
+    Saig_ManForEachLi( p, pObj, i )
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    Aig_ManCleanup( pNew );
+    return pNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Duplicate the AIG w/o POs and transforms to transit into init state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo )
+{
+    Aig_Man_t * pNew;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    Aig_Obj_t * pCtrl = NULL; // Suppress "might be used uninitialized"
+    int i;
+    assert( Aig_ManRegNum(p) > 0 );
+    // create the new manager
+    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
+    pNew->pName = Aig_UtilStrsav( p->pName );
+    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
+    // create the PIs
+    Aig_ManCleanData( p );
+    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
+    Aig_ManForEachPi( p, pObj, i )
+    {
+        if ( i == Saig_ManPiNum(p) )
+            pCtrl = Aig_ObjCreatePi( pNew );
+        pObj->pData = Aig_ObjCreatePi( pNew );
+    }
+    // set registers
+    pNew->nRegs    = fAddFirstPo? 0 : p->nRegs;
+    pNew->nTruePis = fAddFirstPo? Aig_ManPiNum(p) + 1 : p->nTruePis + 1;
+    pNew->nTruePos = fAddFirstPo;
+    // duplicate internal nodes
+    Aig_ManForEachNode( p, pObj, i )
+        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+    // add the PO
+    if ( fAddFirstPo )
+    {
+        pObj = Aig_ManPo( p, 0 );
+        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
+    }
+    else
+    {
+        // create register inputs with MUXes
+        Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
+        {
+            pObj = Aig_Mux( pNew, pCtrl, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) );
+    //        pObj = Aig_Mux( pNew, pCtrl, Aig_ManConst0(pNew), Aig_ObjChild0Copy(pObjLi) );
+            Aig_ObjCreatePo( pNew, pObj );
+        }
+    }
+    Aig_ManCleanup( pNew );
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/int/intFrames.c b/src/aig/int/intFrames.c
new file mode 100644
index 00000000..809cb06b
--- /dev/null
+++ b/src/aig/int/intFrames.c
@@ -0,0 +1,103 @@
+/**CFile****************************************************************
+
+  FileName    [intFrames.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Interpolation engine.]
+
+  Synopsis    [Sequential AIG unrolling for interpolation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 24, 2008.]
+
+  Revision    [$Id: intFrames.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "intInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Create timeframes of the manager for interpolation.]
+
+  Description [The resulting manager is combinational. The primary inputs
+  corresponding to register outputs are ordered first. The only POs of the 
+  manager is the property output of the last timeframe.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts )
+{
+    Aig_Man_t * pFrames;
+    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
+    int i, f;
+    assert( Saig_ManRegNum(pAig) > 0 );
+    assert( Saig_ManPoNum(pAig) == 1 );
+    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
+    // map the constant node
+    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
+    // create variables for register outputs
+    if ( fAddRegOuts )
+    {
+        Saig_ManForEachLo( pAig, pObj, i )
+            pObj->pData = Aig_ManConst0( pFrames );
+    }
+    else
+    {
+        Saig_ManForEachLo( pAig, pObj, i )
+            pObj->pData = Aig_ObjCreatePi( pFrames );
+    }
+    // add timeframes
+    for ( f = 0; f < nFrames; f++ )
+    {
+        // create PI nodes for this frame
+        Saig_ManForEachPi( pAig, pObj, i )
+            pObj->pData = Aig_ObjCreatePi( pFrames );
+        // add internal nodes of this frame
+        Aig_ManForEachNode( pAig, pObj, i )
+            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
+        if ( f == nFrames - 1 )
+            break;
+        // save register inputs
+        Saig_ManForEachLi( pAig, pObj, i )
+            pObj->pData = Aig_ObjChild0Copy(pObj);
+        // transfer to register outputs
+        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
+            pObjLo->pData = pObjLi->pData;
+    }
+    // create POs for each register output
+    if ( fAddRegOuts )
+    {
+        Saig_ManForEachLi( pAig, pObj, i )
+            Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+    }
+    // create the only PO of the manager
+    else
+    {
+        pObj = Aig_ManPo( pAig, 0 );
+        Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
+    }
+    Aig_ManCleanup( pFrames );
+    return pFrames;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/int/intInt.h b/src/aig/int/intInt.h
new file mode 100644
index 00000000..ea2c48b8
--- /dev/null
+++ b/src/aig/int/intInt.h
@@ -0,0 +1,127 @@
+/**CFile****************************************************************
+
+  FileName    [intInt.h]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Interpolation engine.]
+
+  Synopsis    [Internal declarations.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 24, 2008.]
+
+  Revision    [$Id: intInt.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef __INT_INT_H__
+#define __INT_INT_H__
+
+#ifdef __cplusplus
+extern "C" {
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "saig.h"
+#include "cnf.h"
+#include "satSolver.h"
+#include "satStore.h"
+#include "int.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// simulation manager
+typedef struct Inter_Man_t_ Inter_Man_t;
+struct Inter_Man_t_
+{
+    // AIG manager
+    Aig_Man_t *      pAig;         // the original AIG manager
+    Aig_Man_t *      pAigTrans;    // the transformed original AIG manager
+    Cnf_Dat_t *      pCnfAig;      // CNF for the original manager
+    // interpolant
+    Aig_Man_t *      pInter;       // the current interpolant
+    Cnf_Dat_t *      pCnfInter;    // CNF for the current interplant
+    // timeframes
+    Aig_Man_t *      pFrames;      // the timeframes      
+    Cnf_Dat_t *      pCnfFrames;   // CNF for the timeframes 
+    // other data
+    Vec_Int_t *      vVarsAB;      // the variables participating in 
+    // temporary place for the new interpolant
+    Aig_Man_t *      pInterNew;
+    Vec_Ptr_t *      vInters;
+    // parameters
+    int              nFrames;      // the number of timeframes
+    int              nConfCur;     // the current number of conflicts
+    int              nConfLimit;   // the limit on the number of conflicts
+    int              fVerbose;     // the verbosiness flag
+    // runtime
+    int              timeRwr;
+    int              timeCnf;
+    int              timeSat;
+    int              timeInt;
+    int              timeEqu;
+    int              timeOther;
+    int              timeTotal;
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== intContain.c ==========================================================*/
+extern int           Inter_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld );
+extern int           Inter_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld );
+extern int           Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
+
+/*=== intDup.c ==========================================================*/
+extern Aig_Man_t *   Inter_ManStartInitState( int nRegs );
+extern Aig_Man_t *   Inter_ManStartDuplicated( Aig_Man_t * p );
+extern Aig_Man_t *   Inter_ManStartOneOutput( Aig_Man_t * p, int fAddFirstPo );
+
+/*=== intFrames.c ==========================================================*/
+extern Aig_Man_t *   Inter_ManFramesInter( Aig_Man_t * pAig, int nFrames, int fAddRegOuts );
+
+/*=== intMan.c ==========================================================*/
+extern Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars );
+extern void          Inter_ManClean( Inter_Man_t * p );
+extern void          Inter_ManStop( Inter_Man_t * p );
+
+/*=== intM114.c ==========================================================*/
+extern int           Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward );
+
+/*=== intM114p.c ==========================================================*/
+#ifdef ABC_USE_LIBRARIES
+extern int           Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther );
+#endif
+
+/*=== intUtil.c ==========================================================*/
+extern int           Inter_ManCheckInitialState( Aig_Man_t * p );
+extern int           Inter_ManCheckAllStates( Aig_Man_t * p );
+
+#ifdef __cplusplus
+}
+#endif
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/aig/int/intInter.c b/src/aig/int/intInter.c
new file mode 100644
index 00000000..592eedcf
--- /dev/null
+++ b/src/aig/int/intInter.c
@@ -0,0 +1,140 @@
+/**CFile****************************************************************
+
+  FileName    [intInter.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Interpolation engine.]
+
+  Synopsis    [Experimental procedures to derive and compare interpolants.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 24, 2008.]
+
+  Revision    [$Id: intInter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "intInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Inter_ManDupExpand( Aig_Man_t * pInter, Aig_Man_t * pOther )
+{
+    Aig_Man_t * pInterC;
+    assert( Aig_ManPiNum(pInter) <= Aig_ManPiNum(pOther) );
+    pInterC = Aig_ManDupSimple( pInter );
+    Aig_IthVar( pInterC, Aig_ManPiNum(pOther)-1 );
+    assert( Aig_ManPiNum(pInterC) == Aig_ManPiNum(pOther) );
+    return pInterC;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Inter_ManVerifyInterpolant1( Inta_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter )
+{
+    extern Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA );
+    Aig_Man_t * pLower, * pUpper, * pInterC;
+    int RetValue1, RetValue2;
+
+    pLower = Inta_ManDeriveClauses( pMan, pCnf, 1 );
+    pUpper = Inta_ManDeriveClauses( pMan, pCnf, 0 );
+    Aig_ManFlipFirstPo( pUpper );
+
+    pInterC = Inter_ManDupExpand( pInter, pLower );
+    RetValue1 = Inter_ManCheckContainment( pLower, pInterC );
+    Aig_ManStop( pInterC );
+
+    pInterC = Inter_ManDupExpand( pInter, pUpper );
+    RetValue2 = Inter_ManCheckContainment( pInterC, pUpper );
+    Aig_ManStop( pInterC );
+    
+    if ( RetValue1 && RetValue2 )
+        printf( "Im is correct.\n" );
+    if ( !RetValue1 )
+        printf( "Property A => Im fails.\n" );
+    if ( !RetValue2 )
+        printf( "Property Im => !B fails.\n" );
+
+    Aig_ManStop( pLower );
+    Aig_ManStop( pUpper );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Inter_ManVerifyInterpolant2( Intb_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter )
+{
+    extern Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA );
+    Aig_Man_t * pLower, * pUpper, * pInterC;
+    int RetValue1, RetValue2;
+
+    pLower = Intb_ManDeriveClauses( pMan, pCnf, 1 );
+    pUpper = Intb_ManDeriveClauses( pMan, pCnf, 0 );
+    Aig_ManFlipFirstPo( pUpper );
+
+    pInterC = Inter_ManDupExpand( pInter, pLower );
+//Aig_ManPrintStats( pLower );
+//Aig_ManPrintStats( pUpper );
+//Aig_ManPrintStats( pInterC );
+//Aig_ManDumpBlif( pInterC, "inter_c.blif", NULL, NULL );
+    RetValue1 = Inter_ManCheckContainment( pLower, pInterC );
+    Aig_ManStop( pInterC );
+
+    pInterC = Inter_ManDupExpand( pInter, pUpper );
+    RetValue2 = Inter_ManCheckContainment( pInterC, pUpper );
+    Aig_ManStop( pInterC );
+    
+    if ( RetValue1 && RetValue2 )
+        printf( "Ip is correct.\n" );
+    if ( !RetValue1 )
+        printf( "Property A => Ip fails.\n" );
+    if ( !RetValue2 )
+        printf( "Property Ip => !B fails.\n" );
+
+    Aig_ManStop( pLower );
+    Aig_ManStop( pUpper );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/int/intM114.c b/src/aig/int/intM114.c
new file mode 100644
index 00000000..f92ba179
--- /dev/null
+++ b/src/aig/int/intM114.c
@@ -0,0 +1,311 @@
+/**CFile****************************************************************
+
+  FileName    [intM114.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Interpolation engine.]
+
+  Synopsis    [Intepolation using ABC's proof generator added to MiniSat-1.14c.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 24, 2008.]
+
+  Revision    [$Id: intM114.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "intInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the SAT solver for one interpolation run.]
+
+  Description [pInter is the previous interpolant. pAig is one time frame.
+  pFrames is the unrolled time frames.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+sat_solver * Inter_ManDeriveSatSolver( 
+    Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter, 
+    Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig, 
+    Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames, 
+    Vec_Int_t * vVarsAB, int fUseBackward )
+{
+    sat_solver * pSat;
+    Aig_Obj_t * pObj, * pObj2;
+    int i, Lits[2];
+
+//Aig_ManDumpBlif( pInter,  "out_inter.blif", NULL, NULL );
+//Aig_ManDumpBlif( pAig,    "out_aig.blif", NULL, NULL );
+//Aig_ManDumpBlif( pFrames, "out_frames.blif", NULL, NULL );
+
+    // sanity checks
+    assert( Aig_ManRegNum(pInter) == 0 );
+    assert( Aig_ManRegNum(pAig) > 0 );
+    assert( Aig_ManRegNum(pFrames) == 0 );
+    assert( Aig_ManPoNum(pInter) == 1 );
+    assert( Aig_ManPoNum(pFrames) == fUseBackward? Saig_ManRegNum(pAig) : 1 );
+    assert( fUseBackward || Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) );
+//    assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
+
+    // prepare CNFs
+    Cnf_DataLift( pCnfAig,   pCnfFrames->nVars );
+    Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars );
+
+    // start the solver
+    pSat = sat_solver_new();
+    sat_solver_store_alloc( pSat );
+    sat_solver_setnvars( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars );
+
+    // add clauses of A
+    // interpolant
+    for ( i = 0; i < pCnfInter->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) )
+        {
+            sat_solver_delete( pSat );
+            // return clauses to the original state
+            Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
+            Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
+            return NULL;
+        }
+    }
+    // connector clauses
+    if ( fUseBackward )
+    {
+        Saig_ManForEachLi( pAig, pObj2, i )
+        {
+            if ( Saig_ManRegNum(pAig) == Aig_ManPiNum(pInter) )
+                pObj = Aig_ManPi( pInter, i );
+            else
+            {
+                assert( Aig_ManPiNum(pAig) == Aig_ManPiNum(pInter) );
+                pObj = Aig_ManPi( pInter, Aig_ManPiNum(pAig)-Saig_ManRegNum(pAig) + i );
+            }
+
+            Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
+            Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
+            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+                assert( 0 );
+            Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
+            Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
+            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+                assert( 0 );
+        }
+    }
+    else
+    {
+        Aig_ManForEachPi( pInter, pObj, i )
+        {
+            pObj2 = Saig_ManLo( pAig, i );
+
+            Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
+            Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
+            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+                assert( 0 );
+            Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
+            Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
+            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+                assert( 0 );
+        }
+    }
+    // one timeframe
+    for ( i = 0; i < pCnfAig->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) )
+            assert( 0 );
+    }
+    // connector clauses
+    Vec_IntClear( vVarsAB );
+    if ( fUseBackward )
+    {
+        Aig_ManForEachPo( pFrames, pObj, i )
+        {
+            assert( pCnfFrames->pVarNums[pObj->Id] >= 0 );
+            Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
+
+            pObj2 = Saig_ManLo( pAig, i );
+            Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
+            Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
+            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+                assert( 0 );
+            Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
+            Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
+            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+                assert( 0 );
+        }
+    }
+    else
+    {
+        Aig_ManForEachPi( pFrames, pObj, i )
+        {
+            if ( i == Aig_ManRegNum(pAig) )
+                break;
+            Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
+
+            pObj2 = Saig_ManLi( pAig, i );
+            Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
+            Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
+            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+                assert( 0 );
+            Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
+            Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
+            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
+                assert( 0 );
+        }
+    }
+    // add clauses of B
+    sat_solver_store_mark_clauses_a( pSat );
+    for ( i = 0; i < pCnfFrames->nClauses; i++ )
+    {
+        if ( !sat_solver_addclause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) )
+        {
+            pSat->fSolved = 1;
+            break;
+        }
+    }
+    sat_solver_store_mark_roots( pSat );
+    // return clauses to the original state
+    Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
+    Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
+    return pSat;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one SAT run with interpolation.]
+
+  Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward )
+{
+    sat_solver * pSat;
+    void * pSatCnf = NULL;
+    Inta_Man_t * pManInterA; 
+//    Intb_Man_t * pManInterB; 
+    int * pGlobalVars;
+    int clk, status, RetValue;
+    int i, Var;
+    assert( p->pInterNew == NULL );
+
+    // derive the SAT solver
+    pSat = Inter_ManDeriveSatSolver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB, fUseBackward );
+    if ( pSat == NULL )
+    {
+        p->pInterNew = NULL;
+        return 1;
+    }
+
+    // collect global variables
+    pGlobalVars = CALLOC( int, sat_solver_nvars(pSat) );
+    Vec_IntForEachEntry( p->vVarsAB, Var, i )
+        pGlobalVars[Var] = 1;
+    pSat->pGlobalVars = fUseBias? pGlobalVars : NULL;
+
+    // solve the problem
+clk = clock();
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
+    p->nConfCur = pSat->stats.conflicts;
+p->timeSat += clock() - clk;
+
+    pSat->pGlobalVars = NULL;
+    FREE( pGlobalVars );
+    if ( status == l_False )
+    {
+        pSatCnf = sat_solver_store_release( pSat );
+        RetValue = 1;
+    }
+    else if ( status == l_True )
+    {
+        RetValue = 0;
+    } 
+    else
+    {
+        RetValue = -1;
+    }
+    sat_solver_delete( pSat );
+    if ( pSatCnf == NULL )
+        return RetValue;
+
+    // create the resulting manager
+clk = clock();
+/*
+    if ( !fUseIp )
+    {
+        pManInterA = Inta_ManAlloc();
+        p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
+        Inta_ManFree( pManInterA );
+    }
+    else
+    {
+        Aig_Man_t * pInterNew2;
+        int RetValue;
+
+        pManInterA = Inta_ManAlloc();
+        p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
+//        Inter_ManVerifyInterpolant1( pManInterA, pSatCnf, p->pInterNew );
+        Inta_ManFree( pManInterA );
+
+        pManInterB = Intb_ManAlloc();
+        pInterNew2 = Intb_ManInterpolate( pManInterB, pSatCnf, p->vVarsAB, 0 );
+        Inter_ManVerifyInterpolant2( pManInterB, pSatCnf, pInterNew2 );
+        Intb_ManFree( pManInterB );
+
+        // check relationship
+        RetValue = Inter_ManCheckEquivalence( pInterNew2, p->pInterNew );
+        if ( RetValue )
+            printf( "Equivalence \"Ip == Im\" holds\n" );
+        else
+        {
+//            printf( "Equivalence \"Ip == Im\" does not hold\n" );
+            RetValue = Inter_ManCheckContainment( pInterNew2, p->pInterNew );
+            if ( RetValue )
+                printf( "Containment \"Ip -> Im\" holds\n" );
+            else
+                printf( "Containment \"Ip -> Im\" does not hold\n" );
+
+            RetValue = Inter_ManCheckContainment( p->pInterNew, pInterNew2 );
+            if ( RetValue )
+                printf( "Containment \"Im -> Ip\" holds\n" );
+            else
+                printf( "Containment \"Im -> Ip\" does not hold\n" );
+        }
+
+        Aig_ManStop( pInterNew2 );
+    }
+*/
+
+    pManInterA = Inta_ManAlloc();
+    p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
+    Inta_ManFree( pManInterA );
+
+p->timeInt += clock() - clk;
+    Sto_ManFree( pSatCnf );
+    return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/int/intM114p.c b/src/aig/int/intM114p.c
new file mode 100644
index 00000000..69c643ae
--- /dev/null
+++ b/src/aig/int/intM114p.c
@@ -0,0 +1,435 @@
+/**CFile****************************************************************
+
+  FileName    [intM114p.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Interpolation engine.]
+
+  Synopsis    [Intepolation using interfaced to MiniSat-1.14p.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 24, 2008.]
+
+  Revision    [$Id: intM114p.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#ifdef ABC_USE_LIBRARIES
+
+#include "intInt.h"
+#include "m114p.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the SAT solver for one interpolation run.]
+
+  Description [pInter is the previous interpolant. pAig is one time frame.
+  pFrames is the unrolled time frames.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+M114p_Solver_t Inter_ManDeriveSatSolverM114p( 
+    Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter, 
+    Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig, 
+    Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames, 
+    Vec_Int_t ** pvMapRoots, Vec_Int_t ** pvMapVars )
+{
+    M114p_Solver_t pSat;
+    Aig_Obj_t * pObj, * pObj2;
+    int i, Lits[2];
+
+    // sanity checks
+    assert( Aig_ManRegNum(pInter) == 0 );
+    assert( Aig_ManRegNum(pAig) > 0 );
+    assert( Aig_ManRegNum(pFrames) == 0 );
+    assert( Aig_ManPoNum(pInter) == 1 );
+    assert( Aig_ManPoNum(pFrames) == 1 );
+    assert( Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) );
+//    assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
+
+    // prepare CNFs
+    Cnf_DataLift( pCnfAig,   pCnfFrames->nVars );
+    Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars );
+
+    *pvMapRoots = Vec_IntAlloc( 10000 );
+    *pvMapVars = Vec_IntAlloc( 0 );
+    Vec_IntFill( *pvMapVars, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars, -1 );
+    for ( i = 0; i < pCnfFrames->nVars; i++ )
+        Vec_IntWriteEntry( *pvMapVars, i, -2 );
+
+    // start the solver
+    pSat = M114p_SolverNew( 1 );
+    M114p_SolverSetVarNum( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars );
+
+    // add clauses of A
+    // interpolant
+    for ( i = 0; i < pCnfInter->nClauses; i++ )
+    {
+        Vec_IntPush( *pvMapRoots, 0 );
+        if ( !M114p_SolverAddClause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) )
+            assert( 0 );
+    }
+    // connector clauses
+    Aig_ManForEachPi( pInter, pObj, i )
+    {
+        pObj2 = Saig_ManLo( pAig, i );
+        Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
+        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
+        Vec_IntPush( *pvMapRoots, 0 );
+        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+        Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
+        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
+        Vec_IntPush( *pvMapRoots, 0 );
+        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+    }
+    // one timeframe
+    for ( i = 0; i < pCnfAig->nClauses; i++ )
+    {
+        Vec_IntPush( *pvMapRoots, 0 );
+        if ( !M114p_SolverAddClause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) )
+            assert( 0 );
+    }
+    // connector clauses
+    Aig_ManForEachPi( pFrames, pObj, i )
+    {
+        if ( i == Aig_ManRegNum(pAig) )
+            break;
+//        Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
+        Vec_IntWriteEntry( *pvMapVars, pCnfFrames->pVarNums[pObj->Id], i );
+
+        pObj2 = Saig_ManLi( pAig, i );
+        Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
+        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
+        Vec_IntPush( *pvMapRoots, 0 );
+        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+        Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
+        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
+        Vec_IntPush( *pvMapRoots, 0 );
+        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
+            assert( 0 );
+    }
+    // add clauses of B
+    for ( i = 0; i < pCnfFrames->nClauses; i++ )
+    {
+        Vec_IntPush( *pvMapRoots, 1 );
+        if ( !M114p_SolverAddClause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) )
+        {
+//            assert( 0 );
+            break;
+        }
+    }
+    // return clauses to the original state
+    Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
+    Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
+    return pSat;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one resolution step.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Inter_ManResolveM114p( Vec_Int_t * vResolvent, int * pLits, int nLits, int iVar )
+{
+    int i, k, iLit = -1, fFound = 0;
+    // find the variable in the clause
+    for ( i = 0; i < vResolvent->nSize; i++ )
+        if ( lit_var(vResolvent->pArray[i]) == iVar )
+        {
+            iLit = vResolvent->pArray[i];
+            vResolvent->pArray[i] = vResolvent->pArray[--vResolvent->nSize];
+            break;
+        }
+    assert( iLit != -1 );
+    // add other variables
+    for ( i = 0; i < nLits; i++ )
+    {
+        if ( lit_var(pLits[i]) == iVar )
+        {
+            assert( iLit == lit_neg(pLits[i]) );
+            fFound = 1;
+            continue;
+        }
+        // check if this literal appears
+        for ( k = 0; k < vResolvent->nSize; k++ )
+            if ( vResolvent->pArray[k] == pLits[i] )
+                break;
+        if ( k < vResolvent->nSize )
+            continue;
+        // add this literal
+        Vec_IntPush( vResolvent, pLits[i] );
+    }
+    assert( fFound );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes interpolant using MiniSat-1.14p.]
+
+  Description [Assumes that the solver returned UNSAT and proof
+  logging was enabled. Array vMapRoots maps number of each root clause 
+  into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
+  solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
+  where <num> is the var's 0-based number in the ordering of C variables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Inter_ManInterpolateM114pPudlak( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
+{
+    Aig_Man_t * p;
+    Aig_Obj_t * pInter, * pInter2, * pVar;
+    Vec_Ptr_t * vInters;
+    Vec_Int_t * vLiterals, * vClauses, * vResolvent;
+    int * pLitsNext, nLitsNext, nOffset, iLit;
+    int * pLits, * pClauses, * pVars;
+    int nLits, nVars, i, k, v, iVar;
+    assert( M114p_SolverProofIsReady(s) );
+    vInters = Vec_PtrAlloc( 1000 );
+
+    vLiterals = Vec_IntAlloc( 10000 );
+    vClauses = Vec_IntAlloc( 1000 );
+    vResolvent = Vec_IntAlloc( 100 );
+
+    // create elementary variables
+    p = Aig_ManStart( 10000 );
+    Vec_IntForEachEntry( vMapVars, iVar, i )
+        if ( iVar >= 0 )
+            Aig_IthVar(p, iVar);
+    // process root clauses
+    M114p_SolverForEachRoot( s, &pLits, nLits, i )
+    {
+        if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
+            pInter = Aig_ManConst1(p);
+        else // clause of A
+            pInter = Aig_ManConst0(p);
+        Vec_PtrPush( vInters, pInter );
+
+        // save the root clause
+        Vec_IntPush( vClauses, Vec_IntSize(vLiterals) );
+        Vec_IntPush( vLiterals, nLits );
+        for ( v = 0; v < nLits; v++ )
+            Vec_IntPush( vLiterals, pLits[v] );
+    }
+    assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );
+
+    // process learned clauses
+    M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
+    {
+        pInter = Vec_PtrEntry( vInters, pClauses[0] );
+
+        // initialize the resolvent
+        nOffset = Vec_IntEntry( vClauses, pClauses[0] );
+        nLitsNext = Vec_IntEntry( vLiterals, nOffset );
+        pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1;
+        Vec_IntClear( vResolvent );
+        for ( v = 0; v < nLitsNext; v++ )
+            Vec_IntPush( vResolvent, pLitsNext[v] );
+
+        for ( k = 0; k < nVars; k++ )
+        {
+            iVar = Vec_IntEntry( vMapVars, pVars[k] );
+            pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );
+
+            // resolve it with the next clause
+            nOffset = Vec_IntEntry( vClauses, pClauses[k+1] );
+            nLitsNext = Vec_IntEntry( vLiterals, nOffset );
+            pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1;
+            Inter_ManResolveM114p( vResolvent, pLitsNext, nLitsNext, pVars[k] );
+
+            if ( iVar == -1 ) // var of A
+                pInter = Aig_Or( p, pInter, pInter2 );
+            else if ( iVar == -2 ) // var of B
+                pInter = Aig_And( p, pInter, pInter2 );
+            else // var of C
+            {
+                // check polarity of the pivot variable in the clause
+                for ( v = 0; v < nLitsNext; v++ )
+                    if ( lit_var(pLitsNext[v]) == pVars[k] )
+                        break;
+                assert( v < nLitsNext );
+                pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLitsNext[v]) );
+                pInter = Aig_Mux( p, pVar, pInter, pInter2 );
+            }
+        }
+        Vec_PtrPush( vInters, pInter );
+
+        // store the resulting clause
+        Vec_IntPush( vClauses, Vec_IntSize(vLiterals) );
+        Vec_IntPush( vLiterals, Vec_IntSize(vResolvent) );
+        Vec_IntForEachEntry( vResolvent, iLit, v )
+            Vec_IntPush( vLiterals, iLit );
+    }
+    assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
+    assert( Vec_IntSize(vResolvent) == 0 ); // the empty clause
+    Vec_PtrFree( vInters );
+    Vec_IntFree( vLiterals );
+    Vec_IntFree( vClauses );
+    Vec_IntFree( vResolvent );
+    Aig_ObjCreatePo( p, pInter );
+    Aig_ManCleanup( p );
+    return p;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Computes interpolant using MiniSat-1.14p.]
+
+  Description [Assumes that the solver returned UNSAT and proof
+  logging was enabled. Array vMapRoots maps number of each root clause 
+  into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
+  solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
+  where <num> is the var's 0-based number in the ordering of C variables.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Inter_ManpInterpolateM114( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
+{
+    Aig_Man_t * p;
+    Aig_Obj_t * pInter, * pInter2, * pVar;
+    Vec_Ptr_t * vInters;
+    int * pLits, * pClauses, * pVars;
+    int nLits, nVars, i, k, iVar;
+
+    assert( M114p_SolverProofIsReady(s) );
+
+    vInters = Vec_PtrAlloc( 1000 );
+    // process root clauses
+    p = Aig_ManStart( 10000 );
+    M114p_SolverForEachRoot( s, &pLits, nLits, i )
+    {
+        if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
+            pInter = Aig_ManConst1(p);
+        else // clause of A
+        {
+            pInter = Aig_ManConst0(p);
+            for ( k = 0; k < nLits; k++ )
+            {
+                iVar = Vec_IntEntry( vMapVars, lit_var(pLits[k]) );
+                if ( iVar < 0 ) // var of A or B
+                    continue;
+                // this is a variable of C
+                pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLits[k]) );
+                pInter = Aig_Or( p, pInter, pVar );
+            }
+        }
+        Vec_PtrPush( vInters, pInter );
+    }
+//    assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );
+
+    // process learned clauses
+    M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
+    {
+        pInter = Vec_PtrEntry( vInters, pClauses[0] );
+        for ( k = 0; k < nVars; k++ )
+        {
+            iVar = Vec_IntEntry( vMapVars, pVars[k] );
+            pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );
+            if ( iVar == -1 ) // var of A
+                pInter = Aig_Or( p, pInter, pInter2 );
+            else // var of B or C
+                pInter = Aig_And( p, pInter, pInter2 );
+        }
+        Vec_PtrPush( vInters, pInter );
+    }
+
+    assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
+    Vec_PtrFree( vInters );
+    Aig_ObjCreatePo( p, pInter );
+    Aig_ManCleanup( p );
+    assert( Aig_ManCheck(p) );
+    return p;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs one SAT run with interpolation.]
+
+  Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Inter_ManPerformOneStepM114p( Inter_Man_t * p, int fUsePudlak, int fUseOther )
+{
+    M114p_Solver_t pSat;
+    Vec_Int_t * vMapRoots, * vMapVars;
+    int clk, status, RetValue;
+    assert( p->pInterNew == NULL );
+    // derive the SAT solver
+    pSat = Inter_ManDeriveSatSolverM114p( p->pInter, p->pCnfInter, 
+        p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, 
+        &vMapRoots, &vMapVars );
+    // solve the problem
+clk = clock();
+    status = M114p_SolverSolve( pSat, NULL, NULL, 0 );
+    p->nConfCur = M114p_SolverGetConflictNum( pSat );
+p->timeSat += clock() - clk;
+    if ( status == 0 )
+    {
+        RetValue = 1;
+//        Inter_ManpInterpolateM114Report( pSat, vMapRoots, vMapVars );
+
+clk = clock();
+        if ( fUsePudlak )
+            p->pInterNew = Inter_ManInterpolateM114pPudlak( pSat, vMapRoots, vMapVars );
+        else
+            p->pInterNew = Inter_ManpInterpolateM114( pSat, vMapRoots, vMapVars );
+p->timeInt += clock() - clk;
+    }
+    else if ( status == 1 )
+    {
+        RetValue = 0;
+    }
+    else
+    {
+        RetValue = -1;
+    }
+    M114p_SolverDelete( pSat );
+    Vec_IntFree( vMapRoots );
+    Vec_IntFree( vMapVars );
+    return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+#endif
+
+
diff --git a/src/aig/int/intMan.c b/src/aig/int/intMan.c
new file mode 100644
index 00000000..b9b2bce9
--- /dev/null
+++ b/src/aig/int/intMan.c
@@ -0,0 +1,128 @@
+/**CFile****************************************************************
+
+  FileName    [intMan.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Interpolation engine.]
+
+  Synopsis    [Interpolation manager procedures.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 24, 2008.]
+
+  Revision    [$Id: intMan.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "intInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the interpolation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Inter_Man_t * Inter_ManCreate( Aig_Man_t * pAig, Inter_ManParams_t * pPars )
+{
+    Inter_Man_t * p;
+    // create interpolation manager
+    p = ALLOC( Inter_Man_t, 1 );
+    memset( p, 0, sizeof(Inter_Man_t) );
+    p->vVarsAB = Vec_IntAlloc( Aig_ManRegNum(pAig) );
+    p->nConfLimit = pPars->nBTLimit;
+    p->fVerbose = pPars->fVerbose;
+    p->pAig = pAig;   
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the interpolation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Inter_ManClean( Inter_Man_t * p )
+{
+    if ( p->pCnfInter )
+        Cnf_DataFree( p->pCnfInter );
+    if ( p->pCnfFrames )
+        Cnf_DataFree( p->pCnfFrames );
+    if ( p->pInter )
+        Aig_ManStop( p->pInter );
+    if ( p->pFrames )
+        Aig_ManStop( p->pFrames );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Frees the interpolation manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Inter_ManStop( Inter_Man_t * p )
+{
+    if ( p->fVerbose )
+    {
+        p->timeOther = p->timeTotal-p->timeRwr-p->timeCnf-p->timeSat-p->timeInt-p->timeEqu;
+        printf( "Runtime statistics:\n" );
+        PRTP( "Rewriting  ", p->timeRwr,   p->timeTotal );
+        PRTP( "CNF mapping", p->timeCnf,   p->timeTotal );
+        PRTP( "SAT solving", p->timeSat,   p->timeTotal );
+        PRTP( "Interpol   ", p->timeInt,   p->timeTotal );
+        PRTP( "Containment", p->timeEqu,   p->timeTotal );
+        PRTP( "Other      ", p->timeOther, p->timeTotal );
+        PRTP( "TOTAL      ", p->timeTotal, p->timeTotal );
+    }
+
+    if ( p->pCnfAig )
+        Cnf_DataFree( p->pCnfAig );
+    if ( p->pCnfFrames )
+        Cnf_DataFree( p->pCnfFrames );
+    if ( p->pCnfInter )
+        Cnf_DataFree( p->pCnfInter );
+    Vec_IntFree( p->vVarsAB );
+    if ( p->pAigTrans )
+        Aig_ManStop( p->pAigTrans );
+    if ( p->pFrames )
+        Aig_ManStop( p->pFrames );
+    if ( p->pInter )
+        Aig_ManStop( p->pInter );
+    if ( p->pInterNew )
+        Aig_ManStop( p->pInterNew );
+    free( p );
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/int/intUtil.c b/src/aig/int/intUtil.c
new file mode 100644
index 00000000..722a3611
--- /dev/null
+++ b/src/aig/int/intUtil.c
@@ -0,0 +1,92 @@
+/**CFile****************************************************************
+
+  FileName    [intUtil.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Interpolation engine.]
+
+  Synopsis    [Various interpolation utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 24, 2008.]
+
+  Revision    [$Id: intUtil.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "intInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the property fails in the initial state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Inter_ManCheckInitialState( Aig_Man_t * p )
+{
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    int status;
+    int clk = clock();
+    pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); 
+    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 1 );
+    Cnf_DataFree( pCnf );
+    if ( pSat == NULL )
+        return 0;
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+    sat_solver_delete( pSat );
+    PRT( "Time", clock() - clk );
+    return status == l_True;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if the property holds in all states.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Inter_ManCheckAllStates( Aig_Man_t * p )
+{
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    int status;
+    int clk = clock();
+    pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); 
+    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    Cnf_DataFree( pCnf );
+    if ( pSat == NULL )
+        return 1;
+    status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
+    sat_solver_delete( pSat );
+    PRT( "Time", clock() - clk );
+    return status == l_False;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/aig/int/module.make b/src/aig/int/module.make
new file mode 100644
index 00000000..0652ab39
--- /dev/null
+++ b/src/aig/int/module.make
@@ -0,0 +1,9 @@
+SRC +=    src/aig/int/intContain.c \
+    src/aig/int/intCore.c \
+    src/aig/int/intDup.c \
+    src/aig/int/intFrames.c \
+    src/aig/int/intInter.c \
+    src/aig/int/intM114.c \
+    src/aig/int/intM114p.c \
+    src/aig/int/intMan.c \
+    src/aig/int/intUtil.c
diff --git a/src/aig/ntl/ntlExtract.c b/src/aig/ntl/ntlExtract.c
index 79cd640a..3ef1d60e 100644
--- a/src/aig/ntl/ntlExtract.c
+++ b/src/aig/ntl/ntlExtract.c
@@ -803,8 +803,8 @@ Nwk_Man_t * Ntl_ManExtractNwk( Ntl_Man_t * p, Aig_Man_t * pAig, Tim_Man_t * pMan
         pNtk->pManTime = Tim_ManDup( pManTime, 0 );
     else
         pNtk->pManTime = Tim_ManDup( p->pManTime, 0 );
-//    Nwk_ManRemoveDupFanins( pNtk, 0 );
-//    assert( Nwk_ManCheck( pNtk ) );
+    Nwk_ManRemoveDupFanins( pNtk, 0 );
+    assert( Nwk_ManCheck( pNtk ) );
     return pNtk;
 }
 
diff --git a/src/aig/ntl/ntlFraig.c b/src/aig/ntl/ntlFraig.c
index bd39956e..38568d26 100644
--- a/src/aig/ntl/ntlFraig.c
+++ b/src/aig/ntl/ntlFraig.c
@@ -145,13 +145,20 @@ void Ntl_ManReduce( Ntl_Man_t * p, Aig_Man_t * pAig )
             continue;
         assert( pObj != pObjRepr );
         pNet = pObj->pData;
-        // do not reduce the net if it is driven by a multi-output box
-        if ( Ntl_ObjIsBox(pNet->pDriver) && Ntl_ObjFanoutNum(pNet->pDriver) > 1 )
-            continue;
-        // do not reduce the net if it has no-merge attribute
-        if ( Ntl_ObjIsBox(pNet->pDriver) && pNet->pDriver->pImplem->attrNoMerge )
-            continue;
         pNetRepr = pObjRepr->pData;
+        // consider special cases, when the net should not be reduced
+        if ( Ntl_ObjIsBox(pNet->pDriver) )
+        {
+            // do not reduce the net if it is driven by a multi-output box
+            if ( Ntl_ObjFanoutNum(pNet->pDriver) > 1 )
+                continue;
+            // do not reduce the net if it has no-merge attribute
+            if ( pNet->pDriver->pImplem->attrNoMerge )
+                continue;
+            // do not reduce the net if the replacement net has no-merge attribute
+            if ( pNetRepr != NULL && pNetRepr->pDriver->pImplem->attrNoMerge )
+                continue;
+        }
         if ( pNetRepr == NULL )
         {
             // this is the constant node
diff --git a/src/aig/saig/module.make b/src/aig/saig/module.make
index b9a18ce2..5a0f98da 100644
--- a/src/aig/saig/module.make
+++ b/src/aig/saig/module.make
@@ -1,7 +1,6 @@
 SRC +=    src/aig/saig/saigBmc.c \
     src/aig/saig/saigCone.c \
     src/aig/saig/saigHaig.c \
-    src/aig/saig/saigInter.c \
     src/aig/saig/saigIoa.c \
     src/aig/saig/saigMiter.c \
     src/aig/saig/saigPhase.c \
@@ -9,5 +8,4 @@ SRC +=    src/aig/saig/saigBmc.c \
     src/aig/saig/saigRetMin.c \
     src/aig/saig/saigRetStep.c \
     src/aig/saig/saigScl.c \
-    src/aig/saig/saigTrans.c \
-    src/aig/saig/saigUnique.c
+    src/aig/saig/saigTrans.c
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h
index e2fbda2d..88cc2c2d 100644
--- a/src/aig/saig/saig.h
+++ b/src/aig/saig/saig.h
@@ -30,6 +30,7 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 
 #include "aig.h"
+#include "int.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                         PARAMETERS                               ///
@@ -85,7 +86,7 @@ extern Aig_Man_t *       Saig_ManHaigRecord( Aig_Man_t * p, int nIters, int nSte
 extern void              Saig_ManDumpBlif( Aig_Man_t * p, char * pFileName );
 extern Aig_Man_t *       Saig_ManReadBlif( char * pFileName );
 /*=== saigInter.c ==========================================================*/
-extern int               Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth );
+extern int               Saig_Interpolate( Aig_Man_t * pAig, Inter_ManParams_t * pPars, int * pDepth );
 /*=== saigMiter.c ==========================================================*/
 extern Aig_Man_t *       Saig_ManCreateMiter( Aig_Man_t * p1, Aig_Man_t * p2, int Oper );
 /*=== saigPhase.c ==========================================================*/
diff --git a/src/aig/saig/saigInter.c b/src/aig/saig/saigInter.c
deleted file mode 100644
index 65fe6d87..00000000
--- a/src/aig/saig/saigInter.c
+++ /dev/null
@@ -1,1735 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [saigInter.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Sequential AIG package.]
-
-  Synopsis    [Interplation for unbounded model checking.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: saigInter.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "saig.h"
-#include "fra.h"
-#include "cnf.h"
-#include "satStore.h"
-
-/* 
-    The interpolation algorithm implemented here was introduced in the paper:
-    K. L. McMillan. Interpolation and SAT-based model checking. CAV’03, pp. 1-13.
-*/
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-// simulation manager
-typedef struct Saig_IntMan_t_ Saig_IntMan_t;
-struct Saig_IntMan_t_
-{
-    // AIG manager
-    Aig_Man_t *      pAig;         // the original AIG manager
-    Aig_Man_t *      pAigTrans;    // the transformed original AIG manager
-    Cnf_Dat_t *      pCnfAig;      // CNF for the original manager
-    // interpolant
-    Aig_Man_t *      pInter;       // the current interpolant
-    Cnf_Dat_t *      pCnfInter;    // CNF for the current interplant
-    // timeframes
-    Aig_Man_t *      pFrames;      // the timeframes      
-    Cnf_Dat_t *      pCnfFrames;   // CNF for the timeframes 
-    // other data
-    Vec_Int_t *      vVarsAB;      // the variables participating in 
-    // temporary place for the new interpolant
-    Aig_Man_t *      pInterNew;
-    Vec_Ptr_t *      vInters;
-    // parameters
-    int              nFrames;      // the number of timeframes
-    int              nConfCur;     // the current number of conflicts
-    int              nConfLimit;   // the limit on the number of conflicts
-    int              fVerbose;     // the verbosiness flag
-    // runtime
-    int              timeRwr;
-    int              timeCnf;
-    int              timeSat;
-    int              timeInt;
-    int              timeEqu;
-    int              timeOther;
-    int              timeTotal;
-};
-
-#ifdef ABC_USE_LIBRARIES
-static int Saig_M144pPerformOneStep( Saig_IntMan_t * p, int fUsePudlak, int fUseOther );
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Create trivial AIG manager for the init state.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_ManInit( int nRegs )
-{
-    Aig_Man_t * p;
-    Aig_Obj_t * pRes;
-    Aig_Obj_t ** ppInputs;
-    int i;
-    assert( nRegs > 0 );
-    ppInputs = ALLOC( Aig_Obj_t *, nRegs );
-    p = Aig_ManStart( nRegs );
-    for ( i = 0; i < nRegs; i++ )
-        ppInputs[i] = Aig_Not( Aig_ObjCreatePi(p) );
-    pRes = Aig_Multi( p, ppInputs, nRegs, AIG_OBJ_AND );
-    Aig_ObjCreatePo( p, pRes );
-    free( ppInputs );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicate the AIG w/o POs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_ManDuplicated( Aig_Man_t * p )
-{
-    Aig_Man_t * pNew;
-    Aig_Obj_t * pObj;
-    int i;
-    assert( Aig_ManRegNum(p) > 0 );
-    // create the new manager
-    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    // create the PIs
-    Aig_ManCleanData( p );
-    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManForEachPi( p, pObj, i )
-        pObj->pData = Aig_ObjCreatePi( pNew );
-    // set registers
-    pNew->nRegs    = p->nRegs;
-    pNew->nTruePis = p->nTruePis;
-    pNew->nTruePos = 0;
-    // duplicate internal nodes
-    Aig_ManForEachNode( p, pObj, i )
-        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    // create register inputs with MUXes
-    Saig_ManForEachLi( p, pObj, i )
-        Aig_ObjCreatePo( pNew, Aig_ObjChild0Copy(pObj) );
-    Aig_ManCleanup( pNew );
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicate the AIG w/o POs and transforms to transit into init state.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_ManTransformed( Aig_Man_t * p )
-{
-    Aig_Man_t * pNew;
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    Aig_Obj_t * pCtrl = NULL; // Suppress "might be used uninitialized"
-    int i;
-    assert( Aig_ManRegNum(p) > 0 );
-    // create the new manager
-    pNew = Aig_ManStart( Aig_ManObjNumMax(p) );
-    pNew->pName = Aig_UtilStrsav( p->pName );
-    pNew->pSpec = Aig_UtilStrsav( p->pSpec );
-    // create the PIs
-    Aig_ManCleanData( p );
-    Aig_ManConst1(p)->pData = Aig_ManConst1(pNew);
-    Aig_ManForEachPi( p, pObj, i )
-    {
-        if ( i == Saig_ManPiNum(p) )
-            pCtrl = Aig_ObjCreatePi( pNew );
-        pObj->pData = Aig_ObjCreatePi( pNew );
-    }
-    // set registers
-    pNew->nRegs    = p->nRegs;
-    pNew->nTruePis = p->nTruePis + 1;
-    pNew->nTruePos = 0;
-    // duplicate internal nodes
-    Aig_ManForEachNode( p, pObj, i )
-        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    // create register inputs with MUXes
-    Saig_ManForEachLiLo( p, pObjLi, pObjLo, i )
-    {
-        pObj = Aig_Mux( pNew, pCtrl, pObjLo->pData, Aig_ObjChild0Copy(pObjLi) );
-//        pObj = Aig_Mux( pNew, pCtrl, Aig_ManConst0(pNew), Aig_ObjChild0Copy(pObjLi) );
-        Aig_ObjCreatePo( pNew, pObj );
-    }
-    Aig_ManCleanup( pNew );
-    return pNew;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Create timeframes of the manager for interpolation.]
-
-  Description [The resulting manager is combinational. The primary inputs
-  corresponding to register outputs are ordered first. The only POs of the 
-  manager is the property output of the last timeframe.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_ManFramesInter( Aig_Man_t * pAig, int nFrames )
-{
-    Aig_Man_t * pFrames;
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    int i, f;
-    assert( Saig_ManRegNum(pAig) > 0 );
-    assert( Saig_ManPoNum(pAig) == 1 );
-    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
-    // map the constant node
-    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
-    // create variables for register outputs
-    Saig_ManForEachLo( pAig, pObj, i )
-        pObj->pData = Aig_ObjCreatePi( pFrames );
-    // add timeframes
-    for ( f = 0; f < nFrames; f++ )
-    {
-        // create PI nodes for this frame
-        Saig_ManForEachPi( pAig, pObj, i )
-            pObj->pData = Aig_ObjCreatePi( pFrames );
-        // add internal nodes of this frame
-        Aig_ManForEachNode( pAig, pObj, i )
-            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-        if ( f == nFrames - 1 )
-            break;
-        // save register inputs
-        Saig_ManForEachLi( pAig, pObj, i )
-            pObj->pData = Aig_ObjChild0Copy(pObj);
-        // transfer to register outputs
-        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
-            pObjLo->pData = pObjLi->pData;
-    }
-    // create the only PO of the manager
-    pObj = Aig_ManPo( pAig, 0 );
-    Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
-    Aig_ManCleanup( pFrames );
-    return pFrames;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the SAT solver for one interpolation run.]
-
-  Description [pInter is the previous interpolant. pAig is one time frame.
-  pFrames is the unrolled time frames.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-sat_solver * Saig_DeriveSatSolver( 
-    Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter, 
-    Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig, 
-    Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames, 
-    Vec_Int_t * vVarsAB )
-{
-    sat_solver * pSat;
-    Aig_Obj_t * pObj, * pObj2;
-    int i, Lits[2];
-
-    // sanity checks
-    assert( Aig_ManRegNum(pInter) == 0 );
-    assert( Aig_ManRegNum(pAig) > 0 );
-    assert( Aig_ManRegNum(pFrames) == 0 );
-    assert( Aig_ManPoNum(pInter) == 1 );
-    assert( Aig_ManPoNum(pFrames) == 1 );
-    assert( Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) );
-//    assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
-
-    // prepare CNFs
-    Cnf_DataLift( pCnfAig,   pCnfFrames->nVars );
-    Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars );
-
-    // start the solver
-    pSat = sat_solver_new();
-    sat_solver_store_alloc( pSat );
-    sat_solver_setnvars( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars );
-
-    // add clauses of A
-    // interpolant
-    for ( i = 0; i < pCnfInter->nClauses; i++ )
-    {
-        if ( !sat_solver_addclause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) )
-            assert( 0 );
-    }
-    // connector clauses
-    Aig_ManForEachPi( pInter, pObj, i )
-    {
-        pObj2 = Saig_ManLo( pAig, i );
-        Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
-        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
-        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
-            assert( 0 );
-        Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
-        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
-        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
-            assert( 0 );
-    }
-    // one timeframe
-    for ( i = 0; i < pCnfAig->nClauses; i++ )
-    {
-        if ( !sat_solver_addclause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) )
-            assert( 0 );
-    }
-    // connector clauses
-    Vec_IntClear( vVarsAB );
-    Aig_ManForEachPi( pFrames, pObj, i )
-    {
-        if ( i == Aig_ManRegNum(pAig) )
-            break;
-        Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
-
-        pObj2 = Saig_ManLi( pAig, i );
-        Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
-        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
-        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
-            assert( 0 );
-        Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
-        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
-        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
-            assert( 0 );
-    }
-    // add clauses of B
-    sat_solver_store_mark_clauses_a( pSat );
-    for ( i = 0; i < pCnfFrames->nClauses; i++ )
-    {
-        if ( !sat_solver_addclause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) )
-        {
-            pSat->fSolved = 1;
-            break;
-        }
-    }
-    sat_solver_store_mark_roots( pSat );
-    // return clauses to the original state
-    Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
-    Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
-    return pSat;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks constainment of two interpolants.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_ManCheckContainment( Aig_Man_t * pNew, Aig_Man_t * pOld )
-{
-    Aig_Man_t * pMiter, * pAigTemp;
-    int RetValue;
-    pMiter = Aig_ManCreateMiter( pNew, pOld, 1 );
-//    pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 );
-//    Aig_ManStop( pAigTemp );
-    RetValue = Fra_FraigMiterStatus( pMiter );
-    if ( RetValue == -1 )
-    {
-        pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
-        RetValue = Fra_FraigMiterStatus( pAigTemp );
-        Aig_ManStop( pAigTemp );
-//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 );
-    }
-    assert( RetValue != -1 );
-    Aig_ManStop( pMiter );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Checks constainment of two interpolants.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_ManCheckEquivalence( Aig_Man_t * pNew, Aig_Man_t * pOld )
-{
-    Aig_Man_t * pMiter, * pAigTemp;
-    int RetValue;
-    pMiter = Aig_ManCreateMiter( pNew, pOld, 0 );
-//    pMiter = Dar_ManRwsat( pAigTemp = pMiter, 1, 0 );
-//    Aig_ManStop( pAigTemp );
-    RetValue = Fra_FraigMiterStatus( pMiter );
-    if ( RetValue == -1 )
-    {
-        pAigTemp = Fra_FraigEquivence( pMiter, 1000000, 1 );
-        RetValue = Fra_FraigMiterStatus( pAigTemp );
-        Aig_ManStop( pAigTemp );
-//        RetValue = Fra_FraigSat( pMiter, 1000000, 0, 0, 0 );
-    }
-    assert( RetValue != -1 );
-    Aig_ManStop( pMiter );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs one SAT run with interpolation.]
-
-  Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_PerformOneStep_old( Saig_IntMan_t * p, int fUseIp )
-{
-    sat_solver * pSat;
-    void * pSatCnf = NULL;
-    Inta_Man_t * pManInterA; 
-    Intb_Man_t * pManInterB; 
-    int clk, status, RetValue;
-    assert( p->pInterNew == NULL );
-
-    // derive the SAT solver
-    pSat = Saig_DeriveSatSolver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB );
-//Sat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 1 );
-    // solve the problem
-clk = clock();
-    status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
-    p->nConfCur = pSat->stats.conflicts;
-p->timeSat += clock() - clk;
-    if ( status == l_False )
-    {
-        pSatCnf = sat_solver_store_release( pSat );
-        RetValue = 1;
-    }
-    else if ( status == l_True )
-    {
-        RetValue = 0;
-    }
-    else
-    {
-        RetValue = -1;
-    }
-    sat_solver_delete( pSat );
-    if ( pSatCnf == NULL )
-        return RetValue;
-
-    // create the resulting manager
-clk = clock();
-    if ( !fUseIp )
-    {
-        pManInterA = Inta_ManAlloc();
-        p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
-        Inta_ManFree( pManInterA );
-    }
-    else
-    {
-        pManInterB = Intb_ManAlloc();
-        p->pInterNew = Intb_ManInterpolate( pManInterB, pSatCnf, p->vVarsAB, 0 );
-        Intb_ManFree( pManInterB );
-    }
-p->timeInt += clock() - clk;
-    Sto_ManFree( pSatCnf );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Aig_ManDupExpand( Aig_Man_t * pInter, Aig_Man_t * pOther )
-{
-    Aig_Man_t * pInterC;
-    assert( Aig_ManPiNum(pInter) <= Aig_ManPiNum(pOther) );
-    pInterC = Aig_ManDupSimple( pInter );
-    Aig_IthVar( pInterC, Aig_ManPiNum(pOther)-1 );
-    assert( Aig_ManPiNum(pInterC) == Aig_ManPiNum(pOther) );
-    return pInterC;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_VerifyInterpolant1( Inta_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter )
-{
-    extern Aig_Man_t * Inta_ManDeriveClauses( Inta_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA );
-    Aig_Man_t * pLower, * pUpper, * pInterC;
-    int RetValue1, RetValue2;
-
-    pLower = Inta_ManDeriveClauses( pMan, pCnf, 1 );
-    pUpper = Inta_ManDeriveClauses( pMan, pCnf, 0 );
-    Aig_ManFlipFirstPo( pUpper );
-
-    pInterC = Aig_ManDupExpand( pInter, pLower );
-    RetValue1 = Saig_ManCheckContainment( pLower, pInterC );
-    Aig_ManStop( pInterC );
-
-    pInterC = Aig_ManDupExpand( pInter, pUpper );
-    RetValue2 = Saig_ManCheckContainment( pInterC, pUpper );
-    Aig_ManStop( pInterC );
-    
-    if ( RetValue1 && RetValue2 )
-        printf( "Im is correct.\n" );
-    if ( !RetValue1 )
-        printf( "Property A => Im fails.\n" );
-    if ( !RetValue2 )
-        printf( "Property Im => !B fails.\n" );
-
-    Aig_ManStop( pLower );
-    Aig_ManStop( pUpper );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_VerifyInterpolant2( Intb_Man_t * pMan, Sto_Man_t * pCnf, Aig_Man_t * pInter )
-{
-    extern Aig_Man_t * Intb_ManDeriveClauses( Intb_Man_t * pMan, Sto_Man_t * pCnf, int fClausesA );
-    Aig_Man_t * pLower, * pUpper, * pInterC;
-    int RetValue1, RetValue2;
-
-    pLower = Intb_ManDeriveClauses( pMan, pCnf, 1 );
-    pUpper = Intb_ManDeriveClauses( pMan, pCnf, 0 );
-    Aig_ManFlipFirstPo( pUpper );
-
-    pInterC = Aig_ManDupExpand( pInter, pLower );
-//Aig_ManPrintStats( pLower );
-//Aig_ManPrintStats( pUpper );
-//Aig_ManPrintStats( pInterC );
-//Aig_ManDumpBlif( pInterC, "inter_c.blif", NULL, NULL );
-    RetValue1 = Saig_ManCheckContainment( pLower, pInterC );
-    Aig_ManStop( pInterC );
-
-    pInterC = Aig_ManDupExpand( pInter, pUpper );
-    RetValue2 = Saig_ManCheckContainment( pInterC, pUpper );
-    Aig_ManStop( pInterC );
-    
-    if ( RetValue1 && RetValue2 )
-        printf( "Ip is correct.\n" );
-    if ( !RetValue1 )
-        printf( "Property A => Ip fails.\n" );
-    if ( !RetValue2 )
-        printf( "Property Ip => !B fails.\n" );
-
-    Aig_ManStop( pLower );
-    Aig_ManStop( pUpper );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs one SAT run with interpolation.]
-
-  Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_PerformOneStep( Saig_IntMan_t * p, int fUseIp )
-{
-    sat_solver * pSat;
-    void * pSatCnf = NULL;
-    Inta_Man_t * pManInterA; 
-    Intb_Man_t * pManInterB; 
-    int clk, status, RetValue;
-    assert( p->pInterNew == NULL );
-
-    // derive the SAT solver
-    pSat = Saig_DeriveSatSolver( p->pInter, p->pCnfInter, p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, p->vVarsAB );
-//Sat_SolverWriteDimacs( pSat, "test.cnf", NULL, NULL, 1 );
-    // solve the problem
-clk = clock();
-    status = sat_solver_solve( pSat, NULL, NULL, (sint64)p->nConfLimit, (sint64)0, (sint64)0, (sint64)0 );
-    p->nConfCur = pSat->stats.conflicts;
-p->timeSat += clock() - clk;
-    if ( status == l_False )
-    {
-        pSatCnf = sat_solver_store_release( pSat );
-        RetValue = 1;
-    }
-    else if ( status == l_True )
-    {
-        RetValue = 0;
-    } 
-    else
-    {
-        RetValue = -1;
-    }
-    sat_solver_delete( pSat );
-    if ( pSatCnf == NULL )
-        return RetValue;
-
-    // create the resulting manager
-clk = clock();
-    if ( !fUseIp )
-    {
-        pManInterA = Inta_ManAlloc();
-        p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
-        Inta_ManFree( pManInterA );
-    }
-    else
-    {
-        Aig_Man_t * pInterNew2;
-        int RetValue;
-
-        pManInterA = Inta_ManAlloc();
-        p->pInterNew = Inta_ManInterpolate( pManInterA, pSatCnf, p->vVarsAB, 0 );
-//        Saig_VerifyInterpolant1( pManInterA, pSatCnf, p->pInterNew );
-        Inta_ManFree( pManInterA );
-
-        pManInterB = Intb_ManAlloc();
-        pInterNew2 = Intb_ManInterpolate( pManInterB, pSatCnf, p->vVarsAB, 0 );
-        Saig_VerifyInterpolant2( pManInterB, pSatCnf, pInterNew2 );
-        Intb_ManFree( pManInterB );
-
-        // check relationship
-        RetValue = Saig_ManCheckEquivalence( pInterNew2, p->pInterNew );
-        if ( RetValue )
-            printf( "Equivalence \"Ip == Im\" holds\n" );
-        else
-        {
-//            printf( "Equivalence \"Ip == Im\" does not hold\n" );
-            RetValue = Saig_ManCheckContainment( pInterNew2, p->pInterNew );
-            if ( RetValue )
-                printf( "Containment \"Ip -> Im\" holds\n" );
-            else
-                printf( "Containment \"Ip -> Im\" does not hold\n" );
-
-            RetValue = Saig_ManCheckContainment( p->pInterNew, pInterNew2 );
-            if ( RetValue )
-                printf( "Containment \"Im -> Ip\" holds\n" );
-            else
-                printf( "Containment \"Im -> Ip\" does not hold\n" );
-        }
-
-        Aig_ManStop( pInterNew2 );
-    }
-p->timeInt += clock() - clk;
-    Sto_ManFree( pSatCnf );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Frees the interpolation manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManagerClean( Saig_IntMan_t * p )
-{
-    if ( p->pCnfInter )
-        Cnf_DataFree( p->pCnfInter );
-    if ( p->pCnfFrames )
-        Cnf_DataFree( p->pCnfFrames );
-    if ( p->pInter )
-        Aig_ManStop( p->pInter );
-    if ( p->pFrames )
-        Aig_ManStop( p->pFrames );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Frees the interpolation manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManagerFreeInters( Saig_IntMan_t * p )
-{
-    Aig_Man_t * pTemp;
-    int i;
-    Vec_PtrForEachEntry( p->vInters, pTemp, i )
-        Aig_ManStop( pTemp );
-    Vec_PtrClear( p->vInters );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Frees the interpolation manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManagerFree( Saig_IntMan_t * p )
-{
-    if ( p->fVerbose )
-    {
-        p->timeOther = p->timeTotal-p->timeRwr-p->timeCnf-p->timeSat-p->timeInt-p->timeEqu;
-        printf( "Runtime statistics:\n" );
-        PRTP( "Rewriting  ", p->timeRwr,   p->timeTotal );
-        PRTP( "CNF mapping", p->timeCnf,   p->timeTotal );
-        PRTP( "SAT solving", p->timeSat,   p->timeTotal );
-        PRTP( "Interpol   ", p->timeInt,   p->timeTotal );
-        PRTP( "Containment", p->timeEqu,   p->timeTotal );
-        PRTP( "Other      ", p->timeOther, p->timeTotal );
-        PRTP( "TOTAL      ", p->timeTotal, p->timeTotal );
-    }
-
-    if ( p->pCnfAig )
-        Cnf_DataFree( p->pCnfAig );
-    if ( p->pCnfFrames )
-        Cnf_DataFree( p->pCnfFrames );
-    if ( p->pCnfInter )
-        Cnf_DataFree( p->pCnfInter );
-    Vec_IntFree( p->vVarsAB );
-    if ( p->pAigTrans )
-        Aig_ManStop( p->pAigTrans );
-    if ( p->pFrames )
-        Aig_ManStop( p->pFrames );
-    if ( p->pInter )
-        Aig_ManStop( p->pInter );
-    if ( p->pInterNew )
-        Aig_ManStop( p->pInterNew );
-    Saig_ManagerFreeInters( p );
-    Vec_PtrFree( p->vInters );
-    free( p );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Check inductive containment.]
-
-  Description [Given interpolant I and transition relation T, here we
-  check that I(x) * T(x,y) => T(y). ]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_ManCheckInductiveContainment( Saig_IntMan_t * p, int fSubtractOld )
-{
-    sat_solver * pSat;
-    Aig_Man_t * pInterOld = p->pInter;
-    Aig_Man_t * pInterNew = p->pInterNew;
-    Aig_Man_t * pTrans    = p->pAigTrans;
-    Cnf_Dat_t * pCnfOld   = p->pCnfInter;
-    Cnf_Dat_t * pCnfNew   = Cnf_Derive( p->pInterNew, 0 ); 
-    Cnf_Dat_t * pCnfTrans = p->pCnfAig;
-    Aig_Obj_t * pObj, * pObj2;
-    int status, i, Lits[2];
-
-    // start the solver
-    pSat = sat_solver_new();
-    if ( fSubtractOld )
-        sat_solver_setnvars( pSat, 2 * pCnfNew->nVars + pCnfTrans->nVars + pCnfOld->nVars );
-    else
-        sat_solver_setnvars( pSat, 2 * pCnfNew->nVars + pCnfTrans->nVars );
-
-    // interpolant
-    for ( i = 0; i < pCnfNew->nClauses; i++ )
-    {
-        if ( !sat_solver_addclause( pSat, pCnfNew->pClauses[i], pCnfNew->pClauses[i+1] ) )
-            assert( 0 );
-    }
-
-    // connector clauses
-    Cnf_DataLift( pCnfTrans, pCnfNew->nVars );
-    Aig_ManForEachPi( pInterNew, pObj, i )
-    {
-        pObj2 = Saig_ManLo( pTrans, i );
-        Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 0 );
-        Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 1 );
-        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
-            assert( 0 );
-        Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 1 );
-        Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 0 );
-        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
-            assert( 0 );
-    }
-    // one timeframe
-    for ( i = 0; i < pCnfTrans->nClauses; i++ )
-    {
-        if ( !sat_solver_addclause( pSat, pCnfTrans->pClauses[i], pCnfTrans->pClauses[i+1] ) )
-            assert( 0 );
-    }
-
-    // connector clauses
-    Cnf_DataLift( pCnfNew, pCnfNew->nVars + pCnfTrans->nVars );
-    Aig_ManForEachPi( pInterNew, pObj, i )
-    {
-        pObj2 = Saig_ManLi( pTrans, i );
-        Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 0 );
-        Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 1 );
-        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
-            assert( 0 );
-        Lits[0] = toLitCond( pCnfNew->pVarNums[pObj->Id], 1 );
-        Lits[1] = toLitCond( pCnfTrans->pVarNums[pObj2->Id], 0 );
-        if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
-            assert( 0 );
-    }
-
-    // complement the last literal
-    // add clauses of B
-    Cnf_DataFlipLastLiteral( pCnfNew );
-    for ( i = 0; i < pCnfNew->nClauses; i++ )
-    {
-        if ( !sat_solver_addclause( pSat, pCnfNew->pClauses[i], pCnfNew->pClauses[i+1] ) )
-        {
-//            assert( 0 );
-            Cnf_DataFree( pCnfNew );
-            return 1;
-        }
-    }
-    Cnf_DataFlipLastLiteral( pCnfNew );
-
-    // return clauses to the original state
-    Cnf_DataLift( pCnfTrans, -pCnfNew->nVars );
-    Cnf_DataLift( pCnfNew, -pCnfNew->nVars -pCnfTrans->nVars );
-    if ( fSubtractOld )
-    {
-        Cnf_DataLift( pCnfOld, 2 * pCnfNew->nVars + pCnfTrans->nVars );
-        // old interpolant clauses
-        Cnf_DataFlipLastLiteral( pCnfOld );
-        for ( i = 0; i < pCnfOld->nClauses; i++ )
-        {
-            if ( !sat_solver_addclause( pSat, pCnfOld->pClauses[i], pCnfOld->pClauses[i+1] ) )
-                assert( 0 );
-        }
-        Cnf_DataFlipLastLiteral( pCnfOld );
-        // connector clauses
-        Aig_ManForEachPi( pInterOld, pObj, i )
-        {
-            pObj2 = Aig_ManPi( pInterNew, i );
-            Lits[0] = toLitCond( pCnfOld->pVarNums[pObj->Id], 0 );
-            Lits[1] = toLitCond( pCnfNew->pVarNums[pObj2->Id], 1 );
-            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
-                assert( 0 );
-            Lits[0] = toLitCond( pCnfOld->pVarNums[pObj->Id], 1 );
-            Lits[1] = toLitCond( pCnfNew->pVarNums[pObj2->Id], 0 );
-            if ( !sat_solver_addclause( pSat, Lits, Lits+2 ) )
-                assert( 0 );
-        }
-        Cnf_DataLift( pCnfOld, - 2 * pCnfNew->nVars - pCnfTrans->nVars );
-    }
-    Cnf_DataFree( pCnfNew );
-
-    // solve the problem
-    status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
-    sat_solver_delete( pSat );
-    return status == l_False;
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Interplates while the number of conflicts is not exceeded.]
-
-  Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
-               
-  SideEffects [Does not check the property in 0-th frame.]
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth )
-{
-    extern int Saig_ManUniqueState( Aig_Man_t * pTrans, Vec_Ptr_t * vInters );
-    Saig_IntMan_t * p;
-    Aig_Man_t * pAigTemp;
-    int s, i, RetValue, Status, clk, clk2, clkTotal = clock();
-
-    // sanity checks
-    assert( Saig_ManRegNum(pAig) > 0 );
-    assert( Saig_ManPiNum(pAig) > 0 );
-    assert( Saig_ManPoNum(pAig) == 1 );
-
-    // create interpolation manager
-    p = ALLOC( Saig_IntMan_t, 1 );
-    memset( p, 0, sizeof(Saig_IntMan_t) );
-    p->vVarsAB = Vec_IntAlloc( Aig_ManRegNum(pAig) );
-    p->nFrames = 1;
-    p->nConfLimit = nConfLimit;
-    p->fVerbose = fVerbose;
-    p->vInters = Vec_PtrAlloc( 10 );
-    // can perform SAT sweeping and/or rewriting of this AIG...
-    p->pAig = pAig;      
-    if ( fTransLoop )
-        p->pAigTrans = Saig_ManTransformed( pAig );
-    else
-        p->pAigTrans = Saig_ManDuplicated( pAig );
-    // derive CNF for the transformed AIG
-clk = clock();
-    p->pCnfAig = Cnf_Derive( p->pAigTrans, Aig_ManRegNum(p->pAigTrans) ); 
-p->timeCnf += clock() - clk;    
-    if ( fVerbose )
-    { 
-        printf( "AIG: PI/PO/Reg = %d/%d/%d. And = %d. Lev = %d.  CNF: Var/Cla = %d/%d.\n",
-            Saig_ManPiNum(pAig), Saig_ManPoNum(pAig), Saig_ManRegNum(pAig), 
-            Aig_ManAndNum(pAig), Aig_ManLevelNum(pAig),
-            p->pCnfAig->nVars, p->pCnfAig->nClauses );
-    }
-
-    // derive interpolant
-    *pDepth = -1;
-    for ( s = 0; ; s++ )
-    {
-        Saig_ManagerFreeInters( p );
-clk2 = clock();
-        // initial state
-        p->pInter = Saig_ManInit( Aig_ManRegNum(pAig) );
-        Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInter) );
-clk = clock();
-        p->pCnfInter = Cnf_Derive( p->pInter, 0 );  
-p->timeCnf += clock() - clk;    
-        // timeframes
-        p->pFrames = Saig_ManFramesInter( pAig, p->nFrames );
-clk = clock();
-        if ( fRewrite )
-        {
-            p->pFrames = Dar_ManRwsat( pAigTemp = p->pFrames, 1, 0 );
-            Aig_ManStop( pAigTemp );
-//        p->pFrames = Fra_FraigEquivence( pAigTemp = p->pFrames, 100, 0 );
-//        Aig_ManStop( pAigTemp );
-        }
-p->timeRwr += clock() - clk;
-        // can also do SAT sweeping on the timeframes...
-clk = clock();
-        p->pCnfFrames = Cnf_Derive( p->pFrames, 0 );  
-p->timeCnf += clock() - clk;    
-        // report statistics
-        if ( fVerbose )
-        {
-            printf( "Step = %2d. Frames = 1 + %d. And = %5d. Lev = %5d.  ", 
-                s+1, p->nFrames, Aig_ManNodeNum(p->pFrames), Aig_ManLevelNum(p->pFrames) );
-            PRT( "Time", clock() - clk2 );
-        }
-        // iterate the interpolation procedure
-        for ( i = 0; ; i++ )
-        {
-            if ( p->nFrames + i >= nFramesMax )
-            {
-                if ( fVerbose )
-                    printf( "Reached limit (%d) on the number of timeframes.\n", nFramesMax );
-                p->timeTotal = clock() - clkTotal;
-                Saig_ManagerFree( p );
-                return -1;
-            }
-            // perform interplation
-            clk = clock();
-#ifdef ABC_USE_LIBRARIES
-            if ( fUseMiniSat )
-                RetValue = Saig_M144pPerformOneStep( p, fUsePudlak, fUseOther );
-            else
-#endif
-                RetValue = Saig_PerformOneStep( p, 0 );
-
-            if ( fVerbose )
-            {
-                printf( "   I = %2d. Bmc =%3d. IntAnd =%6d. IntLev =%5d. Conf =%6d.  ", 
-                    i+1, i + 1 + p->nFrames, Aig_ManNodeNum(p->pInter), Aig_ManLevelNum(p->pInter), p->nConfCur );
-                PRT( "Time", clock() - clk );
-            }
-            if ( RetValue == 0 ) // found a (spurious?) counter-example
-            {
-                if ( i == 0 ) // real counterexample
-                {
-                    if ( fVerbose )
-                        printf( "Found a real counterexample in the first frame.\n" );
-                    p->timeTotal = clock() - clkTotal;
-                    *pDepth = p->nFrames + 1;
-                    Saig_ManagerFree( p );
-                    return 0;
-                }
-                // likely spurious counter-example
-                p->nFrames += i;
-                Saig_ManagerClean( p );
-                break;
-            }
-            else if ( RetValue == -1 ) // timed out
-            {
-                if ( fVerbose )
-                    printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit );
-                assert( p->nConfCur >= p->nConfLimit );
-                p->timeTotal = clock() - clkTotal;
-                Saig_ManagerFree( p );
-                return -1;
-            }
-            assert( RetValue == 1 ); // found new interpolant
-            // compress the interpolant
-clk = clock();
-            p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 1, 0 );
-            Aig_ManStop( pAigTemp );
-p->timeRwr += clock() - clk;
-            // save the new interpolant
-            Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInterNew) );
-            // check containment of interpolants
-clk = clock();
-            if ( fCheckKstep ) // k-step unique-state induction
-                Status = Saig_ManUniqueState( p->pAigTrans, p->vInters );
-            else if ( fCheckInd ) // simple induction
-                Status = Saig_ManCheckInductiveContainment( p, 1 );
-            else // combinational containment
-                Status = Saig_ManCheckContainment( p->pInterNew, p->pInter );
-p->timeEqu += clock() - clk;
-            if ( Status ) // contained
-            {
-                if ( fVerbose )
-                    printf( "Proved containment of interpolants.\n" );
-                p->timeTotal = clock() - clkTotal;
-                Saig_ManagerFree( p );
-                return 1;
-            }
-            // save interpolant and convert it into CNF
-            if ( fTransLoop )
-            {
-                Aig_ManStop( p->pInter );
-                p->pInter = p->pInterNew; 
-            }
-            else
-            {
-                p->pInter = Aig_ManCreateMiter( pAigTemp = p->pInter, p->pInterNew, 2 );
-                Aig_ManStop( pAigTemp );
-                Aig_ManStop( p->pInterNew );
-                // compress the interpolant
-clk = clock();
-                p->pInter = Dar_ManRwsat( pAigTemp = p->pInter, 1, 0 );
-                Aig_ManStop( pAigTemp );
-p->timeRwr += clock() - clk;
-            }
-            p->pInterNew = NULL;
-            Cnf_DataFree( p->pCnfInter );
-clk = clock();
-            p->pCnfInter = Cnf_Derive( p->pInter, 0 );  
-p->timeCnf += clock() - clk;
-        }
-    }
-    assert( 0 );
-    return RetValue;
-}
-
-
-#ifdef ABC_USE_LIBRARIES
-
-#include "m114p.h"
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the SAT solver for one interpolation run.]
-
-  Description [pInter is the previous interpolant. pAig is one time frame.
-  pFrames is the unrolled time frames.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-M114p_Solver_t Saig_M144pDeriveSatSolver( 
-    Aig_Man_t * pInter, Cnf_Dat_t * pCnfInter, 
-    Aig_Man_t * pAig, Cnf_Dat_t * pCnfAig, 
-    Aig_Man_t * pFrames, Cnf_Dat_t * pCnfFrames, 
-    Vec_Int_t ** pvMapRoots, Vec_Int_t ** pvMapVars )
-{
-    M114p_Solver_t pSat;
-    Aig_Obj_t * pObj, * pObj2;
-    int i, Lits[2];
-
-    // sanity checks
-    assert( Aig_ManRegNum(pInter) == 0 );
-    assert( Aig_ManRegNum(pAig) > 0 );
-    assert( Aig_ManRegNum(pFrames) == 0 );
-    assert( Aig_ManPoNum(pInter) == 1 );
-    assert( Aig_ManPoNum(pFrames) == 1 );
-    assert( Aig_ManPiNum(pInter) == Aig_ManRegNum(pAig) );
-//    assert( (Aig_ManPiNum(pFrames) - Aig_ManRegNum(pAig)) % Saig_ManPiNum(pAig) == 0 );
-
-    // prepare CNFs
-    Cnf_DataLift( pCnfAig,   pCnfFrames->nVars );
-    Cnf_DataLift( pCnfInter, pCnfFrames->nVars + pCnfAig->nVars );
-
-    *pvMapRoots = Vec_IntAlloc( 10000 );
-    *pvMapVars = Vec_IntAlloc( 0 );
-    Vec_IntFill( *pvMapVars, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars, -1 );
-    for ( i = 0; i < pCnfFrames->nVars; i++ )
-        Vec_IntWriteEntry( *pvMapVars, i, -2 );
-
-    // start the solver
-    pSat = M114p_SolverNew( 1 );
-    M114p_SolverSetVarNum( pSat, pCnfInter->nVars + pCnfAig->nVars + pCnfFrames->nVars );
-
-    // add clauses of A
-    // interpolant
-    for ( i = 0; i < pCnfInter->nClauses; i++ )
-    {
-        Vec_IntPush( *pvMapRoots, 0 );
-        if ( !M114p_SolverAddClause( pSat, pCnfInter->pClauses[i], pCnfInter->pClauses[i+1] ) )
-            assert( 0 );
-    }
-    // connector clauses
-    Aig_ManForEachPi( pInter, pObj, i )
-    {
-        pObj2 = Saig_ManLo( pAig, i );
-        Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 0 );
-        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
-        Vec_IntPush( *pvMapRoots, 0 );
-        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
-            assert( 0 );
-        Lits[0] = toLitCond( pCnfInter->pVarNums[pObj->Id], 1 );
-        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
-        Vec_IntPush( *pvMapRoots, 0 );
-        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
-            assert( 0 );
-    }
-    // one timeframe
-    for ( i = 0; i < pCnfAig->nClauses; i++ )
-    {
-        Vec_IntPush( *pvMapRoots, 0 );
-        if ( !M114p_SolverAddClause( pSat, pCnfAig->pClauses[i], pCnfAig->pClauses[i+1] ) )
-            assert( 0 );
-    }
-    // connector clauses
-    Aig_ManForEachPi( pFrames, pObj, i )
-    {
-        if ( i == Aig_ManRegNum(pAig) )
-            break;
-//        Vec_IntPush( vVarsAB, pCnfFrames->pVarNums[pObj->Id] );
-        Vec_IntWriteEntry( *pvMapVars, pCnfFrames->pVarNums[pObj->Id], i );
-
-        pObj2 = Saig_ManLi( pAig, i );
-        Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 0 );
-        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 1 );
-        Vec_IntPush( *pvMapRoots, 0 );
-        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
-            assert( 0 );
-        Lits[0] = toLitCond( pCnfFrames->pVarNums[pObj->Id], 1 );
-        Lits[1] = toLitCond( pCnfAig->pVarNums[pObj2->Id], 0 );
-        Vec_IntPush( *pvMapRoots, 0 );
-        if ( !M114p_SolverAddClause( pSat, Lits, Lits+2 ) )
-            assert( 0 );
-    }
-    // add clauses of B
-    for ( i = 0; i < pCnfFrames->nClauses; i++ )
-    {
-        Vec_IntPush( *pvMapRoots, 1 );
-        if ( !M114p_SolverAddClause( pSat, pCnfFrames->pClauses[i], pCnfFrames->pClauses[i+1] ) )
-        {
-//            assert( 0 );
-            break;
-        }
-    }
-    // return clauses to the original state
-    Cnf_DataLift( pCnfAig, -pCnfFrames->nVars );
-    Cnf_DataLift( pCnfInter, -pCnfFrames->nVars -pCnfAig->nVars );
-    return pSat;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes interpolant using MiniSat-1.14p.]
-
-  Description [Assumes that the solver returned UNSAT and proof
-  logging was enabled. Array vMapRoots maps number of each root clause 
-  into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
-  solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
-  where <num> is the var's 0-based number in the ordering of C variables.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_M144pInterpolateReport( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
-{
-    Vec_Int_t * vASteps;
-    int * pLits, * pClauses, * pVars;
-    int nLits, nVars, i, k, iVar, haveASteps;
-    int CountA, CountB, CountC, CountCsaved;
-
-    assert( M114p_SolverProofIsReady(s) );
-    vASteps = Vec_IntAlloc( 1000 );
-    // process root clauses
-    M114p_SolverForEachRoot( s, &pLits, nLits, i )
-    {
-        if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
-        {
-        }
-        else // clause of A
-        {
-        }
-        Vec_IntPush( vASteps, Vec_IntEntry(vMapRoots, i) );
-    }
-//    assert( Vec_IntSize(vASteps) == Vec_IntSize(vMapRoots) );
- 
-    // process learned clauses
-    CountA = CountB = CountC = CountCsaved = 0;
-    M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
-    {
-        haveASteps = Vec_IntEntry( vASteps, pClauses[0] );
-        for ( k = 0; k < nVars; k++ )
-        {
-            iVar = Vec_IntEntry( vMapVars, pVars[k] );
-            haveASteps |= Vec_IntEntry( vASteps, pClauses[k+1] );
-            if ( iVar == -1 ) // var of A
-            {
-                haveASteps = 1;
-            }
-            else // var of B or C
-            {
-            }
-
-            if ( iVar == -1 )
-                CountA++;
-            else if ( iVar == -2 )
-                CountB++;
-            else 
-            {
-                if ( haveASteps == 0 )
-                    CountCsaved++;
-                CountC++;
-            }
-        }
-        Vec_IntPush( vASteps, haveASteps );
-    }
-    assert( Vec_IntSize(vASteps) == M114p_SolverProofClauseNum(s) );
-
-    printf( "ResSteps: A = %6d. B = %6d. C = %6d. C_saved = %6d. (%6.2f %%)\n", 
-        CountA, CountB, CountC, CountCsaved, 100.0 * CountCsaved/CountC );
-    Vec_IntFree( vASteps );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes interpolant using MiniSat-1.14p.]
-
-  Description [Assumes that the solver returned UNSAT and proof
-  logging was enabled. Array vMapRoots maps number of each root clause 
-  into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
-  solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
-  where <num> is the var's 0-based number in the ordering of C variables.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_M144pInterpolateLastStep( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
-{
-    int * pLits, * pClauses, * pVars;
-    int nLits, nVars, i, k, iVar;
-    int nSteps, iStepA, iStepB;
-    assert( M114p_SolverProofIsReady(s) );
-    // process root clauses
-    M114p_SolverForEachRoot( s, &pLits, nLits, i )
-    {
-        if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
-        {
-        }
-        else // clause of A
-        {
-        }
-    }
-//    assert( Vec_IntSize(vASteps) == Vec_IntSize(vMapRoots) );
-    // process learned clauses
-    nSteps = 0;
-    M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
-    {
-        for ( k = 0; k < nVars; k++ )
-        {
-            iVar = Vec_IntEntry( vMapVars, pVars[k] );
-            if ( iVar == -1 ) // var of A
-            {
-                iStepA = nSteps;
-            }
-            else if ( iVar == -2 ) // var of B
-            {
-                iStepB = nSteps;
-            }
-            else // var of C
-            {
-            }
-            nSteps++;
-        }
-    }
-//    assert( Vec_IntSize(vASteps) == M114p_SolverProofClauseNum(s) );
-    if ( iStepA < iStepB )
-        return iStepB;
-    return iStepA;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes interpolant using MiniSat-1.14p.]
-
-  Description [Assumes that the solver returned UNSAT and proof
-  logging was enabled. Array vMapRoots maps number of each root clause 
-  into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
-  solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
-  where <num> is the var's 0-based number in the ordering of C variables.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_M144pInterpolate( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
-{
-    Aig_Man_t * p;
-    Aig_Obj_t * pInter, * pInter2, * pVar;
-    Vec_Ptr_t * vInters;
-    int * pLits, * pClauses, * pVars;
-    int nLits, nVars, i, k, iVar;
-    assert( M114p_SolverProofIsReady(s) );
-    vInters = Vec_PtrAlloc( 1000 );
-    // process root clauses
-    p = Aig_ManStart( 10000 );
-    M114p_SolverForEachRoot( s, &pLits, nLits, i )
-    {
-        if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
-            pInter = Aig_ManConst1(p);
-        else // clause of A
-        {
-            pInter = Aig_ManConst0(p);
-            for ( k = 0; k < nLits; k++ )
-            {
-                iVar = Vec_IntEntry( vMapVars, lit_var(pLits[k]) );
-                if ( iVar < 0 ) // var of A or B
-                    continue;
-                pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLits[k]) );
-                pInter = Aig_Or( p, pInter, pVar );
-            }
-        }
-        Vec_PtrPush( vInters, pInter );
-    }
-//    assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );
-
-    // process learned clauses
-    M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
-    {
-        pInter = Vec_PtrEntry( vInters, pClauses[0] );
-        for ( k = 0; k < nVars; k++ )
-        {
-            iVar = Vec_IntEntry( vMapVars, pVars[k] );
-            pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );
-            if ( iVar == -1 ) // var of A
-                pInter = Aig_Or( p, pInter, pInter2 );
-            else // var of B or C
-                pInter = Aig_And( p, pInter, pInter2 );
-        }
-        Vec_PtrPush( vInters, pInter );
-    }
-    assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
-    Vec_PtrFree( vInters );
-    Aig_ObjCreatePo( p, pInter );
-    Aig_ManCleanup( p );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs one resolution step.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_M144pResolve( Vec_Int_t * vResolvent, int * pLits, int nLits, int iVar )
-{
-    int i, k, iLit = -1, fFound = 0;
-    // find the variable in the clause
-    for ( i = 0; i < vResolvent->nSize; i++ )
-        if ( lit_var(vResolvent->pArray[i]) == iVar )
-        {
-            iLit = vResolvent->pArray[i];
-            vResolvent->pArray[i] = vResolvent->pArray[--vResolvent->nSize];
-            break;
-        }
-    assert( iLit != -1 );
-    // add other variables
-    for ( i = 0; i < nLits; i++ )
-    {
-        if ( lit_var(pLits[i]) == iVar )
-        {
-            assert( iLit == lit_neg(pLits[i]) );
-            fFound = 1;
-            continue;
-        }
-        // check if this literal appears
-        for ( k = 0; k < vResolvent->nSize; k++ )
-            if ( vResolvent->pArray[k] == pLits[i] )
-                break;
-        if ( k < vResolvent->nSize )
-            continue;
-        // add this literal
-        Vec_IntPush( vResolvent, pLits[i] );
-    }
-    assert( fFound );
-    return 1;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes interpolant using MiniSat-1.14p.]
-
-  Description [Assumes that the solver returned UNSAT and proof
-  logging was enabled. Array vMapRoots maps number of each root clause 
-  into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
-  solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
-  where <num> is the var's 0-based number in the ordering of C variables.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_M144pInterpolatePudlak( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
-{
-    Aig_Man_t * p;
-    Aig_Obj_t * pInter, * pInter2, * pVar;
-    Vec_Ptr_t * vInters;
-    Vec_Int_t * vLiterals, * vClauses, * vResolvent;
-    int * pLitsNext, nLitsNext, nOffset, iLit;
-    int * pLits, * pClauses, * pVars;
-    int nLits, nVars, i, k, v, iVar;
-    assert( M114p_SolverProofIsReady(s) );
-    vInters = Vec_PtrAlloc( 1000 );
-
-    vLiterals = Vec_IntAlloc( 10000 );
-    vClauses = Vec_IntAlloc( 1000 );
-    vResolvent = Vec_IntAlloc( 100 );
-
-    // create elementary variables
-    p = Aig_ManStart( 10000 );
-    Vec_IntForEachEntry( vMapVars, iVar, i )
-        if ( iVar >= 0 )
-            Aig_IthVar(p, iVar);
-    // process root clauses
-    M114p_SolverForEachRoot( s, &pLits, nLits, i )
-    {
-        if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
-            pInter = Aig_ManConst1(p);
-        else // clause of A
-            pInter = Aig_ManConst0(p);
-        Vec_PtrPush( vInters, pInter );
-
-        // save the root clause
-        Vec_IntPush( vClauses, Vec_IntSize(vLiterals) );
-        Vec_IntPush( vLiterals, nLits );
-        for ( v = 0; v < nLits; v++ )
-            Vec_IntPush( vLiterals, pLits[v] );
-    }
-    assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );
-
-    // process learned clauses
-    M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
-    {
-        pInter = Vec_PtrEntry( vInters, pClauses[0] );
-
-        // initialize the resolvent
-        nOffset = Vec_IntEntry( vClauses, pClauses[0] );
-        nLitsNext = Vec_IntEntry( vLiterals, nOffset );
-        pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1;
-        Vec_IntClear( vResolvent );
-        for ( v = 0; v < nLitsNext; v++ )
-            Vec_IntPush( vResolvent, pLitsNext[v] );
-
-        for ( k = 0; k < nVars; k++ )
-        {
-            iVar = Vec_IntEntry( vMapVars, pVars[k] );
-            pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );
-
-            // resolve it with the next clause
-            nOffset = Vec_IntEntry( vClauses, pClauses[k+1] );
-            nLitsNext = Vec_IntEntry( vLiterals, nOffset );
-            pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1;
-            Saig_M144pResolve( vResolvent, pLitsNext, nLitsNext, pVars[k] );
-
-            if ( iVar == -1 ) // var of A
-                pInter = Aig_Or( p, pInter, pInter2 );
-            else if ( iVar == -2 ) // var of B
-                pInter = Aig_And( p, pInter, pInter2 );
-            else // var of C
-            {
-                // check polarity of the pivot variable in the clause
-                for ( v = 0; v < nLitsNext; v++ )
-                    if ( lit_var(pLitsNext[v]) == pVars[k] )
-                        break;
-                assert( v < nLitsNext );
-                pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLitsNext[v]) );
-                pInter = Aig_Mux( p, pVar, pInter, pInter2 );
-            }
-        }
-        Vec_PtrPush( vInters, pInter );
-
-        // store the resulting clause
-        Vec_IntPush( vClauses, Vec_IntSize(vLiterals) );
-        Vec_IntPush( vLiterals, Vec_IntSize(vResolvent) );
-        Vec_IntForEachEntry( vResolvent, iLit, v )
-            Vec_IntPush( vLiterals, iLit );
-    }
-    assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
-    assert( Vec_IntSize(vResolvent) == 0 ); // the empty clause
-    Vec_PtrFree( vInters );
-    Vec_IntFree( vLiterals );
-    Vec_IntFree( vClauses );
-    Vec_IntFree( vResolvent );
-    Aig_ObjCreatePo( p, pInter );
-    Aig_ManCleanup( p );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes interpolant using MiniSat-1.14p.]
-
-  Description [Assumes that the solver returned UNSAT and proof
-  logging was enabled. Array vMapRoots maps number of each root clause 
-  into 0 (clause of A) or 1 (clause of B). Array vMapVars maps each SAT
-  solver variable into -1 (var of A), -2 (var of B), and <num> (var of C),
-  where <num> is the var's 0-based number in the ordering of C variables.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_M144pInterpolatePudlakASteps( M114p_Solver_t s, Vec_Int_t * vMapRoots, Vec_Int_t * vMapVars )
-{
-    Aig_Man_t * p;
-    Aig_Obj_t * pInter, * pInter2, * pVar;
-    Vec_Ptr_t * vInters;
-    Vec_Int_t * vASteps;
-    Vec_Int_t * vLiterals, * vClauses, * vResolvent;
-    int * pLitsNext, nLitsNext, nOffset, iLit;
-    int * pLits, * pClauses, * pVars;
-    int nLits, nVars, i, k, v, iVar, haveASteps;
-    assert( M114p_SolverProofIsReady(s) );
-    vInters = Vec_PtrAlloc( 1000 );
-    vASteps = Vec_IntAlloc( 1000 );
-
-    vLiterals = Vec_IntAlloc( 10000 );
-    vClauses = Vec_IntAlloc( 1000 );
-    vResolvent = Vec_IntAlloc( 100 );
-
-    // create elementary variables
-    p = Aig_ManStart( 10000 );
-    Vec_IntForEachEntry( vMapVars, iVar, i )
-        if ( iVar >= 0 )
-            Aig_IthVar(p, iVar);
-    // process root clauses
-    M114p_SolverForEachRoot( s, &pLits, nLits, i )
-    {
-        if ( Vec_IntEntry(vMapRoots, i) == 1 ) // clause of B
-            pInter = Aig_ManConst1(p);
-        else // clause of A
-            pInter = Aig_ManConst0(p);
-        Vec_PtrPush( vInters, pInter );
-        Vec_IntPush( vASteps, Vec_IntEntry(vMapRoots, i) );
-
-        // save the root clause
-        Vec_IntPush( vClauses, Vec_IntSize(vLiterals) );
-        Vec_IntPush( vLiterals, nLits );
-        for ( v = 0; v < nLits; v++ )
-            Vec_IntPush( vLiterals, pLits[v] );
-    }
-    assert( Vec_PtrSize(vInters) == Vec_IntSize(vMapRoots) );
-
-    // process learned clauses
-    M114p_SolverForEachChain( s, &pClauses, &pVars, nVars, i )
-    {
-        pInter = Vec_PtrEntry( vInters, pClauses[0] );
-        haveASteps = Vec_IntEntry( vASteps, pClauses[0] );
-
-        // initialize the resolvent
-        nOffset = Vec_IntEntry( vClauses, pClauses[0] );
-        nLitsNext = Vec_IntEntry( vLiterals, nOffset );
-        pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1;
-        Vec_IntClear( vResolvent );
-        for ( v = 0; v < nLitsNext; v++ )
-            Vec_IntPush( vResolvent, pLitsNext[v] );
-
-        for ( k = 0; k < nVars; k++ )
-        {
-            iVar = Vec_IntEntry( vMapVars, pVars[k] );
-            pInter2 = Vec_PtrEntry( vInters, pClauses[k+1] );
-            haveASteps |= Vec_IntEntry( vASteps, pClauses[k+1] );
-
-            // resolve it with the next clause
-            nOffset = Vec_IntEntry( vClauses, pClauses[k+1] );
-            nLitsNext = Vec_IntEntry( vLiterals, nOffset );
-            pLitsNext = Vec_IntArray(vLiterals) + nOffset + 1;
-            Saig_M144pResolve( vResolvent, pLitsNext, nLitsNext, pVars[k] );
-
-            if ( iVar == -1 ) // var of A
-                pInter = Aig_Or( p, pInter, pInter2 ), haveASteps = 1;
-            else if ( iVar == -2 ) // var of B
-                pInter = Aig_And( p, pInter, pInter2 );
-            else // var of C
-            {
-                if ( haveASteps == 0 )
-                    pInter = Aig_ManConst0(p);
-                else
-                {
-                    // check polarity of the pivot variable in the clause
-                    for ( v = 0; v < nLitsNext; v++ )
-                        if ( lit_var(pLitsNext[v]) == pVars[k] )
-                            break;
-                    assert( v < nLitsNext );
-                    pVar = Aig_NotCond( Aig_IthVar(p, iVar), lit_sign(pLitsNext[v]) );
-                    pInter = Aig_Mux( p, pVar, pInter, pInter2 );
-                }
-            }
-        }
-        Vec_PtrPush( vInters, pInter );
-        Vec_IntPush( vASteps, haveASteps );
-
-        // store the resulting clause
-        Vec_IntPush( vClauses, Vec_IntSize(vLiterals) );
-        Vec_IntPush( vLiterals, Vec_IntSize(vResolvent) );
-        Vec_IntForEachEntry( vResolvent, iLit, v )
-            Vec_IntPush( vLiterals, iLit );
-    }
-    assert( Vec_PtrSize(vInters) == M114p_SolverProofClauseNum(s) );
-    assert( Vec_IntSize(vResolvent) == 0 ); // the empty clause
-    Vec_PtrFree( vInters );
-    Vec_IntFree( vASteps );
-
-    Vec_IntFree( vLiterals );
-    Vec_IntFree( vClauses );
-    Vec_IntFree( vResolvent );
-    Aig_ObjCreatePo( p, pInter );
-    Aig_ManCleanup( p );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs one SAT run with interpolation.]
-
-  Description [Returns 1 if proven. 0 if failed. -1 if undecided.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_M144pPerformOneStep( Saig_IntMan_t * p, int fUsePudlak, int fUseOther )
-{
-    M114p_Solver_t pSat;
-    Vec_Int_t * vMapRoots, * vMapVars;
-    int clk, status, RetValue;
-    assert( p->pInterNew == NULL );
-    // derive the SAT solver
-    pSat = Saig_M144pDeriveSatSolver( p->pInter, p->pCnfInter, 
-        p->pAigTrans, p->pCnfAig, p->pFrames, p->pCnfFrames, 
-        &vMapRoots, &vMapVars );
-    // solve the problem
-clk = clock();
-    status = M114p_SolverSolve( pSat, NULL, NULL, 0 );
-    p->nConfCur = M114p_SolverGetConflictNum( pSat );
-p->timeSat += clock() - clk;
-    if ( status == 0 )
-    {
-        RetValue = 1;
-
-        ///// report the savings of the modified Pudlak's approach
-        Saig_M144pInterpolateReport( pSat, vMapRoots, vMapVars );
-        /////
-
-clk = clock();
-        if ( fUseOther )
-            p->pInterNew = Saig_M144pInterpolatePudlakASteps( pSat, vMapRoots, vMapVars );
-        else if ( fUsePudlak )
-            p->pInterNew = Saig_M144pInterpolatePudlak( pSat, vMapRoots, vMapVars );
-        else
-            p->pInterNew = Saig_M144pInterpolate( pSat, vMapRoots, vMapVars );
-p->timeInt += clock() - clk;
-    }
-    else if ( status == 1 )
-    {
-        RetValue = 0;
-    }
-    else
-    {
-        RetValue = -1;
-    }
-    M114p_SolverDelete( pSat );
-    Vec_IntFree( vMapRoots );
-    Vec_IntFree( vMapVars );
-    return RetValue;
-}
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/aig/saig/saigUnique.c b/src/aig/saig/saigUnique.c
deleted file mode 100644
index 8b4d80e7..00000000
--- a/src/aig/saig/saigUnique.c
+++ /dev/null
@@ -1,170 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [saigUnique.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Sequential AIG package.]
-
-  Synopsis    [Containment checking with unique state constraints.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: saigUnique.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "saig.h"
-#include "cnf.h"
-#include "satSolver.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Create timeframes of the manager for interpolation.]
-
-  Description [The resulting manager is combinational. The primary inputs
-  corresponding to register outputs are ordered first.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Saig_ManFramesLatches( Aig_Man_t * pAig, int nFrames, Vec_Ptr_t ** pvMapReg )
-{
-    Aig_Man_t * pFrames;
-    Aig_Obj_t * pObj, * pObjLi, * pObjLo;
-    int i, f;
-    assert( Saig_ManRegNum(pAig) > 0 );
-    pFrames = Aig_ManStart( Aig_ManNodeNum(pAig) * nFrames );
-    // map the constant node
-    Aig_ManConst1(pAig)->pData = Aig_ManConst1( pFrames );
-    // create variables for register outputs
-    *pvMapReg = Vec_PtrAlloc( (nFrames+1) * Saig_ManRegNum(pAig) );
-    Saig_ManForEachLo( pAig, pObj, i )
-    {
-        pObj->pData = Aig_ObjCreatePi( pFrames );
-        Vec_PtrPush( *pvMapReg, pObj->pData );
-    }
-    // add timeframes
-    for ( f = 0; f < nFrames; f++ )
-    {
-        // create PI nodes for this frame
-        Saig_ManForEachPi( pAig, pObj, i )
-            pObj->pData = Aig_ObjCreatePi( pFrames );
-        // add internal nodes of this frame
-        Aig_ManForEachNode( pAig, pObj, i )
-            pObj->pData = Aig_And( pFrames, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-        // save register inputs
-        Saig_ManForEachLi( pAig, pObj, i )
-            pObj->pData = Aig_ObjChild0Copy(pObj);
-        // transfer to register outputs
-        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
-        {
-            pObjLo->pData = pObjLi->pData;
-            Vec_PtrPush( *pvMapReg, pObjLo->pData );
-        }
-    }
-    return pFrames;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Duplicates AIG while mapping PIs into the given array.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Saig_ManAppendCone( Aig_Man_t * pOld, Aig_Man_t * pNew, Aig_Obj_t ** ppNewPis, int fCompl )
-{
-    Aig_Obj_t * pObj;
-    int i;
-    assert( Aig_ManPoNum(pOld) == 1 );
-    // create the PIs
-    Aig_ManCleanData( pOld );
-    Aig_ManConst1(pOld)->pData = Aig_ManConst1(pNew);
-    Aig_ManForEachPi( pOld, pObj, i )
-        pObj->pData = ppNewPis[i];
-    // duplicate internal nodes
-    Aig_ManForEachNode( pOld, pObj, i )
-        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-    // add one PO to new
-    pObj = Aig_ManPo( pOld, 0 );
-    Aig_ObjCreatePo( pNew, Aig_NotCond( Aig_ObjChild0Copy(pObj), fCompl ) );
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Saig_ManUniqueState( Aig_Man_t * pTrans, Vec_Ptr_t * vInters )
-{
-    Aig_Man_t * pFrames, * pInterNext, * pInterThis;
-    Aig_Obj_t ** ppNodes;
-    Vec_Ptr_t * vMapRegs;
-    Cnf_Dat_t * pCnf;
-    sat_solver * pSat;
-    int f, nRegs, status;
-    nRegs = Saig_ManRegNum(pTrans);
-    assert( nRegs > 0 );
-    assert( Vec_PtrSize(vInters) > 1 );
-    // generate the timeframes
-    pFrames = Saig_ManFramesLatches( pTrans, Vec_PtrSize(vInters)-1, &vMapRegs );
-    assert( Vec_PtrSize(vMapRegs) == Vec_PtrSize(vInters) * nRegs );
-    // add main constraints to the timeframes
-    ppNodes = (Aig_Obj_t **)Vec_PtrArray(vMapRegs);
-    Vec_PtrForEachEntryStop( vInters, pInterThis, f, Vec_PtrSize(vInters)-1 )
-    {
-        assert( nRegs == Aig_ManPiNum(pInterThis) );
-        pInterNext = Vec_PtrEntry( vInters, f+1 );
-        Saig_ManAppendCone( pInterNext, pFrames, ppNodes + f * nRegs, 0 );
-        Saig_ManAppendCone( pInterThis, pFrames, ppNodes + f * nRegs, 1 );
-    }
-    Saig_ManAppendCone( Vec_PtrEntryLast(vInters), pFrames, ppNodes + f * nRegs, 1 );
-    Aig_ManCleanup( pFrames );
-    Vec_PtrFree( vMapRegs );
-
-    // convert to CNF
-    pCnf = Cnf_Derive( pFrames, 0 ); 
-    pSat = Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
-    Cnf_DataFree( pCnf );
-    Aig_ManStop( pFrames );
-
-    if ( pSat == NULL )
-        return 1;
-
-     // solve the problem
-    status = sat_solver_solve( pSat, NULL, NULL, (sint64)0, (sint64)0, (sint64)0, (sint64)0 );
-    sat_solver_delete( pSat );
-    return status == l_False;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 09ea8b16..e4b0ad69 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -748,7 +748,7 @@ extern ABC_DLL bool               Abc_NodeIsBuf( Abc_Obj_t * pNode );
 extern ABC_DLL bool               Abc_NodeIsInv( Abc_Obj_t * pNode );    
 extern ABC_DLL void               Abc_NodeComplement( Abc_Obj_t * pNode );
 /*=== abcPrint.c ==========================================================*/
-extern ABC_DLL void               Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib );
+extern ABC_DLL void               Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes );
 extern ABC_DLL void               Abc_NtkPrintIo( FILE * pFile, Abc_Ntk_t * pNtk );
 extern ABC_DLL void               Abc_NtkPrintLatch( FILE * pFile, Abc_Ntk_t * pNtk );
 extern ABC_DLL void               Abc_NtkPrintFanio( FILE * pFile, Abc_Ntk_t * pNtk );
diff --git a/src/base/abc/abcUtil.c b/src/base/abc/abcUtil.c
index 39f44c11..90cf50b0 100644
--- a/src/base/abc/abcUtil.c
+++ b/src/base/abc/abcUtil.c
@@ -933,9 +933,9 @@ bool Abc_NodeIsMuxType( Abc_Obj_t * pNode )
     pNode0 = Abc_ObjFanin0(pNode);
     pNode1 = Abc_ObjFanin1(pNode);
     // if the children are not ANDs, this is not MUX
-    if ( Abc_ObjFaninNum(pNode0) != 2 || Abc_ObjFaninNum(pNode1) != 2 )
+    if ( !Abc_AigNodeIsAnd(pNode0) || !Abc_AigNodeIsAnd(pNode1) )
         return 0;
-    // otherwise the node is MUX iff it has a pair of equal grandchildren
+    // otherwise the node is MUX iff it has a pair of equal grandchildren with opposite polarity
     return (Abc_ObjFaninId0(pNode0) == Abc_ObjFaninId0(pNode1) && (Abc_ObjFaninC0(pNode0) ^ Abc_ObjFaninC0(pNode1))) || 
            (Abc_ObjFaninId0(pNode0) == Abc_ObjFaninId1(pNode1) && (Abc_ObjFaninC0(pNode0) ^ Abc_ObjFaninC1(pNode1))) ||
            (Abc_ObjFaninId1(pNode0) == Abc_ObjFaninId0(pNode1) && (Abc_ObjFaninC1(pNode0) ^ Abc_ObjFaninC0(pNode1))) ||
@@ -944,6 +944,27 @@ bool Abc_NodeIsMuxType( Abc_Obj_t * pNode )
 
 /**Function*************************************************************
 
+  Synopsis    [Returns 1 if the node is the root of MUX or EXOR/NEXOR.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_NtkCountMuxes( Abc_Ntk_t * pNtk )
+{
+    Abc_Obj_t * pNode;
+    int i;
+    int Counter = 0;
+    Abc_NtkForEachNode( pNtk, pNode, i )
+        Counter += Abc_NodeIsMuxType( pNode );
+    return Counter;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Returns 1 if the node is the control type of the MUX.]
 
   Description []
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index b8a9cefe..b0cd2f7e 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -34,6 +34,7 @@
 #include "fra.h"
 #include "saig.h"
 #include "nwkMerge.h"
+#include "int.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -65,6 +66,7 @@ static int Abc_CommandShowCut        ( Abc_Frame_t * pAbc, int argc, char ** arg
 static int Abc_CommandCollapse       ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandStrash         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandBalance        ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandMuxStruct      ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandMulti          ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandRenode         ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandCleanup        ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -327,6 +329,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "Synthesis",    "collapse",      Abc_CommandCollapse,         1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "strash",        Abc_CommandStrash,           1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "balance",       Abc_CommandBalance,          1 );
+    Cmd_CommandAdd( pAbc, "Synthesis",    "mux_struct",    Abc_CommandMuxStruct,        1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "multi",         Abc_CommandMulti,            1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "renode",        Abc_CommandRenode,           1 );
     Cmd_CommandAdd( pAbc, "Synthesis",    "cleanup",       Abc_CommandCleanup,          1 );
@@ -588,6 +591,7 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
     int fDumpResult;
     int fUseLutLib;
     int fPrintTime;
+    int fPrintMuxes;
     int c;
 
     pNtk = Abc_FrameReadNtk(pAbc);
@@ -600,8 +604,9 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
     fDumpResult = 0;
     fUseLutLib = 0;
     fPrintTime = 0;
+    fPrintMuxes = 1;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "fbdlth" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "fbdltmh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -620,6 +625,9 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 't':
             fPrintTime ^= 1;
             break;
+        case 'm':
+            fPrintMuxes ^= 1;
+            break;
         case 'h':
             goto usage;
         default:
@@ -632,7 +640,12 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( Abc_FrameReadErr(pAbc), "Empty network.\n" );
         return 1;
     }
-    Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest, fDumpResult, fUseLutLib );
+    if ( !Abc_NtkIsLogic(pNtk) && fUseLutLib )
+    {
+        fprintf( Abc_FrameReadErr(pAbc), "Cannot print LUT delay for a non-logic network.\n" );
+        return 1;
+    }
+    Abc_NtkPrintStats( pOut, pNtk, fFactor, fSaveBest, fDumpResult, fUseLutLib, fPrintMuxes );
     if ( fPrintTime )
     {
         pAbc->TimeTotal += pAbc->TimeCommand;
@@ -643,13 +656,14 @@ int Abc_CommandPrintStats( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: print_stats [-fbdlth]\n" );
+    fprintf( pErr, "usage: print_stats [-fbdltmh]\n" );
     fprintf( pErr, "\t        prints the network statistics\n" );
     fprintf( pErr, "\t-f    : toggles printing the literal count in the factored forms [default = %s]\n", fFactor? "yes": "no" );
     fprintf( pErr, "\t-b    : toggles saving the best logic network in \"best.blif\" [default = %s]\n", fSaveBest? "yes": "no" );
     fprintf( pErr, "\t-d    : toggles dumping network into file \"<input_file_name>_dump.blif\" [default = %s]\n", fDumpResult? "yes": "no" );
     fprintf( pErr, "\t-l    : toggles printing delay of LUT mapping using LUT library [default = %s]\n", fSaveBest? "yes": "no" );
     fprintf( pErr, "\t-t    : toggles printing runtime statistics [default = %s]\n", fPrintTime? "yes": "no" );
+    fprintf( pErr, "\t-m    : toggles printing MUX statistics [default = %s]\n", fPrintMuxes? "yes": "no" );
     fprintf( pErr, "\t-h    : print the command usage\n");
     return 1;
 }
@@ -735,7 +749,7 @@ int Abc_CommandPrintExdc( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     else
         printf( "EXDC network statistics: \n" );
-    Abc_NtkPrintStats( pOut, pNtk->pExdc, 0, 0, 0, 0 );
+    Abc_NtkPrintStats( pOut, pNtk->pExdc, 0, 0, 0, 0, 0 );
     return 0;
 
 usage:
@@ -2483,6 +2497,78 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandMuxStruct( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    FILE * pOut, * pErr;
+    Abc_Ntk_t * pNtk, * pNtkRes;
+    int c;
+    int fVerbose;
+
+    extern Abc_Ntk_t * Abc_NtkMuxRestructure( Abc_Ntk_t * pNtk, int fVerbose );
+
+    pNtk = Abc_FrameReadNtk(pAbc);
+    pOut = Abc_FrameReadOut(pAbc);
+    pErr = Abc_FrameReadErr(pAbc);
+
+    // set defaults
+    fVerbose     = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+
+    if ( pNtk == NULL )
+    {
+        fprintf( pErr, "Empty network.\n" );
+        return 1;
+    }
+    // get the new network
+    if ( !Abc_NtkIsStrash(pNtk) )
+    {
+        fprintf( pErr, "Does not work for a logic network.\n" );
+        return 1;
+    }
+    // check if balancing worked
+//    pNtkRes = Abc_NtkMuxRestructure( pNtk, fVerbose );
+    pNtkRes = NULL;
+    if ( pNtkRes == NULL )
+    {
+        fprintf( pErr, "MUX restructuring has failed.\n" );
+        return 1;
+    }
+    // replace the current network
+    Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
+    return 0;
+
+usage:
+    fprintf( pErr, "usage: mux_struct [-vh]\n" );
+    fprintf( pErr, "\t        performs MUX restructuring of the current network\n" );
+    fprintf( pErr, "\t-v    : print verbose information [default = %s]\n", fVerbose? "yes": "no" ); 
+    fprintf( pErr, "\t-h    : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandMulti( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     FILE * pOut, * pErr;
@@ -15494,6 +15580,7 @@ usage:
     return 1;
 }
   
+
 /**Function*************************************************************
 
   Synopsis    []
@@ -15507,39 +15594,21 @@ usage:
 ***********************************************************************/
 int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
+    Inter_ManParams_t Pars, * pPars = &Pars;
     FILE * pOut, * pErr;
     Abc_Ntk_t * pNtk;
     int c;
-    int nBTLimit;
-    int nFramesMax;
-    int fRewrite;
-    int fTransLoop;
-    int fUsePudlak;
-    int fUseOther;
-    int fUseMiniSat;
-    int fCheckInd;
-    int fCheckKstep;
-    int fVerbose;
 
-    extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose );
+    extern int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
     pErr = Abc_FrameReadErr(pAbc);
 
     // set defaults
-    nBTLimit   = 20000;
-    nFramesMax = 40;
-    fRewrite   = 0;
-    fTransLoop = 1;
-    fUsePudlak = 0;
-    fUseOther  = 0;
-    fUseMiniSat= 0;
-    fCheckInd  = 0;
-    fCheckKstep= 0;
-    fVerbose   = 0;
+    Inter_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CFrtpomikvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CNFrtpomcgbvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -15549,9 +15618,20 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-C\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nBTLimit = atoi(argv[globalUtilOptind]);
+            pPars->nBTLimit = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nBTLimit < 0 ) 
+            if ( pPars->nBTLimit < 0 ) 
+                goto usage;
+            break;
+        case 'N':
+            if ( globalUtilOptind >= argc )
+            {
+                fprintf( pErr, "Command line switch \"-N\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nFramesMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nFramesMax < 0 ) 
                 goto usage;
             break;
         case 'F':
@@ -15560,34 +15640,37 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
                 fprintf( pErr, "Command line switch \"-F\" should be followed by an integer.\n" );
                 goto usage;
             }
-            nFramesMax = atoi(argv[globalUtilOptind]);
+            pPars->nFramesK = atoi(argv[globalUtilOptind]);
             globalUtilOptind++;
-            if ( nFramesMax < 0 ) 
+            if ( pPars->nFramesK < 0 ) 
                 goto usage;
             break;
         case 'r':
-            fRewrite ^= 1;
+            pPars->fRewrite ^= 1;
             break;
         case 't':
-            fTransLoop ^= 1;
+            pPars->fTransLoop ^= 1;
             break;
         case 'p':
-            fUsePudlak ^= 1;
+            pPars->fUsePudlak ^= 1;
             break;
         case 'o':
-            fUseOther ^= 1;
+            pPars->fUseOther ^= 1;
             break;
         case 'm':
-            fUseMiniSat ^= 1;
+            pPars->fUseMiniSat ^= 1;
             break;
-        case 'i':
-            fCheckInd ^= 1;
+        case 'c':
+            pPars->fCheckKstep ^= 1;
             break;
-        case 'k':
-            fCheckKstep ^= 1;
+        case 'g':
+            pPars->fUseBias ^= 1;
+            break;
+        case 'b':
+            pPars->fUseBackward ^= 1;
             break;
         case 'v':
-            fVerbose ^= 1;
+            pPars->fVerbose ^= 1;
             break;
         case 'h':
             goto usage;
@@ -15615,22 +15698,24 @@ int Abc_CommandBmcInter( Abc_Frame_t * pAbc, int argc, char ** argv )
         fprintf( stdout, "Currently only works for single-output miters (run \"orpos\").\n" );
         return 0;
     }
-    Abc_NtkDarBmcInter( pNtk, nBTLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fUseOther, fUseMiniSat, fCheckInd, fCheckKstep, fVerbose );
+    Abc_NtkDarBmcInter( pNtk, pPars );
     return 0;
 
 usage:
-    fprintf( pErr, "usage: int [-CF num] [-rtpomikvh]\n" );
+    fprintf( pErr, "usage: int [-CNF num] [-rtpomcgbvh]\n" );
     fprintf( pErr, "\t         uses interpolation to prove the property\n" );
-    fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", nBTLimit );
-    fprintf( pErr, "\t-F num : the limit on number of frames to unroll [default = %d]\n", nFramesMax );
-    fprintf( pErr, "\t-r     : toggle the use of rewriting [default = %s]\n", fRewrite? "yes": "no" );
-    fprintf( pErr, "\t-t     : toggle adding transition into the init state [default = %s]\n", fTransLoop? "yes": "no" );
-    fprintf( pErr, "\t-p     : toggle using original Pudlak's interpolation procedure [default = %s]\n", fUsePudlak? "yes": "no" );
-    fprintf( pErr, "\t-o     : toggle using optimized Pudlak's interpolation procedure [default = %s]\n", fUseOther? "yes": "no" );
-    fprintf( pErr, "\t-m     : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", fUseMiniSat? "yes": "no" );
-    fprintf( pErr, "\t-i     : toggle inductive containment checking [default = %s]\n", fCheckInd? "yes": "no" );
-    fprintf( pErr, "\t-k     : toggle simple and k-step induction [default = %s]\n", fCheckKstep? "k-step": "simple" );
-    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );
+    fprintf( pErr, "\t-C num : the limit on conflicts for one SAT run [default = %d]\n", pPars->nBTLimit );
+    fprintf( pErr, "\t-N num : the limit on number of frames to unroll [default = %d]\n", pPars->nFramesMax );
+    fprintf( pErr, "\t-F num : the number of steps in inductive checking [default = %d]\n", pPars->nFramesK );
+    fprintf( pErr, "\t-r     : toggle the use of rewriting unrolled timeframes [default = %s]\n", pPars->fRewrite? "yes": "no" );
+    fprintf( pErr, "\t-t     : toggle adding transition into the init state [default = %s]\n", pPars->fTransLoop? "yes": "no" );
+    fprintf( pErr, "\t-p     : toggle using original Pudlak's interpolation procedure [default = %s]\n", pPars->fUsePudlak? "yes": "no" );
+    fprintf( pErr, "\t-o     : toggle using optimized Pudlak's interpolation procedure [default = %s]\n", pPars->fUseOther? "yes": "no" );
+    fprintf( pErr, "\t-m     : toggle using MiniSat-1.14p (now, Windows-only) [default = %s]\n", pPars->fUseMiniSat? "yes": "no" );
+    fprintf( pErr, "\t-c     : toggle using inductive containment check [default = %s]\n", pPars->fCheckKstep? "yes": "no" );
+    fprintf( pErr, "\t-g     : toggle using bias for global variables using SAT [default = %s]\n", pPars->fUseBias? "yes": "no" );
+    fprintf( pErr, "\t-b     : toggle using backward interpolation [default = %s]\n", pPars->fUseBackward? "yes": "no" );
+    fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", pPars->fVerbose? "yes": "no" );
     fprintf( pErr, "\t-h     : print the command usage\n");
     return 1;
 }
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 03790c4b..71f84272 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -25,6 +25,7 @@
 #include "cnf.h"
 #include "fra.h"
 #include "fraig.h"
+#include "int.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -1295,7 +1296,7 @@ PRT( "Time", clock() - clk );
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose )
+int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, Inter_ManParams_t * pPars )
 {
     Aig_Man_t * pMan;
     int RetValue, Depth, clk = clock();
@@ -1307,7 +1308,7 @@ int Abc_NtkDarBmcInter( Abc_Ntk_t * pNtk, int nConfLimit, int nFramesMax, int fR
         return -1;
     }
     assert( pMan->nRegs > 0 );
-    RetValue = Saig_Interpolate( pMan, nConfLimit, nFramesMax, fRewrite, fTransLoop, fUsePudlak, fUseOther, fUseMiniSat, fCheckInd, fCheckKstep, fVerbose, &Depth );
+    RetValue = Inter_ManPerformInterpolation( pMan, pPars, &Depth );
     if ( RetValue == 1 )
         printf( "Property proved.  " );
     else if ( RetValue == 0 )
diff --git a/src/base/abci/abcPrint.c b/src/base/abci/abcPrint.c
index b753700e..2e01a141 100644
--- a/src/base/abci/abcPrint.c
+++ b/src/base/abci/abcPrint.c
@@ -111,7 +111,7 @@ int Abc_NtkCompareAndSaveBest( Abc_Ntk_t * pNtk )
   SeeAlso     []
 
 ***********************************************************************/
-void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib )
+void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSaveBest, int fDumpResult, int fUseLutLib, int fPrintMuxes )
 {
     int Num;
 
@@ -153,6 +153,12 @@ void Abc_NtkPrintStats( FILE * pFile, Abc_Ntk_t * pNtk, int fFactored, int fSave
 //            fprintf( pFile, " (mux = %d)", Num2-Num );
 //        if ( Num2 )
 //            fprintf( pFile, " (other = %d)", Abc_NtkNodeNum(pNtk)-3*Num2 );
+        if ( fPrintMuxes )
+        {
+            extern int Abc_NtkCountMuxes( Abc_Ntk_t * pNtk );
+            fprintf( pFile, " (mux = %d)", Abc_NtkCountMuxes(pNtk)-Num );
+            fprintf( pFile, " (pure and = %d)", Abc_NtkNodeNum(pNtk) - (Abc_NtkCountMuxes(pNtk) * 3) );
+        }
     }
     else 
     {
diff --git a/src/base/io/ioWriteDot.c b/src/base/io/ioWriteDot.c
index 54beb8b6..64be1425 100644
--- a/src/base/io/ioWriteDot.c
+++ b/src/base/io/ioWriteDot.c
@@ -275,6 +275,12 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
         fprintf( pFile, "  Level%d;\n",  Level );
         Vec_PtrForEachEntry( vNodes, pNode, i )
         {
+            if ( (int)pNode->Level != Level )
+                continue;
+            if ( Abc_ObjFaninNum(pNode) == 0 )
+                continue;
+
+/*
             int SuppSize;
             Vec_Ptr_t * vSupp;
             if ( (int)pNode->Level != Level )
@@ -284,6 +290,7 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
             vSupp = Abc_NtkNodeSupport( pNtk, &pNode, 1 );
             SuppSize = Vec_PtrSize( vSupp );
             Vec_PtrFree( vSupp ); 
+*/
 
 //            fprintf( pFile, "  Node%d [label = \"%d\"", pNode->Id, pNode->Id );
             if ( Abc_NtkIsStrash(pNtk) )
@@ -294,10 +301,10 @@ void Io_WriteDotNtk( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, Vec_Ptr_t * vNodesSho
                 pSopString = Abc_NtkPrintSop(Mio_GateReadSop(pNode->pData));
             else
                 pSopString = Abc_NtkPrintSop(pNode->pData);
-//            fprintf( pFile, "  Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString );
-            fprintf( pFile, "  Node%d [label = \"%d\\n%s\"", pNode->Id, 
-                SuppSize, 
-                pSopString );
+            fprintf( pFile, "  Node%d [label = \"%d\\n%s\"", pNode->Id, pNode->Id, pSopString );
+//            fprintf( pFile, "  Node%d [label = \"%d\\n%s\"", pNode->Id, 
+//                SuppSize, 
+//                pSopString );
 
             fprintf( pFile, ", shape = ellipse" );
             if ( pNode->fMarkB )
diff --git a/src/map/mapper/mapperTree.c b/src/map/mapper/mapperTree.c
index 76c1e520..6e69bc69 100644
--- a/src/map/mapper/mapperTree.c
+++ b/src/map/mapper/mapperTree.c
@@ -34,7 +34,7 @@ static int           Map_LibraryGetMaxSuperPi_rec( Map_Super_t * pGate );
 static unsigned      Map_LibraryGetGateSupp_rec( Map_Super_t * pGate );
 
 // fanout limits
-static const int s_MapFanoutLimits[10] = { 1/*0*/, 10/*1*/, 5/*2*/, 2/*3*/, 1/*4*/, 1/*5*/, 1/*6*/ };
+extern const int s_MapFanoutLimits[10] = { 1/*0*/, 10/*1*/, 5/*2*/, 2/*3*/, 1/*4*/, 1/*5*/, 1/*6*/ };
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -124,7 +124,14 @@ int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileNam
     
     // get the genlib file name (base)
     pLibName = strtok( pTemp, " \t\r\n" );
-    
+#ifdef __linux__
+    if( strchr( pLibName, '/' ) != NULL )
+        pLibName = strrchr( pLibName, '/' ) + 1;
+#else
+    if( strchr( pLibName, '\\' ) != NULL )
+        pLibName = strrchr( pLibName, '\\' ) + 1;
+#endif
+
     if ( strcmp( pLibName, "GATE" ) == 0 )
     {
         printf( "The input file \"%s\" looks like a GENLIB file and not a supergate library file.\n", pLib->pName );
@@ -145,7 +152,7 @@ int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileNam
         if ( pStr == pLibFile )
             strcpy( pLibFile, pLibName );
         else
-            sprintf( pStr, "/%s", pLibName );
+            sprintf( pStr, "\\%s", pLibName );
     }
 #endif
     
diff --git a/src/map/mapper/mapperTree_old.c b/src/map/mapper/mapperTree_old.c
new file mode 100644
index 00000000..041ba2a0
--- /dev/null
+++ b/src/map/mapper/mapperTree_old.c
@@ -0,0 +1,823 @@
+/**CFile****************************************************************
+
+  FileName    [mapperTree.c]
+
+  PackageName [MVSIS 1.3: Multi-valued logic synthesis system.]
+
+  Synopsis    [Generic technology mapping engine.]
+
+  Author      [MVSIS Group]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 2.0. Started - June 1, 2004.]
+
+  Revision    [$Id: mapperTree.c,v 1.9 2005/01/23 06:59:45 alanmi Exp $]
+
+***********************************************************************/
+
+#ifdef __linux__
+#include <libgen.h>
+#endif
+
+#include "mapperInt.h"
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static int           Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileName );
+static Map_Super_t * Map_LibraryReadGateTree( Map_SuperLib_t * pLib, char * pBuffer, int Number, int nVars );
+static int           Map_LibraryDeriveGateInfo( Map_SuperLib_t * pLib, st_table * tExcludeGate );
+static void          Map_LibraryAddFaninDelays( Map_SuperLib_t * pLib, Map_Super_t * pGate, Map_Super_t * pFanin, Mio_Pin_t * pPin );
+static int           Map_LibraryGetMaxSuperPi_rec( Map_Super_t * pGate );
+static unsigned      Map_LibraryGetGateSupp_rec( Map_Super_t * pGate );
+
+// fanout limits
+extern const int s_MapFanoutLimits[10] = { 1/*0*/, 10/*1*/, 5/*2*/, 2/*3*/, 1/*4*/, 1/*5*/, 1/*6*/ };
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the supergate library from file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Map_LibraryReadTree( Map_SuperLib_t * pLib, char * pFileName, char * pExcludeFile )
+{
+    FILE * pFile;
+    int Status, num;
+    Abc_Frame_t * pAbc;
+    st_table * tExcludeGate = 0;
+
+    // read the beginning of the file
+    assert( pLib->pGenlib == NULL );
+    pFile = Io_FileOpen( pFileName, "open_path", "r", 1 );
+//    pFile = fopen( pFileName, "r" ); 
+    if ( pFile == NULL )
+    {
+        printf( "Cannot open input file \"%s\".\n", pFileName );
+        return 0;
+    }
+
+    if ( pExcludeFile )
+    {
+        pAbc = Abc_FrameGetGlobalFrame();
+        
+        tExcludeGate = st_init_table(strcmp, st_strhash);
+        if ( (num = Mio_LibraryReadExclude( pAbc, pExcludeFile, tExcludeGate )) == -1 )
+        {
+            st_free_table( tExcludeGate );
+            tExcludeGate = 0;
+            return 0;
+        }
+
+        fprintf ( Abc_FrameReadOut( pAbc ), "Read %d gates from exclude file\n", num );
+    }
+    
+    Status = Map_LibraryReadFileTree( pLib, pFile, pFileName );
+    fclose( pFile );
+    if ( Status == 0 )
+        return 0;
+    // prepare the info about the library
+    return Map_LibraryDeriveGateInfo( pLib, tExcludeGate );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the library file.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Map_LibraryReadFileTree( Map_SuperLib_t * pLib, FILE * pFile, char *pFileName )
+{
+    ProgressBar * pProgress;
+    char pBuffer[5000], pLibFile[5000];
+    FILE * pFileGen;
+    Map_Super_t * pGate;
+    char * pTemp = 0, * pLibName;
+    int nCounter, k, i;
+
+    // skip empty and comment lines
+    while ( fgets( pBuffer, 5000, pFile ) != NULL )
+    {
+        // skip leading spaces
+        for ( pTemp = pBuffer; *pTemp == ' ' || *pTemp == '\r' || *pTemp == '\n'; pTemp++ );
+        // skip comment lines and empty lines
+        if ( *pTemp != 0 && *pTemp != '#' )
+            break;
+    }
+    
+    // get the genlib file name (base)
+    pLibName = strtok( pTemp, " \t\r\n" );
+#ifdef __linux__
+    pLibName = strrchr( pLibName, '/' )+1;
+#else
+    pLibName = strrchr( pLibName, '\\' )+1;
+#endif
+
+    if ( strcmp( pLibName, "GATE" ) == 0 )
+    {
+        printf( "The input file \"%s\" looks like a GENLIB file and not a supergate library file.\n", pLib->pName );
+        return 0;
+    }
+    
+
+    // now figure out the directory if any in the pFileName
+#ifdef __linux__
+    snprintf( pLibFile, 5000, "%s/%s", dirname(strdup(pFileName)), pLibName ); 
+#else
+    {
+        char * pStr;
+        strcpy( pLibFile, pFileName );
+        pStr = pLibFile + strlen(pBuffer) - 1;
+        while ( pStr > pLibFile && *pStr != '\\' && *pStr != '/' )
+            pStr--;
+        if ( pStr == pLibFile )
+            strcpy( pLibFile, pLibName );
+        else
+            sprintf( pStr, "\\%s", pLibName );
+    }
+#endif
+    
+    pFileGen = Io_FileOpen( pLibFile, "open_path", "r", 1 );
+//    pFileGen = fopen( pLibFile, "r" ); 
+    if ( pFileGen == NULL )
+    {
+        printf( "Cannot open the GENLIB file \"%s\".\n", pLibFile );
+        return 0;
+    }
+    fclose( pFileGen );
+
+    // read the genlib library
+    pLib->pGenlib = Mio_LibraryRead( Abc_FrameGetGlobalFrame(), pLibFile, 0, 0 );
+    if ( pLib->pGenlib == NULL )
+    {
+        printf( "Cannot read GENLIB file \"%s\".\n", pLibFile );
+        return 0;
+    }
+
+    // read the number of variables
+    fscanf( pFile, "%d\n", &pLib->nVarsMax );
+    if ( pLib->nVarsMax < 2 || pLib->nVarsMax > 10 )
+    {
+        printf( "Suspicious number of variables (%d).\n", pLib->nVarsMax );
+        return 0;
+    }
+
+    // read the number of gates
+    fscanf( pFile, "%d\n", &pLib->nSupersReal );
+    if ( pLib->nSupersReal < 1 || pLib->nSupersReal > 10000000 )
+    {
+        printf( "Suspicious number of gates (%d).\n", pLib->nSupersReal );
+        return 0;
+    }
+
+    // read the number of lines
+    fscanf( pFile, "%d\n", &pLib->nLines );
+    if ( pLib->nLines < 1 || pLib->nLines > 10000000 )
+    {
+        printf( "Suspicious number of lines (%d).\n", pLib->nLines );
+        return 0;
+    }
+
+    // allocate room for supergate pointers
+    pLib->ppSupers = ALLOC( Map_Super_t *, pLib->nLines + 10000 );
+
+    // create the elementary supergates
+    for ( i = 0; i < pLib->nVarsMax; i++ )
+    {
+        // get a new gate
+        pGate = (Map_Super_t *)Extra_MmFixedEntryFetch( pLib->mmSupers );
+        memset( pGate, 0, sizeof(Map_Super_t) );
+        // assign the elementary variable, the truth table, and the delays
+        pGate->Num = i;
+        // set the truth table
+        pGate->uTruth[0] = pLib->uTruths[i][0];
+        pGate->uTruth[1] = pLib->uTruths[i][1];
+        // set the arrival times of all input to non-existent delay
+        for ( k = 0; k < pLib->nVarsMax; k++ )
+        {
+            pGate->tDelaysR[k].Rise = pGate->tDelaysR[k].Fall = MAP_NO_VAR;
+            pGate->tDelaysF[k].Rise = pGate->tDelaysF[k].Fall = MAP_NO_VAR;
+        }
+        // set an existent arrival time for rise and fall
+        pGate->tDelaysR[i].Rise = 0.0;
+        pGate->tDelaysF[i].Fall = 0.0;
+        // set the gate
+        pLib->ppSupers[i] = pGate;
+    }
+
+    // read the lines
+    nCounter = pLib->nVarsMax;
+    pProgress = Extra_ProgressBarStart( stdout, pLib->nLines );
+    while ( fgets( pBuffer, 5000, pFile ) != NULL )
+    {
+        for ( pTemp = pBuffer; *pTemp == ' ' || *pTemp == '\r' || *pTemp == '\n'; pTemp++ );
+        if ( pTemp[0] == '\0' )
+            continue;
+//        if ( pTemp[0] == 'a' || pTemp[2] == 'a' )
+//        {
+//            pLib->nLines--;
+//            continue;
+//        }
+
+        // get the gate
+        pGate = Map_LibraryReadGateTree( pLib, pTemp, nCounter, pLib->nVarsMax );
+        if ( pGate == NULL )
+        {
+            Extra_ProgressBarStop( pProgress );
+            return 0;
+        }
+        pLib->ppSupers[nCounter++] = pGate;
+        // later we will derive: truth table, delays, area, number of component gates, etc
+
+        // update the progress bar
+        Extra_ProgressBarUpdate( pProgress, nCounter, NULL );
+    }
+    Extra_ProgressBarStop( pProgress );
+    if ( nCounter != pLib->nLines )
+        printf( "The number of lines read (%d) is different what the file says (%d).\n", nCounter, pLib->nLines );
+    pLib->nSupersAll = nCounter;
+    // count the number of real supergates
+    nCounter = 0;
+    for ( k = 0; k < pLib->nLines; k++ )
+        nCounter += pLib->ppSupers[k]->fSuper;
+    if ( nCounter != pLib->nSupersReal )
+        printf( "The number of gates read (%d) is different what the file says (%d).\n", nCounter, pLib->nSupersReal );
+    pLib->nSupersReal = nCounter;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads one gate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Map_Super_t * Map_LibraryReadGateTree( Map_SuperLib_t * pLib, char * pBuffer, int Number, int nVarsMax )
+{
+    Map_Super_t * pGate;
+    char * pTemp;
+    int i, Num;
+
+    // start and clean the gate
+    pGate = (Map_Super_t *)Extra_MmFixedEntryFetch( pLib->mmSupers );
+    memset( pGate, 0, sizeof(Map_Super_t) );
+
+    // set the gate number
+    pGate->Num = Number;
+
+    // read the mark
+    pTemp = strtok( pBuffer, " " );
+    if ( pTemp[0] == '*' )
+    {
+        pGate->fSuper = 1;
+        pTemp = strtok( NULL, " " );
+    }
+
+    // read the root gate
+    pGate->pRoot = Mio_LibraryReadGateByName( pLib->pGenlib, pTemp );
+    if ( pGate->pRoot == NULL )
+    {
+        printf( "Cannot read the root gate names %s.\n", pTemp );
+        return NULL;
+    }
+    // set the max number of fanouts
+    pGate->nFanLimit = s_MapFanoutLimits[ Mio_GateReadInputs(pGate->pRoot) ];
+
+    // read the pin-to-pin delay
+    for ( i = 0; ( pTemp = strtok( NULL, " \n\0" ) ); i++ )
+    {
+        if ( pTemp[0] == '#' )
+            break;
+        if ( i == nVarsMax )
+        {
+            printf( "There are too many entries on the line.\n" );
+            return NULL;
+        }
+        Num = atoi(pTemp);
+        if ( Num < 0 )
+        {
+            printf( "The number of a child supergate is negative.\n" );
+            return NULL;
+        }
+        if ( Num > pLib->nLines )
+        {
+            printf( "The number of a child supergate (%d) exceeded the number of lines (%d).\n", 
+                Num, pLib->nLines );
+            return NULL;
+        }
+        pGate->pFanins[i] = pLib->ppSupers[Num];
+    }
+    pGate->nFanins = i;
+    if ( pGate->nFanins != (unsigned)Mio_GateReadInputs(pGate->pRoot) )
+    {
+        printf( "The number of fanins of a root gate is wrong.\n" );
+        return NULL;
+    }
+
+    // save the gate name, just in case
+    if ( pTemp && pTemp[0] == '#' )
+    {
+        if ( pTemp[1] == 0 )
+            pTemp = strtok( NULL, " \n\0" );
+        else // skip spaces
+            for ( pTemp++; *pTemp == ' '; pTemp++ );
+        // save the formula
+        pGate->pFormula = Extra_MmFlexEntryFetch( pLib->mmForms, strlen(pTemp)+1 );
+        strcpy( pGate->pFormula, pTemp );
+    }
+    // check the rest of the string
+    pTemp = strtok( NULL, " \n\0" );
+    if ( pTemp != NULL )
+        printf( "The following trailing symbols found \"%s\".\n", pTemp );
+    return pGate;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives information about the library.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Map_LibraryDeriveGateInfo( Map_SuperLib_t * pLib, st_table * tExcludeGate )
+{
+    Map_Super_t * pGate, * pFanin;
+    Mio_Pin_t * pPin;
+    unsigned uCanon[2];
+    unsigned uTruths[6][2];
+    int i, k, nRealVars;
+
+    // set all the derivable info related to the supergates
+    for ( i = pLib->nVarsMax; i < (int)pLib->nLines; i++ )
+    {
+        pGate = pLib->ppSupers[i];
+
+        if ( tExcludeGate )
+        {
+            if ( st_is_member( tExcludeGate, Mio_GateReadName( pGate->pRoot ) ) )
+                pGate->fExclude = 1;
+            for ( k = 0; k < (int)pGate->nFanins; k++ )
+            {
+                pFanin = pGate->pFanins[k];
+                if ( pFanin->fExclude )
+                {
+                    pGate->fExclude = 1;
+                    continue;
+                }
+            }
+        }
+        
+        // collect the truth tables of the fanins
+        for ( k = 0; k < (int)pGate->nFanins; k++ )
+        {
+            pFanin = pGate->pFanins[k];
+            uTruths[k][0] = pFanin->uTruth[0];
+            uTruths[k][1] = pFanin->uTruth[1];
+        }
+        // derive the new truth table
+        Mio_DeriveTruthTable( pGate->pRoot, uTruths, pGate->nFanins, 6, pGate->uTruth );
+
+        // set the initial delays of the supergate
+        for ( k = 0; k < pLib->nVarsMax; k++ )
+        {
+            pGate->tDelaysR[k].Rise = pGate->tDelaysR[k].Fall = MAP_NO_VAR;
+            pGate->tDelaysF[k].Rise = pGate->tDelaysF[k].Fall = MAP_NO_VAR;
+        }
+        // get the linked list of pins for the given root gate
+        pPin = Mio_GateReadPins( pGate->pRoot );
+        // update the initial delay of the supergate using info from the corresponding pin
+        for ( k = 0; k < (int)pGate->nFanins; k++, pPin = Mio_PinReadNext(pPin) )
+        {
+            // if there is no corresponding pin, this is a bug, return fail
+            if ( pPin == NULL )
+            {
+                printf( "There are less pins than gate inputs.\n" );
+                return 0;
+            }
+            // update the delay information of k-th fanins info from the corresponding pin
+            Map_LibraryAddFaninDelays( pLib, pGate, pGate->pFanins[k], pPin );
+        }
+        // if there are some pins left, this is a bug, return fail
+        if ( pPin != NULL )
+        {
+            printf( "There are more pins than gate inputs.\n" );
+            return 0;
+        }
+        // find the max delay
+        pGate->tDelayMax.Rise = pGate->tDelayMax.Fall = MAP_NO_VAR;
+        for ( k = 0; k < pLib->nVarsMax; k++ )
+        {
+            // the rise of the output depends on the rise and fall of the output
+            if ( pGate->tDelayMax.Rise < pGate->tDelaysR[k].Rise )
+                pGate->tDelayMax.Rise = pGate->tDelaysR[k].Rise;
+            if ( pGate->tDelayMax.Rise < pGate->tDelaysR[k].Fall )
+                pGate->tDelayMax.Rise = pGate->tDelaysR[k].Fall;
+            // the fall of the output depends on the rise and fall of the output
+            if ( pGate->tDelayMax.Fall < pGate->tDelaysF[k].Rise )
+                pGate->tDelayMax.Fall = pGate->tDelaysF[k].Rise;
+            if ( pGate->tDelayMax.Fall < pGate->tDelaysF[k].Fall )
+                pGate->tDelayMax.Fall = pGate->tDelaysF[k].Fall;
+
+            pGate->tDelaysF[k].Worst = MAP_MAX( pGate->tDelaysF[k].Fall, pGate->tDelaysF[k].Rise );
+            pGate->tDelaysR[k].Worst = MAP_MAX( pGate->tDelaysR[k].Fall, pGate->tDelaysR[k].Rise );
+        }
+
+        // count gates and area of the supergate
+        pGate->nGates = 1;
+        pGate->Area   = (float)Mio_GateReadArea(pGate->pRoot);
+        for ( k = 0; k < (int)pGate->nFanins; k++ )
+        {
+            pGate->nGates += pGate->pFanins[k]->nGates;
+            pGate->Area   += pGate->pFanins[k]->Area;
+        }
+        // do not add the gate to the table, if this gate is an internal gate
+        // of some supegate and does not correspond to a supergate output
+        if ( ( !pGate->fSuper ) || pGate->fExclude )
+            continue;
+
+        // find the maximum index of a variable in the support of the supergates
+        // this is important for two reasons:
+        // (1) to limit the number of permutations considered for canonicization
+        // (2) to get rid of equivalence phases to speed-up matching
+        nRealVars = Map_LibraryGetMaxSuperPi_rec( pGate ) + 1;
+        assert( nRealVars > 0 && nRealVars <= pLib->nVarsMax );
+        // if there are some problems with this code, try this instead
+//        nRealVars = pLib->nVarsMax;
+
+        // find the N-canonical form of this supergate
+        pGate->nPhases = Map_CanonComputeSlow( pLib->uTruths, pLib->nVarsMax, nRealVars, pGate->uTruth, pGate->uPhases, uCanon );
+        // add the supergate into the table by its N-canonical table
+        Map_SuperTableInsertC( pLib->tTableC, uCanon, pGate );
+/*
+        {
+            int uCanon1, uCanon2;
+            uCanon1 = uCanon[0];
+            pGate->uTruth[0] = ~pGate->uTruth[0];
+            pGate->uTruth[1] = ~pGate->uTruth[1];
+            Map_CanonComputeSlow( pLib->uTruths, pLib->nVarsMax, nRealVars, pGate->uTruth, pGate->uPhases, uCanon );
+            uCanon2 = uCanon[0];
+Rwt_Man5ExploreCount( uCanon1 < uCanon2 ? uCanon1 : uCanon2 );
+        }
+*/
+    }
+    // sort the gates in each line
+    Map_SuperTableSortSupergatesByDelay( pLib->tTableC, pLib->nSupersAll );
+
+    // let the glory be manifest
+//    Map_LibraryPrintTree( pLib );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the largest PI number in the support of the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Map_LibraryGetMaxSuperPi_rec( Map_Super_t * pGate )
+{
+    int i, VarCur, VarMax = 0;
+    if ( pGate->pRoot == NULL )
+        return pGate->Num;
+    for ( i = 0; i < (int)pGate->nFanins; i++ )
+    {
+        VarCur = Map_LibraryGetMaxSuperPi_rec( pGate->pFanins[i] );
+        if ( VarMax < VarCur )
+            VarMax = VarCur;
+    }
+    return VarMax;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Finds the largest PI number in the support of the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Map_LibraryGetGateSupp_rec( Map_Super_t * pGate )
+{
+    unsigned uSupport;
+    int i;
+    if ( pGate->pRoot == NULL )
+        return (unsigned)(1 << (pGate->Num));
+    uSupport = 0;
+    for ( i = 0; i < (int)pGate->nFanins; i++ )
+        uSupport |= Map_LibraryGetGateSupp_rec( pGate->pFanins[i] );
+    return uSupport;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives the pin-to-pin delay constraints for the supergate.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_LibraryAddFaninDelays( Map_SuperLib_t * pLib, Map_Super_t * pGate, Map_Super_t * pFanin, Mio_Pin_t * pPin )
+{
+    Mio_PinPhase_t PinPhase;
+    float tDelayBlockRise, tDelayBlockFall, tDelayPin;
+    bool fMaxDelay = 0;
+    int i;
+
+    // use this node to enable max-delay model
+    if ( fMaxDelay )
+    {
+        float tDelayBlockMax;
+        // get the maximum delay
+        tDelayBlockMax = (float)Mio_PinReadDelayBlockMax(pPin);
+        // go through the supergate inputs
+        for ( i = 0; i < pLib->nVarsMax; i++ )
+        {
+            if ( pFanin->tDelaysR[i].Rise < 0 )
+                continue;
+            tDelayPin = pFanin->tDelaysR[i].Rise + tDelayBlockMax;
+            if ( pGate->tDelaysR[i].Rise < tDelayPin )
+                pGate->tDelaysR[i].Rise = tDelayPin;
+        }
+        // go through the supergate inputs
+        for ( i = 0; i < pLib->nVarsMax; i++ )
+        {
+            if ( pFanin->tDelaysF[i].Fall < 0 )
+                continue;
+            tDelayPin = pFanin->tDelaysF[i].Fall + tDelayBlockMax;
+            if ( pGate->tDelaysF[i].Fall < tDelayPin )
+                pGate->tDelaysF[i].Fall = tDelayPin;
+        }
+        return;
+    }
+
+    // get the interesting parameters of this pin
+    PinPhase = Mio_PinReadPhase(pPin);
+    tDelayBlockRise = (float)Mio_PinReadDelayBlockRise( pPin );  
+    tDelayBlockFall = (float)Mio_PinReadDelayBlockFall( pPin );  
+
+    // update the rise and fall of the output depending on the phase of the pin 
+    if ( PinPhase != MIO_PHASE_INV )  // NONINV phase is present
+    {
+        // the rise of the gate is determined by the rise of the fanin
+        // the fall of the gate is determined by the fall of the fanin
+        for ( i = 0; i < pLib->nVarsMax; i++ )
+        {
+            ////////////////////////////////////////////////////////
+            // consider the rise of the gate
+            ////////////////////////////////////////////////////////
+            // check two types of constraints on the rise of the fanin:
+            // (1) the constraints related to the rise of the PIs
+            // (2) the constraints related to the fall of the PIs
+            if ( pFanin->tDelaysR[i].Rise >= 0 ) // case (1)
+            { // fanin's rise depends on the rise of i-th PI
+                // update the rise of the gate's output
+                if ( pGate->tDelaysR[i].Rise < pFanin->tDelaysR[i].Rise + tDelayBlockRise )
+                    pGate->tDelaysR[i].Rise = pFanin->tDelaysR[i].Rise + tDelayBlockRise;
+            }
+            if ( pFanin->tDelaysR[i].Fall >= 0 ) // case (2)
+            { // fanin's rise depends on the fall of i-th PI
+                // update the rise of the gate's output
+                if ( pGate->tDelaysR[i].Fall < pFanin->tDelaysR[i].Fall + tDelayBlockRise )
+                    pGate->tDelaysR[i].Fall = pFanin->tDelaysR[i].Fall + tDelayBlockRise;
+            }
+            ////////////////////////////////////////////////////////
+
+            ////////////////////////////////////////////////////////
+            // consider the fall of the gate (similar)
+            ////////////////////////////////////////////////////////
+            // check two types of constraints on the fall of the fanin:
+            // (1) the constraints related to the rise of the PIs
+            // (2) the constraints related to the fall of the PIs
+            if ( pFanin->tDelaysF[i].Rise >= 0 ) // case (1) 
+            { 
+                if ( pGate->tDelaysF[i].Rise < pFanin->tDelaysF[i].Rise + tDelayBlockFall )
+                    pGate->tDelaysF[i].Rise = pFanin->tDelaysF[i].Rise + tDelayBlockFall;
+            }
+            if ( pFanin->tDelaysF[i].Fall >= 0 ) // case (2) 
+            { 
+                if ( pGate->tDelaysF[i].Fall < pFanin->tDelaysF[i].Fall + tDelayBlockFall )
+                    pGate->tDelaysF[i].Fall = pFanin->tDelaysF[i].Fall + tDelayBlockFall;
+            }
+            ////////////////////////////////////////////////////////
+        }
+    }
+    if ( PinPhase != MIO_PHASE_NONINV )  // INV phase is present
+    {
+        // the rise of the gate is determined by the fall of the fanin
+        // the fall of the gate is determined by the rise of the fanin
+        for ( i = 0; i < pLib->nVarsMax; i++ )
+        {
+            ////////////////////////////////////////////////////////
+            // consider the rise of the gate's output
+            ////////////////////////////////////////////////////////
+            // check two types of constraints on the fall of the fanin:
+            // (1) the constraints related to the rise of the PIs
+            // (2) the constraints related to the fall of the PIs
+            if ( pFanin->tDelaysF[i].Rise >= 0 ) // case (1)
+            { // fanin's rise depends on the rise of i-th PI
+                // update the rise of the gate
+                if ( pGate->tDelaysR[i].Rise < pFanin->tDelaysF[i].Rise + tDelayBlockRise )
+                    pGate->tDelaysR[i].Rise = pFanin->tDelaysF[i].Rise + tDelayBlockRise;
+            }
+            if ( pFanin->tDelaysF[i].Fall >= 0 ) // case (2)
+            { // fanin's rise depends on the fall of i-th PI
+                // update the rise of the gate
+                if ( pGate->tDelaysR[i].Fall < pFanin->tDelaysF[i].Fall + tDelayBlockRise )
+                    pGate->tDelaysR[i].Fall = pFanin->tDelaysF[i].Fall + tDelayBlockRise;
+            }
+            ////////////////////////////////////////////////////////
+
+            ////////////////////////////////////////////////////////
+            // consider the fall of the gate (similar)
+            ////////////////////////////////////////////////////////
+            // check two types of constraints on the rise of the fanin:
+            // (1) the constraints related to the rise of the PIs
+            // (2) the constraints related to the fall of the PIs
+            if ( pFanin->tDelaysR[i].Rise >= 0 ) // case (1) 
+            { 
+                if ( pGate->tDelaysF[i].Rise < pFanin->tDelaysR[i].Rise + tDelayBlockFall )
+                    pGate->tDelaysF[i].Rise = pFanin->tDelaysR[i].Rise + tDelayBlockFall;
+            }
+            if ( pFanin->tDelaysR[i].Fall >= 0 ) // case (2) 
+            { 
+                if ( pGate->tDelaysF[i].Fall < pFanin->tDelaysR[i].Fall + tDelayBlockFall )
+                    pGate->tDelaysF[i].Fall = pFanin->tDelaysR[i].Fall + tDelayBlockFall;
+            }
+            ////////////////////////////////////////////////////////
+        }
+    }
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs phase transformation for one function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+unsigned Map_CalculatePhase( unsigned uTruths[][2], int nVars, unsigned uTruth, unsigned uPhase )
+{
+    int v, Shift;
+    for ( v = 0, Shift = 1; v < nVars; v++, Shift <<= 1 )
+        if ( uPhase & Shift )
+            uTruth = (((uTruth & ~uTruths[v][0]) << Shift) | ((uTruth & uTruths[v][0]) >> Shift));
+    return uTruth;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs phase transformation for one function.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_CalculatePhase6( unsigned uTruths[][2], int nVars, unsigned uTruth[], unsigned uPhase, unsigned uTruthRes[] )
+{
+    unsigned uTemp;
+    int v, Shift;
+
+    // initialize the result
+    uTruthRes[0] = uTruth[0];
+    uTruthRes[1] = uTruth[1];
+    if ( uPhase == 0 )
+        return;
+    // compute the phase 
+    for ( v = 0, Shift = 1; v < nVars; v++, Shift <<= 1 )
+        if ( uPhase & Shift )
+        {
+            if ( Shift < 32 )
+            {
+                uTruthRes[0] = (((uTruthRes[0] & ~uTruths[v][0]) << Shift) | ((uTruthRes[0] & uTruths[v][0]) >> Shift));
+                uTruthRes[1] = (((uTruthRes[1] & ~uTruths[v][1]) << Shift) | ((uTruthRes[1] & uTruths[v][1]) >> Shift));
+            }
+            else
+            {
+                uTemp        = uTruthRes[0];
+                uTruthRes[0] = uTruthRes[1];
+                uTruthRes[1] = uTemp;
+            }
+        }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the supergate library after deriving parameters.]
+
+  Description [This procedure is very useful to see the library after
+  it has been read into the mapper by "read_super" and all the information
+  about the supergates derived.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Map_LibraryPrintTree( Map_SuperLib_t * pLib )
+{
+    Map_Super_t * pGate;
+    int i, k;
+
+    // print all the info related to the supergates
+//    for ( i = pLib->nVarsMax; i < (int)pLib->nLines; i++ )
+    for ( i = pLib->nVarsMax; i < 20; i++ )
+    {
+        pGate = pLib->ppSupers[i];
+
+        // write the gate's fanin info and formula
+        printf( "%6d  ", pGate->Num );
+        printf( "%c ", pGate->fSuper? '*' : ' ' );
+        printf( "%6s", Mio_GateReadName(pGate->pRoot) );
+        for ( k = 0; k < (int)pGate->nFanins; k++ )
+            printf( " %6d", pGate->pFanins[k]->Num );
+        printf( "  %s", pGate->pFormula );
+        printf( "\n" );
+
+        // write the gate's derived info
+        Extra_PrintBinary( stdout, pGate->uTruth, 64 );
+        printf( "  %3d",   pGate->nGates );
+        printf( "  %6.2f", pGate->Area );
+        printf( "  (%4.2f, %4.2f)", pGate->tDelayMax.Rise, pGate->tDelayMax.Fall );
+        printf( "\n" );
+        for ( k = 0; k < pLib->nVarsMax; k++ )
+        {
+            // print the constraint on the rise of the gate in the form (D1, D2), 
+            // where D1 is the constraint related to the rise of the k-th PI
+            // where D2 is the constraint related to the fall of the k-th PI
+            if ( pGate->tDelaysR[k].Rise < 0 && pGate->tDelaysR[k].Fall < 0 )
+                printf( " (----, ----)" );
+            else if ( pGate->tDelaysR[k].Fall < 0 )
+                printf( " (%4.2f, ----)", pGate->tDelaysR[k].Rise );
+            else if ( pGate->tDelaysR[k].Rise < 0 )
+                printf( " (----, %4.2f)", pGate->tDelaysR[k].Fall );
+            else
+                printf( " (%4.2f, %4.2f)", pGate->tDelaysR[k].Rise, pGate->tDelaysR[k].Fall );
+
+            // print the constraint on the fall of the gate in the form (D1, D2), 
+            // where D1 is the constraint related to the rise of the k-th PI
+            // where D2 is the constraint related to the fall of the k-th PI
+            if ( pGate->tDelaysF[k].Rise < 0 && pGate->tDelaysF[k].Fall < 0 )
+                printf( " (----, ----)" );
+            else if ( pGate->tDelaysF[k].Fall < 0 )
+                printf( " (%4.2f, ----)", pGate->tDelaysF[k].Rise );
+            else if ( pGate->tDelaysF[k].Rise < 0 )
+                printf( " (----, %4.2f)", pGate->tDelaysF[k].Fall );
+            else
+                printf( " (%4.2f, %4.2f)", pGate->tDelaysF[k].Rise, pGate->tDelaysF[k].Fall );
+            printf( "\n" );
+        }
+        printf( "\n" );
+    }
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
diff --git a/src/sat/bsat/satSolver.c b/src/sat/bsat/satSolver.c
index 12529ca7..833ea394 100644
--- a/src/sat/bsat/satSolver.c
+++ b/src/sat/bsat/satSolver.c
@@ -226,7 +226,8 @@ static inline void act_var_rescale(sat_solver* s) {
 }
 
 static inline void act_var_bump(sat_solver* s, int v) {
-    s->activity[v] += s->var_inc;
+//    s->activity[v] += s->var_inc;
+    s->activity[v] += (s->pGlobalVars? 3.0 : 1.0) * s->var_inc;
     if (s->activity[v] > 1e100)
         act_var_rescale(s);
     //printf("bump %d %f\n", v-1, activity[v]);
@@ -243,6 +244,15 @@ static inline void act_var_bump_factor(sat_solver* s, int v) {
         order_update(s,v);
 }
 
+static inline void act_var_bump_global(sat_solver* s, int v) {
+    s->activity[v] += (s->var_inc * 3.0 * s->pGlobalVars[v]);
+    if (s->activity[v] > 1e100)
+        act_var_rescale(s);
+    //printf("bump %d %f\n", v-1, activity[v]);
+    if (s->orderpos[v] != -1)
+        order_update(s,v);
+}
+
 static inline void act_var_decay(sat_solver* s) { s->var_inc *= s->var_decay; }
 
 static inline void act_clause_rescale(sat_solver* s) {
@@ -845,6 +855,11 @@ static lbool sat_solver_search(sat_solver* s, sint64 nof_conflicts, sint64 nof_l
         for ( i = 0; i < s->act_vars.size; i++ )
             act_var_bump_factor(s, s->act_vars.ptr[i]);
 
+    // use activity factors in every restart
+    if ( s->pGlobalVars && veci_size(&s->act_vars) > 0 )
+        for ( i = 0; i < s->act_vars.size; i++ )
+            act_var_bump_global(s, s->act_vars.ptr[i]);
+
     for (;;){
         clause* confl = sat_solver_propagate(s);
         if (confl != 0){
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index 86e7a966..00ac60ca 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -180,6 +180,7 @@ struct sat_solver_t
 
     int      fSkipSimplify; // set to one to skip simplification of the clause database
 
+    int *    pGlobalVars;   // for experiments with global vars during interpolation
     // clause store
     void *   pStore;
     int      fSolved;