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

Modern C++: Add std::span overload for mk_or, adopt std::clamp, optimize stream output (#8507)

Browse source 
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-02-06 11:54:06 +00:00 • committed by Nikolaj Bjorner
parent ff7898ef7c
commit adf72f2a66
10 changed files with 19 additions and 20 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/smt/dyn_ack.cpp
View file

@ -155,8 +155,7 @@ namespace smt {
proof* ps[2] = { p3, p4 };
p5 = m.mk_unit_resolution(2, ps);
SASSERT(m.get_fact(p5) == m.mk_false());
expr* eqs[3] = { m.mk_not(m_eq1), m.mk_not(m_eq2), m_eq3 };
expr_ref conclusion(m.mk_or(3, eqs), m);
expr_ref conclusion(m.mk_or(m.mk_not(m_eq1), m.mk_not(m_eq2), m_eq3), m);
p6 = m.mk_lemma(p5, conclusion);
return p6;
}