From c5e9506f5d5a5303b9df453fce7f313147799276 Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Mon, 20 Feb 2017 12:58:20 -0800 Subject: small tweaks in %pdra -p --- src/proof/pdr/pdrIncr.c | 7 +++++++ 1 file changed, 7 insertions(+) (limited to 'src') 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 ) -- cgit v1.2.3