mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-02 23:27:53 +00:00
Code Activity

fix build warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-11-26 09:43:52 -08:00
parent 032a3a879b
commit 08babfff60
6 changed files with 4 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

1
src/ast/euf/euf_arith_plugin.cpp
View file

@ -59,7 +59,6 @@ namespace euf {
expr* e = n->get_expr(), * x, * y; expr* e = n->get_expr(), * x, * y;
// x - y = x + (* -1 y) // x - y = x + (* -1 y)
if (a.is_sub(e, x, y)) { if (a.is_sub(e, x, y)) {
auto& m = g.get_manager();
auto e1 = a.mk_numeral(rational(-1), a.is_int(x)); auto e1 = a.mk_numeral(rational(-1), a.is_int(x));
auto n1 = g.find(e1) ? g.find(e1) : g.mk(e1, 0, 0, nullptr); auto n1 = g.find(e1) ? g.find(e1) : g.mk(e1, 0, 0, nullptr);
auto e2 = a.mk_mul(e1, y); auto e2 = a.mk_mul(e1, y);

3
src/ast/euf/ho_matcher.cpp
View file

@ -293,8 +293,7 @@ namespace euf {
// v - offset |-> t // v - offset |-> t
if (is_meta_var(p, wi.pat_offset()) && is_closed(t, 0, wi.term_offset())) { if (is_meta_var(p, wi.pat_offset()) && is_closed(t, 0, wi.term_offset())) {
auto v = to_var(p); auto v = to_var(p);
auto idx = v->get_idx() - wi.pat_offset(); SASSERT(!m_subst.get(v->get_idx() - wi.pat_offset())); // reduce ensures meta variables are not in substitutions
SASSERT(!m_subst.get(idx)); // reduce ensures meta variables are not in substitutions
add_binding(v, wi.pat_offset(), t); add_binding(v, wi.pat_offset(), t);
wi.set_done(); wi.set_done();
return true; return true;

2
src/ast/simplifiers/euf_completion.cpp
View file

@ -1088,7 +1088,7 @@ namespace euf {
verbose_stream() << mk_pp(s->get_expr(), m) << "\n"; verbose_stream() << mk_pp(s->get_expr(), m) << "\n";
} }
#endif #endif
auto n = m_egraph.find(q); // auto n = m_egraph.find(q);
#if 0 #if 0
verbose_stream() << "class of " << mk_pp(q, m) << "\n"; verbose_stream() << "class of " << mk_pp(q, m) << "\n";
for (auto s : euf::enode_class(n)) { for (auto s : euf::enode_class(n)) {

3
src/nlsat/nlsat_solver.cpp
View file

@ -984,8 +984,7 @@ namespace nlsat {
lbool val = l_undef; lbool val = l_undef;
// Arithmetic atom: evaluate directly // Arithmetic atom: evaluate directly
var max = a->max_var(); SASSERT(debug_assignment.is_assigned(a->max_var()));
SASSERT(debug_assignment.is_assigned(max));
val = to_lbool(debug_evaluator.eval(a, l.sign())); val = to_lbool(debug_evaluator.eval(a, l.sign()));
SASSERT(val != l_undef); SASSERT(val != l_undef);
if (val == l_true) if (val == l_true)

2
src/smt/smt_parallel.cpp
View file

@ -131,7 +131,7 @@ namespace smt {
} }
parallel::worker::worker(unsigned id, parallel &p, expr_ref_vector const &_asms) parallel::worker::worker(unsigned id, parallel &p, expr_ref_vector const &_asms)
: id(id), p(p), b(p.m_batch_manager), m_smt_params(p.ctx.get_fparams()), asms(m), m_g2l(p.ctx.m, m), : id(id), p(p), b(p.m_batch_manager), asms(m), m_smt_params(p.ctx.get_fparams()), m_g2l(p.ctx.m, m),
m_l2g(m, p.ctx.m) { m_l2g(m, p.ctx.m) {
for (auto e : _asms) for (auto e : _asms)
asms.push_back(m_g2l(e)); asms.push_back(m_g2l(e));

1
src/smt/smt_relevancy.cpp
View file

@ -385,7 +385,6 @@ namespace smt {
case l_undef: case l_undef:
break; break;
case l_true: { case l_true: {
expr* true_arg = nullptr;
auto arg0 = n->get_arg(0); auto arg0 = n->get_arg(0);
auto arg1 = n->get_arg(1); auto arg1 = n->get_arg(1);
if (m_context.find_assignment(arg0) == l_false) { if (m_context.find_assignment(arg0) == l_false) {