mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-02-22 16:27:37 +00:00
Code Activity

Add initializer_list overloads and update all call sites

Browse source 
Co-authored-by: NikolajBjorner <3085284+NikolajBjorner@users.noreply.github.com>
This commit is contained in:
copilot-swe-agent[bot] 2026-02-16 01:27:08 +00:00 • committed by Nikolaj Bjorner
parent fbda3029fd
commit d958036711
5 changed files with 20 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

12
src/tactic/goal.cpp
View file

@ -549,10 +549,8 @@ void goal::elim_redundancies() {
continue;
if (pos_lits.is_marked(atom)) {
proof * p = nullptr;
if (proofs_enabled()) {
proof * prs[2] = { pr(get_idx(atom)), pr(i) };
p = m().mk_unit_resolution(2, prs);
}
if (proofs_enabled())
p = m().mk_unit_resolution({ pr(get_idx(atom)), pr(i) });
expr_dependency_ref d(m());
if (unsat_core_enabled())
d = m().mk_join(dep(get_idx(atom)), dep(i));
@ -566,10 +564,8 @@ void goal::elim_redundancies() {
continue;
if (neg_lits.is_marked(f)) {
proof * p = nullptr;
if (proofs_enabled()) {
proof * prs[2] = { pr(get_not_idx(f)), pr(i) };
p = m().mk_unit_resolution(2, prs);
}
if (proofs_enabled())
p = m().mk_unit_resolution({ pr(get_not_idx(f)), pr(i) });
expr_dependency_ref d(m());
if (unsat_core_enabled())
d = m().mk_join(dep(get_not_idx(f)), dep(i));