From 4f0f2e09f84b66c1ed9a842a71a09f2f1ec65588 Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Wed, 28 Sep 2016 16:27:39 -0700
Subject: Adding flag 'pdr -e' to output only support variables in the
 invariant.

---
 src/proof/pdr/pdrCore.c | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/proof/pdr/pdrCore.c')

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
-- 
cgit v1.2.3