summaryrefslogtreecommitdiffstats
path: root/src/proof/pdr/pdrCore.c
diff options
context:
space:
mode:
authorMathias Soeken <mathias.soeken@gmail.com>2016-09-29 22:10:16 -0700
committerMathias Soeken <mathias.soeken@gmail.com>2016-09-29 22:10:16 -0700
commitf5be1575832e2028eed0942aa69315870532669e (patch)
tree8888abf063a2bf70829dcc840c9add39a1d7d9b0 /src/proof/pdr/pdrCore.c
parente601df9deac339b7404ef366bf10dc0acad8ad3a (diff)
parent9a35f82d5fd396f04a0baaa50b390281c4673172 (diff)
downloadabc-f5be1575832e2028eed0942aa69315870532669e.tar.gz
abc-f5be1575832e2028eed0942aa69315870532669e.tar.bz2
abc-f5be1575832e2028eed0942aa69315870532669e.zip
Merged alanmi/abc into default
Diffstat (limited to 'src/proof/pdr/pdrCore.c')
-rw-r--r--src/proof/pdr/pdrCore.c1
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