diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2020-12-16 00:06:31 -0800 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2020-12-16 00:06:31 -0800 |
| commit | 06094ade87fbec6000619bf007aaad596e8bc0a2 (patch) | |
| tree | fc05149c4488137f0ccdde3373602d8d3f4327ac /src/proof/cec/cecChoice.c | |
| parent | 901560bb238f8c4e4dafc4d2489eaa77df4defb3 (diff) | |
| download | abc-06094ade87fbec6000619bf007aaad596e8bc0a2.tar.gz abc-06094ade87fbec6000619bf007aaad596e8bc0a2.tar.bz2 abc-06094ade87fbec6000619bf007aaad596e8bc0a2.zip | |
Adding switch to replace proved outputs by const0.
Diffstat (limited to 'src/proof/cec/cecChoice.c')
| -rw-r--r-- | src/proof/cec/cecChoice.c | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/proof/cec/cecChoice.c b/src/proof/cec/cecChoice.c index 47d6a478..780a1196 100644 --- a/src/proof/cec/cecChoice.c +++ b/src/proof/cec/cecChoice.c @@ -256,7 +256,7 @@ int Cec_ManChoiceComputation_int( Gia_Man_t * pAig, Cec_ParChc_t * pPars ) // found counter-examples to speculation clk2 = Abc_Clock(); if ( pPars->fUseCSat ) - vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0 ); + vCexStore = Cbs_ManSolveMiterNc( pSrm, pPars->nBTLimit, &vStatus, 0, 0 ); else vCexStore = Cec_ManSatSolveMiter( pSrm, pParsSat, &vStatus ); Gia_ManStop( pSrm ); |