diff --git a/src/aig/gia/giaMfs.c b/src/aig/gia/giaMfs.c
index d443ddde9..a0e6caed4 100644
--- a/src/aig/gia/giaMfs.c
+++ b/src/aig/gia/giaMfs.c
@@ -67,7 +67,7 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
     int nBoxes   = Gia_ManBoxNum(p), nVars;
     int nRealPis = nBoxes ? Tim_ManPiNum(pManTime) : Gia_ManPiNum(p);
     int nRealPos = nBoxes ? Tim_ManPoNum(pManTime) : Gia_ManPoNum(p);
-    int i, j, k, curCi, curCo, nBoxIns, nBoxOuts;
+    int i, j, k, curCi, curCo, nBoxIns, nBoxOuts, w, nWords;
     int Id, iFan, nMfsVars, nBbIns = 0, nBbOuts = 0, Counter = 0;
     int nLutSizeMax = Gia_ManLutSizeMax( p );
     nLutSizeMax = Abc_MaxInt( nLutSizeMax, 6 );
@@ -113,15 +113,11 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
         pTruth = Gia_ObjComputeTruthTableCut( p, Gia_ManObj(p, Id), vLeaves );
         nVars = Abc_TtMinBase( pTruth, Vec_IntArray(vArray), Vec_IntSize(vArray), Vec_IntSize(vLeaves) );
         Vec_IntShrink( vArray, nVars );
-        if ( nVars <= 6 )
-            Vec_WrdWriteEntry( vTruths, Counter, pTruth[0] );
-        else
-        {
-            int w, nWords = Abc_Truth6WordNum( nVars );
-            Vec_IntWriteEntry( vStarts, Counter, Vec_WrdSize(vTruths2) );
-            for ( w = 0; w < nWords; w++ )
-                Vec_WrdPush( vTruths2, pTruth[w] );
-        }
+        Vec_WrdWriteEntry( vTruths, Counter, pTruth[0] );
+        nWords = Abc_Truth6WordNum( nVars );
+        Vec_IntWriteEntry( vStarts, Counter, Vec_WrdSize(vTruths2) );
+        for ( w = 0; w < nWords; w++ )
+            Vec_WrdPush( vTruths2, pTruth[w] );
         if ( Gia_ObjLutIsMux(p, Id) )
         {
             Vec_StrWriteEntry( vFixed, Counter, (char)1 );
@@ -143,6 +139,8 @@ Sfm_Ntk_t * Gia_ManExtractMfs( Gia_Man_t * p )
             Vec_StrWriteEntry( vEmpty, Counter, (char)1 );
             uTruth = Gia_ObjFaninC0(pObj) ? ~uTruths6[0]: uTruths6[0];
             Vec_WrdWriteEntry( vTruths, Counter, uTruth );
+            Vec_IntWriteEntry( vStarts, Counter, Vec_WrdSize(vTruths2) );
+            Vec_WrdPush( vTruths2, uTruth );
         }
         Gia_ObjSetCopyArray( p, Gia_ObjId(p, pObj), Counter++ );
     }
diff --git a/src/base/abci/abcMfs.c b/src/base/abci/abcMfs.c
index d91bda66f..0533d189f 100644
--- a/src/base/abci/abcMfs.c
+++ b/src/base/abci/abcMfs.c
@@ -100,6 +100,8 @@ Vec_Int_t * Abc_NtkAssignStarts( Abc_Ntk_t * pNtk, Vec_Ptr_t * vNodes, int * pnT
         Vec_IntWriteEntry( vStarts, pObj->iTemp, Counter );
         Counter += Abc_Truth6WordNum( Abc_ObjFaninNum(pObj) );
     }
+    Abc_NtkForEachCo( pNtk, pObj, i )
+        Vec_IntWriteEntry( vStarts, pObj->iTemp, Counter++ );
     *pnTotal = Counter;
     return vStarts;
 }
@@ -167,6 +169,8 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk, int nFirstFixed )
         if ( Abc_ObjFaninNum(pObj) <= 6 )
         {
             word uTruth = Abc_SopToTruth((char *)pObj->pData, Abc_ObjFaninNum(pObj));
+            int Offset  = Vec_IntEntry( vStarts, pObj->iTemp );
+            Vec_WrdWriteEntry( vTruths2, Offset, uTruth );
             Vec_WrdWriteEntry( vTruths, pObj->iTemp, uTruth );
             if ( uTruth == 0 || ~uTruth == 0 )
                 continue;
@@ -177,6 +181,7 @@ Sfm_Ntk_t * Abc_NtkExtractMfs( Abc_Ntk_t * pNtk, int nFirstFixed )
             int Offset  = Vec_IntEntry( vStarts, pObj->iTemp );
             word * pRes = Vec_WrdEntryP( vTruths2, Offset );
             Abc_SopToTruthBig( (char *)pObj->pData, Abc_ObjFaninNum(pObj), pTruths, pCube, pRes );
+            Vec_WrdWriteEntry( vTruths, pObj->iTemp, pRes[0] );
             // check const0
             for ( k = 0; k < nWords; k++ )
                 if ( pRes[k] )
@@ -324,11 +329,13 @@ void Abc_NtkInsertMfs( Abc_Ntk_t * pNtk, Sfm_Ntk_t * p )
         }
         // update fanins
         vArray = Sfm_NodeReadFanins( p, pNode->iTemp );
-        Vec_IntForEachEntry( vArray, Fanin, k )
-            Abc_ObjAddFanin( pNode, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, Fanin)) );
         pTruth = Sfm_NodeReadTruth( p, pNode->iTemp );
         pNode->pData = Abc_SopCreateFromTruthIsop( (Mem_Flex_t *)pNtk->pManFunc, Vec_IntSize(vArray), pTruth, vCover );
+        if ( Abc_SopGetVarNum((char *)pNode->pData) == 0 )
+            continue;
         assert( Abc_SopGetVarNum((char *)pNode->pData) == Vec_IntSize(vArray) );
+        Vec_IntForEachEntry( vArray, Fanin, k )
+            Abc_ObjAddFanin( pNode, Abc_NtkObj(pNtk, Vec_IntEntry(vMap, Fanin)) );
     }
     Vec_IntFree( vCover );
     Vec_IntFree( vMap );
diff --git a/src/opt/sfm/sfmCore.c b/src/opt/sfm/sfmCore.c
index 356aea357..571a35ec8 100644
--- a/src/opt/sfm/sfmCore.c
+++ b/src/opt/sfm/sfmCore.c
@@ -115,6 +115,7 @@ int Sfm_NodeResubSolve( Sfm_Ntk_t * p, int iNode, int f, int fRemoveOnly )
     int fVeryVerbose = 0;//p->pPars->fVeryVerbose && Vec_IntSize(p->vDivs) < 200;// || pNode->Id == 556;
     int i, iFanin, iVar = -1;
     int iFaninRem = -1, iFaninSkip = -1;
+    int nFanins = Sfm_ObjFaninNum(p, iNode); 
     word uTruth, uSign, uMask;
     abctime clk;
     assert( Sfm_ObjIsNode(p, iNode) );
@@ -214,7 +215,10 @@ finish:
     if ( fSkipUpdate )
         return 0;
     // update the network
-    Sfm_NtkUpdate( p, iNode, f, (iVar == -1 ? iVar : Vec_IntEntry(p->vDivs, iVar)), uTruth );
+    Sfm_NtkUpdate( p, iNode, f, (iVar == -1 ? iVar : Vec_IntEntry(p->vDivs, iVar)), uTruth, p->pTruth );
+    // the number of fanins cannot increase
+    assert( nFanins >= Sfm_ObjFaninNum(p, iNode) );
+    //printf( "Modifying node %d with %d fanins (resulting in %d fanins).\n", iNode, nFanins, Sfm_ObjFaninNum(p, iNode) );
     return 1;
 }
 
@@ -304,7 +308,7 @@ int Sfm_NodeResub( Sfm_Ntk_t * p, int iNode )
                 return 1;
         }
     // try simplifying local functions
-    if ( p->pPars->fUseDcs )
+    if ( p->pPars->fUseDcs && Sfm_ObjFaninNum(p, iNode) <= 6 )
         if ( Sfm_NodeResubOne( p, iNode ) )
             return 1;
 /*
@@ -360,7 +364,7 @@ void Sfm_NtkPrint( Sfm_Ntk_t * p )
 ***********************************************************************/
 int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
 {
-    int i, k, Counter = 0;
+    int i, k, Counter = 0, CounterLarge = 0;
     //Sfm_NtkPrint( p );
     p->timeTotal = Abc_Clock();
     if ( pPars->fVerbose )
@@ -382,8 +386,13 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
             continue;
         if ( p->pPars->nDepthMax && Sfm_ObjLevel(p, i) > p->pPars->nDepthMax )
             continue;
-        if ( Sfm_ObjFaninNum(p, i) < 2 || Sfm_ObjFaninNum(p, i) > 6 )
+        if ( Sfm_ObjFaninNum(p, i) < 2 )
             continue;
+        if ( Sfm_ObjFaninNum(p, i) > SFM_SUPP_MAX )
+        {
+            CounterLarge++;
+            continue;
+        }
         for ( k = 0; Sfm_NodeResub(p, i); k++ )
         {
 //            Counter++;
@@ -396,6 +405,8 @@ int Sfm_NtkPerform( Sfm_Ntk_t * p, Sfm_Par_t * pPars )
     p->nTotalNodesEnd = Vec_WecSizeUsedLimits( &p->vFanins, Sfm_NtkPiNum(p), Vec_WecSize(&p->vFanins) - Sfm_NtkPoNum(p) );
     p->nTotalEdgesEnd = Vec_WecSizeSize(&p->vFanins) - Sfm_NtkPoNum(p);
     p->timeTotal = Abc_Clock() - p->timeTotal;
+    if ( pPars->fVerbose && CounterLarge )
+        printf( "MFS skipped %d (out of %d) nodes with more than %d fanins.\n", CounterLarge, p->nNodes, SFM_SUPP_MAX );
     if ( pPars->fVerbose )
         Sfm_NtkPrintStats( p );
     //Sfm_NtkPrint( p );
diff --git a/src/opt/sfm/sfmInt.h b/src/opt/sfm/sfmInt.h
index 08edf353c..ae4bb60a8 100644
--- a/src/opt/sfm/sfmInt.h
+++ b/src/opt/sfm/sfmInt.h
@@ -39,6 +39,7 @@
 #include "misc/st/st.h"
 #include "map/mio/mio.h"
 #include "base/abc/abc.h"
+#include "misc/util/utilTruth.h"
 #include "sfm.h"
 
 ////////////////////////////////////////////////////////////////////////
@@ -47,7 +48,8 @@
 
 ABC_NAMESPACE_HEADER_START
 
-#define SFM_FANIN_MAX 6
+#define SFM_FANIN_MAX 12
+#define SFM_WORDS_MAX ((SFM_FANIN_MAX>6) ? (1<<(SFM_FANIN_MAX-6)) : 1)
 #define SFM_SAT_UNDEC 0x1234567812345678
 #define SFM_SAT_SAT   0x8765432187654321
 
@@ -123,6 +125,10 @@ struct Sfm_Ntk_t_
     Vec_Int_t *       vValues;     // SAT variable values
     Vec_Wec_t *       vClauses;    // CNF clauses for the node
     Vec_Int_t *       vFaninMap;   // mapping fanins into their SAT vars
+    word              TtElems[SFM_FANIN_MAX][SFM_WORDS_MAX];
+    word *            pTtElems[SFM_FANIN_MAX];
+    word              pTruth[SFM_WORDS_MAX];
+    word              pCube[SFM_WORDS_MAX];
     // nodes
     int               nTotalNodesBeg;
     int               nTotalEdgesBeg;
@@ -216,7 +222,7 @@ extern int          Sfm_LibImplementGatesDelay( Sfm_Lib_t * p, int * pFanins, Mi
 /*=== sfmNtk.c ==========================================================*/
 extern Sfm_Ntk_t *  Sfm_ConstructNetwork( Vec_Wec_t * vFanins, int nPis, int nPos );
 extern void         Sfm_NtkPrepare( Sfm_Ntk_t * p );
-extern void         Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth );
+extern void         Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth, word * pTruth );
 /*=== sfmSat.c ==========================================================*/
 extern int          Sfm_NtkWindowToSolver( Sfm_Ntk_t * p );
 extern word         Sfm_ComputeInterpolant( Sfm_Ntk_t * p );
diff --git a/src/opt/sfm/sfmNtk.c b/src/opt/sfm/sfmNtk.c
index d410aa0b3..2d6b928b9 100644
--- a/src/opt/sfm/sfmNtk.c
+++ b/src/opt/sfm/sfmNtk.c
@@ -166,7 +166,7 @@ void Sfm_CreateLevelR( Vec_Wec_t * vFanouts, Vec_Int_t * vLevelsR, Vec_Str_t * v
 ***********************************************************************/
 Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t * vFixed, Vec_Str_t * vEmpty, Vec_Wrd_t * vTruths, Vec_Int_t * vStarts, Vec_Wrd_t * vTruths2 )
 {
-    Sfm_Ntk_t * p;
+    Sfm_Ntk_t * p; int i;
     Sfm_CheckConsistency( vFanins, nPis, nPos, vFixed );
     p = ABC_CALLOC( Sfm_Ntk_t, 1 );
     p->nObjs    = Vec_WecSize( vFanins );
@@ -192,6 +192,10 @@ Sfm_Ntk_t * Sfm_NtkConstruct( Vec_Wec_t * vFanins, int nPis, int nPos, Vec_Str_t
     Vec_IntFill( &p->vVar2Id,   2*p->nObjs, -1 );
     p->vCover   = Vec_IntAlloc( 1 << 16 );
     p->vCnfs    = Sfm_CreateCnf( p );
+    // elementary truth tables
+    for ( i = 0; i < SFM_FANIN_MAX; i++ )
+        p->pTtElems[i] = p->TtElems[i];
+    Abc_TtElemInit( p->pTtElems, SFM_FANIN_MAX );
     return p;
 }
 void Sfm_NtkPrepare( Sfm_Ntk_t * p )
@@ -315,13 +319,14 @@ void Sfm_NtkUpdateLevelR_rec( Sfm_Ntk_t * p, int iNode )
     Sfm_ObjForEachFanin( p, iNode, iFanin, i )
         Sfm_NtkUpdateLevelR_rec( p, iFanin );
 }
-void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth )
+void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth, word * pTruth )
 {
     int iFanin = Sfm_ObjFanin( p, iNode, f );
+    int nWords = Abc_Truth6WordNum( Sfm_ObjFaninNum(p, iNode) );
     assert( Sfm_ObjIsNode(p, iNode) );
     assert( iFanin != iFaninNew );
-    assert( Sfm_ObjFaninNum(p, iNode) <= 6 );
-    if ( uTruth == 0 || ~uTruth == 0 )
+    assert( Sfm_ObjFaninNum(p, iNode) <= SFM_FANIN_MAX );
+    if ( Abc_TtIsConst0(pTruth, nWords) || Abc_TtIsConst1(pTruth, nWords) )
     {
         Sfm_ObjForEachFanin( p, iNode, iFanin, f )
         {
@@ -346,7 +351,9 @@ void Sfm_NtkUpdate( Sfm_Ntk_t * p, int iNode, int f, int iFaninNew, word uTruth
         Sfm_NtkUpdateLevelR_rec( p, iFanin );
     // update truth table
     Vec_WrdWriteEntry( p->vTruths, iNode, uTruth );
-    Sfm_TruthToCnf( uTruth, NULL, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
+    if ( p->vTruths2 && Vec_WrdSize(p->vTruths2) )
+        Abc_TtCopy( Vec_WrdEntryP(p->vTruths2, Vec_IntEntry(p->vStarts, iNode)), pTruth, nWords, 0 );
+    Sfm_TruthToCnf( uTruth, pTruth, Sfm_ObjFaninNum(p, iNode), p->vCover, (Vec_Str_t *)Vec_WecEntry(p->vCnfs, iNode) );
 }
 
 /**Function*************************************************************
diff --git a/src/opt/sfm/sfmSat.c b/src/opt/sfm/sfmSat.c
index ed38e681c..c83f86883 100644
--- a/src/opt/sfm/sfmSat.c
+++ b/src/opt/sfm/sfmSat.c
@@ -153,13 +153,15 @@ int Sfm_NtkWindowToSolver( Sfm_Ntk_t * p )
 ***********************************************************************/
 word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
 {
-    word * pSign, uCube, uTruth = 0;
+    word * pSign;
     int status, i, Div, iVar, nFinal, * pFinal, nIter = 0;
     int pLits[2], nVars = sat_solver_nvars( p->pSat );
+    int nWords = Abc_Truth6WordNum( Vec_IntSize(p->vDivIds) );
     sat_solver_setnvars( p->pSat, nVars + 1 );
     pLits[0] = Abc_Var2Lit( Sfm_ObjSatVar(p, p->iPivotNode), 0 ); // F = 1
     pLits[1] = Abc_Var2Lit( nVars, 0 ); // iNewLit
-    assert( Vec_IntSize(p->vDivIds) <= 6 );
+    assert( Vec_IntSize(p->vDivIds) <= SFM_FANIN_MAX );
+    Abc_TtClear( p->pTruth, nWords );
     while ( 1 ) 
     {
         // find onset minterm
@@ -168,7 +170,7 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
         if ( status == l_Undef )
             return SFM_SAT_UNDEC;
         if ( status == l_False )
-            return uTruth;
+            return p->pTruth[0];
         assert( status == l_True );
         // remember variable values
         Vec_IntClear( p->vValues );
@@ -189,7 +191,7 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
         assert( status == l_False );
         // compute cube and add clause
         nFinal = sat_solver_final( p->pSat, &pFinal );
-        uCube = ~(word)0;
+        Abc_TtFill( p->pCube, nWords );
         Vec_IntClear( p->vLits );
         Vec_IntPush( p->vLits, Abc_LitNot(pLits[1]) ); // NOT(iNewLit)
         for ( i = 0; i < nFinal; i++ )
@@ -198,9 +200,9 @@ word Sfm_ComputeInterpolant( Sfm_Ntk_t * p )
                 continue;
             Vec_IntPush( p->vLits, pFinal[i] );
             iVar = Vec_IntFind( p->vDivIds, Abc_Lit2Var(pFinal[i]) );   assert( iVar >= 0 );
-            uCube &= Abc_LitIsCompl(pFinal[i]) ? s_Truths6[iVar] : ~s_Truths6[iVar];
+            Abc_TtAndSharp( p->pCube, p->pCube, p->pTtElems[iVar], nWords, !Abc_LitIsCompl(pFinal[i]) );
         }
-        uTruth |= uCube;
+        Abc_TtOr( p->pTruth, p->pTruth, p->pCube, nWords );
         status = sat_solver_addclause( p->pSat, Vec_IntArray(p->vLits), Vec_IntArray(p->vLits) + Vec_IntSize(p->vLits) );
         assert( status );
         nIter++;