diff --git a/src/ast/converters/CMakeLists.txt b/src/ast/converters/CMakeLists.txt
index 5343c32a2..52895f064 100644
--- a/src/ast/converters/CMakeLists.txt
+++ b/src/ast/converters/CMakeLists.txt
@@ -2,6 +2,7 @@ z3_add_component(converters
   SOURCES
     equiv_proof_converter.cpp
     generic_model_converter.cpp
+    horn_subsume_model_converter.cpp
     model_converter.cpp
     proof_converter.cpp
     replace_proof_converter.cpp
diff --git a/src/tactic/horn_subsume_model_converter.cpp b/src/ast/converters/horn_subsume_model_converter.cpp
similarity index 99%
rename from src/tactic/horn_subsume_model_converter.cpp
rename to src/ast/converters/horn_subsume_model_converter.cpp
index 979359a46..a0c8b341e 100644
--- a/src/tactic/horn_subsume_model_converter.cpp
+++ b/src/ast/converters/horn_subsume_model_converter.cpp
@@ -18,14 +18,14 @@ Revision History:
 --*/
 
 
-#include "tactic/horn_subsume_model_converter.h"
-#include "ast/rewriter/var_subst.h"
 #include "ast/ast_pp.h"
-#include "model/model_smt2_pp.h"
-#include "ast/rewriter/bool_rewriter.h"
-#include "ast/rewriter/th_rewriter.h"
 #include "ast/for_each_expr.h"
 #include "ast/well_sorted.h"
+#include "ast/rewriter/var_subst.h"
+#include "ast/rewriter/bool_rewriter.h"
+#include "ast/rewriter/th_rewriter.h"
+#include "model/model_smt2_pp.h"
+#include "ast/converters/horn_subsume_model_converter.h"
 
 void horn_subsume_model_converter::insert(app* head, expr* body) {
     m_delay_head.push_back(head);
diff --git a/src/tactic/horn_subsume_model_converter.h b/src/ast/converters/horn_subsume_model_converter.h
similarity index 100%
rename from src/tactic/horn_subsume_model_converter.h
rename to src/ast/converters/horn_subsume_model_converter.h
diff --git a/src/muz/base/dl_util.h b/src/muz/base/dl_util.h
index 3d5501b37..4688a67fd 100644
--- a/src/muz/base/dl_util.h
+++ b/src/muz/base/dl_util.h
@@ -18,12 +18,13 @@ Revision History:
 --*/
 #pragma once
 
+
 #include<vector>
 #include "ast/ast.h"
 #include "util/hashtable.h"
 #include "util/obj_hashtable.h"
 #include "util/uint_set.h"
-#include "tactic/horn_subsume_model_converter.h"
+#include "ast/converters/horn_subsume_model_converter.h"
 #include "ast/converters/replace_proof_converter.h"
 #include "ast/substitution/substitution.h"
 #include "ast/rewriter/ast_counter.h"
diff --git a/src/tactic/CMakeLists.txt b/src/tactic/CMakeLists.txt
index 17f31cacf..72bbbc303 100644
--- a/src/tactic/CMakeLists.txt
+++ b/src/tactic/CMakeLists.txt
@@ -5,7 +5,6 @@ z3_add_component(tactic
     goal_num_occurs.cpp
     goal_shared_occs.cpp
     goal_util.cpp
-    horn_subsume_model_converter.cpp
     probe.cpp
     tactical.cpp
     tactic.cpp