mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00
Code Activity

cleanup for warning message

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2017-07-01 11:47:17 -07:00
parent be4b0ffe69
commit 08524a2d90
10 changed files with 32 additions and 29 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

2
src/ast/rewriter/arith_rewriter.cpp
View file

@ -985,7 +985,7 @@ br_status arith_rewriter::mk_power_core(expr * arg1, expr * arg2, expr_ref & res
br_status arith_rewriter::mk_to_int_core(expr * arg, expr_ref & result) {
numeral a;
expr* x;
expr* x = 0;
if (m_util.is_numeral(arg, a)) {
result = m_util.mk_numeral(floor(a), true);
return BR_DONE;

2
src/muz/base/dl_rule_set.cpp
View file

@ -668,7 +668,7 @@ namespace datalog {
T * el = it->m_key;
item_set * out_edges = it->m_value;
unsigned el_comp;
unsigned el_comp = 0;
VERIFY( m_component_nums.find(el, el_comp) );
item_set::iterator eit = out_edges->begin();

2
src/muz/rel/dl_relation_manager.cpp
View file

@ -294,7 +294,7 @@ namespace datalog {
}
table_relation_plugin & relation_manager::get_table_relation_plugin(table_plugin & tp) {
table_relation_plugin * res;
table_relation_plugin * res = 0;
VERIFY( m_table_relation_plugins.find(&tp, res) );
return *res;
}

2
src/opt/wmax.cpp
View file

@ -216,7 +216,7 @@ namespace opt {
rational remove_negations(smt::theory_wmaxsat& th, expr_ref_vector const& core, ptr_vector<expr>& keys, vector<rational>& weights) {
rational min_weight(-1);
for (unsigned i = 0; i < core.size(); ++i) {
expr* e;
expr* e = 0;
VERIFY(m.is_not(core[i], e));
keys.push_back(m_keys[e]);
rational weight = m_weights[e];

2
src/qe/qe_arith_plugin.cpp
View file

@ -2503,7 +2503,7 @@ public:
}
virtual void subst(contains_app& x, rational const& vl, expr_ref& fml, expr_ref* def) {
nlarith::branch_conditions *brs;
nlarith::branch_conditions *brs = 0;
VERIFY (m_cache.find(x.x(), fml, brs));
SASSERT(vl.is_unsigned());
SASSERT(vl.get_unsigned() < brs->size());

1
src/smt/smt_consequences.cpp
View file

@ -103,6 +103,7 @@ namespace smt {
void context::justify(literal lit, index_set& s) {
ast_manager& m = m_manager;
(void)m;
b_justification js = get_justification(lit.var());
switch (js.get_kind()) {
case b_justification::CLAUSE: {

8
src/smt/theory_lra.cpp
View file

@ -765,7 +765,7 @@ namespace smt {
}
void internalize_eq_eh(app * atom, bool_var) {
expr* lhs, *rhs;
expr* lhs = 0, *rhs = 0;
VERIFY(m.is_eq(atom, lhs, rhs));
enode * n1 = get_enode(lhs);
enode * n2 = get_enode(rhs);
@ -892,7 +892,7 @@ namespace smt {
// to_int (to_real x) = x
// to_real(to_int(x)) <= x < to_real(to_int(x)) + 1
void mk_to_int_axiom(app* n) {
expr* x, *y;
expr* x = 0, *y = 0;
VERIFY (a.is_to_int(n, x));
if (a.is_to_real(x, y)) {
mk_axiom(th.mk_eq(y, n, false));
@ -908,7 +908,7 @@ namespace smt {
// is_int(x) <=> to_real(to_int(x)) = x
void mk_is_int_axiom(app* n) {
expr* x;
expr* x = 0;
VERIFY(a.is_is_int(n, x));
literal eq = th.mk_eq(a.mk_to_real(a.mk_to_int(x)), x, false);
literal is_int = ctx().get_literal(n);
@ -1299,12 +1299,14 @@ namespace smt {
return;
}
int num_of_p = m_solver->settings().st().m_num_of_implied_bounds;
(void)num_of_p;
local_bound_propagator bp(*this);
m_solver->propagate_bounds_for_touched_rows(bp);
if (m.canceled()) {
return;
}
int new_num_of_p = m_solver->settings().st().m_num_of_implied_bounds;
(void)new_num_of_p;
CTRACE("arith", new_num_of_p > num_of_p, tout << "found " << new_num_of_p << " implied bounds\n";);
if (m_solver->get_status() == lean::lp_status::INFEASIBLE) {
set_conflict();

34
src/smt/theory_seq.cpp
View file

@ -1074,7 +1074,7 @@ expr_ref theory_seq::mk_first(expr* s) {
void theory_seq::mk_decompose(expr* e, expr_ref& head, expr_ref& tail) {
expr* e1, *e2;
expr* e1 = 0, *e2 = 0;
zstring s;
if (m_util.str.is_empty(e)) {
head = m_util.str.mk_unit(mk_nth(e, m_autil.mk_int(0)));
@ -1401,7 +1401,7 @@ bool theory_seq::occurs(expr* a, expr* b) {
// true if a occurs under an interpreted function or under left/right selector.
SASSERT(is_var(a));
SASSERT(m_todo.empty());
expr* e1, *e2;
expr* e1 = 0, *e2 = 0;
m_todo.push_back(b);
while (!m_todo.empty()) {
b = m_todo.back();
@ -1990,7 +1990,7 @@ bool theory_seq::solve_nc(unsigned idx) {
return true;
}
expr* e1, *e2;
expr* e1 = 0, *e2 = 0;
if (m.is_eq(c, e1, e2)) {
literal eq = mk_eq(e1, e2, false);
propagate_lit(deps, 0, 0, ~eq);
@ -2316,7 +2316,7 @@ bool theory_seq::check_int_string() {
bool theory_seq::add_stoi_axiom(expr* e) {
context& ctx = get_context();
expr* n;
expr* n = 0;
rational val;
TRACE("seq", tout << mk_pp(e, m) << "\n";);
VERIFY(m_util.str.is_stoi(e, n));
@ -2398,7 +2398,7 @@ expr_ref theory_seq::digit2int(expr* ch) {
bool theory_seq::add_itos_axiom(expr* e) {
context& ctx = get_context();
rational val;
expr* n;
expr* n = 0;
TRACE("seq", tout << mk_pp(e, m) << "\n";);
VERIFY(m_util.str.is_itos(e, n));
if (get_num_value(n, val)) {
@ -3197,7 +3197,7 @@ void theory_seq::add_indexof_axiom(expr* i) {
*/
void theory_seq::add_replace_axiom(expr* r) {
expr* a, *s, *t;
expr* a = 0, *s = 0, *t = 0;
VERIFY(m_util.str.is_replace(r, a, s, t));
expr_ref x = mk_skolem(m_indexof_left, a, s);
expr_ref y = mk_skolem(m_indexof_right, a, s);
@ -3330,7 +3330,7 @@ void theory_seq::add_itos_length_axiom(expr* len) {
void theory_seq::propagate_in_re(expr* n, bool is_true) {
TRACE("seq", tout << mk_pp(n, m) << " <- " << (is_true?"true":"false") << "\n";);
expr* e1, *e2;
expr* e1 = 0, *e2 = 0;
VERIFY(m_util.str.is_in_re(n, e1, e2));
expr_ref tmp(n, m);
@ -3462,7 +3462,7 @@ bool theory_seq::get_length(expr* e, rational& val) const {
if (!tha) return false;
rational val1;
expr_ref len(m), len_val(m);
expr* e1, *e2;
expr* e1 = 0, *e2 = 0;
ptr_vector<expr> todo;
todo.push_back(e);
val.reset();
@ -3522,7 +3522,7 @@ bool theory_seq::get_length(expr* e, rational& val) const {
*/
void theory_seq::add_extract_axiom(expr* e) {
expr* s, *i, *l;
expr* s = 0, *i = 0, *l = 0;
VERIFY(m_util.str.is_extract(e, s, i, l));
if (is_tail(s, i, l)) {
add_tail_axiom(e, s);
@ -3682,7 +3682,7 @@ void theory_seq::add_at_axiom(expr* e) {
*/
void theory_seq::propagate_step(literal lit, expr* step) {
SASSERT(get_context().get_assignment(lit) == l_true);
expr* re, *acc, *s, *idx, *i, *j;
expr* re = 0, *acc = 0, *s = 0, *idx = 0, *i = 0, *j = 0;
VERIFY(is_step(step, s, idx, re, i, j, acc));
TRACE("seq", tout << mk_pp(step, m) << " -> " << mk_pp(acc, m) << "\n";);
propagate_lit(0, 1, &lit, mk_literal(acc));
@ -3843,7 +3843,7 @@ void theory_seq::propagate_eq(dependency* deps, literal_vector const& _lits, exp
void theory_seq::assign_eh(bool_var v, bool is_true) {
context & ctx = get_context();
expr* e = ctx.bool_var2expr(v);
expr* e1, *e2;
expr* e1 = 0, *e2 = 0;
expr_ref f(m);
bool change = false;
literal lit(v, !is_true);
@ -4191,7 +4191,7 @@ expr_ref theory_seq::mk_step(expr* s, expr* idx, expr* re, unsigned i, unsigned
rej(s, idx, re, i) -> len(s) > idx if i is final
*/
void theory_seq::propagate_acc_rej_length(literal lit, expr* e) {
expr *s, * idx, *re;
expr *s = 0, *idx = 0, *re = 0;
unsigned src;
eautomaton* aut = 0;
bool is_acc;
@ -4220,7 +4220,7 @@ bool theory_seq::add_accept2step(expr* acc, bool& change) {
TRACE("seq", tout << mk_pp(acc, m) << "\n";);
SASSERT(ctx.get_assignment(acc) == l_true);
expr *e, * idx, *re;
expr *e = 0, *idx = 0, *re = 0;
expr_ref step(m);
unsigned src;
eautomaton* aut = 0;
@ -4299,7 +4299,7 @@ bool theory_seq::add_accept2step(expr* acc, bool& change) {
bool theory_seq::add_step2accept(expr* step, bool& change) {
context& ctx = get_context();
SASSERT(ctx.get_assignment(step) == l_true);
expr* re, *_acc, *s, *idx, *i, *j;
expr* re = 0, *_acc = 0, *s = 0, *idx = 0, *i = 0, *j = 0;
VERIFY(is_step(step, s, idx, re, i, j, _acc));
literal acc1 = mk_accept(s, idx, re, i);
switch (ctx.get_assignment(acc1)) {
@ -4348,7 +4348,7 @@ Recall we also have:
bool theory_seq::add_reject2reject(expr* rej, bool& change) {
context& ctx = get_context();
SASSERT(ctx.get_assignment(rej) == l_true);
expr* s, *idx, *re;
expr* s = 0, *idx = 0, *re = 0;
unsigned src;
rational r;
eautomaton* aut = 0;
@ -4410,7 +4410,7 @@ bool theory_seq::add_reject2reject(expr* rej, bool& change) {
void theory_seq::propagate_not_prefix(expr* e) {
context& ctx = get_context();
expr* e1, *e2;
expr* e1 = 0, *e2 = 0;
VERIFY(m_util.str.is_prefix(e, e1, e2));
literal lit = ctx.get_literal(e);
SASSERT(ctx.get_assignment(lit) == l_false);
@ -4439,7 +4439,7 @@ void theory_seq::propagate_not_prefix(expr* e) {
void theory_seq::propagate_not_prefix2(expr* e) {
context& ctx = get_context();
expr* e1, *e2;
expr* e1 = 0, *e2 = 0;
VERIFY(m_util.str.is_prefix(e, e1, e2));
literal lit = ctx.get_literal(e);
SASSERT(ctx.get_assignment(lit) == l_false);

4
src/tactic/portfolio/bounded_int2bv_solver.cpp
View file

@ -168,7 +168,7 @@ public:
// translate bit-vector consequences back to integer values
for (unsigned i = 0; i < consequences.size(); ++i) {
expr* a, *b, *u, *v;
expr* a = 0, *b = 0, *u = 0, *v = 0;
func_decl* f;
rational num;
unsigned bvsize;
@ -228,7 +228,7 @@ private:
for (; it != end; ++it) {
expr* e = *it;
rational lo, hi;
bool s1, s2;
bool s1 = false, s2 = false;
SASSERT(is_uninterp_const(e));
func_decl* f = to_app(e)->get_decl();

4
src/tactic/portfolio/enum2bv_solver.cpp
View file

@ -116,7 +116,7 @@ public:
// translate enumeration constants to bit-vectors.
for (unsigned i = 0; i < vars.size(); ++i) {
func_decl* f;
func_decl* f = 0;
if (is_app(vars[i]) && is_uninterp_const(vars[i]) && m_rewriter.enum2bv().find(to_app(vars[i])->get_decl(), f)) {
bvars.push_back(m.mk_const(f));
}
@ -128,7 +128,7 @@ public:
// translate bit-vector consequences back to enumeration types
for (unsigned i = 0; i < consequences.size(); ++i) {
expr* a, *b, *u, *v;
expr* a = 0, *b = 0, *u = 0, *v = 0;
func_decl* f;
rational num;
unsigned bvsize;