diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index 03ee6b687..84114a4d8 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -218,8 +218,8 @@ bool theory_user_propagator::internalize_term(app* term) { unsigned v = add_expr(term); - if (!m_created_eh) - throw default_exception("You have to register a created event handler for new terms"); + if (!m_created_eh && m_fixed_eh) + throw default_exception("You have to register a created event handler for new terms if you track them"); m_created_eh(m_user_context, this, term, v); return true; }