diff --git a/src/ast/euf/euf_egraph.cpp b/src/ast/euf/euf_egraph.cpp
index 97a34a744..0c24287ef 100644
--- a/src/ast/euf/euf_egraph.cpp
+++ b/src/ast/euf/euf_egraph.cpp
@@ -805,8 +805,8 @@ namespace euf {
         }
         else if (j.is_equality()) 
             explain_eq(justifications, cc, j.lhs(), j.rhs());
-        else if (j.is_axiom() && j.theory_id() != null_theory_id) {
-            IF_VERBOSE(0, verbose_stream() << "TODO add theory axiom to justification");
+        else if (j.is_axiom() && j.get_theory_id() != null_theory_id) {
+            IF_VERBOSE(20, verbose_stream() << "TODO add theory axiom to justification\n");
         }
         if (cc && j.is_congruence()) 
             cc->push_back(std::tuple(a->get_app(), b->get_app(), j.timestamp(), j.is_commutative()));
diff --git a/src/ast/euf/euf_justification.h b/src/ast/euf/euf_justification.h
index faedea553..8a5a58ad9 100644
--- a/src/ast/euf/euf_justification.h
+++ b/src/ast/euf/euf_justification.h
@@ -112,7 +112,7 @@ namespace euf {
         enode* lhs() const { SASSERT(is_equality()); return m_n1; }
         enode* rhs() const { SASSERT(is_equality()); return m_n2; }
         uint64_t timestamp() const { SASSERT(is_congruence()); return m_timestamp; }
-        theory_id theory_id() const { SASSERT(is_axiom()); return m_theory_id; }
+        theory_id get_theory_id() const { SASSERT(is_axiom()); return m_theory_id; }
         template <typename T>
         T*  ext() const { SASSERT(is_external()); return static_cast<T*>(m_external); }