diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2014-03-11 09:53:38 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2014-03-11 09:53:38 -0700 |
| commit | c97b685c949a1c07fd43e4683e00a030d42865c8 (patch) | |
| tree | 5b92d19804c57cf825c7ba3a6b98875d7e513848 /src/sat/bmc/bmcBmc3.c | |
| parent | 508565ff7209b349ae2a917fb56c94af83063338 (diff) | |
| download | abc-c97b685c949a1c07fd43e4683e00a030d42865c8.tar.gz abc-c97b685c949a1c07fd43e4683e00a030d42865c8.tar.bz2 abc-c97b685c949a1c07fd43e4683e00a030d42865c8.zip | |
Bug fix in multi-output BMC.
Diffstat (limited to 'src/sat/bmc/bmcBmc3.c')
| -rw-r--r-- | src/sat/bmc/bmcBmc3.c | 2 |
1 files changed, 2 insertions, 0 deletions
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c index 72fbcc21..bee14df2 100644 --- a/src/sat/bmc/bmcBmc3.c +++ b/src/sat/bmc/bmcBmc3.c @@ -1642,6 +1642,8 @@ nTimeSat += Abc_Clock() - clk2; 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 ) Gia_ManToBridgeResult( stdout, 0, pCexNew0, pCexNew0->iPo ); |