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

Add std::initializer_list overloads for BV and arith operations (#8467)

Browse source 
* Initial plan

* Add std::initializer_list overloads for BV and arith functions

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

* Update call sites to use initializer_list format for BV and arith functions

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-02-02 10:00:13 -08:00 • committed by Nikolaj Bjorner
parent 17580362e6
commit 957d548bdb
5 changed files with 26 additions and 38 deletions
Download patch file Download diff file Expand all files Collapse all files

3
src/tactic/fd_solver/smtfd_solver.cpp
View file

@ -188,8 +188,7 @@ namespace smtfd {
}
unsigned n = (m_rand() << 16) | m_rand();
expr* num = m_butil.mk_numeral(n, bw);
expr* es[2] = { num, m.mk_fresh_const(name, m_butil.mk_sort(bw)) };
expr* e = m_butil.mk_bv_xor(2, es);
expr* e = m_butil.mk_bv_xor({num, m.mk_fresh_const(name, m_butil.mk_sort(bw))});
return m_butil.mk_concat(e, m_butil.mk_numeral(0, 24 - bw));
}
}