diff options
Diffstat (limited to 'src/proof/cec/cecCore.c')
| -rw-r--r-- | src/proof/cec/cecCore.c | 8 |
1 files changed, 4 insertions, 4 deletions
diff --git a/src/proof/cec/cecCore.c b/src/proof/cec/cecCore.c index 51debba6..4e8e5497 100644 --- a/src/proof/cec/cecCore.c +++ b/src/proof/cec/cecCore.c @@ -232,14 +232,14 @@ void Cec_ManChcSetDefaultParams( Cec_ParChc_t * p ) SeeAlso [] ***********************************************************************/ -Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars ) +Gia_Man_t * Cec_ManSatSolving( Gia_Man_t * pAig, Cec_ParSat_t * pPars, int f0Proved ) { Gia_Man_t * pNew; Cec_ManPat_t * pPat; pPat = Cec_ManPatStart(); - Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL ); + Cec_ManSatSolve( pPat, pAig, pPars, NULL, NULL, NULL, f0Proved ); // pNew = Gia_ManDupDfsSkip( pAig ); - pNew = Gia_ManDup( pAig ); + pNew = Gia_ManCleanup( pAig ); Cec_ManPatStop( pPat ); pNew->vSeqModelVec = pAig->vSeqModelVec; pAig->vSeqModelVec = NULL; @@ -445,7 +445,7 @@ clk = Abc_Clock(); if ( pPars->fRunCSat ) Cec_ManSatSolveCSat( pPat, pSrm, pParsSat ); else - Cec_ManSatSolve( pPat, pSrm, pParsSat, p->pAig->vIdsOrig, p->vXorNodes, pAig->vIdsEquiv ); + Cec_ManSatSolve( pPat, pSrm, pParsSat, p->pAig->vIdsOrig, p->vXorNodes, pAig->vIdsEquiv, 0 ); p->timeSat += Abc_Clock() - clk; if ( Cec_ManFraClassesUpdate( p, pSim, pPat, pSrm ) ) { |