From c5e9506f5d5a5303b9df453fce7f313147799276 Mon Sep 17 00:00:00 2001
From: Yen-Sheng Ho <ysho@berkeley.edu>
Date: Mon, 20 Feb 2017 12:58:20 -0800
Subject: [PATCH] small tweaks in %pdra -p

---
 src/proof/pdr/pdrIncr.c | 7 +++++++
 1 file changed, 7 insertions(+)

diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c
index 85403a7d1..6de86c188 100644
--- a/src/proof/pdr/pdrIncr.c
+++ b/src/proof/pdr/pdrIncr.c
@@ -271,6 +271,13 @@ int IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses )
                 Abc_Print( 1, "IPDR: Finished pushing. After:\n" );
                 Pdr_ManPrintProgress( p, 1, Abc_Clock() - clkStart );
             }
+
+            if ( RetValue ) 
+            {
+                Pdr_ManReportInvariant( p );
+                Pdr_ManVerifyInvariant( p );
+                return 1;
+            }
         }
     }
     while ( 1 )