From 5e5c231712dc57bff527eb22d67d0136218251c3 Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Tue, 23 Jul 2019 11:09:50 +0200 Subject: [PATCH 1/2] Remove unused variables --- src/ast/rewriter/seq_rewriter.cpp | 1 - src/model/model_evaluator.cpp | 2 -- 2 files changed, 3 deletions(-) diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp index 63c881b93..e6a233d3c 100644 --- a/src/ast/rewriter/seq_rewriter.cpp +++ b/src/ast/rewriter/seq_rewriter.cpp @@ -704,7 +704,6 @@ br_status seq_rewriter::mk_seq_extract(expr* a, expr* b, expr* c, expr_ref& resu if (!get_lengths(b, lens, pos)) { return BR_FAILED; } - unsigned rsz = lens.size(); unsigned i = 0; for (; i < m_lhs.size(); ++i) { expr* lhs = m_lhs.get(i); diff --git a/src/model/model_evaluator.cpp b/src/model/model_evaluator.cpp index 823d334b3..08edb1001 100644 --- a/src/model/model_evaluator.cpp +++ b/src/model/model_evaluator.cpp @@ -238,8 +238,6 @@ struct evaluator_cfg : public default_rewriter_cfg { func_decl* g = nullptr; VERIFY(m_ar.is_as_array(f, g)); expr* def = nullptr; - quantifier* q = nullptr; - proof* def_pr = nullptr; if (m_def_cache.find(g, def)) { result = def; return BR_DONE; From 77d5b381ead4711c3d73c8be9256382230e82712 Mon Sep 17 00:00:00 2001 From: Daniel Schemmel Date: Tue, 23 Jul 2019 11:12:29 +0200 Subject: [PATCH 2/2] Order initialization to avoid -Wreorder --- src/sat/sat_model_converter.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/sat/sat_model_converter.cpp b/src/sat/sat_model_converter.cpp index 3a951025b..d28a90e93 100644 --- a/src/sat/sat_model_converter.cpp +++ b/src/sat/sat_model_converter.cpp @@ -23,7 +23,7 @@ Revision History: namespace sat { - model_converter::model_converter(): m_solver(nullptr), m_exposed_lim(0) { + model_converter::model_converter(): m_exposed_lim(0), m_solver(nullptr) { } model_converter::~model_converter() {