mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

fix compiler warnings

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-12 13:39:13 -08:00
parent 85356c5548
commit 8d2b9b41fd
3 changed files with 5 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/math/lp/lar_solver.cpp
View file

@ -2097,6 +2097,7 @@ namespace lp {
switch (kind) {
case LT:
y_of_bound = -1;
Z3_fallthrough;
case LE: {
auto up = numeric_pair<mpq>(right_side, y_of_bound);
if (up < m_mpq_lar_core_solver.m_r_lower_bounds[j]) {
@ -2213,6 +2214,7 @@ namespace lp {
} break;
case GT:
y_of_bound = 1;
Z3_fallthrough;
case GE: {
auto low = numeric_pair<mpq>(right_side, y_of_bound);
m_mpq_lar_core_solver.m_r_lower_bounds[j] = low;

2
src/math/lp/lp_bound_propagator.h
View file

@ -28,7 +28,7 @@ class lp_bound_propagator {
// works for rows of the form x - y + sum of fixed = 0
map<mpq, unsigned, obj_hash<mpq>, default_eq<mpq>> m_row2index_neg;
const vector<column_type>* m_column_types;
const vector<column_type>* m_column_types = nullptr;
// returns true iff there is only one non-fixed column in the row
bool only_one_nfixed(unsigned r, unsigned& x) {
x = UINT_MAX;

4
src/math/lp/var_register.h
View file

@ -23,8 +23,8 @@ namespace lp {
class ext_var_info {
unsigned m_external_j;
bool m_is_integer;
unsigned m_external_j = 0;
bool m_is_integer = false;
std::string m_name;
public:
ext_var_info() = default;