diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
index 2d466c3cd..473be8aae 100644
--- a/RELEASE_NOTES.md
+++ b/RELEASE_NOTES.md
@@ -20,6 +20,13 @@ Version 4.12.2
   benchmarks created by converting bit-vector semantics to integer 
   reasoning.
 - change API function Z3_mk_real to take two int64 as arguments instead of int.
+- Add _simplifiers_ as optional incremental pre-processing to solvers.
+  They are exposed over the SMTLIB API using the command [`set-simplifier`](https://microsoft.github.io/z3guide/docs/strategies/simplifiers).
+  Simplifiers are similar to tactics, but they operate on solver state that can be incrementally updated. 
+  The exposed simplifiers cover all the pre-processing techniques used internally with some additional simplifiers, such as `solve-eqs`
+  and `elim-predicates` that go beyond incremental pre-processing used internally. The advantage of using `solve-eqs` during pre-processing
+  can be significant. Incremental pre-processing simplification using `solve-eqs` and other simplifiers that change interpretations 
+  was not possible before.
 
 Version 4.12.1
 ==============
diff --git a/doc/mk_tactic_doc.py b/doc/mk_tactic_doc.py
index 86e32aa18..e82573134 100644
--- a/doc/mk_tactic_doc.py
+++ b/doc/mk_tactic_doc.py
@@ -65,7 +65,6 @@ def extract_simplifier_doc(ous, f):
             m = is_simplifier.search(line)
             if m:
                 generate_simplifier_doc(ous, m.group(1), m.group(2))
-                return
 
 def find_tactic_name(path):
     with open(path) as ins:
@@ -76,7 +75,16 @@ def find_tactic_name(path):
     print(f"no tactic in {path}")
     return ""
 
-def presort_files():
+def find_simplifier_name(path):
+    with open(path) as ins:
+        for line in ins:
+            m = is_simplifier.search(line)
+            if m:
+                return m.group(1)
+    print(f"no simplifier in {path}")
+    return ""
+
+def presort_files(find_fn):
     tac_files = []
     for root, dirs, files in os.walk(doc_path("../src")):
         for f in files:
@@ -84,16 +92,16 @@ def presort_files():
                 continue
             if f.endswith("tactic.h") or "simplifiers" in root:
                 tac_files += [(f, os.path.join(root, f))]
-    tac_files = sorted(tac_files, key = lambda x: find_tactic_name(x[1]))
+    tac_files = sorted(tac_files, key = lambda x: find_fn(x[1]))
     return tac_files
     
     
 def help(ous):
     ous.write("---\n")
     ous.write("title: Tactics Summary\n")
-    ous.write("sidebar_position: 5\n")
+    ous.write("sidebar_position: 6\n")
     ous.write("---\n")
-    tac_files = presort_files()
+    tac_files = presort_files(find_tactic_name)
     for file, path in tac_files:
         extract_tactic_doc(ous, path)
 
@@ -101,10 +109,10 @@ def help(ous):
 
 def help_simplifier(ous):
     ous.write("---\n")
-    ous.write("title: Simplifier Summary\n")
-    ous.write("sidebar_position: 6\n")
+    ous.write("title: Simplifiers Summary\n")
+    ous.write("sidebar_position: 7\n")
     ous.write("---\n")
-    tac_files = presort_files()
+    tac_files = presort_files(find_simplifier_name)
     for file, path in tac_files:
         extract_simplifier_doc(ous, path)
 
diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py
index e242fa443..bb6d884e6 100644
--- a/scripts/mk_genfile_common.py
+++ b/scripts/mk_genfile_common.py
@@ -743,7 +743,7 @@ def mk_install_tactic_cpp_internal(h_files_full_path, path):
     # First pass will just generate the tactic factories
     fout.write('#define ADD_TACTIC_CMD(NAME, DESCR, CODE) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, [](ast_manager &m, const params_ref &p) { return CODE; }))\n')
     fout.write('#define ADD_PROBE(NAME, DESCR, PROBE) ctx.insert(alloc(probe_info, symbol(NAME), DESCR, PROBE))\n')
-    fout.write('#define ADD_SIMPLIFIER_CMD(NAME, DESCR, FUNCTION) ctx.insert(alloc(simplifier_cmd, symbol(NAME), DESCR, FUNCTION))\n')
+    fout.write('#define ADD_SIMPLIFIER_CMD(NAME, DESCR, CODE) ctx.insert(alloc(simplifier_cmd, symbol(NAME), DESCR, [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return CODE; }))\n')
     fout.write('void install_tactics(tactic_manager & ctx) {\n')
     for data in ADD_TACTIC_DATA:
         fout.write('  ADD_TACTIC_CMD("%s", "%s", %s);\n' % data)
diff --git a/src/api/api_qe.cpp b/src/api/api_qe.cpp
index 328b1f249..94067135f 100644
--- a/src/api/api_qe.cpp
+++ b/src/api/api_qe.cpp
@@ -25,7 +25,7 @@ Notes:
 #include "api/api_model.h"
 #include "api/api_ast_map.h"
 #include "api/api_ast_vector.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "muz/spacer/spacer_util.h"
 
 extern "C"
diff --git a/src/ast/simplifiers/CMakeLists.txt b/src/ast/simplifiers/CMakeLists.txt
index e30224402..2affb793b 100644
--- a/src/ast/simplifiers/CMakeLists.txt
+++ b/src/ast/simplifiers/CMakeLists.txt
@@ -31,6 +31,11 @@ z3_add_component(simplifiers
     substitution
   TACTIC_HEADERS
     bit_blaster.h
+    bit2int.h
+    elim_bounds.h
+    elim_term_ite.h
+    pull_nested_quantifiers.h
+    push_ite.h
+    refine_inj_axiom.h
     rewriter_simplifier.h
-
 )
diff --git a/src/ast/simplifiers/bit2int.h b/src/ast/simplifiers/bit2int.h
index 64c7f3ecf..b899e6b58 100644
--- a/src/ast/simplifiers/bit2int.h
+++ b/src/ast/simplifiers/bit2int.h
@@ -42,3 +42,6 @@ public:
     bool supports_proofs() const override { return true; }
 };
 
+/*
+  ADD_SIMPLIFIER("bit2int", "simplify bit2int expressions.", "alloc(bit2int_simplifier, m, p, s)")
+ */
diff --git a/src/ast/simplifiers/bit_blaster.h b/src/ast/simplifiers/bit_blaster.h
index 820431706..e9f219848 100644
--- a/src/ast/simplifiers/bit_blaster.h
+++ b/src/ast/simplifiers/bit_blaster.h
@@ -33,7 +33,7 @@ public:
         m_rewriter(m, p) {
         updt_params(p);
     }
-    char const* name() const override { return "bit-blaster"; }
+    char const* name() const override { return "bit-blast"; }
     void updt_params(params_ref const & p) override;
     void collect_param_descrs(param_descrs & r) override;
     void reduce() override;
@@ -50,5 +50,5 @@ public:
 };
 
 /*
-  ADD_SIMPLIFIER("bit-blaster", "reduce bit-vector expressions into SAT.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(bit_blaster_simplifier, m, p, s); }")
+  ADD_SIMPLIFIER("bit-blast", "reduce bit-vector expressions into SAT.", "alloc(bit_blaster_simplifier, m, p, s)")
 */
diff --git a/src/ast/simplifiers/elim_bounds.h b/src/ast/simplifiers/elim_bounds.h
index ed93faeba..17a4290e2 100644
--- a/src/ast/simplifiers/elim_bounds.h
+++ b/src/ast/simplifiers/elim_bounds.h
@@ -43,3 +43,6 @@ public:
     }
 };
 
+/*
+  ADD_SIMPLIFIER("cheap-fourier-motzkin", "eliminate variables from quantifiers using partial Fourier-Motzkin elimination.", "alloc(elim_bounds_simplifier, m, p, s)")
+ */
diff --git a/src/ast/simplifiers/elim_term_ite.h b/src/ast/simplifiers/elim_term_ite.h
index 1b8f58f9e..10f039279 100644
--- a/src/ast/simplifiers/elim_term_ite.h
+++ b/src/ast/simplifiers/elim_term_ite.h
@@ -49,3 +49,6 @@ public:
     void pop(unsigned n) override { m_rewriter.pop(n); m_df.pop(n); dependent_expr_simplifier::pop(n); }
 };
 
+/*
+  ADD_SIMPLIFIER("elim-term-ite", "eliminate if-then-else term by hoisting them top top-level.", "alloc(elim_term_ite_simplifier, m, p, s)")
+*/
diff --git a/src/ast/simplifiers/pull_nested_quantifiers.h b/src/ast/simplifiers/pull_nested_quantifiers.h
index fac605d49..f41d4282b 100644
--- a/src/ast/simplifiers/pull_nested_quantifiers.h
+++ b/src/ast/simplifiers/pull_nested_quantifiers.h
@@ -46,3 +46,7 @@ public:
 
     bool supports_proofs() const override { return true; }
 };
+
+/*
+  ADD_SIMPLIFIER("pull-nested-quantifiers", "pull nested quantifiers to top-level.", "alloc(pull_nested_quantifiers_simplifier, m, p, s)")
+*/
diff --git a/src/ast/simplifiers/push_ite.h b/src/ast/simplifiers/push_ite.h
index 8e508bf53..f0db764a0 100644
--- a/src/ast/simplifiers/push_ite.h
+++ b/src/ast/simplifiers/push_ite.h
@@ -64,3 +64,9 @@ public:
     }
 };
 
+/*
+  ADD_SIMPLIFIER("push-app-ite-conservative", "Push functions over if-then else.", "alloc(push_ite_simplifier, m, p, s, true)")
+  ADD_SIMPLIFIER("push-app-ite", "Push functions over if-then else.", "alloc(push_ite_simplifier, m, p, s, false)")
+  ADD_SIMPLIFIER("ng-push-app-ite-conservative", "Push functions over if-then-else within non-ground terms only.", "alloc(ng_push_ite_simplifier, m, p, s, true)")
+  ADD_SIMPLIFIER("ng-push-app-ite", "Push functions over if-then-else within non-ground terms only.", "alloc(ng_push_ite_simplifier, m, p, s, false)")
+*/
diff --git a/src/ast/simplifiers/refine_inj_axiom.h b/src/ast/simplifiers/refine_inj_axiom.h
index 53c960812..35128f3d9 100644
--- a/src/ast/simplifiers/refine_inj_axiom.h
+++ b/src/ast/simplifiers/refine_inj_axiom.h
@@ -42,3 +42,7 @@ public:
         }
     }
 };
+
+/*
+  ADD_SIMPLIFIER("refine-injectivity", "refine injectivity axioms.", "alloc(refine_inj_axiom_simplifier, m, p, s)")
+*/
diff --git a/src/ast/simplifiers/rewriter_simplifier.h b/src/ast/simplifiers/rewriter_simplifier.h
index f74c213d4..7ae409df0 100644
--- a/src/ast/simplifiers/rewriter_simplifier.h
+++ b/src/ast/simplifiers/rewriter_simplifier.h
@@ -55,5 +55,5 @@ public:
 };
 
 /*
-  ADD_SIMPLIFIER("simplify", "apply simplification rules.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(rewriter_simplifier, m, p, s); }")
+  ADD_SIMPLIFIER("simplify", "apply simplification rules.", "alloc(rewriter_simplifier, m, p, s)")
  */
diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h
index 60b2bbe8f..0a8fd955c 100644
--- a/src/muz/base/dl_rule.h
+++ b/src/muz/base/dl_rule.h
@@ -28,7 +28,7 @@ Revision History:
 #include "ast/rewriter/ast_counter.h"
 #include "ast/rewriter/rewriter.h"
 #include "muz/base/hnf.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "ast/rewriter/var_subst.h"
 #include "ast/datatype_decl_plugin.h"
 #include "ast/rewriter/label_rewriter.h"
diff --git a/src/muz/spacer/spacer_legacy_mbp.cpp b/src/muz/spacer/spacer_legacy_mbp.cpp
index 324368cec..0f49381c1 100644
--- a/src/muz/spacer/spacer_legacy_mbp.cpp
+++ b/src/muz/spacer/spacer_legacy_mbp.cpp
@@ -35,7 +35,7 @@ Notes:
 #include "ast/rewriter/expr_replacer.h"
 #include "model/model_smt2_pp.h"
 #include "ast/scoped_proof.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "muz/spacer/spacer_qe_project.h"
 #include "model/model_pp.h"
 #include "ast/rewriter/expr_safe_replace.h"
diff --git a/src/muz/spacer/spacer_legacy_mev.cpp b/src/muz/spacer/spacer_legacy_mev.cpp
index e6da53e32..a0c95fbd9 100644
--- a/src/muz/spacer/spacer_legacy_mev.cpp
+++ b/src/muz/spacer/spacer_legacy_mev.cpp
@@ -23,7 +23,7 @@ Copyright (c) 2017 Arie Gurfinkel
 #include "ast/rewriter/expr_replacer.h"
 #include "model/model_smt2_pp.h"
 #include "ast/scoped_proof.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "muz/spacer/spacer_qe_project.h"
 #include "model/model_pp.h"
 #include "ast/rewriter/expr_safe_replace.h"
diff --git a/src/muz/spacer/spacer_qe_project.cpp b/src/muz/spacer/spacer_qe_project.cpp
index b170a59d0..e52e909ae 100644
--- a/src/muz/spacer/spacer_qe_project.cpp
+++ b/src/muz/spacer/spacer_qe_project.cpp
@@ -36,7 +36,7 @@ Revision History:
 #include "model/model_pp.h"
 
 #include "qe/qe.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 
 #include "muz/spacer/spacer_mev_array.h"
 #include "muz/spacer/spacer_qe_project.h"
diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index bc9224771..4e1da5770 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -51,7 +51,7 @@ Notes:
 #include "model/model_smt2_pp.h"
 #include "smt/params/smt_params.h"
 
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "qe/mbp/mbp_plugin.h"
 #include "qe/mbp/mbp_term_graph.h"
 #include "qe/qe_mbp.h"
diff --git a/src/muz/tab/tab_context.cpp b/src/muz/tab/tab_context.cpp
index b8ca9babb..f65661e9e 100644
--- a/src/muz/tab/tab_context.cpp
+++ b/src/muz/tab/tab_context.cpp
@@ -23,7 +23,7 @@ Revision History:
 #include "muz/base/dl_context.h"
 #include "muz/transforms/dl_mk_rule_inliner.h"
 #include "smt/smt_kernel.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "ast/rewriter/bool_rewriter.h"
 #include "ast/rewriter/th_rewriter.h"
 #include "ast/datatype_decl_plugin.h"
diff --git a/src/qe/lite/CMakeLists.txt b/src/qe/lite/CMakeLists.txt
index 27f9bb09d..fc942d4ae 100644
--- a/src/qe/lite/CMakeLists.txt
+++ b/src/qe/lite/CMakeLists.txt
@@ -1,9 +1,9 @@
 z3_add_component(qe_lite
   SOURCES
-    qe_lite.cpp
+    qe_lite_tactic.cpp
   COMPONENT_DEPENDENCIES
     tactic
     mbp
   TACTIC_HEADERS
-    qe_lite.h
+    qe_lite_tactic.h
 )
diff --git a/src/qe/lite/qe_lite.cpp b/src/qe/lite/qe_lite_tactic.cpp
similarity index 99%
rename from src/qe/lite/qe_lite.cpp
rename to src/qe/lite/qe_lite_tactic.cpp
index 90ea35769..32d11786c 100644
--- a/src/qe/lite/qe_lite.cpp
+++ b/src/qe/lite/qe_lite_tactic.cpp
@@ -34,7 +34,7 @@ Revision History:
 #include "ast/datatype_decl_plugin.h"
 #include "tactic/tactical.h"
 #include "qe/mbp/mbp_solve_plugin.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "tactic/dependent_expr_state_tactic.h"
 
 
@@ -2444,9 +2444,9 @@ namespace {
 }
 
 tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p) {
-    return alloc(dependent_expr_state_tactic, m, p, mk_qe_lite_simplifer);
+    return alloc(dependent_expr_state_tactic, m, p, mk_qe_lite_simplifier);
 }
 
-dependent_expr_simplifier* mk_qe_lite_simplifer(ast_manager& m, params_ref const& p, dependent_expr_state& st) {
+dependent_expr_simplifier* mk_qe_lite_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& st) {
     return alloc(qe_lite_simplifier, m, p, st);
 }
diff --git a/src/qe/lite/qe_lite.h b/src/qe/lite/qe_lite_tactic.h
similarity index 89%
rename from src/qe/lite/qe_lite.h
rename to src/qe/lite/qe_lite_tactic.h
index 9a4d4c0f6..07ce60f35 100644
--- a/src/qe/lite/qe_lite.h
+++ b/src/qe/lite/qe_lite_tactic.h
@@ -68,8 +68,10 @@ public:
 };
 
 tactic * mk_qe_lite_tactic(ast_manager & m, params_ref const & p = params_ref());
+
+dependent_expr_simplifier* mk_qe_lite_simplifier(ast_manager& m, params_ref const& p, dependent_expr_state& st);
+
 /*
   ADD_TACTIC("qe-light", "apply light-weight quantifier elimination.", "mk_qe_lite_tactic(m, p)")
+  ADD_SIMPLIFIER("qe-light", "apply light-weight quantifier elimination.", "mk_qe_lite_simplifier(m, p, s)")
 */
-
-dependent_expr_simplifier* mk_qe_lite_simplifer(ast_manager& m, params_ref const& p, dependent_expr_state& st);
diff --git a/src/qe/qe_mbp.cpp b/src/qe/qe_mbp.cpp
index 6b0e3cf32..9f5d9063c 100644
--- a/src/qe/qe_mbp.cpp
+++ b/src/qe/qe_mbp.cpp
@@ -30,7 +30,7 @@ Revision History:
 #include "qe/mbp/mbp_arith.h"
 #include "qe/mbp/mbp_arrays.h"
 #include "qe/mbp/mbp_datatypes.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "model/model_pp.h"
 #include "model/model_evaluator.h"
 
diff --git a/src/sat/smt/q_solver.cpp b/src/sat/smt/q_solver.cpp
index 26c99180b..fff11898c 100644
--- a/src/sat/smt/q_solver.cpp
+++ b/src/sat/smt/q_solver.cpp
@@ -23,7 +23,7 @@ Author:
 #include "sat/smt/q_solver.h"
 #include "sat/smt/euf_solver.h"
 #include "sat/smt/sat_th.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include <iostream>
 
 
diff --git a/src/solver/assertions/asserted_formulas.h b/src/solver/assertions/asserted_formulas.h
index c4da97704..481af58b7 100644
--- a/src/solver/assertions/asserted_formulas.h
+++ b/src/solver/assertions/asserted_formulas.h
@@ -38,7 +38,7 @@ Revision History:
 #include "ast/normal_forms/elim_term_ite.h"
 #include "ast/pattern/pattern_inference.h"
 #include "smt/params/smt_params.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 
 
 class asserted_formulas {
diff --git a/src/solver/solver_preprocess.cpp b/src/solver/solver_preprocess.cpp
index 71c6d975a..38b0584b5 100644
--- a/src/solver/solver_preprocess.cpp
+++ b/src/solver/solver_preprocess.cpp
@@ -42,7 +42,7 @@ Notes:
 #include "ast/simplifiers/cnf_nnf.h"
 #include "smt/params/smt_params.h"
 #include "solver/solver_preprocess.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 
 void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dependent_expr_state& st) {
 
@@ -53,7 +53,7 @@ void init_preprocess(ast_manager& m, params_ref const& p, seq_simplifier& s, dep
     if (smtp.m_elim_unconstrained) s.add_simplifier(alloc(elim_unconstrained, m, st));
     if (smtp.m_nnf_cnf) s.add_simplifier(alloc(cnf_nnf_simplifier, m, p, st));
     if (smtp.m_macro_finder || smtp.m_quasi_macros) s.add_simplifier(alloc(eliminate_predicates, m, st));
-    if (smtp.m_qe_lite) s.add_simplifier(mk_qe_lite_simplifer(m, p, st));
+    if (smtp.m_qe_lite) s.add_simplifier(mk_qe_lite_simplifier(m, p, st));
     if (smtp.m_pull_nested_quantifiers) s.add_simplifier(alloc(pull_nested_quantifiers_simplifier, m, p, st));
     if (smtp.m_max_bv_sharing) s.add_simplifier(mk_max_bv_sharing(m, p, st));
     if (smtp.m_refine_inj_axiom) s.add_simplifier(alloc(refine_inj_axiom_simplifier, m, p, st));
diff --git a/src/tactic/arith/bound_simplifier_tactic.h b/src/tactic/arith/bound_simplifier_tactic.h
index 5451caa20..b61a10004 100644
--- a/src/tactic/arith/bound_simplifier_tactic.h
+++ b/src/tactic/arith/bound_simplifier_tactic.h
@@ -38,5 +38,5 @@ inline tactic* mk_bound_simplifier_tactic(ast_manager& m, params_ref const& p =
 
 /*
   ADD_TACTIC("bound-simplifier", "Simplify arithmetical expressions modulo bounds.", "mk_bound_simplifier_tactic(m, p)")
-  ADD_SIMPLIFIER("bound-simplifier", "Simplify arithmetical expressions modulo bounds.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(bound_simplifier, m, p, s); }")
+  ADD_SIMPLIFIER("bound-simplifier", "Simplify arithmetical expressions modulo bounds.", "alloc(bound_simplifier, m, p, s)")
 */
diff --git a/src/tactic/arith/card2bv_tactic.h b/src/tactic/arith/card2bv_tactic.h
index 032e964f9..c84b1b04e 100644
--- a/src/tactic/arith/card2bv_tactic.h
+++ b/src/tactic/arith/card2bv_tactic.h
@@ -69,5 +69,5 @@ inline tactic* mk_card2bv_tactic(ast_manager& m, params_ref const& p = params_re
 
 /*
   ADD_TACTIC("card2bv", "convert pseudo-boolean constraints to bit-vectors.", "mk_card2bv_tactic(m, p)")
-  ADD_SIMPLIFIER("card2bv", "convert pseudo-boolean constraints to bit-vectors.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(card2bv, m, p, s); }")
+  ADD_SIMPLIFIER("card2bv", "convert pseudo-boolean constraints to bit-vectors.", "alloc(card2bv, m, p, s)")
 */
diff --git a/src/tactic/arith/propagate_ineqs_tactic.h b/src/tactic/arith/propagate_ineqs_tactic.h
index 68156c410..706276fd7 100644
--- a/src/tactic/arith/propagate_ineqs_tactic.h
+++ b/src/tactic/arith/propagate_ineqs_tactic.h
@@ -64,6 +64,6 @@ inline tactic* mk_propagate_ineqs_tactic(ast_manager& m, params_ref const& p = p
 
 /*
   ADD_TACTIC("propagate-ineqs", "propagate ineqs/bounds, remove subsumed inequalities.", "mk_propagate_ineqs_tactic(m, p)")
-  ADD_SIMPLIFIER("propagate-ineqs", "propagate ineqs/bounds, remove subsumed inequalities.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(bound_simplifier, m, p, s); }")
+  ADD_SIMPLIFIER("propagate-ineqs", "propagate ineqs/bounds, remove subsumed inequalities.", "alloc(bound_simplifier, m, p, s)")
 */
 
diff --git a/src/tactic/bv/CMakeLists.txt b/src/tactic/bv/CMakeLists.txt
index 50dd941e0..9009e6fa5 100644
--- a/src/tactic/bv/CMakeLists.txt
+++ b/src/tactic/bv/CMakeLists.txt
@@ -8,7 +8,6 @@ z3_add_component(bv_tactics
     bv_bound_chk_tactic.cpp
     bv_bounds_tactic.cpp
     bv_size_reduction_tactic.cpp
-    bv_slice_tactic.cpp
     dt2bv_tactic.cpp
     elim_small_bv_tactic.cpp
   COMPONENT_DEPENDENCIES
diff --git a/src/tactic/bv/bv_bounds_tactic.h b/src/tactic/bv/bv_bounds_tactic.h
index eb75ceca7..453f6d27f 100644
--- a/src/tactic/bv/bv_bounds_tactic.h
+++ b/src/tactic/bv/bv_bounds_tactic.h
@@ -46,7 +46,7 @@ tactic * mk_dom_bv_bounds_tactic(ast_manager & m, params_ref const & p = params_
 /*
   ADD_TACTIC("propagate-bv-bounds", "propagate bit-vector bounds by simplifying implied or contradictory bounds.", "mk_bv_bounds_tactic(m, p)")
 
-  ADD_SIMPLIFIER("propagate-bv-bounds", "propagate bit-vector bounds by simplifying implied or contradictory bounds.", "mk_bv_bounds_simplifier")
+  ADD_SIMPLIFIER("propagate-bv-bounds", "propagate bit-vector bounds by simplifying implied or contradictory bounds.", "mk_bv_bounds_simplifier(m, p, s)")
 
   ADD_TACTIC("propagate-bv-bounds2", "propagate bit-vector bounds by simplifying implied or contradictory bounds.", "mk_dom_bv_bounds_tactic(m, p)")
 
diff --git a/src/tactic/bv/bv_slice_tactic.cpp b/src/tactic/bv/bv_slice_tactic.cpp
index d470f6e72..bb3d437d9 100644
--- a/src/tactic/bv/bv_slice_tactic.cpp
+++ b/src/tactic/bv/bv_slice_tactic.cpp
@@ -15,12 +15,4 @@ Author:
 
 --*/
 
-#include "ast/simplifiers/bv_slice.h"
-#include "tactic/tactic.h"
-#include "tactic/dependent_expr_state_tactic.h"
-#include "tactic/bv/bv_slice_tactic.h"
 
-tactic* mk_bv_slice_tactic(ast_manager& m, params_ref const& p) {
-    return alloc(dependent_expr_state_tactic, m, p,
-                 [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(bv::slice, m, s); });
-}
diff --git a/src/tactic/bv/bv_slice_tactic.h b/src/tactic/bv/bv_slice_tactic.h
index 77ff081d8..b16aa4c7c 100644
--- a/src/tactic/bv/bv_slice_tactic.h
+++ b/src/tactic/bv/bv_slice_tactic.h
@@ -45,13 +45,22 @@ simplification
 #pragma once
 
 #include "util/params.h"
+#include "tactic/tactic.h"
+#include "tactic/dependent_expr_state_tactic.h"
+#include "ast/simplifiers/bv_slice.h"
+
 class ast_manager;
 class tactic;
 
-tactic * mk_bv_slice_tactic(ast_manager & m, params_ref const & p = params_ref());
+inline tactic* mk_bv_slice_tactic(ast_manager& m, params_ref const& p = params_ref()) {
+    return alloc(dependent_expr_state_tactic, m, p,
+                 [](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(bv::slice, m, s); });
+}
+
 
 /*
   ADD_TACTIC("bv-slice", "simplify using bit-vector slices.", "mk_bv_slice_tactic(m, p)")
+  ADD_SIMPLIFIER("bv-slice", "simplify using bit-vector slices.", "alloc(bv::slice, m, s)")
 */
 
 
diff --git a/src/tactic/core/demodulator_tactic.h b/src/tactic/core/demodulator_tactic.h
index 507b4e5c5..31916a71e 100644
--- a/src/tactic/core/demodulator_tactic.h
+++ b/src/tactic/core/demodulator_tactic.h
@@ -100,5 +100,5 @@ inline tactic * mk_demodulator_tactic(ast_manager& m, params_ref const& p = para
 
 /*
   ADD_TACTIC("demodulator", "extracts equalities from quantifiers and applies them to simplify.", "mk_demodulator_tactic(m, p)")
-  ADD_SIMPLIFIER("demodulator", "extracts equalities from quantifiers and applies them to simplify.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(demodulator_simplifier, m, p, s); }")
+  ADD_SIMPLIFIER("demodulator", "extracts equalities from quantifiers and applies them to simplify.", "alloc(demodulator_simplifier, m, p, s)")
 */
diff --git a/src/tactic/core/distribute_forall_tactic.h b/src/tactic/core/distribute_forall_tactic.h
index 419eba71e..dea009311 100644
--- a/src/tactic/core/distribute_forall_tactic.h
+++ b/src/tactic/core/distribute_forall_tactic.h
@@ -50,6 +50,6 @@ inline tactic * mk_distribute_forall_tactic(ast_manager& m, params_ref const& p
 
 /*
   ADD_TACTIC("distribute-forall", "distribute forall over conjunctions.", "mk_distribute_forall_tactic(m, p)")
-  ADD_SIMPLIFIER("distribute-forall", "distribute forall over conjunctions.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(distribute_forall_simplifier, m, p, s); }")
+  ADD_SIMPLIFIER("distribute-forall", "distribute forall over conjunctions.", "alloc(distribute_forall_simplifier, m, p, s)")
 */
 
diff --git a/src/tactic/core/dom_simplify_tactic.h b/src/tactic/core/dom_simplify_tactic.h
index 795db0f26..349c96b49 100644
--- a/src/tactic/core/dom_simplify_tactic.h
+++ b/src/tactic/core/dom_simplify_tactic.h
@@ -56,6 +56,6 @@ inline tactic* mk_dom_simplify_tactic(ast_manager& m, params_ref const& p) {
 
 /*
 ADD_TACTIC("dom-simplify", "apply dominator simplification rules.", "mk_dom_simplify_tactic(m, p)")
-ADD_SIMPLIFIER("dom-simplify", "apply dominator simplification rules.", "[](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* { return alloc(dominator_simplifier, m, s, mk_expr_substitution_simplifier(m), p); }")
+ADD_SIMPLIFIER("dom-simplify", "apply dominator simplification rules.", "alloc(dominator_simplifier, m, s, mk_expr_substitution_simplifier(m), p)")
 */
 
diff --git a/src/tactic/core/elim_uncnstr2_tactic.h b/src/tactic/core/elim_uncnstr2_tactic.h
index fc249da64..a07833058 100644
--- a/src/tactic/core/elim_uncnstr2_tactic.h
+++ b/src/tactic/core/elim_uncnstr2_tactic.h
@@ -118,5 +118,5 @@ inline tactic * mk_elim_uncnstr2_tactic(ast_manager & m, params_ref const & p =
 
 /*
   ADD_TACTIC("elim-uncnstr2", "eliminate unconstrained variables.", "mk_elim_uncnstr2_tactic(m, p)")
-  ADD_SIMPLIFIER("elim-unconstrained", "eliminate unconstrained variables.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(elim_unconstrained, m, s); }")
+  ADD_SIMPLIFIER("elim-unconstrained", "eliminate unconstrained variables.", "alloc(elim_unconstrained, m, s)")
 */
diff --git a/src/tactic/core/eliminate_predicates_tactic.h b/src/tactic/core/eliminate_predicates_tactic.h
index b53892e8b..c2eb90742 100644
--- a/src/tactic/core/eliminate_predicates_tactic.h
+++ b/src/tactic/core/eliminate_predicates_tactic.h
@@ -63,6 +63,6 @@ inline tactic * mk_eliminate_predicates_tactic(ast_manager& m, params_ref const&
 }
 
 /*
-  ADD_TACTIC("elim-predicates", "eliminate predicates.", "mk_eliminate_predicates_tactic(m, p)")
-  ADD_SIMPLIFIER("elim-predicates", "eliminate predicates.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(eliminate_predicates, m, s); }")
+  ADD_TACTIC("elim-predicates", "eliminate predicates, macros and implicit definitions.", "mk_eliminate_predicates_tactic(m, p)")
+  ADD_SIMPLIFIER("elim-predicates", "eliminate predicates, macros and implicit definitions.", "alloc(eliminate_predicates, m, s)")
 */
diff --git a/src/tactic/core/euf_completion_tactic.h b/src/tactic/core/euf_completion_tactic.h
index a1c9166ea..cfeda5ac1 100644
--- a/src/tactic/core/euf_completion_tactic.h
+++ b/src/tactic/core/euf_completion_tactic.h
@@ -33,6 +33,9 @@ is extracted.
 #pragma once
 
 #include "util/params.h"
+#include "tactic/dependent_expr_state_tactic.h"
+#include "ast/simplifiers/euf_completion.h"
+
 class ast_manager;
 class tactic;
 
@@ -40,6 +43,7 @@ tactic * mk_euf_completion_tactic(ast_manager & m, params_ref const & p = params
 
 /*
   ADD_TACTIC("euf-completion", "simplify using equalities.", "mk_euf_completion_tactic(m, p)")
+  ADD_SIMPLIFIER("euf-completion", "simplify modulo congruence closure.", "alloc(euf::completion, m, s)")
 */
 
 
diff --git a/src/tactic/core/propagate_values2_tactic.h b/src/tactic/core/propagate_values2_tactic.h
index 466ef87a1..57e94965b 100644
--- a/src/tactic/core/propagate_values2_tactic.h
+++ b/src/tactic/core/propagate_values2_tactic.h
@@ -55,5 +55,5 @@ inline tactic * mk_propagate_values2_tactic(ast_manager & m, params_ref const &
 
 /*
   ADD_TACTIC("propagate-values2", "propagate constants.", "mk_propagate_values2_tactic(m, p)")
-  ADD_SIMPLIFIER("propagate-values", "propagate constants.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(propagate_values, m, p, s); }")
+  ADD_SIMPLIFIER("propagate-values", "propagate constants.", "alloc(propagate_values, m, p, s)")
 */
diff --git a/src/tactic/core/reduce_args_tactic.h b/src/tactic/core/reduce_args_tactic.h
index 4bfb7ed2f..eeb5bff70 100644
--- a/src/tactic/core/reduce_args_tactic.h
+++ b/src/tactic/core/reduce_args_tactic.h
@@ -79,7 +79,7 @@ inline tactic* mk_reduce_args_tactic2(ast_manager& m, params_ref const& p = para
 }
 /*
   ADD_TACTIC("reduce-args2", "reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value.", "mk_reduce_args_tactic2(m, p)")
-  ADD_SIMPLIFIER("reduce-args", "reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value.", "[](auto& m, auto& p, auto& s) -> dependent_expr_simplifier* { return mk_reduce_args_simplifier(m, s, p); }")
+  ADD_SIMPLIFIER("reduce-args", "reduce the number of arguments of function applications, when for all occurrences of a function f the i-th is a value.", "mk_reduce_args_simplifier(m, s, p)")
 
 */
 
diff --git a/src/tactic/core/solve_eqs_tactic.h b/src/tactic/core/solve_eqs_tactic.h
index af27d4576..1e0e5dc5b 100644
--- a/src/tactic/core/solve_eqs_tactic.h
+++ b/src/tactic/core/solve_eqs_tactic.h
@@ -79,5 +79,5 @@ inline tactic * mk_solve_eqs_tactic(ast_manager& m, params_ref const& p = params
 
 /*
   ADD_TACTIC("solve-eqs", "solve for variables.", "mk_solve_eqs_tactic(m, p)")
-  ADD_SIMPLIFIER("solve-eqs", "solve for variables.", "[](auto& m, auto& p, auto &s) -> dependent_expr_simplifier* { return alloc(euf::solve_eqs, m, s); }")
+  ADD_SIMPLIFIER("solve-eqs", "solve for variables.", "alloc(euf::solve_eqs, m, s)")
 */
diff --git a/src/tactic/smtlogics/nra_tactic.cpp b/src/tactic/smtlogics/nra_tactic.cpp
index e29694bc2..4f3d18c1f 100644
--- a/src/tactic/smtlogics/nra_tactic.cpp
+++ b/src/tactic/smtlogics/nra_tactic.cpp
@@ -24,7 +24,7 @@ Notes:
 #include "tactic/smtlogics/smt_tactic.h"
 #include "qe/qe_tactic.h"
 #include "qe/nlqsat.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "nlsat/tactic/qfnra_nlsat_tactic.h"
 
 tactic * mk_nra_tactic(ast_manager & m, params_ref const& p) {
diff --git a/src/tactic/smtlogics/quant_tactics.cpp b/src/tactic/smtlogics/quant_tactics.cpp
index daf020a14..38cb1690b 100644
--- a/src/tactic/smtlogics/quant_tactics.cpp
+++ b/src/tactic/smtlogics/quant_tactics.cpp
@@ -21,7 +21,7 @@ Revision History:
 #include "tactic/core/propagate_values_tactic.h"
 #include "tactic/core/solve_eqs_tactic.h"
 #include "tactic/core/elim_uncnstr_tactic.h"
-#include "qe/lite/qe_lite.h"
+#include "qe/lite/qe_lite_tactic.h"
 #include "qe/qsat.h"
 #include "tactic/core/ctx_simplify_tactic.h"
 #include "tactic/core/elim_term_ite_tactic.h"