From f27485dae7617b8edcc53b4e90dc9032ad703095 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 9 Aug 2022 11:33:29 +0300 Subject: [PATCH] avoid push/pop if diseq/eq are not defined --- src/smt/theory_user_propagator.h | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_user_propagator.h b/src/smt/theory_user_propagator.h index 73fc5bb4506..2ed1acbdff6 100644 --- a/src/smt/theory_user_propagator.h +++ b/src/smt/theory_user_propagator.h @@ -143,8 +143,8 @@ namespace smt { char const* get_name() const override { return "user_propagate"; } bool internalize_atom(app* atom, bool gate_ctx) override; bool internalize_term(app* term) override; - void new_eq_eh(theory_var v1, theory_var v2) override { force_push(); if (m_eq_eh) m_eq_eh(m_user_context, this, var2expr(v1), var2expr(v2)); } - void new_diseq_eh(theory_var v1, theory_var v2) override { force_push(); if (m_diseq_eh) m_diseq_eh(m_user_context, this, var2expr(v1), var2expr(v2)); } + void new_eq_eh(theory_var v1, theory_var v2) override { if (m_eq_eh) force_push(), m_eq_eh(m_user_context, this, var2expr(v1), var2expr(v2)); } + void new_diseq_eh(theory_var v1, theory_var v2) override { if (m_diseq_eh) force_push(), m_diseq_eh(m_user_context, this, var2expr(v1), var2expr(v2)); } bool use_diseqs() const override { return ((bool)m_diseq_eh); } bool build_models() const override { return false; } final_check_status final_check_eh() override;