From 3237bd924374ed1c1371a051e478f0d37928ef39 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 27 Mar 2020 16:05:57 -0700 Subject: [PATCH] better tracing Signed-off-by: Lev Nachmanson --- src/math/lp/lar_solver.cpp | 2 +- src/smt/theory_lra.cpp | 4 ++-- 2 files changed, 3 insertions(+), 3 deletions(-) diff --git a/src/math/lp/lar_solver.cpp b/src/math/lp/lar_solver.cpp index 0d7889041..c602707cf 100644 --- a/src/math/lp/lar_solver.cpp +++ b/src/math/lp/lar_solver.cpp @@ -1799,7 +1799,7 @@ mpq lar_solver::adjust_bound_for_int(lpvar j, lconstraint_kind& k, const mpq& bo } constraint_index lar_solver::mk_var_bound(var_index j, lconstraint_kind kind, const mpq & right_side) { - TRACE("lar_solver", tout << "j = " << j << " " << lconstraint_kind_string(kind) << " " << right_side<< std::endl;); + TRACE("lar_solver", tout << "j = " << get_variable_name(j) << " " << lconstraint_kind_string(kind) << " " << right_side<< std::endl;); constraint_index ci; if (!tv::is_term(j)) { // j is a var mpq rs = adjust_bound_for_int(j, kind, right_side); diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index dd2298591..2cef1f7b3 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -3050,7 +3050,7 @@ public: } constraint_bound& b = vec[ti]; if (b.first == UINT_MAX || (is_lower? b.second < v : b.second > v)) { - TRACE("arith", tout << "tighter bound " << vi << "\n";); + TRACE("arith", tout << "tighter bound " << lp().get_variable_name(vi) << "\n";); m_history.push_back(vec[ti]); ctx().push_trail(history_trail(vec, ti, m_history)); b.first = ci; @@ -3093,7 +3093,7 @@ public: if (lp::tv::is_term(vi)) { theory_var v = lp().local_to_external(vi); rational val; - TRACE("arith", tout << vi << " " << v << "\n";); + TRACE("arith", tout << lp().get_variable_name(vi) << " " << v << "\n";); if (v != null_theory_var && a.is_numeral(get_owner(v), val) && bound == val) { ci = UINT_MAX; return bound == val;