Commit 4dc569c1 by Alan Mishchenko

Remove assertions when the solver becomes UNSAT after adding constraints in 'scorr -c'.

parent 3b4e9573
...@@ -77,7 +77,7 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew ) ...@@ -77,7 +77,7 @@ int Ssw_NodesAreEquiv( Ssw_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead ) if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
{ {
RetValue = sat_solver_simplify(p->pMSat->pSat); RetValue = sat_solver_simplify(p->pMSat->pSat);
assert( RetValue != 0 ); //assert( RetValue != 0 );
} }
clk = Abc_Clock(); clk = Abc_Clock();
...@@ -139,7 +139,7 @@ p->timeSatUndec += Abc_Clock() - clk; ...@@ -139,7 +139,7 @@ p->timeSatUndec += Abc_Clock() - clk;
if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead ) if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead )
{ {
RetValue = sat_solver_simplify(p->pMSat->pSat); RetValue = sat_solver_simplify(p->pMSat->pSat);
assert( RetValue != 0 ); //assert( RetValue != 0 );
} }
clk = Abc_Clock(); clk = Abc_Clock();
......
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