mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-15 21:38:44 +00:00
Code Activity

align column names with column printer

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-09-24 05:03:40 -07:00
parent 43db7df2b5
commit e775964cfd
1 changed files with 2 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

3
src/smt/theory_lra.cpp
View file

@ -3864,9 +3864,10 @@ public:
unsigned nv = th.get_num_vars(); unsigned nv = th.get_num_vars();
for (unsigned v = 0; v < nv; ++v) { for (unsigned v = 0; v < nv; ++v) {
auto t = get_tv(v); auto t = get_tv(v);
auto vi = lp().external_to_column_index(v);
if (!ctx().is_relevant(get_enode(v))) out << "irr: "; if (!ctx().is_relevant(get_enode(v))) out << "irr: ";
out << "v" << v << " "; 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)); 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); else if (can_get_value(v)) out << " = " << get_value(v);
if (is_int(v)) out << ", int"; if (is_int(v)) out << ", int";