summaryrefslogtreecommitdiffstats
path: root/src/base/wlc/wlcNtk.c
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/wlcNtk.c
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/wlcNtk.c')
-rw-r--r--src/base/wlc/wlcNtk.c1
1 files changed, 1 insertions, 0 deletions
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 2df659e0..8c6f8fbe 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -123,6 +123,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
pPars->fHybrid = 1; // Use a hybrid of CBR and PBR
pPars->fCheckCombUnsat = 0; // Check if ABS becomes comb. unsat
pPars->fAbs2 = 0; // Use UFAR style createAbs
+ pPars->fProofUsePPI = 0; // Use PPI values in PBR
pPars->fVerbose = 0; // verbose output`
pPars->fPdrVerbose = 0; // show verbose PDR output
}