diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h
index a8f3c4875..befbc421d 100644
--- a/src/aig/gia/gia.h
+++ b/src/aig/gia/gia.h
@@ -361,6 +361,7 @@ struct Jf_Par_t_
     int            fCnfObjIds;
     int            fAddOrCla;
     int            fCnfMapping;
+    int            fCnfOnly;
     int            fPureAig;
     int            fDoAverage;
     int            fCutHashing;
diff --git a/src/aig/gia/giaMf.c b/src/aig/gia/giaMf.c
index 0e1ae9a97..bfed62a13 100644
--- a/src/aig/gia/giaMf.c
+++ b/src/aig/gia/giaMf.c
@@ -1500,7 +1500,8 @@ void Mf_ManPrintQuit( Mf_Man_t * p, Gia_Man_t * pNew )
     float MemMan   = 1.0 * sizeof(Mf_Obj_t) * Gia_ManObjNum(p->pGia) / (1<<20);
     float MemCuts  = 1.0 * sizeof(int) * (1 << 16) * Vec_PtrSize(&p->vPages) / (1<<20);
     float MemTt    = p->vTtMem ? Vec_MemMemory(p->vTtMem) / (1<<20) : 0;
-    float MemMap   = Vec_IntMemory(pNew->vMapping) / (1<<20);
+    // pNew is NULL under fCnfOnly: no mapped network was built
+    float MemMap   = pNew ? Vec_IntMemory(pNew->vMapping) / (1<<20) : 0;
     if ( p->CutCount[0] == 0 )
         p->CutCount[0] = 1;
     if ( !p->pPars->fVerbose )
@@ -1845,7 +1846,11 @@ Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
     //Mf_ManOptimization( p );
     if ( pPars->fVeryVerbose && pPars->fCutMin )
         Vec_MemDumpTruthTables( p->vTtMem, Gia_ManName(p->pGia), pPars->nLutSize );
-    if ( pPars->fCutMin )
+    // the CNF is derived from the cuts, not from the mapped network, so a
+    // caller that wants only the CNF gets no network and does not pay for one
+    if ( pPars->fCnfOnly )
+        pNew = NULL;
+    else if ( pPars->fCutMin )
         pNew = Mf_ManDeriveMappingGia( p );
     else if ( pPars->fCoarsen )
         pNew = Mf_ManDeriveMappingCoarse( p );
@@ -1855,7 +1860,8 @@ Gia_Man_t * Mf_ManPerformMapping( Gia_Man_t * pGia, Jf_Par_t * pPars )
         pGia->pData = Mf_ManDeriveCnf( p, p->pPars->fCnfObjIds, p->pPars->fAddOrCla );
     //if ( p->pPars->fGenCnf || p->pPars->fGenLit )
     //    Mf_ManProfileTruths( p );
-    Gia_ManMappingVerify( pNew );
+    if ( pNew )
+        Gia_ManMappingVerify( pNew );
     Mf_ManPrintQuit( p, pNew );
     Mf_ManFree( p );
     if ( pCls != pGia )
@@ -1887,6 +1893,8 @@ void * Mf_ManGenerateCnf( Gia_Man_t * pGia, int nLutSize, int fCnfObjIds, int fA
     pPars->fAddOrCla   = fAddOrCla;
     pPars->fCnfMapping = fMapping;
     pPars->fVerbose    = fVerbose;
+    // the mapped network is dropped below, so ask for the CNF alone
+    pPars->fCnfOnly    = 1;
     pNew = Mf_ManPerformMapping( pGia, pPars );
     Gia_ManStopP( &pNew );
 //    Cnf_DataPrint( (Cnf_Dat_t *)pGia->pData, 1 );