diff --git a/src/muz/rel/doc.h b/src/muz/rel/doc.h
index b56947e2e..bae9f64e6 100644
--- a/src/muz/rel/doc.h
+++ b/src/muz/rel/doc.h
@@ -25,7 +25,7 @@ Revision History:
 #include "util/tbv.h"
 #include "util/union_find.h"
 #include "util/buffer.h"
-
+#include "ast/ast.h"
 
 class doc;
 template<typename M, typename T> class union_bvec;
diff --git a/src/util/tbv.cpp b/src/util/tbv.cpp
index 13615b549..017ca0eb7 100644
--- a/src/util/tbv.cpp
+++ b/src/util/tbv.cpp
@@ -20,7 +20,6 @@ Revision History:
 
 #include "util/tbv.h"
 #include "util/hashtable.h"
-#include "ast/ast_util.h"
 
 
 static bool s_debug_alloc = false;
diff --git a/src/util/tbv.h b/src/util/tbv.h
index 2fe00c2a1..2a337be1f 100644
--- a/src/util/tbv.h
+++ b/src/util/tbv.h
@@ -23,7 +23,6 @@ Revision History:
 #include "util/fixed_bit_vector.h"
 #include "util/bit_vector.h"
 #include "util/rational.h"
-#include "ast/ast.h"
 
 class tbv;