From eb751bec4ceee3e1deed4bf6dc360ac20c05b582 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 22 Jan 2023 23:57:59 -0800
Subject: [PATCH] fix riscv/aarch/powerpc build warnings
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
src/ast/recfun_decl_plugin.h | 2 +-
src/ast/rewriter/macro_replacer.cpp | 3 +--
src/ast/simplifiers/bound_simplifier.h | 8 ++++----
src/math/lp/lp_primal_core_solver_def.h | 2 +-
4 files changed, 7 insertions(+), 8 deletions(-)
diff --git a/src/ast/recfun_decl_plugin.h b/src/ast/recfun_decl_plugin.h
index ae9c060e9..e2d480664 100644
--- a/src/ast/recfun_decl_plugin.h
+++ b/src/ast/recfun_decl_plugin.h
@@ -61,7 +61,7 @@ namespace recfun {
expr_ref_vector m_guards; //<! conjunction that is equivalent to this case
expr_ref m_rhs; //<! if guard is true, `f(t1...tn) = rhs` holds
def * m_def; //<! definition this is a part of
- bool m_immediate; //<! does `rhs` contain no defined_fun/case_pred?
+ bool m_immediate = false; //<! does `rhs` contain no defined_fun/case_pred?
case_def(ast_manager& m):
m_pred(m),
diff --git a/src/ast/rewriter/macro_replacer.cpp b/src/ast/rewriter/macro_replacer.cpp
index d8389ae6a..1cbcc14c6 100644
--- a/src/ast/rewriter/macro_replacer.cpp
+++ b/src/ast/rewriter/macro_replacer.cpp
@@ -78,8 +78,7 @@ struct macro_replacer::macro_replacer_cfg : public default_rewriter_cfg {
return false;
p = nullptr;
app* n = to_app(_n);
- quantifier* q = nullptr;
- func_decl* d = n->get_decl(), * d2 = nullptr;
+ func_decl* d = n->get_decl();
app_ref head(m);
expr_ref def(m);
expr_dependency_ref dep(m);
diff --git a/src/ast/simplifiers/bound_simplifier.h b/src/ast/simplifiers/bound_simplifier.h
index c7739715e..06e25920c 100644
--- a/src/ast/simplifiers/bound_simplifier.h
+++ b/src/ast/simplifiers/bound_simplifier.h
@@ -27,9 +27,9 @@ Description:
class bound_simplifier : public dependent_expr_simplifier {
- typedef interval_manager<im_default_config> interval_manager;
- typedef interval_manager::interval interval;
- typedef _scoped_interval<interval_manager> scoped_interval;
+ typedef interval_manager<im_default_config> _interval_manager;
+ typedef _interval_manager::interval interval;
+ typedef _scoped_interval<_interval_manager> scoped_interval;
arith_util a;
th_rewriter m_rewriter;
@@ -37,7 +37,7 @@ class bound_simplifier : public dependent_expr_simplifier {
small_object_allocator m_alloc;
bound_propagator bp;
im_default_config i_cfg;
- interval_manager i_manager;
+ _interval_manager i_manager;
unsigned m_num_vars = 0;
ptr_vector<expr> m_var2expr;
unsigned_vector m_expr2var;
diff --git a/src/math/lp/lp_primal_core_solver_def.h b/src/math/lp/lp_primal_core_solver_def.h
index 7b5dec945..3818b589a 100644
--- a/src/math/lp/lp_primal_core_solver_def.h
+++ b/src/math/lp/lp_primal_core_solver_def.h
@@ -480,7 +480,7 @@ template <typename T, typename X> int lp_primal_core_solver<T, X>::find_leaving_
template <typename T, typename X> int lp_primal_core_solver<T, X>::find_leaving_and_t(unsigned entering, X & t) {
if (this->m_settings.use_breakpoints_in_feasibility_search && !this->current_x_is_feasible())
return find_leaving_and_t_with_breakpoints(entering, t);
- X theta;
+ X theta = zero_of_type<X>();
bool unlimited = get_harris_theta(theta);
lp_assert(unlimited || theta >= zero_of_type<X>());
if (try_jump_to_another_bound_on_entering(entering, theta, t, unlimited)) return entering;