diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-07 19:37:46 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-09-07 19:37:46 -0700 |
| commit | af4c76e21a28beac14886e68a5f7ce29e5e7303b (patch) | |
| tree | 0aad9addb18e114d1b90ccdc378371a5bb1d9f10 /src/sat/bmc/bmcBmcS.c | |
| parent | ba0d855fd4eed9439e4ce4fa6eb778cbb2250708 (diff) | |
| download | abc-af4c76e21a28beac14886e68a5f7ce29e5e7303b.tar.gz abc-af4c76e21a28beac14886e68a5f7ce29e5e7303b.tar.bz2 abc-af4c76e21a28beac14886e68a5f7ce29e5e7303b.zip | |
Disabling CNF simplification in &bmcs -g.
Diffstat (limited to 'src/sat/bmc/bmcBmcS.c')
| -rw-r--r-- | src/sat/bmc/bmcBmcS.c | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcBmcS.c b/src/sat/bmc/bmcBmcS.c index 6a5c2a85..8bfda56b 100644 --- a/src/sat/bmc/bmcBmcS.c +++ b/src/sat/bmc/bmcBmcS.c @@ -682,6 +682,7 @@ int Bmcs_ManPerformOne( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) pPars->iFrame = f+k; pGia->pCexSeq = Bmcs_ManGenerateCex( p, i, f+k, 0 ); pPars->nFailOuts++; + Bmcs_ManPrintFrame( p, f+k, nClauses, -1, clkStart ); if ( !pPars->fNotVerbose ) { int nOutDigits = Abc_Base10Log( Gia_ManPoNum(pGia) ); @@ -872,6 +873,7 @@ int Bmcs_ManPerformMulti( Gia_Man_t * pGia, Bmc_AndPar_t * pPars ) pPars->iFrame = f+k; pGia->pCexSeq = Bmcs_ManGenerateCex( p, i, f+k, Solver ); pPars->nFailOuts++; + Bmcs_ManPrintFrame( p, f+k, nClauses, Solver, clkStart ); if ( !pPars->fNotVerbose ) { int nOutDigits = Abc_Base10Log( Gia_ManPoNum(pGia) ); |