diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 8e7f65ffd..c28cd7f89 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -341,7 +341,7 @@ class theory_lra::imp { return m_th.is_int(v); } else { - return (unsigned)std::hash()(m_th.get_value(v)); + return (unsigned)std::hash()(m_th.get_ivalue(v)); } } }; @@ -1652,7 +1652,7 @@ public: if (!th.is_relevant_and_shared(n1)) { continue; } - if (!can_get_value(v)) { + if (!can_get_ivalue(v)) { continue; } theory_var other = m_model_eqs.insert_if_not_there(v); @@ -1705,7 +1705,7 @@ public: return m_nra->am().eq(nl_value(v1, *m_a1), nl_value(v2, *m_a2)); } else { - return get_value(v1) == get_value(v2); + return get_ivalue(v1) == get_ivalue(v2); } }