diff options
Diffstat (limited to 'src')
| -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..." ); |