Error-call detection depends on order of array initialisation

[Novak756]

Hi, I was looking into the following program:

extern void __VERIFIER_error(void);
extern unsigned long __VERIFIER_nondet_ulong(void);

#define ARRAY_SIZE 4
unsigned long* array_store(unsigned long a[],int p,int v){ //Stores a value in an array
    a[p] = v;
    return a;
}
int array_comp(unsigned long a1[], unsigned long a2[]){ //Element-wise comparison
    for(int i = 0; i < ARRAY_SIZE; i++){
    	if(a1[i] != a2[i]) return 0;
    }
    return 1;
}
void init(unsigned long array[]){ //Initialise array explicitly
    for(int i = 0; i < ARRAY_SIZE; i++){
    	array[i] = __VERIFIER_nondet_ulong();
    }
}

int main(){
	unsigned long b[ARRAY_SIZE];
	init(b);
	unsigned long a[ARRAY_SIZE];
	init(a);
	unsigned long a2[ARRAY_SIZE];
	init(a2);
	unsigned long a3[ARRAY_SIZE];
	init(a3);
	unsigned long a4[ARRAY_SIZE];
	init(a4);
	unsigned long a5[ARRAY_SIZE];
	init(a5);
	unsigned long a6[ARRAY_SIZE];
	init(a6);
	unsigned long a7[ARRAY_SIZE];
	init(a7);
	unsigned long a8[ARRAY_SIZE];
	init(a8);
	unsigned long a9[ARRAY_SIZE];
	init(a9);
	unsigned long a10[ARRAY_SIZE];
	init(a10);
	if(((array_comp((a),(a7))) && (array_comp((a),(a8)))) && ((int) ((int)((array_store((array_store((a8),((unsigned int) 2),((a)[((unsigned int) 1)]))),((unsigned int) 1),((unsigned char) (((int)((a)[((unsigned int) 2)])) >> 0 & 255))))[((unsigned int) 3)])) < (int) ((int)((array_store((array_store((a7),((unsigned int) 2),((a)[((unsigned int) 1)]))),((unsigned int) 1),((unsigned char) (((int)((a)[((unsigned int) 2)])) >> 0 & 255))))[((unsigned int) 2)])))){
		if((((array_comp((a),(a2))) && (array_comp((a),(a4)))) && (array_comp((a),(a3)))) && ((int) ((int)((array_store((array_store((a3),((unsigned int) 2),((a)[((unsigned int) 1)]))),((unsigned int) 1),((unsigned char) (((int)((a)[((unsigned int) 2)])) >> 0 & 255))))[((unsigned int) 3)])) < (int) ((int)((array_store((array_store((array_store((a2),((unsigned int) 2),((a)[((unsigned int) 1)]))),((unsigned int) 1),((unsigned char) (((int)((a)[((unsigned int) 2)])) >> 0 & 255)))),((unsigned int) 3),((array_store((array_store((a2),((unsigned int) 2),((a)[((unsigned int) 1)]))),((unsigned int) 1),((unsigned char) (((int)((a)[((unsigned int) 2)])) >> 0 & 255))))[((unsigned int) 2)])))[((unsigned int) 1)])))){
			if((array_comp((a),(a10))) && (!((int) ((int)((a)[((unsigned int) 2)])) < (int) ((int)((array_store((a10),((unsigned int) 2),((a)[((unsigned int) 1)])))[((unsigned int) 0)]))))){
				if(((((array_comp((a),(a9))) && (array_comp((a),(a5)))) && (array_comp((a),(b)))) && (array_comp((a),(a6)))) && ((int) ((int)((array_store((array_store((a6),((unsigned int) 2),((a)[((unsigned int) 1)]))),((unsigned int) 1),((unsigned char) (((int)((a)[((unsigned int) 2)])) >> 0 & 255))))[((unsigned int) 3)])) < (int) ((int)((array_store((array_store((array_store((array_store((a9),((unsigned int) 2),((a)[((unsigned int) 1)]))),((unsigned int) 1),((unsigned char) (((int)((a)[((unsigned int) 2)])) >> 0 & 255)))),((unsigned int) 3),((array_store((array_store((a9),((unsigned int) 2),((a)[((unsigned int) 1)]))),((unsigned int) 1),((unsigned char) (((int)((a)[((unsigned int) 2)])) >> 0 & 255))))[((unsigned int) 2)]))),((unsigned int) 2),((array_store((array_store((array_store((a9),((unsigned int) 2),((a)[((unsigned int) 1)]))),((unsigned int) 1),((unsigned char) (((int)((a)[((unsigned int) 2)])) >> 0 & 255)))),((unsigned int) 3),((array_store((array_store((a9),((unsigned int) 2),((a)[((unsigned int) 1)]))),((unsigned int) 1),((unsigned char) (((int)((a)[((unsigned int) 2)])) >> 0 & 255))))[((unsigned int) 2)])))[((unsigned int) 1)])))[((unsigned int) 0)])))){
					__VERIFIER_error(); 
				}
			}
		}
	}
    return 0;
}

the error should be reachable, and is found if symbiotic is run with default settings.
However, when running with --explicit-symbolic fails to find the error.
Curiously, running init(a) before init(b), or removing the (array_comp((a),(b)))) call in the last if causes the solver to find the error again (even though this should not affect the semantics of the program, as b is not referenced anywhere else).

Version I am running is:
version: 8.0.0
LLVM version: 10.0.1
symbiotic -> 7ba60a1 (Release)
dg -> 4b374e5dba6e9a1d76191cd76ae8bad42a977171 (Release)
sbt-slicer -> 9636fad069d4fdcb03150e287a14887f7b02b2ad (Release)
sbt-instrumentation -> 9ab2a5930e23a90ecb41fa5f069709ef372991b1 (Release)
klee -> b71309b475b494cbab3b5580e31bed941dd02687 (Release)