mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-27 00:18:45 +00:00
Code Activity

warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-04-15 17:13:02 -07:00
parent d465938496
commit f67077b7ff
6 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -393,7 +393,7 @@ void seq_rewriter::updt_params(params_ref const & p) {
m_coalesce_chars = sp.coalesce_chars(); m_coalesce_chars = sp.coalesce_chars();
} }
static void get_param_descrs(param_descrs & r) { void seq_rewriter::get_param_descrs(param_descrs & r) {
seq_rewriter_params::collect_param_descrs(r); seq_rewriter_params::collect_param_descrs(r);
} }

1
src/muz/spacer/spacer_context.cpp
View file

@ -1115,7 +1115,6 @@ expr_ref pred_transformer::get_cover_delta(func_decl* p_orig, int level)
(*rep)(result); (*rep)(result);
// adjust result according to model converter. // adjust result according to model converter.
unsigned arity = m_head->get_arity();
model_ref md = alloc(model, m); model_ref md = alloc(model, m);
md->register_decl(m_head, result); md->register_decl(m_head, result);
model_converter_ref mc = ctx.get_model_converter(); model_converter_ref mc = ctx.get_model_converter();

1
src/muz/transforms/dl_mk_quantifier_abstraction.cpp
View file

@ -74,7 +74,6 @@ namespace datalog {
bool_vector const& is_bound = m_bound[i]; bool_vector const& is_bound = m_bound[i];
func_interp* f = old_model->get_func_interp(p); func_interp* f = old_model->get_func_interp(p);
expr_ref body(m); expr_ref body(m);
unsigned arity_q = q->get_arity();
SASSERT(0 < p->get_arity()); SASSERT(0 < p->get_arity());
if (f) { if (f) {

2
src/smt/theory_recfun.cpp
View file

@ -33,8 +33,8 @@ namespace smt {
m(m), m(m),
m_plugin(*reinterpret_cast<recfun::decl::plugin*>(m.get_plugin(get_family_id()))), m_plugin(*reinterpret_cast<recfun::decl::plugin*>(m.get_plugin(get_family_id()))),
m_util(m_plugin.u()), m_util(m_plugin.u()),
m_preds(m),
m_disabled_guards(m), m_disabled_guards(m),
m_preds(m),
m_enabled_guards(m), m_enabled_guards(m),
m_num_rounds(0), m_num_rounds(0),
m_q_case_expand(), m_q_case_expand(),

1
src/smt/theory_seq.cpp
View file

@ -4442,7 +4442,6 @@ model_value_proc * theory_seq::mk_value(enode * n, model_generator & mg) {
app* theory_seq::mk_value(app* e) { app* theory_seq::mk_value(app* e) {
expr_ref result(m); expr_ref result(m);
expr* e0 = e;
e = get_ite_value(e); e = get_ite_value(e);
result = m_rep.find(e); result = m_rep.find(e);

5
src/smt/theory_utvpi_def.h
View file

@ -507,6 +507,7 @@ namespace smt {
while (consistent && can_propagate()) { while (consistent && can_propagate()) {
unsigned idx = m_asserted_atoms[m_asserted_qhead]; unsigned idx = m_asserted_atoms[m_asserted_qhead];
m_asserted_qhead++; m_asserted_qhead++;
std::cout << "propagate atom " << idx << "\n";
consistent = propagate_atom(m_atoms[idx]); consistent = propagate_atom(m_atoms[idx]);
} }
} }
@ -656,7 +657,9 @@ namespace smt {
SASSERT(v2 != null_theory_var); SASSERT(v2 != null_theory_var);
SASSERT(pos2 || terms[1].second.is_minus_one()); SASSERT(pos2 || terms[1].second.is_minus_one());
} }
TRACE("utvpi", tout << (pos1?"$":"-$") << v1 << (pos2?" + $":" - $") << v2 << " + " << weight << " <= 0\n";); TRACE("utvpi", tout << (pos1?"$":"-$") << v1;
if (terms.size() == 2) tout << (pos2?" + $":" - $") << v2;
tout << " + " << weight << " <= 0\n";);
edge_id id = m_graph.get_num_edges(); edge_id id = m_graph.get_num_edges();
th_var w1 = to_var(v1), w2 = to_var(v2); th_var w1 = to_var(v1), w2 = to_var(v2);