Z3 doesn't handle some #Not (#Exists ...) predicates

[ana-pantilie]

High priority

Z3 is unable to refute predicates like:

#Not ( 
	#Exists ITER_COUNT_F:Int . 
		     { VV6__data_3c5818c8:Bytes [ 32 *Int ?ITER_COUNT_F:Int .. #sizeByteArray ( VV6__data_3c5818c8:Bytes ) -Int 32 *Int ?ITER_COUNT_F:Int ] #Equals VV6__data_3c5818c8:Bytes [ 32 *Int ITER_COUNT_F:Int .. #sizeByteArray ( VV6__data_3c5818c8:Bytes ) -Int 32 *Int ITER_COUNT_F:Int ] } 
		#And { true #Equals 0 <=Int ITER_COUNT_F:Int }
		#And { true #Equals 32 *Int ITER_COUNT_F:Int <Int #sizeByteArray ( VV6__data_3c5818c8:Bytes ) }
		#And { true #Equals #sizeByteArray ( VV6__data_3c5818c8:Bytes ) <=Int 32 *Int ITER_COUNT_F:Int +Int 32 }
		#And { true #Equals -9 <Int #sizeByteArray ( VV6__data_3c5818c8:Bytes ) } 
	)
...
#And { true #Equals 0 <=Int ?ITER_COUNT_F:Int }
#And { true #Equals 32 *Int ?ITER_COUNT_F:Int <Int #sizeByteArray ( VV6__data_3c5818c8:Bytes ) }
#And { true #Equals #sizeByteArray ( VV6__data_3c5818c8:Bytes ) <=Int 32 *Int ?ITER_COUNT_F:Int +Int 32 }
...

@PetarMax suggests a heuristic which looks for witnesses in the free variables of the predicate.