summaryrefslogtreecommitdiffstats
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/aig/gia/giaMf.c7
1 files changed, 6 insertions, 1 deletions
diff --git a/src/aig/gia/giaMf.c b/src/aig/gia/giaMf.c
index 7d5e14c1..7ec14f9a 100644
--- a/src/aig/gia/giaMf.c
+++ b/src/aig/gia/giaMf.c
@@ -420,8 +420,13 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla )
continue;
pCut = Mf_ObjCutBest( p, Id );
iFunc = Abc_Lit2Var( Mf_CutFunc(pCut) );
- //Dau_DsdPrintFromTruth( Vec_MemReadEntry(p->vTtMem, iFunc), 3 );
fComplLast = Abc_LitIsCompl( Mf_CutFunc(pCut) );
+ if ( iFunc == 0 ) // constant cut
+ {
+ pCnf->pClauses[iCla++] = pCnf->pClauses[0] + iLit;
+ pCnf->pClauses[0][iLit++] = Abc_Var2Lit(pCnfIds[Id], !fComplLast);
+ continue;
+ }
for ( k = 0; k < Mf_CutSize(pCut); k++ )
pFanins[k] = pCnfIds[pCut[k+1]];
pFanins[k++] = pCnfIds[Id];