diff --git a/src/ast/simplifiers/max_bv_sharing.cpp b/src/ast/simplifiers/max_bv_sharing.cpp
index f708f9dce75..cc56280ddaf 100644
--- a/src/ast/simplifiers/max_bv_sharing.cpp
+++ b/src/ast/simplifiers/max_bv_sharing.cpp
@@ -22,6 +22,7 @@ Revision History:
 
 #include "ast/rewriter/maximize_ac_sharing.h"
 #include "ast/simplifiers/dependent_expr_state.h"
+#include "ast/rewriter/rewriter_def.h"
 
 class max_bv_sharing : public dependent_expr_simplifier {
 
diff --git a/src/sat/sat_solver/sat_smt_preprocess.cpp b/src/sat/sat_solver/sat_smt_preprocess.cpp
index c1a4acc9e95..02c6e88b42e 100644
--- a/src/sat/sat_solver/sat_smt_preprocess.cpp
+++ b/src/sat/sat_solver/sat_smt_preprocess.cpp
@@ -16,6 +16,7 @@ Module Name:
 --*/
 
 
+#include "ast/rewriter/rewriter_def.h"
 #include "ast/simplifiers/bit_blaster.h"
 #include "ast/simplifiers/max_bv_sharing.h"
 #include "ast/simplifiers/card2bv.h"