Lines Matching defs:Fra_Sec_t_
114 struct Fra_Sec_t_ struct
116 int fTryComb; // try CEC call as a preprocessing step
117 int fTryBmc; // try BMC call as a preprocessing step
118 int nFramesMax; // the max number of frames used for induction
119 int nBTLimit; // the conflict limit at a node
120 int nBTLimitGlobal; // the global conflict limit
121 int nBTLimitInter; // the conflict limit for interpolation
122 int nBddVarsMax; // the state space limit for BDD reachability
123 int nBddMax; // the max number of BDD nodes
124 int nBddIterMax; // the limit on the number of BDD iterations
125 int nPdrTimeout; // the timeout for PDR in the end
126 int fPhaseAbstract; // enables phase abstraction
127 int fRetimeFirst; // enables most-forward retiming at the beginning
128 int fRetimeRegs; // enables min-register retiming at the beginning
129 int fFraiging; // enables fraiging at the beginning
130 int fInduction; // enable the use of induction
131 int fInterpolation; // enables interpolation
132 int fInterSeparate; // enables interpolation for each outputs separately
133 int fReachability; // enables BDD based reachability
134 int fReorderImage; // enables BDD reordering during image computation
135 … fStopOnFirstFail; // enables stopping after first output of a miter has failed to prove
136 int fUseNewProver; // the new prover
137 int fUsePdr; // the PDR
138 int fSilent; // disables all output
139 int fVerbose; // enables verbose reporting of statistics
140 int fVeryVerbose; // enables very verbose reporting
141 int TimeLimit; // enables the timeout
142 int fReadUnsolved; // inserts the unsolved model back
143 int nSMnumber; // the number of model written
145 int fRecursive; // set to 1 when SEC is called recursively
146 int fReportSolution; // enables report solution in a special form