2 files changed, 37 insertions, 3 deletions

diff --git a/src/aig/fra/fraSec.c b/src/aig/fra/fraSec.c
index 04adb7e3..5944cf56 100644
--- a/src/aig/fra/fraSec.c
+++ b/src/aig/fra/fraSec.c
@@ -20,6 +20,7 @@
 
 #include "fra.h"
 #include "ioa.h"
+#include "int.h"
 
 ////////////////////////////////////////////////////////////////////////
 ///                        DECLARATIONS                              ///
@@ -389,11 +390,15 @@ PRT( "Time", clock() - clkTotal );
 clk = clock();
     if ( pParSec->fInterpolation && RetValue == -1 && Aig_ManRegNum(pNew) > 0 && Aig_ManPoNum(pNew)-Aig_ManRegNum(pNew) == 1 )
     {
-        extern int Saig_Interpolate( Aig_Man_t * pAig, int nConfLimit, int nFramesMax, int fRewrite, int fTransLoop, int fUsePudlak, int fUseOther, int fUseMiniSat, int fCheckInd, int fCheckKstep, int fVerbose, int * pDepth );
+        Inter_ManParams_t Pars, * pPars = &Pars;
         int Depth;
         pNew->nTruePis = Aig_ManPiNum(pNew) - Aig_ManRegNum(pNew); 
         pNew->nTruePos = Aig_ManPoNum(pNew) - Aig_ManRegNum(pNew); 
-        RetValue = Saig_Interpolate( pNew, 5000, 40, 0, 1, 0, 0, 0, 1, 1, pParSec->fVeryVerbose, &Depth );
+
+        Inter_ManSetDefaultParams( pPars );
+        pPars->fVerbose = pParSec->fVeryVerbose;
+        RetValue = Inter_ManPerformInterpolation( pNew, pPars, &Depth );
+
         if ( pParSec->fVerbose )
         {
         if ( RetValue == 1 )
@@ -454,7 +459,7 @@ PRT( "Time", clock() - clk );
             iCount++;
             if ( !pParSec->fSilent )
                 printf( "*** Running output %d of the miter (number %d out of %d unsolved).\n", i, iCount, Counter );
-            pNew2 = Aig_ManDupOneOutput( pNew, i );
+            pNew2 = Aig_ManDupOneOutput( pNew, i, 1 );
             
             TimeLimitCopy = pParSec->TimeLimit;
             pParSec->TimeLimit = TimeLimit2;
diff --git a/src/aig/fra/fraSim.c b/src/aig/fra/fraSim.c
index 53493201..d1d73a03 100644
--- a/src/aig/fra/fraSim.c
+++ b/src/aig/fra/fraSim.c
@@ -542,6 +542,35 @@ void Fra_SmlNodeSimulate( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
   SeeAlso     []
 
 ***********************************************************************/
+int Fra_SmlNodesCompareInFrame( Fra_Sml_t * p, Aig_Obj_t * pObj0, Aig_Obj_t * pObj1, int iFrame0, int iFrame1 )
+{
+    unsigned * pSims0, * pSims1;
+    int i;
+    assert( !Aig_IsComplement(pObj0) );
+    assert( !Aig_IsComplement(pObj1) );
+    assert( iFrame0 == 0 || p->nWordsFrame < p->nWordsTotal );
+    assert( iFrame1 == 0 || p->nWordsFrame < p->nWordsTotal );
+    // get hold of the simulation information
+    pSims0  = Fra_ObjSim(p, pObj0->Id) + p->nWordsFrame * iFrame0;
+    pSims1  = Fra_ObjSim(p, pObj1->Id) + p->nWordsFrame * iFrame1;
+    // compare
+    for ( i = 0; i < p->nWordsFrame; i++ )
+        if ( pSims0[i] != pSims1[i] )
+            return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Simulates one node.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Fra_SmlNodeCopyFanin( Fra_Sml_t * p, Aig_Obj_t * pObj, int iFrame )
 {
     unsigned * pSims, * pSims0;