diff --git a/src/ast/pattern/pattern_inference.cpp b/src/ast/pattern/pattern_inference.cpp
index 09f583df4..d751a1388 100644
--- a/src/ast/pattern/pattern_inference.cpp
+++ b/src/ast/pattern/pattern_inference.cpp
@@ -106,7 +106,7 @@ pattern_inference_cfg::pattern_inference_cfg(ast_manager & m, pattern_inference_
     m_params(params),
     m_bfid(m.get_basic_family_id()),
     m_afid(m.mk_family_id("arith")),
-    m_le(m),
+    m_le(),
     m_nested_arith_only(true),
     m_block_loop_patterns(params.m_pi_block_loop_patterns),
     m_candidates(m),
diff --git a/src/ast/pattern/pattern_inference.h b/src/ast/pattern/pattern_inference.h
index 28218ee17..bb4cf4238 100644
--- a/src/ast/pattern/pattern_inference.h
+++ b/src/ast/pattern/pattern_inference.h
@@ -37,7 +37,6 @@ Revision History:
    every instance of f(g(X)) is also an instance of f(X).
 */
 class smaller_pattern {
-    ast_manager &    m;
     ptr_vector<expr> m_bindings;
 
     typedef std::pair<expr *, expr *> expr_pair;
@@ -50,9 +49,7 @@ class smaller_pattern {
 
 public:
 
-    smaller_pattern(ast_manager & m):
-        m(m) {
-    }
+    smaller_pattern() = default;
 
     smaller_pattern & operator=(smaller_pattern const &) = delete;