summaryrefslogtreecommitdiffstats
path: root/src/sat
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2014-04-07 14:20:25 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2014-04-07 14:20:25 -0700
commit22ada3b2b7667c376404b4c870307dd9717563b2 (patch)
tree3d543b0a8ed0376bd313596aa80725a77e1f415b /src/sat
parent7753e097f991b321e6e912b7db1f5f1e0f64ba9d (diff)
downloadabc-22ada3b2b7667c376404b4c870307dd9717563b2.tar.gz
abc-22ada3b2b7667c376404b4c870307dd9717563b2.tar.bz2
abc-22ada3b2b7667c376404b4c870307dd9717563b2.zip
Adding command to dump UNSAT core of BMC instance.
Diffstat (limited to 'src/sat')
-rw-r--r--src/sat/bmc/bmcBCore.c1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcBCore.c b/src/sat/bmc/bmcBCore.c
index 3a13ed88..97076858 100644
--- a/src/sat/bmc/bmcBCore.c
+++ b/src/sat/bmc/bmcBCore.c
@@ -252,6 +252,7 @@ void Bmc_ManBCorePerform( Gia_Man_t * p, Bmc_BCorePar_t * pPars )
Abc_PrintTime( 1, "Time", clock() - clk );
}
// write the problem
+ Vec_IntSort( vCore, 0 );
pFile = pPars->pFileProof ? fopen( pPars->pFileProof, "wb" ) : stdout;
Intp_ManUnsatCorePrintForBmc( pFile, (Sto_Man_t *)pSatCnf, vCore, vVarMap );
if ( pFile != stdout )