mirror of
https://github.com/Z3Prover/z3
synced 2025-04-07 18:05:21 +00:00
fix compiler warnings under clang (#5839)
This commit is contained in:
parent
09da87dc85
commit
9cf50766a6
|
@ -687,7 +687,7 @@ public:
|
|||
return ensure_euf()->user_propagate_register_expr(e);
|
||||
}
|
||||
|
||||
void user_propagate_register_created(user_propagator::created_eh_t& r) {
|
||||
void user_propagate_register_created(user_propagator::created_eh_t& r) override {
|
||||
ensure_euf()->user_propagate_register_created(r);
|
||||
}
|
||||
|
||||
|
|
|
@ -1458,7 +1458,7 @@ namespace pb {
|
|||
return nullptr;
|
||||
}
|
||||
rational weight(0);
|
||||
for (auto const [w, l] : wlits)
|
||||
for (auto const &[w, l] : wlits)
|
||||
weight += w;
|
||||
if (weight < k) {
|
||||
if (lit == sat::null_literal)
|
||||
|
|
|
@ -1563,6 +1563,7 @@ public:
|
|||
return FC_CONTINUE;
|
||||
}
|
||||
for (expr* e : m_not_handled) {
|
||||
(void) e; // just in case TRACE() is a no-op
|
||||
TRACE("arith", tout << "unhandled operator " << mk_pp(e, m) << "\n";);
|
||||
st = FC_GIVEUP;
|
||||
}
|
||||
|
|
|
@ -110,7 +110,6 @@ protected:
|
|||
void operator()(quantifier * q) {
|
||||
m_stats["quantifiers"]++;
|
||||
SASSERT(is_app(q->get_expr()));
|
||||
app * body = to_app(q->get_expr());
|
||||
switch (q->get_kind()) {
|
||||
case forall_k:
|
||||
m_stats["forall-variables"] += q->get_num_decls();
|
||||
|
|
Loading…
Reference in a new issue