diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-03-30 14:10:12 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-03-30 14:10:12 -0700 |
| commit | 37fd73cf9edb946e19b537ae94d8256f64db243e (patch) | |
| tree | 648de6040f6cc34c9a722c8e201431d679081836 /src/sat/bmc/bmcBmc3.c | |
| parent | 2f926f2fafba8dc2ec073c51b5ac9fdabd9ad201 (diff) | |
| download | abc-37fd73cf9edb946e19b537ae94d8256f64db243e.tar.gz abc-37fd73cf9edb946e19b537ae94d8256f64db243e.tar.bz2 abc-37fd73cf9edb946e19b537ae94d8256f64db243e.zip | |
Adding new code to verify invariant derived by 'pdr'.
Diffstat (limited to 'src/sat/bmc/bmcBmc3.c')
| -rw-r--r-- | src/sat/bmc/bmcBmc3.c | 6 |
1 files changed, 4 insertions, 2 deletions
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index 3a84e496..3a27d54c 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -1663,11 +1663,13 @@ nTimeSat += clkSatRun; if ( !pPars->fNotVerbose ) Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", nOutDigits, k, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) ); - // set the output number - pCexNew0->iPo = k; // report to the bridge if ( p->pPars->fUseBridge ) + { + // set the output number + pCexNew0->iPo = k; Gia_ManToBridgeResult( stdout, 0, pCexNew0, pCexNew0->iPo ); + } // remember solved output Vec_PtrWriteEntry( p->vCexes, k, Abc_CexDup(pCexNew, Saig_ManRegNum(pAig)) ); } |