diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-01 02:46:21 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-07-01 02:46:21 -0700 |
| commit | 34b8604a4d7c4368d98a977e0953c790a1445fbe (patch) | |
| tree | 5270427a9b771a95abea781323f721d39e901736 | |
| parent | d3c018cd23df0954be488e6a97c4a7ad7577658e (diff) | |
| download | abc-34b8604a4d7c4368d98a977e0953c790a1445fbe.tar.gz abc-34b8604a4d7c4368d98a977e0953c790a1445fbe.tar.bz2 abc-34b8604a4d7c4368d98a977e0953c790a1445fbe.zip | |
Reducing memory usage in bmc2 and bmc3.
| -rw-r--r-- | src/aig/saig/saigBmc3.c | 3 |
1 files changed, 2 insertions, 1 deletions
diff --git a/src/aig/saig/saigBmc3.c b/src/aig/saig/saigBmc3.c index 0a283bb5..f60f7913 100644 --- a/src/aig/saig/saigBmc3.c +++ b/src/aig/saig/saigBmc3.c @@ -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 * pMapping, i, iLit, Lits[4], uTruth; + assert( fAddClauses ); iLit = Saig_ManBmcLiteral( p, pObj, iFrame ); if ( iLit != ~0 ) return iLit; @@ -1050,7 +1051,7 @@ int Saig_ManBmcCreateCnf_rec( Gia_ManBmc_t * p, Aig_Obj_t * pObj, int iFrame, in { iLit = ABC_INFINITY; } - assert( iLit != ABC_INFINITY ); +// assert( iLit != ABC_INFINITY ); return Saig_ManBmcSetLiteral( p, pObj, iFrame, iLit ); } |