Memory allocation exception in external SMT parser

[Bo-Yuan-Huang]

Describe the bug There are (nondeterministically) memory allocation exception when parsing STM formulas.

To Reproduce Steps to reproduce the behavior:

1. Build with default configuration and Release build type
2. Run unit test TestVlgVerifInvSyn.LoadInvFromBeginning
3. (May need to repeat several times to trigger the issue)

Environment (please complete the following information):

• OS: OSX 15 (Catalina)
• Compiler: Xcode 11.4.1
• Other dependencies: Release build

Additional context First issued in #188. Multiple tests involving the smt-parser have the same issue, TestVlgVerifInvSyn.LoadInvFromBeginning is one of the set.

Error message:

unit_tests(59330,0x10937edc0) malloc: can't allocate region
:*** mach_vm_map(size=3758289336431292416, flags: 100) failed (error code=3)
unit_tests(59330,0x10937edc0) malloc: *** set a breakpoint in malloc_error_break to debug
unknown file: Failure
C++ exception with description "std::bad_alloc" thrown in the test body.

[Bo-Yuan-Huang]

Tracing the root cause, the exception is thrown here: https://github.com/Bo-Yuan-Huang/ILAng/blob/a58890818e2b8df5c0b9fc4cc48bd07501b33ccc/src/smt-inout/chc_inv_in.cc#L926

[Bo-Yuan-Huang]

This issue is only observed in OSX with Release build. The ILANG_BUILD_INVSYN is temporarily set OFF in the corresponding CI. Remember to turn on once fixed. https://github.com/Bo-Yuan-Huang/ILAng/blob/a58890818e2b8df5c0b9fc4cc48bd07501b33ccc/azure-pipelines.yml#L52

[zhanghongce]

Thanks for letting me know! I think the root cause might be that I'm doing some hacky things around the pointers which assumes a fixed memory layout of the class members, however the optimization in release mode will not guarantee that. Will look into it. Thanks!