diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake index d8dc90c05..38b442e83 100644 --- a/cmake/compiler_warnings.cmake +++ b/cmake/compiler_warnings.cmake @@ -20,6 +20,9 @@ set(CLANG_ONLY_WARNINGS "-Wno-c++98-compat" "-Wno-c++98-compat-pedantic" "-Wno-zero-length-array" + "-Wc99-extensions" + "-Wsuggest-override" + "-Winconsistent-missing-override" ) set(MSVC_WARNINGS "/W3") diff --git a/src/math/lp/static_matrix.h b/src/math/lp/static_matrix.h index 08db2245d..3c422c1f9 100644 --- a/src/math/lp/static_matrix.h +++ b/src/math/lp/static_matrix.h @@ -119,9 +119,13 @@ public: void init_empty_matrix(unsigned m, unsigned n); +#ifdef Z3DEBUG + unsigned row_count() const override { return static_cast(m_rows.size()); } + unsigned column_count() const override { return static_cast(m_columns.size()); } +#else unsigned row_count() const { return static_cast(m_rows.size()); } - unsigned column_count() const { return static_cast(m_columns.size()); } +#endif unsigned lowest_row_in_column(unsigned col); @@ -197,7 +201,11 @@ public: void cross_out_row_from_column(unsigned col, unsigned k); +#ifdef Z3DEBUG + T get_elem(unsigned i, unsigned j) const override; +#else T get_elem(unsigned i, unsigned j) const; +#endif unsigned number_of_non_zeroes_in_column(unsigned j) const { return static_cast(m_columns[j].size()); } @@ -218,8 +226,8 @@ public: #ifdef Z3DEBUG unsigned get_number_of_rows() const { return row_count(); } unsigned get_number_of_columns() const { return column_count(); } - virtual void set_number_of_rows(unsigned /*m*/) { } - virtual void set_number_of_columns(unsigned /*n*/) { } + void set_number_of_rows(unsigned /*m*/) override { } + void set_number_of_columns(unsigned /*n*/) override { } #endif T get_balance() const;