1 files changed, 17 insertions, 0 deletions
diff --git a/src/opt/mfs/mfsInter.c b/src/opt/mfs/mfsInter.c
index 5944fd5b..6e50d444 100644
--- a/src/opt/mfs/mfsInter.c
+++ b/src/opt/mfs/mfsInter.c
@@ -123,6 +123,15 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands,
         return NULL;
     }
 
+    // add one-hotness constraints
+    if ( p->pPars->fOneHotness )
+    {
+        p->pSat = pSat;
+        if ( !Abc_NtkAddOneHotness( p ) )
+            return NULL;
+        p->pSat = NULL;
+    }
+
     // bookmark the clauses of A
     if ( pCands )
         sat_solver_store_mark_clauses_a( pSat );
@@ -139,6 +148,14 @@ sat_solver * Abc_MfsCreateSolverResub( Mfs_Man_t * p, int * pCands, int nCands,
             return NULL;
         }
     }
+    // add one-hotness constraints
+    if ( p->pPars->fOneHotness )
+    {
+        p->pSat = pSat;
+        if ( !Abc_NtkAddOneHotness( p ) )
+            return NULL;
+        p->pSat = NULL;
+    }
     // transform the literals
     for ( i = 0; i < p->pCnf->nLiterals; i++ )
         p->pCnf->pClauses[0][i] -= 2 * p->pCnf->nVars;