Prevent ref count from reaching zero in BV instantiator

The `normalize*` methods in `ceg_bv_instantiator_utils.{h,cpp}` each modify a
map that marks terms in which `pv` occurs. The map was mapping `TNode`s to
`bool`s. The problem was that the keys in the map could be new terms that
needed to be kept alive for the map to remain valid. When compiling CVC4 with
Clang under macOS, `theory_quantifiers_bv_instantiator_white` and
`theory_quantifiers_bv_inverter_white` were failing because the reference count
of keys in the map reached zero. Generally, the critical keys are contained in
the result of the functions and kept alive by the `visited` stack in
`rewriteAssertionForSolvePv()`. The unit test
`theory_quantifiers_bv_instantiator_white` did not keep the results alive,
resulting in reference counts reaching zero. However, the failure of
`theory_quantifiers_bv_inverter_white` shows that the issue is not limited to
the unit tests of the `normalize*` methods. To avoid this issue, this commit
changes the map to use `Node` keys instead (so the map itself keeps the keys
alive).

0 files changed, 0 insertions, 0 deletions