From 70511b001c8868e4c694ed1ac2f3051ffbe2b91a Mon Sep 17 00:00:00 2001
From: Yen-Sheng Ho <ysho@berkeley.edu>
Date: Thu, 9 Mar 2017 21:43:18 -0800
Subject: %pdra: added an option -i for weaker proof-based refinement

---
 src/base/wlc/wlc.h | 1 +
 1 file changed, 1 insertion(+)

(limited to 'src/base/wlc/wlc.h')

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index c259d3e5..e1ec0d06 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -179,6 +179,7 @@ struct Wlc_Par_t_
     int                    fHybrid;            // Use a hybrid of CBR and PBR
     int                    fCheckCombUnsat;    // Check if ABS becomes comb. unsat
     int                    fAbs2;              // Use UFAR style createAbs
+    int                    fProofUsePPI;       // Use PPI values in PBR
     int                    fVerbose;           // verbose output
     int                    fPdrVerbose;        // verbose output
 };
-- 
cgit v1.2.3