Commit 22ada3b2 by Alan Mishchenko

Adding command to dump UNSAT core of BMC instance.

parent 7753e097
...@@ -252,6 +252,7 @@ void Bmc_ManBCorePerform( Gia_Man_t * p, Bmc_BCorePar_t * pPars ) ...@@ -252,6 +252,7 @@ void Bmc_ManBCorePerform( Gia_Man_t * p, Bmc_BCorePar_t * pPars )
Abc_PrintTime( 1, "Time", clock() - clk ); Abc_PrintTime( 1, "Time", clock() - clk );
} }
// write the problem // write the problem
Vec_IntSort( vCore, 0 );
pFile = pPars->pFileProof ? fopen( pPars->pFileProof, "wb" ) : stdout; pFile = pPars->pFileProof ? fopen( pPars->pFileProof, "wb" ) : stdout;
Intp_ManUnsatCorePrintForBmc( pFile, (Sto_Man_t *)pSatCnf, vCore, vVarMap ); Intp_ManUnsatCorePrintForBmc( pFile, (Sto_Man_t *)pSatCnf, vCore, vVarMap );
if ( pFile != stdout ) if ( pFile != stdout )
......
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