summaryrefslogtreecommitdiffstats
path: root/src/base/wlc/wlc.h
diff options
context:
space:
mode:
authorYen-Sheng Ho <ysho@berkeley.edu>2017-03-09 21:43:18 -0800
committerYen-Sheng Ho <ysho@berkeley.edu>2017-03-09 21:43:18 -0800
commit70511b001c8868e4c694ed1ac2f3051ffbe2b91a (patch)
tree40f19159a3c5473ca625b0604fd050cfdda15303 /src/base/wlc/wlc.h
parent566beb9c92deebc82996f5f46f831a747fe7fd4d (diff)
downloadabc-70511b001c8868e4c694ed1ac2f3051ffbe2b91a.tar.gz
abc-70511b001c8868e4c694ed1ac2f3051ffbe2b91a.tar.bz2
abc-70511b001c8868e4c694ed1ac2f3051ffbe2b91a.zip
%pdra: added an option -i for weaker proof-based refinement
Diffstat (limited to 'src/base/wlc/wlc.h')
-rw-r--r--src/base/wlc/wlc.h1
1 files changed, 1 insertions, 0 deletions
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
};