Initial new interpolation code.

7 files changed, 1254 insertions, 0 deletions

diff --git a/src/proof/int2/int2.h b/src/proof/int2/int2.h
new file mode 100644
index 00000000..b85006b7
--- /dev/null
+++ b/src/proof/int2/int2.h
@@ -0,0 +1,90 @@
+/**CFile****************************************************************
+
+  FileName    [int2.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 - Dec 1, 2013.]
+
+  Revision    [$Id: int2.h,v 1.00 2013/12/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__aig__int2__int_h
+#define ABC__aig__int2__int_h
+
+
+/* 
+    The interpolation algorithm implemented here was introduced in the papers:
+    K. L. McMillan. Interpolation and SAT-based model checking. CAV’03, pp. 1-13.
+    C.-Y. Wu et al. A CEX-Guided Interpolant Generation Algorithm for 
+    SAT-based Model Checking. DAC'13.
+*/
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+
+
+ABC_NAMESPACE_HEADER_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// simulation manager
+typedef struct Int2_ManPars_t_ Int2_ManPars_t;
+struct Int2_ManPars_t_
+{
+    int     nBTLimit;       // limit on the number of conflicts
+    int     nFramesS;       // the starting number timeframes
+    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     fDropInvar;     // dump inductive invariant into file
+    int     fVerbose;       // print verbose statistics
+    int     iFrameMax;      // the time frame reached
+    char *  pFileName;      // file name to dump interpolant
+};
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== intCore.c ==========================================================*/
+extern void       Int2_ManSetDefaultParams( Int2_ManPars_t * p );
+extern int        Int2_ManPerformInterpolation( Gia_Man_t * p, Int2_ManPars_t * pPars );
+
+
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/proof/int2/int2Bmc.c b/src/proof/int2/int2Bmc.c
new file mode 100644
index 00000000..cd7f1a74
--- /dev/null
+++ b/src/proof/int2/int2Bmc.c
@@ -0,0 +1,355 @@
+/**CFile****************************************************************
+
+  FileName    [int2Bmc.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Interpolation engine.]
+
+  Synopsis    [BMC used inside IMC.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - Dec 1, 2013.]
+
+  Revision    [$Id: int2Bmc.c,v 1.00 2013/12/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "int2Int.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+
+/**Function*************************************************************
+
+  Synopsis    [Trasnforms AIG to transition into the init state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Int2_ManDupInit( Gia_Man_t * p, int fVerbose )
+{
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj, * pObjRi, * pObjRo;
+    int i, iCtrl;
+    assert( Gia_ManRegNum(p) > 0 );
+    pNew = Gia_ManStart( 10000 );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+    {
+        if ( i == Gia_ManPiNum(p) )
+            iCtrl = Gia_ManAppendCi( pNew );
+        pObj->Value = Gia_ManAppendCi( pNew );
+    }
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachAnd( p, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Gia_ManForEachPo( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pNew, Gia_ObjFanin0Copy(pObj) );
+    Gia_ManForEachRiRo( p, pObjRi, pObjRo, i )
+        Gia_ManAppendCo( pNew, Gia_ManHashMux( pNew, iCtrl, pObjRo->Value, Gia_ObjFanin0Copy(pObjRi) ) );
+    Gia_ManHashStop( pNew );
+    Gia_ManSetRegNum( pNew, Gia_ManRegNum(p) );
+    // remove dangling
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    if ( fVerbose )
+        printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n", 
+            Gia_ManAndNum(pTemp), Gia_ManAndNum(pNew) );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if AIG has transition into init state.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Int2_ManCheckInit( Gia_Man_t * p )
+{
+    sat_solver * pSat;
+    Cnf_Dat_t * pCnf;
+    Gia_Man_t * pNew;
+    Gia_Obj_t * pObj;
+    Vec_Int_t * vLits;
+    int i, Lit, RetValue = 0;
+    assert( Gia_ManRegNum(p) > 0 );
+    pNew = Jf_ManDeriveCnf( p, 0 );  
+    pCnf = (Cnf_Dat_t *)pNew->pData; pNew->pData = NULL;
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    if ( pSat != NULL )
+    {
+        vLits = Vec_IntAlloc( Gia_ManRegNum(p) );
+        Gia_ManForEachRi( pNew, pObj, i )
+        {
+            Lit = pCnf->pVarNums[ Gia_ObjId(pNew, Gia_ObjFanin0(pObj)) ];
+            Lit = Abc_Var2Lit( Lit, Gia_ObjFaninC0(pObj) );
+            Vec_IntPush( vLits, Abc_LitNot(Lit) );
+        }
+        if ( sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits), 0, 0, 0, 0 ) == l_True )
+            RetValue = 1;
+        Vec_IntFree( vLits );
+        sat_solver_delete( pSat );
+    }
+    Cnf_DataFree( pCnf );
+    Gia_ManStop( pNew );
+    return RetValue;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates the BMC instance in the SAT solver.]
+
+  Description [The PIs are mapped in the natural order. The flop inputs
+  are the last Gia_ManRegNum(p) variables of resulting SAT solver.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Int2_ManFrameInit( Gia_Man_t * p, int nFrames, int fVerbose )
+{
+    Gia_Man_t * pFrames, * pTemp;
+    Gia_Obj_t * pObj;
+    int i, f;
+    pFrames = Gia_ManStart( 10000 );
+    pFrames->pName = Abc_UtilStrsav( p->pName );
+    pFrames->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    // perform structural hashing
+    Gia_ManHashAlloc( pFrames );
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Gia_ManForEachPi( p, pObj, i )
+            pObj->Value = Gia_ManAppendCi( pFrames );
+        Gia_ManForEachRo( p, pObj, i )
+            pObj->Value = f ? Gia_ObjRoToRi(p, pObj)->Value : 0;
+        Gia_ManForEachAnd( p, pObj, i )
+            pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        Gia_ManForEachRi( p, pObj, i )
+            pObj->Value = Gia_ObjFanin0Copy(pObj);
+    }
+    Gia_ManHashStop( pFrames );
+    // create flop inputs
+    Gia_ManForEachRi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCo( pFrames, Gia_ObjFanin0Copy(pObj) );
+    // remove dangling
+    pFrames = Gia_ManCleanup( pTemp = pFrames );
+    if ( fVerbose )
+        printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n", 
+            Gia_ManAndNum(pTemp), Gia_ManAndNum(pFrames) );
+    Gia_ManStop( pTemp );
+    return pFrames;
+}
+sat_solver * Int2_ManSetupBmcSolver( Gia_Man_t * p, int nFrames )
+{
+    Gia_Man_t * pFrames, * pTemp;
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    // unfold for the given number of timeframes
+    pFrames = Int2_ManFrameInit( p, nFrames, 1 );
+    assert( Gia_ManRegNum(pFrames) == 0 );
+    // derive CNF for the timeframes
+    pFrames = Jf_ManDeriveCnf( pTemp = pFrames, 0 );  Gia_ManStop( pTemp );
+    pCnf = (Cnf_Dat_t *)pFrames->pData; pFrames->pData = NULL;
+    // create SAT solver
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    if ( pSat != NULL )
+    {
+        Gia_Obj_t * pObj;
+        int i, nVars = sat_solver_nvars( pSat );
+        sat_solver_setnvars( pSat, nVars + Gia_ManPoNum(pFrames) );
+        // add clauses for the POs
+        Gia_ManForEachCo( pFrames, pObj, i )
+            sat_solver_add_buffer( pSat, nVars + i, pCnf->pVarNums[Gia_ObjId(pFrames, Gia_ObjFanin0(pObj))], Gia_ObjFaninC0(pObj) );
+    }
+    Cnf_DataFree( pCnf );
+    Gia_ManStop( pFrames );
+    return pSat;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Int2_ManCheckFrames( Int2_Man_t * p, int iFrame, int iObj )
+{
+    Vec_Int_t * vMapFrame = (Vec_Int_t *)Vec_PtrEntry(p->vMapFrames, iFrame);
+    return Vec_IntEntry(vMapFrame, iObj);
+}
+static inline void Int2_ManWriteFrames( Int2_Man_t * p, int iFrame, int iObj, int iRes )
+{
+    Vec_Int_t * vMapFrame = (Vec_Int_t *)Vec_PtrEntry(p->vMapFrames, iFrame);
+    assert( Vec_IntEntry(vMapFrame, iObj) == -1 );
+    Vec_IntWriteEntry( vMapFrame, iObj, iRes );
+}
+void Int2_ManCreateFrames( Int2_Man_t * p, int iFrame, Vec_Int_t * vPrefCos )
+{
+    Gia_Obj_t * pObj;
+    int i, Entry, iLit;
+    // create storage room for unfolded IDs
+    for ( i = Vec_PtrSize(p->vMapFrames); i <= iFrame; i++ )
+        Vec_PtrPush( p->vMapFrames, Vec_IntStartFull( Gia_ManObjNum(p->pGia) ) );
+    assert( Vec_PtrSize(p->vMapFrames) == iFrame + 1 );
+    // create constant 0 node
+    if ( f == 0 )
+    {
+        iLit = 1;
+        Int2_ManWriteFrames( p, iFrame, iObj, 0 );
+        sat_solver_addclause( p->pGiaPref, &iLit, &iLit + 1 );
+    }
+    // start the stack
+    Vec_IntClear( p->vStack );
+    Vec_IntForEachEntry( vPrefCos, Entry, i )
+    {
+        pObj = Gia_ManCo( p->pGia, Entry );
+        Vec_IntPush( p->vStack, iFrame );
+        Vec_IntPush( p->vStack, Gia_ObjId(p->pGia, pObj) );
+    }
+    // construct unfolded AIG
+    while ( Vec_IntSize(p->vStack) > 0 )
+    {
+        int iObj   = Vec_IntPop(p->vStack);
+        int iFrame = Vec_IntPop(p->vStack);
+        if ( Int2_ManCheckFrames(p, iFrame, iObj) >= 0 )
+            continue;
+        pObj = Gia_ManObj( p->pGia, iObj );
+        if ( Gia_ObjIsPi(p->pGia, pObj) )
+            Int2_ManWriteFrames( p, iFrame, iObj, Gia_ManAppendCi(p->pFrames) );
+        else if ( iFrame == 0 && Gia_ObjIsRo(p->pGia, iObj) )
+            Int2_ManWriteFrames( p, iFrame, iObj, 0 );
+        else if ( Gia_ObjIsRo(p->pGia, iObj) )
+        {
+            int iObjF = Gia_ObjId( p->pGia, Gia_ObjRoToRi(p->pGia, pObj) );
+            int iLit = Int2_ManCheckFrames( p, iFrame-1, iObjF );
+            if ( iLit >= 0 )
+                Int2_ManWriteFrames( p, iFrame, iObj, iLit );
+            else
+            {
+                Vec_IntPush( p->vStack, iFrame );
+                Vec_IntPush( p->vStack, iObj );
+                Vec_IntPush( p->vStack, iFrame-1 );
+                Vec_IntPush( p->vStack, iObjF );
+            }
+        }
+        else if ( Gia_ObjIsCo(pObj) )
+        {
+            int iObjF = Gia_ObjFaninId0(p->pGia, iObj) );
+            int iLit = Int2_ManCheckFrames( p, iFrame, iObjF );
+            if ( iLit >= 0 )
+                Int2_ManWriteFrames( p, iFrame, iObj, Abc_LitNotCond(iLit, Gia_ObjFaninC0(pObj)) );
+            else
+            {
+                Vec_IntPush( p->vStack, iFrame );
+                Vec_IntPush( p->vStack, iObj );
+                Vec_IntPush( p->vStack, iFrame );
+                Vec_IntPush( p->vStack, iObjF );
+            }
+        }
+        else if ( Gia_ObjIsAnd(pObj) )
+        {
+            int iObjF0 = Gia_ObjFaninId0(p->pGia, iObj) );
+            int iLit0 = Int2_ManCheckFrames( p, iFrame, iObjF0 );
+            int iObjF1 = Gia_ObjFaninId1(p->pGia, iObj) );
+            int iLit1 = Int2_ManCheckFrames( p, iFrame, iObjF1 );
+            if ( iLit0 >= 0 && iLit1 >= 0 )
+            {
+                Entry = Gia_ManObjNum(pFrames);
+                iLit = Gia_ManHashAnd(pFrames, iLit0, iLit1);
+                Int2_ManWriteFrames( p, iFrame, iObj, iLit );
+                if ( Entry < Gia_ManObjNum(pFrames) )
+                {
+                    assert( !Abc_LitIsCompl(iLit) );
+                    sat_solver_add_and( p->pGiaPref, Abc_Lit2Var(iLit), Abc_Lit2Var(iLit0), Abc_Lit2Var(iLit1), Abc_LitIsCompl(iLit0), Abc_LitIsCompl(iLit1) ); 
+                }
+            }
+            else
+            {
+                Vec_IntPush( p->vStack, iFrame );
+                Vec_IntPush( p->vStack, iObj );
+                if ( iLit0 < 0 )
+                {
+                    Vec_IntPush( p->vStack, iFrame );
+                    Vec_IntPush( p->vStack, iObjF0 );
+                }
+                if ( iLit1 < 0 )
+                {
+                    Vec_IntPush( p->vStack, iFrame );
+                    Vec_IntPush( p->vStack, iObjF1 );
+                }
+            }
+        }
+        else assert( 0 );
+    }
+}
+int Int2_ManCheckBmc( Int2_Man_t * p, Vec_Int_t * vCube )
+{
+    int status;
+    if ( vCube == NULL )
+    {
+        Gia_Obj_t * pObj;
+        int i, iLit;
+        Gia_ManForEachPo( p->pGia, pObj, i )
+        {
+            iLit = Int2_ManCheckFrames( p, 0, Gia_ObjId(p->pGia, pObj) );
+            if ( iLit == 0 )
+                continue;
+            if ( iLit == 1 )
+                return 0;
+            status = sat_solver_solve( p->pSatPref, &iLit, &iLit + 1, 0, 0, 0, 0 );
+            if ( status == l_False )
+                continue;
+            if ( status == l_True )
+                return 0;
+            return -1;
+        }
+        return 1;
+    }
+    status = sat_solver_solve( p->pSatPref, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube), 0, 0, 0, 0 );
+    if ( status == l_False )
+        return 1;
+    if ( status == l_True )
+        return 0;
+    return -1;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/int2/int2Core.c b/src/proof/int2/int2Core.c
new file mode 100644
index 00000000..feeab3ca
--- /dev/null
+++ b/src/proof/int2/int2Core.c
@@ -0,0 +1,335 @@
+/**CFile****************************************************************
+
+  FileName    [int2Core.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 - Dec 1, 2013.]
+
+  Revision    [$Id: int2Core.c,v 1.00 2013/12/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "int2Int.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [This procedure sets default values of interpolation parameters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Int2_ManSetDefaultParams( Int2_ManPars_t * p )
+{ 
+    memset( p, 0, sizeof(Int2_ManPars_t) );
+    p->nBTLimit      =  0;     // limit on the number of conflicts
+    p->nFramesS      =  1;     // the starting number timeframes
+    p->nFramesMax    =  0;     // 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->fDropInvar    =  0;     // dump inductive invariant into file
+    p->fVerbose      =  0;     // print verbose statistics
+    p->iFrameMax     = -1;
+}
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Gia_Man_t * Int2_ManUnroll( Gia_Man_t * p, int nFrames )
+{
+    Gia_Man_t * pFrames, * pTemp;
+    Gia_Obj_t * pObj;
+    int i, f;
+    assert( Gia_ManRegNum(pAig) > 0 );
+    pFrames = Gia_ManStart( Gia_ManObjNum(pAig) );
+    pFrames->pName = Abc_UtilStrsav( pAig->pName );
+    pFrames->pSpec = Abc_UtilStrsav( pAig->pSpec );
+    Gia_ManHashAlloc( pFrames );
+    Gia_ManConst0(pAig)->Value = 0;
+    for ( f = 0; f < nFrames; f++ )
+    {
+        Gia_ManForEachRo( pAig, pObj, i )
+            pObj->Value = f ? Gia_ObjRoToRi( pAig, pObj )->Value : 0;
+        Gia_ManForEachPi( pAig, pObj, i )
+            pObj->Value = Gia_ManAppendCi( pFrames );
+        Gia_ManForEachAnd( pAig, pObj, i )
+            pObj->Value = Gia_ManHashAnd( pFrames, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+        Gia_ManForEachRi( pAig, pObj, i )
+            pObj->Value = Gia_ObjFanin0Copy(pObj);
+    }
+    Gia_ManForEachRi( pAig, pObj, i )
+        Gia_ManAppendCo( pFrames, pObj->Value );
+    Gia_ManHashStop( pFrames );
+    pFrames = Gia_ManCleanup( pTemp = pFrames );
+    Gia_ManStop( pTemp );
+    return pFrames;
+}
+sat_solver * Int2_ManPreparePrefix( Gia_Man_t * p, int f, Vec_Int_t ** pvCiMap )
+{
+    Gia_Man_t * pPref, * pNew;
+    sat_solver * pSat;
+    // create subset of the timeframe
+    pPref = Int2_ManUnroll( p, f );
+    // create SAT solver
+    pNew = Jf_ManDeriveCnf( pPref, 0 );  
+    pCnf = (Cnf_Dat_t *)pPref->pData; pPref->pData = NULL;
+    Gia_ManStop( pPref );
+    // derive the SAT solver
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    // collect indexes of CO variables
+    *pvCiMap = Vec_IntAlloc( 100 );
+    Gia_ManForEachPo( pNew, pObj, i )     
+        Vec_IntPush( *pvCiMap, pCnf->pVarNums[ Gia_ObjId(pNew, pObj) ] );
+    // cleanup
+    Cnf_DataFree( pCnf );
+    Gia_ManStop( pNew );
+    return pSat;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+sat_solver * Int2_ManPrepareSuffix( Gia_Man_t * p, Vec_Int_t * vImageOne, Vec_Int_t * vImagesAll, Vec_Int_t ** pvCoMap, Gia_Man_t ** ppSuff )
+{
+    Gia_Man_t * pSuff, * pNew;
+    Gia_Obj_t * pObj;
+    Cnf_Dat_t * pCnf;
+    sat_solver * pSat;
+    Vec_Int_t * vLits;
+    int i, Lit, Limit;
+    // create subset of the timeframe
+    pSuff = Int2_ManProbToGia( p, vImageOne );
+    assert( Gia_ManPiNum(pSuff) == Gia_ManCiNum(p) );
+    // create SAT solver
+    pNew = Jf_ManDeriveCnf( pSuff, 0 );  
+    pCnf = (Cnf_Dat_t *)pSuff->pData; pSuff->pData = NULL;
+    Gia_ManStop( pSuff );
+    // derive the SAT solver
+    pSat = (sat_solver *)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    // create new constraints
+    vLits = Vec_IntAlloc( 1000 );
+    Vec_IntForEachEntryStart( vImagesAll, Limit, i, 1 )
+    {
+        Vec_IntClear( vLits );
+        for ( k = 0; k < Limit; k++ )
+        {
+            i++;
+            Lit = Vec_IntEntry( vSop, i + k );
+            Vec_IntPush( vLits, Abc_LitNot(Lit) );
+        }
+        if ( !sat_solver_addclause( pSat, Vec_IntArray(vLits), Vec_IntArray(vLits) + Vec_IntSize(vLits) )  )  // UNSAT
+        {
+            Vec_IntFree( vLits );
+            Cnf_DataFree( pCnf );
+            Gia_ManStop( pNew );
+            *pvCoMap = NULL;
+            return NULL;
+        }
+    }
+    Vec_IntFree( vLits );
+    // collect indexes of CO variables
+    *pvCoMap = Vec_IntAlloc( 100 );
+    Gia_ManForEachRo( p, pObj, i )     
+    {
+        pObj = Gia_ManPi( pNew, i + Gia_ManPiNum(p) );
+        Vec_IntPush( *pvCoMap, pCnf->pVarNums[ Gia_ObjId(pNew, pObj) ] );
+    }
+    // cleanup
+    Cnf_DataFree( pCnf );
+    if ( ppSuff )
+        *ppSuff = pNew;
+    else
+        Gia_ManStop( pNew );
+    return pSat;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the cube cover and status.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Int2_ManComputePreimage( Gia_Man_t * pSuff, sat_solver * pSatPref, sat_solver * pSatSuff, Vec_Int_t * vCiMap, Vec_Int_t * vCoMap, Vec_Int_t * vPrio )
+{
+    int i, iVar, status;
+    Vec_IntClear( p->vImage );
+    while ( 1 )
+    {
+        // run suffix solver
+        status = sat_solver_solve( p->pSatSuff, NULL, NULL, 0, 0, 0, 0 );
+        if ( status == l_Undef )
+            return NULL; // timeout
+        if ( status == l_False )
+            return INT2_COMPUTED;
+        assert( status == l_True );
+        // collect assignment
+        Vec_IntClear( p->vAssign );
+        Vec_IntForEachEntry( p->vCiMap, iVar, i )
+            Vec_IntPush( p->vAssign, sat_solver_var_value(p->pSatSuff, iVar) );
+        // derive initial cube
+        vCube = Int2_ManRefineCube( p->pSuff, p->vAssign, p->vPrio );
+        // expend the cube using prefix
+        status = sat_solver_solve( p->pSatPref, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube), 0, 0, 0, 0 );
+        if ( status == l_False )
+        {
+            int k, nCoreLits, * pCoreLits;
+            nCoreLits = sat_solver_final( p->pSatPref, &pCoreLits );
+            // create cube
+            Vec_IntClear( vCube );
+            Vec_IntPush( vImage, nCoreLits );
+            for ( k = 0; k < nCoreLits; k++ )
+            {
+                Vec_IntPush( vCube, pCoreLits[k] );
+                Vec_IntPush( vImage, pCoreLits[k] );
+            }
+            // add cube to the solver
+            if ( !sat_solver_addclause( p->pSatSuff, Vec_IntArray(vCube), Vec_IntArray(vCube) + Vec_IntSize(vCube) ) )
+            {
+                Vec_IntFree( vCube );
+                return INT2_COMPUTED;
+            }
+        }
+        Vec_IntFree( vCube );
+        if ( status == l_Undef )
+            return INT2_TIME_OUT;
+        if ( status == l_True )
+            return INT2_FALSE_NEG;
+        assert( status == l_False );
+        continue;
+    }
+    return p->vImage;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Interpolates 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 Int2_ManPerformInterpolation( Gia_Man_t * pInit, Int2_ManPars_t * pPars )
+{
+    Int2_Man_t * p;
+    int f, i, RetValue = -1;
+    abctime clk, clkTotal = Abc_Clock(), timeTemp = 0;
+    abctime nTimeToStop = pPars->nSecLimit ? pPars->nSecLimit * CLOCKS_PER_SEC + Abc_Clock() : 0;
+
+    // sanity checks
+    assert( Gia_ManPiNum(pInit) > 0 );
+    assert( Gia_ManPoNum(pInit) > 0 );
+    assert( Gia_ManRegNum(pInit) > 0 );
+
+    // create manager
+    p = Int2_ManCreate( pInit, pPars );
+
+    // create SAT solver
+    p->pSatPref = sat_solver_new();
+    sat_solver_setnvars( p->pSatPref, 1000 );
+    sat_solver_set_runtime_limit( p->pSatPref, nTimeToStop );
+
+    // check outputs in the first frame
+    for ( i = 0; i < Gia_ManPoNum(pInit); i++ )
+        Vec_IntPush( p->vPrefCos, i );
+    Int2_ManCreateFrames( p, 0, p->vPrefCos );
+    RetValue = Int2_ManCheckBmc( p, NULL );
+    if ( RetValue != 1 )
+        return RetValue;
+
+    // create original image
+    for ( f = pPars->nFramesS; f < p->nFramesMax; f++ )
+    {
+        for ( i = 0; i < p->nFramesMax; i++ )
+        {
+            p->pSatSuff = Int2_ManPrepareSuffix( p, vImageOne. vImagesAll, &vCoMap, &pGiaSuff );
+            sat_solver_set_runtime_limit( p->pSatSuff, nTimeToStop );
+            Vec_IntFreeP( &vImageOne );
+            vImageOne = Int2_ManComputePreimage( pGiaSuff, p->pSatPref, p->pSatSuff, vCiMap, vCoMap );
+            Vec_IntFree( vCoMap );
+            Gia_ManStop( pGiaSuff );
+            if ( nTimeToStop && Abc_Clock() > nTimeToStop )
+                return -1;
+            if ( vImageOne == NULL )
+            {
+                if ( i == 0 )
+                {
+                    printf( "Satisfiable in frame %d.\n", f );
+                    Vec_IntFree( vCiMap );
+                    sat_solver_delete( p->pSatPref ); p->pSatPref = NULL;
+                    return 0;
+                }
+                f += i;
+                break;
+            }
+            Vec_IntAppend( vImagesAll, vImageOne );
+            sat_solver_delete( p->pSatSuff ); p->pSatSuff = NULL;
+        }
+        Vec_IntFree( vCiMap );
+        sat_solver_delete( p->pSatPref ); p->pSatPref = NULL;
+    }
+    Abc_PrintTime( "Time", Abc_Clock() - clk );
+
+
+p->timeSatPref += Abc_Clock() - clk;
+
+    Int2_ManStop( p );
+    return RetValue;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/int2/int2Int.h b/src/proof/int2/int2Int.h
new file mode 100644
index 00000000..837a2bca
--- /dev/null
+++ b/src/proof/int2/int2Int.h
@@ -0,0 +1,164 @@
+/**CFile****************************************************************
+
+  FileName    [int2Int.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 - Dec 1, 2013.]
+
+  Revision    [$Id: int2Int.h,v 1.00 2013/12/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+ 
+#ifndef ABC__Gia__int2__intInt_h
+#define ABC__Gia__int2__intInt_h
+
+
+////////////////////////////////////////////////////////////////////////
+///                          INCLUDES                                ///
+////////////////////////////////////////////////////////////////////////
+
+#include "aig/gia/gia.h"
+#include "sat/bsat/satSolver.h"
+#include "sat/cnf/cnf.h"
+#include "int2.h"
+
+////////////////////////////////////////////////////////////////////////
+///                         PARAMETERS                               ///
+////////////////////////////////////////////////////////////////////////
+
+ABC_NAMESPACE_HEADER_START
+
+////////////////////////////////////////////////////////////////////////
+///                         BASIC TYPES                              ///
+////////////////////////////////////////////////////////////////////////
+
+// interpolation manager
+typedef struct Int2_Man_t_ Int2_Man_t;
+struct Int2_Man_t_
+{
+    // parameters
+    Int2_ManPars_t * pPars;        // parameters
+    // GIA managers
+    Gia_Man_t *      pGia;         // original manager
+    Gia_Man_t *      pGiaPref;     // prefix manager
+    Gia_Man_t *      pGiaSuff;     // suffix manager
+    // subset of the manager
+    Vec_Int_t *      vSuffCis;     // suffix CIs
+    Vec_Int_t *      vSuffCos;     // suffix COs
+    Vec_Int_t *      vPrefCos;     // suffix POs
+    Vec_Int_t *      vStack;       // temporary stack
+    // preimages
+    Vec_Int_t *      vImageOne;    // latest preimage
+    Vec_Int_t *      vImagesAll;   // cumulative preimage
+    // variable maps
+    Vec_Ptr_t *      vMapFrames;   // mapping of GIA IDs into frame IDs
+    Vec_Int_t *      vMapPref;     // mapping of flop inputs into SAT variables
+    Vec_Int_t *      vMapSuff;     // mapping of flop outputs into SAT variables
+    // initial minimization
+    Vec_Int_t *      vAssign;      // assignment of PIs in pGiaSuff
+    Vec_Int_t *      vPrio;        // priority of PIs in pGiaSuff
+    // SAT solving
+    sat_solver *     pSatPref;     // prefix solver
+    sat_solver *     pSatSuff;     // suffix solver
+    // runtime
+    abctime          timeSatPref;
+    abctime          timeSatSuff;
+    abctime          timeOther;
+    abctime          timeTotal;
+};
+
+static inline Int2_Man_t * Int2_ManCreate( Gia_Man_t * pGia, Int2_ManPars_t * pPars )
+{
+    Int2_Man_t * p;
+    p = ABC_CALLOC( Int2_Man_t, 1 );
+    p->pPars       = pPars;
+    p->pGia        = pGia;
+    p->pGiaPref    = Gia_ManStart( 10000 );
+    // perform structural hashing
+    Gia_ManHashAlloc( pFrames );
+    // subset of the manager
+    p->vSuffCis    = Vec_IntAlloc( Gia_ManCiNum(pGia) );
+    p->vSuffCos    = Vec_IntAlloc( Gia_ManCoNum(pGia) );
+    p->vPrefCos    = Vec_IntAlloc( Gia_ManCoNum(pGia) );
+    p->vStack      = Vec_IntAlloc( 10000 );
+    // preimages
+    p->vImageOne   = Vec_IntAlloc( 1000 );
+    p->vImagesAll  = Vec_IntAlloc( 1000 );
+    // variable maps
+    p->vMapFrames  = Vec_PtrAlloc( 100 );
+    p->vMapPref    = Vec_IntAlloc( Gia_ManRegNum(pGia) );
+    p->vMapSuff    = Vec_IntAlloc( Gia_ManRegNum(pGia) );
+    // initial minimization
+    p->vAssign     = Vec_IntAlloc( Gia_ManCiNum(pGia) );
+    p->vPrio       = Vec_IntAlloc( Gia_ManCiNum(pGia) );
+    return p;
+}
+static inline void Int2_ManStop( Int2_Man_t * p )
+{
+    // GIA managers
+    Gia_ManStopP( &p->pGiaPref );
+    Gia_ManStopP( &p->pGiaSuff );
+    // subset of the manager
+    Vec_IntFreeP( &p->vSuffCis );
+    Vec_IntFreeP( &p->vSuffCos );
+    Vec_IntFreeP( &p->vPrefCos );
+    Vec_IntFreeP( &p->vStack );
+    // preimages
+    Vec_IntFreeP( &p->vImageOne );
+    Vec_IntFreeP( &p->vImagesAll );
+    // variable maps
+    Vec_VecFree( (Vec_Vec_t *)p->vMapFrames );
+    Vec_IntFreeP( &p->vMapPref );
+    Vec_IntFreeP( &p->vMapSuff );
+    // initial minimization
+    Vec_IntFreeP( &p->vAssign );
+    Vec_IntFreeP( &p->vPrio );
+    // SAT solving
+    if ( p->pSatPref )
+        sat_solver_delete( p->pSatPref );
+    if ( p->timeSatSuff )
+        sat_solver_delete( p->pSatSuff );
+    ABC_FREE( p );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                      MACRO DEFINITIONS                           ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                    FUNCTION DECLARATIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/*=== int2Bmc.c =============================================================*/
+extern int           Int2_ManCheckInit( Gia_Man_t * p );
+extern Gia_Man_t *   Int2_ManDupInit( Gia_Man_t * p, int fVerbose );
+extern sat_solver *  Int2_ManSetupBmcSolver( Gia_Man_t * p, int nFrames );
+extern void          Int2_ManCreateFrames( Int2_Man_t * p, int iFrame, Vec_Int_t * vPrefCos );
+extern int           Int2_ManCheckBmc( Int2_Man_t * p, Vec_Int_t * vCube );
+
+/*=== int2Refine.c =============================================================*/
+extern Vec_Int_t *   Int2_ManRefineCube( Gia_Man_t * p, Vec_Int_t * vAssign, Vec_Int_t * vPrio );
+
+/*=== int2Util.c ============================================================*/
+extern Gia_Man_t *   Int2_ManProbToGia( Gia_Man_t * p, Vec_Int_t * vSop );
+
+
+ABC_NAMESPACE_HEADER_END
+
+
+
+#endif
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
diff --git a/src/proof/int2/int2Refine.c b/src/proof/int2/int2Refine.c
new file mode 100644
index 00000000..91008ac6
--- /dev/null
+++ b/src/proof/int2/int2Refine.c
@@ -0,0 +1,154 @@
+/**CFile****************************************************************
+
+  FileName    [int2Refine.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Interpolation engine.]
+
+  Synopsis    [Various utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - Dec 1, 2013.]
+
+  Revision    [$Id: int2Refine.c,v 1.00 2013/12/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "int2Int.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Int2_ManJustify_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vSelect )
+{ 
+    if ( pObj->fMark1 )
+        return;
+    pObj->fMark1 = 1;
+    if ( Gia_ObjIsPi(p, pObj) )
+        return;
+    if ( Gia_ObjIsCo(pObj) )
+    {
+        Vec_IntPush( vSelect, Gia_ObjCioId(pObj) );
+        return;
+    }
+    assert( Gia_ObjIsAnd(pObj) );
+    if ( pObj->Value == 1 )
+    {
+        if ( Gia_ObjFanin0(pObj)->Value < ABC_INFINITY )
+            Int2_ManJustify_rec( p, Gia_ObjFanin0(pObj), vSelect );
+        if ( Gia_ObjFanin1(pObj)->Value < ABC_INFINITY )
+            Int2_ManJustify_rec( p, Gia_ObjFanin1(pObj), vSelect );
+        return;
+    }
+    if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 )
+    {
+        if ( Gia_ObjFanin0(pObj)->fMark0 <= Gia_ObjFanin1(pObj)->fMark0 ) // choice
+        {
+            if ( Gia_ObjFanin0(pObj)->Value < ABC_INFINITY )
+                Int2_ManJustify_rec( p, Gia_ObjFanin0(pObj), vSelect );
+        }
+        else
+        {
+            if ( Gia_ObjFanin1(pObj)->Value < ABC_INFINITY )
+                Int2_ManJustify_rec( p, Gia_ObjFanin1(pObj), vSelect );
+        }
+    }
+    else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 )
+    {
+        if ( Gia_ObjFanin0(pObj)->Value < ABC_INFINITY )
+            Int2_ManJustify_rec( p, Gia_ObjFanin0(pObj), vSelect );
+    }
+    else if ( (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 )
+    {
+        if ( Gia_ObjFanin1(pObj)->Value < ABC_INFINITY )
+            Int2_ManJustify_rec( p, Gia_ObjFanin1(pObj), vSelect );
+    }
+    else assert( 0 );
+ }
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the reduced set of flop variables.]
+
+  Description [Given is a single-output seq AIG manager and an assignment 
+  of its CIs.  Returned is a subset of flops that justifies the output.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Int2_ManRefineCube( Gia_Man_t * p, Vec_Int_t * vAssign, Vec_Int_t * vPrio )
+{
+    Vec_Int_t * vSubset;
+    Gia_Obj_t * pObj;
+    int i;
+    // set values and prios
+    assert( Gia_ManRegNum(p) > 0 );
+    assert( Vec_IntSize(vAssign) == Vec_IntSize(vPrio) );
+    Gia_ManConst0(p)->fMark0 = 0;
+    Gia_ManConst0(p)->fMark1 = 0;
+    Gia_ManConst0(p)->Value = ABC_INFINITY;
+    Gia_ManForEachCi( p, pObj, i )
+    {
+        pObj->fMark0 = Vec_IntEntry(vAssign, i);
+        pObj->fMark1 = 0;
+        pObj->Value  = Vec_IntEntry(vPrio, i);        
+    }
+    Gia_ManForEachAnd( p, pObj, i )
+    {
+        pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) & (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj));
+        pObj->fMark1 = 0;
+        if ( pObj->fMark0 == 1 )
+            pObj->Value = Abc_MaxInt( Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value );
+        else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 && (Gia_ObjFanin1(pObj)->fMark0 ^ Gia_ObjFaninC1(pObj)) == 0 )
+            pObj->Value = Abc_MinInt( Gia_ObjFanin0(pObj)->Value, Gia_ObjFanin1(pObj)->Value ); // choice
+        else if ( (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj)) == 0 )
+            pObj->Value = Gia_ObjFanin0(pObj)->Value;
+        else 
+            pObj->Value = Gia_ObjFanin1(pObj)->Value;
+    }
+    pObj = Gia_ManPo( p, 0 );
+    pObj->fMark0 = (Gia_ObjFanin0(pObj)->fMark0 ^ Gia_ObjFaninC0(pObj));
+    pObj->fMark1 = 0;
+    pObj->Value  = Gia_ObjFanin0(pObj)->Value;
+    assert( pObj->fMark0 == 1 );
+    assert( pObj->Value < ABC_INFINITY );
+    // select subset
+    vSubset = Vec_IntAlloc( 100 );
+    Int2_ManJustify_rec( p, Gia_ObjFanin0(pObj), vSubset );
+    return vSubset;
+}
+
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/int2/int2Util.c b/src/proof/int2/int2Util.c
new file mode 100644
index 00000000..f675d0b9
--- /dev/null
+++ b/src/proof/int2/int2Util.c
@@ -0,0 +1,152 @@
+/**CFile****************************************************************
+
+  FileName    [int2Util.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [Interpolation engine.]
+
+  Synopsis    [Various utilities.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - Dec 1, 2013.]
+
+  Revision    [$Id: int2Util.c,v 1.00 2013/12/01 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "int2Int.h"
+
+ABC_NAMESPACE_IMPL_START
+
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Int2_ManComputeCoPres( Vec_Int_t * vSop, int nRegs )
+{
+    Vec_Int_t * vCoPres, * vMap;
+    vCoPres = Vec_IntAlloc( 100 );
+    if ( vSop == NULL )
+        Vec_IntPush( vCoPres, 0 );
+    else
+    {
+        int i, k, Limit;
+        vMap = Vec_IntStart( nRegs );
+        Vec_IntForEachEntryStart( vSop, Limit, i, 1 )
+        {
+            for ( k = 0; k < Limit; k++ )
+            {
+                i++;
+                assert( Vec_IntEntry(vSop, i + k) < 2 * nRegs );
+                Vec_IntWriteEntry( vMap, Abc_Lit2Var(Vec_IntEntry(vSop, i + k)), 1 );
+            }
+        }
+        Vec_IntForEachEntry( vMap, Limit, i )
+            if ( Limit )
+                Vec_IntPush( vCoPres, i+1 );
+        Vec_IntFree( vMap );
+    }
+    return vCoPres;
+}
+
+void Int2_ManCollectInternal_rec( Gia_Man_t * p, Gia_Obj_t * pObj, Vec_Int_t * vNodes )
+{
+    if ( Gia_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Gia_ObjSetTravIdCurrent(p, pObj);
+    if ( Gia_ObjIsCi(pObj) )
+        return;
+    assert( Gia_ObjIsAnd(pObj) );
+    Int2_ManCollectInternal_rec( p, Gia_ObjFanin0(pObj), vNodes );
+    Int2_ManCollectInternal_rec( p, Gia_ObjFanin1(pObj), vNodes );
+    Vec_IntPush( vNodes, Gia_ObjId(p, pObj) );
+}
+Vec_Int_t * Int2_ManCollectInternal( Gia_Man_t * p, Vec_Int_t * vCoPres )
+{
+    Vec_Int_t * vNodes;
+    Gia_Obj_t * pObj;
+    int i, Entry;
+    Gia_ManIncrementTravId( p );
+    Gia_ObjSetTravIdCurrent(p, Gia_ManConst0(p));
+    Gia_ManForEachCi( p, pObj, i )
+        Gia_ObjSetTravIdCurrent(p, pObj);
+    vNodes = Vec_IntAlloc( 1000 );
+    Vec_IntForEachEntry( vCoPres, Entry, i )
+        Int2_ManCollectInternal_rec( p, Gia_ObjFanin0(Gia_ManCo(p, Entry)), vNodes );
+    return vNodes;
+}
+Gia_Man_t * Int2_ManProbToGia( Gia_Man_t * p, Vec_Int_t * vSop )
+{
+    Vec_Int_t * vCoPres, * vNodes;
+    Gia_Man_t * pNew, * pTemp;
+    Gia_Obj_t * pObj;
+    int i, k, Entry, Limit;
+    int Lit, Cube, Sop;
+    assert( Gia_ManPoNum(p) == 1 );
+    // collect COs and ANDs
+    vCoPres = Int2_ManComputeCoPres( vSop, Gia_ManRegNum(p) );
+    vNodes = Int2_ManCollectInternal( p, vCoPres );
+    // create new manager
+    pNew = Gia_ManStart( Gia_ManObjNum(p) );
+    pNew->pName = Abc_UtilStrsav( p->pName );
+    pNew->pSpec = Abc_UtilStrsav( p->pSpec );
+    Gia_ManConst0(p)->Value = 0;
+    Gia_ManForEachCi( p, pObj, i )
+        pObj->Value = Gia_ManAppendCi(pNew);
+    Gia_ManHashAlloc( pNew );
+    Gia_ManForEachObjVec( vNodes, p, pObj, i )
+        pObj->Value = Gia_ManHashAnd( pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) );
+    Vec_IntForEachEntry( vCoPres, Entry, i )
+    {
+        pObj = Gia_ManCo(p, Entry);
+        pObj->Value = Gia_ObjFanin0Copy( pObj );
+    }
+    // create additional cubes
+    Sop = 0;
+    Vec_IntForEachEntryStart( vSop, Limit, i, 1 )
+    {
+        Cube = 1;
+        for ( k = 0; k < Limit; k++ )
+        {
+            i++;
+            Lit = Vec_IntEntry( vSop, i + k );
+            pObj = Gia_ManRi( p, Abc_Lit2Var(Lit) );
+            Cube = Gia_ManHashAnd( pNew, Cube, Abc_LitNotCond(pObj->Value, Abc_LitIsCompl(Lit)) );
+        }
+        Sop = Gia_ManHashOr( pNew, Sop, Cube );
+    }
+    Gia_ManAppendCo( pNew, Sop );
+    Gia_ManHashStop( pNew );
+    // cleanup
+    pNew = Gia_ManCleanup( pTemp = pNew );
+    Gia_ManStop( pTemp );
+    return pNew;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/proof/int2/module.make b/src/proof/int2/module.make
new file mode 100644
index 00000000..900ec7f4
--- /dev/null
+++ b/src/proof/int2/module.make
@@ -0,0 +1,4 @@
+SRC +=    src/proof/int2/int2Bmc.c \
+    src/proof/int2/int2Core.c \
+    src/proof/int2/int2Refine.c \
+    src/proof/int2/int2Util.c