mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
reduce set of mainly verbose warnings raised by -Wmaybe-uninitialized and unused variable warnings from release mode builds
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
fa6f9b4a37
commit
5b497b6249
|
@ -324,7 +324,7 @@ namespace datalog {
|
|||
if (!is_rel_sort(r, sorts)) {
|
||||
return 0;
|
||||
}
|
||||
unsigned index0;
|
||||
unsigned index0 = 0;
|
||||
sort* last_sort = 0;
|
||||
SASSERT(num_params > 0);
|
||||
for (unsigned i = 0; i < num_params; ++i) {
|
||||
|
|
|
@ -2267,6 +2267,7 @@ void fpa2bv_converter::mk_to_fp(func_decl * f, unsigned num, expr * const * args
|
|||
|
||||
expr * bv = args[0];
|
||||
int sz = m_bv_util.get_bv_size(bv);
|
||||
(void)to_sbits;
|
||||
SASSERT((unsigned)sz == to_sbits + to_ebits);
|
||||
|
||||
result = m_util.mk_fp(m_bv_util.mk_extract(sz - 1, sz - 1, bv),
|
||||
|
@ -2399,6 +2400,7 @@ void fpa2bv_converter::mk_to_fp_float(sort * to_srt, expr * rm, expr * x, expr_r
|
|||
|
||||
res_sig = m_bv_util.mk_zero_extend(1, res_sig); // extra zero in the front for the rounder.
|
||||
unsigned sig_sz = m_bv_util.get_bv_size(res_sig);
|
||||
(void) sig_sz;
|
||||
SASSERT(sig_sz == to_sbits + 4);
|
||||
|
||||
expr_ref exponent_overflow(m), exponent_underflow(m);
|
||||
|
|
|
@ -210,7 +210,7 @@ bool defined_names::impl::mk_name(expr * e, expr_ref & new_def, proof_ref & new_
|
|||
TRACE("mk_definition_bug", tout << "name for expression is already cached..., returning false...\n";);
|
||||
n = n_ptr;
|
||||
if (m_manager.proofs_enabled()) {
|
||||
proof * pr_ptr;
|
||||
proof * pr_ptr = 0;
|
||||
m_expr2proof.find(e, pr_ptr);
|
||||
SASSERT(pr_ptr);
|
||||
pr = pr_ptr;
|
||||
|
|
|
@ -58,7 +58,7 @@ struct pull_quant::imp {
|
|||
}
|
||||
|
||||
bool found_quantifier = false;
|
||||
bool forall_children;
|
||||
bool forall_children = false;
|
||||
|
||||
for (unsigned i = 0; i < num_children; i++) {
|
||||
expr * child = children[i];
|
||||
|
|
|
@ -572,7 +572,7 @@ bool bool_rewriter::local_ctx_simp(unsigned num_args, expr * const * args, expr_
|
|||
|
||||
*/
|
||||
br_status bool_rewriter::try_ite_value(app * ite, app * val, expr_ref & result) {
|
||||
expr* cond, *t, *e;
|
||||
expr* cond = 0, *t = 0, *e = 0;
|
||||
VERIFY(m().is_ite(ite, cond, t, e));
|
||||
SASSERT(m().is_value(val));
|
||||
|
||||
|
|
|
@ -103,8 +103,8 @@ template<typename Config>
|
|||
template<bool ProofGen>
|
||||
bool rewriter_tpl<Config>::visit(expr * t, unsigned max_depth) {
|
||||
TRACE("rewriter_visit", tout << "visiting\n" << mk_ismt2_pp(t, m()) << "\n";);
|
||||
expr * new_t;
|
||||
proof * new_t_pr;
|
||||
expr * new_t = 0;
|
||||
proof * new_t_pr = 0;
|
||||
if (m_cfg.get_subst(t, new_t, new_t_pr)) {
|
||||
TRACE("rewriter_subst", tout << "subst\n" << mk_ismt2_pp(t, m()) << "\n---->\n" << mk_ismt2_pp(new_t, m()) << "\n";);
|
||||
SASSERT(m().get_sort(t) == m().get_sort(new_t));
|
||||
|
|
|
@ -303,7 +303,7 @@ eautomaton* re2automaton::re2aut(expr* e) {
|
|||
}
|
||||
else if (u.re.is_full(e)) {
|
||||
expr_ref tt(m.mk_true(), m);
|
||||
sort* seq_s, *char_s;
|
||||
sort *seq_s = 0, *char_s = 0;
|
||||
VERIFY (u.is_re(m.get_sort(e), seq_s));
|
||||
VERIFY (u.is_seq(seq_s, char_s));
|
||||
sym_expr* _true = sym_expr::mk_pred(tt, char_s);
|
||||
|
@ -794,7 +794,7 @@ br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
|
|||
|
||||
bool isc1 = false;
|
||||
bool isc2 = false;
|
||||
expr* a1, *a2, *b1, *b2;
|
||||
expr *a1 = 0, *a2 = 0, *b1 = 0, *b2 = 0;
|
||||
if (m_util.str.is_concat(a, a1, a2) && m_util.str.is_string(a2, s1)) {
|
||||
isc1 = true;
|
||||
}
|
||||
|
@ -1321,7 +1321,7 @@ br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
|
|||
}
|
||||
|
||||
br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
|
||||
sort* s;
|
||||
sort* s = 0;
|
||||
VERIFY(m_util.is_re(a, s));
|
||||
result = m_util.re.mk_union(m_util.re.mk_to_re(m_util.str.mk_empty(s)), a);
|
||||
return BR_REWRITE1;
|
||||
|
|
|
@ -273,7 +273,7 @@ void bit2int::visit(app* n) {
|
|||
// bv2int(x) <= z - bv2int(y) -> bv2int(x) + bv2int(y) <= z
|
||||
//
|
||||
|
||||
expr* e1, *e2;
|
||||
expr* e1 = 0, *e2 = 0;
|
||||
expr_ref tmp1(m_manager), tmp2(m_manager);
|
||||
expr_ref tmp3(m_manager);
|
||||
expr_ref pos1(m_manager), neg1(m_manager);
|
||||
|
|
|
@ -146,7 +146,7 @@ void substitution::apply(unsigned num_actual_offsets, unsigned const * deltas, e
|
|||
bool has_new_args = false;
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
expr * arg = to_app(e)->get_arg(i);
|
||||
expr * new_arg;
|
||||
expr * new_arg = 0;
|
||||
|
||||
VERIFY(m_apply_cache.find(expr_offset(arg, off), new_arg));
|
||||
new_args.push_back(new_arg);
|
||||
|
|
|
@ -283,7 +283,7 @@ public:
|
|||
++m_stats.m_num_removes;
|
||||
// assumption: key is in table.
|
||||
node* n = m_root;
|
||||
node* m;
|
||||
node* m = 0;
|
||||
for (unsigned i = 0; i < num_keys(); ++i) {
|
||||
n->dec_ref();
|
||||
VERIFY (to_trie(n)->find(get_key(keys, i), m));
|
||||
|
|
|
@ -1035,7 +1035,7 @@ namespace algebraic_numbers {
|
|||
|
||||
unsigned num_rem = 0; // number of remaining sequences
|
||||
unsigned target_i = UINT_MAX; // index of sequence that is isolating
|
||||
int target_lV, target_uV;
|
||||
int target_lV = 0, target_uV = 0;
|
||||
for (unsigned i = 0; i < num_fs; i++) {
|
||||
if (seqs[i] == 0)
|
||||
continue; // sequence was discarded because it does not contain the root.
|
||||
|
@ -1113,7 +1113,7 @@ namespace algebraic_numbers {
|
|||
|
||||
unsigned num_rem = 0; // number of remaining sequences
|
||||
unsigned target_i = UINT_MAX; // index of sequence that is isolating
|
||||
int target_lV, target_uV;
|
||||
int target_lV = 0, target_uV = 0;
|
||||
for (unsigned i = 0; i < num_fs; i++) {
|
||||
if (seqs[i] == 0)
|
||||
continue; // sequence was discarded because it does not contain the root.
|
||||
|
|
|
@ -540,7 +540,7 @@ namespace simplex {
|
|||
var_t max = get_num_vars();
|
||||
var_t result = max;
|
||||
row r = row(m_vars[x_i].m_base2row);
|
||||
int n;
|
||||
int n = 0;
|
||||
unsigned best_col_sz = UINT_MAX;
|
||||
int best_so_far = INT_MAX;
|
||||
|
||||
|
|
|
@ -666,8 +666,8 @@ void model_implicant::eval_eq(app* e, expr* arg1, expr* arg2) {
|
|||
}
|
||||
|
||||
void model_implicant::eval_basic(app* e) {
|
||||
expr* arg1, *arg2;
|
||||
expr *argCond, *argThen, *argElse, *arg;
|
||||
expr* arg1 = 0, *arg2 = 0;
|
||||
expr *argCond = 0, *argThen = 0, *argElse = 0, *arg = 0;
|
||||
bool has_x = false;
|
||||
unsigned arity = e->get_num_args();
|
||||
switch(e->get_decl_kind()) {
|
||||
|
|
|
@ -601,7 +601,7 @@ namespace datalog {
|
|||
return;
|
||||
}
|
||||
while (!m_stack_P.empty()) {
|
||||
unsigned on_stack_num;
|
||||
unsigned on_stack_num = 0;
|
||||
VERIFY( m_preorder_nums.find(m_stack_P.back(), on_stack_num) );
|
||||
if (on_stack_num <= p_num) {
|
||||
break;
|
||||
|
@ -710,7 +710,7 @@ namespace datalog {
|
|||
item_set::iterator eend=deps.end();
|
||||
for (; eit!=eend; ++eit) {
|
||||
T * tgt = *eit;
|
||||
unsigned tgt_comp;
|
||||
unsigned tgt_comp = 0;
|
||||
VERIFY( m_component_nums.find(tgt, tgt_comp) );
|
||||
|
||||
//m_components[tgt_comp]==0 means the edge is intra-component.
|
||||
|
|
|
@ -836,7 +836,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
void compile_eq(expr* e, expr_ref& result, var* v, unsigned hi, unsigned lo, expr* c) {
|
||||
tbv* t;
|
||||
tbv* t = 0;
|
||||
// TBD: hi, lo are ignored.
|
||||
VERIFY(m_expr2tbv.find(e, t));
|
||||
var_ref w(m);
|
||||
|
|
|
@ -274,7 +274,7 @@ namespace pdr {
|
|||
|
||||
for (unsigned i = 0; i < src.size(); ) {
|
||||
expr * curr = src[i].get();
|
||||
unsigned stored_lvl;
|
||||
unsigned stored_lvl = 0;
|
||||
VERIFY(m_prop2level.find(curr, stored_lvl));
|
||||
SASSERT(stored_lvl >= src_level);
|
||||
bool assumes_level;
|
||||
|
|
|
@ -247,7 +247,7 @@ namespace pdr {
|
|||
}
|
||||
|
||||
bool test_eq(expr* e) const {
|
||||
expr* lhs, *rhs;
|
||||
expr* lhs = 0, *rhs = 0;
|
||||
VERIFY(m.is_eq(e, lhs, rhs));
|
||||
if (!a.is_int_real(lhs)) {
|
||||
return true;
|
||||
|
|
|
@ -466,7 +466,7 @@ namespace datalog {
|
|||
|
||||
//used to save on filter_identical instructions where the check is already done
|
||||
//by the join operation
|
||||
unsigned second_tail_arg_ofs;
|
||||
unsigned second_tail_arg_ofs = 0;
|
||||
|
||||
// whether to dealloc the previous result
|
||||
bool dealloc = true;
|
||||
|
|
|
@ -109,7 +109,7 @@ namespace datalog {
|
|||
rule_vector const& rv = *(it->m_value);
|
||||
bool has_symmetry = false;
|
||||
bool has_transitivity = false;
|
||||
unsigned i_symmetry, i_transitivity;
|
||||
unsigned i_symmetry = 0, i_transitivity = 0;
|
||||
family_id kind = rm.get_requested_predicate_kind(p);
|
||||
for (unsigned i = 0; i < rv.size(); ++i) {
|
||||
|
||||
|
|
|
@ -277,7 +277,7 @@ namespace datalog {
|
|||
relation_plugin & relation_manager::get_relation_plugin(family_id kind) {
|
||||
SASSERT(kind>=0);
|
||||
SASSERT(kind<m_next_relation_fid);
|
||||
relation_plugin * res;
|
||||
relation_plugin * res = 0;
|
||||
VERIFY(m_kind2plugin.find(kind, res));
|
||||
return *res;
|
||||
}
|
||||
|
|
|
@ -327,8 +327,7 @@ namespace datalog {
|
|||
key_value key;
|
||||
key.resize(key_len);
|
||||
|
||||
offset_vector * index_entry;
|
||||
DEBUG_CODE( index_entry = 0; );
|
||||
offset_vector * index_entry = 0;
|
||||
bool key_modified = true;
|
||||
|
||||
for (; ofs!=after_last; ofs+=t.m_fact_size) {
|
||||
|
|
|
@ -56,7 +56,7 @@ namespace datalog {
|
|||
|
||||
app_ref mk_loop_counter::del_arg(app* fn) {
|
||||
expr_ref_vector args(m);
|
||||
func_decl* old_fn, *new_fn = fn->get_decl();
|
||||
func_decl* old_fn = 0, *new_fn = fn->get_decl();
|
||||
SASSERT(fn->get_num_args() > 0);
|
||||
args.append(fn->get_num_args()-1, fn->get_args());
|
||||
VERIFY (m_new2old.find(new_fn, old_fn));
|
||||
|
|
|
@ -264,7 +264,7 @@ namespace datalog {
|
|||
}
|
||||
|
||||
|
||||
func_decl * new_head_pred;
|
||||
func_decl * new_head_pred = 0;
|
||||
VERIFY( m_adorned_preds.find(adornment_desc(head->get_decl(), head_adornment), new_head_pred) );
|
||||
app * new_head = m.mk_app(new_head_pred, head->get_args());
|
||||
|
||||
|
|
|
@ -317,7 +317,6 @@ namespace datalog {
|
|||
unsigned tail_index = 0;
|
||||
while (tail_index < utail_len) {
|
||||
app * t = r->get_tail(tail_index);
|
||||
func_decl * t_pred = t->get_decl();
|
||||
|
||||
add_in_progress_indices(arg_indices, t);
|
||||
|
||||
|
|
|
@ -140,7 +140,7 @@ class nlsat_tactic : public tactic {
|
|||
m_solver.set_display_var(m_display_var);
|
||||
|
||||
lbool st = m_solver.check();
|
||||
|
||||
|
||||
if (st == l_undef) {
|
||||
}
|
||||
else if (st == l_true) {
|
||||
|
|
|
@ -345,10 +345,9 @@ namespace opt {
|
|||
}
|
||||
|
||||
expr_ref opt_solver::mk_ge(unsigned var, inf_eps const& val) {
|
||||
if (!val.is_finite())
|
||||
{
|
||||
return expr_ref(val.is_pos() ? m.mk_false() : m.mk_true(), m);
|
||||
}
|
||||
if (!val.is_finite()) {
|
||||
return expr_ref(val.is_pos() ? m.mk_false() : m.mk_true(), m);
|
||||
}
|
||||
smt::theory_opt& opt = get_optimizer();
|
||||
smt::theory_var v = m_objective_vars[var];
|
||||
|
||||
|
|
|
@ -362,7 +362,7 @@ namespace qe {
|
|||
}
|
||||
app* ite;
|
||||
if (find_ite(fml, ite)) {
|
||||
expr* cond, *th, *el;
|
||||
expr* cond = 0, *th = 0, *el = 0;
|
||||
VERIFY(m.is_ite(ite, cond, th, el));
|
||||
expr_ref tmp1(fml, m), tmp2(fml, m);
|
||||
m_replace->apply_substitution(ite, th, tmp1);
|
||||
|
|
|
@ -673,7 +673,7 @@ namespace qe {
|
|||
}
|
||||
|
||||
unsigned find_max(model& mdl, bool do_pos) {
|
||||
unsigned result;
|
||||
unsigned result = 0;
|
||||
bool new_max = true;
|
||||
rational max_r, r;
|
||||
expr_ref val(m);
|
||||
|
|
|
@ -2445,7 +2445,7 @@ public:
|
|||
}
|
||||
|
||||
virtual void assign(contains_app& x, expr* fml, rational const& vl) {
|
||||
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());
|
||||
|
|
|
@ -792,9 +792,8 @@ namespace qe {
|
|||
TRACE("qe", tout << mk_pp(x.x(), m) << " has a recognizer\n";);
|
||||
}
|
||||
else {
|
||||
unsigned sz = m_datatype_util.get_datatype_num_constructors(s);
|
||||
SASSERT(vl.is_unsigned());
|
||||
SASSERT(vl.get_unsigned() < sz);
|
||||
SASSERT(vl.get_unsigned() < m_datatype_util.get_datatype_num_constructors(s));
|
||||
c = (*m_datatype_util.get_datatype_constructors(s))[vl.get_unsigned()];
|
||||
}
|
||||
subst_constructor(x, c, fml, def);
|
||||
|
|
|
@ -1667,7 +1667,7 @@ namespace fm {
|
|||
sbuffer<var> xs;
|
||||
buffer<rational> as;
|
||||
rational c;
|
||||
bool strict;
|
||||
bool strict = false;
|
||||
unsigned num;
|
||||
expr * const * args;
|
||||
if (m.is_or(f)) {
|
||||
|
|
|
@ -70,9 +70,9 @@ namespace sat {
|
|||
tout << "watch_list:\n";
|
||||
sat::display(tout, s.m_cls_allocator, s.get_wlist(~c[0]));
|
||||
tout << "\n";);
|
||||
SASSERT(contains_watched(s.get_wlist(~c[0]), c[1], c[2]));
|
||||
SASSERT(contains_watched(s.get_wlist(~c[1]), c[0], c[2]));
|
||||
SASSERT(contains_watched(s.get_wlist(~c[2]), c[0], c[1]));
|
||||
VERIFY(contains_watched(s.get_wlist(~c[0]), c[1], c[2]));
|
||||
VERIFY(contains_watched(s.get_wlist(~c[1]), c[0], c[2]));
|
||||
VERIFY(contains_watched(s.get_wlist(~c[2]), c[0], c[1]));
|
||||
}
|
||||
else {
|
||||
if (s.value(c[0]) == l_false || s.value(c[1]) == l_false) {
|
||||
|
|
|
@ -42,7 +42,7 @@ namespace sat {
|
|||
// if it->get_kind() == BLOCK_LIT, then it might be the case that m[it->var()] != l_undef,
|
||||
// and the following procedure flips its value.
|
||||
bool sat = false;
|
||||
bool var_sign;
|
||||
bool var_sign = false;
|
||||
literal_vector::const_iterator it2 = it->m_clauses.begin();
|
||||
literal_vector::const_iterator end2 = it->m_clauses.end();
|
||||
for (; it2 != end2; ++it2) {
|
||||
|
|
|
@ -381,7 +381,7 @@ private:
|
|||
|
||||
m_core.reset();
|
||||
for (unsigned i = 0; i < core.size(); ++i) {
|
||||
expr* e;
|
||||
expr* e = 0;
|
||||
VERIFY(asm2dep.find(core[i].index(), e));
|
||||
m_core.push_back(e);
|
||||
}
|
||||
|
|
|
@ -2147,7 +2147,7 @@ namespace smt {
|
|||
enode_vector * best_v = 0;
|
||||
for (unsigned i = 0; i < num_args; i++) {
|
||||
enode * bare = c->m_joints[i];
|
||||
enode_vector * curr_v;
|
||||
enode_vector * curr_v = 0;
|
||||
switch (GET_TAG(bare)) {
|
||||
case NULL_TAG:
|
||||
curr_v = 0;
|
||||
|
|
|
@ -183,7 +183,7 @@ public:
|
|||
sort_info* s_info = s->get_info();
|
||||
sort_size const* sz = s_info?&s_info->get_num_elements():0;
|
||||
bool has_max = false;
|
||||
Number max_size;
|
||||
Number max_size(0);
|
||||
if (sz && sz->is_finite() && sz->size() < UINT_MAX) {
|
||||
unsigned usz = static_cast<unsigned>(sz->size());
|
||||
max_size = Number(usz);
|
||||
|
|
|
@ -363,7 +363,7 @@ namespace smt {
|
|||
<< ", scope_level: " << m_context.get_scope_level() << "\n";);
|
||||
if (m_params.m_qi_conservative_final_check) {
|
||||
bool init = false;
|
||||
float min_cost;
|
||||
float min_cost = 0.0;
|
||||
unsigned sz = m_delayed_entries.size();
|
||||
for (unsigned i = 0; i < sz; i++) {
|
||||
entry & e = m_delayed_entries[i];
|
||||
|
|
|
@ -2790,7 +2790,7 @@ void theory_seq::tightest_prefix(expr* s, expr* x) {
|
|||
(len(s) <= len(t) -> i <= len(t)-len(s))
|
||||
*/
|
||||
void theory_seq::add_indexof_axiom(expr* i) {
|
||||
expr* s, *t, *offset = 0;
|
||||
expr* s = 0, *t = 0, *offset = 0;
|
||||
rational r;
|
||||
VERIFY(m_util.str.is_index(i, t, s) ||
|
||||
m_util.str.is_index(i, t, s, offset));
|
||||
|
@ -2891,7 +2891,7 @@ void theory_seq::add_elim_string_axiom(expr* n) {
|
|||
*/
|
||||
void theory_seq::add_length_axiom(expr* n) {
|
||||
context& ctx = get_context();
|
||||
expr* x;
|
||||
expr* x = 0;
|
||||
VERIFY(m_util.str.is_length(n, x));
|
||||
if (m_util.str.is_concat(x) ||
|
||||
m_util.str.is_unit(x) ||
|
||||
|
@ -2914,7 +2914,7 @@ void theory_seq::add_length_axiom(expr* n) {
|
|||
}
|
||||
|
||||
void theory_seq::add_itos_length_axiom(expr* len) {
|
||||
expr* x, *n;
|
||||
expr* x = 0, *n = 0;
|
||||
VERIFY(m_util.str.is_length(len, x));
|
||||
VERIFY(m_util.str.is_itos(x, n));
|
||||
|
||||
|
@ -3295,7 +3295,7 @@ void theory_seq::add_extract_suffix_axiom(expr* e, expr* s, expr* i) {
|
|||
|
||||
*/
|
||||
void theory_seq::add_at_axiom(expr* e) {
|
||||
expr* s, *i;
|
||||
expr* s = 0, *i = 0;
|
||||
VERIFY(m_util.str.is_at(e, s, i));
|
||||
expr_ref len_e(m_util.str.mk_length(e), m);
|
||||
expr_ref len_s(m_util.str.mk_length(s), m);
|
||||
|
@ -4090,7 +4090,7 @@ void theory_seq::propagate_not_prefix2(expr* e) {
|
|||
|
||||
void theory_seq::propagate_not_suffix(expr* e) {
|
||||
context& ctx = get_context();
|
||||
expr* e1, *e2;
|
||||
expr* e1 = 0, *e2 = 0;
|
||||
VERIFY(m_util.str.is_suffix(e, e1, e2));
|
||||
literal lit = ctx.get_literal(e);
|
||||
SASSERT(ctx.get_assignment(lit) == l_false);
|
||||
|
@ -4119,7 +4119,7 @@ void theory_seq::propagate_not_suffix(expr* e) {
|
|||
*/
|
||||
bool theory_seq::add_prefix2prefix(expr* e, bool& change) {
|
||||
context& ctx = get_context();
|
||||
expr* e1, *e2;
|
||||
expr* e1 = 0, *e2 = 0;
|
||||
VERIFY(m_util.str.is_prefix(e, e1, e2));
|
||||
SASSERT(ctx.get_assignment(e) == l_false);
|
||||
if (canonizes(false, e)) {
|
||||
|
@ -4191,7 +4191,7 @@ bool theory_seq::add_prefix2prefix(expr* e, bool& change) {
|
|||
*/
|
||||
bool theory_seq::add_suffix2suffix(expr* e, bool& change) {
|
||||
context& ctx = get_context();
|
||||
expr* e1, *e2;
|
||||
expr* e1 = 0, *e2 = 0;
|
||||
VERIFY(m_util.str.is_suffix(e, e1, e2));
|
||||
SASSERT(ctx.get_assignment(e) == l_false);
|
||||
if (canonizes(false, e)) {
|
||||
|
@ -4276,7 +4276,7 @@ bool theory_seq::canonizes(bool sign, expr* e) {
|
|||
|
||||
bool theory_seq::add_contains2contains(expr* e, bool& change) {
|
||||
context& ctx = get_context();
|
||||
expr* e1, *e2;
|
||||
expr* e1 = 0, *e2 = 0;
|
||||
VERIFY(m_util.str.is_contains(e, e1, e2));
|
||||
SASSERT(ctx.get_assignment(e) == l_false);
|
||||
if (canonizes(false, e)) {
|
||||
|
@ -4346,7 +4346,7 @@ bool theory_seq::propagate_automata() {
|
|||
}
|
||||
|
||||
void theory_seq::get_concat(expr* e, ptr_vector<expr>& concats) {
|
||||
expr* e1, *e2;
|
||||
expr* e1 = 0, *e2 = 0;
|
||||
while (true) {
|
||||
e = m_rep.find(e);
|
||||
if (m_util.str.is_concat(e, e1, e2)) {
|
||||
|
|
|
@ -993,7 +993,7 @@ class fm_tactic : public tactic {
|
|||
sbuffer<var> xs;
|
||||
buffer<rational> as;
|
||||
rational c;
|
||||
bool strict;
|
||||
bool strict = false;
|
||||
unsigned num;
|
||||
expr * const * args;
|
||||
if (m.is_or(f)) {
|
||||
|
|
|
@ -147,11 +147,10 @@ class elim_small_bv_tactic : public tactic {
|
|||
expr_ref body(old_body, m);
|
||||
for (unsigned i = num_decls-1; i != ((unsigned)-1) && !max_steps_exceeded(num_steps); i--) {
|
||||
sort * s = q->get_decl_sort(i);
|
||||
symbol const & name = q->get_decl_name(i);
|
||||
unsigned bv_sz = m_util.get_bv_size(s);
|
||||
|
||||
if (is_small_bv(s) && !max_steps_exceeded(num_steps)) {
|
||||
TRACE("elim_small_bv", tout << "eliminating " << name <<
|
||||
TRACE("elim_small_bv", tout << "eliminating " << q->get_decl_name(i) <<
|
||||
"; sort = " << mk_ismt2_pp(s, m) <<
|
||||
"; body = " << mk_ismt2_pp(body, m) << std::endl;);
|
||||
|
||||
|
|
|
@ -176,7 +176,7 @@ private:
|
|||
app_map coloring;
|
||||
app_map depth;
|
||||
inv_app_map inv_color;
|
||||
unsigned num_occs;
|
||||
unsigned num_occs = 0;
|
||||
compute_sort_colors(fml, coloring);
|
||||
compute_max_depth(fml, depth);
|
||||
merge_colors(occs, coloring);
|
||||
|
@ -233,7 +233,7 @@ private:
|
|||
typedef map<u_pair, unsigned, u_pair::hash, u_pair::eq> pair_map;
|
||||
bool merge_colors(app_map const& colors1, app_map& colors2) {
|
||||
pair_map recolor;
|
||||
unsigned num_colors = 0, v1, v2, w, old_max = 0;
|
||||
unsigned num_colors = 0, v1 = 0, v2 = 0, w = 0, old_max = 0;
|
||||
app_map::iterator it = colors2.begin(), end = colors2.end();
|
||||
for (; it != end; ++it) {
|
||||
app* a = it->m_key;
|
||||
|
@ -545,7 +545,7 @@ private:
|
|||
term_set& cts, term_set const& consts, app_map const& occs) {
|
||||
SASSERT(!T.empty());
|
||||
app* t = T[0];
|
||||
unsigned weight, weight1;
|
||||
unsigned weight = 0, weight1 = 0;
|
||||
VERIFY(occs.find(t, weight));
|
||||
unsigned cts_delta = compute_cts_delta(t, cts, consts);
|
||||
TRACE("symmetry_reduce", tout << mk_pp(t, m()) << " " << weight << " " << cts_delta << "\n";);
|
||||
|
@ -559,9 +559,9 @@ private:
|
|||
TRACE("symmetry_reduce", tout << mk_pp(t1, m()) << " " << weight1 << " " << cts_delta1 << "\n";);
|
||||
if ((t->get_num_args() == t1->get_num_args() && (weight1 > weight || cts_delta1 < cts_delta)) ||
|
||||
t->get_num_args() > t1->get_num_args()) {
|
||||
cts_delta = cts_delta1;
|
||||
weight = weight1;
|
||||
t = t1;
|
||||
cts_delta = cts_delta1;
|
||||
weight = weight1;
|
||||
t = t1;
|
||||
}
|
||||
}
|
||||
return t;
|
||||
|
|
|
@ -154,8 +154,7 @@ public:
|
|||
|
||||
void mk_interface_bool(func_decl * f, unsigned num, expr* const* args, expr_ref& result, proof_ref& pr) {
|
||||
expr_ref old_pred(m.mk_app(f, num, args), m);
|
||||
polarity_t pol;
|
||||
VERIFY(m_polarities.find(old_pred, pol));
|
||||
polarity_t pol = m_polarities.find(old_pred);
|
||||
result = m.mk_fresh_const(0, m.mk_bool_sort());
|
||||
m_polarities.insert(result, pol);
|
||||
m_new_preds.push_back(to_app(result));
|
||||
|
|
|
@ -48,7 +48,7 @@ tactic * or_else(tactic * t1, tactic * t2, tactic * t3, tactic * t4, tactic * t5
|
|||
tactic * repeat(tactic * t, unsigned max = UINT_MAX);
|
||||
/**
|
||||
\brief Fails if \c t produeces more than \c threshold subgoals.
|
||||
Otherwise, it behabes like \c t.
|
||||
Otherwise, it behaves like \c t.
|
||||
*/
|
||||
tactic * fail_if_branching(tactic * t, unsigned threshold = 1);
|
||||
|
||||
|
|
|
@ -1290,6 +1290,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
|
|||
m_mpz_manager.machine_div2k(Q_sig, sbits+3);
|
||||
renormalize(ebits, sbits, Q_exp, Q_sig);
|
||||
|
||||
(void)Q_sgn;
|
||||
TRACE("mpf_dbg_rem", tout << "Q_exp=" << Q_exp << std::endl;
|
||||
tout << "Q_sig=" << m_mpz_manager.to_string(Q_sig) << std::endl;
|
||||
tout << "Q=" << to_string_hexfloat(Q_sgn, Q_exp, Q_sig, ebits, sbits, 0) << std::endl;);
|
||||
|
@ -1310,6 +1311,7 @@ void mpf_manager::partial_remainder(mpf & x, mpf const & y, mpf_exp_t const & ex
|
|||
m_mpz_manager.mul(y.significand, Q_sig, YQ_sig);
|
||||
renormalize(ebits, 2*sbits-1, YQ_exp, YQ_sig); // YQ_sig has `sbits-1' extra bits.
|
||||
|
||||
(void)YQ_sgn;
|
||||
TRACE("mpf_dbg_rem", tout << "YQ_sgn=" << YQ_sgn << std::endl;
|
||||
tout << "YQ_exp=" << YQ_exp << std::endl;
|
||||
tout << "YQ_sig=" << m_mpz_manager.to_string(YQ_sig) << std::endl;
|
||||
|
|
Loading…
Reference in a new issue