diff --git a/src/sat/smt/euf_solver.cpp b/src/sat/smt/euf_solver.cpp
index e336fff93..cf968daed 100644
--- a/src/sat/smt/euf_solver.cpp
+++ b/src/sat/smt/euf_solver.cpp
@@ -169,7 +169,7 @@ namespace euf {
             e = m_var2expr[l.var()];
             n = m_egraph.find(e);
             SASSERT(n);
-            SASSERT(m.is_bool(n->get_owner()));
+            SASSERT(m.is_bool(n->get_expr()));
             m_egraph.explain_eq<size_t>(m_explain, n, (l.sign() ? mk_false() : mk_true()));
             break;
         default:
diff --git a/src/smt/smt_enode.h b/src/smt/smt_enode.h
index 4233c51b1..fb43d2299 100644
--- a/src/smt/smt_enode.h
+++ b/src/smt/smt_enode.h
@@ -165,13 +165,11 @@ namespace smt {
 
         void del_eh(ast_manager & m, bool update_children_parent = true);
         
-        app * get_owner() const { 
-            return m_owner; 
-        }
+        app * get_owner() const { return m_owner; }
+        app * get_expr() const { return m_owner; }
 
-        unsigned get_owner_id() const {
-            return m_owner->get_id();
-        }
+        unsigned get_owner_id() const { return m_owner->get_id(); }
+        unsigned get_expr_id() const { return m_owner->get_id(); }
 
         func_decl * get_decl() const {
             return m_owner->get_decl();