diff options
| -rw-r--r-- | src/proof/pdr/pdrIncr.c | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c index 85403a7d..6de86c18 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 ) |