mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-07-14 19:15:41 +00:00
Code Activity

fix warnings

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2026-07-12 16:45:24 -07:00
parent f7afe8e025
commit 606a06fa5f
1 changed files with 2 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/smt/smt_quantifier.cpp
View file

@ -664,7 +664,6 @@ namespace smt {
quantifier_manager_plugin * mk_fresh() override { return alloc(default_qm_plugin); }
void on_ho_match(euf::ho_subst &s) {
ast_manager &m = m_context->get_manager();
auto &st = m_ho_state;
auto *hoq = st.m_q;
auto *q = m_ho_matcher->hoq2q(hoq);
@ -679,7 +678,6 @@ namespace smt {
}
void consume_ho_match(quantifier * q, expr_ref_vector const& binding) {
ast_manager &m = m_context->get_manager();
auto &st = m_ho_state;
// Create enodes for the refined bindings and add instance
ptr_buffer<enode> new_bindings;
@ -700,7 +698,8 @@ namespace smt {
max_gen = gen;
}
TRACE(ho_matching,
TRACE(ho_matching,
ast_manager &m = m_context->get_manager();
tout << "ho_match refined for " << mk_pp(q, m) << "\n";
for (unsigned i = 0; i < new_bindings.size(); ++i)
tout << " binding[" << i << "] = " << mk_bounded_pp(new_bindings[i]->get_expr(), m) << "\n";);
@ -725,7 +724,6 @@ namespace smt {
for (unsigned i = 0; i < num_bindings; ++i)
s.push_back(bindings[i]->get_expr());
unsigned num_instances = m_stat_ho_instances;
m_ho_state.m_q = qa;
m_ho_state.m_pat = pat;
m_ho_state.m_num_bindings = num_bindings;