Decision Procedures for Flat Array Properties