Skip to content

A
abc
Commit 1f9abfd7 by Alan Mishchenko
Options

Bug fix: no need to normalize const0 node.

parent 819b41bb
Showing with 2 additions and 2 deletions
src/proof/cec/cecSolve.c
...@@ -383,8 +383,8 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p ) ...@@ -383,8 +383,8 @@ void Cec_ManSatSolverRecycle( Cec_ManSat_t * p )
p->nSatVars = 1; p->nSatVars = 1;
// p->nSatVars = 0; // p->nSatVars = 0;
Lit = toLitCond( p->nSatVars, 1 ); Lit = toLitCond( p->nSatVars, 1 );
if ( p->pPars->fPolarFlip ) // if ( p->pPars->fPolarFlip ) // no need to normalize const0 node (bug fix by SS on 9/17/2012)
Lit = lit_neg( Lit ); // Lit = lit_neg( Lit );
sat_solver_addclause( p->pSat, &Lit, &Lit + 1 ); sat_solver_addclause( p->pSat, &Lit, &Lit + 1 );
Cec_ObjSetSatNum( p, Gia_ManConst0(p->pAig), p->nSatVars++ ); Cec_ObjSetSatNum( p, Gia_ManConst0(p->pAig), p->nSatVars++ );
......
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