diff --git a/src/sat/smt/euf_internalize.cpp b/src/sat/smt/euf_internalize.cpp
index f8b6f1cc394..54b8210af73 100644
--- a/src/sat/smt/euf_internalize.cpp
+++ b/src/sat/smt/euf_internalize.cpp
@@ -36,7 +36,7 @@ namespace euf {
         loop:
             if (!m.inc())
                 throw tactic_exception(m.limit().get_cancel_msg());
-            sat::frame & fr = m_stack.back();
+            sat::eframe & fr = m_stack.back();
             expr* e = fr.m_e;
             if (m_egraph.find(e)) {
                 m_stack.pop_back();
@@ -80,7 +80,7 @@ namespace euf {
             return n;
         }
         if (is_app(e) && to_app(e)->get_num_args() > 0) {
-            m_stack.push_back(sat::frame(e));
+            m_stack.push_back(sat::eframe(e));
             return nullptr;
         }
         n = m_egraph.mk(e, 0, nullptr);
diff --git a/src/sat/smt/euf_solver.h b/src/sat/smt/euf_solver.h
index 0d22161adca..afcd9187a12 100644
--- a/src/sat/smt/euf_solver.h
+++ b/src/sat/smt/euf_solver.h
@@ -82,7 +82,7 @@ namespace euf {
         ptr_vector<euf::enode>                          m_var2node;
         ptr_vector<unsigned>                            m_explain;
         euf::enode_vector                               m_args;
-        svector<sat::frame>                             m_stack;
+        svector<sat::eframe>                            m_stack;
         unsigned                                        m_num_scopes { 0 };
         unsigned_vector                                 m_var_trail;
         svector<scope>                                  m_scopes;
diff --git a/src/sat/smt/sat_smt.h b/src/sat/smt/sat_smt.h
index 4898303447b..82b1ab16a79 100644
--- a/src/sat/smt/sat_smt.h
+++ b/src/sat/smt/sat_smt.h
@@ -21,16 +21,16 @@ Module Name:
 
 namespace sat {
     
-    struct frame {
+    struct eframe {
         expr* m_e;
         unsigned m_idx;
-        frame(expr* e) : m_e(e), m_idx(0) {}
+        eframe(expr* e) : m_e(e), m_idx(0) {}
     };
 
     struct scoped_stack {
-        svector<frame>& s;
+        svector<eframe>& s;
         unsigned sz;
-        scoped_stack(svector<frame>& s):s(s), sz(s.size()) {}
+        scoped_stack(svector<eframe>& s):s(s), sz(s.size()) {}
         ~scoped_stack() { s.shrink(sz); }
     };