diff --git a/src/util/lp/var_eqs.cpp b/src/util/lp/var_eqs.cpp
index 31da7d92b..0a422c254 100644
--- a/src/util/lp/var_eqs.cpp
+++ b/src/util/lp/var_eqs.cpp
@@ -51,10 +51,10 @@ void var_eqs::merge(signed_var v1, signed_var v2, eq_justification const& j) {
     m_trail.push_back(std::make_pair(v1, v2));
     m_uf.merge(v1.index(), v2.index());
     m_uf.merge((~v1).index(), (~v2).index());
-    m_eqs[v1.index()].push_back(justified_var(v2, j));
-    m_eqs[v2.index()].push_back(justified_var(v1, j));
-    m_eqs[(~v1).index()].push_back(justified_var(~v2, j));
-    m_eqs[(~v2).index()].push_back(justified_var(~v1, j));
+    m_eqs[v1.index()].push_back(eq_edge(v2, j));
+    m_eqs[v2.index()].push_back(eq_edge(v1, j));
+    m_eqs[(~v1).index()].push_back(eq_edge(~v2, j));
+    m_eqs[(~v2).index()].push_back(eq_edge(~v1, j));
 }
 
 signed_var var_eqs::find(signed_var v) const {
@@ -71,7 +71,7 @@ void var_eqs::explain_dfs(signed_var v1, signed_var v2, lp::explanation& e) cons
         return;
     }
     m_todo.push_back(var_frame(v1, 0));
-    m_jtrail.reset();
+    m_justtrail.reset();
     m_marked.reserve(m_eqs.size(), false);
     SASSERT(m_marked_trail.empty());
     m_marked[v1.index()] = true;
@@ -87,30 +87,30 @@ void var_eqs::explain_dfs(signed_var v1, signed_var v2, lp::explanation& e) cons
         bool seen_all = true;
         unsigned sz = next.size();
         for (unsigned i = f.m_index; seen_all && i < sz; ++i) {
-            justified_var const& jv = next[i];
+            eq_edge const& jv = next[i];
             signed_var v3 = jv.m_var;
             if (!m_marked[v3.index()]) {
                 seen_all = false;
                 f.m_index = i + 1;
                 m_todo.push_back(var_frame(v3, 0));
-                m_jtrail.push_back(jv.m_j);
+                m_justtrail.push_back(jv.m_just);
                 m_marked_trail.push_back(v3.index());
                 m_marked[v3.index()] = true;
             }
         }
         if (seen_all) {
             m_todo.pop_back();
-            m_jtrail.pop_back();
+            m_justtrail.pop_back();
         }
     }
         
-    for (eq_justification const& j : m_jtrail) {
+    for (eq_justification const& j : m_justtrail) {
         j.explain(e);
     }
-    m_stats.m_num_explains += m_jtrail.size();
+    m_stats.m_num_explains += m_justtrail.size();
     m_stats.m_num_explain_calls++;
     m_todo.reset();
-    m_jtrail.reset();
+    m_justtrail.reset();
     for (unsigned idx : m_marked_trail) {
         m_marked[idx] = false;
     }
@@ -125,7 +125,7 @@ void var_eqs::explain_bfs(signed_var v1, signed_var v2, lp::explanation& e) cons
         return;
     }
     m_todo.push_back(var_frame(v1, 0));
-    m_jtrail.push_back(eq_justification({}));
+    m_justtrail.push_back(eq_justification({}));
     m_marked.reserve(m_eqs.size(), false);
     SASSERT(m_marked_trail.empty());
     m_marked[v1.index()] = true;
@@ -140,11 +140,11 @@ void var_eqs::explain_bfs(signed_var v1, signed_var v2, lp::explanation& e) cons
         auto const& next = m_eqs[v.index()];
         unsigned sz = next.size();
         for (unsigned i = sz; i-- > 0; ) {
-            justified_var const& jv = next[i];
+            eq_edge const& jv = next[i];
             signed_var v3 = jv.m_var;
             if (!m_marked[v3.index()]) {
                 m_todo.push_back(var_frame(v3, head));
-                m_jtrail.push_back(jv.m_j);
+                m_justtrail.push_back(jv.m_just);
                 m_marked_trail.push_back(v3.index());
                 m_marked[v3.index()] = true;
             }
@@ -152,14 +152,14 @@ void var_eqs::explain_bfs(signed_var v1, signed_var v2, lp::explanation& e) cons
     }
         
     while (head != 0) {
-        m_jtrail[head].explain(e);
+        m_justtrail[head].explain(e);
         head = m_todo[head].m_index;
         ++m_stats.m_num_explains;
     }
     ++m_stats.m_num_explain_calls;
         
     m_todo.reset();
-    m_jtrail.reset();
+    m_justtrail.reset();
     for (unsigned idx : m_marked_trail) {
         m_marked[idx] = false;
     }
diff --git a/src/util/lp/var_eqs.h b/src/util/lp/var_eqs.h
index 04d3474a8..a1bde7ca1 100644
--- a/src/util/lp/var_eqs.h
+++ b/src/util/lp/var_eqs.h
@@ -56,12 +56,12 @@ public:
  };
 
 class var_eqs {
-    struct justified_var {
+    struct eq_edge {
         signed_var       m_var;
-        eq_justification m_j;
-        justified_var(signed_var v, eq_justification const& j): m_var(v), m_j(j) {}
+        eq_justification m_just;
+        eq_edge(signed_var v, eq_justification const& j): m_var(v), m_just(j) {}
     };
-    typedef svector<justified_var> justified_vars;
+    typedef svector<eq_edge> eq_edges;
 
     struct var_frame {
         signed_var m_var;
@@ -80,14 +80,14 @@ class var_eqs {
     union_find<var_eqs>         m_uf;
     svector<signed_var_pair>    m_trail;
     unsigned_vector         m_trail_lim;
-    vector<justified_vars>  m_eqs;    // signed_var-index -> justified_var corresponding to edges in a graph used to extract justifications.
+    vector<eq_edges>  m_eqs;    // signed_var-index -> eq_edges corresponding to edges in a graph used to extract justifications.
 
     typedef trail_stack<var_eqs>    trail_stack_t;       
     trail_stack_t                   m_stack;
     mutable svector<var_frame>      m_todo;
     mutable svector<bool>           m_marked;
     mutable unsigned_vector         m_marked_trail;
-    mutable svector<eq_justification> m_jtrail;
+    mutable svector<eq_justification> m_justtrail;
         
     mutable stats m_stats;
 public:
@@ -154,7 +154,7 @@ public:
         return explain(find(s), s, e); 
     }
 
-    // iterates over the class of signed_var(m_idx)
+    // iterates over the class of lpvar(m_idx)
     class iterator {
         var_eqs& m_ve;        // context.
         unsigned m_idx;       // index into a signed variable, same as union-find index