diff --git a/src/tactic/sls/sls_tactic.cpp b/src/tactic/sls/sls_tactic.cpp
index 4e49e0d76..f4ef300e4 100644
--- a/src/tactic/sls/sls_tactic.cpp
+++ b/src/tactic/sls/sls_tactic.cpp
@@ -94,13 +94,13 @@ public:
 
 };
 
-tactic * mk_sls_tactic(ast_manager & m, params_ref const & p) {
+static tactic * mk_sls_tactic(ast_manager & m, params_ref const & p) {
     return and_then(fail_if_not(mk_is_qfbv_probe()), // Currently only QF_BV is supported.
                     clean(alloc(sls_tactic, m, p)));
 }
 
 
-tactic * mk_preamble(ast_manager & m, params_ref const & p) {
+static tactic * mk_preamble(ast_manager & m, params_ref const & p) {
     params_ref main_p;
     main_p.set_bool("elim_and", true);
     // main_p.set_bool("pull_cheap_ite", true);
diff --git a/src/tactic/smtlogics/qfbv_tactic.cpp b/src/tactic/smtlogics/qfbv_tactic.cpp
index 7cc875fba..918e0fc6d 100644
--- a/src/tactic/smtlogics/qfbv_tactic.cpp
+++ b/src/tactic/smtlogics/qfbv_tactic.cpp
@@ -32,7 +32,7 @@ Notes:
 
 #define MEMLIMIT 300
 
-tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
+static tactic * mk_qfbv_preamble(ast_manager& m, params_ref const& p) {
 
     params_ref solve_eq_p;
     // conservative guassian elimination.
@@ -80,7 +80,7 @@ static tactic * main_p(tactic* t) {
 }
 
 
-tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tactic* smt) {
+static tactic * mk_qfbv_tactic(ast_manager& m, params_ref const & p, tactic* sat, tactic* smt) {
 
     params_ref local_ctx_p = p;
     local_ctx_p.set_bool("local_ctx", true);
diff --git a/src/tactic/smtlogics/qfnia_tactic.cpp b/src/tactic/smtlogics/qfnia_tactic.cpp
index 950291221..5a71281fb 100644
--- a/src/tactic/smtlogics/qfnia_tactic.cpp
+++ b/src/tactic/smtlogics/qfnia_tactic.cpp
@@ -29,7 +29,7 @@ Notes:
 #include"ctx_simplify_tactic.h"
 #include"cofactor_term_ite_tactic.h"
 
-tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) {
+static tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) {
     params_ref p = p_ref;
     p.set_bool("flat", false);
     p.set_bool("hi_div0", true); 
@@ -51,7 +51,7 @@ tactic * mk_qfnia_bv_solver(ast_manager & m, params_ref const & p_ref) {
     return r;
 }
 
-tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) {
+static tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) {
     params_ref pull_ite_p = p_ref;
     pull_ite_p.set_bool("pull_cheap_ite", true);
     pull_ite_p.set_bool("local_ctx", true);
@@ -77,7 +77,7 @@ tactic * mk_qfnia_premable(ast_manager & m, params_ref const & p_ref) {
                  using_params(mk_simplify_tactic(m), simp_p));    
 }
 
-tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) {
+static tactic * mk_qfnia_sat_solver(ast_manager & m, params_ref const & p) {
     params_ref nia2sat_p = p;
     nia2sat_p.set_uint("nla2bv_max_bv_size", 64);   
 
diff --git a/src/tactic/ufbv/ufbv_tactic.cpp b/src/tactic/ufbv/ufbv_tactic.cpp
index 7a185c854..19d41be68 100644
--- a/src/tactic/ufbv/ufbv_tactic.cpp
+++ b/src/tactic/ufbv/ufbv_tactic.cpp
@@ -31,11 +31,11 @@ Notes:
 #include"ufbv_tactic.h"
 
 
-tactic * mk_der_fp_tactic(ast_manager & m, params_ref const & p) {
+static tactic * mk_der_fp_tactic(ast_manager & m, params_ref const & p) {
     return repeat(and_then(mk_der_tactic(m), mk_simplify_tactic(m, p)));
 }
 
-tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) {
+static tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p) {
     params_ref no_elim_and(p);
     no_elim_and.set_bool("elim_and", false);
 
diff --git a/src/tactic/ufbv/ufbv_tactic.h b/src/tactic/ufbv/ufbv_tactic.h
index 2d5454de5..300fdd84a 100644
--- a/src/tactic/ufbv/ufbv_tactic.h
+++ b/src/tactic/ufbv/ufbv_tactic.h
@@ -23,8 +23,6 @@ Notes:
 class ast_manager;
 class tactic;
 
-tactic * mk_ufbv_preprocessor_tactic(ast_manager & m, params_ref const & p = params_ref());
-
 tactic * mk_ufbv_tactic(ast_manager & m, params_ref const & p = params_ref());
 
 /*