diff --git a/src/model/func_interp.cpp b/src/model/func_interp.cpp index ae4c657bd..406f7a89b 100644 --- a/src/model/func_interp.cpp +++ b/src/model/func_interp.cpp @@ -159,11 +159,17 @@ void func_interp::insert_entry(expr * const * args, expr * r) { void func_interp::insert_new_entry(expr * const * args, expr * r) { reset_interp_cache(); CTRACE("func_interp_bug", get_entry(args) != 0, + tout << "Old: " << mk_ismt2_pp(get_entry(args)->m_result, m_manager) << "\n"; + tout << "Args:"; + for (unsigned i = 0; i < m_arity; i++) { + tout << mk_ismt2_pp(get_entry(args)->get_arg(i), m_manager) << "\n"; + } + tout << "New: " << mk_ismt2_pp(r, m_manager) << "\n"; + tout << "Args:"; for (unsigned i = 0; i < m_arity; i++) { tout << mk_ismt2_pp(args[i], m_manager) << "\n"; } - tout << "Old: " << mk_ismt2_pp(get_entry(args)->m_result, m_manager) << "\n"; - tout << "New: " << mk_ismt2_pp(r, m_manager) << "\n";); + ); SASSERT(get_entry(args) == 0); func_entry * new_entry = func_entry::mk(m_manager, m_arity, args, r); if (!new_entry->args_are_values()) diff --git a/src/opt/optsmt.cpp b/src/opt/optsmt.cpp index 19ea39521..668043c03 100644 --- a/src/opt/optsmt.cpp +++ b/src/opt/optsmt.cpp @@ -117,7 +117,6 @@ namespace opt { void optsmt::update_lower(unsigned idx, rational const& r) { inf_eps v(r); - std::cout << "update lower: " << r << "\n"; if (m_lower[idx] < v) { m_lower[idx] = v; if (m_s) m_s->get_model(m_model);