diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2019-10-05 10:40:01 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2019-10-05 10:40:01 -0700 |
| commit | 4dc569c1348275e0049fa461b300992078eab4c8 (patch) | |
| tree | 68298a883924de025f34a1f008f673a56b3a7e4d /src | |
| parent | 3b4e9573bc689e5b612669042179d44f2131b359 (diff) | |
| download | abc-4dc569c1348275e0049fa461b300992078eab4c8.tar.gz abc-4dc569c1348275e0049fa461b300992078eab4c8.tar.bz2 abc-4dc569c1348275e0049fa461b300992078eab4c8.zip | |
Remove assertions when the solver becomes UNSAT after adding constraints in 'scorr -c'.
Diffstat (limited to 'src')
| -rw-r--r-- | src/proof/ssw/sswSat.c | 4 |
1 files changed, 2 insertions, 2 deletions
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(); |