diff --git a/src/ast/euf/euf_sgraph.h b/src/ast/euf/euf_sgraph.h
index 950fc8c06..3881256d0 100644
--- a/src/ast/euf/euf_sgraph.h
+++ b/src/ast/euf/euf_sgraph.h
@@ -91,9 +91,6 @@ namespace euf {
         stats            m_stats;
         bool             m_add_plugin; // whether sgraph created the seq_plugin
 
-        // tracks allocated subst caches for cleanup
-        ptr_vector<snode_subst_cache> m_subst_caches;
-
         // maps expression id to snode
         ptr_vector<snode> m_expr2snode;
 
diff --git a/src/ast/euf/euf_snode.h b/src/ast/euf/euf_snode.h
index 1028cdfa1..d0be50946 100644
--- a/src/ast/euf/euf_snode.h
+++ b/src/ast/euf/euf_snode.h
@@ -32,7 +32,6 @@ namespace euf {
 
     class sgraph;
     class snode;
-    struct snode_subst_cache;
 
     typedef ptr_vector<snode> snode_vector;
 
@@ -73,9 +72,6 @@ namespace euf {
         // all zeros means not cached, non-zero means cached
         unsigned    m_hash_matrix[2][2] = {{0,0},{0,0}};
 
-        // substitution cache (lazy-initialized, owned by sgraph)
-        snode_subst_cache* m_subst_cache = nullptr;
-
         snode*      m_args[0]; // variable-length array, allocated via get_snode_size(num_args)
 
         friend class sgraph;