diff --git a/src/tactic/bv/CMakeLists.txt b/src/tactic/bv/CMakeLists.txt
index 9009e6fa5..d5920b88e 100644
--- a/src/tactic/bv/CMakeLists.txt
+++ b/src/tactic/bv/CMakeLists.txt
@@ -4,7 +4,6 @@ z3_add_component(bv_tactics
     bit_blaster_tactic.cpp
     bv1_blaster_tactic.cpp
     bvarray2uf_rewriter.cpp
-    bvarray2uf_tactic.cpp
     bv_bound_chk_tactic.cpp
     bv_bounds_tactic.cpp
     bv_size_reduction_tactic.cpp
diff --git a/src/tactic/bv/bvarray2uf_tactic.h b/src/tactic/bv/bvarray2uf_tactic.h
index c5d4d3a03..d71752853 100644
--- a/src/tactic/bv/bvarray2uf_tactic.h
+++ b/src/tactic/bv/bvarray2uf_tactic.h
@@ -32,15 +32,14 @@ Tactic that rewrites bit-vector arrays into bit-vector
 #pragma once
 
 #include "util/params.h"
+#include "tactic/tactic.h"
 #include "tactic/dependent_expr_state_tactic.h"
 #include "tactic/bv/bvarray2uf_simplifier.h"
 
 class ast_manager;
 class tactic;
 
-tactic * mk_bvarray2uf_tactic(ast_manager & m, params_ref const & p = params_ref());
-
-inline tactic * mk_bvarray2uf2_tactic(ast_manager & m, params_ref const & p = params_ref()) {
+inline tactic * mk_bvarray2uf_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(bvarray2uf_simplifier, m, p, s);
@@ -49,7 +48,6 @@ inline tactic * mk_bvarray2uf2_tactic(ast_manager & m, params_ref const & p = pa
 
 /*
     ADD_TACTIC("bvarray2uf", "Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.", "mk_bvarray2uf_tactic(m, p)")
-    ADD_TACTIC("bvarray2uf2", "Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.", "mk_bvarray2uf2_tactic(m, p)")
     ADD_SIMPLIFIER("bvarray2uf", "Rewrite bit-vector arrays into bit-vector (uninterpreted) functions.", "alloc(bvarray2uf_simplifier, m, p, s)")
 */