Commit b06908d1 by Alan Mishchenko

Making BMC engines (bmc2, bmc3) to perform OR-decomposition by default (bug fix).

parent 3f525b0d
...@@ -1852,7 +1852,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int ...@@ -1852,7 +1852,7 @@ int Abc_NtkDarBmc( Abc_Ntk_t * pNtk, int nStart, int nFrames, int nSizeMax, int
return RetValue; return RetValue;
} }
assert( pMan->nRegs > 0 ); assert( pMan->nRegs > 0 );
assert( Vec_IntSize(vMap) == Aig_ManPoNum(pMan) ); assert( Vec_IntSize(vMap) == Saig_ManPoNum(pMan) );
if ( fVerbose && vMap && Abc_NtkPoNum(pNtk) != Saig_ManPoNum(pMan) ) if ( fVerbose && vMap && Abc_NtkPoNum(pNtk) != Saig_ManPoNum(pMan) )
printf( "Expanded %d outputs into %d outputs using OR decomposition.\n", Abc_NtkPoNum(pNtk), Saig_ManPoNum(pMan) ); printf( "Expanded %d outputs into %d outputs using OR decomposition.\n", Abc_NtkPoNum(pNtk), Saig_ManPoNum(pMan) );
......
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