From 42927d5ebb7b7a828790394dc555cd129aa2481b Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Mon, 7 Apr 2014 14:10:51 -0700 Subject: Adding command to dump UNSAT core of BMC instance. --- src/aig/saig/saigGlaPba.c | 2 +- src/aig/saig/saigRetMin.c | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) (limited to 'src/aig/saig') diff --git a/src/aig/saig/saigGlaPba.c b/src/aig/saig/saigGlaPba.c index 14f47c5c..d26bbe89 100644 --- a/src/aig/saig/saigGlaPba.c +++ b/src/aig/saig/saigGlaPba.c @@ -429,7 +429,7 @@ Vec_Int_t * Saig_AbsSolverUnsatCore( sat_solver * pSat, int nConfMax, int fVerbo // derive the UNSAT core clk = clock(); pManProof = Intp_ManAlloc(); - vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0 ); + vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0, 0 ); Intp_ManFree( pManProof ); if ( fVerbose ) { diff --git a/src/aig/saig/saigRetMin.c b/src/aig/saig/saigRetMin.c index ff3e45df..a1bebd64 100644 --- a/src/aig/saig/saigRetMin.c +++ b/src/aig/saig/saigRetMin.c @@ -128,7 +128,7 @@ int Saig_ManRetimeUnsatCore( Aig_Man_t * p, int fVerbose ) sat_solver_delete( pSat ); // derive the UNSAT core pManProof = Intp_ManAlloc(); - vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, fVeryVerbose ); + vCore = (Vec_Int_t *)Intp_ManUnsatCore( pManProof, (Sto_Man_t *)pSatCnf, 0, fVeryVerbose ); Intp_ManFree( pManProof ); Sto_ManFree( (Sto_Man_t *)pSatCnf ); // derive the set of variables on which the core depends -- cgit v1.2.3