Commit 120a30c2 by Alan Mishchenko

Bug fix in &cec (not generating a CEX).

parent 7fe11c51
...@@ -30954,6 +30954,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv ) ...@@ -30954,6 +30954,7 @@ int Abc_CommandAbc9Cec( Abc_Frame_t * pAbc, int argc, char ** argv )
Abc_Print( 1, "Assuming the current network is a single-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit ); Abc_Print( 1, "Assuming the current network is a single-output miter. (Conflict limit = %d.)\n", pPars->nBTLimit );
pTemp = Gia_ManTransformToDual( pAbc->pGia ); pTemp = Gia_ManTransformToDual( pAbc->pGia );
pAbc->Status = Cec_ManVerify( pTemp, pPars ); pAbc->Status = Cec_ManVerify( pTemp, pPars );
ABC_SWAP( Abc_Cex_t *, pAbc->pGia->pCexComb, pTemp->pCexComb );
Gia_ManStop( pTemp ); Gia_ManStop( pTemp );
} }
Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb ); Abc_FrameReplaceCex( pAbc, &pAbc->pGia->pCexComb );
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment