[clang] [clang][analyzer] Correct SMT Layer for _BitInt cases refutations (PR #143310)

[Donát Nagy via cfe-commits]

================
@@ -0,0 +1,23 @@
+// RUN: %clang_cc1 -analyze -analyzer-checker=core -w -DNO_CROSSCHECK -verify %s
+// RUN: %clang_cc1 -analyze -analyzer-checker=core -w -analyzer-config crosscheck-with-z3=true -verify %s
+// REQUIRES: z3
+
+// The SMTConv layer did not comprehend _BitInt types (because this was an
+// evolved feature) and was crashing due to needed updates in 2 places.
+// Analysis is expected to find these cases using _BitInt without crashing.
----------------
NagyDonat wrote:

:thinking: Perhaps it's worth to keep a shorter comment like "Previously these tests were crashing because the SMTConv layer did not comprehend the _BitInt types." -- although I can deduce something like this by examining the git blame, I usually feel that these "previously this was the problem" comments are valuable for understanding the test quickly.

https://github.com/llvm/llvm-project/pull/143310