From 8cb5f32ef7bc3263b95e9b09f549dc702e71e1fd Mon Sep 17 00:00:00 2001 From: David Detlefs Date: Thu, 18 Jun 2026 09:16:25 -0700 Subject: [PATCH] Some of the overrides are only in debug builds; handle this. --- src/math/lp/static_matrix.h | 18 +++++++++++++++--- 1 file changed, 15 insertions(+), 3 deletions(-) diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h index 5395bf44f..c04728cc8 100644 --- a/src/math/lp/static_matrix.h +++ b/src/math/lp/static_matrix.h @@ -60,6 +60,14 @@ std::ostream& operator<<(std::ostream& out, const row_strip& r) { return out << "\n"; } +// Below, static_matrix has a superclass when Z3DEBUG is set, and some +// methods are overrides in that case. +#ifdef Z3DEBUG +#define DEBUG_OVERRIDE override +#else +#define DEBUG_OVERRIDE +#endif + // each assignment for this matrix should be issued only once!!! template class static_matrix @@ -119,9 +127,13 @@ public: void init_empty_matrix(unsigned m, unsigned n); - unsigned row_count() const override { return static_cast(m_rows.size()); } + unsigned row_count() const DEBUG_OVERRIDE { + return static_cast(m_rows.size()); + } - unsigned column_count() const override { return static_cast(m_columns.size()); } + unsigned column_count() const DEBUG_OVERRIDE { + return static_cast(m_columns.size()); + } unsigned lowest_row_in_column(unsigned col); @@ -197,7 +209,7 @@ public: void cross_out_row_from_column(unsigned col, unsigned k); - T get_elem(unsigned i, unsigned j) const override; + T get_elem(unsigned i, unsigned j) const DEBUG_OVERRIDE; unsigned number_of_non_zeroes_in_column(unsigned j) const { return static_cast(m_columns[j].size()); }