Spurious pointer-out-of-bounds-error

[Novak756]

Hi,
I was looking into the following program (let's call it test.c) and I believe that CBMC is giving an imprecise pointer error.

#include<assert.h>
extern void __VERIFIER_error(void);
extern unsigned long __VERIFIER_nondet_ulong(void);
extern long __VERIFIER_nondet_long(void);
#define ARRAY_SIZE 2

int main(){
	const unsigned long index1 = __VERIFIER_nondet_ulong();
	const unsigned long index2 = __VERIFIER_nondet_ulong();
	long array[ARRAY_SIZE][ARRAY_SIZE] = {{__VERIFIER_nondet_long(),__VERIFIER_nondet_long()},{__VERIFIER_nondet_long(),__VERIFIER_nondet_long()}};
	long result[ARRAY_SIZE] = {0,0};
	if((index1  <  ARRAY_SIZE)  &&  (0ULL  <=  index1)){
		if((index2  <  ARRAY_SIZE)  &&  (0ULL  <=  index2)){
			if((((((long *)array)+(ARRAY_SIZE*index1))[index2])  <=  1ULL)  &&  (0ULL  <=  ((((long *)array)+(ARRAY_SIZE*index1))[index2]))){
				if((((long *)result)[(unsigned long)((((long *)array)+(ARRAY_SIZE*index1))[index2])]) != 0U){
					__VERIFIER_error();
                }
            }
        }
    }
    return 0;
}

the first three ifs should ensure that the following array accesses are in range (in this case between 0 and 1, as we have size 2).
Also CBMC is able to prove that the result of the access cannot be different from 0, which it could be if the access were out of bounds.
Or am I overlooking something?

CBMC version: Built from commit 13a452d
Operating system: Linux (Ubuntu 20.04)
Exact command line resulting in the issue: cbmc --pointer-check --bounds-check test.c
What behaviour did you expect: VERIFICATION SUCCESSFUL
What happened instead:

[main.pointer_dereference.8] line 13 dereference failure: pointer outside object bounds in ((signed long int *)result)[((signed long int *)array + (signed long int)((unsigned long int)2 * index1))[(signed long int)index2]]: FAILURE