diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-17 10:02:37 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-17 10:02:37 -0700 |
| commit | 1f9abfd7a8c2d3978ee58d4be2d07cc633a5008d (patch) | |
| tree | a5f7d429777ba06e2ec90282c46288e93c65d40a /src/proof/cec | |
| parent | 819b41bb59b99b82e2c0391ce515d969ead585d7 (diff) | |
| download | abc-1f9abfd7a8c2d3978ee58d4be2d07cc633a5008d.tar.gz abc-1f9abfd7a8c2d3978ee58d4be2d07cc633a5008d.tar.bz2 abc-1f9abfd7a8c2d3978ee58d4be2d07cc633a5008d.zip | |
Bug fix: no need to normalize const0 node.
Diffstat (limited to 'src/proof/cec')
| -rw-r--r-- | src/proof/cec/cecSolve.c | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c index 5e108ae5..41053cf0 100644 --- a/src/proof/cec/cecSolve.c +++ b/src/proof/cec/cecSolve.c @@ -383,8 +383,8 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p ) p->nSatVars = 1; // p->nSatVars = 0; Lit = toLitCond( p->nSatVars, 1 ); - if ( p->pPars->fPolarFlip ) - Lit = lit_neg( Lit ); +// if ( p->pPars->fPolarFlip ) // no need to normalize const0 node (bug fix by SS on 9/17/2012) +// Lit = lit_neg( Lit ); sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); Cec_ObjSetSatNum( p, Gia_ManConst0(p->pAig), p->nSatVars++ ); |