mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-03 21:01:22 +00:00
Code Activity

Merge pull request #2428 from danielschemmel/warnings

Browse source 
Fix Some Warnings
This commit is contained in:
Nikolaj Bjorner 2019-07-23 08:45:34 -07:00 • committed by GitHub
commit df04d7f108
No known key found for this signature in database
GPG key ID: 4AEE18F83AFDEB23
3 changed files with 1 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/rewriter/seq_rewriter.cpp
View file

@ -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)) { if (!get_lengths(b, lens, pos)) {
return BR_FAILED; return BR_FAILED;
} }
unsigned rsz = lens.size();
unsigned i = 0; unsigned i = 0;
for (; i < m_lhs.size(); ++i) { for (; i < m_lhs.size(); ++i) {
expr* lhs = m_lhs.get(i); expr* lhs = m_lhs.get(i);

2
src/model/model_evaluator.cpp
View file

@ -238,8 +238,6 @@ struct evaluator_cfg : public default_rewriter_cfg {
func_decl* g = nullptr; func_decl* g = nullptr;
VERIFY(m_ar.is_as_array(f, g)); VERIFY(m_ar.is_as_array(f, g));
expr* def = nullptr; expr* def = nullptr;
quantifier* q = nullptr;
proof* def_pr = nullptr;
if (m_def_cache.find(g, def)) { if (m_def_cache.find(g, def)) {
result = def; result = def;
return BR_DONE; return BR_DONE;

2
src/sat/sat_model_converter.cpp
View file

@ -23,7 +23,7 @@ Revision History:
namespace sat { 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() { model_converter::~model_converter() {