From db746e0c2f0a4ba446852cf8429cdf0ed3890b42 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Tue, 12 Jan 2016 09:52:16 -0800 Subject: [PATCH] fix more unused variable warning messages Signed-off-by: Nikolaj Bjorner --- src/api/api_fpa.cpp | 8 ++++---- src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h | 1 - src/ast/seq_decl_plugin.cpp | 1 - 3 files changed, 4 insertions(+), 6 deletions(-) diff --git a/src/api/api_fpa.cpp b/src/api/api_fpa.cpp index 90b818b4b..eaffdd226 100644 --- a/src/api/api_fpa.cpp +++ b/src/api/api_fpa.cpp @@ -943,7 +943,7 @@ extern "C" { return ""; } scoped_mpf val(mpfm); - app * a = to_app(e); +// app * a = to_app(e); bool r = plugin->is_numeral(e, val); if (!r || !mpfm.is_regular(val)) { SET_ERROR_CODE(Z3_INVALID_ARG) @@ -981,7 +981,7 @@ extern "C" { return 0; } scoped_mpf val(mpfm); - app * a = to_app(e); +// app * a = to_app(e); bool r = plugin->is_numeral(e, val); const mpz & z = mpfm.sig(val); if (!r || mpfm.is_regular(val)|| !mpzm.is_uint64(z)) { @@ -1012,7 +1012,7 @@ extern "C" { return ""; } scoped_mpf val(mpfm); - app * a = to_app(e); +// app * a = to_app(e); bool r = plugin->is_numeral(e, val); if (!r || !mpfm.is_regular(val)) { SET_ERROR_CODE(Z3_INVALID_ARG); @@ -1044,7 +1044,7 @@ extern "C" { return 0; } scoped_mpf val(mpfm); - app * a = to_app(e); +// app * a = to_app(e); bool r = plugin->is_numeral(e, val); if (!r || !mpfm.is_regular(val)) { SET_ERROR_CODE(Z3_INVALID_ARG); diff --git a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h index 102082cd5..16aef6a00 100644 --- a/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h +++ b/src/ast/rewriter/bit_blaster/bit_blaster_tpl_def.h @@ -1171,7 +1171,6 @@ void bit_blaster_tpl::mk_carry_save_adder(unsigned sz, expr * const * a_bit template bool bit_blaster_tpl::mk_const_case_multiplier(unsigned sz, expr * const * a_bits, expr * const * b_bits, expr_ref_vector & out_bits) { - unsigned nb = 0; unsigned case_size = 1; unsigned circuit_size = sz*sz*5; for (unsigned i = 0; case_size < circuit_size && i < sz; ++i) { diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index e31b168b8..e715ef571 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/src/ast/seq_decl_plugin.cpp @@ -429,7 +429,6 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter if (!parameters[0].is_ast() || !is_sort(parameters[0].get_ast())) { m.raise_exception("invalid regex sort, parameter is not a sort"); } - sort * s = to_sort(parameters[0].get_ast()); return m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, num_parameters, parameters)); } case _STRING_SORT: