3 files changed, 3 insertions, 0 deletions
diff --git a/src/sat/cnf/cnf.h b/src/sat/cnf/cnf.h
index 0b6fc8c2..54aaf5ca 100644
--- a/src/sat/cnf/cnf.h
+++ b/src/sat/cnf/cnf.h
@@ -64,6 +64,7 @@ struct Cnf_Dat_t_
     int *           pVarNums;        // the number of CNF variable for each node ID (-1 if unused)
     int *           pObj2Clause;     // the mapping of objects into clauses
     int *           pObj2Count;      // the mapping of objects into clause number
+    Vec_Int_t *     vMapping;        // mapping of internal nodes
 };
 
 // the cut used to represent node in the AIG
diff --git a/src/sat/cnf/cnfCore.c b/src/sat/cnf/cnfCore.c
index eb46e704..d1dd8561 100644
--- a/src/sat/cnf/cnfCore.c
+++ b/src/sat/cnf/cnfCore.c
@@ -180,6 +180,7 @@ clk = clock();
     Cnf_ManTransferCuts( p );
     vMapped = Cnf_ManScanMapping( p, 1, 1 );
     pCnf = Cnf_ManWriteCnfOther( p, vMapped );
+    pCnf->vMapping = Cnf_ManWriteCnfMapping( p, vMapped );
     Vec_PtrFree( vMapped );
     Aig_MmFixedStop( pMemCuts, 0 );
 p->timeSave = clock() - clk;
diff --git a/src/sat/cnf/cnfMan.c b/src/sat/cnf/cnfMan.c
index a4081f86..c3099d1e 100644
--- a/src/sat/cnf/cnfMan.c
+++ b/src/sat/cnf/cnfMan.c
@@ -181,6 +181,7 @@ void Cnf_DataFree( Cnf_Dat_t * p )
 {
     if ( p == NULL )
         return;
+    Vec_IntFreeP( &p->vMapping );
     ABC_FREE( p->pObj2Clause );
     ABC_FREE( p->pObj2Count );
     ABC_FREE( p->pClauses[0] );