From 902a78eeb883cb97131e03cc31cf0892787e806e Mon Sep 17 00:00:00 2001 From: Yen-Sheng Ho Date: Tue, 28 Feb 2017 18:05:58 -0800 Subject: added an option -r to %pdra: proof-based refinement only --- src/base/wlc/wlc.h | 9 +++++---- 1 file changed, 5 insertions(+), 4 deletions(-) (limited to 'src/base/wlc/wlc.h') diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 1a2bc505..f5dbba42 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -171,11 +171,12 @@ struct Wlc_Par_t_ int nIterMax; // the max number of iterations int nLimit; // the max number of signals int fXorOutput; // XOR outputs of word-level miter - int fCheckClauses; // Check clauses in the reloaded trace - int fPushClauses; // Push clauses in the reloaded trace - int fMFFC; // Refine the entire MFFC of a PPI - int fPdra; // Use pdr -nct + int fCheckClauses; // Check clauses in the reloaded trace + int fPushClauses; // Push clauses in the reloaded trace + int fMFFC; // Refine the entire MFFC of a PPI + int fPdra; // Use pdr -nct int fProofRefine; // Use proof-based refinement + int fHybrid; // Use a hybrid of CBR and PBR int fVerbose; // verbose output int fPdrVerbose; // verbose output }; -- cgit v1.2.3