JDart currently does not add constraints for array access with a symbolic index.
A solution would be to add the decisions to the constraints tree in all the *ALOAD instructions. The decisions to be added should correspond to accessing all the elements of the array (which has a fixed length), plus two additional decisions corresponding to the two cases where access is out of bounds.