From 7753e097f991b321e6e912b7db1f5f1e0f64ba9d Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 7 Apr 2014 14:13:06 -0700 Subject: Adding command to dump UNSAT core of BMC instance. --- src/sat/bmc/bmcBCore.c | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/sat/bmc/bmcBCore.c b/src/sat/bmc/bmcBCore.c index cde49f52..3a13ed88 100644 --- a/src/sat/bmc/bmcBCore.c +++ b/src/sat/bmc/bmcBCore.c @@ -240,7 +240,7 @@ void Bmc_ManBCorePerform( Gia_Man_t * p, Bmc_BCorePar_t * pPars ) } assert( RetValue == l_False ); pSatCnf = sat_solver_store_release( pSat ); - Sto_ManDumpClauses( (Sto_Man_t *)pSatCnf, "cnf_store.txt" ); +// Sto_ManDumpClauses( (Sto_Man_t *)pSatCnf, "cnf_store.txt" ); // derive the UNSAT core clk = clock(); pManProof = Intp_ManAlloc(); @@ -248,7 +248,7 @@ void Bmc_ManBCorePerform( Gia_Man_t * p, Bmc_BCorePar_t * pPars ) Intp_ManFree( pManProof ); if ( pPars->fVerbose ) { - printf( "UNSAT core contains %8d (out of %8d) learned clauses. ", Vec_IntSize(vCore), sat_solver_nconflicts(pSat) ); + printf( "UNSAT core contains %d (out of %d) learned clauses. ", Vec_IntSize(vCore), sat_solver_nconflicts(pSat) ); Abc_PrintTime( 1, "Time", clock() - clk ); } // write the problem -- cgit v1.2.3