From 1f9abfd7a8c2d3978ee58d4be2d07cc633a5008d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 17 Sep 2012 10:02:37 -0700 Subject: Bug fix: no need to normalize const0 node. --- src/proof/cec/cecSolve.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src/proof/cec') 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++ ); -- cgit v1.2.3