mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-06-07 17:40:54 +00:00
Code Activity

Fixed the assertion violation in mpz.cpp:602 when running with -tr:arith.

Browse source 
**Root cause**: `vector::resize(SZ s, Args args...)` in `src/util/vector.h` took `args` by value and used `std::forward<Args>(args)` in a loop. The first iteration moved from `args`, leaving all subsequent elements with a moved-from state (`rational{0/0}` instead of
`rational{0/1}`). This corrupted the coefficient vector in the pretty printer, causing a division-by-zero assertion when multiplying.

**Fix**: Changed `resize` to take `Args const& args` and copy-construct each element instead of forwarding/moving.
This commit is contained in:
Lev Nachmanson 2026-03-11 12:42:39 -10:00
parent 235448d929
commit 8e47c0d842
1 changed files with 2 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/util/vector.h
View file

@ -494,7 +494,7 @@ public:
} }
template<typename Args> template<typename Args>
void resize(SZ s, Args args...) { void resize(SZ s, Args const& args) {
SZ sz = size(); SZ sz = size();
if (s <= sz) { shrink(s); return; } if (s <= sz) { shrink(s); return; }
while (s > capacity()) { while (s > capacity()) {
@ -505,7 +505,7 @@ public:
iterator it = m_data + sz; iterator it = m_data + sz;
iterator end = m_data + s; iterator end = m_data + s;
for (; it != end; ++it) { for (; it != end; ++it) {
new (it) T(std::forward<Args>(args)); new (it) T(args);
} }
} }