Alive2 doesn't support verification of optimizations that use inter-procedural analyses.
Right now, clang uses GlobalsAA by default and there's no way to disable it. This leads to Alive2 producing false positives.
Example:
file.c:
static int x;
int f() {
  x = 0;
  *p = 1;
  x = 2;
  return *p;
}This file.c right now compiles to:
define i32 @f(ptr nocapture noundef %p) {
  store i32 1, ptr %p, align 4
  store i1 true, ptr @x, align 4
  ret i32 1
}without globalsaa:
$ clang -S -emit-llvm -o - -O3 file.c -mllvm -enable-global-analyses=0
define i32 @f(ptr nocapture noundef %p) {
  store i32 1, ptr %p, align 4
  store i1 true, ptr @x, align 4
  %0 = load i32, ptr %p, align 4
  ret i32 %0
}
Make the var name EnableGlobalAnalyses to match the option name?