diff --git a/src/front_end_params/front_end_params.cpp b/src/front_end_params/front_end_params.cpp index 2dc037e1b..a30e1dfd3 100644 --- a/src/front_end_params/front_end_params.cpp +++ b/src/front_end_params/front_end_params.cpp @@ -28,8 +28,6 @@ void front_end_params::register_params(ini_params & p) { p.register_int_param("ENGINE", 0, 2, reinterpret_cast(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, diff --git a/src/front_end_params/front_end_params.h b/src/front_end_params/front_end_params.h index d13c01076..cd582e28a 100644 --- a/src/front_end_params/front_end_params.h +++ b/src/front_end_params/front_end_params.h @@ -41,7 +41,6 @@ struct front_end_params : public preprocessor_params, public spc_params, public { ref 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),