diff --git a/src/front_end_params/front_end_params.cpp b/src/front_end_params/front_end_params.cpp
index b445f0ba8..7aea7e7ee 100644
--- a/src/front_end_params/front_end_params.cpp
+++ b/src/front_end_params/front_end_params.cpp
@@ -25,8 +25,6 @@ void front_end_params::register_params(ini_params & p) {
     parser_params::register_params(p);
     arith_simplifier_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/model_params.cpp b/src/front_end_params/model_params.cpp
index ca3693c97..df6420b7a 100644
--- a/src/front_end_params/model_params.cpp
+++ b/src/front_end_params/model_params.cpp
@@ -21,7 +21,6 @@ Revision History:
 
 void model_params::register_params(ini_params & p) {
     p.register_bool_param("MODEL_PARTIAL", m_model_partial, "enable/disable partial function interpretations", true);
-    p.register_bool_param("MODEL_HIDE_UNUSED_PARTITIONS", m_model_hide_unused_partitions, "hide unused partitions, some partitions are associated with internal terms/formulas created by Z3", true);
     p.register_bool_param("MODEL_V1", m_model_v1_pp, 
                           "use Z3 version 1.x pretty printer", true);
     p.register_bool_param("MODEL_V2", m_model_v2_pp, 
@@ -30,8 +29,7 @@ void model_params::register_params(ini_params & p) {
                           "try to compact function graph (i.e., function interpretations that are lookup tables", true);
     p.register_bool_param("MODEL_COMPLETION", m_model_completion, 
                           "assigns an interptetation to symbols that do not have one in the current model, when evaluating expressions in the current model", true);
-    p.register_bool_param("MODEL_DISPLAY_ARG_SORT", m_model_display_arg_sort, 
-                          "display the sort of each argument when printing function interpretations", true);
+
 }
 
 
diff --git a/src/front_end_params/model_params.h b/src/front_end_params/model_params.h
index 9ab351a6c..2718d4e5f 100644
--- a/src/front_end_params/model_params.h
+++ b/src/front_end_params/model_params.h
@@ -23,21 +23,17 @@ Revision History:
 
 struct model_params {
     bool m_model_partial;
-    bool m_model_hide_unused_partitions;
     bool m_model_compact;
     bool m_model_v1_pp;
     bool m_model_v2_pp;
     bool m_model_completion;
-    bool m_model_display_arg_sort;
 
     model_params():
         m_model_partial(false),
-        m_model_hide_unused_partitions(true),
         m_model_compact(false),
         m_model_v1_pp(false),
         m_model_v2_pp(false),
-        m_model_completion(false),
-        m_model_display_arg_sort(true) {
+        m_model_completion(false) {
     }
 
     void register_params(ini_params & p);
diff --git a/src/front_end_params/pattern_inference_params.cpp b/src/front_end_params/pattern_inference_params.cpp
index 38fc24dca..176fdd8c2 100644
--- a/src/front_end_params/pattern_inference_params.cpp
+++ b/src/front_end_params/pattern_inference_params.cpp
@@ -21,7 +21,7 @@ Revision History:
 void pattern_inference_params::register_params(ini_params & p) {
     p.register_unsigned_param("PI_MAX_MULTI_PATTERNS", m_pi_max_multi_patterns, 
                               "when patterns are not provided, the prover uses a heuristic to infer them. This option sets the threshold on the number of extra multi-patterns that can be created. By default, the prover creates at most one multi-pattern when there is no unary pattern");
-    p.register_bool_param("PI_BLOCK_LOOOP_PATTERNS", m_pi_block_loop_patterns,
+    p.register_bool_param("PI_BLOCK_LOOP_PATTERNS", m_pi_block_loop_patterns,
                           "block looping patterns during pattern inference");
     p.register_int_param("PI_ARITH", 0, 2, reinterpret_cast<int&>(m_pi_arith), 
                          "0 - do not infer patterns with arithmetic terms, 1 - use patterns with arithmetic terms if there is no other pattern, 2 - always use patterns with arithmetic terms.");
diff --git a/src/front_end_params/preprocessor_params.h b/src/front_end_params/preprocessor_params.h
index d2ba0bd43..4b32feb60 100644
--- a/src/front_end_params/preprocessor_params.h
+++ b/src/front_end_params/preprocessor_params.h
@@ -39,7 +39,6 @@ struct preprocessor_params : public nnf_params, public cnf_params, public patter
     bool            m_pull_nested_quantifiers;
     bool            m_eliminate_term_ite;
     bool            m_eliminate_and; // represent (and a b) as (not (or (not a) (not b)))
-    bool            m_reverse_implies; // translate (implies a b) into (or b (not a))
     bool            m_macro_finder;
     bool            m_propagate_values;
     bool            m_propagate_booleans;