False precondition for refinement of global variable alignment

[can-leh-emmtrix]

Increasing the alignment of a global variable should be a refinement. Alive2 already proves this is in fact a refinement when the size of the global variable is a multiple of the new alignment. However, when the size of the global is not a multiple of the new alignment, the precondition is false:

****************************************
WARNING: Source function is always UB.
It can be refined by any target function.
Please make sure this is what you wanted.
****************************************

ERROR: Precondition is always false

Source:

@global = external global [100 x i8], align 4

define i32 @test() {
entry:
  %0 = load i32, ptr @global, align 4
  ret i32 %0
}

Target:

@global = external global [100 x i8], align 8

define i32 @test() {
entry:
  %0 = load i32, ptr @global, align 4
  ret i32 %0
}

Note that the only difference between the source and target is changing the align of @global from 4 to 8.

The size of the global variable is rounded up to the next multiple of its alignment here.
As the resulting size is different for source and target, the precondition now contains the axioms (= (_ bv100 8) (blk_size (_ bv0 1))) and (= (blk_size (_ bv0 1)) (_ bv104 8)) making it always false.

Related: #1028