From c97b685c949a1c07fd43e4683e00a030d42865c8 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Tue, 11 Mar 2014 09:53:38 -0700
Subject: Bug fix in multi-output BMC.

---
 src/sat/bmc/bmcBmc3.c | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'src')

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 );
-- 
cgit v1.2.3