Improve performance and language support of memory initialization checks

[artemagvanian]

This is a follow-up PR for #3264 in the making, a part of the larger work towards #3300.

This PR introduces:

• [x] Use of demonic non-determinism (prophecy variables) to improve memory initialization checks performance
• [x] Tests for memory initialization checks when using compiler intrinsics
• [x] Memory initialization checks in test cases from standard library
• [ ] ...

By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses.