From a0f6447a33ff9139d7119e107b0ba8f079ad598c Mon Sep 17 00:00:00 2001 From: nilsbecker Date: Fri, 5 Oct 2018 13:58:22 +0200 Subject: [PATCH] logging which theory added constraints --- src/smt/smt_internalizer.cpp | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_internalizer.cpp b/src/smt/smt_internalizer.cpp index 618450f9d..4a6cd086c 100644 --- a/src/smt/smt_internalizer.cpp +++ b/src/smt/smt_internalizer.cpp @@ -1018,8 +1018,17 @@ namespace smt { void context::apply_sort_cnstr(app * term, enode * e) { sort * s = term->get_decl()->get_range(); theory * th = m_theories.get_plugin(s->get_family_id()); - if (th) + if (th) { + if (m_manager.has_trace_stream()) { + m_manager.trace_stream() << "[theory-constraints] " << m_manager.get_family_name(s->get_family_id()) << "\n"; + } + th->apply_sort_cnstr(e, s); + + if (m_manager.has_trace_stream()) { + m_manager.trace_stream() << "[end-theory-constraints]\n"; + } + } } /**