diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp
index 25feaed26..d55c20c1c 100644
--- a/src/ast/pattern/pattern_inference.cpp
+++ b/src/ast/pattern/pattern_inference.cpp
@@ -576,7 +576,7 @@ void pattern_inference::mk_patterns(unsigned num_bindings,
     m_candidates.reset();
 }
 
-#include "smt/database.h"
+#include "database.h"
 
 void pattern_inference::reduce1_quantifier(quantifier * q) {
     TRACE("pattern_inference", tout << "processing:\n" << mk_pp(q, m) << "\n";);