diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-04-07 14:10:51 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-04-07 14:10:51 -0700 |
| commit | 42927d5ebb7b7a828790394dc555cd129aa2481b (patch) | |
| tree | e608e44763ffb52169a8e7d19021643fb8a27bdc /src/aig/saig | |
| parent | af6705a8b1c75d069ef1fc504080b7bc6ee1c8f5 (diff) | |
| download | abc-42927d5ebb7b7a828790394dc555cd129aa2481b.tar.gz abc-42927d5ebb7b7a828790394dc555cd129aa2481b.tar.bz2 abc-42927d5ebb7b7a828790394dc555cd129aa2481b.zip | |
Adding command to dump UNSAT core of BMC instance.
Diffstat (limited to 'src/aig/saig')
| -rw-r--r-- | src/aig/saig/saigGlaPba.c | 2 | ||||
| -rw-r--r-- | src/aig/saig/saigRetMin.c | 2 |
2 files changed, 2 insertions, 2 deletions
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 |