Homebrew upgrade from Z3 4.15.4 to 4.16.0 failed on macOS 12 during
`src/ast/ast.cpp` compilation because `obj_map::key_data` was used with
`(key, value)` construction but only implicit constructors existed. This
surfaced at `m_poly_roots.insert(new_node, new_node)` and similar map
operations.
- **Root cause addressed**
- `obj_map<Key, Value>::key_data` relied on implicit constructors, which
are insufficient under stricter toolchains when `key_data(k, v)` /
`key_data(k)` are instantiated via `obj_map` helpers.
- **Code change (minimal, targeted)**
- Added explicit struct constructors in `src/util/obj_hashtable.h` for:
- default initialization
- key-only construction (`key_data(Key* k)`)
- key + lvalue value (`key_data(Key* k, Value const& v)`)
- key + rvalue value (`key_data(Key* k, Value&& v)`)
- No behavioral changes to map semantics; this only makes existing call
sites well-formed across compilers.
- **Example of the change**
```c++
struct key_data {
Key * m_key = nullptr;
Value m_value;
key_data() = default;
key_data(Key* k): m_key(k) {}
key_data(Key* k, Value const& v): m_key(k), m_value(v) {}
key_data(Key* k, Value&& v): m_key(k), m_value(std::move(v)) {}
// ...
};
```
---------
Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
