diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-09-28 16:27:39 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-09-28 16:27:39 -0700 |
| commit | 4f0f2e09f84b66c1ed9a842a71a09f2f1ec65588 (patch) | |
| tree | ecd646bd842662c7c4d165b3f2e7358c0d752c2b /src/proof/pdr/pdrCore.c | |
| parent | ca93730781ac2a6559e16a6203786073b1cbd514 (diff) | |
| download | abc-4f0f2e09f84b66c1ed9a842a71a09f2f1ec65588.tar.gz abc-4f0f2e09f84b66c1ed9a842a71a09f2f1ec65588.tar.bz2 abc-4f0f2e09f84b66c1ed9a842a71a09f2f1ec65588.zip | |
Adding flag 'pdr -e' to output only support variables in the invariant.
Diffstat (limited to 'src/proof/pdr/pdrCore.c')
| -rw-r--r-- | src/proof/pdr/pdrCore.c | 1 |
1 files changed, 1 insertions, 0 deletions
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c index 5b619f4b..c020c56a 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -60,6 +60,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ) pPars->fTwoRounds = 0; // use two rounds for generalization pPars->fMonoCnf = 0; // monolythic CNF pPars->fDumpInv = 0; // dump inductive invariant + pPars->fUseSupp = 1; // using support variables in the invariant pPars->fShortest = 0; // forces bug traces to be shortest pPars->fUsePropOut = 1; // use property output pPars->fVerbose = 0; // verbose output |