diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-04-07 14:13:06 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-04-07 14:13:06 -0700 |
| commit | 7753e097f991b321e6e912b7db1f5f1e0f64ba9d (patch) | |
| tree | be6dd8bfb70fef087291908d187a189129612daf /src | |
| parent | 42927d5ebb7b7a828790394dc555cd129aa2481b (diff) | |
| download | abc-7753e097f991b321e6e912b7db1f5f1e0f64ba9d.tar.gz abc-7753e097f991b321e6e912b7db1f5f1e0f64ba9d.tar.bz2 abc-7753e097f991b321e6e912b7db1f5f1e0f64ba9d.zip | |
Adding command to dump UNSAT core of BMC instance.
Diffstat (limited to 'src')
| -rw-r--r-- | src/sat/bmc/bmcBCore.c | 4 |
1 files 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 |