Sets, lists, and maps are elementary data structures used in most programs. Program analysis tools therefore need to decide verification conditions containing variables of such types. We propose a new theory for the SMT-Lib standard as the standard format for such formulae.