From a4087e45f030476cb071f20ccf60b4619320cd36 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Fri, 13 Sep 2013 17:36:29 -0700
Subject: Enabling additional printouts in 'pdr'.

---
 src/base/abci/abc.c     | 7 +++++++
 src/proof/pdr/pdrCore.c | 6 ++++--
 2 files changed, 11 insertions(+), 2 deletions(-)

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index f264a32d..c8918e90 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2469,6 +2469,13 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
                 printf( "In total, %d (out of %d) outputs are \"sat\" but CEXes are not recorded.\n", Counter, Vec_PtrSize(pAbc->vCexVec) );
         }
     }
+    if ( pAbc->vStatuses )
+    {
+        int i, Entry;
+        Vec_IntForEachEntry( pAbc->vStatuses, Entry, i )
+            printf( "%d=%d  ", i, Entry );
+        printf( "\n" );
+    }
     return 0;
 
 usage:
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 009e9f5d..27426a60 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -738,8 +738,10 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                 if ( p->pTime4Outs[p->iOutCur] == 0 && (p->vCexes == NULL || Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL) )
                 {
                     p->pPars->nDropOuts++;
-                    if ( p->pPars->vOutMap ) Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
-//                    printf( "Dropping output %d.\n", p->iOutCur );
+                    if ( p->pPars->vOutMap ) 
+                        Vec_IntWriteEntry( p->pPars->vOutMap, p->iOutCur, -1 );
+                    if ( p->pPars->fVerbose ) 
+                        printf( "Timing out on output %d.\n", p->iOutCur );
                 }
                 p->timeToStopOne = 0;
             }
-- 
cgit v1.2.3