From c6539deb6169afde2b569fba89a828f2f726691f Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 25 Jan 2022 17:25:42 +0100 Subject: [PATCH] fixing null check Signed-off-by: Nikolaj Bjorner --- src/smt/theory_user_propagator.cpp | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_user_propagator.cpp b/src/smt/theory_user_propagator.cpp index 84114a4d8..5e5bd1e1d 100644 --- a/src/smt/theory_user_propagator.cpp +++ b/src/smt/theory_user_propagator.cpp @@ -218,9 +218,10 @@ bool theory_user_propagator::internalize_term(app* term) { unsigned v = add_expr(term); - if (!m_created_eh && m_fixed_eh) + if (!m_created_eh && (m_fixed_eh || m_eq_eh || m_diseq_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); + if (m_created_eh) + m_created_eh(m_user_context, this, term, v); return true; }