From 66dd93a03559ba7abdb184259fee4f8834203347 Mon Sep 17 00:00:00 2001 From: Lev Nachmanson Date: Fri, 28 Feb 2020 17:18:51 -0800 Subject: [PATCH] fix a bug in nla_intervals - add explanations when getting intervals from a term Signed-off-by: Lev Nachmanson --- src/math/lp/nla_core.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/math/lp/nla_core.cpp b/src/math/lp/nla_core.cpp index 9982100d7..2a2043604 100644 --- a/src/math/lp/nla_core.cpp +++ b/src/math/lp/nla_core.cpp @@ -166,7 +166,7 @@ rational core::product_value(const unsigned_vector & m) const { bool core::check_monic(const monic& m) const { SASSERT((!m_lar_solver.column_is_int(m.var())) || m_lar_solver.get_column_value(m.var()).is_int()); bool ret = product_value(m.vars()) == m_lar_solver.get_column_value_rational(m.var()); - CTRACE("nla_solver", !ret, print_monic(m, tout) << '\n';); + CTRACE("nla_solver_check_monic", !ret, print_monic(m, tout) << '\n';); return ret; }