From feebac4156f8d2314e664aa9ac5d33157c3df5b8 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Thu, 28 Dec 2017 13:26:08 -0800
Subject: Corner-case bug fixed in CNF generation.

---
 src/aig/gia/giaMf.c | 7 ++++++-
 1 file changed, 6 insertions(+), 1 deletion(-)

(limited to 'src')

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];
-- 
cgit v1.2.3