mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-01-27 12:28:43 +00:00
Code Activity

Refactor dyn_ack propagate_eh to use structured bindings (#8317)

Browse source 
* Initial plan

* Refactor dyn_ack propagate_eh to use C++17 structured bindings

Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
Copilot 2026-01-24 10:17:27 -08:00 • committed by GitHub
parent 39b9038449
commit 1cf9ba152b
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 4 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/dyn_ack.cpp
View file

@ -379,16 +379,16 @@ namespace smt {
}
unsigned max_instances = static_cast<unsigned>(m_context.get_num_conflicts() * m_params.m_dack_factor);
while (m_num_instances < max_instances && m_qhead < m_to_instantiate.size()) {
app_pair & p = m_to_instantiate[m_qhead];
auto& [first, second] = m_to_instantiate[m_qhead];
m_qhead++;
m_num_instances++;
instantiate(p.first, p.second);
instantiate(first, second);
}
while (m_num_instances < max_instances && m_triple.m_qhead < m_triple.m_to_instantiate.size()) {
app_triple & p = m_triple.m_to_instantiate[m_triple.m_qhead];
auto& [first, second, third] = m_triple.m_to_instantiate[m_triple.m_qhead];
m_triple.m_qhead++;
m_num_instances++;
instantiate(p.first, p.second, p.third);
instantiate(first, second, third);
}
}