From 4dc569c1348275e0049fa461b300992078eab4c8 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 5 Oct 2019 10:40:01 -0700 Subject: Remove assertions when the solver becomes UNSAT after adding constraints in 'scorr -c'. --- src/proof/ssw/sswSat.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) (limited to 'src') diff --git a/src/proof/ssw/sswSat.c b/src/proof/ssw/sswSat.c index 59ed6945..8a8a9710 100644 --- a/src/proof/ssw/sswSat.c +++ b/src/proof/ssw/sswSat.c @@ -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 ) { RetValue = sat_solver_simplify(p->pMSat->pSat); - assert( RetValue != 0 ); + //assert( RetValue != 0 ); } clk = Abc_Clock(); @@ -139,7 +139,7 @@ p->timeSatUndec += Abc_Clock() - clk; if ( p->pMSat->pSat->qtail != p->pMSat->pSat->qhead ) { RetValue = sat_solver_simplify(p->pMSat->pSat); - assert( RetValue != 0 ); + //assert( RetValue != 0 ); } clk = Abc_Clock(); -- cgit v1.2.3