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 )