Skip to content

A
abc
Commit c3dccf30 by Alan Mishchenko
Options

Corner-case bug fixed in CNF generation.

parent feebac41
Showing with 1 additions and 0 deletions
src/aig/gia/giaMf.c
...@@ -425,6 +425,7 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla ) ...@@ -425,6 +425,7 @@ Cnf_Dat_t * Mf_ManDeriveCnf( Mf_Man_t * p, int fCnfObjIds, int fAddOrCla )
{ {
pCnf->pClauses[iCla++] = pCnf->pClauses[0] + iLit; pCnf->pClauses[iCla++] = pCnf->pClauses[0] + iLit;
pCnf->pClauses[0][iLit++] = Abc_Var2Lit(pCnfIds[Id], !fComplLast); pCnf->pClauses[0][iLit++] = Abc_Var2Lit(pCnfIds[Id], !fComplLast);
assert( pCnf->vMapping == NULL ); // bug fix does not handle generated mapping
continue; continue;
} }
for ( k = 0; k < Mf_CutSize(pCut); k++ ) for ( k = 0; k < Mf_CutSize(pCut); k++ )
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment