Commit c97b685c by Alan Mishchenko

Bug fix in multi-output BMC.

parent 508565ff
...@@ -1642,6 +1642,8 @@ nTimeSat += Abc_Clock() - clk2; ...@@ -1642,6 +1642,8 @@ nTimeSat += Abc_Clock() - clk2;
if ( !pPars->fNotVerbose ) if ( !pPars->fNotVerbose )
Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n", 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) ); nOutDigits, k, f, nOutDigits, pPars->nFailOuts, nOutDigits, Saig_ManPoNum(pAig) );
// set the output number
pCexNew0->iPo = k;
// report to the bridge // report to the bridge
if ( p->pPars->fUseBridge ) if ( p->pPars->fUseBridge )
Gia_ManToBridgeResult( stdout, 0, pCexNew0, pCexNew0->iPo ); Gia_ManToBridgeResult( stdout, 0, pCexNew0, pCexNew0->iPo );
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment