diff options
Diffstat (limited to 'src/proof')
| -rw-r--r-- | src/proof/cec/cecSolve.c | 15 | ||||
| -rw-r--r-- | src/proof/fra/fraLcr.c | 2 |
2 files changed, 13 insertions, 4 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..." ); diff --git a/src/proof/fra/fraLcr.c b/src/proof/fra/fraLcr.c index 2d8b3d64..b9e2ccb4 100644 --- a/src/proof/fra/fraLcr.c +++ b/src/proof/fra/fraLcr.c @@ -604,7 +604,7 @@ p->timePart += Abc_Clock() - clk2; p->nNodesBeg = Aig_ManNodeNum(p->pAig); p->nRegsBeg = Aig_ManRegNum(p->pAig); - // perforn interative reduction of the partitions + // perform iterative reduction of the partitions p->fRefining = 1; for ( nIter = 0; p->fRefining; nIter++ ) { |