From c54da1e990b0e2c52d0f0aaa6af693f9c9dd99b4 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Wed, 18 Mar 2020 19:00:29 -0700 Subject: Corner case bug fix in &sat -a. --- src/proof/cec/cecSolve.c | 15 ++++++++++++--- 1 file changed, 12 insertions(+), 3 deletions(-) (limited to 'src/proof/cec') 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..." ); -- cgit v1.2.3