From b723e1093b81391deb66ff7a2cff7ec0e267e635 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sat, 31 Jul 2021 13:01:02 -0700 Subject: [PATCH] misc warnings Signed-off-by: Nikolaj Bjorner --- src/muz/spacer/spacer_manager.cpp | 2 +- src/sat/smt/euf_model.cpp | 1 + src/sat/smt/fpa_solver.cpp | 1 - src/smt/theory_str.cpp | 12 ++++++------ 4 files changed, 8 insertions(+), 8 deletions(-) diff --git a/src/muz/spacer/spacer_manager.cpp b/src/muz/spacer/spacer_manager.cpp index ba20e5f24..e8d769621 100644 --- a/src/muz/spacer/spacer_manager.cpp +++ b/src/muz/spacer/spacer_manager.cpp @@ -247,7 +247,7 @@ bool is_zk_const (const app *a, int &n) { } bool sk_lt_proc::operator()(const app *a1, const app *a2) { if (a1 == a2) return false; - int n1, n2; + int n1 = 0, n2 = 0; bool z1, z2; z1 = is_zk_const(a1, n1); z2 = is_zk_const(a2, n2); diff --git a/src/sat/smt/euf_model.cpp b/src/sat/smt/euf_model.cpp index 412aec533..d2fa19eee 100644 --- a/src/sat/smt/euf_model.cpp +++ b/src/sat/smt/euf_model.cpp @@ -284,6 +284,7 @@ namespace euf { tout << "Failed to validate " << n->bool_var() << " " << bpp(n) << " " << mdl(e) << "\n"; s().display(tout); tout << mdl << "\n";); + (void)first; first = false; } diff --git a/src/sat/smt/fpa_solver.cpp b/src/sat/smt/fpa_solver.cpp index 13837d0ce..590929a91 100644 --- a/src/sat/smt/fpa_solver.cpp +++ b/src/sat/smt/fpa_solver.cpp @@ -121,7 +121,6 @@ namespace fpa { bool solver::post_visit(expr* e, bool sign, bool root) { euf::enode* n = expr2enode(e); - app* a = to_app(e); SASSERT(!n || !n->is_attached_to(get_id())); if (!n) n = mk_enode(e, false); diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp index 6705d40e4..0b772f17d 100644 --- a/src/smt/theory_str.cpp +++ b/src/smt/theory_str.cpp @@ -1859,18 +1859,18 @@ namespace smt { axiomatized_terms.insert(ex); TRACE("str", tout << "instantiate str.from_code axiom for " << mk_pp(ex, m) << std::endl;); - expr * arg; - u.str.is_from_code(ex, arg); + expr * arg = nullptr; + VERIFY(u.str.is_from_code(ex, arg)); // (str.from_code N) == "" if N is not in the range [0, max_char]. { - expr_ref premise(m.mk_or(m_autil.mk_le(arg, mk_int(-1)), m_autil.mk_ge(arg, mk_int(u.max_char() + 1))), m); + expr_ref premise(m.mk_or(m_autil.mk_le(arg, mk_int(-1)), m_autil.mk_ge(arg, mk_int(u.max_char() + 1))), m); expr_ref conclusion(ctx.mk_eq_atom(ex, mk_string("")), m); expr_ref axiom(rewrite_implication(premise, conclusion), m); assert_axiom_rw(axiom); } // len (str.from_code N) == 1 if N is in the range [0, max_char]. { - expr_ref premise(m.mk_and(m_autil.mk_ge(arg, mk_int(0)), m_autil.mk_le(arg, mk_int(u.max_char() + 1))), m); + expr_ref premise(m.mk_and(m_autil.mk_ge(arg, mk_int(0)), m_autil.mk_le(arg, mk_int(u.max_char() + 1))), m); expr_ref conclusion(ctx.mk_eq_atom(mk_strlen(ex), mk_int(1)), m); expr_ref axiom(rewrite_implication(premise, conclusion), m); assert_axiom_rw(axiom); @@ -1895,8 +1895,8 @@ namespace smt { axiomatized_terms.insert(ex); TRACE("str", tout << "instantiate str.to_code axiom for " << mk_pp(ex, m) << std::endl;); - expr * arg; - u.str.is_to_code(ex, arg); + expr * arg = nullptr; + VERIFY(u.str.is_to_code(ex, arg)); // (str.to_code S) == -1 if len(S) != 1. { expr_ref premise(m.mk_not(ctx.mk_eq_atom(mk_strlen(arg), mk_int(1))), m);