From e775964cfdd48ad0a2edcea89b644d884d57efeb Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Thu, 24 Sep 2020 05:03:40 -0700 Subject: [PATCH] align column names with column printer Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index 534964344..104dc430d 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3864,9 +3864,10 @@ public: unsigned nv = th.get_num_vars(); for (unsigned v = 0; v < nv; ++v) { auto t = get_tv(v); + auto vi = lp().external_to_column_index(v); if (!ctx().is_relevant(get_enode(v))) out << "irr: "; out << "v" << v << " "; - if (t.is_null()) out << "null"; else out << (t.is_term() ? "t":"j") << t.id(); + if (t.is_null()) out << "null"; else out << (t.is_term() ? "t":"j") << vi; if (use_nra_model() && can_get_ivalue(v)) m_nla->am().display(out << " = ", nl_value(v, *m_a1)); else if (can_get_value(v)) out << " = " << get_value(v); if (is_int(v)) out << ", int";