Commit 34b8604a by Alan Mishchenko

Reducing memory usage in bmc2 and bmc3.

parent d3c018cd
...@@ -992,6 +992,7 @@ static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits ...@@ -992,6 +992,7 @@ static inline void Saig_ManBmcAddClauses( Gia_ManBmc_t * p, int uTruth, int Lits
int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, int fAddClauses ) int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, int fAddClauses )
{ {
int * pMapping, i, iLit, Lits[4], uTruth; int * pMapping, i, iLit, Lits[4], uTruth;
assert( fAddClauses );
iLit = Saig_ManBmcLiteral( p, pObj, iFrame ); iLit = Saig_ManBmcLiteral( p, pObj, iFrame );
if ( iLit != ~0 ) if ( iLit != ~0 )
return iLit; return iLit;
...@@ -1050,7 +1051,7 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in ...@@ -1050,7 +1051,7 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in
{ {
iLit = ABC_INFINITY; iLit = ABC_INFINITY;
} }
assert( iLit != ABC_INFINITY ); // assert( iLit != ABC_INFINITY );
return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit ); return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit );
} }
......
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