mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 18:31:49 +00:00
avoid push/pop if diseq/eq are not defined
This commit is contained in:
parent
78eaefe5a8
commit
f27485dae7
|
@ -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;
|
||||
|
|
Loading…
Reference in a new issue