mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-22 08:35:31 +00:00
Code Activity

remove unused m_max_num_cex parameter

Browse source 
Signed-off-by: Nuno Lopes <nuno.lopes@ist.utl.pt>
This commit is contained in:
Nuno Lopes 2012-11-22 14:23:18 +00:00
parent 6679fc4c0b
commit 0ccae8e2e3
2 changed files with 0 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/front_end_params/front_end_params.cpp
View file

@ -28,8 +28,6 @@ void front_end_params::register_params(ini_params & p) {
p.register_int_param("ENGINE", 0, 2, reinterpret_cast<int&>(m_engine), "0: SMT solver, 1: Superposition prover, 2: EPR solver, true");
z3_solver_params::register_params(p);
model_params::register_params(p);
p.register_unsigned_param("MAX_COUNTEREXAMPLES", m_max_num_cex,
"set the maximum number of counterexamples when using Simplify front end");
p.register_bool_param("AT_LABELS_CEX", m_at_labels_cex,
"only use labels that contain '@' when building multiple counterexamples");
p.register_bool_param("CHECK_AT_LABELS", m_check_at_labels,

2
src/front_end_params/front_end_params.h
View file

@ -41,7 +41,6 @@ struct front_end_params : public preprocessor_params, public spc_params, public
{
ref<param_vector> m_param_vector;
engine m_engine;
unsigned m_max_num_cex; // maximum number of counterexamples
bool m_at_labels_cex; // only use labels which contains the @ symbol when building multiple counterexamples.
bool m_check_at_labels; // check that @ labels are inserted to generate unique counter-examples.
bool m_default_qid;
@ -76,7 +75,6 @@ struct front_end_params : public preprocessor_params, public spc_params, public
front_end_params():
m_param_vector(alloc(param_vector, this)),
m_engine(ENG_SMT),
m_max_num_cex(1),
m_at_labels_cex(false),
m_check_at_labels(false),
m_default_qid(false),