diff options
| author | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-20 12:58:20 -0800 |
|---|---|---|
| committer | Yen-Sheng Ho <ysho@berkeley.edu> | 2017-02-20 12:58:20 -0800 |
| commit | c5e9506f5d5a5303b9df453fce7f313147799276 (patch) | |
| tree | 55f5b7955eb94e2fe8a6ee5b23c06f860f6bbd69 /src/proof/pdr | |
| parent | 9f43c84501cf8c5a8ae74cc5bebea63dafc3a714 (diff) | |
| download | abc-c5e9506f5d5a5303b9df453fce7f313147799276.tar.gz abc-c5e9506f5d5a5303b9df453fce7f313147799276.tar.bz2 abc-c5e9506f5d5a5303b9df453fce7f313147799276.zip | |
small tweaks in %pdra -p
Diffstat (limited to 'src/proof/pdr')
| -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 ) |