Combining --undefined-are-pure and --exit-on-error causes missed error

[Novak756]

Hi, given the following program

extern void __VERIFIER_error(void);

extern unsigned char __VERIFIER_nondet_uchar(void);
extern unsigned short __VERIFIER_nondet_ushort(void);
extern unsigned int __VERIFIER_nondet_uint(void);


int main(){
	unsigned char T1_1900 = __VERIFIER_nondet_uchar();
	unsigned char T1_2310 = __VERIFIER_nondet_uchar();
	unsigned char T1_2300 = __VERIFIER_nondet_uchar();
	unsigned char T1_2650 = __VERIFIER_nondet_uchar();
	unsigned char T1_2649 = __VERIFIER_nondet_uchar();
	unsigned short T2_1908 = __VERIFIER_nondet_ushort();
	unsigned char T1_2651 = __VERIFIER_nondet_uchar();
	unsigned short T2_2649 = __VERIFIER_nondet_ushort();
	unsigned short T2_2716 = __VERIFIER_nondet_ushort();
	unsigned char T1_2309 = __VERIFIER_nondet_uchar();
	unsigned char T1_2707 = __VERIFIER_nondet_uchar();
	unsigned char T1_1901 = __VERIFIER_nondet_uchar();
	unsigned char T1_1903 = __VERIFIER_nondet_uchar();
	unsigned char T1_1902 = __VERIFIER_nondet_uchar();
	unsigned char T1_1899 = __VERIFIER_nondet_uchar();
	unsigned int T4_1900 = __VERIFIER_nondet_uint();
	unsigned char T1_2664 = __VERIFIER_nondet_uchar();
	unsigned short T2_2309 = __VERIFIER_nondet_ushort();
	unsigned char T1_2647 = __VERIFIER_nondet_uchar();
	
	if((unsigned int) ((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int)(T1_1899)) + ((unsigned int) 1))) + ((unsigned int) 4270364))) + ((unsigned int)(T2_1908)))) + ((unsigned int) 6))) + ((unsigned int) (((unsigned int)(T1_2300)) + ((unsigned int) 1))))) + ((unsigned int) 2))) + ((unsigned int)(T2_2309)))) + ((unsigned int) 6))) + ((unsigned int) (((unsigned int)(T1_2647)) + ((unsigned int) 1))))) + ((unsigned int) 2))) + ((unsigned int)(T2_2649)))) + ((unsigned int) 6))) + ((unsigned int) (((unsigned int)(T1_2707)) + ((unsigned int) 1))))) + ((unsigned int) 2))) <= (unsigned int) ((unsigned int) 4271190)){
		if((unsigned int) ((unsigned int) (((unsigned int)(T1_2664)) + ((unsigned int) 1))) <= (unsigned int) ((unsigned int) (((unsigned int)(T2_2649)) + (((unsigned int) 4294967295) - ((unsigned int)(T1_2651)))))){
			if((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int) (((unsigned int)(T1_1899)) + ((unsigned int) 1))) + ((unsigned int) 4270364))) + ((unsigned int)(T2_1908)))) + ((unsigned int) 6))) + ((unsigned int) (((unsigned int)(T1_2300)) + ((unsigned int) 1))))) + ((unsigned int) 2))) + ((unsigned int)(T2_2309)))) + ((unsigned int) 6))) + ((unsigned int) (((unsigned int)(T1_2647)) + ((unsigned int) 1))))) + ((unsigned int) 2))) + ((unsigned int)(T2_2649)))) + ((unsigned int) 6))) + ((unsigned int) (((unsigned int)(T1_2707)) + ((unsigned int) 1))))) + ((unsigned int) 2))) + ((unsigned int)(T2_2716)))) - ((unsigned int) 4270344)) <= (unsigned int) ((unsigned int) 846)){
				if((T2_2309) == ((((unsigned short)(T1_2310)) << ((unsigned short) 8)) | ((unsigned short)(T1_2309)))){
					if((unsigned int) ((unsigned int) 8) <= (unsigned int) ((unsigned int)(T1_1899))){
						__VERIFIER_error();
					}
				}
			}
		}
	}
    
    return 0;
}

Symbiotic fails to find the error when running with --undefined-are-pure and --exit-on-error, but finds the error when only --undefined-are-pure is set.
Seems like these flags should be unrelated though?
I built symbiotic with the install-ubuntu.sh script, the full Dockerfiles are attached.