mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-19 07:06:28 +00:00
Code Activity

Fix MacOS CMake build: guard override with #ifdef Z3DEBUG in static_matrix.h, add clang warnings

Browse source
This commit is contained in:
copilot-swe-agent[bot] 2026-06-17 18:12:28 +00:00 • committed by GitHub
parent 17b85cbe20
commit 222a5a467b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
2 changed files with 14 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

3
cmake/compiler_warnings.cmake
View file

@ -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")

14
src/math/lp/static_matrix.h
View file

@ -119,9 +119,13 @@ public:
void init_empty_matrix(unsigned m, unsigned n);
#ifdef Z3DEBUG
unsigned row_count() const override { return static_cast<unsigned>(m_rows.size()); }
unsigned column_count() const override { return static_cast<unsigned>(m_columns.size()); }
#else
unsigned row_count() const { return static_cast<unsigned>(m_rows.size()); }
unsigned column_count() const { return static_cast<unsigned>(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<unsigned>(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;