mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-07-29 07:27:57 +00:00
Code Activity

compile warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-07-21 16:20:08 -07:00
parent 1d1a01c6cc
commit fc51067207
2 changed files with 3 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

2
src/ast/euf/ho_matcher.h
View file

@ -369,8 +369,8 @@ namespace euf {
ho_matcher(ast_manager& m, trail_stack &trail) : ho_matcher(ast_manager& m, trail_stack &trail) :
m(m), m(m),
m_subst(m),
m_trail(trail), m_trail(trail),
m_subst(m),
m_goals(*this, m), m_goals(*this, m),
m_unitary(m), m_unitary(m),
m_rewriter(m), m_rewriter(m),

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

@ -509,7 +509,6 @@ namespace euf {
body.push_back(x); body.push_back(x);
} }
else if (m.is_or(f)) { else if (m.is_or(f)) {
auto a = to_app(f);
for (auto arg : *to_app(f)) { for (auto arg : *to_app(f)) {
if (m.is_eq(arg)) { if (m.is_eq(arg)) {
if (head) if (head)
@ -973,15 +972,14 @@ namespace euf {
if (!m_closures.find(q, clos)) if (!m_closures.find(q, clos))
return expr_ref(q, m); return expr_ref(q, m);
expr* body = clos.second; expr* body = clos.second;
auto n = m_egraph.find(body); SASSERT(m_egraph.find(body));
SASSERT(n);
#if 0 #if 0
verbose_stream() << "class of " << mk_pp(body, m) << "\n"; verbose_stream() << "class of " << mk_pp(body, m) << "\n";
for (auto s : euf::enode_class(n)) { for (auto s : euf::enode_class(n)) {
verbose_stream() << mk_pp(s->get_expr(), m) << "\n"; verbose_stream() << mk_pp(s->get_expr(), m) << "\n";
} }
#endif #endif
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)) {