diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-14 20:53:06 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-11-14 20:53:06 -0800 |
| commit | f95476b45d8846140f02acd5f60fd1a1e654a28e (patch) | |
| tree | 49d64828cac5779d8590582d1559614b67b29cc3 /src/proof/cec/cecSatG2.c | |
| parent | fef0c368bc64bb9e8109c4d2adcdde9fed0f7399 (diff) | |
| download | abc-f95476b45d8846140f02acd5f60fd1a1e654a28e.tar.gz abc-f95476b45d8846140f02acd5f60fd1a1e654a28e.tar.bz2 abc-f95476b45d8846140f02acd5f60fd1a1e654a28e.zip | |
Improvements to the SAT sweeper (bug fix).
Diffstat (limited to 'src/proof/cec/cecSatG2.c')
| -rw-r--r-- | src/proof/cec/cecSatG2.c | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/proof/cec/cecSatG2.c b/src/proof/cec/cecSatG2.c index ffd6c264..45f56cf0 100644 --- a/src/proof/cec/cecSatG2.c +++ b/src/proof/cec/cecSatG2.c @@ -1549,6 +1549,7 @@ int Cec4_ManPerformSweeping( Gia_Man_t * p, Cec_ParFra_t * pPars, Gia_Man_t ** p pMan->nAndNodes++; pObj->Value = Gia_ManHashAnd( pMan->pNew, Gia_ObjFanin0Copy(pObj), Gia_ObjFanin1Copy(pObj) ); pObjNew = Gia_ManObj( pMan->pNew, Abc_Lit2Var(pObj->Value) ); + if ( Gia_ObjIsAnd(pObjNew) ) if ( Vec_BitEntry(pMan->vFails, Gia_ObjFaninId0(pObjNew, Abc_Lit2Var(pObj->Value))) || Vec_BitEntry(pMan->vFails, Gia_ObjFaninId1(pObjNew, Abc_Lit2Var(pObj->Value))) ) Vec_BitWriteEntry( pMan->vFails, Abc_Lit2Var(pObjNew->Value), 1 ); |