diff options
| author | Miodrag Milanovic <mmicko@gmail.com> | 2021-11-12 12:31:29 +0100 |
|---|---|---|
| committer | Miodrag Milanovic <mmicko@gmail.com> | 2021-11-12 12:31:29 +0100 |
| commit | d2d6bbd9f86f61fc9b5cc7d703e1386bbd6ad6a2 (patch) | |
| tree | 071fb2118c158c748ff9969ef250affe7b9a3561 /src/proof/cec/cecSolve.c | |
| parent | 4f5f73d18b137930fb3048c0b385c82fa078db38 (diff) | |
| parent | 9b245d9f6910c048e9bbcf95ee5dee46f2f24f2c (diff) | |
| download | abc-d2d6bbd9f86f61fc9b5cc7d703e1386bbd6ad6a2.tar.gz abc-d2d6bbd9f86f61fc9b5cc7d703e1386bbd6ad6a2.tar.bz2 abc-d2d6bbd9f86f61fc9b5cc7d703e1386bbd6ad6a2.zip | |
Merge remote-tracking branch 'upstream/master' into yosys-experimental
Diffstat (limited to 'src/proof/cec/cecSolve.c')
| -rw-r--r-- | src/proof/cec/cecSolve.c | 7 |
1 files changed, 5 insertions, 2 deletions
diff --git a/src/proof/cec/cecSolve.c b/src/proof/cec/cecSolve.c index af6a4fdb..f8342859 100644 --- a/src/proof/cec/cecSolve.c +++ b/src/proof/cec/cecSolve.c @@ -696,7 +696,7 @@ Abc_Cex_t * Cex_ManGenCex( Cec_ManSat_t * p, int iOut ) } return pCex; } -void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs ) +void Cec_ManSatSolve( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * pPars, Vec_Int_t * vIdsOrig, Vec_Int_t * vMiterPairs, Vec_Int_t * vEquivPairs, int f0Proved ) { Bar_Progress_t * pProgress = NULL; Cec_ManSat_t * p; @@ -747,6 +747,9 @@ clk2 = Abc_Clock(); if ( pPars->fSaveCexes && status != -1 ) Vec_PtrWriteEntry( pAig->vSeqModelVec, i, status ? (Abc_Cex_t *)(ABC_PTRINT_T)1 : Cex_ManGenCex(p, i) ); + if ( f0Proved && status == 1 ) + Gia_ManPatchCoDriver( pAig, i, 0 ); + /* if ( status == -1 ) { @@ -807,7 +810,7 @@ void Cec_ManSatSolveCSat( Cec_ManPat_t * pPat, Gia_Man_t * pAig, Cec_ParSat_t * { Vec_Str_t * vStatus; Vec_Int_t * vPat = Vec_IntAlloc( 1000 ); - Vec_Int_t * vCexStore = Cbs_ManSolveMiterNc( pAig, pPars->nBTLimit, &vStatus, 0 ); + Vec_Int_t * vCexStore = Cbs_ManSolveMiterNc( pAig, pPars->nBTLimit, &vStatus, 0, 0 ); Gia_Obj_t * pObj; int i, status, iStart = 0; assert( Vec_StrSize(vStatus) == Gia_ManCoNum(pAig) ); |