diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-05-25 13:47:38 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-05-25 13:47:38 -0700 |
| commit | 1d26d58a17226230b40601c3dc40ef4851827a2e (patch) | |
| tree | 847daf199197cc1f2f2f356458f579f60c8ebf9e /src/proof/pdr/pdrCore.c | |
| parent | 58c81ec097d66abdd1ec77853cdcc95f842f12f2 (diff) | |
| download | abc-1d26d58a17226230b40601c3dc40ef4851827a2e.tar.gz abc-1d26d58a17226230b40601c3dc40ef4851827a2e.tar.bz2 abc-1d26d58a17226230b40601c3dc40ef4851827a2e.zip | |
Adding switch 'pdr -o' to control using property output in induction.
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 8e81795b..5b619f4b 100644 --- a/src/proof/pdr/pdrCore.c +++ b/src/proof/pdr/pdrCore.c @@ -61,6 +61,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars ) pPars->fMonoCnf = 0; // monolythic CNF pPars->fDumpInv = 0; // dump inductive invariant pPars->fShortest = 0; // forces bug traces to be shortest + pPars->fUsePropOut = 1; // use property output pPars->fVerbose = 0; // verbose output pPars->fVeryVerbose = 0; // very verbose output pPars->fNotVerbose = 0; // not printing line-by-line progress |