Memory corruption on Mac version of 4.12.5

[parno]

Each of the two attached SMT2 files (generated by Verus) appear to cause memory corruption on the Mac version of Z3 4.12.5 (z3-4.12.5_version-arm64-osx-11.0). In particular, each cause Z3 to report (:reason-unknown "u$??") where the string's contents vary randomly on each run. When we run the first one (but not the second one) on the Windows version of Z3 4.12.5, it reports (:reason-unknown "Overflow encountered when expanding vector"), which might point at the source of the issue on the Mac.

This problem doesn't manifest with the latest Mac version of Z3 (4.15.4), so the underlying bug may have been addressed, but I wanted to report the issue in case it's still present and just not tickled by this exact set of queries.

cc @Chris-Hawblitzel

z3-memory-corruption1.smt2.txt

z3-memory-corruption2.smt2.txt