mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-23 09:05:31 +00:00
Code Activity

Removed unnecessary variables and added initialization to others to silence warnings.

Browse source 
Signed-off-by: Christoph M. Wintersteiger <cwinter@microsoft.com>
This commit is contained in:
Christoph M. Wintersteiger 2015-02-07 14:47:26 +00:00
parent b96551a1a2
commit 359c7e4da9
4 changed files with 5 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/ast.cpp
View file

@ -1662,7 +1662,7 @@ ast * ast_manager::register_node_core(ast * n) {
for (unsigned i = 0; i < num_args; i++) {
expr * arg = t->get_arg(i);
inc_ref(arg);
unsigned arg_depth;
unsigned arg_depth = 0;
switch (arg->get_kind()) {
case AST_APP: {
app_flags * arg_flags = to_app(arg)->flags();

2
src/ast/fpa_decl_plugin.cpp
View file

@ -252,7 +252,7 @@ func_decl * fpa_decl_plugin::mk_rm_const_decl(decl_kind k, unsigned num_paramete
func_decl * fpa_decl_plugin::mk_float_const_decl(decl_kind k, unsigned num_parameters, parameter const * parameters,
unsigned arity, sort * const * domain, sort * range) {
sort * s;
sort * s = 0;
if (num_parameters == 1 && parameters[0].is_ast() && is_sort(parameters[0].get_ast()) && is_float_sort(to_sort(parameters[0].get_ast()))) {
s = to_sort(parameters[0].get_ast());
}

6
src/ast/rewriter/fpa_rewriter.cpp
View file

@ -724,8 +724,7 @@ br_status fpa_rewriter::mk_to_ubv(func_decl * f, expr * arg1, expr * arg2, expr_
scoped_mpq q(m_fm.mpq_manager());
m_fm.to_sbv_mpq(rmv, v, q);
rational r(q);
unsynch_mpz_manager & mpzm = m_fm.mpz_manager();
rational r(q);
rational ul, ll;
ul = m_fm.m_powers2.m1(bv_sz);
ll = rational(0);
@ -758,8 +757,7 @@ br_status fpa_rewriter::mk_to_sbv(func_decl * f, expr * arg1, expr * arg2, expr_
scoped_mpq q(m_fm.mpq_manager());
m_fm.to_sbv_mpq(rmv, v, q);
rational r(q);
unsynch_mpz_manager & mpzm = m_fm.mpz_manager();
rational r(q);
rational ul, ll;
ul = m_fm.m_powers2.m1(bv_sz - 1);
ll = - m_fm.m_powers2(bv_sz - 1);