diff --git a/src/ast/converters/CMakeLists.txt b/src/ast/converters/CMakeLists.txt
index c11b0dbe1..5343c32a2 100644
--- a/src/ast/converters/CMakeLists.txt
+++ b/src/ast/converters/CMakeLists.txt
@@ -1,8 +1,10 @@
 z3_add_component(converters
   SOURCES
+    equiv_proof_converter.cpp
+    generic_model_converter.cpp
     model_converter.cpp
     proof_converter.cpp
-    generic_model_converter.cpp
+    replace_proof_converter.cpp
   COMPONENT_DEPENDENCIES
     model
 )
diff --git a/src/tactic/equiv_proof_converter.cpp b/src/ast/converters/equiv_proof_converter.cpp
similarity index 93%
rename from src/tactic/equiv_proof_converter.cpp
rename to src/ast/converters/equiv_proof_converter.cpp
index 8bec082d3..d0ed94d8b 100644
--- a/src/tactic/equiv_proof_converter.cpp
+++ b/src/ast/converters/equiv_proof_converter.cpp
@@ -17,7 +17,7 @@ Revision History:
 
 --*/
 
-#include "tactic/equiv_proof_converter.h"
+#include "ast/converters/equiv_proof_converter.h"
 #include "ast/ast_pp.h"
 #include "ast/scoped_proof.h"
 
diff --git a/src/tactic/equiv_proof_converter.h b/src/ast/converters/equiv_proof_converter.h
similarity index 95%
rename from src/tactic/equiv_proof_converter.h
rename to src/ast/converters/equiv_proof_converter.h
index 87a8f7131..7f98d1e0c 100644
--- a/src/tactic/equiv_proof_converter.h
+++ b/src/ast/converters/equiv_proof_converter.h
@@ -23,7 +23,7 @@ Revision History:
 
 #pragma once
 
-#include "tactic/replace_proof_converter.h"
+#include "ast/converters/replace_proof_converter.h"
 
 class equiv_proof_converter : public proof_converter {
     ast_manager&            m;
diff --git a/src/tactic/replace_proof_converter.cpp b/src/ast/converters/replace_proof_converter.cpp
similarity index 97%
rename from src/tactic/replace_proof_converter.cpp
rename to src/ast/converters/replace_proof_converter.cpp
index 4a98110eb..81fe251a3 100644
--- a/src/tactic/replace_proof_converter.cpp
+++ b/src/ast/converters/replace_proof_converter.cpp
@@ -17,7 +17,7 @@ Revision History:
 
 --*/
 
-#include "tactic/replace_proof_converter.h"
+#include "ast/converters/replace_proof_converter.h"
 #include "ast/expr_functors.h"
 #include "ast/ast_pp.h"
 #include "ast/for_each_expr.h"
diff --git a/src/tactic/replace_proof_converter.h b/src/ast/converters/replace_proof_converter.h
similarity index 100%
rename from src/tactic/replace_proof_converter.h
rename to src/ast/converters/replace_proof_converter.h
diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h
index 46e0b42bf..3d5501b37 100644
--- a/src/muz/base/dl_util.h
+++ b/src/muz/base/dl_util.h
@@ -24,7 +24,7 @@ Revision History:
 #include "util/obj_hashtable.h"
 #include "util/uint_set.h"
 #include "tactic/horn_subsume_model_converter.h"
-#include "tactic/replace_proof_converter.h"
+#include "ast/converters/replace_proof_converter.h"
 #include "ast/substitution/substitution.h"
 #include "ast/rewriter/ast_counter.h"
 #include "util/statistics.h"
diff --git a/src/muz/transforms/dl_mk_array_blast.h b/src/muz/transforms/dl_mk_array_blast.h
index 6d1a69825..352c8a248 100644
--- a/src/muz/transforms/dl_mk_array_blast.h
+++ b/src/muz/transforms/dl_mk_array_blast.h
@@ -22,9 +22,9 @@ Revision History:
 #include "muz/base/dl_rule_set.h"
 #include "muz/base/dl_rule_transformer.h"
 #include "muz/transforms/dl_mk_interp_tail_simplifier.h"
-#include "tactic/equiv_proof_converter.h"
 #include "ast/array_decl_plugin.h"
 #include "ast/rewriter/expr_safe_replace.h"
+#include "ast/converters/equiv_proof_converter.h"
 
 namespace datalog {
 
diff --git a/src/muz/transforms/dl_mk_elim_term_ite.h b/src/muz/transforms/dl_mk_elim_term_ite.h
index 11bfb8f23..98acd12f1 100644
--- a/src/muz/transforms/dl_mk_elim_term_ite.h
+++ b/src/muz/transforms/dl_mk_elim_term_ite.h
@@ -21,7 +21,7 @@ Revision History:
 #include "muz/base/dl_context.h"
 #include "muz/base/dl_rule_set.h"
 #include "muz/base/dl_rule_transformer.h"
-#include "tactic/equiv_proof_converter.h"
+#include "ast/converters/equiv_proof_converter.h"
 
 namespace datalog {
     class mk_elim_term_ite : public rule_transformer::plugin {
diff --git a/src/tactic/CMakeLists.txt b/src/tactic/CMakeLists.txt
index ab81ebfe2..17f31cacf 100644
--- a/src/tactic/CMakeLists.txt
+++ b/src/tactic/CMakeLists.txt
@@ -1,14 +1,12 @@
 z3_add_component(tactic
   SOURCES
     dependency_converter.cpp
-    equiv_proof_converter.cpp
     goal.cpp
     goal_num_occurs.cpp
     goal_shared_occs.cpp
     goal_util.cpp
     horn_subsume_model_converter.cpp
     probe.cpp
-    replace_proof_converter.cpp
     tactical.cpp
     tactic.cpp
   COMPONENT_DEPENDENCIES