Major restructuring of the code.

14 files changed, 0 insertions, 2926 deletions

diff --git a/src/aig/int/int.h b/src/aig/int/int.h
deleted file mode 100644
index 4b8d78bb..00000000
--- a/src/aig/int/int.h
+++ /dev/null
@@ -1,94 +0,0 @@
-/**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__
-
-
-/* 
-    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                               ///
-////////////////////////////////////////////////////////////////////////
-
-
-
-ABC_NAMESPACE_HEADER_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                         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  nSecLimit;     // time limit in seconds
-    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  fUseSeparate;  // solve each output separately
-    int  fDropSatOuts;  // replace by 1 the solved outputs
-    int  fDropInvar;    // dump inductive invariant into file
-    int  fVerbose;      // print verbose statistics
-    int  iFrameMax;     // the time frame reached
-};
-
-////////////////////////////////////////////////////////////////////////
-///                      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 * piFrame );
-
-
-
-
-ABC_NAMESPACE_HEADER_END
-
-
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/aig/int/intCheck.c b/src/aig/int/intCheck.c
deleted file mode 100644
index 6b36fe30..00000000
--- a/src/aig/int/intCheck.c
+++ /dev/null
@@ -1,305 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [intCheck.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Interpolation engine.]
-
-  Synopsis    [Procedures to perform incremental inductive check.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 24, 2008.]
-
-  Revision    [$Id: intCheck.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "intInt.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-// checking manager
-struct Inter_Check_t_
-{
-    int           nFramesK;     // the number of timeframes (K=1 for simple induction)
-    int           nVars;        // the current number of variables in the solver
-    Aig_Man_t *   pFrames;      // unrolled timeframes
-    Cnf_Dat_t *   pCnf;         // CNF of unrolled timeframes 
-    sat_solver *  pSat;         // SAT solver 
-    Vec_Int_t *   vOrLits;      // OR vars in each time frame (total number is the number nFrames)
-    Vec_Int_t *   vAndLits;     // AND vars in the last timeframe (total number is the number of interpolants)
-    Vec_Int_t *   vAssLits;     // assumptions (the union of the two)
-};
-
-////////////////////////////////////////////////////////////////////////
-///                     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 * Inter_ManUnrollFrames( Aig_Man_t * pAig, int nFrames )
-{
-    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
-    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) );
-        // 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;
-            Aig_ObjCreatePo( pFrames, (Aig_Obj_t *)pObjLo->pData );
-        }
-    }
-    Aig_ManCleanup( pFrames );
-    return pFrames;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [This procedure sets default values of interpolation parameters.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK )
-{
-    Inter_Check_t * p;
-    // create solver
-    p = ABC_CALLOC( Inter_Check_t, 1 );
-    p->vOrLits  = Vec_IntAlloc( 100 );
-    p->vAndLits = Vec_IntAlloc( 100 );
-    p->vAssLits = Vec_IntAlloc( 100 );
-    // generate the timeframes 
-    p->pFrames = Inter_ManUnrollFrames( pTrans, nFramesK );
-    assert( Aig_ManPiNum(p->pFrames) == nFramesK * Saig_ManPiNum(pTrans) + Saig_ManRegNum(pTrans) );
-    assert( Aig_ManPoNum(p->pFrames) == nFramesK * Saig_ManRegNum(pTrans) );
-    // convert to CNF
-    p->pCnf = Cnf_Derive( p->pFrames, Aig_ManPoNum(p->pFrames) ); 
-    p->pSat = (sat_solver *)Cnf_DataWriteIntoSolver( p->pCnf, 1, 0 );
-    // assign parameters
-    p->nFramesK = nFramesK;
-    p->nVars    = p->pCnf->nVars;
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [This procedure sets default values of interpolation parameters.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Inter_CheckStop( Inter_Check_t * p )
-{
-    if ( p == NULL )
-        return;
-    Vec_IntFree( p->vOrLits );
-    Vec_IntFree( p->vAndLits );
-    Vec_IntFree( p->vAssLits );
-    Cnf_DataFree( p->pCnf );
-    Aig_ManStop( p->pFrames );
-    sat_solver_delete( p->pSat );
-    ABC_FREE( p );
-}
-
-
-/**Function*************************************************************
-
-  Synopsis    [Creates one OR-gate: A + B = C.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Inter_CheckAddOrGate( Inter_Check_t * p, int iVarA, int iVarB, int iVarC )
-{
-    int RetValue, pLits[3];
-    // add A => C   or   !A + C
-    pLits[0] = toLitCond(iVarA, 1);
-    pLits[1] = toLitCond(iVarC, 0);
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
-    assert( RetValue );
-    // add B => C   or   !B + C
-    pLits[0] = toLitCond(iVarB, 1);
-    pLits[1] = toLitCond(iVarC, 0);
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
-    assert( RetValue );
-    // add !A & !B => !C  or A + B + !C
-    pLits[0] = toLitCond(iVarA, 0);
-    pLits[1] = toLitCond(iVarB, 0);
-    pLits[2] = toLitCond(iVarC, 1);
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 3 );
-    assert( RetValue );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Creates equality: A = B.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Inter_CheckAddEqual( Inter_Check_t * p, int iVarA, int iVarB )
-{
-    int RetValue, pLits[3];
-    // add A => B   or   !A + B
-    pLits[0] = toLitCond(iVarA, 1);
-    pLits[1] = toLitCond(iVarB, 0);
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
-    assert( RetValue );
-    // add B => A   or   !B + A
-    pLits[0] = toLitCond(iVarB, 1);
-    pLits[1] = toLitCond(iVarA, 0);
-    RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
-    assert( RetValue );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Perform the checking.]
-
-  Description [Returns 1 if the check has passed.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnfInt, int nTimeNewOut )
-{
-    Aig_Obj_t * pObj, * pObj2;
-    int i, f, VarA, VarB, RetValue, Entry, status;
-    int nRegs = Aig_ManPiNum(pCnfInt->pMan);
-    assert( Aig_ManPoNum(p->pCnf->pMan) == p->nFramesK * nRegs );
-    assert( Aig_ManPoNum(pCnfInt->pMan) == 1 );
-
-    // set runtime limit
-    if ( nTimeNewOut )
-        sat_solver_set_runtime_limit( p->pSat, nTimeNewOut );
-
-    // add clauses to the SAT solver
-    Cnf_DataLift( pCnfInt, p->nVars );
-    for ( f = 0; f <= p->nFramesK; f++ )
-    {
-        // add clauses to the solver
-        for ( i = 0; i < pCnfInt->nClauses; i++ )
-        {
-            RetValue = sat_solver_addclause( p->pSat, pCnfInt->pClauses[i], pCnfInt->pClauses[i+1] );
-            assert( RetValue );
-        }
-        // add equality clauses for the flop variables
-        Aig_ManForEachPi( pCnfInt->pMan, pObj, i )
-        {
-            pObj2 = f ? Aig_ManPo(p->pFrames, i + (f-1) * nRegs) : Aig_ManPi(p->pFrames, i);
-            Inter_CheckAddEqual( p, pCnfInt->pVarNums[pObj->Id], p->pCnf->pVarNums[pObj2->Id] );
-        }
-        // add final clauses
-        if ( f < p->nFramesK )
-        {
-            if ( f == Vec_IntSize(p->vOrLits) ) // find time here
-            {
-                // add literal to this frame
-                VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ];
-                Vec_IntPush( p->vOrLits, VarB );
-            }
-            else
-            {
-                // add OR gate for this frame
-                VarA = Vec_IntEntry( p->vOrLits, f );
-                VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ];
-                Inter_CheckAddOrGate( p, VarA, VarB, p->nVars + pCnfInt->nVars );
-                Vec_IntWriteEntry( p->vOrLits, f, p->nVars + pCnfInt->nVars ); // using var ID!
-            }
-        }
-        else
-        {
-            // add AND gate for this frame
-            VarB = pCnfInt->pVarNums[ Aig_ManPo(pCnfInt->pMan, 0)->Id ];
-            Vec_IntPush( p->vAndLits, VarB );
-        }
-        // update variable IDs
-        Cnf_DataLift( pCnfInt, pCnfInt->nVars + 1 );
-        p->nVars += pCnfInt->nVars + 1;
-    }
-    Cnf_DataLift( pCnfInt, -p->nVars );
-    assert( Vec_IntSize(p->vOrLits) == p->nFramesK );
-
-    // collect the assumption literals
-    Vec_IntClear( p->vAssLits );
-    Vec_IntForEachEntry( p->vOrLits, Entry, i )
-        Vec_IntPush( p->vAssLits, toLitCond(Entry, 0) );
-    Vec_IntForEachEntry( p->vAndLits, Entry, i )
-        Vec_IntPush( p->vAssLits, toLitCond(Entry, 1) );
-/*
-    if ( pCnfInt->nLiterals == 3635 )
-    {
-        int s = 0;
-    }
-*/
-    // call the SAT solver
-    status = sat_solver_solve( p->pSat, Vec_IntArray(p->vAssLits), 
-        Vec_IntArray(p->vAssLits) + Vec_IntSize(p->vAssLits), 
-        (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-
-    return status == l_False;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/int/intContain.c b/src/aig/int/intContain.c
deleted file mode 100644
index 77b057a7..00000000
--- a/src/aig/int/intContain.c
+++ /dev/null
@@ -1,341 +0,0 @@
-/**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"
-
-ABC_NAMESPACE_IMPL_START
-
-////////////////////////////////////////////////////////////////////////
-///                        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, 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, 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 )
-    { 
-        // forward inductive check: 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 );
-    }
-    else
-    {
-        // backward inductive check: 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 );
-    }
-    Vec_PtrFree( vMapRegs );
-    Aig_ManCleanup( pFrames );
-
-    // convert to CNF
-    pCnf = Cnf_Derive( pFrames, 0 ); 
-    pSat = (sat_solver *)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, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-
-//    Inter_ManCheckUniqueness( pTrans, pSat, pCnf, nSteps );
-
-    Cnf_DataFree( pCnf );
-    Aig_ManStop( pFrames );
-
-    sat_solver_delete( pSat );
-    return status == l_False;
-}
-ABC_NAMESPACE_IMPL_END
-
-#include "fra.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-/**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 )
-    
-    // possible consequences here!!!
-    assert( 0 );
-
-    if ( sat_solver_nvars(pSat) == 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 );
-    ABC_FREE( pCounterEx );
-    return 1;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/int/intCore.c b/src/aig/int/intCore.c
deleted file mode 100644
index 3bd111be..00000000
--- a/src/aig/int/intCore.c
+++ /dev/null
@@ -1,389 +0,0 @@
-/**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"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        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->nSecLimit    = 0;     // time limit in seconds
-    p->nFramesK     = 1;     // the number of timeframes to use in induction
-    p->fRewrite     = 0;     // use additional rewriting to simplify timeframes
-    p->fTransLoop   = 0;     // 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->fUseSeparate = 0;     // solve each output separately
-    p->fDropSatOuts = 0;     // replace by 1 the solved outputs
-    p->fVerbose     = 0;     // print verbose statistics
-    p->iFrameMax    =-1;
-}
-
-/**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 * piFrame )
-{
-    extern int Inter_ManCheckInductiveContainment( Aig_Man_t * pTrans, Aig_Man_t * pInter, int nSteps, int fBackward );
-    Inter_Man_t * p;
-    Inter_Check_t * pCheck = NULL;
-    Aig_Man_t * pAigTemp;
-    int s, i, RetValue, Status, clk, clk2, clkTotal = clock(), timeTemp;
-    int nTimeNewOut = pPars->nSecLimit ? time(NULL) + pPars->nSecLimit : 0;
-
-    // sanity checks
-    assert( Saig_ManRegNum(pAig) > 0 );
-    assert( Saig_ManPiNum(pAig) > 0 );
-    assert( Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) == 1 );
-    if ( pPars->fVerbose && Saig_ManConstrNum(pAig) )
-        printf( "Performing interpolation with %d constraints...\n", Saig_ManConstrNum(pAig) );
-
-    if ( Inter_ManCheckInitialState(pAig) )
-    {
-        *piFrame = 0;
-        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
-    *piFrame = -1;
-    p->nFrames = 1;
-    for ( s = 0; ; s++ )
-    {
-        Cnf_Dat_t * pCnfInter2;
-
-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->pCnfFrames = Cnf_DeriveSimple( 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) );
-            ABC_PRT( "Time", clock() - clk2 );
-        }
-
-
-        //////////////////////////////////////////
-        // start containment checking
-        if ( !(pPars->fTransLoop || pPars->fUseBackward) )
-        {
-            pCheck = Inter_CheckStart( p->pAigTrans, pPars->nFramesK );
-            // try new containment check for the initial state
-clk = clock();
-            pCnfInter2 = Cnf_Derive( p->pInter, 1 );  
-p->timeCnf += clock() - clk;    
-            RetValue = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut );
-//            assert( RetValue == 0 );
-            Cnf_DataFree( pCnfInter2 );
-            if ( p->vInters )
-                Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInter) );
-        }
-        //////////////////////////////////////////
-
-        // 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, 0 );
-                Inter_CheckStop( pCheck );
-                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, nTimeNewOut );
-
-            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 );
-                ABC_PRT( "Time", clock() - clk );
-            }
-            // remember the number of timeframes completed
-            pPars->iFrameMax = i + 1 + p->nFrames;
-            if ( RetValue == 0 ) // found a (spurious?) counter-example
-            {
-                if ( i == 0 ) // real counterexample
-                {
-                    if ( pPars->fVerbose )
-                        printf( "Found a real counterexample in frame %d.\n", p->nFrames );
-                    p->timeTotal = clock() - clkTotal;
-                    *piFrame = p->nFrames;
-//                    pAig->pSeqModel = (Abc_Cex_t *)Inter_ManGetCounterExample( pAig, p->nFrames+1, pPars->fVerbose );
-                    {
-                        int RetValue;
-                        Saig_ParBmc_t ParsBmc, * pParsBmc = &ParsBmc;
-                        Saig_ParBmcSetDefaultParams( pParsBmc );
-                        pParsBmc->nConfLimit = 100000000;
-                        pParsBmc->nStart     = p->nFrames;
-                        pParsBmc->fVerbose   = pPars->fVerbose;
-                        RetValue = Saig_ManBmcScalable( pAig, pParsBmc );
-                        if ( RetValue == 1 )
-                            printf( "Error: The problem should be SAT but it is UNSAT.\n" );
-                        else if ( RetValue == -1 )
-                            printf( "Error: The problem timed out.\n" );
-                    }
-                    Inter_ManStop( p, 0 );
-                    Inter_CheckStop( pCheck );
-                    return 0;
-                }
-                // likely spurious counter-example
-                p->nFrames += i;
-                Inter_ManClean( p ); 
-                break;
-            }
-            else if ( RetValue == -1 ) 
-            {
-                if ( pPars->nSecLimit && time(NULL) > nTimeNewOut ) // timed out
-                {
-                    if ( pPars->fVerbose )
-                        printf( "Reached timeout (%d seconds).\n",  pPars->nSecLimit );
-                }
-                else
-                {
-                    assert( p->nConfCur >= p->nConfLimit );
-                    if ( pPars->fVerbose )
-                        printf( "Reached limit (%d) on the number of conflicts.\n", p->nConfLimit );
-                }
-                p->timeTotal = clock() - clkTotal;
-                Inter_ManStop( p, 0 );
-                Inter_CheckStop( pCheck );
-                return -1;
-            }
-            assert( RetValue == 1 ); // found new interpolant
-            // compress the interpolant
-clk = clock();
-            if ( p->pInterNew )
-            {
-//                Ioa_WriteAiger( p->pInterNew, "interpol.aig", 0, 0 );
-                p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 1, 0 );
-//                p->pInterNew = Dar_ManRwsat( pAigTemp = p->pInterNew, 0, 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, 1 );
-                Inter_CheckStop( pCheck );
-                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) )
-                {
-                    if ( pPars->fTransLoop || pPars->fUseBackward )
-                        Status = Inter_ManCheckInductiveContainment( p->pAigTrans, p->pInterNew, pPars->nFramesK, pPars->fUseBackward );
-                    else
-                    {   // new containment check
-clk2 = clock();
-                        pCnfInter2 = Cnf_Derive( p->pInterNew, 1 );  
-p->timeCnf += clock() - clk2;
-timeTemp = clock() - clk2;
-            
-                        Status = Inter_CheckPerform( pCheck, pCnfInter2, nTimeNewOut );
-                        Cnf_DataFree( pCnfInter2 );
-                        if ( p->vInters )
-                            Vec_PtrPush( p->vInters, Aig_ManDupSimple(p->pInterNew) );
-                    }
-                }
-                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 - timeTemp;
-            if ( Status ) // contained
-            {
-                if ( pPars->fVerbose )
-                    printf( "Proved containment of interpolants.\n" );
-                p->timeTotal = clock() - clkTotal;
-                Inter_ManStop( p, 1 );
-                Inter_CheckStop( pCheck );
-                return 1;
-            }
-            if ( pPars->nSecLimit && time(NULL) > nTimeNewOut )
-            {
-                printf( "Reached timeout (%d seconds).\n",  pPars->nSecLimit );
-                p->timeTotal = clock() - clkTotal;
-                Inter_ManStop( p, 1 );
-                Inter_CheckStop( pCheck );
-                return -1;
-            }
-            // save interpolant and convert it into CNF
-            if ( pPars->fTransLoop )
-            {
-                Aig_ManStop( p->pInter );
-                p->pInter = p->pInterNew; 
-            }
-            else
-            {
-                if ( pPars->fUseBackward )
-                {
-                    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;
-                }
-                else // forward with the new containment checking (using only the frontier)
-                {
-                    Aig_ManStop( p->pInter );
-                    p->pInter = p->pInterNew; 
-                }
-            }
-            p->pInterNew = NULL;
-            Cnf_DataFree( p->pCnfInter );
-clk = clock();
-            p->pCnfInter = Cnf_Derive( p->pInter, 0 );  
-p->timeCnf += clock() - clk;
-        }
-
-        // start containment checking
-        Inter_CheckStop( pCheck );
-    }
-    assert( 0 );
-    return RetValue;
-}
-
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/int/intCtrex.c b/src/aig/int/intCtrex.c
deleted file mode 100644
index 0aa60040..00000000
--- a/src/aig/int/intCtrex.c
+++ /dev/null
@@ -1,167 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [intCtrex.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [Interpolation engine.]
-
-  Synopsis    [Counter-example generation after disproving the property.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 24, 2008.]
-
-  Revision    [$Id: intCtrex.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "intInt.h"
-#include "ssw.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Unroll the circuit the given number of timeframes.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Aig_Man_t * Inter_ManFramesBmc( 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_ManConst0( 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;
-        // transfer to register outputs
-        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
-            pObjLi->pData = Aig_ObjChild0Copy(pObjLi);
-        // transfer to register outputs
-        Saig_ManForEachLiLo(  pAig, pObjLi, pObjLo, i )
-            pObjLo->pData = pObjLi->pData;
-    }
-    // create POs for the output of the last frame
-    pObj = Aig_ManPo( pAig, 0 );
-    Aig_ObjCreatePo( pFrames, Aig_ObjChild0Copy(pObj) );
-    Aig_ManCleanup( pFrames );
-    return pFrames;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Run the SAT solver on the unrolled instance.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void * Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose )
-{
-    int nConfLimit = 1000000;
-    Abc_Cex_t * pCtrex = NULL;
-    Aig_Man_t * pFrames;
-    sat_solver * pSat;
-    Cnf_Dat_t * pCnf;
-    int status, clk = clock();
-    Vec_Int_t * vCiIds;
-    // create timeframes
-    assert( Saig_ManPoNum(pAig) == 1 );
-    pFrames = Inter_ManFramesBmc( pAig, nFrames );
-    // derive CNF
-    pCnf = Cnf_Derive( pFrames, 0 );
-    Cnf_DataTranformPolarity( pCnf, 0 );
-    vCiIds = Cnf_DataCollectPiSatNums( pCnf, pFrames );
-    Aig_ManStop( pFrames );
-    // convert into SAT solver
-    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
-    Cnf_DataFree( pCnf );
-    if ( pSat == NULL )
-    {
-        printf( "Counter-example generation in command \"int\" has failed.\n" );
-        printf( "Use command \"bmc2\" to produce a valid counter-example.\n" );
-        Vec_IntFree( vCiIds );
-        return NULL;
-    }
-    // simplify the problem
-    status = sat_solver_simplify(pSat);
-    if ( status == 0 )
-    {
-        Vec_IntFree( vCiIds );
-        sat_solver_delete( pSat );
-        return NULL;
-    }
-    // solve the miter
-    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-    // if the problem is SAT, get the counterexample
-    if ( status == l_True )
-    {
-        int i, * pModel = Sat_SolverGetModel( pSat, vCiIds->pArray, vCiIds->nSize );
-        pCtrex = Abc_CexAlloc( Saig_ManRegNum(pAig), Saig_ManPiNum(pAig), nFrames );
-        pCtrex->iFrame = nFrames - 1;
-        pCtrex->iPo = 0;
-        for ( i = 0; i < Vec_IntSize(vCiIds); i++ )
-            if ( pModel[i] )
-                Aig_InfoSetBit( pCtrex->pData, Saig_ManRegNum(pAig) + i );
-        ABC_FREE( pModel );
-    }
-    // free the sat_solver
-    sat_solver_delete( pSat );
-    Vec_IntFree( vCiIds );
-    // verify counter-example
-    status = Saig_ManVerifyCex( pAig, pCtrex );
-    if ( status == 0 )
-        printf( "Inter_ManGetCounterExample(): Counter-example verification has FAILED.\n" );
-    // report the results
-    if ( fVerbose )
-    {
-        ABC_PRT( "Total ctrex generation time", clock() - clk );
-    }
-    return pCtrex;
-
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/int/intDup.c b/src/aig/int/intDup.c
deleted file mode 100644
index 800375a9..00000000
--- a/src/aig/int/intDup.c
+++ /dev/null
@@ -1,184 +0,0 @@
-/**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"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        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 = ABC_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 );
-    ABC_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->nTruePis = p->nTruePis;
-    pNew->nTruePos = Saig_ManConstrNum(p);
-    pNew->nRegs    = p->nRegs;
-    // duplicate internal nodes
-    Aig_ManForEachNode( p, pObj, i )
-        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-
-    // create constraint outputs
-    Saig_ManForEachPo( p, pObj, i )
-    {
-        if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
-            continue;
-        Aig_ObjCreatePo( pNew, Aig_Not( Aig_ObjChild0Copy(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 + Saig_ManConstrNum(p);
-    // duplicate internal nodes
-    Aig_ManForEachNode( p, pObj, i )
-        pObj->pData = Aig_And( pNew, Aig_ObjChild0Copy(pObj), Aig_ObjChild1Copy(pObj) );
-
-    // create constraint outputs
-    Saig_ManForEachPo( p, pObj, i )
-    {
-        if ( i < Saig_ManPoNum(p)-Saig_ManConstrNum(p) )
-            continue;
-        Aig_ObjCreatePo( pNew, Aig_Not( Aig_ObjChild0Copy(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, (Aig_Obj_t *)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                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/int/intFrames.c b/src/aig/int/intFrames.c
deleted file mode 100644
index 0fbab6cb..00000000
--- a/src/aig/int/intFrames.c
+++ /dev/null
@@ -1,115 +0,0 @@
-/**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"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        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)-Saig_ManConstrNum(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) );
-        // add outputs for constraints
-        Saig_ManForEachPo( pAig, pObj, i )
-        {
-            if ( i < Saig_ManPoNum(pAig)-Saig_ManConstrNum(pAig) )
-                continue;
-            Aig_ObjCreatePo( pFrames, Aig_Not( Aig_ObjChild0Copy(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                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/int/intInt.h b/src/aig/int/intInt.h
deleted file mode 100644
index 66ff9578..00000000
--- a/src/aig/int/intInt.h
+++ /dev/null
@@ -1,142 +0,0 @@
-/**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__
-
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-#include "saig.h"
-#include "cnf.h"
-#include "satSolver.h"
-#include "satStore.h"
-#include "int.h"
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-
-
-ABC_NAMESPACE_HEADER_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-// interpolation 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;
-};
-
-// containment checking manager
-typedef struct Inter_Check_t_ Inter_Check_t;
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                    FUNCTION DECLARATIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== intCheck.c ============================================================*/
-extern Inter_Check_t * Inter_CheckStart( Aig_Man_t * pTrans, int nFramesK );
-extern void            Inter_CheckStop( Inter_Check_t * p );
-extern int             Inter_CheckPerform( Inter_Check_t * p, Cnf_Dat_t * pCnf, int nTimeNewOut );
-
-/*=== 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 );
-
-/*=== intCtrex.c ============================================================*/
-extern void *          Inter_ManGetCounterExample( Aig_Man_t * pAig, int nFrames, int fVerbose );
-
-/*=== 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, int fProved );
-
-/*=== intM114.c ============================================================*/
-extern int             Inter_ManPerformOneStep( Inter_Man_t * p, int fUseBias, int fUseBackward, int nTimeNewOut );
-
-/*=== 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 );
-
-
-
-ABC_NAMESPACE_HEADER_END
-
-
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/aig/int/intInter.c b/src/aig/int/intInter.c
deleted file mode 100644
index ef32294b..00000000
--- a/src/aig/int/intInter.c
+++ /dev/null
@@ -1,145 +0,0 @@
-/**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"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        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                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/int/intM114.c b/src/aig/int/intM114.c
deleted file mode 100644
index 139c9bbd..00000000
--- a/src/aig/int/intM114.c
+++ /dev/null
@@ -1,320 +0,0 @@
-/**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"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        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, int nTimeNewOut )
-{
-    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;
-    }
-
-    // set runtime limit
-    if ( nTimeNewOut )
-        sat_solver_set_runtime_limit( pSat, nTimeNewOut );
-
-    // collect global variables
-    pGlobalVars = ABC_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, (ABC_INT64_T)p->nConfLimit, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-    p->nConfCur = pSat->stats.conflicts;
-p->timeSat += clock() - clk;
-
-    pSat->pGlobalVars = NULL;
-    ABC_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 = (Aig_Man_t *)Inta_ManInterpolate( pManInterA, (Sto_Man_t *)pSatCnf, p->vVarsAB, 0 );
-    Inta_ManFree( pManInterA );
-
-p->timeInt += clock() - clk;
-    Sto_ManFree( (Sto_Man_t *)pSatCnf );
-    return RetValue;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/int/intM114p.c b/src/aig/int/intM114p.c
deleted file mode 100644
index 0ad0552f..00000000
--- a/src/aig/int/intM114p.c
+++ /dev/null
@@ -1,442 +0,0 @@
-/**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 $]
-
-***********************************************************************/
-
-#include "intInt.h"
-#include "m114p.h"
-
-#ifdef ABC_USE_LIBRARIES
-
-ABC_NAMESPACE_IMPL_START
-
-////////////////////////////////////////////////////////////////////////
-///                        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;
-    int nClauses;
-
-    nClauses = M114p_SolverProofClauseNum(s);
-
-    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                                ///
-////////////////////////////////////////////////////////////////////////
-
-ABC_NAMESPACE_IMPL_END
-
-#endif
-
-
diff --git a/src/aig/int/intMan.c b/src/aig/int/intMan.c
deleted file mode 100644
index d6219f6b..00000000
--- a/src/aig/int/intMan.c
+++ /dev/null
@@ -1,163 +0,0 @@
-/**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"
-#include "ioa.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Creates 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 = ABC_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;
-    if ( pPars->fDropInvar )
-        p->vInters = Vec_PtrAlloc( 100 );
-    return p;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Cleans the interpolation manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Inter_ManClean( Inter_Man_t * p )
-{
-    if ( p->vInters )
-    {
-        Aig_Man_t * pMan;
-        int i;
-        Vec_PtrForEachEntry( Aig_Man_t *, p->vInters, pMan, i )
-            Aig_ManStop( pMan );
-        Vec_PtrClear( p->vInters );
-    }
-    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    [Writes interpolant into a file.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Inter_ManInterDump( Inter_Man_t * p, int fProved )
-{
-    Aig_Man_t * pMan;
-    pMan = Aig_ManDupArray( p->vInters );
-    Ioa_WriteAiger( pMan, "invar.aig", 0, 0 );
-    Aig_ManStop( pMan );
-    if ( fProved )
-        printf( "Inductive invariant is dumped into file \"invar.aig\".\n" );
-    else
-        printf( "Interpolants are dumped into file \"inter.aig\".\n" );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Frees the interpolation manager.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Inter_ManStop( Inter_Man_t * p, int fProved )
-{
-    if ( p->fVerbose )
-    {
-        p->timeOther = p->timeTotal-p->timeRwr-p->timeCnf-p->timeSat-p->timeInt-p->timeEqu;
-        printf( "Runtime statistics:\n" );
-        ABC_PRTP( "Rewriting  ", p->timeRwr,   p->timeTotal );
-        ABC_PRTP( "CNF mapping", p->timeCnf,   p->timeTotal );
-        ABC_PRTP( "SAT solving", p->timeSat,   p->timeTotal );
-        ABC_PRTP( "Interpol   ", p->timeInt,   p->timeTotal );
-        ABC_PRTP( "Containment", p->timeEqu,   p->timeTotal );
-        ABC_PRTP( "Other      ", p->timeOther, p->timeTotal );
-        ABC_PRTP( "TOTAL      ", p->timeTotal, p->timeTotal );
-    }
-
-    if ( p->vInters )
-        Inter_ManInterDump( p, fProved );
-
-    if ( p->pCnfAig )
-        Cnf_DataFree( p->pCnfAig );
-    if ( p->pAigTrans )
-        Aig_ManStop( p->pAigTrans );
-    if ( p->pInterNew )
-        Aig_ManStop( p->pInterNew );
-    Inter_ManClean( p );
-    Vec_PtrFreeP( &p->vInters );
-    Vec_IntFreeP( &p->vVarsAB );
-    ABC_FREE( p );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/int/intUtil.c b/src/aig/int/intUtil.c
deleted file mode 100644
index ce48c37d..00000000
--- a/src/aig/int/intUtil.c
+++ /dev/null
@@ -1,108 +0,0 @@
-/**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"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        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;
-    Aig_Obj_t * pObj;
-    sat_solver * pSat;
-    int i, status;
-    int clk = clock();
-    pCnf = Cnf_Derive( p, Saig_ManRegNum(p) ); 
-    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 1 );
-    if ( pSat == NULL )
-    {
-        Cnf_DataFree( pCnf );
-        return 0;
-    }
-    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-    ABC_PRT( "Time", clock() - clk );
-    if ( status == l_True )
-    {
-        p->pSeqModel = Abc_CexAlloc( Aig_ManRegNum(p), Saig_ManPiNum(p), 1 );
-        Saig_ManForEachPi( p, pObj, i )
-            if ( sat_solver_var_value( pSat, pCnf->pVarNums[Aig_ObjId(pObj)] ) )
-                Aig_InfoSetBit( p->pSeqModel->pData, Aig_ManRegNum(p) + i );
-    }
-    Cnf_DataFree( pCnf );
-    sat_solver_delete( pSat );
-    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 = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
-    Cnf_DataFree( pCnf );
-    if ( pSat == NULL )
-        return 1;
-    status = sat_solver_solve( pSat, NULL, NULL, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0, (ABC_INT64_T)0 );
-    sat_solver_delete( pSat );
-    ABC_PRT( "Time", clock() - clk );
-    return status == l_False;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/int/module.make b/src/aig/int/module.make
deleted file mode 100644
index 8e0e4319..00000000
--- a/src/aig/int/module.make
+++ /dev/null
@@ -1,11 +0,0 @@
-SRC +=    src/aig/int/intCheck.c \
-    src/aig/int/intContain.c \
-    src/aig/int/intCore.c \
-    src/aig/int/intCtrex.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