diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-03-18 19:00:29 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-03-18 19:00:29 -0700 |
| commit | c54da1e990b0e2c52d0f0aaa6af693f9c9dd99b4 (patch) | |
| tree | e226d09670694e76fc73b4ee7dd92b6989a7df21 | |
| parent | 488f949721f3e68edc6028cff40afd8c60f53619 (diff) | |
| download | abc-c54da1e990b0e2c52d0f0aaa6af693f9c9dd99b4.tar.gz abc-c54da1e990b0e2c52d0f0aaa6af693f9c9dd99b4.tar.bz2 abc-c54da1e990b0e2c52d0f0aaa6af693f9c9dd99b4.zip | |
Corner case bug fix in &sat -a.
| -rw-r--r-- | src/proof/cec/cecSolve.c | 15 |
1 files changed, 12 insertions, 3 deletions
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c index 02f14b76..af6a4fdb 100644 --- a/src/proof/cec/cecSolve.c +++ b/src/proof/cec/cecSolve.c @@ -673,6 +673,14 @@ p->timeSatUndec += Abc_Clock() - clk; SeeAlso [] ***********************************************************************/ +Abc_Cex_t * Cex_ManGenSimple( Cec_ManSat_t * p, int iOut ) +{ + Abc_Cex_t * pCex; + pCex = Abc_CexAlloc( 0, Gia_ManCiNum(p->pAig), 1 ); + pCex->iPo = iOut; + pCex->iFrame = 0; + return pCex; +} Abc_Cex_t * Cex_ManGenCex( Cec_ManSat_t * p, int iOut ) { Abc_Cex_t * pCex; @@ -715,10 +723,11 @@ void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPar { if ( Gia_ObjIsConst0(Gia_ObjFanin0(pObj)) ) { - pObj->fMark0 = 0; - pObj->fMark1 = 1; + status = !Gia_ObjFaninC0(pObj); + pObj->fMark0 = (status == 0); + pObj->fMark1 = (status == 1); if ( pPars->fSaveCexes ) - Vec_PtrWriteEntry( pAig->vSeqModelVec, i, (Abc_Cex_t *)(ABC_PTRINT_T)1 ); + Vec_PtrWriteEntry( pAig->vSeqModelVec, i, status ? (Abc_Cex_t *)(ABC_PTRINT_T)1 : Cex_ManGenSimple(p, i) ); continue; } Bar_ProgressUpdate( pProgress, i, "SAT..." ); |